Skip to content

Commit 56959d3

Browse files
gHashTagDmitrii Vasilevclaude
authored
feat(igla): Wave Loop 418 — PVT regression, VCD/CSV hardening, standalone Lean integration (#1356)
* docs(NOW): W418 setup, mark W417 PR #1354 merged Closes #1353 - Add W418 in-progress section at the top of docs/NOW.md. - Update W417 section to show PR #1354 merged and issue #1353 created. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * feat(igla): Wave Loop 418 — PVT lower-bound regression, VCD header skip, analog CSV voltage detection, standalone Lean integration - Add Rust regression test guarding n25q128_min_sck_half_ns_pvt >= 6 ns across the operating rectangle. - Add matching Lean 4 lemma pvt_half_ns_at_least_nominal and n25q128_min_sck_half_ns_pvt. - Harden VCD parser for multi-line $date/$version/$comment headers. - Auto-detect analog CSV voltage column by header name (voltage/v/analog). - Add standalone lake-package integration test for measured-to-lean --standalone. - Update fpga/HARDWARE_SSOT.md with first-real-capture checklist and PVT coefficient replacement recipe. - Produce W418 report, evidence, and W419 cooperation variants. Closes #1353 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Dmitrii Vasilev <admin@t27.ai> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent f0e27a2 commit 56959d3

11 files changed

Lines changed: 1033 additions & 30 deletions

File tree

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

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,152 @@
1+
# Wave Loop 418 Plan
2+
3+
**Issue:** #1353
4+
**Branch:** `wave-loop-418`
5+
6+
---
7+
8+
## Decision gate
9+
10+
| Bench available? | Pick |
11+
|--------------------|------|
12+
| P12 + analyzer + DLC10/Digilent cable | Variant A |
13+
| Relay / power switch + cable | Variant B |
14+
| Nothing | Variant C |
15+
16+
Current state (2026-07-04): **nothing** — P12 unwired, DLC10 cable missing, no
17+
USB relay detected. The W417 hygiene wave did not change the bench. Default to
18+
**Variant C** for W418.
19+
20+
---
21+
22+
## Goals
23+
24+
1. If the bench becomes available, capture real CCLK for `OSCFSEL=6/7` and
25+
commit instrument-to-Lean theorems (Variant A).
26+
2. If relay hardware becomes available, automate cold-POR power-cycling and
27+
capture real STAT (Variant B).
28+
3. Otherwise, keep hardening the formal model and the instrument-import path:
29+
add a PVT-envelope lower-bound regression test, extend VCD parser coverage for
30+
`$date`/`$version`/`$comment` headers and analog CSV voltage columns, build a
31+
standalone Lean integration test from a synthetic CSV, and document the
32+
first-real-capture checklist (Variant C).
33+
34+
---
35+
36+
## Work breakdown
37+
38+
### Variant A — Physical CCLK capture
39+
40+
Files: `fpga/HARDWARE_SSOT.md`, `proofs/lean4/Trinity/TernaryFPGABoot.lean`, `docs/reports/*`
41+
42+
- Wire P12 to the logic analyzer.
43+
- Generate `OSCFSEL=6` and `OSCFSEL=7` variants with `tri fpga cclk-variants`.
44+
- Program each variant to flash, cold-POR boot, and capture CCLK.
45+
- Import captures with `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone --validate --pvt-context`.
46+
- Commit generated theorems and update `fpga/HARDWARE_SSOT.md`.
47+
48+
### Variant B — Real relay-controlled cold-POR
49+
50+
Files: `cli/tri/src/fpga.rs`, `fpga/HARDWARE_SSOT.md`
51+
52+
- Select a relay interface (USB-serial relay module, smart power strip, or MCU GPIO bridge).
53+
- Implement a `RelayControl` trait with `power_cycle(delay_ms: u64)`.
54+
- Extend `FpgaCmd::ColdPor` to accept real `--relay-port` values.
55+
- Capture STAT after relay power-cycle and write a non-mock log.
56+
- Document wiring and safety rules.
57+
58+
### Variant C — Further formal tooling (default fallback)
59+
60+
Files: `cli/tri/src/fpga.rs`, `proofs/lean4/Trinity/TernaryFPGABoot.lean`, `fpga/HARDWARE_SSOT.md`, `docs/reports/*`
61+
62+
1. **PVT-envelope regression test**
63+
- Add a Rust unit test that exhaustively samples the operating rectangle
64+
(temp, vccint, corner) and asserts
65+
`n25q128_min_sck_half_ns_pvt ≥ NOMINAL_HALF_NS`.
66+
- Add a Lean 4 lemma `n25q128_min_sck_half_ns_pvt_nonneg` proving the same
67+
bound symbolically.
68+
- Document in `fpga/HARDWARE_SSOT.md` how to replace the linear coefficients
69+
once real N25Q128_3V PVT curves are available.
70+
71+
2. **Instrument import coverage**
72+
- VCD parser: skip `$date`, `$version`, `$comment` multi-line header sections
73+
without confusing them with `$var` declarations.
74+
- CSV parser: support analog CSV exports that contain a voltage column
75+
directly, so `--vcd-threshold-v` is not the only analog path.
76+
- Add unit tests for both.
77+
78+
3. **Standalone Lean integration test**
79+
- Extend `measured-to-lean --standalone` output so the generated file is a
80+
complete, lake-buildable package snippet (imports + theorem + main proof).
81+
- Add a Rust integration test that writes a synthetic CSV, runs
82+
`tri fpga measured-to-lean --csv --raw-ns --standalone --pvt-context`, and
83+
type-checks the result in a temporary `lake` package.
84+
85+
4. **First-real-capture checklist**
86+
- Update `fpga/HARDWARE_SSOT.md` with a step-by-step checklist for the first
87+
real CCLK capture (wiring, samplerate, PVT context, validation,
88+
theorem generation).
89+
90+
---
91+
92+
## Weak points
93+
94+
1. **Physical evidence gap remains** under Variant C. The formal pipeline keeps
95+
improving, but no silicon evidence is produced until P12 is wired and the
96+
cable/relay hardware is available.
97+
2. **PVT envelope coefficients are still informed estimates**, not Micron
98+
datasheet curves. The regression test only guards the lower bound; real
99+
characterization may require larger margins.
100+
3. **VCD header sections** vary across tools (some emit `$date` on one line,
101+
others across multiple lines). Header handling will be best-effort for the
102+
most common variants.
103+
4. **Analog CSV voltage columns** have no standard format; the parser will
104+
support the Saleae/DSView single-channel layout and document the expected
105+
column names.
106+
5. **Standalone Lean integration test** depends on `lake` being available in
107+
the test environment. CI must have Lean 4 installed.
108+
109+
---
110+
111+
## Competitor scan
112+
113+
- **Sparkle HDL / Verilean:** formal Verilog-to-Lean/Coq verification; no public
114+
instrument-to-Lean bridge or PVT-aware timing envelope for flash boot.
115+
- **SymbiYosys / Yosys formal:** bounded property checking on RTL; no link to
116+
logic-analyzer measurements.
117+
- **Koika / Kami:** processor-model verification in Coq; unrelated to 7-series
118+
boot timing.
119+
- **OpenFPGALoader / prjxray:** bitstream/JTAG tooling; no formal proof pipeline.
120+
- **TinyTapeout / Efabless:** silicon-shuttle flow; relies on PDK
121+
characterization, not user-captured proofs.
122+
- **OpenSTA / vyges-sta-si:** gate-level STA with PVT/OCV derating, but no
123+
instrument capture and no theorem-prover output.
124+
- **t27 differentiation:** still the only open pipeline converting instrument
125+
exports (CSV/VCD) into Lean 4 proofs of flash timing compliance, now with an
126+
explicit, falsifiable PVT uncertainty envelope, envelope monotonicity proofs,
127+
per-OSCFSEL transaction theorems, and an integration-test path.
128+
129+
---
130+
131+
## Verification checklist
132+
133+
- [ ] `cargo test -p tri fpga::tests` passes (new + existing tests).
134+
- [ ] `lake build Trinity.TernaryFPGABoot` passes from `proofs/lean4/`.
135+
- [ ] `./scripts/tri test` passes parse/typecheck/gen/seal-verify.
136+
- [ ] For Variant A: at least one generated `.lean` file builds standalone.
137+
- [ ] For Variant B: real relay port produces a non-mock boot log.
138+
- [x] For Variant C: PVT-envelope regression test, VCD header/analog CSV tests,
139+
and standalone Lean integration test land.
140+
141+
---
142+
143+
## Acceptance criteria
144+
145+
- The chosen variant is fully implemented and verified.
146+
- All invariant checks pass.
147+
- Report + evidence + W419 cooperation variants are produced.
148+
- PR closes #1353.
149+
150+
---
151+
152+
*φ² + φ⁻² = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 64 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,85 @@
1-
# Wave Loop 417 — hygiene, reland W415/W416, and next-variant gate
1+
# Wave Loop 418 — FPGA physical capture, real relay gate, or further formal tooling
22

3-
**Issue:** #1350
4-
**Branch:** `wave-loop-417`
5-
**Milestone:** Close out the W415/W416 reland mess and set up the next FPGA boot-evidence wave.
3+
**Issue:** #1353
4+
**Branch:** `wave-loop-418`
5+
**Milestone:** Continue the FPGA boot-evidence line from W417.
66

77
---
88

99
## Goal
1010

11-
Wave 415 and Wave 416 were stuck on a dirty PR (#1346) and a branch that had
12-
fallen behind `master`. Wave 417 lands the hygiene work: close/replace stale
13-
PRs, fix the branch target to `master` (Strategy P), repair the CI blocker
14-
introduced by the Russian cross-walk file, and produce the W417 report plus
15-
W418 cooperation variants.
11+
Wave 417 closed the W415/W416 hygiene loop. Wave 418 re-evaluates the bench
12+
state and executes the first available variant.
13+
14+
1. **Variant A (preferred when bench becomes available):**
15+
- Wire P12 to a logic-analyzer channel and capture real CCLK for
16+
`OSCFSEL=6` and `OSCFSEL=7`.
17+
- Import the captures with `tri fpga measured-to-lean --csv/--vcd --raw-ns
18+
--standalone --validate --pvt-context <ctx.json>` and commit the generated
19+
Lean theorems.
20+
- Document the measured frequencies/duty cycles and PVT context in
21+
`fpga/HARDWARE_SSOT.md`.
22+
23+
2. **Variant B (if relay hardware is available):**
24+
- Implement a real `--relay-port` backend for `tri fpga cold-por`
25+
(e.g. serial or TCP relay controlling board power).
26+
- Perform an automated cold-POR power-cycle and capture STAT without
27+
operator intervention.
28+
- Document relay wiring in `fpga/HARDWARE_SSOT.md`.
29+
30+
3. **Variant C (fallback if bench still blocked):**
31+
- Add a regression test that the PVT envelope stays ≥ the nominal bound
32+
across the full operating rectangle.
33+
- Extend instrument import for VCD `$date`/`$version`/`$comment` headers and
34+
analog CSV voltage columns.
35+
- Build a standalone Lean proof integration test from a synthetic CSV.
36+
- Document the first-real-capture checklist in `fpga/HARDWARE_SSOT.md`.
1637

1738
---
1839

1940
## Decomposed plan
2041

42+
See `docs/reports/FPGA_LOOP_COOPERATION_W418_2026-07-04.md`.
43+
2144
| Step | File(s) | Deliverable |
2245
|------|---------|-------------|
23-
| 1 | GitHub PRs/issues | Close superseded #1351; confirm stale wave-loop PRs/issues are closed |
24-
| 2 | `docs/BRANCHING_MODEL.md` | Document Strategy P: wave-loop PR target is `master` |
25-
| 3 | `docs/.legacy-non-english-docs` | Allowlist `conformance/vectors/CROSSWALK_sw_hw.md` until translated |
26-
| 4 | `docs/NOW.md` | Update W417 section to in-progress / close-out state |
27-
| 5 | `docs/reports/*` | `WAVE_LOOP_417_REPORT.md`, `FPGA_LOOP_EVIDENCE_W417_2026-07-04.md`, `FPGA_LOOP_COOPERATION_W418_2026-07-04.md` |
28-
| 6 | `.trinity/experience.md` | Capture W417 learnings |
29-
| 7 | git/PR | Open PR from `wave-loop-417` to `master`, close #1350, create #1353 for W418 |
46+
| 1 | `cli/tri/src/fpga.rs` | Variant A import, B relay backend, or C regression/integration tests |
47+
| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | PVT envelope regression lemma or new measured theorems |
48+
| 3 | `fpga/HARDWARE_SSOT.md` | Updated capture / relay / integration protocol |
49+
| 4 | `docs/reports/*` | W418 report, evidence, W419 cooperation |
50+
| 5 | `.trinity/experience.md` | W418 learnings |
51+
| 6 | git/PR | squash-merge to `master`, close #1353, open #? for W419 |
3052

3153
---
3254

3355
## Acceptance criteria
3456

35-
- [ ] AC-1: `docs/BRANCHING_MODEL.md` clearly states wave-loop PRs target `master`.
36-
- [ ] AC-2: `cargo build --release` in `bootstrap/` no longer panics on the Russian cross-walk file.
37-
- [ ] AC-3: `./scripts/tri test` parse/typecheck/gen/seal phases pass.
38-
- [ ] AC-4: W417 report and W418 cooperation files exist and are linked from `docs/NOW.md`.
39-
- [ ] AC-5: PR from `wave-loop-417` to `master` is opened with `Closes #1350`.
57+
### Bundle A
58+
- [ ] AC-A1: P12 is wired to a logic-analyzer channel and real CCLK capture files exist for `OSCFSEL=6` and `OSCFSEL=7`.
59+
- [ ] AC-A2: `tri fpga measured-to-lean --csv/--vcd --raw-ns --standalone` generated Lean files build with `lake build`.
60+
- [ ] AC-A3: Measured CCLK is within the N25Q128_3V spec, or any exceedance is explicitly explained.
61+
62+
### Bundle B
63+
- [ ] AC-B1: `tri fpga cold-por <bit> --relay-port <real>` performs an automated power-cycle and captures STAT.
64+
- [ ] AC-B2: The resulting log has `relay_mock: false` and a real STAT raw value.
65+
- [ ] AC-B3: `fpga/HARDWARE_SSOT.md` documents relay wiring and port mapping.
66+
67+
### Bundle C
68+
- [ ] AC-C1: A regression test verifies the PVT envelope lower bound across the operating rectangle.
69+
- [ ] AC-C2: Instrument import handles VCD `$date`/`$version`/`$comment` headers or analog CSV voltage columns.
70+
- [ ] AC-C3: A standalone `.lean` file generated from the CLI type-checks in a temporary `lake` package.
71+
72+
### Invariant checks
73+
- [ ] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
74+
- [ ] `lake build Trinity.TernaryFPGABoot` passes.
75+
- [ ] `cargo test -p tri fpga::tests` passes.
76+
77+
---
78+
79+
## Default variant
80+
81+
Execute **Variant A** if the analyzer is wired. Otherwise try **Variant B** if a
82+
relay is available. Otherwise fall back to **Variant C**.
4083

4184
---
4285

‎.trinity/current_task/activity.md‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1444,3 +1444,19 @@
14441444
- **Commit:** docs(NOW): W418 header, fix W417 issue reference to #1350, add Last updated line
14451445
- **Files:** .trinity/current-issue.md,.trinity/experience.md,docs/.legacy-non-english-docs,docs/BRANCHING_MODEL.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W418_2026-07-04.md,docs/reports/FPGA_LOOP_EVIDENCE_W417_2026-07-04.md,docs/reports/WAVE_LOOP_417_REPORT.md
14461446

1447+
## 2026-07-04T16:40:02Z — wave-loop-418
1448+
- **Commit:** docs(w417): hygiene, Strategy P, legacy allowlist, W417 close-out artifacts
1449+
- **Files:** .trinity/current-issue.md
1450+
1451+
## 2026-07-04T16:40:27Z — wave-loop-418
1452+
- **Commit:** docs(w418): set up current issue for Wave Loop 418
1453+
- **Files:** docs/NOW.md
1454+
1455+
## 2026-07-04T16:40:35Z — wave-loop-418
1456+
- **Commit:** docs(NOW): W418 setup, mark W417 PR #1354 merged
1457+
- **Files:** .trinity/current_task/activity.md,docs/NOW.md
1458+
1459+
## 2026-07-04T16:57:24Z — wave-loop-418
1460+
- **Commit:** docs(NOW): W418 setup, mark W417 PR #1354 merged
1461+
- **Files:** .claude/plans/wave-loop-418.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W419_2026-07-04.md,docs/reports/FPGA_LOOP_EVIDENCE_W418_2026-07-04.md,docs/reports/WAVE_LOOP_418_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
1462+

‎.trinity/experience.md‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,63 @@
11
# t27 / Trinity Agent Experience Log
22

3+
## 2026-07-04 — Wave Loop 418 (Variant C fallback: PVT regression, instrument import, standalone Lean integration)
4+
5+
### What worked
6+
- Adding a PVT-envelope **lower-bound regression test** in Rust and a matching
7+
Lean 4 lemma kept the placeholder envelope honest: every sampled operating
8+
context must produce `n25q128_min_sck_half_ns_pvt >= 6 ns`. The Rust test
9+
catches accidental coefficient changes; the Lean lemma proves the bound
10+
symbolically.
11+
- Skipping multi-line VCD `$date`/`$version`/`$comment` header sections with a
12+
small state machine was a contained parser change that prevents common
13+
vendor headers from being mistaken for `$var` declarations.
14+
- Detecting the analog CSV voltage column by header name (`voltage`, `v`,
15+
`analog`) fixes multi-channel imports where the first numeric column after
16+
time is the wrong signal. Adding a `header_named_columns` guard prevents the
17+
first-data-row numeric fallback from overriding an explicitly named column.
18+
- The **standalone Lean integration test** proves that `measured-to-lean
19+
--standalone --raw-ns` emits a file that builds inside a fresh temporary lake
20+
package requiring only the local Trinity library. This closes the gap between
21+
CLI output and external consumption.
22+
- Documenting the first-real-capture checklist and the PVT coefficient replacement
23+
recipe in `fpga/HARDWARE_SSOT.md` turns the current physical-evidence gap into
24+
an actionable protocol once the bench is wired.
25+
26+
### What changed behavior
27+
- `cli/tri/src/fpga.rs`: added PVT lower-bound regression test; added VCD
28+
multi-line header skip; added analog CSV voltage-column auto-detection; added
29+
standalone lake-package integration test.
30+
- `proofs/lean4/Trinity/TernaryFPGABoot.lean`: added
31+
`n25q128_min_sck_half_ns_pvt` and `pvt_half_ns_at_least_nominal`.
32+
- `fpga/HARDWARE_SSOT.md`: added §3.6.14 first-real-capture checklist and
33+
§3.6.15 PVT coefficient replacement recipe.
34+
- `docs/NOW.md`: updated W418 close-out and W419 setup.
35+
- Close-out artifacts: `docs/reports/WAVE_LOOP_418_REPORT.md`,
36+
`docs/reports/FPGA_LOOP_EVIDENCE_W418_2026-07-04.md`, and
37+
`docs/reports/FPGA_LOOP_COOPERATION_W419_2026-07-04.md`.
38+
39+
### Patterns to reuse
40+
- When a formal model uses placeholder coefficients, add both a symbolic
41+
lower-bound lemma and an exhaustive numeric regression test. The lemma
42+
documents the invariant; the test guards against accidental regressions.
43+
- For instrument parsers, add a regression test that exercises the exact quirk
44+
(multi-line VCD header, named CSV column) so future refactors do not drop the
45+
special case.
46+
- To prove a generated proof artifact is externally consumable, build it inside
47+
a temporary package that depends on the real library via a local path. This
48+
reuses existing `.lake` caches and avoids network downloads in CI.
49+
- When hardware is unavailable, convert the blocked physical step into a
50+
checklist and a falsifiable model update so the next wave can execute it
51+
immediately once the bench is ready.
52+
53+
### Anti-patterns to avoid
54+
- Do not let a parser fallback override an explicit user/header signal; track
55+
whether the header named the columns and skip the fallback when it did.
56+
- Do not add PVT coefficients in only one of the Rust or Lean files; keep the
57+
two models synchronized so the CLI and the proof assistant agree.
58+
- Do not claim an integration test passes just because the unit test of the
59+
generator passes; actually invoke `lake build` on the generated file.
60+
361
## 2026-07-04 — Wave Loop 417 (hygiene, reland W415/W416, Strategy P)
462

563
### What worked

0 commit comments

Comments
 (0)