@@ -7,6 +7,60 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
77
88## [ Unreleased]
99
10+ ## [ 0.36.0] - 2026-07-08
11+
12+ ** ` unreachable ` finally traps (it was decode-dropped as an "intentional no-op"
13+ on every backend — WASM §4.4.5); RV32 rem_s stops over-trapping; sparse
14+ funcref tables dispatch with null-slot traps (falcon complete); the verified
15+ selector DSL reaches 40 rules and the Sail/ASL bridge reaches 81 Qed —
16+ catching two latent bugs in our own hand-written model.**
17+
18+ ### Changed
19+
20+ - ** Post-exhaustion code quality (PR #672 , #242 — the VCR-VER-001-named
21+ capability):** spill-cleanup now reaches allocation-time Belady slots
22+ (exit-dead scratch renaming, const rematerialization, bounded cleanup
23+ fixpoint, const-divisor guard elision under spill) — all scoped to
24+ ` SYNTH_SPILL_ON_EXHAUST ` firings; flag-off bit-identical. Cycle-proxy vs
25+ PR #659 : spill_rung +32.4% → +8.8%, exhaust +30.4% → +17.4%,
26+ high_pressure_i32 and signed_div_const now BEAT the decline path (−24%,
27+ −33%). Residual named: the bridge's fixed 5-register destination pool —
28+ i.e. the Track-A allocator replacement itself. Flip stays held (#580 ).
29+
30+ ### Fixed
31+
32+ - ** WASM ` unreachable ` compiled to a no-op on thumb-2 AND rv32 (#665 , PR
33+ #668 ).** One decode drop: ` Unreachable ` was whitelisted as intentionally
34+ ignorable next to ` Nop ` , so every backend's existing trap arm was dead
35+ code. Now decoded; UDF/ebreak/brk fire per backend; optimized path
36+ loud-declines to direct. Differential: 5 red → green with non-vacuity.
37+ - ** RV32 i32.rem_s(INT_MIN,-1) spuriously trapped (#666 , PR #668 )** — rem_s
38+ had inherited div_s's overflow guard; M-ext REM already returns 0 per
39+ spec. The ARM #633 twin-pins now exist on RV32 (rem_s carries only the
40+ zero guard).
41+
42+ ### Added
43+
44+ - ** Null-funcref-slot call_indirect (#664 , PR #669 ):** sparse tables no
45+ longer decline — initialized slots type-verified closed-world, null slots
46+ trap at runtime (check emitted only when the table has nulls; fully-
47+ initialized tables whole-ELF byte-identical, 24/24). Contract: null slots
48+ link as zero words (BSS satisfies). falcon's dispatch story is complete.
49+ - ** VCR-SEL-001 increment 4 (PR #670 , #242 /#667 ):** 40 rules / 40 Qed —
50+ clz, ctz (scratch=dest, no side condition), popcnt (pseudo-op tier), and
51+ the ten binary i64 comparisons (the #615 cond-mapping class, register-
52+ polymorphic). New DSL-coverage metric in coq/STATUS.md: 26% DSL-served /
53+ 62% model-only / 12% unverified — the #73 divergence now retires by
54+ measurable subtraction. Named executor gap (SBCS flags-chain) converges
55+ with the ISA spike's PC-executor gap.
56+ - ** VCR-ISA-001 round 2 (PR #671 , #242 ):** SailArmBridge.v 23 → ** 81 Qed**
57+ (28 whole-instruction bridges: AddWithCarry family incl. live-carry
58+ ADC/SBC, flag-free ALU, all four shifts in both forms, MOV/MOVW/MOVT).
59+ ** Found two latent hand-model divergences from ARM's ASL** (LSR/ASR #32 ,
60+ register shift amounts ≥ 32 — unreachable via WASM masking, documented).
61+ Amortization beat the spike estimate: six-plus classes in ~ half a day.
62+ VCR-ISA-001 → approved.
63+
1064## [ 0.35.0] - 2026-07-08
1165
1266** The North-Star acceleration wave: the verified selector DSL enters the i64
0 commit comments