v0.40.0 — five-lane North-Star hub

A five-lane supervised feature hub. The f32 hard-float path completes and becomes sound, the verified selector now generates its own Rocq model, the beat-LLVM lane collapses branchless clamps, the gust size gap is quantified and pinned, and a self-contained call_indirect silent miscompile becomes an honest decline. Every lane landed as its own gated PR (#713–#717); two soundness fixes were independently re-verified against wasmtime before merge, and a cold-agent clean-room review confirmed all claims pre-tag.

Fixed (soundness)

• f32 i32.trunc_f32_s/u now TRAP on NaN/±∞/out-of-range (#709). The v0.39.0 path lowered trunc to a bare saturating VCVT where WASM Core §4.3.3 requires a trap. A domain guard (VCMP/VMRS/branch/UDF) now precedes the — provably in-range — VCVT. 48/48 vs wasmtime incl. the full trap table.
• f32 comparisons no longer silently return 0 (#709 prerequisite). A MOVS after VMRS clobbered the transferred FPSCR flags, so every v0.39.0 f32 compare returned 0 on hardware — masked because the harness skipped compare execution. Fixed + now execution-tested (60/60).
• Self-contained --cortex-m call_indirect no longer silently miscompiles (#275). The dispatch read the func table from [R11,idx*4], but R11 is the linear-memory base with no funcref table there — so it dispatched through data. It now declines LOUDLY pointing at --relocatable; the relocatable path is byte-untouched (#642/#650/#664/#676 pass).

Falsification: compile (func (result i32) (i32.trunc_f32_s (f32.const nan))) for cortex-m4f and run it — it must stop at a UDF, not return 0. Compile the 3-entry call_indirect module --cortex-m (no --relocatable) — the calling function must be skipped with a warning, not emitted.

Added

• f32.load + i32.reinterpret_f32 / f32.reinterpret_i32 (#708, #369). Unblocks the falcon float path (its float functions start with a load or reinterpret — 20 of 24 skips clear; f64 is phase 2). FPU-gated, honest-reject on M0/M3.
• The verified selector generates its own Rocq model (#667, VCR-ISA-001). The shipped DSL rule table emits VcrSelRulesGenerated.v + a per-rule reflexivity Qed proving Gen.rule_X = rule_X, wired into //coq:verify_proofs — Coq's kernel is now the model↔selector divergence gate, directly closing the #682 vacuous-proof class. Proof count 472→512 (the +40 are generated-vs-model gate lemmas, not new correctness proofs).
• gust size-gap attribution + tracked size oracle (#390, VCR-PERF-001). 3.56× vs LLVM quantified, overhead led by spill/reload (~31%); pinned as a CI gate.

Changed

• fact-spec collapses branchless select clamps (#494 ph3, VCR-PERF-002). Under a ValueRange premise it discharges an ordeal QF_BV obligation per select and deletes the dead arm — gust_mix 50 B → 14 B on a shape LLVM structurally can't beat. Opt-in (verify feature + SYNTH_FACT_SPEC), frozen-safe. This is a byte win; the 0.45× cycle floor remains gale's silicon measurement.

Gates

Pin sweep 0.39.1→0.40.0 (workspace + path deps + MODULE.bazel + npm). Claim gate 17/17, frozen anchors 10/10, clippy/fmt clean.