mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-10 18:00:34 +00:00
allaun
4f7c554981
New modules in formal/SilverSight/: - Schema.lean: Schema class with 6 type instances - WireFormat.lean: WireFormat structure + Layout enum - ProductSchema.lean: Schema (α × β) instance - ProductWireFormat.lean: Row-major pair encoders - Receipt.lean: Receipt structure + GateType enum - Bind.lean: bindReceipt composition primitive Build: 3307 jobs, 0 errors (from Research Stack lake build SilverSight) All modules use Semantics.FixedPoint cross-project import.
67 lines
3 KiB
Text
67 lines
3 KiB
Text
import SilverSight.WireFormat
|
||
import SilverSight.ProductSchema
|
||
|
||
namespace SilverSight
|
||
|
||
open Semantics.FixedPoint
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §1 Row-major wire format for pairs
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- Row-major wire format for (UInt8 × Bool). -/
|
||
def uint8BoolRowMajor : WireFormat (UInt8 × Bool) Layout.rowMajor where
|
||
encode := fun (a, b) => ByteArray.mk #[a, if b then 1 else 0]
|
||
decode := fun bs =>
|
||
match bs.data.toList with
|
||
| [a, b] => some (a, b != 0)
|
||
| _ => none
|
||
encode_size := by intro (a, b); rfl
|
||
roundTrip := by
|
||
intro (a, b)
|
||
simp [ByteArray.mk, ByteArray.size]
|
||
cases b <;> decide
|
||
|
||
#eval uint8BoolRowMajor.encode (42, true) -- expected: ByteArray [42, 1]
|
||
#eval uint8BoolRowMajor.decode (uint8BoolRowMajor.encode (42, true)) -- expected: some (42, true)
|
||
|
||
/-- Row-major wire format for (UInt8 × UInt8). -/
|
||
def uint8PairRowMajor : WireFormat (UInt8 × UInt8) Layout.rowMajor where
|
||
encode := fun (a, b) => ByteArray.mk #[a, b]
|
||
decode := fun bs =>
|
||
match bs.data.toList with
|
||
| [a, b] => some (a, b)
|
||
| _ => none
|
||
encode_size := by intro (a, b); rfl
|
||
roundTrip := by
|
||
intro (a, b)
|
||
simp [ByteArray.mk, ByteArray.size]
|
||
|
||
#eval uint8PairRowMajor.encode (42, 7) -- expected: ByteArray [42, 7]
|
||
#eval uint8PairRowMajor.decode (uint8PairRowMajor.encode (42, 7)) -- expected: some (42, 7)
|
||
|
||
/-- Row-major wire format for (Bool × Bool). -/
|
||
def boolPairRowMajor : WireFormat (Bool × Bool) Layout.rowMajor where
|
||
encode := fun (a, b) => ByteArray.mk #[if a then 1 else 0, if b then 1 else 0]
|
||
decode := fun bs =>
|
||
match bs.data.toList with
|
||
| [a, b] => some (a != 0, b != 0)
|
||
| _ => none
|
||
encode_size := by intro (a, b); rfl
|
||
roundTrip := by
|
||
intro (a, b)
|
||
simp [ByteArray.mk, ByteArray.size]
|
||
cases a <;> cases b <;> decide
|
||
|
||
#eval boolPairRowMajor.encode (true, false) -- expected: ByteArray [1, 0]
|
||
#eval boolPairRowMajor.decode (boolPairRowMajor.encode (true, false)) -- expected: some (true, false)
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §2 #eval witnesses
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
#eval uint8BoolRowMajor.encode (42, true) -- expected: ByteArray [42, 1]
|
||
#eval uint8BoolRowMajor.decode (ByteArray.mk #[42, 1]) -- expected: some (42, true)
|
||
#eval Schema.byteSize (UInt8 × Bool) -- expected: 2
|
||
|
||
end SilverSight
|