gHashTag · gHashTag · Jul 4, 2026 · Jul 4, 2026 · Jul 4, 2026 · Jul 4, 2026
@@ -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*
@@ -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*
@@ -1,15 +1,18 @@
-# Wave Loop 419 — physical CCLK capture, real relay gate, or instrument-import parity
+# Wave Loop 421 — formal-only guarding and instrument-import depth (Variant C fallback)
 
-**Issue:** #1357  
-**Branch:** `wave-loop-419`  
-**Milestone:** Continue the FPGA boot-evidence line from W418.
+**Issue:** #1363  
+**Branch:** `wave-loop-421`  
+**Milestone:** Continue the FPGA boot-evidence line from Wave Loop 420.
 
 ---
 
 ## Goal
 
-Wave 418 closed the Variant C fallback (formal tooling and instrument import).
-Wave 419 re-evaluates the bench state and executes the first available variant.
+Wave 420 closed the Variant C fallback with VCD exact-terminator / real-net
+auto-threshold and PVT process-corner monotonicity while the physical bench
+remains blocked (P12 unwired, DLC10 cable missing, no relay). Wave 421
+re-evaluates the bench state and executes the first available variant from
+`docs/reports/FPGA_LOOP_COOPERATION_W421_2026-07-06.md`.
 
 1. **Variant A (preferred when bench becomes available):**
    - Wire P12 to a logic-analyzer channel and capture real CCLK for
@@ -21,35 +24,36 @@ Wave 419 re-evaluates the bench state and executes the first available variant.
    - Document the measured frequencies/duty cycles and PVT context in
      `fpga/HARDWARE_SSOT.md`.
 
-2. **Variant B (if relay hardware is available, no CCLK probe):**
-   - Implement a real `--relay-port` backend for `tri fpga cold-por`
-     (e.g. serial or TCP relay controlling board power).
-   - Perform an automated cold-POR power-cycle and capture STAT without
-     operator intervention.
-   - Document relay wiring and port syntax in `fpga/HARDWARE_SSOT.md`.
+2. **Variant B (if an external VCD/CSV capture is available, no on-bench relay):**
+   - Add CSV timestamp-column formats (fractional seconds / milliseconds).
+   - Add VCD real-net slope filters (reject transitions with Δt < t_setup or
+     ΔV < threshold_window).
+   - Add a `dlc10 capture --stub` dry-run path for later replay.
+   - Extend the PVT envelope with `OSCFSEL` derating coefficients.
 
 3. **Variant C (fallback if bench still blocked):**
-   - Extend instrument-import parity: additional VCD/CSV formats and hardened
-     `$comment` sections.
-   - Add PVT envelope monotonicity/antitonicity tests in Rust and Lean.
-   - Document the standalone `lake`-package workflow end-to-end in
-     `fpga/HARDWARE_SSOT.md`.
+   - Extend VCD robustness: `$timescale` parsing, `$dumpoff`/`$dumpon`
+     completeness, real-net slope/rise-time rejection.
+   - Add remaining PVT envelope shape lemmas (max half-period antitonicity,
+     combined temp+voltage+corner monotonicity, worst-case operating-point
+     search).
+   - Write a public comparison note: t27 vs Sparkle/Verilean vs Clash/Chisel.
+   - Land one safe gen-verilog #1245 sub-fix that does not increase the
+     16-failure yosys smoke baseline, if a narrow regression-free fix is
+     available.
 
 ---
 
 ## Decomposed plan
 
-See `docs/reports/FPGA_LOOP_COOPERATION_W419_2026-07-04.md` and
-`.claude/plans/wave-loop-419.md`.
-
 | Step | File(s) | Deliverable |
 |------|---------|-------------|
-| 1 | `cli/tri/src/fpga.rs` | Variant A import, B relay backend, or C parity/monotonicity tests |
-| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | PVT monotonicity lemmas or new measured theorems |
-| 3 | `fpga/HARDWARE_SSOT.md` | Updated capture / relay / integration protocol |
-| 4 | `docs/reports/*` | W419 report, evidence, W420 cooperation |
-| 5 | `.trinity/experience.md` | W419 learnings |
-| 6 | git/PR | squash-merge to `master`, close #1357, open #? for W420 |
+| 1 | `cli/tri/src/fpga.rs` or `cli/dlc10/src/main.rs` | Variant A import, B instrument depth, or C parser/formal hardening |
+| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | New measured theorems or PVT shape lemma |
+| 3 | `fpga/HARDWARE_SSOT.md` / `docs/reports` | Updated protocol or comparison note |
+| 4 | `docs/reports/*` | W421 report, evidence, W422 cooperation |
+| 5 | `.trinity/experience.md` | W421 learnings |
+| 6 | git/PR | squash-merge to `master`, close #1363, open #? for W422 |
 
 ---
 
@@ -61,14 +65,15 @@ See `docs/reports/FPGA_LOOP_COOPERATION_W419_2026-07-04.md` and
 - [ ] AC-A3: Measured CCLK satisfies the PVT-aware flash spec, or any exceedance is explicitly explained.
 
 ### Bundle B
