Skip to content

Commit 13fa630

Browse files
Dmitrii Vasilevclaude
Dmitrii Vasilev
and
claude
committed
docs(experience): W433 learnings and missing W429-W431 plan files
- Add W433 experience entry to .trinity/experience.md. - Commit previously untracked .claude/plans for W429, W430, W431. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent ee99f6d commit 13fa630

5 files changed

Lines changed: 695 additions & 0 deletions

File tree

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

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,166 @@
1+
# Wave Loop 429 Implementation Plan
2+
3+
**Issue:** #1385
4+
**Branch:** `wave-loop-429`
5+
**Date:** 2026-07-06
6+
**Anchor:** φ² + φ⁻² = 3 | TRINITY
7+
8+
---
9+
10+
## Variant choice
11+
12+
**Execute Variant C** (formal / tooling / competitor refresh).
13+
14+
**Rationale:**
15+
- P12 CCLK probe is still unwired.
16+
- No relay / remote-power gate; `cold-por` is `MOCK`-only.
17+
- Xilinx DLC10 cable still missing; only Digilent HS2 is connected.
18+
- Only OSCFSEL 0–5 bitstreams exist; no 6/7 variants.
19+
- No external CSV/VCD captures were provided.
20+
- The board is reachable via HS2, but a real XADC readout implementation would be a multi-file JTAG feature and risks destabilizing the wave-loop line; it is better left for a future Variant B once the hardware state changes.
21+
22+
Variant C keeps W429 bounded, shippable, and aligned with the W428 baseline.
23+
24+
---
25+
26+
## Weak points investigated
27+
28+
| Weak point | Status | Risk |
29+
|---|---|---|
30+
| P12 CCLK probe unwired | unchanged | Blocks Variant A |
31+
| Relay / remote-power gate absent | unchanged | Blocks true cold-POR automation |
32+
| DLC10 cable missing | unchanged | Blocks `dlc10` path; HS2 + openFPGALoader still works |
33+
| OSCFSEL 6/7 bitstreams missing | unchanged | Blocks Variant A capture for fastest variants |
34+
| XADC readout placeholder | unchanged | Variant B possible but not in this wave |
35+
| PVT coefficients are conservative placeholders | unchanged | Model is falsifiable but not datasheet-accurate |
36+
| Gen-verilog #1245 residual 7 failures | unchanged | Tied to tuple-return / `let` destructuring / ROM arrays / CORDIC; unsafe for narrow sub-fix |
37+
38+
---
39+
40+
## Competitor snapshot (W429 boundary)
41+
42+
- **Sparkle / Verilean** — last public push July 3 2026; no post-July-5 commits/PRs indexed. PR #66 (IP.Net + compiler perf) and PR #65 (RV32 divider proof) remain the headline 2026 signals. Still the closest Lean-native competitor.
43+
- **Clash** — 1.11.0 Hackage candidate uploaded July 4 2026; not yet an official release. Latest official remains 1.10.0 (April 2026).
44+
- **Chisel / FIRRTL / CIRCT** — Chisel 7.13.0 (June 1 2026) bundles firtool 1.149.0. Standalone firtool 1.152.0 released July 4 2026, so the bundled tool trails the standalone release.
45+
- **Bluespec BSC 2026.01** (May 2026); 2026.07 release expected but not published.
46+
- **SpinalHDL** — v1.14.0 (Feb 2026), patch 1.14.2 (May 2026); no July release.
47+
- **Emerging signals:** CktFormalizer (Lean 4 autoformalization paper), Aria-HDL / fpga-meta-compiler-public (Rust → Lean4/SBY), TernaryCore, BitNet-RISCV-Multicore, MINRES RISC-V Tournament.
48+
49+
Strategic bottom line: Sparkle remains the only credible direct competitor in the same design space, but the ternary + spec-first sealed pipeline + physical boot-evidence triangle is still unoccupied by anyone else.
50+
51+
---
52+
53+
## Decomposed implementation
54+
55+
### Step 1 — Extend the unified OSCFSEL theorem family in Lean 4
56+
57+
**File:** `proofs/lean4/Trinity/TernaryFPGABoot.lean`
58+
59+
Add two quantified theorems that link raw-ns measurements to the W428 unified OSCFSEL theorems:
60+
61+
1. `cclk_variant_raw_ns_worstcase_pvt_satisfies_flash_spec (oscfsel : Nat) (h : oscfsel ≤ 7)`
62+
For any documented OSCFSEL selection, a raw capture whose period equals `cclk_period_ns oscfsel` and whose low/high times equal half the period satisfies the worst-case PVT-aware raw-ns flash predicate.
63+
64+
2. `cclk_variant_raw_ns_worstcase_pvt_implies_transaction_ok (oscfsel : Nat) (h : oscfsel ≤ 7) (bits : Nat)`
65+
The same raw capture produces a flash-spec-compliant SPI transaction under the worst-case PVT corner.
66+
67+
Both are proved by `interval_cases oscfsel <;> decide` and by applying the existing implication theorem with the worst-case context passed explicitly.
68+
69+
**Why:** W428 unified the `freq_hz/duty_pct` view; W429 closes the raw-ns view into the same quantified theorem family. This makes `measured-to-lean --raw-ns` theorems traceable to a single generic OSCFSEL result.
70+
71+
### Step 2 — Machine-readable `tri fpga measured-to-lean --json`
72+
73+
**File:** `cli/tri/src/fpga.rs`
74+
75+
- Add `json: bool` to `FpgaCmd::MeasuredToLean`.
76+
- Plumb the flag through `measured_to_lean` dispatch.
77+
- When `--json` is set, emit a single JSON object to stdout instead of free-form text:
78+
- `source`
79+
- `output_path` (or `null`)
80+
- `theorem_base`
81+
- `predicate` (e.g. `measured_cclk_with_pvt_satisfies_flash_spec`)
82+
- `pvt_context` (or `null`)
83+
- `validated` (bool)
84+
- Keep the existing human-readable path unchanged for backward compatibility.
85+
- Add unit tests:
86+
- `test_measured_to_lean_json_summary`
87+
- `test_measured_to_lean_json_summary_with_pvt_context`
88+
89+
**Why:** `measured-to-lean` is the bridge from bench captures to generated Lean proofs. Making its summary machine-readable lets downstream CI/dashboards consume the theorem metadata without parsing prose.
90+
91+
### Step 3 — Gen-verilog #1245 triage / deferral update
92+
93+
**File:** `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`
94+
95+
- Add "Triage decision for W429" section.
96+
- Confirm the same 7 yosys smoke failures from W428.
97+
- State that no new narrow, regression-free subclass appeared.
98+
- Keep the resolution plan: dedicated master merge/rebase wave after the FPGA boot-evidence line is no longer the primary focus.
99+
100+
**Why:** Documenting the deferral prevents re-investigation each wave and satisfies the weak-point investigation requirement.
101+
102+
### Step 4 — Refresh competitor snapshot
103+
104+
**File:** `docs/reports/T27_VS_FORMAL_HDL_2026.md`
105+
106+
- Update date to 2026-07-06 (W429 boundary).
107+
- Add post-July-5 findings:
108+
- Sparkle: no new indexed commits/PRs after July 5; repo-level last push July 3.
109+
- Clash 1.11.0 candidate still unreleased.
110+
- firtool 1.152.0 (July 4) remains latest; Chisel 7.13.0 bundles 1.149.0.
111+
- Bluespec/SpinalHDL no July releases.
112+
- Add or update "Emerging signals" with Aria-HDL source `zeta1999/fpga-meta-compiler-public`, MINRES RISC-V Tournament.
113+
- Adjust recommendation section to mention W429 progress.
114+
115+
### Step 5 — Close-out artifacts
116+
117+
Create:
118+
- `docs/reports/WAVE_LOOP_429_REPORT.md`
119+
- `docs/reports/FPGA_LOOP_EVIDENCE_W429_2026-07-06.md`
120+
- `docs/reports/FPGA_LOOP_COOPERATION_W430_2026-07-06.md` (three variants)
121+
122+
Update:
123+
- `docs/NOW.md` — W429 close-out / W430 setup.
124+
- `.trinity/experience.md` — W429 learnings.
125+
- `.trinity/current-issue.md` — mark acceptance criteria and PR/issue numbers.
126+
127+
### Step 6 — GitHub state
128+
129+
- Commit all changes to `wave-loop-429`.
130+
- Push branch.
131+
- Open PR `#?` with body `Closes #1385`.
132+
- Create issue `#?` for Wave Loop 430 and branch `wave-loop-430`.
133+
- Update memory entry and `MEMORY.md` index.
134+
135+
---
136+
137+
## Acceptance criteria
138+
139+
### AC-C1 (new theorem)
140+
- `lake build Trinity.TernaryFPGABoot` passes with the two new raw-ns OSCFSEL theorems.
141+
142+
### AC-C2 (gen-verilog)
143+
- `./scripts/tri test` gen-verilog-yosys-smoke reports the same 7 pre-existing failures; no increase.
144+
- `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` contains W429 deferral rationale.
145+
146+
### AC-C3 (CLI JSON)
147+
- `cargo test -p tri` passes including new `measured-to-lean --json` tests.
148+
- `tri fpga measured-to-lean --file capture.json --json` emits valid JSON.
149+
150+
### AC-C4 (competitors)
151+
- `docs/reports/T27_VS_FORMAL_HDL_2026.md` is updated for the W429 boundary with new signals.
152+
153+
### Invariants
154+
- `./scripts/tri test` parse/typecheck/gen-zig/gen-rust/gen-c/seal-verify/fixed-point/FPGA-smoke pass.
155+
- `cargo test -p tri` passes.
156+
- `lake build Trinity.TernaryFPGABoot` passes.
157+
158+
---
159+
160+
## Verification plan
161+
162+
1. After Lean edits: `lake build Trinity.TernaryFPGABoot`.
163+
2. After Rust edits: `cargo test -p tri`.
164+
3. After all edits: `./scripts/tri test` and inspect gen-verilog-yosys-smoke count.
165+
4. Manual CLI check: `tri fpga measured-to-lean --file ... --json`.
166+
5. Run L1/L3 git hooks on commit (already enforced by pre-commit).

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

