Skip to content

Commit 6028a72

Browse files
Dmitrii Vasilevclaude
Dmitrii Vasilev
and
claude
committed
chore(trinity): point current-issue.md to W402 issue #1305 and add decomposed plan
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent a082808 commit 6028a72

2 files changed

Lines changed: 140 additions & 37 deletions

File tree

‎.claude/plans/wave-loop-402.md‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
# Wave Loop 402 — Decomposed Plan
2+
3+
**Issue:** #1305
4+
**Branch:** `trinity-rust-rings`
5+
**Goal:** Close the deferred W401 AC5 (physical CCLK measurement) or pursue the
6+
highest-leverage no-hardware alternative: a Lean 4 formalization of the cold-POR
7+
/ CCLK decision tree.
8+
9+
---
10+
11+
## 1. Weak points
12+
13+
### 1.1 Physical blocker (Variant A)
14+
- **AC5 requires a logic analyser / oscilloscope on pin P12.** Without bench
15+
access the actual CCLK frequency cannot be recorded. The `tri fpga
16+
measure-cclk --csv` parser is already robust, but the measurement itself is
17+
operator-dependent.
18+
- **OSCFSEL-to-MHz mapping remains undocumented.** Even if a capture is taken,
19+
mapping raw `OSCFSEL=0..5` to frequency requires one capture per variant or an
20+
external 7-series configuration reference.
21+
22+
### 1.2 Formal gap (Variant B)
23+
- The W400/W401 decision trees live only in prose (`fpga/HARDWARE_SSOT.md`).
24+
They are not linked to the same formal infrastructure that underpins the
25+
ternary MAC proof lattice (`proofs/lean4/Trinity/TernaryMac.lean`).
26+
- Competitor formal-HDL projects (Sparkle HDL, Verilean, Sail-to-Verilog) can
27+
claim traceability; t27 currently has no formal FPGA-boot specification.
28+
29+
### 1.3 Smoke-gate physical gap (Variant C)
30+
- `tri fpga smoke-gate` is board-less. A cable-connected load would catch
31+
bitstream regressions that the static assertions miss, but it needs the
32+
Digilent FTDI cable and a powered board.
33+
34+
---
35+
36+
## 2. Competitor scan
37+
38+
| Project | Approach | Relevance to W402 |
39+
|---------|----------|-------------------|
40+
| **Sparkle HDL** | Rust-embedded DSL → formal semantics | Credible formal competitor in the RTL-design space; t27's defense is the spec-first `.t27` + Lean 4 proof stack. |
41+
| **Verilean** | Lean 4 → verified RTL | Direct competitor for "Lean 4 HDL"; W402 Variant B closes a small slice of that gap for FPGA boot diagnostics. |
42+
| **Sail / RISC-V Sail** | ISA-level formal → emulator / RTL | Not HDL-focused, but demonstrates formal traceability from spec to silicon. |
43+
| **Kami (MIT)** | Coq → Bluespec-like hardware | Shows theorem-prover-verified hardware is publishable; t27 uses Lean 4 instead. |
44+
| **FIRRTL / Chisel** | Scala DSL → intermediate form → Verilog | Widely used but not formally verified; t27 differentiates on proof. |
45+
| **Clash** | Haskell → VHDL/Verilog | Functional HDL, no proof obligations by default. |
46+
| **Bluespec** | Rule-based HDL with types | Mature, but proprietary tooling; t27's open-source Lean stack is the contrast. |
47+
48+
**Takeaway:** The credible threat is **Verilean / Lean 4 HDL**. Adding a Lean 4
49+
FPGA-boot specification gives t27 a formal story in the same design space and
50+
leverages the existing `TernaryMac` proof infrastructure.
51+
52+
---
53+
54+
## 3. Chosen variant
55+
56+
**Variant B — Formalize the cold-POR / CCLK decision tree in Lean 4** is the
57+
highest-leverage path because:
58+
- it requires no hardware,
59+
- it reuses the existing Lean 4 build (`proofs/lean4/Trinity`),
60+
- it directly addresses the competitor gap (Verilean / Sparkle),
61+
- it documents the W400 empirical result as a formal specification.
62+
63+
Variant A tooling is already complete; if hardware becomes available during the
64+
loop, the physical capture can be slotted in without code changes. Variant C is
65+
deferred to a stretch goal.
66+
67+
---
68+
69+
## 4. Decomposed work
70+
71+
| Step | File(s) | Deliverable |
72+
|------|---------|-------------|
73+
| 4.1 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Definitions: `StatRegister`, `Mode`, `Done`, `Eos`, `CrcError`, `IdError` |
74+
| 4.2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Helper lemmas decoding `STAT` bits into named predicates |
75+
| 4.3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Decision-tree lemmas: `boot_success_iff`, `mode_master_spi_x1_iff`, `crc_or_id_error_implies_not_done` |
76+
| 4.4 | `proofs/lean4/Trinity.lean` | Export the new module |
77+
| 4.5 | `proofs/lean4/lakefile.toml` / CI | Ensure the module builds in `./scripts/tri test` |
78+
| 4.6 | `fpga/HARDWARE_SSOT.md` | Link the documented decision trees to the formal lemmas |
79+
| 4.7 | `docs/reports/WAVE_LOOP_402_REPORT.md` | Close-out report |
80+
| 4.8 | `docs/reports/FPGA_LOOP_EVIDENCE_2026-07-05.md` | Evidence of Lean build and lemma coverage |
81+
| 4.9 | `docs/reports/FPGA_LOOP_COOPERATION_2026-07-05.md` | W403 cooperation variants |
82+
| 4.10 | `.trinity/experience.md` | W402 learnings |
83+
| 4.11 | git/PR | Commit, push `trinity-rust-rings`, create PR, close #1305 |
84+
85+
---
86+
87+
## 5. Acceptance criteria
88+
89+
- AC-B1: `proofs/lean4/Trinity/TernaryFPGABoot.lean` compiles with `lake build`.
90+
- AC-B2: At least three decision-tree lemmas are stated and proved.
91+
- AC-B3: `fpga/HARDWARE_SSOT.md` references the formal lemmas.
92+
- AC-B4: `./scripts/tri test` passes (575/575 baseline maintained).
93+
- AC-B5: Close-out report + evidence + W403 cooperation variants committed.
94+
95+
---
96+
97+
## 6. Risks
98+
99+
- **Lean 4 toolchain drift:** the existing `lakefile.toml` may need updates for
100+
new module inclusion; keep changes minimal.
101+
- **Proof complexity:** full bit-accurate 7-series STAT decoding is unnecessary;
102+
focus on the high-level decision predicates used in `fpga/HARDWARE_SSOT.md`.
103+
- **CI time:** adding a new Lean module must not push `tri test` over budget;
104+
the module is small.
105+
106+
---
107+
108+
*φ² + φ⁻² = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 32 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,65 +1,60 @@
1-
# Wave Loop 401 — CCLK measurement & cold-POR hardening
1+
# Wave Loop 402 — FPGA: close AC5 physical CCLK measurement + follow-up hardening
22

