v0.33.0 — correctness wave: four CF miscompiles closed, safety-bounds enforced, 21 verified selector rules

Four MORE live optimized-path miscompiles closed (#500 class); --safety-bounds actually enforced on BOTH paths (#377 — the direct path's existing check was a fallthrough no-op); zero-init locals (#457); the estimator gap allowlist reaches zero (#498); the verified selector DSL grows to 21 Rocq-proven rules; certified divisor-nonzero guard elision lands.

Fixed

• #500 class (PR #641): real if/else (both arms ran), bare if (then ran unconditionally), function-level br (post-block code ran), non-tail return (dropped) — all silently wrong on ≤v0.32.1's optimized path; now fixed-or-loudly-declined with a 14-case red→green CF differential (4 FAIL → 14/14). ir_to_arm now declines loudly on ANY unresolvable branch target.
• #377 (PR #640): --safety-bounds software was a silent no-op on the optimized path and a fallthrough no-op on the direct path (Bhs to offset-0 — the compare ran, the trap never fired). Both paths now trap 13/13 OOB vectors (was 6/13 on both). mask loud-declines; mpu proven path-independent.
• #457 (PR #638): read-before-write non-param locals read caller garbage on all three backends — fixed via declared param count + prologue zero-init + decline routing.
• #498 (PR #641): estimator allowlist 2 → 0; latent negative-imm MOVS wrong-value bug and far-branch layout-shift hazard fixed; KNOWN_GAP machinery deleted.

Added

• VCR-SEL-001 increment 2 (PR #639, #242): 21 rules / 21 Qed / 0 Admitted — i32 comparisons, register shifts, rotr join the verified selector DSL. OFF ≡ baseline byte-identical.
• Divisor-nonzero fact elision (PR #636, #494 phase 2b): certified div/rem zero-guard elision; the INT64_MIN/-1 overflow guard falls only to its own obligation.

Platform binaries attach ~10 min after the tag.

🤖 Generated with Claude Code