gHashTag · gHashTag · Jul 4, 2026 · Jul 4, 2026
@@ -0,0 +1,99 @@
+# Wave Loop 406 — CCLK measurement + formal timing-safety (variants A/B/C)
+
+**Issue:** #1313  
+**Branch:** `wave-loop-406`  
+**Milestone:** W405 closed the flash-boot cold-POR smoke gate. W406 should close
+one of the remaining gaps: real CCLK measurement on P12, fully automated
+cold-POR, or formal OSCFSEL/CCLK timing-safety in Lean 4.
+
+---
+
+## Goal
+
+1. **Variant A** — Capture the actual CCLK frequency/duty cycle on pin P12 and
+   record it in `fpga/HARDWARE_SSOT.md` §3.6.
+2. **Variant B** — Automate the cold-POR flash-boot smoke gate with a relay
+   power switch and isolated JTAG cable so no operator is required.
+3. **Variant C** — Extend the Lean 4 model with `OSCFSEL` constants, nominal
+   CCLK ranges, and a `cclk_within_flash_spec` predicate; prove the canonical
+   config is timing-safe.
+
+Default recommendation: **Variant A + C bundle** (measurement + formal claim).
+If the bench has no logic analyzer wired to P12 when implementation starts,
+Variant A becomes "live-capture infrastructure + manual CSV evidence" and the
+formal Variant C is still deliverable.
+
+---
+
+## Weak points investigated
+
+| Weak point | Risk | How this wave addresses it |
+|---|---|---|
+| We do not know the real CCLK frequency of the default bitstream | Competitors can ask "how fast is CCLK?" and we cannot answer with data | Variant A measures P12; Variant C bounds it formally; together they close the question |
+| `tri fpga measure-cclk` only parses CSV, it cannot drive a live capture | Operator has to use a separate GUI and remember export format | Add `--live` mode that drives `sigrok-cli` with the connected FTDI/DSLogic analyzer |
+| CSV parser only handles analog `Time,Voltage`; sigrok logic exports are `logic` + `Samplerate` | Live capture output cannot be parsed | Extend parser to support logic-analyzer CSV and compute freq/duty from samples |
+| Formal model assumes `STARTUPCLK=CCLK` but does not quantify it | Timing-safety claim is incomplete | Variant C adds published Artix-7 `OSCFSEL` tables as axiomatic bounds and links them to the N25Q128 spec |
+| No validation that measured CCLK is inside the flash spec | A "works on my bench" value may be marginal across temp/voltage/process | Add `--validate` to `measure-cclk` and a Lean `cclk_within_flash_spec` predicate |
+| Flash-boot smoke gate still needs a human operator | Cannot run in CI without physical intervention | Variant B removes the operator with relay + isolated JTAG (fallback if scope limited) |
+
+---
+
+## Competitor scan
+
+| Competitor / project | Relevant capability | t27 differentiator after this wave |
+|---|---|---|
+| Verilean | Lean 4 hardware proofs | t27 links `cclk_within_flash_spec` to a real `OSCFSEL=0` bitstream and, when wired, to a measured CCLK on real silicon |
+| Sparkle HDL | End-to-end formal + simulation | t27 has physical evidence plus a model, not just simulation |
+| openFPGALoader ecosystem | Tooling for flash / SRAM load | t27 wraps it with formal traceability, evidence reports, and timing validation |
+| Project Trellis / nextpnr | Open-source bitstream tooling | t27 focuses on Artix-7 boot verification and timing-safety, not place-and-route |
+
+The strongest defensive move is to deliver **Variant A + C together**: a
+published measurement and a formal claim form a traceability stack that is hard
+to reproduce. If bench wiring is not available during this wave, the formal
+Variant C still advances the model and prepares the measurement path for W407.
+
+---
+
+## Decomposed plan
+
+| Step | File(s) | Deliverable |
+|---|---|---|
+| 1 | `.claude/plans/wave-loop-406.md` | Decomposed plan + weak-point + competitor scan |
+| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant C) | `OSCFSEL` constants, nominal CCLK lookup, N25Q128 spec, `cclk_within_flash_spec`, proof for `OSCFSEL=0` |
+| 3 | `cli/tri/src/fpga.rs` (Variant A) | `tri fpga measure-cclk --live` using `sigrok-cli` + `ftdi-la` / `dreamsourcelab-dslogic`; logic-CSV parsing; `--validate` against flash spec |
+| 4 | `cli/tri/src/fpga.rs` | Unit tests for logic-CSV parsing and validation |
+| 5 | `fpga/HARDWARE_SSOT.md` §3.6 | CCLK spec, measurement procedure, expected value range |
+| 6 | `docs/reports/*` | W406 report, evidence, W407 cooperation |
+| 7 | `.trinity/experience.md` | W406 learnings |
+| 8 | git/PR | squash-merge to master, close #1313, open #W407 |
+
+---
+
+## Acceptance criteria
+
+- [x] AC-A1 (Variant A): a CCLK capture is attempted live; the dominant frequency
+      is deferred to W407 because P12 is not wired to a logic-analyzer channel.
+      A CSV fallback is documented in §3.6.3.
+- [x] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.6 contains the expected nominal
+      value (2.5 MHz for `OSCFSEL=0`) and the validation range (100 kHz–50 MHz).
+- [x] AC-A3 (Variant A): `tri fpga measure-cclk --live` drives `sigrok-cli` and
+      returns structured frequency/duty output.
+- [x] AC-C1 (Variant C): new Lean 4 lemmas link `OSCFSEL`/CCLK bounds to the
+      cold-POR predicate and prove `cclk_within_flash_spec 0`.
+- [x] AC-D1: `./scripts/tri test` passes.
+- [x] AC-D2: `lake build Trinity.TernaryFPGABoot` passes.
+- [x] AC-D3: W406 report + evidence + W407 cooperation variants committed.
+
+---
+
+## Default variant
+
+**Variant A + C bundle**. The bench has a Digilent FTDI cable that `sigrok-cli`
+sees as `ftdi-la`, so live capture infrastructure is buildable. If P12 is not
+wired when the code is ready, capture a CSV manually in DSView and commit it as
+evidence. The formal Variant C does not depend on hardware and closes the
+timing-safety gap regardless.
+
+---
+
+*phi^2 + phi^-2 = 3 | TRINITY*
@@ -1,68 +1,72 @@
-# Wave Loop 405 — FPGA boot loop closure (variant A/B/C)
+# Wave Loop 407 — close the CCLK measurement gap or deepen formal timing safety
 
