Skip to content

Commit ee99f6d

Browse files
Dmitrii Vasilevclaude
Dmitrii Vasilev
and
claude
committed
feat(igla): Wave Loop 433 — formal bridge fallback, compose W431 XADC envelope with W432 per-corner raw-ns OSCFSEL theorem
- Add three theorems in TernaryFPGABoot.lean: - xadc_envelope_justifies_cclk_variant_raw_ns_pvt - xadc_envelope_justifies_cclk_variant_transaction_ok - xadc_live_example_oscfsel_6_raw_ns_pvt - Refresh T27_VS_FORMAL_HDL_2026.md competitor snapshot for W433. - Update GEN_VERILOG_DEFECTS_REPRO.md baseline for W433 (7 residual yosys smoke failures remain). - Add WAVE_LOOP_433_REPORT.md, FPGA_LOOP_EVIDENCE_W433_2026-07-01.md, FPGA_LOOP_COOPERATION_W434_2026-07-01.md. - Update NOW.md and current-issue.md for W434 (#1395). Closes #1393 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 9e93632 commit ee99f6d

10 files changed

Lines changed: 662 additions & 64 deletions

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

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
# Wave Loop 433 Decomposed Plan
2+
3+
**Issue:** #1393
4+
**Branch:** `wave-loop-433`
5+
**Date:** 2026-07-01
6+
**Anchor:** φ² + φ⁻² = 3 | TRINITY
7+
8+
---
9+
10+
## 1. Weak-point analysis
11+
12+
### Physical bench (still blocked)
13+
- P12 (CFGCLK / CCLK_0) is not wired to a logic-analyzer channel.
14+
- No relay / remote-power cold-POR gate is wired.
15+
- The on-board Xilinx DLC10 / Platform Cable USB II is not connected.
16+
- **Implication:** Variant A (real CCLK capture) and Variant B (live XADC + real board) are not executable unless the user has wired new hardware since W432.
17+
18+
### Master-merge debt (still blocked)
19+
- W432 probed `origin/master` and found the `gen-verilog` fix set (`701d79b3b`, `507408f47`) is on a divergent `master` lineage not safely reachable from `wave-loop-432`.
20+
- A direct cherry-pick of `507408f47` conflicts heavily with `bootstrap/src/compiler.rs`, seals, and `docs/NOW.md`.
21+
- **Implication:** Variant C1 (master-merge to clear #1245) is high-risk and would destabilize the FPGA/formal work. It should only be attempted in a dedicated wave when the boot-evidence line is not the primary focus.
22+
23+
### Formal gap left by W432
24+
- W432 added per-process-corner raw-ns OSCFSEL theorems at the **worst-case** envelope corner (temp = +85 °C, vccint = 900 mV).
25+
- A live `tri fpga read-xadc` measurement will almost always be **inside** the envelope but not exactly at the worst-case corner.
26+
- The W431 bridge (`xadc_envelope_implies_raw_ns_satisfies_any_in_envelope`) shows that any raw-ns capture safe at the worst-case corner is also safe at any in-envelope point.
27+
- **Gap:** there is no single theorem that says "for any OSCFSEL and any in-envelope live XADC point, the nominal raw-ns period is safe under the measured PVT context." Closing this gap makes the W432 corner theorem directly usable with real XADC data.
28+
29+
### Tooling/reporting gap
30+
- `tri fpga sweep-report --json` exists but does not surface per-variant PVT context or process-corner metadata.
31+
- `docs/reports/T27_VS_FORMAL_HDL_2026.md` needs a late-July 2026 refresh (firtool 1.152.0 published July 4, Sparkle IP.Net PR #66 still open, Clash 1.11 candidate).
32+
- `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` needs a W433 triage entry.
33+
34+
---
35+
36+
## 2. Competitor research (summary)
37+
38+
- **Sparkle / Verilean:** PR #66 ("IP.Net") remains the headline signal — USB web server + memcached + compiler perf, +27k lines. Last public push 2026-07-03. No new public PRs after that. The RV32 divider proof (commit `9c7809c`, June 25) remains the deepest formal IP-level proof t27 has not yet matched.
39+
- **Clash 1.11.0:** still a Hackage candidate as of late July 2026; no promoted release. Latest official release remains 1.10.0 (April 2026).
40+
- **CIRCT / firtool:** `firtool-1.152.0` was published 2026-07-04; it is a maintenance release (ImportVerilog/Moore, Arc dialect, FIRRTL inliner). The major formal-verification expansion was `firtool-1.143.0` (March 2026). PR #10387 (`ifdef SYNTHESIS` guards for SV lowering) was merged in May and later reconsidered.
41+
- **Aria-HDL / fpga-meta-compiler-public:** Rust-based meta-compiler with `--emit-lean4` proof extraction and `--emit-sby` backend. Recent 2026 updates around Leiserson-Saxe retiming, constraint annotations, and PCIe BAR testing.
42+
- **CktFormalizer:** arXiv 2605.07782 (autoformalization into dependently-typed Lean 4 HDL) — no new public July signal, but reinforces the "Lean 4 as hardware proof backend" trend.
43+
44+
---
45+
46+
## 3. Selected primary variant
47+
48+
**Variant C3 — formal bridge fallback**
49+
50+
Land a board-less formal lemma that connects a live `XadcOperatingPoint` to the
51+
W432 per-process-corner raw-ns OSCFSEL theorem. This closes the remaining gap in
52+
the boot-to-proof pipeline without touching the compiler or requiring physical
53+
hardware.
54+
55+
### Acceptance criteria
56+
- New theorem `xadc_envelope_justifies_cclk_variant_raw_ns_pvt` in
57+
`proofs/lean4/Trinity/TernaryFPGABoot.lean` passes `lake build`.
58+
- New transaction variant `xadc_envelope_justifies_cclk_variant_transaction_ok`.
59+
- `cargo test --bin tri fpga::` passes.
60+
- `./scripts/tri test` passes with the documented 7-failure baseline.
61+
- `docs/reports/T27_VS_FORMAL_HDL_2026.md` and
62+
`docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` are refreshed.
63+
- W433 report, evidence note, and W434 cooperation variants are written.
64+
- GitHub issue and branch for W434 are created.
65+
66+
---
67+
68+
## 4. Decomposed tasks
69+
70+
1. **Formal lemma**
71+
- Add `xadc_envelope_justifies_cclk_variant_raw_ns_pvt`.
72+
- Add `xadc_envelope_justifies_cclk_variant_transaction_ok`.
73+
- Build `Trinity.TernaryFPGABoot`.
74+
75+
2. **Rust validation**
76+
- Run `cargo test --bin tri fpga::`.
77+
78+
3. **Full CI sweep**
79+
- Run `./scripts/tri test` and record baseline.
80+
81+
4. **Documentation refresh**
82+
- Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md`.
83+
- Add W433 triage to `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`.
84+
85+
5. **Close-out artifacts**
86+
- Write `docs/reports/WAVE_LOOP_433_REPORT.md`.
87+
- Write `docs/reports/FPGA_LOOP_EVIDENCE_W433_2026-07-01.md`.
88+
- Write `docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md`.
89+
90+
6. **Next-wave setup**
91+
- Create GitHub issue #? for W434.
92+
- Create and push branch `wave-loop-434`.
93+
- Update `.trinity/current-issue.md` and `docs/NOW.md`.
94+
- Append W433 learnings to `.trinity/experience.md`.
95+
- Save persistent memory entry.
96+
97+
---
98+
99+
## 5. Fallback if formal lemma is blocked
100+
101+
If the Lean composition proves unexpectedly difficult, redirect to one of:
102+
103+
- **C2-bis:** harden `tri fpga sweep-report --json` with per-variant `process_corner` / `pvt_context` fields (when boot-log JSON contains XADC data).
104+
- **C4:** deeper competitor refresh only, with a clear note that no code changed.
105+
106+
---
107+
108+
*φ² + φ⁻² = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 17 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,20 @@
1-
# Wave Loop 433 — FPGA boot-evidence next variant (real CCLK capture, live XADC validation, or master-merge retry)
1+
# Wave Loop 434 — FPGA boot-evidence next variant (real capture, live XADC validation, or master-merge retry)
22

3-
**Issue:** #1393
4-
**Branch:** `wave-loop-433`
5-
**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 432.
3+
**Issue:** #1395
4+
**Branch:** `wave-loop-434`
5+
**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 433.
66

77
---
88

99
## Goal
1010

11-
Wave Loop 432 shipped per-process-corner raw-ns OSCFSEL theorems in Lean 4 and
12-
probed the `origin/master` merge path for the `gen-verilog` fix set
13-
(`701d79b3b`), finding it not safely reachable from `wave-loop-432`. The bench
14-
remains blocked (P12 unwired, no relay gate, no DLC10 cable). Wave Loop 433
15-
executes the first available variant from
16-
`docs/reports/FPGA_LOOP_COOPERATION_W433_2026-07-01.md`.
11+
Wave Loop 433 composed the W431 live-XADC envelope bound with the W432
12+
per-process-corner raw-ns OSCFSEL theorem, producing a single theorem that covers
13+
any in-envelope XADC operating point and any documented OSCFSEL selection. The
14+
bench remains blocked (P12 unwired, no relay gate, no DLC10 cable) and the
15+
master-merge path for the `gen-verilog` fix set (`701d79b3b`) is still not safely
16+
reachable from `wave-loop-433`. Wave Loop 434 executes the first available variant
17+
from `docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md`.
1718

1819
1. **Variant A (preferred when bench becomes fully available):**
1920
- Confirm P12 is wired to a logic-analyzer channel and a relay/remote-power
@@ -24,13 +25,16 @@ executes the first available variant from
2425
- Import with `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone
2526
--validate --pvt-context <xadc.json> --out <theorem.lean> --json` and commit
2627
generated Lean theorems plus JSON summaries.
28+
- Reference the W433 quantified theorem
29+
(`xadc_envelope_justifies_cclk_variant_raw_ns_pvt`) in the generated proof.
2730
- Update `fpga/HARDWARE_SSOT.md` §3.6 with measured frequency/duty/margin.
2831

2932
2. **Variant B (if board is reachable but P12 / relay are still blocked):**
3033
- Capture a real `tri fpga read-xadc --json` from the live board.
3134
- Verify the JSON converts to a valid `PvtContext` via `tri fpga pvt-envelope`.
3235
- Generate at least one `measured-to-lean` theorem using the real XADC context
3336
(synthetic CCLK fixture is acceptable for proof-of-pipeline).
37+
- Reference the W433 quantified theorem in the generated proof.
3438
- Alternatively, run `tri fpga cclk-sweep` over OSCFSEL 0..5 with `--xadc` and
3539
manual power cycles.
3640
- Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md` and re-evaluate
@@ -41,9 +45,8 @@ executes the first available variant from
4145
the `gen-verilog` fix set (`701d79b3b`) into the wave-loop line and clear the
4246
7 residual yosys smoke failures (#1245).
4347
- If the merge is still too risky, land another formal/tooling sub-task:
44-
machine-readable `sweep-report --json` hardening, a Lean theorem linking a
45-
live `XadcOperatingPoint` to the per-process-corner raw-ns OSCFSEL theorem,
46-
or a deeper competitor refresh.
48+
harden `measured-to-lean` to emit the W433 theorem name, add a computable
49+
combined OSCFSEL+XADC envelope check, or refresh the competitor report.
4750
- Update `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` with the new baseline.
4851

4952
---
@@ -57,7 +60,7 @@ executes the first available variant from
5760
cleared).
5861
- [ ] `cargo test --bin tri fpga::` passes.
5962
- [ ] Close-out report and next-wave cooperation variants are written.
60-
- [ ] Issue/branch for Wave Loop 434 are created.
63+
- [ ] Issue/branch for Wave Loop 435 are created.
6164

6265
---
6366

‎.trinity/current_task/activity.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1604,3 +1604,7 @@
16041604
- **Commit:** feat(igla): Wave Loop 432 — per-process-corner raw-ns OSCFSEL theorems, master-merge feasibility probe, W432 close-out artifacts
16051605
- **Files:** .trinity/experience.md
16061606

1607+
## 2026-07-05T12:07:23Z — wave-loop-433
1608+
- **Commit:** docs(experience): W432 learnings — per-process-corner theorem, master-merge probe, blocked bench redirect
1609+
- **Files:** .claude/plans/wave-loop-433.md,.trinity/current-issue.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md,docs/reports/FPGA_LOOP_EVIDENCE_W433_2026-07-01.md,docs/reports/GEN_VERILOG_DEFECTS_REPRO.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_433_REPORT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
1610+

‎docs/NOW.md‎

Lines changed: 29 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,41 @@
1-
# NOW — Wave Loop 432 close-out / Wave Loop 433 setup (2026-07-01)
1+
# NOW — Wave Loop 433 close-out / Wave Loop 434 setup (2026-07-01)
22

33
**Last updated:** 2026-07-01
44

5-
## Wave Loop 432 — FPGA boot-evidence per-process-corner raw-ns theorems (Closes #1391)
5+
## Wave Loop 433 — FPGA boot-evidence XADC-to-OSCFSEL raw-ns PVT bridge (Closes #1393)
66

7-
- Branch: `wave-loop-432`
8-
- Issue: #1391
7+
- Branch: `wave-loop-433`
8+
- Issue: #1393
99
- PR: (to open after this close-out)
10-
- Report: `docs/reports/WAVE_LOOP_432_REPORT.md`
11-
- Evidence W432: `docs/reports/FPGA_LOOP_EVIDENCE_W432_2026-07-01.md`
12-
- Cooperation W433: `docs/reports/FPGA_LOOP_COOPERATION_W433_2026-07-01.md`
10+
- Report: `docs/reports/WAVE_LOOP_433_REPORT.md`
11+
- Evidence W433: `docs/reports/FPGA_LOOP_EVIDENCE_W433_2026-07-01.md`
12+
- Cooperation W434: `docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md`
1313

14-
### What landed (Variant C2 — bench still blocked)
14+
### What landed (Variant C3 — bench still blocked)
1515

1616
- `proofs/lean4/Trinity/TernaryFPGABoot.lean`
17-
- Added `cclk_variant_raw_ns_per_process_corner_pvt_satisfies_flash_spec`:
18-
for every documented OSCFSEL 0..7 and every process corner (`ff`/`tt`/`ss`),
19-
the ideal raw-ns CCLK capture satisfies the PVT-aware flash predicate at the
20-
worst-case envelope corner.
21-
- Added `cclk_variant_raw_ns_per_process_corner_pvt_implies_transaction_ok`:
22-
the same capture produces a flash-spec-compliant SPI read transaction.
17+
- Added `xadc_envelope_justifies_cclk_variant_raw_ns_pvt`: for every OSCFSEL 0..7
18+
and any in-envelope `XadcOperatingPoint` with corner at least as slow as `ss`,
19+
the nominal raw-ns CCLK capture satisfies the PVT-aware flash predicate under
20+
the measured context.
21+
- Added `xadc_envelope_justifies_cclk_variant_transaction_ok`: the same capture
22+
produces a flash-spec-compliant SPI read transaction.
23+
- Added `xadc_live_example_oscfsel_6_raw_ns_pvt`: concrete example for OSCFSEL=6
24+
and a representative live readout.
2325

2426
- `docs/reports/T27_VS_FORMAL_HDL_2026.md`
25-
- Refreshed for W432; noted the per-process-corner theorem, the blocked bench,
26-
the unchanged 7 residual yosys failures, and July 2026 competitor signals
27-
(firtool 1.152.0, Aria-HDL retiming/PCIe BAR, Clash 1.11 candidate).
27+
- Refreshed for W433; noted Sparkle PR #66 remains open, `firtool-1.152.0`
28+
published 2026-07-04, Clash 1.11 candidate still unreleased, Aria-HDL updates,
29+
and the W433 theorem composition.
2830

2931
- `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`
30-
- Documented the W432 triage decision: the `origin/master` merge probe did not
31-
bring the `gen-verilog` fix set (`701d79b3b`) into `wave-loop-432`; the
32-
fix commits are on a divergent `master` lineage. The 7 residual yosys smoke
33-
failures remain the documented baseline.
32+
- Documented the W433 triage decision: no compiler work attempted; the 7
33+
residual yosys smoke failures remain the documented baseline.
3434

3535
- Close-out artifacts:
36-
`docs/reports/WAVE_LOOP_432_REPORT.md`,
37-
`docs/reports/FPGA_LOOP_EVIDENCE_W432_2026-07-01.md`,
38-
`docs/reports/FPGA_LOOP_COOPERATION_W433_2026-07-01.md`.
36+
`docs/reports/WAVE_LOOP_433_REPORT.md`,
37+
`docs/reports/FPGA_LOOP_EVIDENCE_W433_2026-07-01.md`,
38+
`docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md`.
3939

4040
### Not done (blocked on hardware or out of scope)
4141

@@ -44,7 +44,7 @@
4444
- Real cold-POR `cclk-sweep --xadc` with manual power cycle — possible but not
4545
performed this wave.
4646
- Master-merge to clear #1245 — fix set not safely reachable from
47-
`wave-loop-432` this wave.
47+
`wave-loop-433` this wave.
4848

4949
### Verification
5050

@@ -55,12 +55,12 @@
5555

5656
---
5757

58-
## Wave Loop 433 — Next: real capture, live XADC validation, or master-merge retry
58+
## Wave Loop 434 — Next: real capture, live XADC validation, or master-merge retry
5959

60-
- Branch: `wave-loop-433` (to create)
61-
- Issue: #1393
60+
- Branch: `wave-loop-434` (to create)
61+
- Issue: (to create)
6262
- Default variant: **B** unless P12 or the relay gate becomes available.
63-
- Plan: `docs/reports/FPGA_LOOP_COOPERATION_W433_2026-07-01.md`
63+
- Plan: `docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md`
6464

6565
---
6666

0 commit comments

Comments
 (0)