gHashTag · gHashTag · Jul 4, 2026 · Jul 4, 2026
@@ -0,0 +1,109 @@
+# Wave Loop 404 Plan — FPGA: close physical CCLK measurement or extend formal CCLK bounds
+
+**Issue:** [#1309](https://github.com/t27/t27/issues/1309)  
+**Branch:** `trinity-rust-rings`  
+**Date:** 2026-07-06  
+**Anchor:** φ² + φ⁻² = 3 | TRINITY
+
+---
+
+## Context
+
+W403 closed without bench hardware by extending the Lean 4 model with the
+`BitstreamConfig` canonical predicate and `ColdPOR` linkage lemmas. At the start
+of W404 the attached Digilent FTDI cable and XC7A200T board were found to be
+reachable (`openFPGALoader --detect` returned idcode `0x3636093`), so the
+wave executed **Variant C** — a cable-connected SRAM smoke load in `tri fpga
+smoke-gate --require-cable`. Variant A (P12 CCLK measurement) remains blocked
+because no logic analyzer / oscilloscope is available.
+
+---
+
+## Weak points
+
+1. **Physical CCLK measurement still blocked.** A Digilent FTDI cable and the
+   XC7A200T board are connected, but no logic analyzer / oscilloscope is
+   available for pin P12 capture. The agent can drive JTAG but cannot sample
+   the analog CCLK waveform autonomously.
+2. **Operator-dependent capture.** A logic-analyzer/oscilloscope capture
+   requires human bench time; the agent cannot perform it autonomously.
+3. **Cable detection fragility.** The `--require-cable` path depends on
+   `openFPGALoader --detect` successfully returning an `idcode` line. If the
+   board is powered off or the cable is swapped, the gate fails cleanly but
+   cannot self-heal.
+4. **Competitor formal-HDL pressure.** Verilean / Sparkle HDL and Aria-HDL can
+   produce timing/properties claims; t27 must keep adding traceability layers
+   (formal → spec → generated code → physical measurement) to stay ahead.
+
+---
+
+## Competitor scan
+
+- **Verilean / Sparkle HDL:** Lean 4-based HDL with embedded proofs. Closest
+  formal competitor. Their strength is correctness of generated hardware;
+  t27's differentiation is the spec-first `t27`/`tri` pipeline plus physical
+  FPGA evidence.
+- **Aria-HDL:** meta-compiler with Lean 4 backend. Focuses on compiling
+  existing HDL to verified code, not on the physical bring-up traceability chain.
+- **seLe4n:** Lean 4 microkernel. Relevant only to secure-boot claims, not
+  directly to FPGA CCLK measurement.
+- **USENIX WOOT 2024 Zynq secure-boot paper:** shows that bitstream config
+  fields matter for security; t27's formal config audit is a defensive parallel.
+- **FIRRTL/Chisel/Clash/Bluespec:** no formal proof of FPGA boot timing or
+  STAT-register outcomes in their standard flows.
+
+---
+
+## Cooperation variants
+
+See `docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md` for the pre-implementation
+variants. The implemented wave chose **Variant C** because the Digilent cable
+and XC7A200T board were detected; Variant A remains blocked by the lack of a
+logic analyzer / oscilloscope.
+
+### Variant A — Physical CCLK measurement (deferred)
+
+Capture CCLK on P12, run `tri fpga measure-cclk --csv`, and record the
+frequency/duty cycle in `fpga/HARDWARE_SSOT.md` §3.5. Deferred to W405 unless
+hardware becomes available.
+
+### Variant B — Formal `OSCFSEL`/CCLK bounds (not executed)
+
+Add `OSCFSEL` value constants and a `cclk_within_flash_spec` predicate to
+`TernaryFPGABoot.lean`; prove that the canonical config implies the N25Q128
+read timing is satisfied under published Artix-7 startup-clock tables. This
+remains a candidate for a future no-hardware wave.
+
+### Variant C — `--require-cable` SRAM smoke load (implemented)
+
+Extend `tri fpga smoke-gate` to detect the Digilent cable and, when present,
+load the GF16 matrix into SRAM and assert `DONE=HIGH`. Verified on the bench:
+- `openFPGALoader --detect -c digilent_hs2` returns idcode `0x3636093`.
+- `tri fpga load-sram` completes with `done 1`.
+- Post-load STAT = `0x401079FC`, matching `Trinity.StatRegister.boot_success`.
+
+---
+
+## Acceptance criteria
+
+| ID | Criterion | Status |
+|----|-----------|--------|
+| AC-A1 | Physical CCLK trace captured on P12. | ⏸️ deferred |
+| AC-A2 | `fpga/HARDWARE_SSOT.md` §3.5 contains measured value. | ⏸️ deferred |
+| AC-B1 | New Lean 4 lemmas link `OSCFSEL`/CCLK bounds to decision trees. | ⏸️ not executed |
+| AC-C1 | `tri fpga smoke-gate --require-cable` reaches `DONE=HIGH` on the bench. | ✅ |
+| AC-D1 | `./scripts/tri test` passes. | ✅ |
+| AC-D2 | W404 report + evidence + W405 cooperation variants committed. | ✅ |
+
+---
+
+## Chosen variant
+
+**Variant C** — because the Digilent FTDI cable and XC7A200T board are
+connected and reachable, making the hardware smoke gate the highest-leverage
+close-out for W404. Variant A remains the next priority once a logic analyzer
+or oscilloscope is available.
+
+---
+
+*φ² + φ⁻² = 3 | TRINITY*
@@ -1,38 +1,39 @@
-# Wave Loop 403 — FPGA: close physical CCLK measurement or extend formal/physical smoke coverage
+# Wave Loop 404 — FPGA: close physical CCLK measurement or extend formal CCLK bounds
 
-**Issue:** #1307  
+**Issue:** #1309  
 **Branch:** `trinity-rust-rings`  
-**Milestone:** W402 formalized the cold-POR decision tree in Lean 4. W403 should
-close the remaining physical AC or extend formal/physical smoke coverage.
+**Milestone:** W403 extended the Lean 4 bitstream-config model. W404 should
+close the remaining physical AC or extend formal 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 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).
+2. OR extend the Lean 4 model with `OSCFSEL` variants / CCLK frequency-bound
+   predicates and prove the canonical config is timing-safe (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 W404 cooperation variants.
+4. Update close-out reports and open W405 cooperation variants.
 
 ---
 
 ## Decomposed plan
 
-See `.claude/plans/wave-loop-403.md` for the full work breakdown.
+See `docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md` for the full cooperation
+variants.
 
 | Step | File(s) | Deliverable |
 |------|---------|-------------|
-| 1 | `.claude/plans/wave-loop-403.md` | Decomposed plan + weak-point + competitor scan |
+| 1 | `.claude/plans/wave-loop-404.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) | Bitstream-config lemmas |
+| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | OSCFSEL/CCLK-bound lemmas |
 | 4 | `cli/tri/src/fpga.rs` (Variant C) | Optional cable-connected SRAM smoke load |
-| 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 |
+| 5 | `docs/reports/*` | W404 report, evidence, W405 cooperation |
+| 6 | `.trinity/experience.md` | W404 learnings |
+| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1309, open #W405 |
 
 ---
 
@@ -41,12 +42,12 @@ See `.claude/plans/wave-loop-403.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 lemmas link canonical bitstream config to the
+- [ ] AC-B1 (Variant B): new Lean 4 lemmas link `OSCFSEL`/CCLK bounds 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: W403 report + evidence + W404 cooperation variants committed.
+- [ ] AC-D2: W404 report + evidence + W405 cooperation variants committed.
 
 ---
 

@@ -1368,3 +1368,27 @@
 - **Commit:** Merge branch 'master' into trinity-rust-rings for W403 (Closes #1307)
 - **Files:** .claude/plans/wave-loop-403.md,.trinity/current-issue.md,.trinity/current_task/activity.md,.trinity/experience.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-06.md,docs/reports/WAVE_LOOP_403_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
 
+## 2026-07-04T09:16:11Z — trinity-rust-rings
+- **Commit:** feat(igla): Wave Loop 403 — bitstream config linked to cold-POR decision tree in Lean 4 (Closes #1307)
+- **Files:** .trinity/current-issue.md
+
+## 2026-07-04T09:16:34Z — trinity-rust-rings
+- **Commit:** chore(trinity): point current-issue.md to W404 issue #1309
+- **Files:** .claude/plans/wave-loop-404.md
+
+## 2026-07-04T09:29:40Z — trinity-rust-rings
+- **Commit:** docs(trinity): add decomposed W404 plan with weak points and competitor scan (Closes #1309)
+- **Files:** .claude/plans/wave-loop-404.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-07.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-07.md,docs/reports/WAVE_LOOP_404_REPORT.md,fpga/HARDWARE_SSOT.md
+
+## 2026-07-04T09:30:41Z — trinity-rust-rings
+- **Commit:** feat(igla): Wave Loop 404 — hardware smoke-gate --require-cable for FPGA SRAM load (Closes #1309)
+- **Files:** .claude/plans/wave-loop-404.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_2026-07-07.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-07.md,docs/reports/WAVE_LOOP_404_REPORT.md,fpga/HARDWARE_SSOT.md
+
+## 2026-07-04T09:42:42Z — trinity-rust-rings
+- **Commit:** feat(igla): Wave Loop 404 — hardware smoke-gate --require-cable for FPGA SRAM load (Closes #1309)
+- **Files:** docs/NOW.md
+
+## 2026-07-04T09:43:49Z — trinity-rust-rings
+- **Commit:** feat(igla): Wave Loop 404 — hardware smoke-gate --require-cable for FPGA SRAM load (Closes #1309)
+- **Files:** docs/NOW.md
+
@@ -1,5 +1,51 @@
 # t27 / Trinity Agent Experience Log
 
+## 2026-07-06 — Wave Loop 404 (Hardware smoke-gate `--require-cable`)
+
+### What worked
+- Checking the bench before choosing the variant changed the wave outcome: the
+  Digilent FTDI cable and XC7A200T board were reachable, so **Variant C**
+  (hardware smoke gate) became feasible instead of another no-hardware formal
+  extension.
+- Keeping `--require-cable` as an **optional** flag preserved the board-less
+  default path. CI without a cable still passes all static checks; a runner
+  with hardware can opt into the SRAM load assertion.
+- Reusing the existing `load_sram` and `capture_stat` helpers kept the change
+  small and avoided duplicating openFPGALoader parsing logic.
+- Asserting the same `boot_success` conditions used by the Lean model
+  (`DONE=1`, `MODE=0b001`, no CRC/ID/DEC errors) links the hardware smoke gate
+  directly to the formal predicates.
+- On the bench: `openFPGALoader --detect` returned idcode `0x3636093`, SRAM
+  load completed with `done 1`, and post-load STAT matched `0x401079FC`.
+- Conformance suite: **576/576 PASS**.
+
+### What changed behavior
+- `cli/tri/src/fpga.rs`: `FpgaCmd::SmokeGate` now accepts `--require-cable`,
+  `--cable`, and `--part`. When `--require-cable` is set, the gate runs
+  `cable_detected`, `load_sram`, `capture_stat`, and `assert_stat_boot_success`
+  before the existing board-less checks.
+- `fpga/HARDWARE_SSOT.md` §3.2 now references the hardware smoke traceability.
+- `docs/NOW.md` updated with the W404 entry.
+- Close-out artifacts: `docs/reports/WAVE_LOOP_404_REPORT.md`,
+  `FPGA_LOOP_EVIDENCE_2026-07-07.md`, and
+  `FPGA_LOOP_COOPERATION_2026-07-07.md`.
+
+### Patterns to reuse
+- Probe hardware availability at the start of a wave; it can change which
+  variant is highest leverage.
+- Add optional hardware gates as `--require-<resource>` flags so board-less CI
+  stays green while physical evidence can be collected when a resource is present.
+- Reuse existing command helpers (`load_sram`, `capture_stat`) instead of
+  spawning openFPGALoader ad-hoc; this keeps parsing and error handling
+  consistent.
+
+### Anti-patterns to avoid
+- Do not make a hardware gate mandatory unless the normal CI environment is
+  guaranteed to have the resource. A broken cable should fail the specific
+  check, not the whole pipeline.
+- Do not skip the board-less path when adding hardware coverage; the static
+  audit is still the regression barrier that runs on every PR.
+
 ## 2026-07-05 — Wave Loop 403 (Bitstream config linked to cold-POR decision tree)
 
 ### What worked

@@ -217,13 +217,26 @@ pub enum FpgaCmd {
     ///
     /// Asserts the canonical 200T configuration: IDCODE 0x03636093, SPI x1,
     /// CCLK startup, OSCFSEL=0, and no CRC register writes.
+    ///
+    /// With `--require-cable`, also detect the Digilent FTDI cable, load the
+    /// bitstream into FPGA SRAM via openFPGALoader, and assert DONE=HIGH.
     SmokeGate {
         /// Bitstream to audit (default: fpga/verilog/ternary_mac_demo_top_200t.bit).
         #[arg(long)]
         bit: Option<PathBuf>,
         /// Verilog top module to synthesize (default: ternary_mac_demo_top).
         #[arg(long, default_value = "ternary_mac_demo_top")]
         top: String,
+        /// Require a connected Digilent cable and load the bitstream into SRAM.
+        /// If no device is detected, the gate fails. Board-less checks still run.
+        #[arg(long)]
+        require_cable: bool,
+        /// openFPGALoader cable profile for the cable-connected check.
+        #[arg(long, default_value = "digilent_hs2")]
+        cable: String,
+        /// FPGA part/package for openFPGALoader (default: xc7a200tfgg676).
+        #[arg(long, default_value = "xc7a200tfgg676")]
+        part: String,
     },
     /// Print or interactively confirm the cold-POR boot protocol. This is the
     /// standalone version of the instructions embedded in `boot-log` and
@@ -524,7 +537,13 @@ pub fn run(cmd: &FpgaCmd) -> Result<()> {
             wait_seconds,
             log_dir,
         } => boot_log(bit, cable, part, bridge.as_ref(), *freq, *repeat, *wait_seconds, log_dir.as_ref()),
-        FpgaCmd::SmokeGate { bit, top } => smoke_gate(bit.as_ref(), top),
+        FpgaCmd::SmokeGate {
+            bit,
+            top,
+            require_cable,
+            cable,
+            part,
+        } => smoke_gate(bit.as_ref(), top, *require_cable, cable, part),
         FpgaCmd::BootProtocol { checklist } => boot_protocol(*checklist),
         FpgaCmd::PatchCor0 { bit, out, oscfsel } => patch_cor0(bit, out, *oscfsel),
         FpgaCmd::CclkVariants { bit, output_dir, values } => {
@@ -2636,15 +2655,86 @@ fn boot_log(
     }
 }
 
-fn smoke_gate(bit: Option<&PathBuf>, top: &str) -> Result<()> {
+/// Detect whether a target FPGA is reachable on the given openFPGALoader
+/// cable profile. Returns false when the chain is empty / cable missing.
+fn cable_detected(cable: &str) -> bool {
+    let Ok((_, Some(output))) = run_openfpgaloader(cable, &["--detect"], true) else {
+        return false;
+    };
+    output.contains("idcode")&& output.contains("manufacturer")
+}
+
+/// Assert that the decoded STAT register shows a successful boot/config.
+fn assert_stat_boot_success(bits: &StatBits, ctx: &str) -> Result<()> {
+    if !bits.done {
+        bail!("{}: DONE=LOW (raw=0x{:08X}, {})", ctx, bits.raw, bits.diagnose());
+    }
+    if bits.mode != 0b001 {
+        bail!(
+            "{}: MODE=0b{:03b} != 0b001 (Master SPI x1)",
+            ctx,
+            bits.mode
+        );
+    }
+    if bits.crc_error {
+        bail!("{}: CRC_ERROR=1", ctx);
+    }
+    if bits.id_error {
+        bail!("{}: ID_ERROR=1", ctx);
+    }
+    if bits.dec_error {
+        bail!("{}: DEC_ERROR=1", ctx);
+    }
+    Ok(())
+}
+
+fn smoke_gate(
+    bit: Option<&PathBuf>,
+    top: &str,
+    require_cable: bool,
+    cable: &str,
+    part: &str,
+) -> Result<()> {
     let root = repo_root()?;
     let bit_path = bit.cloned().unwrap_or_else(|| {
         root.join("fpga")
             .join("verilog")
             .join("ternary_mac_demo_top_200t.bit")
     });
 
-    println!("== FPGA board-less smoke gate ==");
+    println!("== FPGA smoke gate ==");
+
+    // Cable-connected hardware check (optional, gated by --require-cable).
+    if require_cable {
+        println!("[smoke-gate] require-cable: detecting FPGA via {}...", cable);
+        if !cable_detected(cable) {
+            bail!(
+                "no FPGA detected on cable {} (is the board powered and connected?)",
+                cable
+            );
+        }
+        println!("[smoke-gate] cable OK (FPGA detected)");
+
+        if !bit_path.is_file() {
+            bail!(
+                "bitstream not found at {} (required for --require-cable)",
+                bit_path.display()
+            );
+        }
+
+        println!(
+            "[smoke-gate] loading SRAM: {}",
+            bit_path.display()
+        );
+        load_sram(&bit_path, cable, part, false, false)?;
+
+        println!("[smoke-gate] reading STAT after SRAM load...");
+        let samples = capture_stat(cable, false, 1)?;
+        let bits = samples.first().cloned().expect("at least one STAT sample");
+        assert_stat_boot_success(&bits, "SRAM load")
+            .with_context(|| "hardware smoke-gate failed after SRAM load")?;
+        println!("[smoke-gate] hardware check OK (DONE=HIGH, mode=001, no errors)");
+    }
 
     // 1. bit-config audit if the bitstream exists.
     if bit_path.is_file() {