Skip to content

Commit a0f024c

Browse files
gHashTaggHashTag
authored
feat(igla): Wave Loop 411 — measured-to-lean auto-proof, PVT-margin predicate, W411 close-out docs
Closes #1329 🤖 Generated with [Claude Code](https://claude.com/claude-code)
1 parent c4dc8ee commit a0f024c

11 files changed

Lines changed: 2428 additions & 95 deletions

File tree

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

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
# Wave Loop 411 — real P12 + OSCFSEL 6/7 retry, relay CI gate, or auto-proof tooling
2+
3+
**Issue:** #1329
4+
**Branch:** `wave-loop-411`
5+
**Date:** 2026-07-04
6+
**Milestone:** W410 completed the measured-duty formal link but both physical
7+
paths (real P12 capture and DLC10-based `OSCFSEL=6,7` boot) remain blocked by
8+
missing bench wiring and the missing DLC10 cable. W411 either finally connects
9+
the bench or uses the cycle to build automation/formal tooling.
10+
11+
---
12+
13+
## Goal
14+
15+
1. **Variant A** — Real P12 CCLK capture + physical `OSCFSEL=6,7` cold-POR
16+
boot. Requires wiring P12 to a logic-analyzer channel and connecting the
17+
Digilent DLC10 cable to the host.
18+
2. **Variant B** — Relay-controlled cold-POR hardware CI gate. Build the relay
19+
+ tri-stateable JTAG automation infrastructure so the flash-boot gate can
20+
run unattended.
21+
3. **Variant C** — Auto-proof tooling + PVT margins. Add a subcommand that
22+
generates a Lean theorem from a `tri fpga measure-cclk --json` measurement,
23+
and extend the formal model with conservative process/voltage/temperature
24+
margins.
25+
26+
Default recommendation: **Variant A + C bundle**. However, the 2026-07-04 bench
27+
check confirms both physical blockers persist (P12 not wired, DLC10 not
28+
detected). Therefore the **effective W411 default falls back to Variant C
29+
alone**, with a small relay-trait scaffold from Variant B kept as a documented
30+
optional add-on if time allows.
31+
32+
---
33+
34+
## Weak points investigated
35+
36+
| Weak point | Risk | How this wave addresses it |
37+
|---|---|---|
38+
| Measured CCLK data still requires manual copy-paste into Lean | Human error, not reproducible in CI | Add `tri fpga measured-to-lean` that reads `--json` output and emits a type-correct theorem skeleton |
39+
| Formal model has no PVT margin layer | A single measured frequency does not prove compliance across temp/voltage/process corners | Add conservative temperature/voltage derating to `t_CL`/`t_CH` and prove the margin predicate still implies `transaction_satisfies_flash_spec` |
40+
| `measured_cclk_satisfies_flash_spec` only checks one corner | Silicon CCLK and flash timing both vary with conditions | Introduce `measured_cclk_with_margin_satisfies_flash_spec` parameterized by temp (°C) and voltage (mV) |
41+
| No board-less way to exercise the formal link end-to-end | The theorem is only tested by `decide` on a few examples | Add Rust-driven round-trip test: generate synthetic fixture → JSON → theorem snippet, and verify it type-checks against the Lean model |
42+
| Relay-controlled cold-POR is still undefined | W405's manual power-cycle prevents unattended CI | (Optional) Add a `PowerSwitch` trait + mock implementation behind `--auto-power-cycle`, without requiring real relay hardware |
43+
| Competitors can claim the measured-duty link is ad-hoc | The bridge between Rust and Lean is not principled | Mirror the integer-period/duty conversion exactly in both languages and document the conservative rounding directions in one place (`fpga/HARDWARE_SSOT.md`) |
44+
45+
---
46+
47+
## Competitor scan (2026-07-04)
48+
49+
| Competitor / project | Relevant capability | t27 differentiator after W411 |
50+
|---|---|---|
51+
| [Sparkle HDL / Verilean](https://github.com/Verilean/sparkle) | Lean 4 HDL compiler + cycle-accurate simulation | Sparkle has no public 7-series configuration-engine timing model. t27 adds a *measured-to-formal* pipeline: `sigrok-cli` capture → Rust JSON → Lean theorem. |
52+
| [Kami / Kôika](https://github.com/SteffenReith/Kami) | Coq-based hardware DSL + verified compilation | Kami proves custom processors; t27 proves vendor FPGA configuration timing with external-flash datasheet margins. |
53+
| [Project X-Ray / prjxray](https://github.com/f4pga/prjxray) | Reverse-engineered 7-series bitstream docs | prjxray documents *what* the bits mean; t27 formalizes the *timing consequences* across PVT corners. |
54+
| [OpenTitan](https://opentitan.org/book/doc/security/specs/secure_boot/) | Secure SoC boot / RoT with formal security verification | OpenTitan secures processor boot; t27 secures the FPGA *configuration stage* including external SPI flash PVT margins. |
55+
| [spispy](https://github.com/StackSmashing/spispy) / SPI flash emulators | SPI flash emulation/monitoring | Emulators study protocol semantics; t27 models real N25Q128 timing with conservative margins and validates against live capture. |
56+
| Commercial SPI NOR VIP | Closed simulation reference models | t27 provides an open, machine-checked Lean 4 bound tied to a real Artix-7 board and a `sigrok-cli` measurement gate, plus PVT margin reasoning. |
57+
| Yosys + SymbiYosys / Verilator formal | Open-source RTL formal verification | These verify custom RTL; t27 verifies vendor configuration-engine behavior and external flash interface timing at the system level. |
58+
59+
After W411, the defensive value is a **machine-checked, PVT-margin-aware,
60+
measured-to-formal pipeline** that turns a real CCLK capture into a
61+
`transaction_satisfies_flash_spec` proof. The remaining competitive gap is the
62+
physical P12 measurement, which is blocked only by wiring.
63+
64+
---
65+
66+
## Decomposed plan
67+
68+
| Step | File(s) | Deliverable |
69+
|---|---|---|
70+
| 1 | `.claude/plans/wave-loop-411.md` | This plan: weak points, competitor scan, chosen fallback variant |
71+
| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | `measured_cclk_with_margin_satisfies_flash_spec` predicate and theorem linking it to `transaction_satisfies_flash_spec`; helper lemmas for conservative PVT derating |
72+
| 3 | `cli/tri/src/fpga.rs` | New `tri fpga measured-to-lean` subcommand; `MeasuredCclk` helper to print a Lean theorem snippet; optional `PowerSwitch` trait scaffold for Variant B |
73+
| 4 | `fpga/HARDWARE_SSOT.md` §3.6.10/§3.6.11 | Document the measured-to-Lean pipeline and the PVT margin model; note remaining P12/DLC10 blockers |
74+
| 5 | `cli/tri/src/fpga.rs` tests + integration test | Round-trip test: synthetic fixture → JSON → theorem snippet parseable by Lean |
75+
| 6 | `docs/reports/FPGA_LOOP_EVIDENCE_W411_2026-07-04.md` | Build outputs, `measured-to-lean` example, Lean build, Rust tests, `tri test` summary |
76+
| 7 | `docs/reports/WAVE_LOOP_411_REPORT.md` | Close-out report with AC status |
77+
| 8 | `docs/reports/FPGA_LOOP_COOPERATION_W412_2026-07-04.md` | Three W412 cooperation variants |
78+
| 9 | `docs/NOW.md`, `.trinity/experience.md`, `.trinity/current-issue.md` | W411 entry, learnings, and updated AC status |
79+
| 10 | git/PR | Commit, push `wave-loop-411`, open PR #1329, create W412 issue/branch |
80+
81+
---
82+
83+
## Acceptance criteria
84+
85+
- [ ] AC-C1: `measured-to-lean` subcommand emits a type-correct Lean theorem
86+
skeleton from `--json` input.
87+
- [ ] AC-C2: PVT margin predicate exists in Lean 4 and implies
88+
`measured_cclk_satisfies_flash_spec`.
89+
- [ ] AC-C3: A Lean theorem proves that the PVT margin predicate implies
90+
`transaction_satisfies_flash_spec`.
91+
- [ ] AC-B1 (optional): `PowerSwitch` trait + mock relay exists behind an
92+
`--auto-power-cycle` flag scaffold, or explicitly deferred.
93+
- [ ] AC-D1: `lake build Trinity.TernaryFPGABoot` passes with the new lemmas.
94+
- [ ] AC-D2: `cargo test -p tri fpga::tests` passes.
95+
- [ ] AC-D3: `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
96+
- [ ] AC-D4: gen-verilog-yosys-smoke failures remain tracked separately.
97+
- [ ] AC-D5: W411 report + evidence + W412 cooperation variants committed.
98+
99+
---
100+
101+
## Chosen variant
102+
103+
**Variant C alone** (auto-proof tooling + PVT margins), with an optional small
104+
Variant B scaffold if time allows. This is the strongest implementable step
105+
while the bench remains blocked.
106+
107+
---
108+
109+
*phi^2 + 1/phi^-2 = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 63 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -1,68 +1,89 @@
1-
# Wave Loop 405 — FPGA boot loop closure (variant A/B/C)
1+
# Wave Loop 411 — real P12 + OSCFSEL 6/7 retry, relay CI gate, or auto-proof tooling
22

3-
**Issue:** #1311
4-
**Branch:** `wave-loop-405`
5-
**Milestone:** W404 closed the SRAM hardware smoke gate. W405 should close one
6-
of the remaining gaps: real CCLK measurement, flash-boot cold-POR gate, or
7-
formal CCLK timing-safety.
3+
**Issue:** #1329
4+
**Branch:** `wave-loop-411`
5+
**Milestone:** W410 completed the measured-duty formal link but both physical
6+
paths (real P12 capture and DLC10-based `OSCFSEL=6,7` boot) remain blocked. W411
7+
either finally connects the bench or uses the extra cycle to build automation /
8+
formal tooling.
89

910
---
1011

1112
## Goal
1213

13-
1. **Variant A** — Capture the actual CCLK frequency/duty cycle on pin P12 and
14-
record it in `fpga/HARDWARE_SSOT.md` §3.5.
15-
2. **Variant B** — Extend `tri fpga smoke-gate --require-cable` to flash boot:
16-
program flash, prompt for power-cycle, capture cold-POR STAT, assert
17-
`boot_success`.
18-
3. **Variant C** — Extend the Lean 4 model with `OSCFSEL` constants, nominal
19-
CCLK ranges, and a `cclk_within_flash_spec` predicate; prove the canonical
20-
config is timing-safe.
21-
4. Update close-out reports and open W406 cooperation variants.
14+
1. **Variant A** — Real P12 CCLK capture + physical `OSCFSEL=6,7` cold-POR
15+
boot. Wire P12 to ADBUS4 (or a DSLogic/scope channel), connect the DLC10
16+
cable, capture the real CCLK, run the 6/7 sweep, and turn the measured
17+
values into a `measured_cclk_satisfies_flash_spec` proof.
18+
2. **Variant B** — Relay-controlled cold-POR hardware CI gate. Build the
19+
relay + tri-stateable JTAG automation infrastructure so the flash-boot gate
20+
can run unattended.
21+
3. **Variant C** — Auto-proof tooling + PVT margins. Add a subcommand that
22+
generates a Lean theorem from a `--json` measurement, and extend the formal
23+
model with conservative process/voltage/temperature margins.
24+
25+
Default recommendation: **Variant A + C bundle**. If the bench is still
26+
unavailable, pick **Variant B** or **Variant C alone**.
2227

2328
---
2429

2530
## Decomposed plan
2631

27-
See `.claude/plans/wave-loop-405.md` for the full weak-point / competitor scan
28-
and detailed decomposition.
32+
See `docs/reports/FPGA_LOOP_COOPERATION_W411_2026-07-04.md` for the full
33+
weak-point / competitor scan and detailed decomposition.
2934

3035
| Step | File(s) | Deliverable |
31-
|------|---------|-------------|
32-
| 1 | `.claude/plans/wave-loop-405.md` | Decomposed plan + weak-point + competitor scan |
33-
| 2 | `fpga/HARDWARE_SSOT.md` (Variant A) | Measured CCLK frequency/duty cycle on P12 |
34-
| 3 | `cli/tri/src/fpga.rs` (Variant B) | `--flash-boot` flag + program/reset/capture flow |
35-
| 4 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant C) | OSCFSEL/CCLK-bound lemmas |
36-
| 5 | `docs/reports/*` | W405 report, evidence, W406 cooperation |
37-
| 6 | `.trinity/experience.md` | W405 learnings |
38-
| 7 | git/PR | squash-merge to master, close #1311, open #W406 |
36+
|---|---|---|
37+
| 1 | `docs/reports/FPGA_LOOP_COOPERATION_W411_2026-07-04.md` | Cooperation variants |
38+
| 2 | `fpga/HARDWARE_SSOT.md` §3.6.1/§3.6.9 (Variant A) | Real measured CCLK and 6/7 boot status |
39+
| 3 | `build/fpga/` + `docs/reports/` (Variant A) | Real capture CSV + boot-log JSON |
40+
| 4 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant A/C) | `measured_*_satisfies_flash_spec` instance from real data |
41+
| 5 | `cli/tri/src/fpga.rs` (Variant B/C) | Relay trait + auto-power-cycle mode, or `measured-to-lean` subcommand |
42+
| 6 | `docs/reports/*` | W411 report, evidence, W412 cooperation |
43+
| 7 | `.trinity/experience.md` | W411 learnings |
44+
| 8 | `docs/NOW.md` | W411 entry |
45+
| 9 | git/PR | squash-merge to master, close #1329, open #W412 |
3946

4047
---
4148

4249
## Acceptance criteria
4350

44-
- [ ] AC-A1 (Variant A): a physical CCLK trace is captured and the dominant
45-
frequency is recorded.
46-
- [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.5 contains the measured value.
47-
- [ ] AC-B1 (Variant B): `tri fpga smoke-gate --require-cable --flash-boot`
48-
programs flash and asserts `boot_success` after a cold POR.
49-
- [ ] AC-C1 (Variant C): new Lean 4 lemmas link `OSCFSEL`/CCLK bounds to the
50-
documented decision trees.
51-
- [ ] AC-D1: `./scripts/tri test` passes.
52-
- [ ] AC-D2: W405 report + evidence + W406 cooperation variants committed.
51+
- [ ] AC-A1: real P12 CCLK capture CSV exists (or blocker documented). **Blocked — P12 not wired.**
52+
- [ ] AC-A2: `OSCFSEL=6,7` boot logs exist (PASS or documented failure). **Blocked — DLC10 cable missing.**
53+
- [ ] AC-A3: a Lean theorem links the captured `(frequency, duty)` pair to
54+
`transaction_satisfies_flash_spec`. **Delivered via `measured-to-lean` generated theorems on synthetic data.**
55+
- [ ] AC-B1: relay auto-power-cycle mode exists behind a trait with a board-less
56+
mock path, or explicitly deferred. **Deferred to W412.**
57+
- [x] AC-C1: `measured-to-lean` subcommand generates a type-correct theorem
58+
skeleton from `--json`.
59+
- [x] AC-C2: PVT margin predicate exists in Lean 4 and implies
60+
`measured_cclk_satisfies_flash_spec`.
61+
- [x] AC-C3: A Lean theorem proves that the PVT margin predicate implies
62+
`transaction_satisfies_flash_spec`.
63+
- [x] AC-D1: `lake build Trinity.TernaryFPGABoot` passes.
64+
- [x] AC-D2: `cargo test -p tri fpga::tests` passes.
65+
- [x] AC-D3: `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
66+
- [x] AC-D4: gen-verilog-yosys-smoke failures remain tracked separately.
67+
- [x] AC-D5: W411 report + evidence + W412 cooperation variants committed.
5368

5469
---
5570

56-
## Default variant
71+
## Close-out note
72+
73+
W411 implemented **Variant C alone** because the bench blockers persisted. The
74+
`tri fpga measured-to-lean` subcommand and the PVT-margin predicate close two
75+
real weak points in the measured-to-formal pipeline. Variant A and the physical
76+
half of any bundle remain blocked until P12 is wired and the DLC10 cable is
77+
connected.
5778

58-
The bench cable and board are reachable, so the recommended default is
59-
**Variant B** (flash-boot cold-POR smoke gate). It directly extends the W404
60-
SRAM gate and closes the boot loop end-to-end.
79+
---
80+
81+
## Default variant
6182

62-
If the manual power-cycle step proves too awkward, fall back to **Variant C**
63-
(no hardware) and pursue Variant B in W406. If a logic analyzer / oscilloscope
64-
becomes available before implementation starts, switch to **Variant A**.
83+
**Variant A + C bundle**: physical measurement and 6/7 boot, with auto-proof
84+
tooling. If the bench is still unavailable, fall back to **Variant B** (relay
85+
CI gate) or **Variant C alone** (formal-tooling improvements).
6586

6687
---
6788

68-
*φ² + φ⁻² = 3 | TRINITY*
89+
*phi^2 + phi^-2 = 3 | TRINITY*

0 commit comments

Comments
 (0)