pulseengine · avrabe · Aug 5, 2026 · Aug 5, 2026 · Aug 5, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -1078,7 +1078,7 @@ jobs:
       # emitting no verdicts) — see the script docstring.
       - name: Audit the SHIPPING allocator against the ABI contract (#242)
         run: |
-          set -o pipefail
+          set -euo pipefail
           SYNTH=./target/debug/synth python scripts/repro/vcr_ver_004_shipping_path_audit.py | tee vcr_ver_004_ship.out
           grep -q "^VCR-VER-004-SHIPPING .* VIOLATED=0 " vcr_ver_004_ship.out
           test "$(grep -c '^  Holds ' vcr_ver_004_ship.out)" -eq 1
@@ -1087,7 +1087,7 @@ jobs:
       # assertion would otherwise pass while gating nothing.
       - name: Re-run the v0.53 mutation against all three instruments (#242)
         run: |
-          set -o pipefail
+          set -euo pipefail
           python scripts/repro/vcr_ver_004_instrument_independence.py | tee vcr_ver_004.out
           grep -q "^VCR-VER-004-INDEPENDENCE ASSERTIONS=4/4$" vcr_ver_004.out
           test "$(grep -c '^OK   ' vcr_ver_004.out)" -eq 5

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -7,6 +7,59 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.54.0] - 2026-08-05
+
+**"Close what we measured."** v0.53 built the instruments; this release acts on
+what they said. Every lane targeted a gap a v0.53 gate named *mechanically* —
+not one someone guessed at — which inverts the usual order and is only possible
+because the measurement landed first.
+
+- **aarch64 is no longer a subset with a hand-written excuse list.** The scalar
+  float surface is COMPLETE (rounding via `FRINT{P,M,Z,N}`, FP memory, i64↔float
+  converts, and domain-guarded trapping i64-target truncations), and the two
+  largest structural declines are gone: `call_indirect` with all three WASM
+  §4.4.8 trap guards emitted inline, and WASM globals. The selector goes
+  **161 → 184 ops**; gale's acceptance matrix goes **45 → 61 ops / 119 → 355
+  native checks with an empty declined frontier**. Every op closed was picked
+  off the VCR-SEL-005 third-backend oracle's own complement, and each flipped
+  its `Err(reason)` ledger entry to `Ok(())` in the same commit that made it
+  lower — a gap claim must not outlive the gap.
+- **The allocator reaches across calls (#242).** VCR-DEC-001 increment 3 takes
+  57 of the 68 `call` declines; measured delta doubles to **−100 B relocatable /
+  −120 B self-contained, 0 WCET-bound regressions**. Still flag-off: the honest
+  read is that reach improved and the flip criterion is not met.
+- **VCR-VER-004 — a validator that fails *differently*.** v0.53 found that a
+  wrong-return-register rewrite was accepted by BOTH existing per-compilation
+  validators, caught only by execution. Both are backward liveness analyses
+  whose obligation set is a variable — and ∅ is a fixpoint, so an emptied seed
+  is vacuously green. The new check is FORWARD and value-level: exactly one
+  obligation per return site, so there is no seed to shrink. The v0.53 mutation
+  is now caught **statically**, with zero false rejections on the corpus.
+
+### The pattern this release kept finding
+
+Nine of the defects fixed here were in **checkers, not in the code they check**:
+a differential that printed `MISMATCH <-- BUG` and exited 0; the oracle-wiring
+gate's own CI step passing while the gate failed; three `set -o pipefail` steps
+without `-e`, where the step's status is its *last* command's; two test files
+that located the `synth` binary by walking up from `current_exe()`, which held
+`Code Coverage` RED repo-wide while the required `Test` job — same assertions,
+different target-dir layout — stayed green; and, at fan-in, an aarch64 decline
+oracle whose two sides were stale in OPPOSITE directions, each lane correctly
+updating the honesty ledger for its own work and being wrong about the other's.
+
+That last one is worth stating plainly: the error existed in **neither parent**
+and was created by the merge. Resolving it meant re-deriving what actually ships
+rather than choosing a side — and the oracle then confirmed the result, which is
+the only reason to trust it.
+
+**#890 remains the load-bearing open item.** The oracle-wiring gate took the
+repo from **70 undeclared scripts to 0** (145 wired / 7 manual with reasons),
+and it is enforced inside an already-required check so it cannot sit red
+unnoticed. But the count it fixed had *risen* over the preceding releases while
+individual instances were being fixed — the reminder that a bug factory is not
+addressed by fixing its output.
+
 ### Added
 
 - **aarch64 `call_indirect` and WASM globals — the two largest remaining
@@ -156,9 +209,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   (renamed `call-indirect-pseudo` — the high-level `Call`/`CallIndirect`
   pseudo-ops are expanded downstream into a bounds guard + table load + result
   move, so the register footprint here is not the one that ships, and they stay
-  declined by name). The residual buckets are `unmodeled-op` 174, `single-block`
-  73, `identity-colouring` 31, `unreachable-block` 11, `call-indirect-pseudo` 11,
-  `numeric-branch` 10.
+  declined by name). Measured at the release commit, the residual buckets are
+  `unmodeled-op` 175, `single-block` 73, `identity-colouring` 31,
+  `unreachable-block` 11, `call-indirect-pseudo` 17, `numeric-branch` 10.
+  (The corpus is `scripts/repro/*.{wat,wasm}` and therefore GROWS as lanes add
+  fixtures — it went 617 → 633 functions during this release's own fan-in, which
+  moved two of these buckets after the lane measured them. The durable claims
+  are the byte/cycle deltas and `Violated 0`; the absolute bucket counts are a
+  snapshot.)
 
   Still **flag-off by default** (`SYNTH_GRAPH_ALLOC`): this is a measurement
   spike, not a behaviour change. Frozen anchors byte-identical, 10/10.
@@ -255,10 +313,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   op; declining keeps it latent rather than shipping it. A real `VRINT.F32`
   lowering (the f32 twin of the shipping f64 path) is the follow-up.
 - The aarch64 decline-matrix oracle and the #554 float-honesty fixture were
-  repointed at constructs that are still genuinely declined (structural ones:
-  `call_indirect`, `br_table`, param writes, globals, bulk memory,
-  value-carrying blocks, SIMD), and the #554 assertion was strengthened to
-  require the diagnostic to come from the aarch64 SELECTOR and name its reason.
+  repointed at constructs that are still genuinely declined: `br_table`, writing
+  a PARAM local in a leaf function, `memory.copy`/`fill`, value-carrying blocks
+  and loops, v128/SIMD, multi-memory, `>8` args, float-result callees, import
+  calls — plus the six "rather than guess" refusals (imported global, global
+  with no decoded const initializer, non-leaf float param, growable imported
+  table, non-statically-verifiable element segment, table slot holding an
+  imported function). The #554 assertion was strengthened to require the
+  diagnostic to come from the aarch64 SELECTOR and to name its reason.
+  (An earlier draft of this sentence also listed `call_indirect` and globals —
+  both of which SHIP in this release, below. That draft was written by the float
+  lane before the call_indirect/globals lane landed; it was the third copy of a
+  list this release had to reconcile at fan-in, and the one the oracle and the
+  matrix row did not cover. Caught by cold review.)
 - **VCR-VER-004 — the ABI observable-contract validator: a per-compilation check
   that fails *differently*** (#242).
 

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/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.53.0"
+version = "0.54.0"
 edition = "2024"
 rust-version = "1.88"
 authors = ["PulseEngine Team"]

diff --git a/MODULE.bazel b/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.53.0",
+    version = "0.54.0",
 )
 
 # Bazel dependencies

diff --git a/README.md b/README.md
@@ -36,7 +36,7 @@
 
 &nbsp;
 
-Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, `--target cortex-r5`), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, `-b aarch64`). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), scalar f32/f64 via VFP on FPU targets (f32 complete v0.41, f64 complete v0.43 — #369 closed; the falcon `--relocatable cortex-m7dp` VFP-exhaustion tail closed in v0.53 via register-file spilling, #881; the remaining float residual is `i64.trunc_sat_f32_*` declining on single-precision FPUs, which needs the f64 promote), control flow, and memory operations; any construct without a lowering declines loudly rather than miscompiling (the #369/#554 gate class). Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs.
+Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, `--target cortex-r5`), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, `-b aarch64`). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), scalar f32/f64 via VFP on FPU targets (f32 complete v0.41, f64 complete v0.43 — #369 closed; the falcon `--relocatable cortex-m7dp` VFP-exhaustion tail closed in v0.53 via register-file spilling, #881; the remaining float residuals are `f32.{ceil,floor,trunc,nearest}`, which loud-decline on every ARM target pending a real `VRINT.F32` lowering (v0.54 — the legacy pseudo-op was unsound via a saturating `VCVT`), and `i64.trunc_sat_f32_*` declining on single-precision FPUs, which needs the f64 promote), control flow, and memory operations; any construct without a lowering declines loudly rather than miscompiling (the #369/#554 gate class). Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs.
 
 **This is pre-release software.** Generated code is validated by unit tests, Renode/QEMU emulation, execution differentials against wasmtime, and — for specific fixtures — cycle- and correctness-gated runs on real Cortex-M silicon (NUCLEO-G474RE, STM32F100, via the gale test loop). Broad hardware validation is still missing. Use at your own risk.
 

diff --git a/artifacts/status.json b/artifacts/status.json
@@ -21,7 +21,7 @@
   "sel_dsl_rule_qed": 50,
   "sel_dsl_rules": 50,
   "sel_rules_simplified_basis": 50,
-  "version": "0.53.0",
+  "version": "0.54.0",
   "verus_spec_fns": 8,
   "wasmcert_bridge_qed": 104
 }