-**Issue:** #1311  
-**Branch:** `wave-loop-405`  
-**Milestone:** W404 closed the SRAM hardware smoke gate. W405 should close one
-of the remaining gaps: real CCLK measurement, flash-boot cold-POR gate, or
-formal CCLK timing-safety.
+**Issue:** #1315  
+**Branch:** `wave-loop-407` (to be created)  
+**Milestone:** W406 added live CCLK capture infrastructure and formal
+OSCFSEL/CCLK timing safety in Lean 4. W407 should pick one of the remaining
+next steps: a real CCLK measurement on P12, full cold-POR automation, or deeper
+SPI flash timing formalization.
 
 ---
 
 ## Goal
 
-1. **Variant A** — Capture the actual CCLK frequency/duty cycle on pin P12 and
-   record it in `fpga/HARDWARE_SSOT.md` §3.5.
-2. **Variant B** — Extend `tri fpga smoke-gate --require-cable` to flash boot:
-   program flash, prompt for power-cycle, capture cold-POR STAT, assert
-   `boot_success`.
-3. **Variant C** — Extend the Lean 4 model with `OSCFSEL` constants, nominal
-   CCLK ranges, and a `cclk_within_flash_spec` predicate; prove the canonical
-   config is timing-safe.
-4. Update close-out reports and open W406 cooperation variants.
+1. **Variant A** — Complete the real CCLK measurement on pin P12 during
+   cold-POR from flash and record it in `fpga/HARDWARE_SSOT.md` §3.6.
+2. **Variant B** — Automate the cold-POR flash-boot smoke gate with a relay
+   power switch and isolated/tri-stateable JTAG cable so no operator is
+   required.
+3. **Variant C** — Extend the Lean 4 model with additional Micron N25Q128_3V
+   timing constraints (CS# high, clock low/high, wake-up) and link them to the
+   cold-POR predicate.
+
+Default recommendation: **Variant A + C bundle** (measurement + deeper formal
+timing claim). If P12 is still unwired, Variant A becomes "manual CSV evidence"
+and Variant C remains fully deliverable.
 
 ---
 
 ## Decomposed plan
 
-See `.claude/plans/wave-loop-405.md` for the full weak-point / competitor scan
-and detailed decomposition.
+See `.claude/plans/wave-loop-406.md` for the W406 close-out and
+`docs/reports/FPGA_LOOP_COOPERATION_2026-07-12.md` for the full W407 variants.
 
 | Step | File(s) | Deliverable |
-|------|---------|-------------|
-| 1 | `.claude/plans/wave-loop-405.md` | Decomposed plan + weak-point + competitor scan |
-| 2 | `fpga/HARDWARE_SSOT.md` (Variant A) | Measured CCLK frequency/duty cycle on P12 |
-| 3 | `cli/tri/src/fpga.rs` (Variant B) | `--flash-boot` flag + program/reset/capture flow |
-| 4 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant C) | OSCFSEL/CCLK-bound lemmas |
-| 5 | `docs/reports/*` | W405 report, evidence, W406 cooperation |
-| 6 | `.trinity/experience.md` | W405 learnings |
-| 7 | git/PR | squash-merge to master, close #1311, open #W406 |
+|---|---|---|
+| 1 | `.claude/plans/wave-loop-407.md` | Decomposed plan + weak-point + competitor scan |
+| 2 | `fpga/HARDWARE_SSOT.md` §3.6 (Variant A) | Measured CCLK frequency/duty cycle on P12 |
+| 3 | `cli/tri/src/fpga.rs` (Variant A/B) | Optional live-capture hardening or auto-power-cycle trait |
+| 4 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant C) | CS-high / SCK duty / wake-up lemmas |
+| 5 | `docs/reports/*` | W407 report, evidence, W408 cooperation |
+| 6 | `.trinity/experience.md` | W407 learnings |
+| 7 | git/PR | squash-merge to master, close #1315, open #W408 |
 
 ---
 
 ## Acceptance criteria
 
