chore(release): v0.44.0 — five-lane hub (live trap classes, verified-selector 40→41, multi-mem coverage, size win, DWARF gate)

CHANGELOG.md

@@ -7,6 +7,77 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.44.0] - 2026-07-15
+
+**Five-lane hub: two more live trap classes, an extended verified-selector model,
+multi-memory coverage + honest isolation decline, a size win, and de-circularized
+DWARF.** Every lane oracle-gated; coordinator re-verified each soundness oracle
+before merge. Builds on the v0.43.1 clean base.
+
+### Added (verification)
+
+- **i64 div/rem + i32.trunc_f64 wired into the LIVE trap validator (#756).** The
+  VCR-VER-002 derived-ARM-trap-term validator goes from 5 → **7 live trap
+  classes**. i64 div/rem carries its zero/overflow guards as pseudo-op fields
+  (ARM32 has no 64-bit divide) — the trap term is reconstructed from those fields,
+  so a guard elided without a discharged fact is rejected. i32.trunc_f64_s/u gets
+  real `VCMP.F64` domain-guard semantics. Red-first gate proven non-vacuous
+  (dropped guard → Sat/caught; preserved → Unsat/accepted) across all classes.
+  **Residual:** `i64.trunc_f64_s/u` is NOT wired live — the selector loud-declines
+  it (no i64 register pairs on 32-bit ARM ⇒ no shipped lowering to validate); its
+  classifier stays unit-gated (documented in the roadmap).
+- **Verified-selector model extended 40 → 41 ops (VCR-ISA-001, #667 lineage).**
+  `i32.eqz` joins the generate-not-mirror Rocq model (new `rule_i32_eqz` in the
+  shipped `sel_dsl::RULES`, regenerated `Gen` module, `rule_i32_eqz_correct` Qed
+  stated directly about the generated model). **473 → 474 Qed / 5 Admitted.**
+  Byte-invisible (bit-identical under `SYNTH_NO_SEL_DSL=1`); the drift-guard holds
+  (flipping `MOVEQ→MOVNE` in the generated rule breaks the eqz Qed).
+
+### Added (capability)
+
+- **Multi-memory phase 2 — coverage hardening + honest isolation decline (#406).**
+  A new multi-segment static-data differential exercises multi-chunk/multi-segment
+  data across BOTH the self-contained and relocatable paths (varied offsets,
+  page-straddling, overlap-later-wins, near-globals) — 26/26 green, anti-vacuity
+  proven (neutering the reset copy goes RED). Per-memory MPU isolation is
+  **loud-declined**, not silently no-op'd: an architectural interlock (MPU
+  programming needs synth's own startup = self-contained path, but multi-memory
+  compiles only on `--relocatable` = host owns startup) means no path both emits
+  the startup and lowers >1 memory. `--safety-bounds mpu` on a multi-memory module
+  now refuses loudly naming the interlock; single-memory `mpu` unchanged.
+
+### Changed (size / optimization)
+
+- **Redundant-store elimination in `forward_stack_reloads` (#390).** A full-word
+  `str rd,[sp,#N]` whose slot the holder lattice PROVES already holds `rd` is a
+  no-op and is deleted. **gust_poll 724 → 716 B.** Reuses the same conservative
+  lattice that powers shipped reload-forwarding; `holders` left unchanged on
+  deletion; #606 frozen-span guard preserved; OVERWRITE-ONLY / sub-word-hole
+  invariants untouched. Only gust_poll's bytes change; all differentials green on
+  the new bytes.
+
+### Changed (test infrastructure)
+
+- **DWARF verification de-circularized (#394).** The `.debug_line`/`.debug_info`
+  emission (already shipped) was only checked with `gimli::read` — the same library
+  `gimli::write` emitted the bytes with, so a self-consistent emitter bug could
+  pass every oracle. Added an INDEPENDENT-parser gate (`llvm-dwarfdump --verify`
+  must report "No errors" + decode the CU/subprogram DIEs + line rows); fails hard
+  (never skips) when the tool is absent; CI installs `llvm`.
+
+### Known issues (still open)
+
+- **#757 — accepted residual for this release.** The wide-static *copy* path
+  carries a miscompile confirmed on gale's silicon but NOT reproducible from the
+  issue text (seven faithful reconstructions all byte-identical vs wasmtime; the
+  symptom decodes to `base + 12` with the correct relocation base = wrong runtime
+  offset, not wrong relocation). This release WIDENS static-data coverage (#406's
+  26/26 differential found no miscompile) but does not close #757 — it stays open,
+  blocked on the reporter's reduced module. Narrow, external-blocked, common shapes
+  green: documented acceptance, not a fix.
+- **#761 — latent self-contained linmem/globals top-of-SRAM overlap** (impact
+  unverified), filed for investigation.
+
 ## [0.43.1] - 2026-07-15
 
 **Soundness patch — the default `--cortex-m` path now ships its initialized data.**

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.43.1"
+version = "0.44.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.43.1",
+    version = "0.44.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.43.1" }
+synth-core = { path = "../synth-core", version = "0.44.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.43.1" }
+synth-core = { path = "../synth-core", version = "0.44.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.43.1" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.43.1" }
+synth-core = { path = "../synth-core", version = "0.44.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.44.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.43.1" }
+synth-core = { path = "../synth-core", version = "0.44.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.43.1" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.43.1", optional = true }
+synth-core = { path = "../synth-core", version = "0.44.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.44.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.43.1", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.44.0", features = ["arm"] }

crates/synth-cli/Cargo.toml

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