Wave Loop 408 — real CCLK measurement on P12 + complete SPI transaction model in Lean 4 #1318

Wave Loop 408 should close the remaining gap between the synthetic CCLK fixture and the physical board by capturing a real CCLK measurement on pin P12, and strengthen the formal argument with a complete SPI flash read-transaction model in Lean 4.

Background

W407 extended proofs/lean4/Trinity/TernaryFPGABoot.lean with static N25Q128_3V timing constants and a flash_spi_timing_ok predicate, and added tri fpga measure-cclk --synth so the measurement pipeline runs in CI without a wired probe (PR #1317). The real silicon anchor and a transaction-level proof are still missing.

Goals

1. Variant A — Real CCLK measurement on P12
   • Wire P12 (CCLK) → ADBUS4 and GND → GND on the Digilent FTDI cable (or use DSLogic/scope).
   • Run the canonical cold-POR protocol and capture the first ~1 ms after POR:

     tri fpga measure-cclk --live --driver ftdi-la --channel ADBUS4 \
         --samplerate 10000000 --samples 1000000 --validate
     

   • Commit the resulting CSV under docs/reports/ or build/fpga/.
   • Update fpga/HARDWARE_SSOT.md §3.6.1 with the measured frequency ± tolerance and duty cycle.
2. Variant C — Complete SPI flash transaction model in Lean 4
   • Define SPIReadTransaction with CS# high time, SCK edges, clock low/high times, wake-up delay.
   • Add artix7_boot_transaction (cfg : BitstreamConfig) that computes these from OSCFSEL.
   • Prove cfg.canonical → transaction_satisfies_flash_spec.

Acceptance criteria

• Real CCLK capture CSV exists in the repo.
• fpga/HARDWARE_SSOT.md contains the measured frequency and duty cycle.
• tri fpga measure-cclk --live ... --validate passes on real hardware.
• lake build Trinity.TernaryFPGABoot passes with the new transaction lemmas.
• ./scripts/tri test passes.
• W408 report + three W409 cooperation variants committed.

Cooperation fallback

If P12 cannot be wired in W408, fall back to Variant C alone (formal transaction model). If CI automation is the priority, pick Variant B (relay-controlled cold-POR) in W409.

🤖 Generated with Claude Code