-- [ ] AC-A1 (Variant A): a physical CCLK trace is captured and the dominant
+- [ ] AC-A1 (Variant A): a real CCLK capture CSV exists and the dominant
       frequency is recorded.
-- [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.5 contains the measured value.
-- [ ] AC-B1 (Variant B): `tri fpga smoke-gate --require-cable --flash-boot`
-      programs flash and asserts `boot_success` after a cold POR.
-- [ ] AC-C1 (Variant C): new Lean 4 lemmas link `OSCFSEL`/CCLK bounds to the
-      documented decision trees.
+- [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.6 contains the measured
+      frequency ± tolerance and duty cycle.
+- [ ] AC-A3 (Variant A): `tri fpga measure-cclk --live ... --validate` passes.
+- [ ] AC-B1 (Variant B): `tri fpga smoke-gate --flash-boot --auto-power-cycle`
+      runs the cold-POR gate without operator intervention.
+- [ ] AC-C1 (Variant C): new Lean 4 lemmas link CS# / SCK / wake-up bounds to
+      the cold-POR predicate for `OSCFSEL=0`.
 - [ ] AC-D1: `./scripts/tri test` passes.
-- [ ] AC-D2: W405 report + evidence + W406 cooperation variants committed.
+- [ ] AC-D2: `lake build Trinity.TernaryFPGABoot` passes.
+- [ ] AC-D3: W407 report + evidence + W408 cooperation variants committed.
 
 ---
 
 ## Default variant
 
-The bench cable and board are reachable, so the recommended default is
-**Variant B** (flash-boot cold-POR smoke gate). It directly extends the W404
-SRAM gate and closes the boot loop end-to-end.
-
-If the manual power-cycle step proves too awkward, fall back to **Variant C**
-(no hardware) and pursue Variant B in W406. If a logic analyzer / oscilloscope
-becomes available before implementation starts, switch to **Variant A**.
+**Variant A + C bundle**. The live-capture infrastructure from W406 is ready;
+once P12 is wired to a logic-analyzer channel, the actual frequency can be
+captured and the deeper formal timing model can be proved against the same
+silicon anchor.
 
 ---
 
-*φ² + φ⁻² = 3 | TRINITY*
+*phi^2 + phi^-2 = 3 | TRINITY*
@@ -1400,3 +1400,11 @@
 - **Commit:** docs(wave-loop-405): set up W405 issue pointer and decomposed plan (refs #1311)
 - **Files:** .claude/plans/wave-loop-405.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-10.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-10.md,docs/reports/WAVE_LOOP_405_REPORT.md
 
+## 2026-07-04T11:10:30Z — wave-loop-406
+- **Commit:** feat(igla): Wave Loop 405 — flash-boot cold-POR smoke gate
+- **Files:** .claude/plans/wave-loop-406.md,.trinity/current-issue.md
+
+## 2026-07-04T11:31:40Z — wave-loop-406
+- **Commit:** docs(w406): W406 plan and current-issue for CCLK measurement + formal timing-safety
+- **Files:** .claude/plans/wave-loop-406.md,.trinity/current-issue.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-12.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-12.md,docs/reports/WAVE_LOOP_406_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
+
@@ -1,5 +1,61 @@
 # t27 / Trinity Agent Experience Log
 
+## 2026-07-12 — Wave Loop 406 (CCLK measurement + OSCFSEL/CCLK timing safety in Lean 4)
+
+### What worked
+- Adding an axiomatic `cclk_nominal_hz` lookup and `N25Q128_MAX_SCK_HZ` flash spec to
+  `TernaryFPGABoot.lean` closed the quantitative gap in the cold-POR formal model.
+  `cclk_within_flash_spec` now links `OSCFSEL` to the Micron standard-read timing
+  bound (≤ 50 MHz) and is integrated into `cold_por_spi_flash_pred`.
+- Extending `tri fpga measure-cclk` with a `--live` path that drives `sigrok-cli`
+  and parses exported logic CSV gives a repeatable way to verify nominal CCLK
+  against the same flash bound, not just a manual spreadsheet.
+- Keeping the measurement command board-less (CSV) by default and opt-in (`--live`)
+  preserves CI while enabling bench evidence when the P12 wiring is ready.
+- The W405 `cclk_sweep` gate was already sufficient to prove cold-POR success; W406
+  adds the *formal reason* the CCLK rate itself is safe, which is the remaining
+  half of the boot-verification gap.
+
+### What changed behavior
+- `proofs/lean4/Trinity/TernaryFPGABoot.lean`: added `OSCFSEL_COUNT`,
+  `OSCFSEL_MAX`, `cclk_nominal_hz`, `N25Q128_MAX_SCK_HZ`,
+  `N25Q128_MIN_CS_HIGH_NS`, and `cclk_within_flash_spec`. Three theorems connect
+  the canonical config, any canonical config, and the cold-POR predicate to the
+  flash spec.
+- `proofs/lean4/Trinity/TernaryFPGABoot.lean`: `cold_por_spi_flash_pred` now
+  requires `BitstreamConfig.cclk_within_flash_spec p.cfg.oscfsel`.
+- `cli/tri/src/fpga.rs`: `FpgaCmd::MeasureCclk` now accepts `--live`, `--driver`,
+  `--channel`, `--samplerate`, `--samples`, and `--validate`. Added live capture
+  through `sigrok-cli`, logic CSV parsing, frequency/period estimation, and
+  flash-spec validation.
+- `fpga/HARDWARE_SSOT.md` §3.6 updated with nominal CCLK table, live-capture
+  protocol, CSV parsing rules, and formal traceability to
+  `BitstreamConfig.cclk_within_flash_spec`.
+- `docs/NOW.md` updated with the W406 entry.
+- Close-out artifacts: `docs/reports/WAVE_LOOP_406_REPORT.md`,
+  `FPGA_LOOP_EVIDENCE_2026-07-12.md`, and
+  `FPGA_LOOP_COOPERATION_2026-07-12.md`.
+
+### Patterns to reuse
+- When a physical quantity is implicit in a formal model, expose it as a lookup
+  table + spec constant + predicate; then prove that the concrete/default case
+  satisfies the predicate. This makes the model auditable without over-fitting
+  to one board.
+- Bridge bench tooling and formal models through a single CLI subcommand that
+  accepts both recorded CSV (offline) and live logic-analyzer capture (online)
+  so the same validation predicate can be evaluated on either data source.
+- Document the *blocking hardware precondition* (P12 → logic analyzer channel)
+  explicitly in the report and cooperation variants rather than silently leaving
+  the measurement at zero.
+
+### Anti-patterns to avoid
+- Do not let a CLI live-capture helper swallow the underlying tool error. The
+  first implementation masked `sigrok-cli` failures; surfacing `stderr` in the
+  `anyhow` error made the "no transitions" case immediately interpretable.
+- Do not add new formal constants without a corresponding test/theorem; the
+  `canonical_oscfsel_within_flash_spec` `decide` theorem catches lookup-table
+  typos at build time.
+
 ## 2026-07-04 — Wave Loop 405 (Hardware smoke-gate `--flash-boot`)
 
 ### What worked