Wave Loop 409 — per-OSCFSEL SPI transaction lookup + tighter duty bound

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

@@ -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*

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

@@ -0,0 +1,112 @@
+# Wave Loop 407 — deeper SPI flash timing safety + synthetic CCLK validation (variants A/B/C)
+
+**Issue:** #1316  
+**Branch:** `wave-loop-407`  
+**Milestone:** W406 added live CCLK capture infrastructure and formal
+OSCFSEL/CCLK timing safety in Lean 4. W407 closes the remaining timing gaps
+and hardens the CLI validation pipeline so it can be exercised without a wired
+P12 probe.
+
+---
+
+## Goal
+
+1. **Variant A** — Complete the real CCLK measurement on pin P12 and record it
+   in `fpga/HARDWARE_SSOT.md` §3.6. This is still blocked by the missing P12 →
+   logic-analyzer wire on the bench, so for W407 it becomes: (a) a synthetic CSV
+   fixture that exercises the entire `tri fpga measure-cclk --csv --validate`
+   pipeline, and (b) documentation of the exact wiring needed for a real
+   capture.
+2. **Variant B** — Fully automate the cold-POR flash-boot smoke gate with a
+   relay power switch and isolated/tri-stateable JTAG cable. Deferred to W408
+   because the relay hardware is not on the bench and the W405 manual path is
+   still reproducible.
+3. **Variant C** — Extend the Lean 4 model with additional Micron N25Q128_3V
+   timing constraints (CS# high, SCK low/high, wake-up) and prove that the
+   canonical `OSCFSEL=0` configuration satisfies them. This is the primary
+   deliverable of W407.
+
+Default recommendation for this wave: **Variant C + synthetic Variant A**.
+The formal extension closes the timing-safety argument; the synthetic fixture
+lets CI validate the measurement/validation pipeline even when P12 is
+unconnected.
+
+---
+
+## Weak points investigated
+
+| Weak point | Risk | How this wave addresses it |
+|---|---|---|
+| Formal model only bounds CCLK frequency, not CS# / SCK duty / wake-up | Competitors can say "frequency is only half the SPI timing story" | Variant C adds N25Q128 CS# high, SCK low/high, and wake-up constants; defines `flash_spi_timing_ok` and proves it for the canonical config |
+| No fixture to test `measure-cclk` validation without a live board | The `--validate` path is only exercised when P12 is wired | Synthetic CSV fixture (2.5 MHz square wave) plus unit tests for `parse_logic_csv` exercise the pipeline in CI |
+| `cold_por_spi_flash_pred` conflates static config and dynamic STAT observations | CS# timing is a property of the bitstream + flash, not the STAT register | Split into static `flash_spi_timing_ok` (config only) and retain the link via a separate lemma |
+| Live CCLK is only active during configuration (100 µs–1 ms after POR) | A naive `sigrok-cli` capture may miss the window entirely | Document the trigger/timing requirement in HARDWARE_SSOT.md and record a TODO for integrating capture with the cold-POR power-cycle step |
+| No empirical duty-cycle validation | Even if frequency is safe, a 10%/90% duty cycle could violate SCK low/high limits | `--validate` will also check duty cycle once the synthetic fixture proves the parser computes it correctly |
+| Competitors (Verilean/Sparkle, prjxray, OpenTitan) have deeper formal stories | t27 needs a complete board-grounded timing stack | W407 delivers a full set of N25Q128 timing constants, machine-checked proofs, and a CI-runnable validation fixture |
+
+---
+
+## Competitor scan
+
+See also the detailed scan in `docs/reports/WAVE_LOOP_406_REPORT.md` §4. The
+key competitors and how W407 differentiates:
+
+| Competitor / project | Relevant capability | t27 differentiator after W407 |
+|---|---|---|
+| Verilean / Sparkle HDL | Lean 4 HDL compiler + cycle-accurate simulation | t27 does not design RTL in Lean; it formalizes a *vendor* 7-series boot interface (OSCFSEL→CCLK, N25Q128 CS/SCK/wake-up) and links it to physical cold-POR evidence |
+| VerilLean | Verilog module verification in Lean 4 | t27 targets system-level boot protocol: STAT decoding, cold-POR decision tree, CCLK frequency/duty, CS-high / SCK timing |
+| Kami / Kôika | Coq-based hardware DSL + verified compilation | Kami proves custom processors; t27 proves vendor FPGA configuration engine timing against an external flash datasheet |
+| Project X-Ray / prjxray | Reverse-engineered 7-series bitstream docs | prjxray documents *what* the bits mean; t27 formalizes the *timing consequences* of the CCLK bits and validates them empirically |
+| OpenTitan | Secure SoC boot / RoT | OpenTitan secures a processor boot chain; t27 secures the FPGA configuration stage itself |
+| SILVER | Formal masking verification of crypto netlists | SILVER verifies side-channel resistance; t27 verifies functional timing compliance of FPGA config with external flash |
+| spispy | SPI flash emulator/monitor for boot research | spispy emulates flash to study TOCTOU; t27 models the real on-board N25Q128 timing spec and validates against live capture |
+| Commercial SPI NOR VIP | Closed simulation reference models | t27 provides an open, machine-checked Lean 4 bound tied to a real Artix-7 board and a `sigrok-cli` measurement gate |
+
+The unique position after W407 is an **open, board-grounded, formally proved
+boot-timing assurance layer** that covers frequency, duty cycle, CS# high time,
+and wake-up constraints, with a CI-runnable validation fixture.
+
+---
+
+## Decomposed plan
+
+| Step | File(s) | Deliverable |
+|---|---|---|
+| 1 | `.claude/plans/wave-loop-407.md` | This plan: weak points, competitor scan, chosen variant |
+| 2 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` | Add N25Q128 timing constants (CS high, SCK low/high, wake-up), `cclk_period_ns`, `sck_duty_ok`, `flash_spi_timing_ok`; prove `flash_spi_timing_ok 0`; add `cold_por_implies_flash_spi_timing_ok` |
+| 3 | `cli/tri/src/fpga.rs` | Add unit tests for `parse_logic_csv`; add `--synth` mode to generate a 2.5 MHz logic CSV fixture and run `--csv` + `--validate` on it |
+| 4 | `cli/tri/src/fpga.rs` | Extend `--validate` to also check duty-cycle bounds (placeholder: 25%–75% sensible range; can be tightened once real capture exists) |
+| 5 | `fpga/HARDWARE_SSOT.md` §3.6 | Document the deeper timing constraints, synthetic fixture command, and real-capture wiring checklist |
+| 6 | `docs/reports/*` | W407 report, evidence, and W408 cooperation variants |
+| 7 | `.trinity/experience.md` | W407 learnings |
+| 8 | `docs/NOW.md` | W407 entry |
+| 9 | git/PR | Squash-merge to `master`, close #1316, open #W408 |
+
+---
+
+## Acceptance criteria
+
+- [ ] AC-A1 (Variant A, synthetic): a synthetic 2.5 MHz logic CSV fixture is
+      generated by `tri fpga measure-cclk --synth` and validated successfully.
+- [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.6 documents the exact P12 →
+      ADBUS4 wiring needed for a real capture and the expected 2.5 MHz result.
+- [ ] AC-C1 (Variant C): `TernaryFPGABoot.lean` defines `flash_spi_timing_ok` and
+      proves `flash_spi_timing_ok 0` for the canonical config.
+- [ ] AC-C2 (Variant C): a lemma links `cold_por_spi_flash_pred` to
+      `flash_spi_timing_ok`.
+- [ ] AC-D1: `./scripts/tri test` passes.
+- [ ] AC-D2: `lake build Trinity.TernaryFPGABoot` passes.
+- [ ] AC-D3: W407 report + evidence + W408 cooperation variants committed.
+
+---
+
+## Default variant
+
+**Variant C + synthetic Variant A**. The formal timing extension does not depend
+on bench hardware and advances the model; the synthetic fixture proves the CLI
+measurement/validation path works in CI. A real P12 capture remains the first
+priority once the wiring is available.
+
+---
+
+*phi^2 + phi^-2 = 3 | TRINITY*