gHashTag · gHashTag · Jul 4, 2026 · Jul 4, 2026
@@ -0,0 +1,112 @@
+# Wave Loop 403 — Decomposed Plan
+
+**Issue:** #1307  
+**Branch:** `trinity-rust-rings`  
+**Goal:** Close the deferred physical CCLK measurement (Variant A), extend the
+Lean 4 formal model to bitstream configuration (Variant B), or add a
+physical-cable smoke path (Variant C).
+
+---
+
+## 1. Weak points
+
+### 1.1 Physical blocker (Variant A)
+- **CCLK measurement still requires bench access.** Without a logic analyser /
+  oscilloscope on pin P12, Variant A cannot close. The `tri fpga measure-cclk`
+  parser is ready, but the actual capture is operator-dependent and cannot be
+  performed autonomously in a headless session.
+- **OSCFSEL-to-MHz mapping is undocumented.** Even if a capture is taken, mapping
+  raw `OSCFSEL=0..5` to frequency requires either multiple captures or an
+  external 7-series configuration reference.
+
+### 1.2 Formal gap (Variant B)
+- `TernaryFPGABoot.lean` models STAT decoding and the cold-POR decision tree,
+  but does not yet link the canonical bitstream configuration (`IDCODE`,
+  `SPI_BUSWIDTH`, `STARTUPCLK`, `OSCFSEL`) to the boot predicates.
+- The smoke-gate assertions in `cli/tri/src/fpga.rs` and
+  `scripts/dump_bit_config.py` are executable, but they are not connected to
+  the formal specification. A formal proof that the canonical configuration
+  implies the preconditions for `boot_success` would close this gap.
+
+### 1.3 Smoke-gate physical gap (Variant C)
+- `tri fpga smoke-gate` is board-less. A cable-connected SRAM load would catch
+  bitstream regressions that the static assertions miss, but it needs the
+  Digilent FTDI cable and a powered board.
+
+---
+
+## 2. Competitor scan
+
+| Project | Approach | Relevance to W403 |
+|---------|----------|-------------------|
+| **[Verilean / Sparkle](https://github.com/Verilean/sparkle)** | Lean 4-embedded HDL with native proofs and SystemVerilog synthesis | Strongest formal-HDL competitor. Includes verified RISC-V SoC, BitNet accelerator, AXI4-Lite. Does not model FPGA boot configuration, so t27 can differentiate by formalizing the bring-up path. |
+| **[Aria-HDL](https://github.com/zeta1999/fpga-meta-compiler-public)** | FPGA meta-compiler emitting Verilog/VHDL/SVA/Lean 4 proof obligations | Competes in the "spec → formal proof → FPGA" space. Does not specifically cover 7-series boot config, leaving a niche for t27. |
+| **[seLe4n](https://sele4n.org/)** | Microkernel verified in Lean 4 | Shows Lean 4 can verify low-level system bring-up code; analogous discipline can be applied to FPGA cold-POR. |
+| **[USENIX WOOT 2024 Zynq secure boot paper](https://www.usenix.org/system/files/woot24-ravi.pdf)** | Offensive analysis of Zynq-7000 secure boot / bitstream recovery | Motivation: boot configuration mistakes have real security consequences. Formal audit of config registers is a defensive countermeasure. |
+| **FIRRTL / Chisel** | Scala DSL → intermediate form → Verilog | Widely used, no proof obligations by default. |
+| **Clash** | Haskell → VHDL/Verilog | Functional HDL, no proof obligations by default. |
+| **Bluespec** | Rule-based HDL with types | Mature, but proprietary tooling. |
+
+**Takeaway:** The credible threat is **Verilean / Sparkle / Aria-HDL**. They can
+claim "Lean 4 + FPGA synthesis + proofs"; t27 counters by extending its proof
+lattice into the **configuration and boot domain** — a space they do not
+currently cover.
+
+---
+
+## 3. Chosen variant
+
+**Variant B — Extend the Lean 4 model to bitstream configuration predicates** is
+the highest-leverage path because:
+- it requires no hardware,
+- it directly closes the formal gap identified in W402,
+- it strengthens t27's differentiation against Sparkle/Aria-HDL,
+- it documents why the smoke-gate assertions are exactly the right set.
+
+Variant A tooling is already complete; if hardware becomes available, the
+physical capture can be slotted in without code changes. Variant C is deferred
+to a stretch goal.
+
+---
+
+## 4. Decomposed work
+
+| Step | File(s) | Deliverable |
+|------|---------|-------------|
+| 4.1 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | `BitstreamConfig` structure: `idcode`, `spi_buswidth`, `startupclk`, `oscfsel` |
+| 4.2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Canonical config constant / predicate matching smoke-gate assertions |
+| 4.3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Lemmas: `canonical_config_implies_spi_x1_cclk`, `config_and_mode_implies_boot_pred`, `boot_success_decision_tree` |
+| 4.4 | `fpga/HARDWARE_SSOT.md` | Link the bitstream config audit checklist to the Lean 4 predicates |
+| 4.5 | `docs/reports/WAVE_LOOP_403_REPORT.md` | Close-out report |
+| 4.6 | `docs/reports/FPGA_LOOP_EVIDENCE_2026-07-05.md` | Evidence of build and lemma coverage |
+| 4.7 | `docs/reports/FPGA_LOOP_COOPERATION_2026-07-05.md` | W404 cooperation variants |
+| 4.8 | `.trinity/experience.md` | W403 learnings |
+| 4.9 | git/PR | Commit, push `trinity-rust-rings`, create PR, close #1307 |
+
+---
+
+## 5. Acceptance criteria
+
+- AC-B1: `BitstreamConfig` defined with the four fields matching the smoke-gate
+  assertions.
+- AC-B2: `canonical_config` predicate matches the canonical Wukong V1 / XC7A200T
+  setup.
+- AC-B3: At least three lemmas link config / mode / boot predicates.
+- AC-B4: `fpga/HARDWARE_SSOT.md` references the formal config predicates.
+- AC-B5: `lake build Trinity.TernaryFPGABoot` passes.
+- AC-B6: `./scripts/tri test` passes (576/576 baseline maintained).
+- AC-B7: Close-out report + evidence + W404 cooperation variants committed.
+
+---
+
+## 6. Risks
+
+- **Lean 4 proof complexity:** keep the model shallow — encode configuration as
+  a record and prove implication lemmas, not a full bitstream parser.
+- **Backend hash drift:** after editing Lean files only, no spec hashes should
+  change; but run `tri test` to confirm.
+- **CI time:** the new module is small and should not affect the suite budget.
+
+---
+
+*φ² + φ⁻² = 3 | TRINITY*
@@ -1,38 +1,38 @@
-# Wave Loop 402 — FPGA: close AC5 physical CCLK measurement + follow-up hardening
+# Wave Loop 403 — FPGA: close physical CCLK measurement or extend formal/physical smoke coverage
 
-**Issue:** #1305  
+**Issue:** #1307  
 **Branch:** `trinity-rust-rings`  
-**Milestone:** W401 hardened the cold-POR protocol and added board-less CI guards.
-Now close the deferred AC5 (physical CCLK measurement on P12) or pursue one of the
-alternate cooperation variants.
+**Milestone:** W402 formalized the cold-POR decision tree in Lean 4. W403 should
+close the remaining physical AC or extend formal/physical smoke coverage.
 
 ---
 
 ## Goal
 
 1. Capture the actual CCLK frequency on pin P12 and record it in
    `fpga/HARDWARE_SSOT.md` (Variant A — default if hardware is available).
-2. OR encode the cold-POR / CCLK decision tree in Lean 4 (Variant B — no
-   hardware required).
+2. OR extend the Lean 4 model with bitstream-configuration predicates
+   (`STARTUPCLK`, `OSCFSEL`, `SPI_BUSWIDTH`) and link them to the decision trees
+   (Variant B — no hardware required).
 3. OR extend `tri fpga smoke-gate` to optionally load the GF16 matrix into SRAM
    and assert `DONE=HIGH` when a cable is present (Variant C — stretch).
-4. Update close-out reports and open W403 cooperation variants.
+4. Update close-out reports and open W404 cooperation variants.
 
 ---
 
 ## Decomposed plan
 
-See `.claude/plans/wave-loop-402.md` for the full work breakdown.
+See `.claude/plans/wave-loop-403.md` for the full work breakdown.
 
 | Step | File(s) | Deliverable |
 |------|---------|-------------|
-| 1 | `.claude/plans/wave-loop-402.md` | Decomposed plan + weak-point + competitor scan |
+| 1 | `.claude/plans/wave-loop-403.md` | Decomposed plan + weak-point + competitor scan |
 | 2 | `fpga/HARDWARE_SSOT.md` (Variant A) | Measured CCLK frequency/duty cycle on P12 |
-| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | Formal STAT/decision-tree lemmas |
+| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | Bitstream-config lemmas |
 | 4 | `cli/tri/src/fpga.rs` (Variant C) | Optional cable-connected SRAM smoke load |
-| 5 | `docs/reports/*` | W402 report, evidence, W403 cooperation |
-| 6 | `.trinity/experience.md` | W402 learnings |
-| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1305, open #W403 |
+| 5 | `docs/reports/*` | W403 report, evidence, W404 cooperation |
+| 6 | `.trinity/experience.md` | W403 learnings |
+| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1307, open #W404 |
 
 ---
 
@@ -41,12 +41,12 @@ See `.claude/plans/wave-loop-402.md` for the full work breakdown.
 - [ ] AC-A1 (Variant A): a physical CCLK trace is captured and the dominant
       frequency is recorded.
 - [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.5 contains the measured value.
-- [ ] AC-B1 (Variant B): new Lean 4 module builds and links `STAT` decoding to the
+- [ ] AC-B1 (Variant B): new Lean 4 lemmas link canonical bitstream config to the
       documented decision trees.
 - [ ] AC-C1 (Variant C): `tri fpga smoke-gate --require-cable` reaches
       `DONE=HIGH` on the bench.
 - [ ] AC-D1: `./scripts/tri test` passes.
-- [ ] AC-D2: W402 report + evidence + W403 cooperation variants committed.
+- [ ] AC-D2: W403 report + evidence + W404 cooperation variants committed.
 
 ---
 

@@ -1356,3 +1356,15 @@
 - **Commit:** merge(master): integrate upstream master into trinity-rust-rings for W401 land
 - **Files:** docs/NOW.md
 
+## 2026-07-04T09:08:07Z — trinity-rust-rings
+- **Commit:** chore(trinity): point current-issue.md to W403 issue #1307 and add decomposed plan
+- **Files:** .claude/plans/wave-loop-403.md,.trinity/experience.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-06.md,docs/reports/WAVE_LOOP_403_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
+
+## 2026-07-04T09:11:36Z — trinity-rust-rings
+- **Commit:** feat(igla): Wave Loop 403 — bitstream config linked to cold-POR decision tree in Lean 4 (Closes #1307)
+- **Files:** 
+
+## 2026-07-04T09:13:38Z — trinity-rust-rings
+- **Commit:** Merge branch 'master' into trinity-rust-rings for W403 (Closes #1307)
+- **Files:** .claude/plans/wave-loop-403.md,.trinity/current-issue.md,.trinity/current_task/activity.md,.trinity/experience.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-06.md,docs/reports/WAVE_LOOP_403_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
+
@@ -1,5 +1,53 @@
 # t27 / Trinity Agent Experience Log
 
+## 2026-07-05 — Wave Loop 403 (Bitstream config linked to cold-POR decision tree)
+
+### What worked
+- Falling back to **Variant B** again (Lean 4 extension) let W403 close without
+  bench hardware. The formal layer added value by connecting the `.bit`
+  configuration audit to the STAT-register decision tree.
+- Keeping the `BitstreamConfig` structure field names identical to the
+  `tri fpga bit-config` output (`idcode`, `spi_buswidth`, `startupclk`,
+  `oscfsel`) makes the formal model traceable to the CLI tool.
+- The `ColdPOR` structure cleanly separates static bitstream facts from dynamic
+  physical preconditions (`mode_ok`, `no_cable_interference`), matching the
+  prose in `fpga/HARDWARE_SSOT.md`.
+- Proving `decision_tree_exhaustive` by explicit `Or.inl` / `Or.inr`
+  construction avoided fragile `tauto`/`rcases` behavior on `Bool` disjunctions
+  defined via `decide`.
+- Removing the unnecessary `eos` requirement from `boot_success` closed a
+  logical gap and made the exhaustiveness theorem provable without inventing an
+  unreachable "other" branch.
+- Conformance suite: **576/576 PASS**; `lake build Trinity.TernaryFPGABoot` green.
+
+### What changed behavior
+- `proofs/lean4/Trinity/TernaryFPGABoot.lean` now contains:
+  - `BitstreamConfig` and `BitstreamConfig.canonical`
+  - `ColdPOR` and `cold_por_spi_flash_pred`
+  - Linkage lemmas `cold_por_done_eos_high_implies_boot_success`,
+    `cold_por_done_low_implies_h2`, and `decision_tree_exhaustive`
+- `fpga/HARDWARE_SSOT.md` §3.2 now links the canonical bitstream config audit to
+  the Lean 4 predicates and the exhaustive decision-tree theorem.
+- `docs/NOW.md` updated with the W403 entry.
+- Close-out artifacts: `docs/reports/WAVE_LOOP_403_REPORT.md`,
+  `FPGA_LOOP_EVIDENCE_2026-07-06.md`, and
+  `FPGA_LOOP_COOPERATION_2026-07-06.md`.
+
+### Patterns to reuse
+- Extend a formal model one layer at a time: W402 formalized STAT decode and
+  the decision tree; W403 formalized the static bitstream config that feeds the
+  tree. Each layer is a small, reviewable diff.
+- Use explicit disjunct construction in Lean 4 when working with `Bool`
+  predicates that contain `decide` terms; automation is brittle there.
+- Keep the physical-deferred AC explicit in the report and the next-loop
+  cooperation variants so the work does not silently drop off the radar.
+
+### Anti-patterns to avoid
+- Do not require `eos` in a success predicate unless the exhaustiveness proof
+  actually needs it. Unnecessary conjuncts create unreachable model corners.
+- Do not rely on `tauto`/`rcases` to split `Bool` disjunctions that are not
+  syntactic inductives; build the proof term explicitly instead.
+
 ## 2026-07-05 — Wave Loop 402 (Cold-POR decision tree formalized in Lean 4)
 
 ### What worked

@@ -2,6 +2,13 @@
 
 Last updated: 2026-07-05
 
+## w403-fpga-bitstream-config-lean4 -- extend Lean 4 formal model to bitstream configuration (Closes #1307)
+
+- **WHERE**: `proofs/lean4/Trinity/TernaryFPGABoot.lean`, `fpga/HARDWARE_SSOT.md`, close-out reports.
+- **WHAT**: Extended the Lean 4 STAT-register model with a `BitstreamConfig` structure and `canonical` predicate (`IDCODE=0x03636093`, `SPI_BUSWIDTH=x1`, `STARTUPCLK=CCLK`, `OSCFSEL=0`). Added `ColdPOR` preconditions (`mode_ok`, `no_cable_interference`) and linkage lemmas: `cold_por_done_eos_high_implies_boot_success`, `cold_por_done_low_implies_h2`, and `decision_tree_exhaustive`. Formal traceability callout added to `fpga/HARDWARE_SSOT.md` §3.2. Physical CCLK measurement on P12 (Variant A) deferred again — no logic-analyzer access. Variant C (`--require-cable` SRAM smoke) not attempted. Conformance suite `576/576 PASS`; `lake build Trinity.TernaryFPGABoot` green.
+- **Why**: closes W403 without bench hardware by formalizing the static bitstream-config audit that `tri fpga bit-config` performs, making the FPGA boot model traceable end-to-end from `.bit` register settings through cold-Por preconditions to STAT outcomes.
+- **Anchor**: phi^2 + phi^-2 = 3
+
 ## w402-fpga-cold-por-lean4 -- formalize cold-POR / CCLK decision tree in Lean 4 (Closes #1305)
 
 - **WHERE**: `proofs/lean4/Trinity/TernaryFPGABoot.lean`, `proofs/lean4/Trinity.lean`, `fpga/HARDWARE_SSOT.md`, close-out reports.