-- [ ] AC-B1: `tri fpga cold-por <bit> --relay-port <real>` performs an automated power-cycle and captures STAT.
-- [ ] AC-B2: The resulting log has `relay_mock: false` and a real STAT raw value.
-- [ ] AC-B3: `fpga/HARDWARE_SSOT.md` documents relay wiring and port syntax.
+- [ ] AC-B1: CSV fractional-second / millisecond timestamp columns are parsed correctly with a regression test.
+- [ ] AC-B2: VCD real-net slope filter rejects spurious transitions with a regression test.
+- [ ] AC-B3: `dlc10 capture --stub` writes a dry-run command log with a regression test.
 
 ### Bundle C
-- [x] AC-C1: At least one additional instrument-import unit test lands (VCD `$comment` hardening + CSV `--csv-channel` explicit select).
-- [x] AC-C2: Rust and Lean tests verify PVT envelope monotonicity/antitonicity.
-- [x] AC-C3: The standalone lake-package workflow is documented end-to-end.
+- [x] AC-C1: VCD parser hardening lands with unit tests (`$timescale` exact-token terminator + embedded `$end` regression; real-net auto-threshold with `1 us` timescale).
+- [x] AC-C2: New PVT envelope shape lemma/test lands (`pvt_half_ns_monotone_combined`).
+- [x] AC-C3: `docs/reports/T27_VS_FORMAL_HDL_2026.md` comparison note is published.
+- [ ] AC-C4: One safe gen-verilog #1245 sub-fix lands without increasing the 16-failure yosys smoke count (deferred; remaining tracked gaps are not narrow regression-free sub-fixes).
 
 ### Invariant checks
 - [x] `./scripts/tri test` parse/typecheck/gen/seal-verify phases pass.
@@ -79,18 +84,18 @@ See `docs/reports/FPGA_LOOP_COOPERATION_W419_2026-07-04.md` and
 
 ## PR
 - Target: `master`
-- PR: #1360
-- Body: `Closes #1357`
-- Report: `docs/reports/WAVE_LOOP_419_REPORT.md`
-- Evidence: `docs/reports/FPGA_LOOP_EVIDENCE_W419_2026-07-05.md`
-- Cooperation W420: `docs/reports/FPGA_LOOP_COOPERATION_W420_2026-07-05.md`
+- PR: to open after work
+- Body: `Closes #1363`
+- Report: `docs/reports/WAVE_LOOP_421_REPORT.md`
+- Evidence: `docs/reports/FPGA_LOOP_EVIDENCE_W421_YYYY-MM-DD.md`
+- Cooperation W422: `docs/reports/FPGA_LOOP_COOPERATION_W422_YYYY-MM-DD.md`
 
 ---
 
 ## Default variant
 
 Execute **Variant A** if the analyzer and DLC10 cable are available. Otherwise
-try **Variant B** if a relay and DLC10 cable are available. Otherwise fall back
+try **Variant B** if an external capture file is available. Otherwise fall back
 to **Variant C**.
 
 ---

@@ -1464,3 +1464,27 @@
 - **Commit:** docs(w420): set W420 issue number to #1361 and record W419 PR #1360 (Closes #1357, Refs #1361)
 - **Files:** .trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W420_2026-07-05.md,docs/reports/FPGA_LOOP_EVIDENCE_W419_2026-07-05.md,docs/reports/WAVE_LOOP_419_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
 
+## 2026-07-04T18:36:50Z — wave-loop-420
+- **Commit:** feat(igla): Wave Loop 419 — Variant C VCD/CSV hardening, PVT monotonicity, standalone lake workflow
+- **Files:** .trinity/current-issue.md
+
+## 2026-07-04T18:37:55Z — wave-loop-420
+- **Commit:** setup(igla): initialize Wave Loop 420 current issue (#1361)
+- **Files:** .trinity/current-issue.md,.trinity/current_task/activity.md,docs/NOW.md
+
+## 2026-07-04T19:27:38Z — wave-loop-420
+- **Commit:** setup(igla): initialize Wave Loop 420 current issue and NOW.md update
+- **Files:** .claude/plans/wave-loop-420.md,.trinity/current-issue.md,.trinity/current_task/activity.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W421_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_W420_2026-07-06.md,docs/reports/WAVE_LOOP_420_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
+
+## 2026-07-04T19:30:24Z — wave-loop-420
+- **Commit:** feat(igla): Wave Loop 420 — VCD exact-terminator + real-net auto-threshold, PVT process-corner monotonicity
+- **Files:** docs/NOW.md
+
+## 2026-07-04T19:34:37Z — wave-loop-421
+- **Commit:** docs(issue): set current issue to Wave Loop 421\n\nCloses #1363\n\nCo-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
+- **Files:** .trinity/current-issue.md
+
+## 2026-07-04T19:44:52Z — wave-loop-421
+- **Commit:** docs(issue): set current issue to Wave Loop 421
+- **Files:** .claude/plans/wave-loop-421.md,.trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_W422_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_W421_2026-07-06.md,docs/reports/T27_VS_FORMAL_HDL_2026.md,docs/reports/WAVE_LOOP_421_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
+