3-
**Issue:** #1303
3+
**Issue:** #1305
44
**Branch:** `trinity-rust-rings`
5-
**Milestone:** FPGA boot-from-flash is verified; now lock the working default,
6-
harden the cold-POR protocol, and measure/record CCLK.
5+
**Milestone:** W401 hardened the cold-POR protocol and added board-less CI guards.
6+
Now close the deferred AC5 (physical CCLK measurement on P12) or pursue one of the
7+
alternate cooperation variants.
78

89
---
910

1011
## Goal
1112

12-
1. Harden the cold-POR protocol with a standalone `tri fpga boot-protocol`
13-
command and explicit operator checklist.
14-
2. Extend `tri fpga smoke-gate` to enforce the canonical bitstream:
15-
`IDCODE=0x03636093`, `SPI_BUSWIDTH=x1`, `STARTUPCLK=CCLK`, `OSCFSEL=0`,
16-
and no CRC register writes.
17-
3. Make `tri fpga measure-cclk --csv` robust to DSView, PulseView, and Saleae
18-
CSV exports, and add unit tests for the parser.
19-
4. Add a board-less dry-run sweep guard so CI exercises `cclk-sweep` and
20-
`sweep-report` without hardware.
21-
5. If a physical CCLK capture is available, record the measured frequency in
22-
`fpga/HARDWARE_SSOT.md`.
23-
6. Land W401 and publish W402 cooperation variants.
13+
1. Capture the actual CCLK frequency on pin P12 and record it in
14+
`fpga/HARDWARE_SSOT.md` (Variant A — default if hardware is available).
15+
2. OR encode the cold-POR / CCLK decision tree in Lean 4 (Variant B — no
16+
hardware required).
17+
3. OR extend `tri fpga smoke-gate` to optionally load the GF16 matrix into SRAM
18+
and assert `DONE=HIGH` when a cable is present (Variant C — stretch).
19+
4. Update close-out reports and open W403 cooperation variants.
2420

