@@ -7,8 +7,65 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
77
88## [ Unreleased]
99
10+ ## [ 0.48.0] - 2026-07-17
11+
12+ ** "Real modules, verified allocator" — the real falcon fused core drove the
13+ breadth (its skip classes became implemented ops or honest declines), and the
14+ register allocator (the North Star's last major unverified component) finally got
15+ a per-compilation validator.** Wave 1 closed the real-module frontier (trunc_sat,
16+ the float select/return class, RV32 data segments) and hardened the claim surface
17+ into machine-derived badges; Wave 2 deepened the verified core (an unconditional
18+ allocation validator, inter-procedural WCET, the WasmCert dep hook). Every lane
19+ oracle-gated red-first; frozen anchors byte-identical throughout.
20+
1021### Added
1122
23+ - ** #782a: the WASM ` trunc_sat ` family — nontrapping saturating float→int.**
24+ Un-dropped the decoder family (` i32/i64.trunc_sat_f32/f64_s/u ` ); i32 forms
25+ lowered on ARM32 (bare round-toward-zero VCVT), all 8 forms on aarch64
26+ (FCVTZS/FCVTZU — native saturation is the CORRECT semantics here, the guard-free
27+ dual of the #709 trapping forms); ARM32 i64 forms loud-decline by name. Full
28+ boundary table (NaN→0, ±inf→min/max, exact INT_MIN..MAX bounds, ±0.5) verified
29+ bit-identical to wasmtime on m7dp+m4f+aarch64 — no traps anywhere. This gate
30+ caught an optimized-path silent-NOP drop at land time.
31+ - ** #782b: float ` select ` + explicit float ` return ` — the dominant falcon
32+ fused-core skip class.** The "an integer operation popped an f32" reports were
33+ NOT register pressure (that hypothesis was disproven by getting the real falcon
34+ bytes) but two missing lowerings: ` select ` over two f32/f64 values (the clamp
35+ idiom) and ` return ` of a float result. Getting the real bytes also surfaced two
36+ soundness bugs fixed red-first: a ** wide (i64) ` select ` hi-half SILENT
37+ miscompile on every target** (cond==0 returned val2's lo paired with val1's hi;
38+ soft-float f64 select rode the same path), and a ** hard-float signature-only ABI
39+ hole** (a float-signature function with no float op stayed on the float-naive
40+ optimized path — callers marshalled S0/S1, the body read R0/R1). 702-case
41+ differential vs wasmtime.
42+ - ** VCR-RA-003 (#242 ): unconditional register-allocation validator** — the North
43+ Star's last major unverified component gets a per-compilation checker
44+ (` synth_synthesis::liveness::validate_final_allocation ` , wired in ` arm_backend ` ,
45+ runs on every ARM compile in the default build, hard-errors on a violation).
46+ Bounded first increment: straight-line segments + spill/reload discipline, with
47+ two non-vacuous in-stream invariants — ** callee-saved preservation (#490 )** and
48+ ** spill-slot non-aliasing** . Red-first: a reverted #490 prologue / dropped
49+ epilogue / aliased slot / unmodeled-op-no-prologue are CAUGHT; correct codegen
50+ is silent (frozen 10/10 byte-identical is the silent-on-real-codegen proof).
51+ CF-joins + calls are the named phase 2.
52+ - ** WCET phase 3 (#778 ): inter-procedural composition over the direct call graph.**
53+ A caller with a direct ` BL func_N ` to a LOCAL bounded callee is now BOUNDED (was
54+ a blanket ` call ` decline): ` total = own_cycles + Σ_site multiplier × callee_total ` ,
55+ the per-site multiplier being the call site's proven execution count so a callee
56+ inside a proven loop is counted ` trip× ` . New sound-critical constant
57+ ` BL_BLX_CALL_OVERHEAD_CYCLES = 4 ` (MAX{M3,M4}, pinned in ` claims.yaml ` ).
58+ Decline-honesty preserved (moved, never deleted): recursion / any call-graph
59+ cycle → ` recursion ` , indirect → ` indirect-call ` , external import → ` call ` , a
60+ declined callee → ` callee-unbounded ` (propagates up). Unicorn-verified bound ≥
61+ actual; ` .text ` byte-identical (sidecar-only).
62+ - ** VCR-WASM-001 phase 3 (#242 ): the ` extra_coq_package ` bzlmod hook** — a generic
63+ mechanism to pull any ` coqPackages.<attr> ` into the hermetic toolchain without
64+ forking rules_rocq_rust (closes named blocker 1). The real WasmCert-Coq dep
65+ stays PENDING: the pinned nixpkgs ships wasmcert 2.2.0, which propagates unfree
66+ CompCert 3.16; wasmcert ≥ 2.2.1 (which drops CompCert) is not yet in the pin, and
67+ no unfree dep may enter CI. The 20-op transcription is unchanged (536 Qed held);
68+ the hook is ready to flip to the real dep the moment the pin bumps.
1269- ** #798 : RV32 active data segments SHIP — linker-script placement + startup
1370 copy (the RV32 analogue of #758 ).** The single-base scheme
1471 (` s11 = __linear_memory_base ` , zeroed RAM) used to emit a ` .text ` -only
0 commit comments