chore(release): v0.46.0 — qualification depth + capability breadth

CHANGELOG.md

@@ -7,6 +7,68 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.46.0] - 2026-07-16
+
+**Qualification depth + capability breadth.** The sequel to the #757 arc: synth's
+output now carries machine-checkable evidence an assessor needs — a per-compilation
+addressing validator (the #757 class unrepresentable by construction) and sound
+static WCET bounds — alongside real capability growth (AArch64 scalar floats, the
+self-contained call-graph execution-gated, and a tighter proof base).
+
+### Added (verification depth)
+
+- **VCR-VER-003 — per-compilation static-data addressing validation (#777).** The
+  construction-based answer to #757 (which survived four releases because value
+  differentials are coverage-limited): `synth_core::static_data_addr` proves, for
+  EVERY static-data relocation, that the byte the packed `.data` serves equals the
+  byte the runtime-applied linear memory (segments in declaration order,
+  later-wins) holds at that address — hard-erroring the compile on a wrong-segment
+  binding. Concrete byte-equality, **unconditional** (runs in the default shipping
+  build — a `verify`-gated check would have stayed dormant in exactly the build
+  that shipped #757). Red-first gated: the same validator returns `Mismatch` on
+  the `.position()` (first-match) resolution and `Consistent` on `.rposition()`;
+  the e2e gate compiles gale's real `loom.wasm`.
+- **Sound static per-function WCET bounds (#778).** `--emit-wcet` writes a
+  `synth-wcet-v1` JSON sidecar (`.text` byte-identical) with a per-function
+  worst-case cycle bound — gale/spar's T3/T4 `C_i` input, a *bound* rather than a
+  DWT observation. Loop-free/call-free functions get an exact conservative sum of
+  documented per-op worst-case cycles (MAX over Cortex-M3/M4; exhaustive
+  no-wildcard cycle table = new-op tripwire; i64-expansion sizes pinned to the
+  encoder-agreement oracle). Everything a sound bound can't cover **loud-declines
+  with a machine reason** — loops (needs a trip count), calls, the i64 software
+  div/rem internal loop, non-M3/M4 cores. Sound-critical constants pinned in
+  `claims.yaml`. Loop-bound inference (scry, untrusted-hint + sound-check) and
+  inter-procedural composition are named follow-ups.
+- **Verify-what-ships proof residuals closed (#166).** **485 → 489 Qed, 5 → 3
+  Admitted**: two Compilation.v admits discharged (`vm_compute` on the
+  constant-size guard) + two new Qed proving the shipped MOVW/MOVT split-immediate
+  reconstruction. The remaining three are pinned as honest T3 with in-file
+  rationale (a raw-vs-normalized representation gap with a concrete
+  counterexample — closing it needs a contract change, not a proof; and two
+  Sail-axiom placeholders superseded by `SailArmBridge.v`). The arc's named
+  control-flow/division residuals were confirmed already closed by #73.
+
+### Added (capability breadth)
+
+- **AArch64 milestone 3 — scalar floating point, 0 → 35 ops (#538).** f32/f64
+  arithmetic (add/sub/mul/div), abs/neg, f64 sqrt, const, the full NaN-correct
+  compare family, promote/demote, int→float converts, and bit-cast reinterprets —
+  on a new file-tagged (GP/FP) selector value stack with AAPCS64 float argument
+  passing. Every encoding clang-cross-verified; native+unicorn differential
+  **513/513** vs wasmtime (incl. NaN/±0/±inf). **Trapping float→int truncations
+  stay loud-declined** (A64 `FCVTZS`/`FCVTZU` saturate where WASM traps — the
+  #709 soundness class); min/max (NaN-propagation differs) and i64↔float likewise.
+  The m2 decline-matrix oracle + the #554 loudskip test were updated to assert the
+  *still-declined* floats (the CI decline-honesty gate correctly went red when m3
+  implemented ops the matrix still asserted declined).
+- **Self-contained reachable call-graph, execution-gated (#275 — refs, not
+  closes).** Finding: direct reachable-call-graph compilation already shipped
+  (#235); the genuine gap was the missing *execution* gate. Added a differential
+  that runs the self-contained image (real Reset_Handler on zeroed RAM) vs
+  wasmtime across a transitive call chain, plus a feature-gated non-vacuity probe
+  (RED when reverted to exports-only; the hatch is compiled OUT of release
+  binaries). The `call_indirect` table-dispatch residual remains open on #275.
+
 ## [0.45.2] - 2026-07-16
 
 **Soundness patch — #776 closed (aarch64 rotl clobber).**

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.45.2"
+version = "0.46.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.45.2",
+    version = "0.46.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.45.2" }
+synth-core = { path = "../synth-core", version = "0.46.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.45.2" }
+synth-core = { path = "../synth-core", version = "0.46.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.45.2" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.45.2" }
+synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.46.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.45.2" }
+synth-core = { path = "../synth-core", version = "0.46.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.45.2" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.45.2", optional = true }
+synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.46.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.45.2", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.46.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.45.2" }
-synth-frontend = { path = "../synth-frontend", version = "0.45.2" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.45.2" }
-synth-backend = { path = "../synth-backend", version = "0.45.2" }
+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" }
 
 # AArch64 host-native backend (#538) — small pure-Rust crate, always on.
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.45.2" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.46.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.45.2", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.45.2", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.45.2", optional = true }
+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 }
 
 # 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.45.2", optional = true, features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.46.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.45.2" }
+synth-core = { path = "../synth-core", version = "0.46.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.45.2" }
+synth-cfg = { path = "../synth-cfg", version = "0.46.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.45.2" }
-synth-cfg = { path = "../synth-cfg", version = "0.45.2" }
-synth-opt = { path = "../synth-opt", version = "0.45.2" }
+synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.46.0" }
+synth-opt = { path = "../synth-opt", version = "0.46.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.45.2" }
-synth-cfg = { path = "../synth-cfg", version = "0.45.2" }
-synth-opt = { path = "../synth-opt", version = "0.45.2" }
+synth-core = { path = "../synth-core", version = "0.46.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.46.0" }
+synth-opt = { path = "../synth-opt", version = "0.46.0" }
 
 # ARM synthesis (optional, behind 'arm' feature)
-synth-synthesis = { path = "../synth-synthesis", version = "0.45.2", optional = true }
+synth-synthesis = { path = "../synth-synthesis", version = "0.46.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.45.2",
+  "version": "0.46.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"