2521
---
2622

2723
## Decomposed plan
2824

29-
See `.claude/plans/wave-loop-401.md` for the full work breakdown.
25+
See `.claude/plans/wave-loop-402.md` for the full work breakdown.
3026

3127
| Step | File(s) | Deliverable |
3228
|------|---------|-------------|
33-
| 1 | `scripts/dump_bit_config.py` | `--assert-oscfsel N`, `--assert-no-crc-writes` |
34-
| 2 | `cli/tri/src/fpga.rs` | Extended `smoke-gate`, new `boot-protocol`, robust CSV parser + tests |
35-
| 3 | `bootstrap/src/suite.rs` | Board-less dry-run sweep + report guard |
36-
| 4 | `fpga/HARDWARE_SSOT.md`, `docs/reports/*` | SSOT update + W401 report/evidence/cooperation |
37-
| 5 | `.trinity/experience.md` | W401 learnings |
38-
| 6 | git/PR | squash-merge to `trinity-rust-rings`, close #1303, open #W402 |
29+
| 1 | `.claude/plans/wave-loop-402.md` | Decomposed plan + weak-point + competitor scan |
30+
| 2 | `fpga/HARDWARE_SSOT.md` (Variant A) | Measured CCLK frequency/duty cycle on P12 |
31+
| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | Formal STAT/decision-tree lemmas |
32+
| 4 | `cli/tri/src/fpga.rs` (Variant C) | Optional cable-connected SRAM smoke load |
33+
| 5 | `docs/reports/*` | W402 report, evidence, W403 cooperation |
34+
| 6 | `.trinity/experience.md` | W402 learnings |
35+
| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1305, open #W403 |
3936

4037
---
4138

4239
## Acceptance criteria
4340

44-
- [ ] AC1: `tri fpga smoke-gate` asserts `OSCFSEL=0` and no CRC writes.
45-
- [ ] AC2: `tri fpga boot-protocol --checklist` prints the cold-POR steps.
46-
- [ ] AC3: `tri fpga measure-cclk --csv` parses DSView, PulseView, and Saleae CSV
47-
exports.
48-
- [ ] AC4: Unit tests for CSV parsing pass.
49-
- [ ] AC5: Board-less dry-run sweep + report path is exercised in CI/smoke gate.
50-
- [ ] AC6: `./scripts/tri test` passes (575/575).
51-
- [ ] AC7: W401 report + evidence + W402 cooperation variants committed.
52-
- [ ] AC8: If a physical CCLK capture is available, pin P12 frequency is recorded
53-
in `fpga/HARDWARE_SSOT.md`.
41+
- [ ] AC-A1 (Variant A): a physical CCLK trace is captured and the dominant
42+
frequency is recorded.
43+
- [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.5 contains the measured value.
44+
- [ ] AC-B1 (Variant B): new Lean 4 module builds and links `STAT` decoding to the
45+
documented decision trees.
46+
- [ ] AC-C1 (Variant C): `tri fpga smoke-gate --require-cable` reaches
47+
`DONE=HIGH` on the bench.
48+
- [ ] AC-D1: `./scripts/tri test` passes.
49+
- [ ] AC-D2: W402 report + evidence + W403 cooperation variants committed.
5450

5551
---
5652

5753
## Default variant
5854

59-
Execute **Variant A** from `docs/reports/FPGA_LOOP_COOPERATION_2026-07-08.md`
60-
when a logic analyser is available; otherwise execute **Variant B**:
61-
board-less hardening and CI guards. This wave implements both so that the
62-
physical capture can be slotted in as soon as hardware is ready.
55+
Execute **Variant A** when a logic analyser / oscilloscope is available; otherwise
56+
fall back to **Variant B** (Lean 4 formalization). **Variant C** is a stretch
57+
goal once Variant A is closed.
6358

6459
---
6560

0 commit comments

Comments
 (0)