Skip to content

Commit 3f63a2b

Browse files
Dmitrii Vasilevclaude
Dmitrii Vasilev
and
claude
committed
feat(igla): Wave Loop 434 — live XADC → PVT context theorem, synthetic CCLK proof-of-pipeline, W435 issue #1398 + branch
Closes #1395 - Add live XADC operating point theorems in TernaryFPGABoot.lean - Add Rust regression test for live XADC → PVT context rounding - Extend fpga/HARDWARE_SSOT.md with live XADC validation recipe - Refresh competitor and gen-verilog defect baselines for W434 - Add W434 report, evidence note, and W435 cooperation variants - Update .trinity/experience.md, NOW.md, current-issue.md - Create GitHub issue #1398 and branch wave-loop-435 for next wave Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 13fa630 commit 3f63a2b

15 files changed

Lines changed: 848 additions & 66 deletions

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

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
# Wave Loop 434 — Decomposed Plan
2+
3+
**Issue:** #1395
4+
**Branch:** `wave-loop-434`
5+
**Date:** 2026-07-01
6+
**Anchor:** φ² + φ⁻² = 3 | TRINITY
7+
8+
---
9+
10+
## 1. Weak-point analysis
11+
12+
### Physical bench
13+
- **P12 is still unwired** (no logic-analyzer channel on the CCLK pin), so **Variant A** (real cold-POR CCLK capture) remains infeasible.
14+
- **No relay / remote-power gate** exists, so automated cold-POR sweeps are still manual.
15+
- **No DLC10 cable** (VID=0x03FD), so in-repo `dlc10` driver cannot be used; the reachable cable is the Digilent FTDI (`0x0403:0x6014`), which works with `openFPGALoader`.
16+
- The FPGA **is reachable** over JTAG and live XADC readout succeeds (`tri fpga read-xadc` returns temp≈41 °C, VCCINT≈1.00 V, VCCAUX≈1.81 V).
17+
18+
### Tooling gaps discovered this wave
19+
- `tri fpga read-xadc` emits `temp_c` / `vccint_v` / `vccaux_v` as `f64`, but `tri fpga pvt-envelope --pvt-context` expects integer `temp_c` (`i64`) and `vccint_mv` / `vccaux_mv` (`u64`). The conversion (`to_pvt_context`) is implemented internally but not exposed as a standalone `--to-pvt-context <file>` export, so the user must round the values by hand.
20+
- `tri fpga measured-to-lean --pvt-context` generates a `decide` theorem for the exact rounded point, but it does **not** automatically reference the W433 quantified theorem `xadc_envelope_justifies_cclk_variant_raw_ns_pvt`. The formal bridge exists in the library but is not wired into the generator.
21+
22+
### Strategic / competitive
23+
- The 7 residual `gen-verilog` yosys smoke failures (#1245) are unchanged. A master-merge of the full fix set is still too risky for a wave whose primary goal is FPGA boot-evidence formalization.
24+
- Competitor `Sparkle / Verilean` remains the closest Lean-native threat; its PR #66 is still open, PR #65 (RV32 divider proof) demonstrates IP-level depth, and the July 2026 Functional Matsuri talk positions Lean 4 as an RTL core. Other signals: `firtool-1.152.0` published; `Clash 1.11.0` still a Hackage candidate; `Aria-HDL` retiming/PCIe BAR updates; `CktFormalizer` and ternary-compute projects (`TernaryCore`, `BitNet-RISCV-Multicore`) validate the ternary direction.
25+
26+
---
27+
28+
## 2. Competitor scan summary
29+
30+
| Competitor | Update for W434 | Implication for t27 |
31+
|---|---|---|
32+
| **Sparkle / Verilean** | PR #66 open, last public push 2026-07-03; PR #65 divider proof is a concrete IP-level correctness milestone; public talk July 11 2026. | Closest structural competitor; t27's differentiation is the sealed spec→bitstream loop + physical boot evidence. |
33+
| **Clash** | 1.11.0 still a Hackage candidate (no final release); 1.10 remains latest official. | Functional-HDL maturity but external proof; no physical evidence loop. |
34+
| **Chisel / FIRRTL / CIRCT** | `firtool-1.152.0` published July 2026; LTL/Verif dialects and ChiselTest formal compatibility layer advancing. | Industry adoption; formal reasoning still RTL/SVA/external, not source-level dependent types. |
35+
| **Aria-HDL** | Rust meta-compiler with `--emit-lean4` and `--emit-sby`; retiming + PCIe BAR test added. | Validates spec→proof→bitstream pipelines but no ternary focus or sealed hashes. |
36+
| **CktFormalizer** | arXiv 2605.07782; LLM-to-circuit autoformalization in Lean 4 with Yosys/OpenROAD flow. | Another signal that Lean 4 as HDL proof backend is crowded. |
37+
| **TernaryCore / BitNet-RISCV-Multicore** | Ternary inference and multicore RISC-V ternary PEs simulating; no formal proofs yet. | Confirms ternary compute hardware is visible; t27 must keep formal ternary IP ahead. |
38+
39+
---
40+
41+
## 3. Variant selection
42+
43+
**Selected: Variant B** — board is reachable over JTAG, live XADC readout works, but P12 / relay are still blocked, so real CCLK capture is not possible. Use the live XADC operating point as the PVT context and a synthetic CCLK fixture for proof-of-pipeline.
44+
45+
---
46+
47+
## 4. Decomposed tasks
48+
49+
### Task 1 — Live XADC operating point → PVT context (tooling)
50+
- [x] Probe: `openFPGALoader --detect -c digilent_hs2` succeeds.
51+
- [x] Capture: `tri fpga read-xadc` returns valid JSON.
52+
- [x] Convert manually to integer `PvtContext` JSON: `{ "temp_c": 41, "vccint_mv": 1000, "vccaux_mv": 1807, "process_corner": "ss" }`.
53+
- [x] Validate: `tri fpga pvt-envelope --pvt-context ... --json` reports in-envelope with `margin_ns = 5`, `min_sck_half_ns = 11`.
54+
- [ ] Optionally expose `tri fpga read-xadc --to-pvt-context <file>` or `--process-corner <corner>` in CLI (deferred to W435 if scope grows).
55+
56+
### Task 2 — Generate proof artifact from live XADC context
57+
- [x] Create synthetic raw-ns CCLK fixture: `period_ns=40, sck_low_ns=20, sck_high_ns=20` (OSCFSEL=6 nominal 25 MHz, 50% duty).
58+
- [x] Run `tri fpga measured-to-lean --raw-ns --file <fixture> --pvt-context <xadc> --validate --standalone --name xadc_live_w434 --out <file> --json`.
59+
- [ ] Add a hand-written theorem in `proofs/lean4/Trinity/TernaryFPGABoot.lean` that applies the W433 quantified theorem `xadc_envelope_justifies_cclk_variant_raw_ns_pvt` to the live XADC point and OSCFSEL=6, closing the formal loop.
60+
61+
### Task 3 — Rust test coverage for live XADC → PVT conversion
62+
- [ ] Add a unit test in `cli/tri/src/fpga.rs` asserting `XadcContext::to_pvt_context` rounds the captured live values (41.4422 °C → 41, 1.00049 V → 1000 mV, 1.80688 V → 1807 mV) correctly.
63+
64+
### Task 4 — Competitor and defect refresh
65+
- [ ] Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md` date/header and W434 note.
66+
- [ ] Update `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` with W434 triage entry: 7 residual failures remain; master-merge deferred; no new narrow defect.
67+
68+
### Task 5 — Documentation
69+
- [ ] Update `fpga/HARDWARE_SSOT.md` §3.6 with the W434 live XADC validation recipe and the synthetic-CCLK proof-of-pipeline note.
70+
71+
### Task 6 — Close-out artifacts
72+
- [ ] Write `docs/reports/WAVE_LOOP_434_REPORT.md`.
73+
- [ ] Write `docs/reports/FPGA_LOOP_EVIDENCE_W434_2026-07-01.md`.
74+
- [ ] Write `docs/reports/FPGA_LOOP_COOPERATION_W435_2026-07-01.md` with three variants for W435.
75+
- [ ] Update `docs/NOW.md` and `.trinity/current-issue.md` for W435.
76+
- [ ] Create GitHub issue #1397 and branch `wave-loop-435`.
77+
78+
### Task 7 — Verification
79+
- [ ] `lake build Trinity.TernaryFPGABoot` passes.
80+
- [ ] `cargo test -p tri --bin tri fpga::` passes.
81+
- [ ] `./scripts/tri test` passes with the documented 7 pre-existing gen-verilog yosys smoke failures.
82+
83+
---
84+
85+
## 5. Definition of done
86+
87+
- [ ] Variant B acceptance criteria met: live XADC validated in PVT envelope; at least one `measured-to-lean` theorem generated from the live XADC context; W433 quantified theorem referenced in the formal library for the live point.
88+
- [ ] New unit test for live XADC → PVT context rounding passes.
89+
- [ ] Competitor snapshot and gen-verilog baseline updated.
90+
- [ ] `lake build Trinity.TernaryFPGABoot` passes.
91+
- [ ] `cargo test -p tri --bin tri fpga::` passes.
92+
- [ ] `./scripts/tri test` passes with documented 7 residual failures.
93+
- [ ] Close-out report and W435 cooperation variants written.
94+
- [ ] Issue/branch for W435 created.
95+
96+
---
97+
98+
*φ² + φ⁻² = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 30 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,22 @@
1-
# Wave Loop 434 — FPGA boot-evidence next variant (real capture, live XADC validation, or master-merge retry)
1+
# Wave Loop 435 — FPGA boot-evidence next variant (real capture, live XADC pipeline hardening, or master-merge retry)
22

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

77
---
88

99
## Goal
1010

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`.
11+
Wave Loop 434 validated the live XADC → PVT context pipeline on a real FPGA
12+
readout (temp≈41 °C, VCCINT≈1.00 V, VCCAUX≈1.81 V), generated a
13+
`measured-to-lean` theorem from the live context using a synthetic CCLK fixture,
14+
and added `xadc_live_w434_justifies_cclk_variant_raw_ns_pvt` in
15+
`proofs/lean4/Trinity/TernaryFPGABoot.lean`. The bench remains blocked (P12
16+
unwired, no relay gate, no DLC10 cable) and the master-merge path for the
17+
`gen-verilog` fix set (`701d79b3b`) is still not safely reachable. Wave Loop 435
18+
executes the first available variant from
19+
`docs/reports/FPGA_LOOP_COOPERATION_W435_2026-07-01.md`.
1820

1921
1. **Variant A (preferred when bench becomes fully available):**
2022
- Confirm P12 is wired to a logic-analyzer channel and a relay/remote-power
@@ -25,28 +27,29 @@ from `docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md`.
2527
- Import with `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone
2628
--validate --pvt-context <xadc.json> --out <theorem.lean> --json` and commit
2729
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.
30+
- Reference `xadc_live_w434_justifies_cclk_variant_raw_ns_pvt` or the generic
31+
W433 theorem in the generated proof.
3032
- Update `fpga/HARDWARE_SSOT.md` §3.6 with measured frequency/duty/margin.
3133

32-
2. **Variant B (if board is reachable but P12 / relay are still blocked):**
33-
- Capture a real `tri fpga read-xadc --json` from the live board.
34-
- Verify the JSON converts to a valid `PvtContext` via `tri fpga pvt-envelope`.
35-
- Generate at least one `measured-to-lean` theorem using the real XADC context
36-
(synthetic CCLK fixture is acceptable for proof-of-pipeline).
37-
- Reference the W433 quantified theorem in the generated proof.
38-
- Alternatively, run `tri fpga cclk-sweep` over OSCFSEL 0..5 with `--xadc` and
39-
manual power cycles.
34+
2. **Variant B (default if board reachable but P12/relay still blocked):**
35+
- Harden `tri fpga read-xadc` to export a rounded `PvtContext` JSON directly
36+
(e.g. `--to-pvt-context <file>` or `--process-corner <corner>`).
37+
- Add unit/integration tests for the full
38+
`read-xadc → pvt-envelope → measured-to-lean` pipeline.
39+
- Extend `measured-to-lean --json` summary with the source operating point
40+
(`temp_c`, `vccint_mv`, `vccaux_mv`, `process_corner`).
41+
- Generate `measured-to-lean` theorems for OSCFSEL 0..7 using the live XADC
42+
context and synthetic CCLK fixtures, producing a coverage matrix.
4043
- Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md` and re-evaluate
4144
`docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`.
4245

43-
3. **Variant C (fallback if bench still blocked):**
46+
3. **Variant C (fallback if bench still blocked and Variant B is too small):**
4447
- Re-attempt the `master` merge/rebase wave from a fresh topic branch to bring
4548
the `gen-verilog` fix set (`701d79b3b`) into the wave-loop line and clear the
4649
7 residual yosys smoke failures (#1245).
4750
- If the merge is still too risky, land another formal/tooling sub-task:
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.
51+
add a computable combined OSCFSEL+XADC envelope check, or refresh the
52+
competitor report.
5053
- Update `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` with the new baseline.
5154

5255
---
@@ -56,11 +59,11 @@ from `docs/reports/FPGA_LOOP_COOPERATION_W434_2026-07-01.md`.
5659
- [ ] The chosen variant is executed and its acceptance criteria are met.
5760
- [ ] `lake build Trinity.TernaryFPGABoot` passes.
5861
- [ ] `./scripts/tri test` passes with the new documented baseline (ideally 0 new
59-
gen-verilog failures; if Variant C succeeds, the 7 #1245 failures are
62+
gen-verilog failures; if Variant C1 succeeds, the 7 #1245 failures are
6063
cleared).
61-
- [ ] `cargo test --bin tri fpga::` passes.
64+
- [ ] `cargo test -p tri --bin tri fpga::` passes.
6265
- [ ] Close-out report and next-wave cooperation variants are written.
63-
- [ ] Issue/branch for Wave Loop 435 are created.
66+
- [ ] Issue/branch for Wave Loop 436 are created.
6467

6568
---
6669

‎.trinity/current_task/.commit_count‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
1817
1+
1821

‎.trinity/current_task/activity.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1612,3 +1612,7 @@
16121612
- **Commit:** feat(igla): Wave Loop 433 — formal bridge fallback, compose W431 XADC envelope with W432 per-corner raw-ns OSCFSEL theorem
16131613
- **Files:** .claude/plans/wave-loop-429.md,.claude/plans/wave-loop-430.md,.claude/plans/wave-loop-431.md,.trinity/experience.md
16141614

1615+
## 2026-07-05T12:23:26Z — wave-loop-434
1616+
- **Commit:** docs(experience): W433 learnings and missing W429-W431 plan files
1617+
- **Files:** .claude/plans/wave-loop-434.md,.trinity/current-issue.md,.trinity/current_task/.commit_count,.trinity/current_task/session_log.jsonl,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W435_2026-07-01.md,docs/reports/FPGA_LOOP_EVIDENCE_W434_2026-07-01.md,docs/reports/GEN_VERILOG_DEFECTS_REPRO.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_434_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
1618+

‎.trinity/current_task/session_log.jsonl‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -291,3 +291,7 @@
291291
{"ts":"2026-07-05T06:47:22Z","branch":"wave-loop-423","msg":"docs(issue): set current issue to Wave Loop 423","files":".trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W424_2026-07-05.md,docs/reports/FPGA_LOOP_EVIDENCE_W423_2026-07-05.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_423_REPORT.md,fpga/HARDWARE_SSOT.md","notebook":"b83263109fb055dc"}
292292
{"ts":"2026-07-05T06:48:03Z","branch":"wave-loop-424","msg":"feat(igla): Wave Loop 423 — CSV time units, VCD slope filter, PVT worst-case, competitor refresh (Closes #1368)","files":".trinity/current-issue.md,docs/reports/FPGA_LOOP_COOPERATION_W424_2026-07-05.md","notebook":"b83263109fb055dc"}
293293
{"ts":"2026-07-05T07:13:01Z","branch":"wave-loop-424","msg":"setup(igla): Wave Loop 424 branch and issue (#1371)","files":".trinity/current-issue.md,.trinity/current_task/.commit_count,.trinity/current_task/session_log.jsonl,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W425_2026-07-05.md,docs/reports/FPGA_LOOP_EVIDENCE_W424_2026-07-05.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_424_REPORT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean","notebook":"b83263109fb055dc"}
294+
{"ts":"2026-07-05T11:58:14Z","branch":"wave-loop-432","msg":"chore(merge): bring origin/master (gf128 promotion) into wave-loop-432","files":".claude/plans/wave-loop-432.md,.trinity/current-issue.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W433_2026-07-01.md,docs/reports/FPGA_LOOP_EVIDENCE_W432_2026-07-01.md,docs/reports/GEN_VERILOG_DEFECTS_REPRO.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_432_REPORT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean","notebook":"b83263109fb055dc"}
295+
{"ts":"2026-07-05T11:59:08Z","branch":"wave-loop-433","msg":"feat(igla): Wave Loop 432 — per-process-corner raw-ns OSCFSEL theorems, master-merge feasibility probe, W432 close-out artifacts","files":".trinity/experience.md","notebook":"b83263109fb055dc"}
296+
{"ts":"2026-07-05T12:07:23Z","branch":"wave-loop-433","msg":"docs(experience): W432 learnings — per-process-corner theorem, master-merge probe, blocked bench redirect","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","notebook":"b83263109fb055dc"}
297+
{"ts":"2026-07-05T12:08:33Z","branch":"wave-loop-433","msg":"feat(igla): Wave Loop 433 — formal bridge fallback, compose W431 XADC envelope with W432 per-corner raw-ns OSCFSEL theorem","files":".claude/plans/wave-loop-429.md,.claude/plans/wave-loop-430.md,.claude/plans/wave-loop-431.md,.trinity/experience.md","notebook":"b83263109fb055dc"}

0 commit comments

Comments
 (0)