chore(release): v0.47.0 — close the loops

CHANGELOG.md

@@ -7,6 +7,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.47.0] - 2026-07-17
+
+**"Close the loops" — every v0.46 loud-decline converted to a proven capability
+(or an honestly sharper decline), driven by real-module needs.** WCET bounds
+statically-proven loops and sound-checks untrusted hints (the scry seam); aarch64
+gains SOUND trapping float→int + IEEE-754-2019 min/max (35→46 ops, all 32 trap
+cases execution-verified); the #275 finale ships self-contained `call_indirect`
+(falcon unblocked, #275 CLOSED); the addressing validator extends to spans, the
+self-contained ROM image, and RV32; the WasmCert anchor grows 489→536 Qed; and
+`cabi-arena-realloc` binds natively on self-contained dissolves (**#418 remains
+open** for the real dissolved fixture). The #791 soundness fix shipped same-day
+as v0.46.1.
+
 ### Added
 
 - **Self-contained `--cortex-m` `call_indirect` — the #275 finale (falcon's
@@ -28,13 +41,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   `select_default` demo path. `--relocatable` output is byte-identical;
   self-contained modules without `call_indirect` are byte-identical.
 
-### Found (tracked separately)
-
-- **#791: the optimized path miscompiles const-only-body functions** (result
-  materialized in r4, never moved to R0) — surfaced by the first execution
-  gate that runs dispatch targets in a default self-contained image; present
-  on main independent of this change (`--no-optimize` is correct).
-
 - **WCET phase 2 — statically-proven loop bounds + the `--wcet-hints` seam
   (#778).** `--emit-wcet` now BOUNDS canonical const-bound counted loops
   instead of declining them: a conservative symbolic walk over the final
@@ -66,6 +72,88 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   additionally executed under unicorn at authoring time (result correct,
   executed machine instructions ≤ bound).
 
+- **aarch64 milestone 4 — sound trapping float→int + IEEE-754-2019 min/max +
+  copysign (#538, 35 → 46 ops).** `i32.trunc_f32/f64_s/u` lower behind a
+  two-sided WASM §4.3.3 domain guard (exact boundary constants, ordered
+  `fcmp`+`b.cond` skipping a `brk #0` only on the proven-in-range path — NaN
+  fails every ordered condition → trap) with `FCVTZS/FCVTZU` only where
+  saturate ≡ trunc; `f32/f64.min/max` use single `FMIN/FMAX` (IEEE 754-2019
+  minimum/maximum = exactly WASM NaN-propagation + −0<+0, verified vs wasmtime
+  — `FMINNM/FMAXNM` would be the wrong minNum semantics); `copysign` via GP-file
+  bit surgery; `f32.sqrt` un-dropped at decode (now reachable on aarch64 AND
+  ARM32). Gate: 167-case boundary differential, **all 32 trap cases
+  execution-verified** (unicorn brk-exception + native SIGTRAP). Two latent
+  bugs found and fixed: an m3 `mov_imm64` halfword-shift bug (constants with
+  all-zero low halfwords materialized wrong) and the ARM32 `F32Min/F32Max`
+  pseudo-op (NaN/±0-wrong, previously dead code) now loud-declines until the
+  VMINNM twin lands. **Still declines (loud, gate-pinned):** f32/f64 rounding
+  ops (ceil/floor/trunc/nearest), i64↔float conversions, div/rem, popcnt —
+  the m2 decline oracle and #554 loudskip test were moved to these.
+
+- **VCR-VER-003 phase 2 — addressing validation for spans, the self-contained
+  ROM image, and RV32 (#777).** The per-compilation static-data addressing
+  validator now checks the FULL access span (a reloc whose access crosses a
+  segment's runtime-owned range no longer validates on byte 0 alone), the
+  self-contained `--cortex-m` packed ROM image (the #758 layout), and the RV32
+  static-data path. Unconditional as in phase 1 (`
+  validate_reloc_resolutions_spanned`, hard compile error on mismatch);
+  red-first gated per class (e2e gate grew 1 → 6 tests). The RV32 probe found
+  **#798** (active data segments silently dropped on RV32 — interim warning
+  landed; the ship-or-hard-decline fix is tracked there).
+
+- **WasmCert-Coq anchor phase 2 — 489 → 536 Qed (+47) and a concrete real-dep
+  path (VCR-WASM-001, epic #242).** 19 i32 ops (arithmetic, bitwise, shifts,
+  eqz, full compare family) transcribed with line-level provenance pinned to
+  the nix-built coq9.0-wasm-2.2.0 sources; 49 real Qed / 0 Admitted in the
+  bridge (genuine discharges — mod-arithmetic, bit-level testbit facts,
+  shift-count normalization collapse, the gt/le/ge orientation gap).
+  Feasibility verdict sharpened from "no-go": `coqPackages.wasmcert` exists in
+  the exact pinned nixpkgs and **nix-builds green**; three named bazel blockers
+  documented in the roadmap, including a **license policy point — CompCert 3.16
+  is unfree** (deliberately NOT taken into CI); upstream wasmcert ≥ 2.2.1 drops
+  the CompCert dep, so the real dep lands with the ruleset hook + the next
+  nixpkgs bump.
+
+- **`cabi-arena-realloc` binds natively on self-contained dissolves (#418 —
+  remains open for the real fixture).** When the wit-bindgen
+  `cabi-realloc-extern` arena import is the module's ONLY import, synth removes
+  it and prepends a defined wasm allocator (an index-preserving wasm→wasm
+  rewrite compiled through the ordinary pipeline — no hand-written machine
+  code, every existing validator applies), so the dissolve produces a real
+  self-contained image instead of degrading to a link-me ET_REL object.
+  Red-first execution differential: the image's own startup + each export vs
+  wasmtime with a host arena at a deliberately different base
+  (pointer-independent observables; exhaustion traps on both sides).
+  **Decline matrix (test-asserted):** `--relocatable` keeps the #420
+  undefined-symbol seam; modules with OTHER imports keep the host seam entirely
+  (never a half-bound hybrid); `--native-pointer-abi` declines (SP-promotion
+  hazard with the cursor global); wrong signature / no memory / non-const data
+  offsets / zero arena room refuse loudly; pinned opt-out
+  `--no-bind-cabi-arena`. #418 stays open on the maintainer ask for the real
+  dissolved `.wasm` as a pinned fixture.
+
+### Found (tracked separately)
+
+- **#791: the optimized path miscompiled const-only-body functions** (result
+  materialized in r4, never moved to R0) — surfaced by the first execution
+  gate that runs dispatch targets in a default self-contained image. Fixed
+  same-day; shipped as the **v0.46.1** backport (see below).
+- **#798: RV32 active data segments silently dropped** — found by the
+  VCR-VER-003 phase-2 RV32 probe; interim warning landed, ship-or-decline fix
+  tracked on #798.
+
+## [0.46.1] - 2026-07-17
+
+**Soundness backport — #791.** The optimized (default) path miscompiled functions
+whose body is a bare constant: `Opcode::Const` was the one value-producing arm
+that never recorded its dest as `last_result_vreg`, so the epilogue never moved
+the result to R0 and the export returned caller residue. Found by the #275
+finale's execution differential (the first gate to run dispatch targets in a
+default self-contained image). Tagged from v0.46.0 + the cherry-picked fix
+(pure patch); also on main. Red-first `const_body_791_differential.py`; frozen
+anchors unchanged; `base_cse_flip_468` goldens re-pinned (+2 B harmless
+`mov r0,rX` on void stored-const tails) after a full differential sweep.
+
 ## [0.46.0] - 2026-07-16
 
 **Qualification depth + capability breadth.** The sequel to the #757 arc: synth's

Cargo.toml

@@ -28,7 +28,7 @@ resolver = "2"
 # semver to publish, so the convention now catches up: workspace
 # version follows the release tag, bumped pre-tag in the release
 # checklist. See docs/release-process.md.
-version = "0.46.0"
+version = "0.47.0"
 edition = "2024"
 rust-version = "1.88"
 authors = ["PulseEngine Team"]

MODULE.bazel

@@ -7,7 +7,7 @@ module(
     name = "synth",
     # Kept in lockstep with [workspace.package] version in Cargo.toml.
     # Both are bumped pre-tag — see docs/release-process.md.
-    version = "0.46.0",
+    version = "0.47.0",
 )
 
 # Bazel dependencies

crates/synth-backend-aarch64/Cargo.toml

@@ -11,6 +11,6 @@ categories.workspace = true
 description = "AArch64 (A64) host-native backend for synth — integer subset (milestone 1, #538)"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-core = { path = "../synth-core", version = "0.47.0" }
 thiserror.workspace = true
 tracing.workspace = true

crates/synth-backend-awsm/Cargo.toml

@@ -11,6 +11,6 @@ categories.workspace = true
 description = "aWsm backend integration for the Synth compiler"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-core = { path = "../synth-core", version = "0.47.0" }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-backend-riscv/Cargo.toml

@@ -11,8 +11,8 @@ categories.workspace = true
 description = "RISC-V encoder, ELF builder, PMP allocator, and bare-metal startup for synth"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.46.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.46.0" }
+synth-core = { path = "../synth-core", version = "0.47.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.47.0" }
 anyhow.workspace = true
 thiserror.workspace = true
 tracing.workspace = true

crates/synth-backend-wasker/Cargo.toml

@@ -11,6 +11,6 @@ categories.workspace = true
 description = "Wasker backend integration for the Synth compiler"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-core = { path = "../synth-core", version = "0.47.0" }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-backend/Cargo.toml

@@ -15,13 +15,13 @@ default = ["arm-cortex-m"]
 arm-cortex-m = ["synth-synthesis"]
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.46.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.46.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.47.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.47.0", optional = true }
 anyhow.workspace = true
 thiserror.workspace = true
 
 [dev-dependencies]
 # #667 move 2: the i64 pseudo-op expansion certification oracle
 # (tests/i64_expansion_certification.rs) feeds THIS crate's emitted encoder
 # bytes to the synth-verify expansion validator. Dev-only — no prod-dep edge.
-synth-verify = { path = "../synth-verify", version = "0.46.0", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.47.0", features = ["arm"] }

crates/synth-cli/Cargo.toml

@@ -58,23 +58,23 @@ exports_only_275_probe = []
 # Path deps carry `version` so `cargo publish` rewrites them to the
 # crates.io coordinate. Bumping the workspace version requires
 # updating these in lockstep — see docs/release-process.md.
-synth-core = { path = "../synth-core", version = "0.46.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.46.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.46.0" }
-synth-backend = { path = "../synth-backend", version = "0.46.0" }
+synth-core = { path = "../synth-core", version = "0.47.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.47.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.47.0" }
+synth-backend = { path = "../synth-backend", version = "0.47.0" }
 
 # AArch64 host-native backend (#538) — small pure-Rust crate, always on.
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.46.0" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.47.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.46.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.46.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.46.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.47.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.47.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.47.0", optional = true }
 
 # Optional translation validation — pure-Rust ordeal engine by default (#553),
 # no C++ toolchain needed. For the Z3 differential oracle build with
 # `--features verify,synth-verify/z3-solver` (+ SYNTH_SOLVER_DIFF=1 at runtime).
-synth-verify = { path = "../synth-verify", version = "0.46.0", optional = true, features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.47.0", optional = true, features = ["arm"] }
 
 # Optional PulseEngine WASM optimizer
 # Uncomment when loom crate is available:

crates/synth-frontend/Cargo.toml

@@ -14,7 +14,7 @@ description = "WASM/WAT parser and module decoder frontend for the Synth compile
 # Internal path deps carry an explicit version so `cargo publish`
 # can rewrite to the crates.io coordinate. `path` is used for
 # in-workspace builds; `version` is what crates.io sees.
-synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-core = { path = "../synth-core", version = "0.47.0" }
 
 wasmparser.workspace = true
 wasm-encoder.workspace = true

crates/synth-opt/Cargo.toml

@@ -11,7 +11,7 @@ categories.workspace = true
 description = "Peephole optimization passes for the Synth compiler"
 
 [dependencies]
-synth-cfg = { path = "../synth-cfg", version = "0.46.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.47.0" }
 
 [dev-dependencies]
 criterion = { version = "0.8", features = ["html_reports"] }