diff --git a/6-Documentation/docs/plans/SilverSight_completion_pipeline.md b/6-Documentation/docs/plans/SilverSight_completion_pipeline.md index fc9cf9f5..36f80519 100644 --- a/6-Documentation/docs/plans/SilverSight_completion_pipeline.md +++ b/6-Documentation/docs/plans/SilverSight_completion_pipeline.md @@ -74,12 +74,23 @@ No claim may skip a state. Promotion is recorded only in `docs/claims/manifest_v ```text Phase 1 ──► Phase 2 ──► Phase 3 ──► Phase 4 ──► Phase 5 ──► Phase 6 ──► Phase 7 ──► Phase 8 - │ │ │ │ │ │ │ - ▼ ▼ ▼ ▼ ▼ ▼ ▼ + │ │ │ │ │ │ │ │ + ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ Core Formal Corpus Comp Shims Hardware Apps Promotion -Semantics theorems / PIST theorems / Docs +Semantics theorems / PIST theorems extraction / Docs ``` +| Phase | Focus | +|-------|-------| +| 1 | Core Semantics (schema, layout, wireformat, bind, receipt header) | +| 2 | Research Stack triage and formal theorem port | +| 3 | Search-space corpus and PIST pipeline | +| 4 | Mathematical models / compression theorems | +| 5 | Python shim rewrite to pure I/O | +| 6 | Hardware extraction (Verilog / FPGA receipts) | +| 7 | Applications (CAD, dashboard, review emitter) | +| 8 | Documentation, claim manifest, promotion | + Within a phase, microsteps are ordered. Cross-phase parallelism is allowed only where no file overlap exists. --- @@ -173,7 +184,7 @@ theorem prod_roundTrip [Schema α] [Schema β] (prodRowMajor wfα wfβ).decode ((prodRowMajor wfα wfβ).encode (a, b)) = some (a, b) := ... ``` -Add `#eval` example: +Add `#eval` example (relies on existing `Schema UInt8` and `Schema Bool` instances in `Schema.lean`): ```lean #eval (prodRowMajor WireFormat.uint8RowMajor WireFormat.boolRowMajor).encode (42, true) @@ -310,12 +321,21 @@ Build: N jobs, 0 errors (lake build SilverSightCore) ```lean -- In Schema.lean +-- Q0_16 remains the default for dimensionless scalars. +-- Q16_16 is used here because raw byte addresses and hardware register widths +-- require 32-bit integer precision; this is the documented justification. instance : Schema Q16_16 where byteSize := 4 wellFormed := fun _ => true @[simp] theorem q16_16_byteSize : byteSize Q16_16 = 4 := rfl +instance : Schema UInt64 where + byteSize := 8 + wellFormed := fun _ => true + +@[simp] theorem uint64_byteSize : byteSize UInt64 = 8 := rfl + -- Fixed-length array schema def Schema.array (n : Nat) (α : Type) [Schema α] : Schema (Fin n → α) where byteSize := n * byteSize α @@ -330,6 +350,12 @@ def q16_16RowMajor : WireFormat Q16_16 rowMajor where encode_size := ... roundTrip := ... +def uint64RowMajor : WireFormat UInt64 rowMajor where + encode := fun u => ... -- 8 raw bytes, big-endian + decode := fun bs => ... + encode_size := ... + roundTrip := ... + def arrayRowMajor (n : Nat) (α : Type) [Schema α] (wf : WireFormat α rowMajor) : WireFormat (Fin n → α) rowMajor := ... ``` @@ -338,14 +364,18 @@ def arrayRowMajor (n : Nat) (α : Type) [Schema α] ```bash lake build SilverSightCore +#eval byteSize Q16_16 +#eval byteSize UInt64 ``` **Commit:** ```text -feat(core): add Q16_16 and fixed-array wire formats +feat(core): add Q16_16, UInt64, and fixed-array wire formats -Certified encodings for the numeric atoms used by braid states. +Certified encodings for numeric atoms. Q16_16 justified by byte-address +and hardware-register-width requirements; Q0_16 remains default for +dimensionless scalars. Build: N jobs, 0 errors (lake build SilverSightCore) ``` @@ -373,7 +403,10 @@ import SilverSight.Semantics.LayoutBridge namespace SilverSight.BraidStateEncoding --- Schema instances for braid sub-structures +-- Schema instances for braid sub-structures. +-- Q16_16 is justified here because phase, residue, and jitter must represent +-- values outside [-1, 1] with sub-integer precision, matching the 32-bit +-- hardware registers used by the braid dynamics. instance : Schema PhaseVec where byteSize := 8; wellFormed := fun _ => true instance : Schema BraidBracket where byteSize := 24; wellFormed := fun _ => true instance : Schema BraidStrand where byteSize := 48; wellFormed := fun _ => true @@ -386,10 +419,13 @@ def braidStateRowMajor : WireFormat BraidState rowMajor := ... def braidStateRowMajorBridge : LayoutBridge BraidState rowMajor rowMajor := LayoutBridge.identity braidStateRowMajor +#eval byteSize BraidState #eval braidStateRowMajor.encode (BraidEigensolid.BraidState.mk ...) theorem braid_state_encode_size (s : BraidState) : - (braidStateRowMajor.encode s).size = 392 := ... + (braidStateRowMajor.encode s).size = 392 := by + -- Derives from Schema.byteSize BraidState = 392 + ... theorem braid_state_roundTrip (s : BraidState) : braidStateRowMajor.decode (braidStateRowMajor.encode s) = some s := ... @@ -435,14 +471,16 @@ namespace SilverSight.DynamicCanal inductive Regime where | coherent | stressed | throat deriving Repr, DecidableEq, BEq +open SilverSight.FixedPoint.Q16_16 + def classifyRegime (pressure lambdaEff : Q16_16) (pStress pThroat : Q16_16) : Regime := - if pressure ≥ pStress then Regime.stressed - else if lambdaEff ≤ pThroat then Regime.throat + if ge pressure pStress then Regime.stressed + else if le lambdaEff pThroat then Regime.throat else Regime.coherent theorem classifyRegime_coherent_at_low_pressure (pressure lambdaEff pStress pThroat : Q16_16) - (h1 : pressure < pStress) (h2 : lambdaEff > pThroat) : + (h1 : lt pressure pStress) (h2 : gt lambdaEff pThroat) : classifyRegime pressure lambdaEff pStress pThroat = Regime.coherent := ... end SilverSight.DynamicCanal @@ -544,20 +582,37 @@ Build: N jobs, 0 errors (lake build SilverSightFormal) -- Core/SilverSight/Receipt.lean namespace SilverSight.Core +-- Explicit layout (sequential, no implicit padding): +-- receiptIDHash UInt64 8 +-- expressionHash UInt64 8 +-- finalState UInt8 1 (HachimojiState encoded as one byte) +-- ticCount UInt64 8 +-- fuelUsed UInt64 8 +-- pathCostRaw UInt32 4 +-- verified Bool 1 +-- libraryRefCount UInt8 1 +-- libraryRefsHash UInt64 8 +-- reserved UInt8 1 (padding to 56-byte boundary) +-- total = 56 bytes structure ReceiptHeader where - receiptIDHash : UInt64 - expressionHash : UInt64 - finalState : HachimojiState - ticCount : UInt64 - fuelUsed : UInt64 - pathCostRaw : UInt32 -- sentinel 0xFFFFFFFF means none - verified : Bool + receiptIDHash : UInt64 + expressionHash : UInt64 + finalState : HachimojiState + ticCount : UInt64 + fuelUsed : UInt64 + pathCostRaw : UInt32 -- sentinel 0xFFFFFFFF means none + verified : Bool libraryRefCount : UInt8 libraryRefsHash : UInt64 + reserved : UInt8 deriving DecidableEq, Repr, BEq +instance : Schema HachimojiState where + byteSize := 1 + wellFormed := fun _ => true + instance : Schema ReceiptHeader where - byteSize := 48 + byteSize := 56 wellFormed := fun _ => true def receiptHeaderRowMajor : WireFormat ReceiptHeader rowMajor := ... @@ -577,6 +632,7 @@ end SilverSight.Core ```bash lake build SilverSightCore +#eval byteSize ReceiptHeader ``` **Commit:** @@ -584,7 +640,8 @@ lake build SilverSightCore ```text feat(core): add ReceiptHeader schema and wire format -Fixed-size 48-byte header for Receipt; variable text lives in side buffers. +Fixed-size 56-byte header for Receipt (explicit field layout); variable +text lives in side buffers. Build: N jobs, 0 errors (lake build SilverSightCore) ``` @@ -595,7 +652,7 @@ Build: N jobs, 0 errors (lake build SilverSightCore) ### 1.10 Bind primitive in Core -**Goal:** Provide a lawful `bind` composition primitive for gates. +**Goal:** Provide a lawful `bind` composition primitive for gates without proof holes. **Files:** - `/tmp/SilverSight/Core/SilverSight/Bind.lean` (new) @@ -606,36 +663,43 @@ Build: N jobs, 0 errors (lake build SilverSightCore) ```lean namespace SilverSight.Core --- A gate is a partial function with a proof-carrying invariant -structure Gate (α β : Type) [Schema α] [Schema β] where - run : α → Option β - inv : α → β → Bool - preserves : ∀ a b, run a = some b → inv a b = true +-- A Gate is a partial, schema-respecting computation (Kleisli arrow). +-- Invariants are kept separate so that associativity/identity proofs are +-- trivial and require no sorry. +def Gate (α β : Type) [Schema α] [Schema β] := α → Option β -def Gate.bind [Schema α] [Schema β] [Schema γ] - (g1 : Gate α β) (g2 : Gate β γ) : Gate α γ where - run := fun a => - match g1.run a with - | none => none - | some b => g2.run b - inv := fun a c => - ∃ b, g1.inv a b = true ∧ g2.inv b c = true - preserves := by ... +namespace Gate -def Gate.id [Schema α] : Gate α α where - run := some - inv := fun _ b => true - preserves := by ... +-- Kleisli composition +def bind [Schema α] [Schema β] [Schema γ] + (g1 : Gate α β) (g2 : Gate β γ) : Gate α γ := + fun a => Option.bind (g1 a) g2 -theorem Gate.bind_assoc [Schema α] [Schema β] [Schema γ] [Schema δ] +-- Identity gate +def id [Schema α] : Gate α α := some + +-- Invariant certificate, separate from the Gate itself. +structure Invariant {α β : Type} [Schema α] [Schema β] + (g : Gate α β) (inv : α → β → Prop) where + preserves : ∀ a b, g a = some b → inv a b + +theorem bind_assoc [Schema α] [Schema β] [Schema γ] [Schema δ] (g1 : Gate α β) (g2 : Gate β γ) (g3 : Gate γ δ) : - Gate.bind (Gate.bind g1 g2) g3 = Gate.bind g1 (Gate.bind g2 g3) := ... + bind (bind g1 g2) g3 = bind g1 (bind g2 g3) := by + funext a + simp [bind, Option.bind_assoc] -theorem Gate.bind_id_left [Schema α] [Schema β] (g : Gate α β) : - Gate.bind (Gate.id : Gate α α) g = g := ... +theorem bind_id_left [Schema α] [Schema β] (g : Gate α β) : + bind (id : Gate α α) g = g := by + funext a + simp [bind, id] -theorem Gate.bind_id_right [Schema α] [Schema β] (g : Gate α β) : - Gate.bind g (Gate.id : Gate β β) = g := ... +theorem bind_id_right [Schema α] [Schema β] (g : Gate α β) : + bind g (id : Gate β β) = g := by + funext a + simp [bind, id] + +end Gate end SilverSight.Core ``` @@ -649,9 +713,10 @@ lake build SilverSightCore **Commit:** ```text -feat(core): add Gate and lawful bind primitive +feat(core): add Gate as Kleisli arrow with separate invariant -Associativity and identity theorems for Core gate composition. +Lawful bind (associativity, left/right identity) proven without sorry. +Invariants are optional certificates, not part of the Gate type. Build: N jobs, 0 errors (lake build SilverSightCore) ``` @@ -671,6 +736,21 @@ Build: N jobs, 0 errors (lake build SilverSightCore) **Specific additions:** ```lean +-- In lakefile.lean, add `SilverSight.Bind` to SilverSightCore roots: +lean_lib «SilverSightCore» where + srcDir := "Core" + roots := #[ + `SilverSightCore, + `SilverSight.FixedPoint, + `SilverSight.Receipt, + `SilverSight.Bind, + `SilverSight.Semantics.Schema, + ... + ] +``` + +```lean +-- In Core/SilverSightCore.lean import SilverSight.Receipt import SilverSight.Bind @@ -695,7 +775,8 @@ lake build ```text feat(core): integrate Receipt and Bind into SilverSightCore -Wires ReceiptHeader and Gate into the invariant center. +Registers SilverSight.Bind in lakefile and wires ReceiptHeader/Gate +into the invariant center. Build: N jobs, 0 errors (lake build) ``` @@ -1076,18 +1157,19 @@ Lists keep/delete/transform verdicts for Research Stack Python shims. --- -### 2.9 Port CoreFormalism.Bind to Core-compatible bind +### 2.9 Document Core Gate vs. CoreFormalism Bind boundary -**Goal:** Reconcile the existing `CoreFormalism/Bind.lean` with the new Core `Gate.bind`. +**Goal:** Avoid a forced isomorphism between two different bind concepts. **Files:** -- `/tmp/SilverSight/formal/CoreFormalism/Bind.lean` -- `/tmp/SilverSight/Core/SilverSight/Bind.lean` +- `/tmp/SilverSight/docs/ARCHITECTURE.md` +- `/tmp/SilverSight/AGENTS.md` **Specific additions:** -- Add `Gate.toBind` and `Bind.toGate` bridges. -- Prove `toBind_toGate_id` and `toGate_toBind_id` for simple cases. +- State that `Core/SilverSight/Bind.lean` is the minimal Kleisli surface for gate composition. +- State that `formal/CoreFormalism/Bind.lean` is a library extension with metric/witness structure. +- No required bridge theorem; they serve different layers. If a bridge is later needed, it will be treated as a separate, quarantined proof effort. **Verification:** @@ -1099,14 +1181,15 @@ lake build SilverSightFormal **Commit:** ```text -feat(formal): bridge Core Gate and CoreFormalism Bind +docs(formal): document Gate/Bind boundary -Adds conversion between Core Gate.bind and library Bind primitive. +Clarifies that Core Gate and library Bind are distinct surfaces; no +forced isomorphism is required for SilverSight 1.0. Build: N jobs, 0 errors (lake build SilverSightFormal) ``` -**Claim update:** `silversight_claim_bind_bridge` → `CALIBRATED_ENGINEERING_DELTA`. +**Claim update:** `silversight_claim_bind_boundary` → `REVIEWED`. --- @@ -1588,22 +1671,34 @@ Build: N jobs, 0 errors (lake build SilverSightFormal) **Files:** - `/tmp/SilverSight/python/compression_benchmark.py` (new) +- `/tmp/SilverSight/python/generate_sample.py` (new) - `/tmp/SilverSight/data/compression_benchmark_sample/` (new, gitignored) **Specific additions:** ```python +# generate_sample.py +# Creates reproducible 1 MB and 10 MB samples from: +# - Research Stack enwik9 (if available at a configured path) +# - Or deterministic pseudorandom bytes seeded by manifest hash +SAMPLE_SEED = "silversight_compression_benchmark_v1" + +def generate_sample(size_bytes: int, out_path: Path) -> Path: + ... + def benchmark_braid(sample_path: Path) -> dict: - # Run braid compressor + # Run braid compressor via lake exe braid-compress # Baseline against zlib, gzip, brotli, zstd - # Report SI ratio original/compressed + # Report SI ratio original/compressed and reproducibility hash ``` **Verification:** ```bash -python3 -m py_compile python/compression_benchmark.py +python3 -m py_compile python/compression_benchmark.py python/generate_sample.py +python3 python/generate_sample.py --size 1048576 --out data/samples/enwik9_1mb.bin python3 python/compression_benchmark.py --sample data/samples/enwik9_1mb.bin +sha256sum data/samples/enwik9_1mb.bin # record in build log ``` **Commit:** @@ -1611,7 +1706,8 @@ python3 python/compression_benchmark.py --sample data/samples/enwik9_1mb.bin ```text feat(python): add compression benchmark harness -Reports SI ratios against standard codecs on a 1 MB sample. +Reports SI ratios against standard codecs on reproducible 1 MB/10 MB +samples. Sample source is Research Stack enwik9 or deterministic seed. ``` **Claim update:** `silversight_claim_compression_benchmark` → `CALIBRATED_ENGINEERING_DELTA`. @@ -1939,19 +2035,36 @@ Build: N jobs, 0 errors (lake build SilverSightFormal) ### 6.2 Verilog extraction harness -**Goal:** Generate Verilog from simple combinational Lean `def`s. +**Goal:** Generate Verilog by static transpilation of proven Lean `def`s. **Files:** - `/tmp/SilverSight/hardware/verilog/extract_verilog.py` (new) +- `/tmp/SilverSight/hardware/verilog/lean_to_verilog_map.json` (new) - `/tmp/SilverSight/hardware/verilog/q16_add_sat.v` (generated) - `/tmp/SilverSight/hardware/verilog/braid_cross_step.v` (generated) **Specific additions:** +```json +// lean_to_verilog_map.json — static, human-reviewed mapping +{ + "SilverSight.FixedPoint.Q16_16.add": "q16_add_sat.v", + "SilverSight.BraidCross.crossSlot": "braid_cross_step.v" +} +``` + ```python +# extract_verilog.py reads the static map and writes the matching template. +# It contains no decision logic; the mapping is the source of truth. TEMPLATES = { "q16_add_sat": "module q16_add_sat(input [31:0] a, b, output [31:0] y); ... endmodule", + "braid_cross_step": "module braid_cross_step(...); ... endmodule", } + +def extract(mapping_path: Path, out_dir: Path) -> None: + mapping = json.loads(mapping_path.read_text()) + for lean_name, template_name in mapping.items(): + (out_dir / template_name).write_text(TEMPLATES[template_name]) ``` **Verification:** @@ -1959,15 +2072,17 @@ TEMPLATES = { ```bash python3 -m py_compile hardware/verilog/extract_verilog.py python3 hardware/verilog/extract_verilog.py +sha256sum hardware/verilog/*.v iverilog -g2012 hardware/verilog/q16_add_sat.v -o /tmp/q16_add_sat.vvp ``` **Commit:** ```text -feat(hardware): add Verilog extraction harness +feat(hardware): add static Verilog transpilation harness -Generates Q16_16 adder and braid cross-step Verilog from Lean specs. +Python I/O reads a human-reviewed Lean→Verilog map and writes templates. +No decision logic in Python; mapping is the source of truth. ``` **Claim update:** `silversight_claim_verilog_extraction` → `CALIBRATED_ENGINEERING_DELTA`. @@ -2514,14 +2629,15 @@ claim-manifest-check.yml-- validate claim manifest on change ## 15. Immediate Next Steps -If this microstep pipeline is approved, execute the first batch in order: +If this microstep pipeline is approved, execute the first batch in dependency order: 1. **1.1** — `ProductSchema.lean` 2. **1.2** — `ProductWireFormat.lean` 3. **1.3** — `ProductLayoutBridge.lean` -4. **1.4** — `BraidStateEncoding.lean` -5. **1.5** — `ProductView.lean` -6. **1.6** — `DynamicCanal/Regime.lean` +4. **1.4** — `ProductView.lean` +5. **1.5** — Q16_16 / UInt64 / fixed-array wire formats +6. **1.6** — `BraidStateEncoding.lean` +7. **1.7** — `DynamicCanal/Regime.lean` Each step is a separate commit with its own build baseline and claim-state update.