diff --git a/crates/synth-backend-aarch64/Cargo.toml b/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.53.0" }
+synth-core = { path = "../synth-core", version = "0.54.0" }
 thiserror.workspace = true
 tracing.workspace = true
diff --git a/crates/synth-backend-awsm/Cargo.toml b/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.53.0" }
+synth-core = { path = "../synth-core", version = "0.54.0" }
 anyhow.workspace = true
 thiserror.workspace = true
diff --git a/crates/synth-backend-riscv/Cargo.toml b/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.53.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.53.0" }
+synth-core = { path = "../synth-core", version = "0.54.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.54.0" }
 anyhow.workspace = true
 thiserror.workspace = true
 tracing.workspace = true
@@ -21,4 +21,4 @@ tracing.workspace = true
 proptest.workspace = true
 # VCR-SEL-005 (#851): the cross-backend op-parity oracle probes the AArch64
 # selector as the THIRD backend (tests/cross_backend_op_parity.rs only).
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.53.0" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.54.0" }
diff --git a/crates/synth-backend-wasker/Cargo.toml b/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.53.0" }
+synth-core = { path = "../synth-core", version = "0.54.0" }
 anyhow.workspace = true
 thiserror.workspace = true
diff --git a/crates/synth-backend/Cargo.toml b/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.53.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.53.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.54.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.54.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.53.0", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.54.0", features = ["arm"] }
diff --git a/crates/synth-cli/Cargo.toml b/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.53.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.53.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.53.0" }
-synth-backend = { path = "../synth-backend", version = "0.53.0" }
+synth-core = { path = "../synth-core", version = "0.54.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.54.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.54.0" }
+synth-backend = { path = "../synth-backend", version = "0.54.0" }
 
 # AArch64 host-native backend (#538) — small pure-Rust crate, always on.
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.53.0" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.54.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.53.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.53.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.53.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.54.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.54.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.54.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.53.0", optional = true, features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.54.0", optional = true, features = ["arm"] }
 
 # Optional PulseEngine WASM optimizer
 # Uncomment when loom crate is available:
