pulseengine · avrabe · Jul 23, 2026 · Jul 22, 2026 · Jul 23, 2026 · Jul 23, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -7,8 +7,59 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.50.0] - 2026-07-22
+
+**"Cross-backend verified core, and the allocator endgame begins."** The
+whole-function register-allocation validator is now cross-backend (ARM incl.
+optimized joins + RV32), the SMT validator models i64 remainder natively instead
+of havoc, and — the headline — **a from-construction graph-colouring register
+allocator lands (flag-off), with every function it emits validated by that same
+verified oracle.** That is the North Star's first foothold: the verified checker
+gating its own replacement. Seven parallel lanes; every one oracle-gated red-first;
+frozen anchors byte-identical throughout.
+
 ### Added
 
+- **VCR-DEC-001 — a from-construction graph-colouring register allocator (spike,
+  flag-off `SYNTH_GRAPH_ALLOC`).** The North Star made concrete: a second allocator
+  that builds an interference graph from the whole-function liveness VCR-RA-003
+  already computes, Chaitin/Briggs-colours it over R0–R8 (reserved R9–R12 held
+  identity), and spills by farthest-next-use — declining to the shipping greedy
+  allocator on any control-flow / spill / unmodeled-op it can't yet handle (never
+  hard-fails). **The point is the gate:** with the flag on, every function it emits
+  is checked by the unconditional VCR-RA-003 validator, which returns *Consistent*
+  on every applied function (6/10 corpus fixtures) — the verified acceptance oracle
+  gating its own replacement. Non-vacuity proven (a `signed_div_const` that greedy
+  reallocation shrinks 40 B→34 B is reproduced by the colouring path, not an
+  identity transform); the real gate is `validate_segment_rewrite` trace-equality
+  (rejects a value-flow-breaking merge-rename). **Flag-OFF is byte-identical** —
+  frozen 10/10, the shipping path untouched; NO default flip (that is the
+  widen-and-measure step). Whole-function webs across CF joins are the named next
+  increment. New module `crates/synth-synthesis/src/graph_alloc.rs`.
+- **RV32: `memory.size` / `memory.grow` lower (cross-backend parity, #223/#232).**
+  The universe-complete op-parity gate's ledger shrinks 21→19: `memory.size`
+  materializes the fixed-memory page count as a compile-time constant, and
+  `memory.grow` returns `-1` for fixed memory — with the `memory.grow(0)` →
+  `memory.size` fold moved to `synth_core` so ARM and RV32 share ONE implementation
+  (the soundness point: `grow(0)` returns the current size, never miscompiles to
+  `-1`). Executed vs **wasmtime** under unicorn on a real `(memory 3)` module.
+  `global.get`/`global.set` root-caused as a #798-class *substrate* decline (RV32
+  needs the linker-reserved region + startup init before a sound landing), kept an
+  honest ledgered decline rather than a vacuous fix.
+- **AArch64: void-block control flow — `block` / `br` / `br_if` (#538).** The
+  `-b aarch64` backend gains basic control flow (was straight-line-only): A64
+  B/B.cond branches + label resolution. Execution-verified vs wasmtime (arm64 host
+  + unicorn, both branch edges); value-blocks / loop / memory still loud-decline by
+  name.
+- **Pinned the SMT solver at `ordeal =0.9.1` (#849).** The dependabot
+  `ordeal 0.9.1 → 0.12.0` bump (#825) shipped a `bvsrem`/`bvsdiv`
+  solver-performance regression that HANGS div/rem trap-preservation VCs (4–6h
+  CI timeouts on both the ordeal-default Test job and the Z3 differential job).
+  Pinned back to the exact last-green version; the full `synth-verify` suite
+  runs in ~41s again (was a >6h timeout on 0.12). The native i64 `rem_u`/`rem_s`
+  value model that leaned on 0.12's remainder terms (attempted in #844) is
+  reverted and deferred to a later release behind a per-query solver timeout
+  (#848). Verify-only: `.text` byte-identical.
 - **WCET phase 5 (#778) — data-dependent masked-ceiling loop certificates.** The
   `--wcet-hints` scry seam now bounds a DATA-DEPENDENT loop whose exit bound is a
   masked value `i REL (x & K)`. Because `x & K ∈ [0, K]` for ANY runtime `x`

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.49.0"
+version = "0.50.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.49.0",
+    version = "0.50.0",
 )
 
 # Bazel dependencies

diff --git a/artifacts/status.json b/artifacts/status.json
@@ -15,7 +15,7 @@
   "sel_dsl_pilot_qed": 7,
   "sel_dsl_rule_qed": 50,
   "sel_dsl_rules": 50,
-  "version": "0.49.0",
+  "version": "0.50.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.49.0" }
+synth-core = { path = "../synth-core", version = "0.50.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.49.0" }
+synth-core = { path = "../synth-core", version = "0.50.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.49.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.49.0" }
+synth-core = { path = "../synth-core", version = "0.50.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.50.0" }
 anyhow.workspace = true
 thiserror.workspace = true
 tracing.workspace = true

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.49.0" }
+synth-core = { path = "../synth-core", version = "0.50.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.49.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.49.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.50.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.50.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.49.0", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.50.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.49.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.49.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.49.0" }
-synth-backend = { path = "../synth-backend", version = "0.49.0" }
+synth-core = { path = "../synth-core", version = "0.50.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.50.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.50.0" }
+synth-backend = { path = "../synth-backend", version = "0.50.0" }
 
 # AArch64 host-native backend (#538) — small pure-Rust crate, always on.
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.49.0" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.50.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.49.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.49.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.49.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.50.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.50.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.50.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.49.0", optional = true, features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.50.0", optional = true, features = ["arm"] }
 
 # Optional PulseEngine WASM optimizer
 # Uncomment when loom crate is available:

diff --git a/crates/synth-frontend/Cargo.toml b/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.49.0" }
+synth-core = { path = "../synth-core", version = "0.50.0" }
 
 wasmparser.workspace = true
 wasm-encoder.workspace = true

diff --git a/crates/synth-opt/Cargo.toml b/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.49.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.50.0" }
 
 [dev-dependencies]
 criterion = { version = "0.8", features = ["html_reports"] }

diff --git a/crates/synth-synthesis/Cargo.toml b/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.49.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.49.0" }
-synth-opt = { path = "../synth-opt", version = "0.49.0" }
+synth-core = { path = "../synth-core", version = "0.50.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.50.0" }
+synth-opt = { path = "../synth-opt", version = "0.50.0" }
 serde.workspace = true
 anyhow.workspace = true
 thiserror.workspace = true