Skip to content

Commit 2d31a6e

Browse files
Dmitrii Vasilevclaude
Dmitrii Vasilev
and
claude
committed
feat(igla): Wave Loop 435 — live XADC → PVT context CLI export, OSCFSEL 0..7 synthetic theorem matrix, end-to-end integration test
Closes #1398 - tri fpga read-xadc gains --process-corner and --to-pvt-context - measured-to-lean --json includes operating_point provenance - new Rust integration test exercises XADC → PVT → theorem pipeline - TernaryFPGABoot.lean adds cclk_variant_and_xadc_envelope_check and OSCFSEL 0..7 matrix under W434 live point - docs/NOW.md, HARDWARE_SSOT.md, competitor and defect reports refreshed - W435 close-out artifacts and W436 cooperation variants Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent a46805e commit 2d31a6e

12 files changed

Lines changed: 955 additions & 53 deletions

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

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
# Wave Loop 435 — Decomposed Plan
2+
3+
**Issue:** #1398
4+
**Branch:** `wave-loop-435`
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** to a logic-analyzer channel, 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 the 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 (`XadcContext::to_pvt_context`) is implemented internally but **not exposed as a standalone CLI export**, so the user must round the values by hand or call the helper from Rust tests.
20+
- `tri fpga measured-to-lean --json` summary does not yet include the **source operating point** (`temp_c`, `vccint_mv`, `vccaux_mv`, `process_corner`) even though the PVT context is used to generate the theorem. Downstream dashboards cannot correlate the theorem with the live silicon state without parsing the generated Lean snippet.
21+
- No end-to-end integration test exercises `read-xadc → pvt-envelope → measured-to-lean` as a single pipeline. The W434 path was validated manually; W435 should lock it with a regression test.
22+
23+
### Strategic / competitive
24+
- 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.
25+
- Competitor signals since W434:
26+
- **Sparkle / Verilean** remains the closest Lean-native threat. PR #66 is still open; PR #65 (RV32 divider proof) demonstrates IP-level depth; July 2026 Functional Matsuri talk positions Lean 4 as an RTL core.
27+
- **CIRCT / firtool 1.152.0** published July 2026; LTL/Verif dialects and ChiselTest formal compatibility layer keep advancing.
28+
- **Clash 1.11.0** is still a Hackage candidate; **Clash 1.10** (April 2026) remains the latest official release.
29+
- **Aria-HDL** Rust meta-compiler with `--emit-lean4` and `--emit-sby`; retiming + PCIe BAR test added.
30+
- **CktFormalizer** (arXiv 2605.07782) and ternary-compute projects (**TernaryCore**, **BitNet-RISCV-Multicore**) validate the ternary direction.
31+
- **Takahe** multi-radix synthesis supports `--radix 3` balanced ternary with `--equiv` formal equivalence checking, a new signal in the ternary hardware space.
32+
- **ternlang-hdl** Rust crate and **KULeuven-MICAS/ternary-lut-dse** (Chisel, ISPASS 2026) add more ternary-accelerator activity.
33+
34+
---
35+
36+
## 2. Competitor scan summary
37+
38+
| Competitor | Update for W435 | Implication for t27 |
39+
|---|---|---|
40+
| **Sparkle / Verilean** | PR #66 open, PR #65 divider proof closed; public talk July 11 2026; IP catalog growing. | Closest structural competitor; t27's differentiation is the sealed spec→bitstream loop + physical boot evidence. |
41+
| **Clash** | 1.11.0 still a Hackage candidate (no final release); 1.10 remains latest official. Issue #3153 on verification operator translation still open. | Functional-HDL maturity but external proof; no physical evidence loop. |
42+
| **Chisel / FIRRTL / CIRCT** | `firtool-1.152.0` published July 2026; LTL/Verif dialects and ChiselTest formal compatibility layer advancing; `circt-bmc` / `circt-lec` maturing. | Industry adoption; formal reasoning still RTL/SVA/external, not source-level dependent types. |
43+
| **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. |
44+
| **CktFormalizer** | arXiv 2605.07782; LLM-to-circuit autoformalization in Lean 4 with Yosys/OpenROAD flow. Claims 95–100% backend success and closed-loop PPA optimization. | Another signal that **Lean 4 as HDL proof backend** is crowded. |
45+
| **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. |
46+
| **Takahe** | `--radix 3` balanced ternary synthesis with `--equiv` formal equivalence (≤24 inputs exhaustive). | New ternary formal-hardware signal; watch for scaling claims. |
47+
| **ternlang-hdl / KULeuven ternary-lut-dse** | Rust ternary Verilog/VHDL lowering and Chisel ternary matmul accelerator accepted at ISPASS 2026. | More evidence that ternary hardware tooling is gaining momentum. |
48+
49+
---
50+
51+
## 3. Variant selection
52+
53+
**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. This wave hardens the live XADC → PVT context → `measured-to-lean` pipeline and extends the formal library with a synthetic CCLK coverage matrix for OSCFSEL 0..7 under the live operating point.
54+
55+
If P12 or the relay gate becomes available during the wave, switch to **Variant A** immediately.
56+
57+
---
58+
59+
## 4. Decomposed tasks
60+
61+
### Task 1 — Expose `XadcContext → PvtContext` export from `tri fpga read-xadc`
62+
- [ ] Add `--process-corner <corner>` to `tri fpga read-xadc` (default `ss`).
63+
- [ ] Add `--to-pvt-context <file>` to write the rounded `PvtContext` JSON directly.
64+
- [ ] Keep the existing full XADC JSON output on stdout; the new flags are additive.
65+
- [ ] Validate the emitted JSON parses as `PvtContext`.
66+
67+
### Task 2 — Extend `measured-to-lean --json` summary with source operating point
68+
- [ ] Add `operating_point` field to the summary when a PVT context is present:
69+
```json
70+
{
71+
"operating_point": {
72+
"source": "pvt_context_file" | "xadc",
73+
"temp_c": 41,
74+
"vccint_mv": 1000,
75+
"vccaux_mv": 1807,
76+
"process_corner": "ss"
77+
}
78+
}
79+
```
80+
- [ ] For `--pvt-worstcase`, source is `"worstcase"`; for `--pvt-context <file>`, source is `"pvt_context_file"`.
81+
- [ ] Update `build_measured_to_lean_summary` signature and unit tests.
82+
83+
### Task 3 — Integration test for end-to-end live XADC → theorem pipeline
84+
- [ ] Add a test that:
85+
1. Constructs an `XadcContext` matching the W434 live capture.
86+
2. Rounds it to `PvtContext` via `to_pvt_context(ProcessCorner::Ss)`.
87+
3. Writes the PVT context to a temp JSON file.
88+
4. Creates a synthetic raw-ns CCLK fixture (40/20/20 ns).
89+
5. Calls `measured_to_lean(..., raw_ns=true, pvt_context=<file>, validate=true, standalone=true, json=true)`.
90+
6. Asserts the summary `recommendation` is `"in_spec"`, `margin_ns >= 0`, and the generated Lean snippet builds in a standalone `lake` package.
91+
- [ ] Use a temp directory and clean up afterwards.
92+
93+
### Task 4 — Generate synthetic OSCFSEL 0..7 theorem matrix from live XADC context
94+
- [ ] In `proofs/lean4/Trinity/TernaryFPGABoot.lean`, add:
95+
- `XADC_LIVE_W434_OPERATING_POINT` (reuse from W434).
96+
- `xadc_live_w434_all_oscfsel_raw_ns_pvt_satisfies_flash_spec` — quantified theorem over OSCFSEL 0..7 using `xadc_live_w434_justifies_cclk_variant_raw_ns_pvt`.
97+
- Per-OSCFSEL concrete theorems `xadc_live_w434_oscfsel_0_raw_ns_pvt_satisfies_flash_spec` ... `xadc_live_w434_oscfsel_7_raw_ns_pvt_satisfies_flash_spec`.
98+
- Matching transaction theorems `xadc_live_w434_oscfsel_N_transaction_ok`.
99+
- [ ] These are `decide`-cheap because they reuse the quantified bridge.
100+
101+
### Task 5 — Add computable combined OSCFSEL + XADC envelope check
102+
- [ ] Add `cclk_variant_and_xadc_envelope_check (oscfsel : Nat) (pt : XadcOperatingPoint) : Bool`.
103+
- [ ] Prove equivalence with `oscfsel ≤ 7 ∧ xadc_operating_point_within_envelope pt`.
104+
- [ ] Add a theorem linking the combined check to `measured_cclk_from_raw_ns_with_pvt_satisfies_flash_spec` for any in-envelope point and documented OSCFSEL.
105+
106+
### Task 6 — Documentation and baseline refresh
107+
- [ ] Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md` date/header and W435 note.
108+
- [ ] Update `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` with W435 triage entry: 7 residual failures remain; master-merge deferred; no new narrow defect.
109+
- [ ] Extend `fpga/HARDWARE_SSOT.md` §9.6.2 with the `tri fpga read-xadc --to-pvt-context` recipe and the OSCFSEL 0..7 synthetic theorem matrix.
110+
111+
### Task 7 — Close-out artifacts
112+
- [ ] Write `docs/reports/WAVE_LOOP_435_REPORT.md`.
113+
- [ ] Write `docs/reports/FPGA_LOOP_EVIDENCE_W435_2026-07-01.md`.
114+
- [ ] Write `docs/reports/FPGA_LOOP_COOPERATION_W436_2026-07-01.md` with three variants for W436.
115+
- [ ] Update `docs/NOW.md` and `.trinity/current-issue.md` for W436.
116+
- [ ] Create GitHub issue #1401 and branch `wave-loop-436`.
117+
118+
### Task 8 — Verification
119+
- [ ] `lake build Trinity.TernaryFPGABoot` passes.
120+
- [ ] `cargo test -p tri --bin tri fpga::` passes.
121+
- [ ] `./scripts/tri test` passes with the documented 7 pre-existing gen-verilog yosys smoke failures.
122+
123+
---
124+
125+
## 5. Definition of done
126+
127+
- [ ] `tri fpga read-xadc` can emit a valid `--pvt-context` JSON directly.
128+
- [ ] `measured-to-lean --json` summary includes the source operating point.
129+
- [ ] At least one new integration test exercises the end-to-end live XADC → theorem pipeline.
130+
- [ ] `TernaryFPGABoot.lean` contains the OSCFSEL 0..7 synthetic theorem matrix under the live W434 XADC point and the combined computable envelope check.
131+
- [ ] `lake build Trinity.TernaryFPGABoot` passes.
132+
- [ ] `cargo test -p tri --bin tri fpga::` passes.
133+
- [ ] `./scripts/tri test` passes with documented 7 residual failures.
134+
- [ ] Competitor snapshot and gen-verilog baseline updated.
135+
- [ ] Close-out report and W436 cooperation variants written.
136+
- [ ] Issue/branch for W436 created.
137+
138+
---
139+
140+
*φ² + φ⁻² = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 23 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,45 +1,39 @@
1-
# Wave Loop 435 — FPGA boot-evidence next variant (real capture, live XADC pipeline hardening, or master-merge retry)
1+
# Wave Loop 436 — FPGA boot-evidence next variant (real capture, live XADC pipeline extension, or master-merge retry)
22

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

77
---
88

99
## Goal
1010

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`.
11+
Wave Loop 435 hardened the live XADC → PVT context pipeline, added an end-to-end integration test, extended the `measured-to-lean --json` summary with source operating points, and generated a synthetic OSCFSEL 0..7 theorem matrix under the real W434 silicon operating point in `proofs/lean4/Trinity/TernaryFPGABoot.lean`. The bench remains blocked (P12 unwired, no relay gate, no DLC10 cable) and the master-merge path for the `gen-verilog` fix set (`701d79b3b`) is still not safely reachable. Wave Loop 436 executes the first available variant from `docs/reports/FPGA_LOOP_COOPERATION_W436_2026-07-01.md`.
2012

