chore(trinity): point current-issue.md to W403 issue #1307 and add decomposed plan

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: Dmitrii Vasilev

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

@@ -0,0 +1,57 @@
+# Wave Loop 403 — Decomposed Plan
+
+**Issue:** #1307  
+**Branch:** `trinity-rust-rings`  
+**Goal:** Close the deferred physical CCLK measurement (Variant A), extend the
+Lean 4 formal model to bitstream configuration (Variant B), or add a
+physical-cable smoke path (Variant C).
+
+---
+
+## 1. Weak points
+
+### 1.1 Physical blocker (Variant A)
+- **CCLK measurement still requires bench access.** Without a logic analyser /
+  oscilloscope on pin P12, Variant A cannot close.
+
+### 1.2 Formal gap (Variant B)
+- `TernaryFPGABoot.lean` models STAT decoding and the cold-POR decision tree,
+  but does not yet link the canonical bitstream configuration (`IDCODE`,
+  `SPI_BUSWIDTH`, `STARTUPCLK`, `OSCFSEL`) to the boot predicates.
+
+### 1.3 Smoke-gate physical gap (Variant C)
+- `tri fpga smoke-gate` is board-less. A cable-connected SRAM load would catch
+  bitstream regressions that static assertions miss, but it needs hardware.
+
+---
+
+## 2. Competitor scan
+
+Same as W402: Sparkle HDL, Verilean, Sail, Kami, FIRRTL/Chisel, Clash,
+Bluespec. The closest formal-HDL threat remains **Verilean / Lean 4 HDL**;
+Variant B directly counters it by extending the t27 proof lattice into the
+FPGA-boot domain.
+
+---
+
+## 3. Cooperation variants
+
+See `docs/reports/FPGA_LOOP_COOPERATION_2026-07-05.md` for the full three
+variants and acceptance criteria.
+
+| Variant | Hardware needed | Primary deliverable |
+|---------|-----------------|---------------------|
+| A | logic analyser / oscilloscope | Measured CCLK frequency in `fpga/HARDWARE_SSOT.md` |
+| B | none | Lean 4 bitstream-config lemmas |
+| C | Digilent cable + board | Optional `--require-cable` SRAM smoke load |
+
+---
+
+## 4. Recommended next action
+
+If hardware is available, execute **Variant A**. Otherwise execute **Variant
+B**.
+
+---
+
+*φ² + φ⁻² = 3 | TRINITY*

.trinity/current-issue.md

@@ -1,38 +1,38 @@
-# Wave Loop 402 — FPGA: close AC5 physical CCLK measurement + follow-up hardening
+# Wave Loop 403 — FPGA: close physical CCLK measurement or extend formal/physical smoke coverage
 
-**Issue:** #1305  
+**Issue:** #1307  
 **Branch:** `trinity-rust-rings`  
-**Milestone:** W401 hardened the cold-POR protocol and added board-less CI guards.
-Now close the deferred AC5 (physical CCLK measurement on P12) or pursue one of the
-alternate cooperation variants.
+**Milestone:** W402 formalized the cold-POR decision tree in Lean 4. W403 should
+close the remaining physical AC or extend formal/physical smoke coverage.
 
 ---
 
 ## Goal
 
 1. Capture the actual CCLK frequency on pin P12 and record it in
    `fpga/HARDWARE_SSOT.md` (Variant A — default if hardware is available).
-2. OR encode the cold-POR / CCLK decision tree in Lean 4 (Variant B — no
-   hardware required).
+2. OR extend the Lean 4 model with bitstream-configuration predicates
+   (`STARTUPCLK`, `OSCFSEL`, `SPI_BUSWIDTH`) and link them to the decision trees
+   (Variant B — no hardware required).
 3. OR extend `tri fpga smoke-gate` to optionally load the GF16 matrix into SRAM
    and assert `DONE=HIGH` when a cable is present (Variant C — stretch).
-4. Update close-out reports and open W403 cooperation variants.
+4. Update close-out reports and open W404 cooperation variants.
 
 ---
 
 ## Decomposed plan
 
-See `.claude/plans/wave-loop-402.md` for the full work breakdown.
+See `.claude/plans/wave-loop-403.md` for the full work breakdown.
 
 | Step | File(s) | Deliverable |
 |------|---------|-------------|
-| 1 | `.claude/plans/wave-loop-402.md` | Decomposed plan + weak-point + competitor scan |
+| 1 | `.claude/plans/wave-loop-403.md` | Decomposed plan + weak-point + competitor scan |
 | 2 | `fpga/HARDWARE_SSOT.md` (Variant A) | Measured CCLK frequency/duty cycle on P12 |
-| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | Formal STAT/decision-tree lemmas |
+| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | Bitstream-config lemmas |
 | 4 | `cli/tri/src/fpga.rs` (Variant C) | Optional cable-connected SRAM smoke load |
-| 5 | `docs/reports/*` | W402 report, evidence, W403 cooperation |
-| 6 | `.trinity/experience.md` | W402 learnings |
-| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1305, open #W403 |
+| 5 | `docs/reports/*` | W403 report, evidence, W404 cooperation |
+| 6 | `.trinity/experience.md` | W403 learnings |
+| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1307, open #W404 |
 
 ---
 
@@ -41,12 +41,12 @@ See `.claude/plans/wave-loop-402.md` for the full work breakdown.
 - [ ] AC-A1 (Variant A): a physical CCLK trace is captured and the dominant
       frequency is recorded.
 - [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.5 contains the measured value.
-- [ ] AC-B1 (Variant B): new Lean 4 module builds and links `STAT` decoding to the
+- [ ] AC-B1 (Variant B): new Lean 4 lemmas link canonical bitstream config to the
       documented decision trees.
 - [ ] AC-C1 (Variant C): `tri fpga smoke-gate --require-cable` reaches
       `DONE=HIGH` on the bench.
 - [ ] AC-D1: `./scripts/tri test` passes.
-- [ ] AC-D2: W402 report + evidence + W403 cooperation variants committed.
+- [ ] AC-D2: W403 report + evidence + W404 cooperation variants committed.
 
 ---