feat(igla): Wave Loop 436 — live XADC → PVT context in boot logs and sweep reports (closes #1402)

.claude/plans/wave-loop-420.md

@@ -0,0 +1,69 @@
+# Wave Loop 420 — Decomposed Plan
+
+**Issue:** #1361  
+**Branch:** `wave-loop-420`  
+**Default variant:** C (physical bench still blocked: DLC10 cable not found, P12 unwired, no relay)
+
+---
+
+## 1. Weak points identified
+
+1. **Missing VCD `$comment` exact-token terminator.** The W419 report claimed this
+   hardening landed, but the merged commit (`101fd0748`) did not touch the VCD
+   parser. The current code still uses `ends_with("$end")` / `contains(" $end")`
+   heuristics, so a `$comment` block containing the literal substring `$end`
+   terminates early and corrupts the signal dictionary.
+2. **Real-valued VCD nets require an explicit `--vcd-threshold-v`.** There is no
+   auto-threshold fallback for analog VCD exports; users must know the voltage
+   swing up-front.
+3. **PVT half-period bound lacks a process-corner monotonicity lemma.** We have
+   temperature monotonicity and VCCINT antitonicity from W419, but no formal
+   statement that `ff ≤ tt ≤ ss` is preserved by the half-period bound itself.
+
+---
+
+## 2. Competitor landscape (high-level)
+
+The closest formal-HDL competition is **Sparkle / Verilean** (Lean 4 native,
+binary RTL). Other credible players: **Clash** (Haskell, external formal),
+**Chisel/FIRRTL/CIRCT** (mainstream, SVA/model-checking oriented),
+**Bluespec** (rule-based, Coq bridge via Kami), **Coq Kami / Silver Oak**
+(dependent-type hardware), **ACL2** (specification/proof layer only).
+
+None combine Lean 4 native proof, a ternary compute stack, spec-first sealed
+`*.t27 → gen/` code generation, and physical boot-evidence instrumentation.
+That intersection is the gap t27 fills.
+
+---
+
+## 3. Implementation steps
+
+| Step | Files | Deliverable | Acceptance |
+|------|-------|-------------|------------|
+| 3.1 | `cli/tri/src/fpga.rs` | Replace VCD `$date`/`$version`/`$comment` terminator heuristics with exact-token check; clear state immediately on same-line termination. | `test_parse_vcd_comment_with_embedded_end_token` PASS |
+| 3.2 | `cli/tri/src/fpga.rs` | Add VCD auto-threshold for real-valued nets: compute `50% (vmin + vmax)` when `--vcd-threshold-v` is omitted; warn user. | `test_parse_vcd_real_auto_threshold` PASS |
+| 3.3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Add `pvt_half_ns_monotone_in_process_corner` lemma: `c1.worse_than c2 → bound c1 ≤ bound c2`. | `lake build` PASS |
+| 3.4 | `cli/tri/src/fpga.rs` | Add Rust test `test_pvt_half_ns_monotone_in_process_corner`. | `cargo test` PASS |
+| 3.5 | `fpga/HARDWARE_SSOT.md` | Document VCD `$comment` exact-terminator behavior and real-net auto-threshold. | docs render clean |
+| 3.6 | `.trinity/experience.md` | Capture W420 learnings. | committed |
+| 3.7 | `docs/reports/*` | W420 report, evidence, W421 cooperation variants. | committed |
+
+---
+
+## 4. Verification plan
+
+- `cargo test -p tri vcd` — expect 12 tests (was 11).
+- `cargo test -p tri pvt` — expect 10 tests (was 9).
+- `cargo test -p tri fpga::tests` — expect 47 tests (was 45).
+- `lake build Trinity.TernaryFPGABoot` — must PASS.
+- `./scripts/tri test` — must PASS except 16 pre-existing gen-verilog yosys failures.
+
+---
+
+## 5. Land
+
+- Commit with `Closes #1361`.
+- Open PR #? from `wave-loop-420` → `master`.
+- After merge, create issue #? and branch `wave-loop-421`.
+
+*φ² + φ⁻² = 3 | TRINITY*

.claude/plans/wave-loop-421.md

@@ -0,0 +1,77 @@
+# Wave Loop 421 Decomposed Plan
+
+**Issue:** #1363  
+**Branch:** `wave-loop-421`  
+**Date:** 2026-07-06  
+**Selected variant:** C (fallback — hardware still unreachable)
+
+---
+
+## 1. Weak-point analysis
+
+### 1.1 W420 dependency / branch state
+- `wave-loop-421` was created from `master` (101fd0748) **before** PR #1362
+  (Wave Loop 420) merges. This means the W421 branch initially lacked the W420
+  VCD exact-terminator and auto-threshold work.
+- **Mitigation:** reset `wave-loop-421` onto `wave-loop-420` so W421 builds on
+  top of W420. Once PR #1362 lands, W421 can be rebased onto `master` cleanly.
+
+### 1.2 VCD parser remaining gaps
+- `$date` / `$version` / `$comment` sections now use exact-token terminators
+  (W420), but `$timescale` still uses the old substring heuristics
+  `contains(" $end")` / `ends_with(" $end")`. A `$timescale` comment that
+  mentions `$end` could therefore mis-parse.
+- Real-valued net auto-threshold works, but has no regression test for a
+  non-default `$timescale` unit (e.g., `1 us` or `1 ps`).
+
+### 1.3 PVT envelope
+- W419/W420 proved each axis independently (temp monotone, VCCINT antitone,
+  corner monotone). The combined ordering (temp ↑, VCCINT ↓, corner worse) is
+  not yet a single lemma/test, which is what a worst-case operating-point
+  search actually needs.
+
+### 1.4 Competition
+- Sparkle/Verilean (Lean 4 native HDL) is the closest competitor and is
+  accelerating in 2026: RV32IMA SoC, networking stack, crypto, formal proofs.
+- Clash Formal and CIRCT/Chisel LTL/Verif dialects are also closing the formal
+  gap from the mainstream side.
+- t27 must keep differentiating through: (a) ternary/balanced-trit compute + Lean
+  proof lattice, (b) spec-first `*.t27 → gen/` sealed pipeline, (c) physical
+  boot-evidence instrumentation.
+
+### 1.5 Hardware
+- The Digilent FTDI cable is present (`0x0403:0x6014`), but `openFPGALoader
+  --detect` reports **0 devices**. The board is either not powered, not wired,
+  or the JTAG header is disconnected. Variant A is therefore still blocked.
+
+---
+
+## 2. Work items
+
+| # | File | Change | Test |
+|---|------|--------|------|
+| 1 | `cli/tri/src/fpga.rs` | Apply `vcd_line_ends_with_token` to `$timescale` terminator | `test_parse_vcd_timescale_with_embedded_end_token` |
+| 2 | `cli/tri/src/fpga.rs` | Add non-default `$timescale` real-net parse test | `test_parse_vcd_real_auto_threshold_us_timescale` |
+| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Add combined PVT monotonicity lemma | `lake build Trinity.TernaryFPGABoot` |
+| 4 | `cli/tri/src/fpga.rs` | Add combined PVT monotonicity Rust test | `test_pvt_half_ns_monotone_combined` |
+| 5 | `docs/reports/T27_VS_FORMAL_HDL_2026.md` | Competitor comparison note | visual review |
+| 6 | `fpga/HARDWARE_SSOT.md` | §3.6.18 documenting W421 parser + PVT improvements | visual review |
+| 7 | `docs/NOW.md` | W421 close-out / W422 setup | visual review |
+| 8 | `.trinity/experience.md` | W421 learnings | visual review |
+| 9 | `docs/reports/*` | W421 report, evidence, W422 cooperation | visual review |
+| 10 | git/PR/issue | Commit, open PR #? for W421, create W422 issue + branch | CI passes |
+
+---
+
+## 3. Verification checklist
+
+- [ ] `cargo test -p tri vcd`: all PASS (was 13).
+- [ ] `cargo test -p tri pvt`: all PASS (was 10).
+- [ ] `cargo test -p tri fpga::tests`: all PASS (was 48).
+- [ ] `lake build Trinity.TernaryFPGABoot`: PASS.
+- [ ] `./scripts/tri test`: no new failures beyond the 16 pre-existing yosys
+      smoke failures from weak point #1245.
+
+---
+
+*φ² + φ⁻² = 3 | TRINITY*

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

@@ -0,0 +1,166 @@
+# Wave Loop 429 Implementation Plan
+
+**Issue:** #1385  
+**Branch:** `wave-loop-429`  
+**Date:** 2026-07-06  
+**Anchor:** φ² + φ⁻² = 3 | TRINITY
+
+---
+
+## Variant choice
+
+**Execute Variant C** (formal / tooling / competitor refresh).
+
+**Rationale:**
+- P12 CCLK probe is still unwired.
+- No relay / remote-power gate; `cold-por` is `MOCK`-only.
+- Xilinx DLC10 cable still missing; only Digilent HS2 is connected.
+- Only OSCFSEL 0–5 bitstreams exist; no 6/7 variants.
+- No external CSV/VCD captures were provided.
+- 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.
+
+Variant C keeps W429 bounded, shippable, and aligned with the W428 baseline.
+
+---
+
+## Weak points investigated
+
+| Weak point | Status | Risk |
+|---|---|---|
+| P12 CCLK probe unwired | unchanged | Blocks Variant A |
+| Relay / remote-power gate absent | unchanged | Blocks true cold-POR automation |
+| DLC10 cable missing | unchanged | Blocks `dlc10` path; HS2 + openFPGALoader still works |
+| OSCFSEL 6/7 bitstreams missing | unchanged | Blocks Variant A capture for fastest variants |
+| XADC readout placeholder | unchanged | Variant B possible but not in this wave |
+| PVT coefficients are conservative placeholders | unchanged | Model is falsifiable but not datasheet-accurate |
+| Gen-verilog #1245 residual 7 failures | unchanged | Tied to tuple-return / `let` destructuring / ROM arrays / CORDIC; unsafe for narrow sub-fix |
+
+---
+
+## Competitor snapshot (W429 boundary)
+
+- **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.
+- **Clash** — 1.11.0 Hackage candidate uploaded July 4 2026; not yet an official release. Latest official remains 1.10.0 (April 2026).
+- **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.
+- **Bluespec BSC 2026.01** (May 2026); 2026.07 release expected but not published.
+- **SpinalHDL** — v1.14.0 (Feb 2026), patch 1.14.2 (May 2026); no July release.
+- **Emerging signals:** CktFormalizer (Lean 4 autoformalization paper), Aria-HDL / fpga-meta-compiler-public (Rust → Lean4/SBY), TernaryCore, BitNet-RISCV-Multicore, MINRES RISC-V Tournament.
+
+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.
+
+---
+
+## Decomposed implementation
+
+### Step 1 — Extend the unified OSCFSEL theorem family in Lean 4
+
+**File:** `proofs/lean4/Trinity/TernaryFPGABoot.lean`
+
+Add two quantified theorems that link raw-ns measurements to the W428 unified OSCFSEL theorems:
+
+1. `cclk_variant_raw_ns_worstcase_pvt_satisfies_flash_spec (oscfsel : Nat) (h : oscfsel ≤ 7)`  
+   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.
+
+2. `cclk_variant_raw_ns_worstcase_pvt_implies_transaction_ok (oscfsel : Nat) (h : oscfsel ≤ 7) (bits : Nat)`  
+   The same raw capture produces a flash-spec-compliant SPI transaction under the worst-case PVT corner.
+
+Both are proved by `interval_cases oscfsel <;> decide` and by applying the existing implication theorem with the worst-case context passed explicitly.
+
+**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.
+
+### Step 2 — Machine-readable `tri fpga measured-to-lean --json`
+
+**File:** `cli/tri/src/fpga.rs`
+
+- Add `json: bool` to `FpgaCmd::MeasuredToLean`.
+- Plumb the flag through `measured_to_lean` dispatch.
+- When `--json` is set, emit a single JSON object to stdout instead of free-form text:
+  - `source`
+  - `output_path` (or `null`)
+  - `theorem_base`
+  - `predicate` (e.g. `measured_cclk_with_pvt_satisfies_flash_spec`)
+  - `pvt_context` (or `null`)
+  - `validated` (bool)
+- Keep the existing human-readable path unchanged for backward compatibility.
+- Add unit tests:
+  - `test_measured_to_lean_json_summary`
+  - `test_measured_to_lean_json_summary_with_pvt_context`
+
+**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.
+
+### Step 3 — Gen-verilog #1245 triage / deferral update
+
+**File:** `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md`
+
+- Add "Triage decision for W429" section.
+- Confirm the same 7 yosys smoke failures from W428.
+- State that no new narrow, regression-free subclass appeared.
+- Keep the resolution plan: dedicated master merge/rebase wave after the FPGA boot-evidence line is no longer the primary focus.
+
+**Why:** Documenting the deferral prevents re-investigation each wave and satisfies the weak-point investigation requirement.
+
+### Step 4 — Refresh competitor snapshot
+
+**File:** `docs/reports/T27_VS_FORMAL_HDL_2026.md`
+
+- Update date to 2026-07-06 (W429 boundary).
+- Add post-July-5 findings:
+  - Sparkle: no new indexed commits/PRs after July 5; repo-level last push July 3.
+  - Clash 1.11.0 candidate still unreleased.
+  - firtool 1.152.0 (July 4) remains latest; Chisel 7.13.0 bundles 1.149.0.
+  - Bluespec/SpinalHDL no July releases.
+- Add or update "Emerging signals" with Aria-HDL source `zeta1999/fpga-meta-compiler-public`, MINRES RISC-V Tournament.
+- Adjust recommendation section to mention W429 progress.
+
+### Step 5 — Close-out artifacts
+
+Create:
+- `docs/reports/WAVE_LOOP_429_REPORT.md`
+- `docs/reports/FPGA_LOOP_EVIDENCE_W429_2026-07-06.md`
+- `docs/reports/FPGA_LOOP_COOPERATION_W430_2026-07-06.md` (three variants)
+
+Update:
+- `docs/NOW.md` — W429 close-out / W430 setup.
+- `.trinity/experience.md` — W429 learnings.
+- `.trinity/current-issue.md` — mark acceptance criteria and PR/issue numbers.
+
+### Step 6 — GitHub state
+
+- Commit all changes to `wave-loop-429`.
+- Push branch.
+- Open PR `#?` with body `Closes #1385`.
+- Create issue `#?` for Wave Loop 430 and branch `wave-loop-430`.
+- Update memory entry and `MEMORY.md` index.
+
+---
+
+## Acceptance criteria
+
+### AC-C1 (new theorem)
+- `lake build Trinity.TernaryFPGABoot` passes with the two new raw-ns OSCFSEL theorems.
+
+### AC-C2 (gen-verilog)
+- `./scripts/tri test` gen-verilog-yosys-smoke reports the same 7 pre-existing failures; no increase.
+- `docs/reports/GEN_VERILOG_DEFECTS_REPRO.md` contains W429 deferral rationale.
+
+### AC-C3 (CLI JSON)
+- `cargo test -p tri` passes including new `measured-to-lean --json` tests.
+- `tri fpga measured-to-lean --file capture.json --json` emits valid JSON.
+
+### AC-C4 (competitors)
+- `docs/reports/T27_VS_FORMAL_HDL_2026.md` is updated for the W429 boundary with new signals.
+
+### Invariants
+- `./scripts/tri test` parse/typecheck/gen-zig/gen-rust/gen-c/seal-verify/fixed-point/FPGA-smoke pass.
+- `cargo test -p tri` passes.
+- `lake build Trinity.TernaryFPGABoot` passes.
+
+---
+
+## Verification plan
+
+1. After Lean edits: `lake build Trinity.TernaryFPGABoot`.
+2. After Rust edits: `cargo test -p tri`.
+3. After all edits: `./scripts/tri test` and inspect gen-verilog-yosys-smoke count.
+4. Manual CLI check: `tri fpga measured-to-lean --file ... --json`.
+5. Run L1/L3 git hooks on commit (already enforced by pre-commit).