chore(release): v0.42.0 — trap-preservation VC + float completion + parity benchmark + #739 soundness hub

CHANGELOG.md

@@ -7,6 +7,85 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.42.0] - 2026-07-15
+
+**The trap-preservation + float-completion + parity hub: dropping a WASM trap
+becomes a provable defect, the falcon float story completes (f32-across-call +
+scalar f64), the Rocq selector model is generated — not mirrored, and the
+"wasm is slower" claim gets a reproducible, falsifiable answer. Plus a silent
+shadow-stack miscompile fixed with its vacuous oracle de-blinded.**
+
+### Fixed
+
+- **Static above sp_init no longer silently miscompiles under
+  `--shadow-stack-size` (#739, soundness).** The sub-word i32 load/store arms
+  never received the #359 native-pointer static classification, so a
+  meld-fused static at an offset above sp_init was BAKED as an un-relocated
+  MOVW/MOVT immediate — invisible to the #678 rebase AND to the post-link
+  in-range oracle (which only walked relocations: a vacuous gate, the
+  #712-class lesson). Sub-word arms now emit the `__synth_wasm_data + C`
+  relocation like word accesses; the shrink additionally SCANS the encoded
+  text for surviving baked static constants and refuses loudly; a no-reloc
+  shrink now refuses instead of silently no-op'ing. i64 static-region accesses
+  decline loudly (previously silently miscompiled). Execution differential
+  CI-wired; #383/#678/#707 regressions green.
+- **f64 comparisons would have returned stale-flag garbage (#369
+  prerequisite).** `encode_thumb_f64_compare` had the exact #712 flag-clobber
+  (`MOVS` after `VMRS`) — caught and fixed BEFORE f64 shipped, execution-
+  validated non-vacuously.
+- **Mixed-pool parameter backing stored the wrong register (#719
+  prerequisite).** The #204 param-backing prologue used `index_to_reg(i)`,
+  wrong under mixed int/float pools (`(f32,i32)` homes i32 in R0, not R1);
+  the callee read garbage. Caught by a new execution row.
+
+### Added
+
+- **Trap-preservation is now a provable obligation (VCR-VER-002 Phases A+B,
+  #166, ordeal#59).** `synth-verify` consumes ordeal 0.9.1's `trap` module:
+  QF_BV trap conditions for div/rem (÷0 + INT_MIN/-1), memory OOB (symbolic
+  `mem_bound`), `call_indirect` (bounds ∨ null-slot ∨ type, with the
+  closed-world compile-time-discharge mode), `unreachable`, and all six
+  float→int trunc variants (validated against the 31-row #709 boundary table
+  through both `ordeal::eval` and the certified pipeline). The red-first gate
+  proves every trap-DROPPING lowering is caught (`Sat` + counterexample) and
+  every preserving one accepted (`Unsat`, LRAT re-checked) — the systematic
+  end of the #633/#666/#665/#642/#709 whack-a-mole. Live-validator wiring for
+  the remaining classes is the documented follow-on.
+- **The falcon float story completes (#719, #369 phase 2).** f32 live across
+  a call spills/rehomes (16-slot VFP call-spill area, the VFP #188); scalar
+  f64 on cortex-m7dp: const, promote_f32, add/sub/mul/div, abs/neg/sqrt, all
+  six compares, load/store, f64-across-call. Float-signature call boundaries
+  and f64 params decline loudly (marshalling = named next increment). 187/187
+  f32 + 126/126 f64 bit-exact vs wasmtime, CI-gated. m4f/m3 honest-reject.
+- **The Rocq selector model is generated, not mirrored (VCR-ISA-001 #667
+  increment 2).** `VcrSelRules.v` now DEFINES `rule_X := Gen.rule_X` — the
+  shipped `sel_dsl::RULES` table emits the single model source, the 40
+  correctness Qed are stated directly about it, and a selector change breaks
+  the matching proof. The interim reflexivity gate was retired as vacuous
+  (proof count 472, honestly recounted from 512).
+- **Reproducible wasm-AOT vs native-C parity benchmark (#735).**
+  `scripts/repro/parity_benchmark/` + `artifacts/parity-benchmark.md`:
+  measured bytes on pinned toolchains with one falsification command per row.
+  Headline: gust_mix clamp under a loom-proven premise = **14 B vs 26 B
+  measured `arm-none-eabi-gcc -Os` (0.54× of native)** — AOT-wasm SMALLER
+  than native because it carries a machine-checked value-range proof the C
+  compiler doesn't have. Honest gaps shown (gust_poll 3.48×, flat_flight
+  2.54×, falcon f32 1.64×); cycles marked OPEN (gale silicon).
+- **One more certified elision class: redundant-mask (#494).**
+  `SYNTH_FACT_SPEC` elides masks proven redundant by value-range premises —
+  gust_kernel 34 → 20 B, ordeal-certified per elision, sound decline without
+  the premise.
+
+### Changed
+
+- **gust_poll shrinks 740 → 724 B (#390, VCR-RA).** `forward_stack_reloads`
+  upgraded to a conditional-branch-transparent holder-lattice walk — reloads
+  across `br_if` ladders become moves or vanish. Corpus: 26 fixtures shrink,
+  0 grow; full differential sweep on the new bytes BEFORE re-pinning (the
+  refreeze ritual); `SYNTH_NO_STACK_FWD=1` opt-out pinned to old bytes.
+  Filed pre-existing #740 (gust_poll br_if mid-shape) with an anti-vacuous
+  xfail.
+
 ## [0.41.0] - 2026-07-11
 
 **f32 op-completeness for falcon + a soundness-gate hardening.**

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.41.0"
+version = "0.42.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.41.0",
+    version = "0.42.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.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.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.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.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.41.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.42.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.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.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.41.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.41.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.42.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.42.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.41.0", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.42.0", features = ["arm"] }

crates/synth-cli/Cargo.toml

@@ -44,23 +44,23 @@ verify = ["synth-verify"]
 # 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.41.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.41.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.41.0" }
-synth-backend = { path = "../synth-backend", version = "0.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.42.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.42.0" }
+synth-backend = { path = "../synth-backend", version = "0.42.0" }
 
 # AArch64 host-native backend (#538) — small pure-Rust crate, always on.
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.41.0" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.42.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.41.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.41.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.41.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.42.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.42.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.42.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.41.0", optional = true, features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.42.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.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.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.41.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.42.0" }
 
 [dev-dependencies]
 criterion = { version = "0.8", features = ["html_reports"] }

crates/synth-synthesis/Cargo.toml

@@ -11,9 +11,9 @@ categories.workspace = true
 description = "WASM-to-ARM instruction selection and peephole optimizer"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.41.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.41.0" }
-synth-opt = { path = "../synth-opt", version = "0.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.42.0" }
+synth-opt = { path = "../synth-opt", version = "0.42.0" }
 serde.workspace = true
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-verify/Cargo.toml

@@ -22,12 +22,12 @@ arm = ["synth-synthesis"]
 
 [dependencies]
 # Core dependencies (always required)
-synth-core = { path = "../synth-core", version = "0.41.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.41.0" }
-synth-opt = { path = "../synth-opt", version = "0.41.0" }
+synth-core = { path = "../synth-core", version = "0.42.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.42.0" }
+synth-opt = { path = "../synth-opt", version = "0.42.0" }
 
 # ARM synthesis (optional, behind 'arm' feature)
-synth-synthesis = { path = "../synth-synthesis", version = "0.41.0", optional = true }
+synth-synthesis = { path = "../synth-synthesis", version = "0.42.0", optional = true }
 
 # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553).
 # 0.9 adds the `ordeal::trap` module (trap-preservation VCs, VCR-VER-002 / #166);

npm/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@pulseengine/synth",
-  "version": "0.41.0",
+  "version": "0.42.0",
   "description": "synth — a WebAssembly-to-ARM/RISC-V/AArch64 compiler with mechanized correctness proofs. Produces bare-metal ELF binaries for embedded targets.",
   "bin": {
     "synth": "./run.js"