-Original file line number
+Diff line change
@@ Expand Up / @@ -36,7 +36,7 @@ @@
     &nbsp;
-    Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, `--target cortex-r5`), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, `-b aarch64`). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), scalar f32/f64 via VFP on FPU targets (f32 complete v0.41, f64 complete v0.43 — #369 closed; the falcon `--relocatable cortex-m7dp` VFP-exhaustion tail closed in v0.53 via register-file spilling, #881; the remaining float residual is `i64.trunc_sat_f32_*` declining on single-precision FPUs, which needs the f64 promote), control flow, and memory operations; any construct without a lowering declines loudly rather than miscompiling (the #369/#554 gate class). Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs.
+    Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, `--target cortex-r5`), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, `-b aarch64`). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), scalar f32/f64 via VFP on FPU targets (f32 complete v0.41, f64 complete v0.43 — #369 closed; the falcon `--relocatable cortex-m7dp` VFP-exhaustion tail closed in v0.53 via register-file spilling, #881; the remaining float residuals are `f32.{ceil,floor,trunc,nearest}`, which loud-decline on every ARM target pending a real `VRINT.F32` lowering (v0.54 — the legacy pseudo-op was unsound via a saturating `VCVT`), and `i64.trunc_sat_f32_*` declining on single-precision FPUs, which needs the f64 promote), control flow, and memory operations; any construct without a lowering declines loudly rather than miscompiling (the #369/#554 gate class). Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs.
     **This is pre-release software.** Generated code is validated by unit tests, Renode/QEMU emulation, execution differentials against wasmtime, and — for specific fixtures — cycle- and correctness-gated runs on real Cortex-M silicon (NUCLEO-G474RE, STM32F100, via the gale test loop). Broad hardware validation is still missing. Use at your own risk.
@@ Expand Down @@