2113
1. **Variant A (preferred when bench becomes fully available):**
22-
- Confirm P12 is wired to a logic-analyzer channel and a relay/remote-power
23-
gate is available.
14+
- Confirm P12 is wired to a logic-analyzer channel and a relay/remote-power gate is available.
2415
- Program SPI flash with OSCFSEL=6 (and OSCFSEL=7 if time permits).
2516
- Capture real CCLK during cold-POR boot.
26-
- Run `tri fpga cclk-sweep ... --xadc` so boot logs record live operating points.
17+
- Run `tri fpga cclk-sweep ... --xadc --to-pvt-context` so boot logs record live operating points.
2718
- Import with `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone
28-
--validate --pvt-context <xadc.json> --out <theorem.lean> --json` and commit
19+
--validate --pvt-context <xadc_pvt.json> --out <theorem.lean> --json` and commit
2920
generated Lean theorems plus JSON summaries.
30-
- Reference `xadc_live_w434_justifies_cclk_variant_raw_ns_pvt` or the generic
31-
W433 theorem in the generated proof.
21+
- Reference `xadc_live_w434_justifies_cclk_variant_raw_ns_pvt` or the W435
22+
`cclk_variant_and_xadc_envelope_check` gate in the generated proof.
3223
- Update `fpga/HARDWARE_SSOT.md` §3.6 with measured frequency/duty/margin.
3324

3425
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.
26+
- Extend `tri fpga cold-por` / `tri fpga cclk-sweep` to support `--to-pvt-context` so
27+
every boot log JSON contains the rounded PVT context recorded at boot time.
28+
- Add `operating_point` to the sweep/boot log JSON schema, mirroring the
29+
`measured-to-lean --json` summary.
30+
- Add a `tri fpga sweep-report --pvt-context` path producing a machine-readable
31+
JSON report correlating OSCFSEL variant, live XADC point, PVT margin, and
32+
recommendation.
33+
- Teach `measured-to-lean` to accept an `operating_point` source label `"xadc"`
34+
when the PVT context is derived from a live `read-xadc` export.
35+
- Add a Lean example theorem evaluating `cclk_variant_and_xadc_envelope_check`
36+
over OSCFSEL 0..7 at the W434 live point.
4337
- Refresh `docs/reports/T27_VS_FORMAL_HDL_2026.md` and re-evaluate
4438
`docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`.
4539

@@ -48,7 +42,7 @@ executes the first available variant from
4842
the `gen-verilog` fix set (`701d79b3b`) into the wave-loop line and clear the
4943
7 residual yosys smoke failures (#1245).
5044
- If the merge is still too risky, land another formal/tooling sub-task:
51-
add a computable combined OSCFSEL+XADC envelope check, or refresh the
45+
extend PVT bounds to additional process corners/flash parts, or refresh the
5246
competitor report.
5347
- Update `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` with the new baseline.
5448

@@ -63,7 +57,7 @@ executes the first available variant from
6357
cleared).
6458
- [ ] `cargo test -p tri --bin tri fpga::` passes.
6559
- [ ] Close-out report and next-wave cooperation variants are written.
66-
- [ ] Issue/branch for Wave Loop 436 are created.
60+
- [ ] Issue/branch for Wave Loop 437 are created.
6761

6862
---
6963

‎.trinity/current_task/activity.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1620,3 +1620,7 @@
16201620
- **Commit:** feat(igla): Wave Loop 434 — live XADC → PVT context theorem, synthetic CCLK proof-of-pipeline, W435 issue #1398 + branch
16211621
- **Files:** .trinity/current_task/.commit_count,.trinity/current_task/session_log.jsonl
16221622

1623+
## 2026-07-05T12:45:09Z — wave-loop-435
1624+
- **Commit:** chore(trinity): update current_task counters after W434 verification run
1625+
- **Files:** .claude/plans/wave-loop-435.md,.trinity/current-issue.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W436_2026-07-01.md,docs/reports/FPGA_LOOP_EVIDENCE_W435_2026-07-01.md,docs/reports/GEN_VERILOG_DEFECTS_REPRO.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_435_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
1626+

0 commit comments

Comments
 (0)