mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-08-07 06:55:46 +00:00
allaun
4ca1289347
SilverSight modules moved from Semantics/Semantics/SilverSight/ to SilverSight/SilverSight/ (separate directory, same lake project). Changes: - SilverSight Lean modules: Schema, WireFormat, ProductSchema, ProductWireFormat, Receipt, Bind → 0-Core-Formalism/lean/SilverSight/ - Imports updated: Semantics.SilverSight.* → SilverSight.* - Namespace updated: Semantics.SilverSight → SilverSight - Cross-project imports preserved: Semantics.FixedPoint, open Semantics.FixedPoint - lakefile.toml: SilverSight lean_lib now uses srcDir = ../SilverSight - AGENTS.md: READ-ONLY notice added — Research Stack is archived, all new formal work goes to SilverSight - SilverSight/AGENTS.md: clean-slate operating contract Build: SilverSight 3307 jobs, 0 errors Build: Compiler 3314 jobs, 0 errors
68 lines
2.5 KiB
Text
68 lines
2.5 KiB
Text
import Semantics.FixedPoint
|
||
|
||
namespace SilverSight
|
||
|
||
open Semantics.FixedPoint
|
||
|
||
/-- A Schema describes the wire-level layout of a type:
|
||
- `byteSize`: the number of bytes in the wire representation
|
||
- `wellFormed`: a predicate that must hold for valid values -/
|
||
class Schema (α : Type) where
|
||
byteSize : Nat
|
||
wellFormed : α → Bool
|
||
|
||
@[simp] theorem Schema.byteSize_nonneg [Schema α] : 0 ≤ Schema.byteSize α := by
|
||
exact Nat.zero_le _
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §1 Basic Schema instances
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
instance : Schema UInt8 where
|
||
byteSize := 1
|
||
wellFormed := fun _ => true
|
||
|
||
@[simp] theorem uint8_byteSize : Schema.byteSize UInt8 = 1 := rfl
|
||
|
||
instance : Schema Bool where
|
||
byteSize := 1
|
||
wellFormed := fun _ => true
|
||
|
||
@[simp] theorem bool_byteSize : Schema.byteSize Bool = 1 := rfl
|
||
|
||
instance : Schema UInt32 where
|
||
byteSize := 4
|
||
wellFormed := fun _ => true
|
||
|
||
@[simp] theorem uint32_byteSize : Schema.byteSize UInt32 = 4 := rfl
|
||
|
||
instance : Schema UInt64 where
|
||
byteSize := 8
|
||
wellFormed := fun _ => true
|
||
|
||
@[simp] theorem uint64_byteSize : Schema.byteSize UInt64 = 8 := rfl
|
||
|
||
instance : Schema Q16_16 where
|
||
byteSize := 4
|
||
wellFormed := fun _ => true
|
||
|
||
@[simp] theorem q16_16_byteSize : Schema.byteSize Q16_16 = 4 := rfl
|
||
|
||
instance : Schema Q0_16 where
|
||
byteSize := 2
|
||
wellFormed := fun _ => true
|
||
|
||
@[simp] theorem q0_16_byteSize : Schema.byteSize Q0_16 = 2 := rfl
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §2 #eval witnesses
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
#eval Schema.byteSize UInt8 -- expected: 1
|
||
#eval Schema.byteSize Bool -- expected: 1
|
||
#eval Schema.byteSize UInt32 -- expected: 4
|
||
#eval Schema.byteSize UInt64 -- expected: 8
|
||
#eval Schema.byteSize Q16_16 -- expected: 4
|
||
#eval Schema.byteSize Q0_16 -- expected: 2
|
||
|
||
end SilverSight
|