|
| 1 | +# Wave Loop 403 — Decomposed Plan |
| 2 | + |
| 3 | +**Issue:** #1307 |
| 4 | +**Branch:** `trinity-rust-rings` |
| 5 | +**Goal:** Close the deferred physical CCLK measurement (Variant A), extend the |
| 6 | +Lean 4 formal model to bitstream configuration (Variant B), or add a |
| 7 | +physical-cable smoke path (Variant C). |
| 8 | + |
| 9 | +--- |
| 10 | + |
| 11 | +## 1. Weak points |
| 12 | + |
| 13 | +### 1.1 Physical blocker (Variant A) |
| 14 | +- **CCLK measurement still requires bench access.** Without a logic analyser / |
| 15 | + oscilloscope on pin P12, Variant A cannot close. The `tri fpga measure-cclk` |
| 16 | + parser is ready, but the actual capture is operator-dependent and cannot be |
| 17 | + performed autonomously in a headless session. |
| 18 | +- **OSCFSEL-to-MHz mapping is undocumented.** Even if a capture is taken, mapping |
| 19 | + raw `OSCFSEL=0..5` to frequency requires either multiple captures or an |
| 20 | + external 7-series configuration reference. |
| 21 | + |
| 22 | +### 1.2 Formal gap (Variant B) |
| 23 | +- `TernaryFPGABoot.lean` models STAT decoding and the cold-POR decision tree, |
| 24 | + but does not yet link the canonical bitstream configuration (`IDCODE`, |
| 25 | + `SPI_BUSWIDTH`, `STARTUPCLK`, `OSCFSEL`) to the boot predicates. |
| 26 | +- The smoke-gate assertions in `cli/tri/src/fpga.rs` and |
| 27 | + `scripts/dump_bit_config.py` are executable, but they are not connected to |
| 28 | + the formal specification. A formal proof that the canonical configuration |
| 29 | + implies the preconditions for `boot_success` would close this gap. |
| 30 | + |
| 31 | +### 1.3 Smoke-gate physical gap (Variant C) |
| 32 | +- `tri fpga smoke-gate` is board-less. A cable-connected SRAM load would catch |
| 33 | + bitstream regressions that the static assertions miss, but it needs the |
| 34 | + Digilent FTDI cable and a powered board. |
| 35 | + |
| 36 | +--- |
| 37 | + |
| 38 | +## 2. Competitor scan |
| 39 | + |
| 40 | +| Project | Approach | Relevance to W403 | |
| 41 | +|---------|----------|-------------------| |
| 42 | +| **[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. | |
| 43 | +| **[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. | |
| 44 | +| **[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. | |
| 45 | +| **[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. | |
| 46 | +| **FIRRTL / Chisel** | Scala DSL → intermediate form → Verilog | Widely used, no proof obligations by default. | |
| 47 | +| **Clash** | Haskell → VHDL/Verilog | Functional HDL, no proof obligations by default. | |
| 48 | +| **Bluespec** | Rule-based HDL with types | Mature, but proprietary tooling. | |
| 49 | + |
| 50 | +**Takeaway:** The credible threat is **Verilean / Sparkle / Aria-HDL**. They can |
| 51 | +claim "Lean 4 + FPGA synthesis + proofs"; t27 counters by extending its proof |
| 52 | +lattice into the **configuration and boot domain** — a space they do not |
| 53 | +currently cover. |
| 54 | + |
| 55 | +--- |
| 56 | + |
| 57 | +## 3. Chosen variant |
| 58 | + |
| 59 | +**Variant B — Extend the Lean 4 model to bitstream configuration predicates** is |
| 60 | +the highest-leverage path because: |
| 61 | +- it requires no hardware, |
| 62 | +- it directly closes the formal gap identified in W402, |
| 63 | +- it strengthens t27's differentiation against Sparkle/Aria-HDL, |
| 64 | +- it documents why the smoke-gate assertions are exactly the right set. |
| 65 | + |
| 66 | +Variant A tooling is already complete; if hardware becomes available, the |
| 67 | +physical capture can be slotted in without code changes. Variant C is deferred |
| 68 | +to a stretch goal. |
| 69 | + |
| 70 | +--- |
| 71 | + |
| 72 | +## 4. Decomposed work |
| 73 | + |
| 74 | +| Step | File(s) | Deliverable | |
| 75 | +|------|---------|-------------| |
| 76 | +| 4.1 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | `BitstreamConfig` structure: `idcode`, `spi_buswidth`, `startupclk`, `oscfsel` | |
| 77 | +| 4.2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Canonical config constant / predicate matching smoke-gate assertions | |
| 78 | +| 4.3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Lemmas: `canonical_config_implies_spi_x1_cclk`, `config_and_mode_implies_boot_pred`, `boot_success_decision_tree` | |
| 79 | +| 4.4 | `fpga/HARDWARE_SSOT.md` | Link the bitstream config audit checklist to the Lean 4 predicates | |
| 80 | +| 4.5 | `docs/reports/WAVE_LOOP_403_REPORT.md` | Close-out report | |
| 81 | +| 4.6 | `docs/reports/FPGA_LOOP_EVIDENCE_2026-07-05.md` | Evidence of build and lemma coverage | |
| 82 | +| 4.7 | `docs/reports/FPGA_LOOP_COOPERATION_2026-07-05.md` | W404 cooperation variants | |
| 83 | +| 4.8 | `.trinity/experience.md` | W403 learnings | |
| 84 | +| 4.9 | git/PR | Commit, push `trinity-rust-rings`, create PR, close #1307 | |
| 85 | + |
| 86 | +--- |
| 87 | + |
| 88 | +## 5. Acceptance criteria |
| 89 | + |
| 90 | +- AC-B1: `BitstreamConfig` defined with the four fields matching the smoke-gate |
| 91 | + assertions. |
| 92 | +- AC-B2: `canonical_config` predicate matches the canonical Wukong V1 / XC7A200T |
| 93 | + setup. |
| 94 | +- AC-B3: At least three lemmas link config / mode / boot predicates. |
| 95 | +- AC-B4: `fpga/HARDWARE_SSOT.md` references the formal config predicates. |
| 96 | +- AC-B5: `lake build Trinity.TernaryFPGABoot` passes. |
| 97 | +- AC-B6: `./scripts/tri test` passes (576/576 baseline maintained). |
| 98 | +- AC-B7: Close-out report + evidence + W404 cooperation variants committed. |
| 99 | + |
| 100 | +--- |
| 101 | + |
| 102 | +## 6. Risks |
| 103 | + |
| 104 | +- **Lean 4 proof complexity:** keep the model shallow — encode configuration as |
| 105 | + a record and prove implication lemmas, not a full bitstream parser. |
| 106 | +- **Backend hash drift:** after editing Lean files only, no spec hashes should |
| 107 | + change; but run `tri test` to confirm. |
| 108 | +- **CI time:** the new module is small and should not affect the suite budget. |
| 109 | + |
| 110 | +--- |
| 111 | + |
| 112 | +*φ² + φ⁻² = 3 | TRINITY* |
0 commit comments