mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
docs(plans): address review conditions on completion pipeline
- Reorders Phase 1 next steps to dependency order. - Adds Q16_16 / UInt64 justification notes and explicit ReceiptHeader 56-byte layout with #eval witness. - Redesigns Core Gate.bind as a Kleisli arrow with separate Invariant certificate to avoid proof holes. - Registers SilverSight.Bind in lakefile.lean integration step. - Removes forced Core Gate ↔ CoreFormalism Bind bridge; documents boundary. - Clarifies Verilog extraction as static, reviewed Lean→template mapping. - Specifies compression benchmark sample source and reproducibility. - Fixes fixed-point comparison operators in classifyRegime. - Adds phase/focus table to dependency graph. Build: docs only; no Lean/Python changes
This commit is contained in:
parent
f7c08f7a6a
commit
4dd0c18759
1 changed files with 184 additions and 68 deletions
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue