mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
3504bca392
Implements the YaFF-inspired separation of schema, layout, and access pattern
in Core/SilverSight/Semantics/:
- Schema.lean: fixed-size Schema typeclass with byteSize and wellFormed.
- Layout.lean: Layout enum, AccessProfile cost model, and cost-based selector
with an ε-suboptimality theorem.
- WireFormat.lean: certified encode/decode/roundTrip/encode_size structure.
- View.lean: zero-copy View with address-arithmetic invariant.
- LayoutBridge.lean: certified layout-conversion structure and identity bridges.
- CanalLayout.lean: CanalRegime enum and regime-aware layout selection.
Also updates:
- lakefile.lean: adds SilverSight.Semantics.* roots to SilverSightCore.
- docs/ARCHITECTURE.md, RRC_REFACTOR_READINESS.md, PROJECT_MAP.{md,json},
build_logs/2026-06-21_session_build_baseline.md, and GLOSSARY.md.
- AGENTS.md: build baseline, blessed surfaces, and pending proof work.
Build: 2987 jobs, 0 errors (lake build)
Tests: Python 21/21, Lean/C 35/35
73 lines
2.2 KiB
Text
73 lines
2.2 KiB
Text
/-
|
||
SilverSight.Semantics.WireFormat
|
||
|
||
A WireFormat is a certified encoder/decoder pair for a fixed-size Schema
|
||
under a specific Layout. The `roundTrip` field is a Lean proof that decoding
|
||
an encoded value reproduces the original value.
|
||
|
||
Core WireFormats are intentionally simple. Complex layout-specific encodings
|
||
(columnar stripping, compact packing, mmap views) are library extensions that
|
||
must provide their own `roundTrip` proofs against this interface.
|
||
-/
|
||
|
||
import SilverSight.Semantics.Schema
|
||
import SilverSight.Semantics.Layout
|
||
|
||
namespace SilverSight.Semantics
|
||
|
||
/-- Certified wire format: encode, decode, and a proof that they round-trip.
|
||
|
||
The `encode_size` field guarantees that every encoding consumes exactly
|
||
`Schema.byteSize α` bytes, matching the schema contract. -/
|
||
structure WireFormat (α : Type) [Schema α] (layout : Layout) where
|
||
encode : α → ByteArray
|
||
decode : ByteArray → Option α
|
||
encode_size : ∀ a, (encode a).size = byteSize α
|
||
roundTrip : ∀ a, decode (encode a) = some a
|
||
|
||
namespace WireFormat
|
||
|
||
/-- The trivial wire format for `Unit`: zero bytes round-trip. -/
|
||
def unitRowMajor : WireFormat Unit rowMajor where
|
||
encode := fun _ => ByteArray.empty
|
||
decode := fun _ => some ()
|
||
encode_size := fun _ => rfl
|
||
roundTrip := fun _ => rfl
|
||
|
||
/-- Row-major wire format for `Bool`: one byte, 1 = true, 0 = false. -/
|
||
def boolRowMajor : WireFormat Bool rowMajor where
|
||
encode := fun b => ByteArray.mk #[if b then (1 : UInt8) else (0 : UInt8)]
|
||
decode := fun bs =>
|
||
if h : bs.size = 1 then
|
||
let idx : Fin bs.size := ⟨0, by rw [h]; decide⟩
|
||
match bs.get idx with
|
||
| 1 => some true
|
||
| 0 => some false
|
||
| _ => none
|
||
else none
|
||
encode_size := by
|
||
intro _
|
||
rfl
|
||
roundTrip := by
|
||
intro b
|
||
cases b <;> simp [ByteArray.get, ByteArray.size]
|
||
|
||
/-- Row-major wire format for `UInt8`: one byte, identity. -/
|
||
def uint8RowMajor : WireFormat UInt8 rowMajor where
|
||
encode := fun u => ByteArray.mk #[u]
|
||
decode := fun bs =>
|
||
if h : bs.size = 1 then
|
||
let idx : Fin bs.size := ⟨0, by rw [h]; decide⟩
|
||
some (bs.get idx)
|
||
else
|
||
none
|
||
encode_size := by
|
||
intro _
|
||
rfl
|
||
roundTrip := by
|
||
intro u
|
||
simp [ByteArray.get, ByteArray.size]
|
||
|
||
end WireFormat
|
||
|
||
end SilverSight.Semantics
|