chore(release): v0.36.0 — unreachable traps, sparse tables, 40 verified rules, 81 bridge Qed

CHANGELOG.md

@@ -7,6 +7,60 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.36.0] - 2026-07-08
+
+**`unreachable` finally traps (it was decode-dropped as an "intentional no-op"
+on every backend — WASM §4.4.5); RV32 rem_s stops over-trapping; sparse
+funcref tables dispatch with null-slot traps (falcon complete); the verified
+selector DSL reaches 40 rules and the Sail/ASL bridge reaches 81 Qed —
+catching two latent bugs in our own hand-written model.**
+
+### Changed
+
+- **Post-exhaustion code quality (PR #672, #242 — the VCR-VER-001-named
+  capability):** spill-cleanup now reaches allocation-time Belady slots
+  (exit-dead scratch renaming, const rematerialization, bounded cleanup
+  fixpoint, const-divisor guard elision under spill) — all scoped to
+  `SYNTH_SPILL_ON_EXHAUST` firings; flag-off bit-identical. Cycle-proxy vs
+  PR #659: spill_rung +32.4% → +8.8%, exhaust +30.4% → +17.4%,
+  high_pressure_i32 and signed_div_const now BEAT the decline path (−24%,
+  −33%). Residual named: the bridge's fixed 5-register destination pool —
+  i.e. the Track-A allocator replacement itself. Flip stays held (#580).
+
+### Fixed
+
+- **WASM `unreachable` compiled to a no-op on thumb-2 AND rv32 (#665, PR
+  #668).** One decode drop: `Unreachable` was whitelisted as intentionally
+  ignorable next to `Nop`, so every backend's existing trap arm was dead
+  code. Now decoded; UDF/ebreak/brk fire per backend; optimized path
+  loud-declines to direct. Differential: 5 red → green with non-vacuity.
+- **RV32 i32.rem_s(INT_MIN,-1) spuriously trapped (#666, PR #668)** — rem_s
+  had inherited div_s's overflow guard; M-ext REM already returns 0 per
+  spec. The ARM #633 twin-pins now exist on RV32 (rem_s carries only the
+  zero guard).
+
+### Added
+
+- **Null-funcref-slot call_indirect (#664, PR #669):** sparse tables no
+  longer decline — initialized slots type-verified closed-world, null slots
+  trap at runtime (check emitted only when the table has nulls; fully-
+  initialized tables whole-ELF byte-identical, 24/24). Contract: null slots
+  link as zero words (BSS satisfies). falcon's dispatch story is complete.
+- **VCR-SEL-001 increment 4 (PR #670, #242/#667):** 40 rules / 40 Qed —
+  clz, ctz (scratch=dest, no side condition), popcnt (pseudo-op tier), and
+  the ten binary i64 comparisons (the #615 cond-mapping class, register-
+  polymorphic). New DSL-coverage metric in coq/STATUS.md: 26% DSL-served /
+  62% model-only / 12% unverified — the #73 divergence now retires by
+  measurable subtraction. Named executor gap (SBCS flags-chain) converges
+  with the ISA spike's PC-executor gap.
+- **VCR-ISA-001 round 2 (PR #671, #242):** SailArmBridge.v 23 → **81 Qed**
+  (28 whole-instruction bridges: AddWithCarry family incl. live-carry
+  ADC/SBC, flag-free ALU, all four shifts in both forms, MOV/MOVW/MOVT).
+  **Found two latent hand-model divergences from ARM's ASL** (LSR/ASR #32,
+  register shift amounts ≥ 32 — unreachable via WASM masking, documented).
+  Amortization beat the spike estimate: six-plus classes in ~half a day.
+  VCR-ISA-001 → approved.
+
 ## [0.35.0] - 2026-07-08
 
 **The North-Star acceleration wave: the verified selector DSL enters the i64

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.35.0"
+version = "0.36.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.35.0",
+    version = "0.36.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.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.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.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.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.35.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.36.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.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.0" }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-backend/Cargo.toml

@@ -15,7 +15,7 @@ default = ["arm-cortex-m"]
 arm-cortex-m = ["synth-synthesis"]
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.35.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.35.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.36.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.36.0", optional = true }
 anyhow.workspace = true
 thiserror.workspace = true

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.35.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.35.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.35.0" }
-synth-backend = { path = "../synth-backend", version = "0.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.36.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.36.0" }
+synth-backend = { path = "../synth-backend", version = "0.36.0" }
 
 # AArch64 host-native backend (#538) — small pure-Rust crate, always on.
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.35.0" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.36.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.35.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.35.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.35.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.36.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.36.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.36.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.35.0", optional = true, features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.36.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.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.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.35.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.36.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.35.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.35.0" }
-synth-opt = { path = "../synth-opt", version = "0.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.36.0" }
+synth-opt = { path = "../synth-opt", version = "0.36.0" }
 serde.workspace = true
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-verify/Cargo.toml

@@ -20,12 +20,12 @@ arm = ["synth-synthesis"]
 
 [dependencies]
 # Core dependencies (always required)
-synth-core = { path = "../synth-core", version = "0.35.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.35.0" }
-synth-opt = { path = "../synth-opt", version = "0.35.0" }
+synth-core = { path = "../synth-core", version = "0.36.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.36.0" }
+synth-opt = { path = "../synth-opt", version = "0.36.0" }
 
 # ARM synthesis (optional, behind 'arm' feature)
-synth-synthesis = { path = "../synth-synthesis", version = "0.35.0", optional = true }
+synth-synthesis = { path = "../synth-synthesis", version = "0.36.0", optional = true }
 
 # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553)
 ordeal = "0.4"