Lines changed: 219 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,219 @@
1+
# Wave Loop 430 Decomposed Plan
2+
3+
**Issue:** #1388
4+
**Branch:** `wave-loop-430`
5+
**Date:** 2026-07-01
6+
**Anchor:** φ² + φ⁻² = 3 | TRINITY
7+
8+
---
9+
10+
## 1. OBSERVE summary
11+
12+
- We are on `wave-loop-430`, issue `#1388`.
13+
- W429 closed with PR #1387; next wave should continue the FPGA boot-evidence line.
14+
- The bench is **partially unblocked**: a Digilent HS2 FTDI cable is connected to
15+
the XC7A200T Wukong V1 board (`idcode 0x03636093`). `openFPGALoader -c digilent_hs2`
16+
works for SRAM load, STAT read, and **XADC readout**.
17+
- Live XADC probe returned:
18+
```text
19+
temp: 42.8206 °C
20+
vccint: 1.00049 V
21+
vccaux: 1.80615 V
22+
```
23+
- **P12 CCLK probe is still unwired**, so real CCLK capture (Variant A) is not
24+
possible today.
25+
- No external CSV/VCD captures exist in the repo, so pure import-only Variant B
26+
is also not directly available.
27+
- Therefore the default selection rule points to **Variant B via real XADC
28+
readout**, with a small formal-extension side-car so the wave also advances
29+
the PVT-aware theorem library.
30+
31+
---
32+
33+
## 2. Weak points
34+
35+
1. **XADC readout is not wired into `tri fpga`.** `boot-log`, `cold-por`, and
36+
`cclk-sweep` still emit `"source": "not_read"` for `xadc`. The live operating
37+
point cannot yet flow into generated Lean theorems or JSON logs.
38+
2. **P12 CCLK probe unwired.** Real CCLK capture for OSCFSEL 6/7 remains blocked.
39+
3. **SPI flash cold-POR automation needs a relay gate.** Without it, the physical
40+
OSCFSEL sweep still requires manual power cycles.
41+
4. **Gen-verilog #1245 residual 7 failures** are tied to tuple-return / `let`
42+
destructuring / ROM arrays / CORDIC. They are not safe as a single-wave
43+
regression-free sub-fix.
44+
5. **Competitive pressure from Lean-native HDL** (Sparkle/Verilean, CktFormalizer,
45+
Aria-HDL) is rising; the ternary + physical-evidence angle is the key
46+
differentiator.
47+
6. **PVT derating coefficients remain conservative placeholders**, not Micron
48+
datasheet values. Any new XADC-derived operating point must be explicitly
49+
framed as "within the modeled envelope" rather than "exact datasheet".
50+
51+
---
52+
53+
## 3. Competitor snapshot (July 2026)
54+
55+
- **Sparkle / Verilean**: last public push 2026-07-03; PR #66 (IP.Net + compiler
56+
perf) and PR #65 (RV32 divider proof) remain the headline 2026 signals. Still
57+
the closest Lean-native competitor.
58+
- **Clash**: 1.11.0 is only a Hackage candidate; latest release remains 1.10.0
59+
(April 2026). No new formal headline.
60+
- **Chisel / CIRCT / firtool**: Chisel 7.13.0 (June 2026) is the latest release;
61+
firtool 1.152.0 (July 4 2026) is the latest available. No 7.14.0 / 1.153
62+
evidence yet.
63+
- **CktFormalizer**: arXiv 2605.07782 (May 2026) — LLM-to-circuit autoformalization
64+
in Lean 4, 95–100% synthesis/P&R success, 35% area / 30% power reduction with
65+
closed-loop PPA optimization. Validates Lean 4 as a hardware proof backend.
66+
- **TernaryCore**: `shepherdscientific/ternarycore` (April–May 2026) — BitNet b1.58
67+
ternary inference on FPGA, zero-DSP MAC/dot/GEMM, 31/31 simulation tests.
68+
- **ternfpga**: `Neumann-Labs/ternfpga` (June 2026) — multiplier-free ternary LLM
69+
engine on Arty A7-35T, claims better energy-per-token than RTX 3060.
70+
- **KU Leuven MICAS ternary-lut-dse** (April 2026) — Chisel RTL generator for
71+
LUT-based 1.58-bit LLM accelerators, validated in TSMC 16nm.
72+
- **Aria-HDL**: no new July signal; keep watching.
73+
74+
Strategic implication: the Lean-native + ternary + physical-evidence triangle is
75+
still the unique intersection. W430 should harden the physical-evidence loop by
76+
consuming real XADC data.
77+
78+
---
79+
80+
## 4. Variant selection
81+
82+
**Primary: Variant B — real XADC readout.**
83+
84+
The board is reachable and `openFPGALoader --read-xadc` already returns live
85+
data. Implementing a parser and wiring it into `tri fpga boot-log` /
86+
`cold-por` / `cclk-sweep` advances the physical boot-evidence story without
87+
needing the P12 probe or relay gate.
88+
89+
**Side-car: a small formal extension.**
90+
Add a Lean lemma that any operating point with temp ≤ 85 °C, vccint ≥ 900 mV,
91+
vccaux ≥ 1800 mV lies inside the modeled PVT rectangle, plus a theorem that the
92+
real XADC values (≈43 °C, ≈1000 mV, ≈1806 mV) satisfy this rectangle. This gives
93+
AC-C1-style coverage and links the live measurement to the PVT envelope
94+
family.
95+
96+
**Gen-verilog #1245:** re-evaluate; if no narrow subclass is safe, explicitly
97+
defer and update the defects doc.
98+
99+
---
100+
101+
## 5. Decomposed implementation steps
102+
103+
### 5.1 Parse `openFPGALoader --read-xadc` output
104+
- Add `XadcContext` struct in `cli/tri/src/fpga.rs`:
105+
- `temp_c: f64`, `max_temp_c: f64`, `min_temp_c: f64`
106+
- `vccint_v: f64`, `max_vccint_v: f64`, `min_vccint_v: f64`
107+
- `vccaux_v: f64`, `max_vccaux_v: f64`, `min_vccaux_v: f64`
108+
- `raw: serde_json::Value`
109+
- Add `read_xadc_via_openfpgaloader(cable: &str) -> Result<XadcContext>`.
110+
- Run `openFPGALoader -c <cable> --read-xadc`.
111+
- Parse the emitted pseudo-JSON with `serde_json` after a normalization pass
112+
(remove trailing commas, collapse whitespace). Fallback to regex if
113+
normalization fails.
114+
- Add unit tests with captured sample output (the live probe above).
115+
116+
### 5.2 Wire live XADC into `tri fpga` commands
117+
- Add `--xadc` flag to `FpgaCmd::BootLog`, `FpgaCmd::ColdPor`, and
118+
`FpgaCmd::CclkSweep` (default: false / auto-detect only when the flag is
119+
passed, to avoid breaking board-less CI).
120+
- When `--xadc` is set and a Digilent cable is detected:
121+
- Call `read_xadc_via_openfpgaloader`.
122+
- Populate the `xadc` field of `BootLog` / `ColdPorLog` / `SweepLog` with
123+
`source: "xadc"` and live values.
124+
- When `--xadc` is not set or the board is absent, keep the existing
125+
`"not_read"` / PVT-context fallback so board-less CI stays green.
126+
- Add `test_read_xadc_context_parses_sample_output` and a test that a missing
127+
board yields an actionable error.
128+
129+
### 5.3 Formal bridge in Lean 4
130+
- Add `pvt_operating_rectangle` predicate in
131+
`proofs/lean4/Trinity/TernaryFPGABoot.lean`:
132+
- `temp_c ≤ PVT_TEMP_MAX_C`
133+
- `vccint_mv ≥ PVT_VCCINT_MIN_MV`
134+
- `vccaux_mv ≥ PVT_VCCAUX_MIN_MV`
135+
- Add `xadc_operating_point_within_pvt_envelope` theorem: the real operating
136+
point (≈43 °C, ≈1000 mV, ≈1806 mV) satisfies the rectangle.
137+
- Add `xadc_context_implies_pvt_envelope` theorem: any XADC context within the
138+
rectangle implies the worst-case PVT corner bounds the flash timing. This
139+
links the live measurement to the existing `measured_cclk_from_raw_ns_with_pvt`
140+
family.
141+
142+
### 5.4 Documentation and evidence
143+
- Update `fpga/HARDWARE_SSOT.md` §3.6.19:
144+
- Add the canonical `tri fpga read-xadc` / `--xadc` recipe.
145+
- Document the captured sample values and the `--pvt-context` workflow.
146+
- Create `docs/reports/FPGA_LOOP_EVIDENCE_W430_2026-07-01.md` with the live XADC
147+
capture and the JSON log artifact.
148+
149+
### 5.5 Competitor refresh
150+
- Update `docs/reports/T27_VS_FORMAL_HDL_2026.md`:
151+
- Refresh date to W430.
152+
- Add the July 2026 signals above.
153+
- Note that the live XADC readout further differentiates the physical-evidence
154+
loop.
155+
156+
### 5.6 Gen-verilog triage
157+
- Re-run `./scripts/tri test` at start of wave and confirm the same 7 failures.
158+
- If no narrow safe subclass appears, update
159+
`docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` with W430 triage decision.
160+
161+
### 5.7 Verification
162+
- `cargo test --bin tri fpga::`: must pass.
163+
- `lake build Trinity.TernaryFPGABoot`: must pass.
164+
- `./scripts/tri test`: must pass except the 7 pre-existing #1245 failures.
165+
- Manual: `tri fpga read-xadc` or `tri fpga boot-log ... --xadc` produces a JSON
166+
log with `xadc.source: "xadc"` and live values.
167+
168+
### 5.8 Close-out
169+
- Write `docs/reports/WAVE_LOOP_430_REPORT.md`.
170+
- Write `docs/reports/FPGA_LOOP_COOPERATION_W431_2026-07-01.md` with Variant A/B/C
171+
for W431.
172+
- Create GitHub issue #1389 and branch `wave-loop-431`.
173+
- Update `.trinity/current-issue.md`, `docs/NOW.md`, `.trinity/experience.md`, and
174+
persistent memory.
175+
176+
---
177+
178+
## 6. Acceptance criteria
179+
180+
- AC-B1: `tri fpga read-xadc` (or `--xadc` flag) returns live temp/vccint/vccaux
181+
from the board and emits `source: "xadc"`.
182+
- AC-B2: `boot-log`, `cold-por`, and `cclk-sweep` can include live XADC context
183+
in their JSON logs.
184+
- AC-B3: At least one new Lean theorem links the live/any XADC operating point
185+
to the PVT envelope and builds with `lake build`.
186+
- AC-B4: The XADC recipe is documented in `fpga/HARDWARE_SSOT.md`.
187+
- AC-C1-equivalent: the formal extension above satisfies the Variant C fallback
188+
theorem requirement.
189+
190+
---
191+
192+
## 7. Files to touch
193+
194+
- `cli/tri/src/fpga.rs`
195+
- `proofs/lean4/Trinity/TernaryFPGABoot.lean`
196+
- `fpga/HARDWARE_SSOT.md`
197+
- `docs/reports/T27_VS_FORMAL_HDL_2026.md`
198+
- `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`
199+
- `docs/reports/WAVE_LOOP_430_REPORT.md` (new)
200+
- `docs/reports/FPGA_LOOP_EVIDENCE_W430_2026-07-01.md` (new)
201+
- `docs/reports/FPGA_LOOP_COOPERATION_W431_2026-07-01.md` (new)
202+
- `docs/NOW.md`
203+
- `.trinity/current-issue.md`
204+
- `.trinity/experience.md`
205+
206+
---
207+
208+
## 8. Risks and mitigations
209+
210+
| Risk | Mitigation |
211+
|---|---|
212+
| openFPGALoader `--read-xadc` output format changes | Parser uses normalization + regex fallback; unit test against captured sample. |
213+
| Board not powered during CI | `--xadc` is opt-in; board-less CI uses existing placeholder path. |
214+
| Live XADC values drift across runs | Evidence file records one representative capture; the formal theorem bounds the rectangle, not a single point. |
215+
| No narrow gen-verilog fix | Explicitly defer and update defects doc; do not broaden scope. |
216+
217+
---
218+
219+
*φ² + φ⁻² = 3 | TRINITY*

0 commit comments

Comments
 (0)