diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0acb0193..c4bbe9c2 100644
--- 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
index 2f18873c..7c76510b 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -659,18 +659,18 @@ checksum = "d6790f58c7ff633d8771f42965289203411a5e5c68388703c06e14f24770b41e"
 
 [[package]]
 name = "ordeal"
-version = "0.12.0"
+version = "0.9.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9b416f1d806dc12028cd553a243c16d1df68b1bd775fb778a82bd7e3736ff2af"
+checksum = "0c55b06587e2790390f278f8e0fdcb627aedf1ee45b9484a712c6cf1f80dccab"
 dependencies = [
  "ordeal-lrat",
 ]
 
 [[package]]
 name = "ordeal-lrat"
-version = "0.12.0"
+version = "0.9.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "35a63f37dab283272407df6aaeada83b7673fb5263e2fe7ef5f3e09336575ffd"
+checksum = "3affdf66f317047ddc588c7df4fbe5a463ee8f40a1e23f30115a8f8c7dffe82a"
 
 [[package]]
 name = "page_size"
@@ -1111,14 +1111,14 @@ dependencies = [
 
 [[package]]
 name = "synth-abi"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "synth-wit",
 ]
 
 [[package]]
 name = "synth-analysis"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "synth-core",
@@ -1127,7 +1127,7 @@ dependencies = [
 
 [[package]]
 name = "synth-backend"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "synth-core",
@@ -1138,7 +1138,7 @@ dependencies = [
 
 [[package]]
 name = "synth-backend-aarch64"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "synth-core",
  "thiserror",
@@ -1147,7 +1147,7 @@ dependencies = [
 
 [[package]]
 name = "synth-backend-awsm"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "synth-core",
@@ -1156,7 +1156,7 @@ dependencies = [
 
 [[package]]
 name = "synth-backend-riscv"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "proptest",
@@ -1168,7 +1168,7 @@ dependencies = [
 
 [[package]]
 name = "synth-backend-wasker"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "synth-core",
@@ -1177,11 +1177,11 @@ dependencies = [
 
 [[package]]
 name = "synth-cfg"
-version = "0.49.0"
+version = "0.50.0"
 
 [[package]]
 name = "synth-cli"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "clap",
@@ -1208,7 +1208,7 @@ dependencies = [
 
 [[package]]
 name = "synth-core"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "gimli",
@@ -1223,7 +1223,7 @@ dependencies = [
 
 [[package]]
 name = "synth-frontend"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "synth-core",
@@ -1237,14 +1237,14 @@ dependencies = [
 
 [[package]]
 name = "synth-memory"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "bitflags",
 ]
 
 [[package]]
 name = "synth-opt"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "criterion",
  "synth-cfg",
@@ -1252,11 +1252,11 @@ dependencies = [
 
 [[package]]
 name = "synth-qemu"
-version = "0.49.0"
+version = "0.50.0"
 
 [[package]]
 name = "synth-synthesis"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "proptest",
@@ -1271,7 +1271,7 @@ dependencies = [
 
 [[package]]
 name = "synth-test"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "clap",
@@ -1287,7 +1287,7 @@ dependencies = [
 
 [[package]]
 name = "synth-verify"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "chrono",
@@ -1306,7 +1306,7 @@ dependencies = [
 
 [[package]]
 name = "synth-wit"
-version = "0.49.0"
+version = "0.50.0"
 
 [[package]]
 name = "tempfile"
diff --git a/Cargo.toml b/Cargo.toml
index 1938e1b0..5c70871a 100644
--- 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
index 27abc426..937c0e5c 100644
--- 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
index a05827b8..5201ba03 100644
--- 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
index 1ff337b1..e8b88f5f 100644
--- 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
index 751db645..e93de7b0 100644
--- 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
index eb6f75a9..bf6ee04c 100644
--- 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
index 5c37c408..d2bfd5fa 100644
--- 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
index 3099329a..11086a4b 100644
--- a/crates/synth-backend/Cargo.toml
+++ b/crates/synth-backend/Cargo.toml
@@ -15,8 +15,8 @@ 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
 
@@ -24,4 +24,4 @@ thiserror.workspace = true
 # #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
index ba5d4eee..0e8467b4 100644
--- 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
index 16b7ec3e..a50c33df 100644
--- 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
index 87859d1a..1a7ebc2a 100644
--- 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
index 97919067..3451f2f5 100644
--- 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
diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml
index e088dace..1db90f6a 100644
--- a/crates/synth-verify/Cargo.toml
+++ b/crates/synth-verify/Cargo.toml
@@ -22,17 +22,21 @@ arm = ["synth-synthesis"]
 
 [dependencies]
 # Core dependencies (always required)
-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" }
 
 # ARM synthesis (optional, behind 'arm' feature)
-synth-synthesis = { path = "../synth-synthesis", version = "0.49.0", optional = true }
+synth-synthesis = { path = "../synth-synthesis", version = "0.50.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);
 # 0.9.1 adds the float→int trunc trap classifier (`trap_trunc`, ordeal#59/TR-020).
-ordeal = "0.12.0"
+# PINNED at 0.9.1: the 0.12.0 bump (#825) has a bvsrem/bvsdiv solver-performance
+# regression that HANGS div/rem trap-preservation VCs (4-6h CI timeouts, #849).
+# Re-adopt only once the perf regression is fixed upstream AND native i64 rem
+# (#844/#848) re-lands behind a per-query timeout. Do NOT let dependabot bump this.
+ordeal = "=0.9.1"
 
 # Z3: optional differential oracle (feature `z3-solver`) — no longer default.
 # Default features only (NO `static-link-z3`/`bundled`): z3-sys links the
diff --git a/crates/synth-verify/src/arm_semantics.rs b/crates/synth-verify/src/arm_semantics.rs
index c1bc53bc..ff28bfd3 100644
--- a/crates/synth-verify/src/arm_semantics.rs
+++ b/crates/synth-verify/src/arm_semantics.rs
@@ -689,73 +689,20 @@ impl ArmSemantics {
                 state.set_reg(rdhi, BV::new_const("i64_divu_hi", 32));
             }
 
-            ArmOp::I64RemS {
-                rdlo,
-                rdhi,
-                rnlo,
-                rnhi,
-                rmlo,
-                rmhi,
-                ..
-            } => {
-                // Signed 64-bit remainder (modulo). Same shape as I64RemU but
-                // the SIGNED remainder (`bvsrem`, SMT-LIB sign-of-dividend). The
-                // shipped lowering is an `__aeabi_ldivmod` library call; the
-                // value it must produce is exactly the native 64-bit signed
-                // remainder. The value VC (`verify_i64_rem_value_preservation`)
-                // asserts the R0:R1 pair equals it on the non-trapping path.
-                // rem_s traps ONLY on ÷0 (`rem_s(INT64_MIN,-1) == 0`, no
-                // overflow trap).
-                let n_lo = state.get_reg(rnlo).clone();
-                let n_hi = state.get_reg(rnhi).clone();
-                let m_lo = state.get_reg(rmlo).clone();
-                let m_hi = state.get_reg(rmhi).clone();
-
-                let dividend = n_hi.concat(&n_lo); // 64-bit: n_hi:n_lo
-                let divisor = m_hi.concat(&m_lo); // 64-bit: m_hi:m_lo
-                let rem = dividend.bvsrem(&divisor); // native signed rem, 64-bit
-
-                state.set_reg(rdlo, rem.extract(31, 0));
-                state.set_reg(rdhi, rem.extract(63, 32));
+            ArmOp::I64RemS { rdlo, rdhi, .. } => {
+                // Signed 64-bit remainder (modulo)
+                // Real implementation would require __aeabi_ldivmod or equivalent
+                // For verification, return symbolic values
+                state.set_reg(rdlo, BV::new_const("i64_rems_lo", 32));
+                state.set_reg(rdhi, BV::new_const("i64_rems_hi", 32));
             }
 
-            ArmOp::I64RemU {
-                rdlo,
-                rdhi,
-                rnlo,
-                rnhi,
-                rmlo,
-                rmhi,
-                ..
-            } => {
-                // Unsigned 64-bit remainder (modulo). ARM32 has no 64-bit
-                // divide instruction — the shipped lowering expands this
-                // pseudo-op to an `__aeabi_uldivmod` library call — but for
-                // translation-validation the *value* the call must produce is
-                // exactly the native 64-bit unsigned remainder. Model it with
-                // the native `BvTerm::Urem` (ordeal 0.12, plumbed via
-                // `BV::bvurem`) instead of a HAVOC constant, so the value VC
-                // (`verify_i64_rem_value_preservation`) proves the register
-                // pair actually equals `dividend % divisor`.
-                //
-                // Compose the 64-bit operands from their register halves
-                // (`concat` puts self in the HIGH bits), take the 64-bit
-                // unsigned remainder, and split back to lo/hi. On a zero
-                // divisor SMT-LIB `bvurem` is total (returns the dividend),
-                // but WASM traps — the value clause is asserted only on the
-                // non-trapping path by the trap-guarded value VC, so this
-                // total model is sound.
-                let n_lo = state.get_reg(rnlo).clone();
-                let n_hi = state.get_reg(rnhi).clone();
-                let m_lo = state.get_reg(rmlo).clone();
-                let m_hi = state.get_reg(rmhi).clone();
-
-                let dividend = n_hi.concat(&n_lo); // 64-bit: n_hi:n_lo
-                let divisor = m_hi.concat(&m_lo); // 64-bit: m_hi:m_lo
-                let rem = dividend.bvurem(&divisor); // native bvurem, 64-bit
-
-                state.set_reg(rdlo, rem.extract(31, 0)); // low 32 bits
-                state.set_reg(rdhi, rem.extract(63, 32)); // high 32 bits
+            ArmOp::I64RemU { rdlo, rdhi, .. } => {
+                // Unsigned 64-bit remainder (modulo)
+                // Real implementation would require __aeabi_uldivmod or equivalent
+                // For verification, return symbolic values
+                state.set_reg(rdlo, BV::new_const("i64_remu_lo", 32));
+                state.set_reg(rdhi, BV::new_const("i64_remu_hi", 32));
             }
 
             ArmOp::I64And {
@@ -2738,18 +2685,6 @@ impl ArmSemantics {
                 Ok(())
             }
             ArmOp::Strb { .. } | ArmOp::Strh { .. } => Ok(()),
-            // i64 rem_u/rem_s pseudo-ops (VCR-VER, #825/#836): register-only
-            // (they set the `rd*` pair), so they belong in this subset — the
-            // executor delegates to the general value model, which now builds a
-            // real `BvTerm::Urem`/`bvsrem` term. The ÷0 TRAP is NOT derived
-            // here (the bare pseudo-op carries no `UDF`); the VC reconstructs
-            // it from the pseudo-op's `elide_zero_guard` field, exactly like
-            // the i64 trap-only VC. div_u/div_s stay OUT (their 64-bit quotient
-            // value model is havoc — no value VC consumes it).
-            ArmOp::I64RemU { .. } | ArmOp::I64RemS { .. } => {
-                self.encode_op(op, state);
-                Ok(())
-            }
             other => Err(format!(
                 "op {other:?} outside the trap-derivation subset — loud decline"
             )),
diff --git a/crates/synth-verify/src/solver.rs b/crates/synth-verify/src/solver.rs
index 40724a4a..dbc70c1c 100644
--- a/crates/synth-verify/src/solver.rs
+++ b/crates/synth-verify/src/solver.rs
@@ -187,7 +187,6 @@ mod z3_backend {
             BvTerm::Sub(a, b) => bv_to_z3(a).bvsub(&bv_to_z3(b)),
             BvTerm::Mul(a, b) => bv_to_z3(a).bvmul(&bv_to_z3(b)),
             BvTerm::Udiv(a, b) => bv_to_z3(a).bvudiv(&bv_to_z3(b)),
-            BvTerm::Urem(a, b) => bv_to_z3(a).bvurem(&bv_to_z3(b)),
             BvTerm::And(a, b) => bv_to_z3(a).bvand(&bv_to_z3(b)),
             BvTerm::Or(a, b) => bv_to_z3(a).bvor(&bv_to_z3(b)),
             BvTerm::Xor(a, b) => bv_to_z3(a).bvxor(&bv_to_z3(b)),
diff --git a/crates/synth-verify/src/term.rs b/crates/synth-verify/src/term.rs
index 8a42f03d..9b16d1e4 100644
--- a/crates/synth-verify/src/term.rs
+++ b/crates/synth-verify/src/term.rs
@@ -64,7 +64,6 @@ fn bv_rank(t: &BvTerm) -> u8 {
         BvTerm::Sub(..) => 3,
         BvTerm::Mul(..) => 4,
         BvTerm::Udiv(..) => 5,
-        BvTerm::Urem(..) => 5,
         BvTerm::And(..) => 6,
         BvTerm::Or(..) => 7,
         BvTerm::Xor(..) => 8,
@@ -236,10 +235,6 @@ fn canonicalize_bv(t: &BvTerm) -> BvTerm {
             let (a, b) = bin(a, b);
             BvTerm::Udiv(a, b)
         }
-        BvTerm::Urem(a, b) => {
-            let (a, b) = bin(a, b);
-            BvTerm::Urem(a, b)
-        }
         BvTerm::Shl(a, b) => {
             let (a, b) = bin(a, b);
             BvTerm::Shl(a, b)
@@ -848,7 +843,6 @@ fn fmt_bv(t: &BvTerm, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         BvTerm::Sub(a, b) => fmt_bin(f, "bvsub", a, b),
         BvTerm::Mul(a, b) => fmt_bin(f, "bvmul", a, b),
         BvTerm::Udiv(a, b) => fmt_bin(f, "bvudiv", a, b),
-        BvTerm::Urem(a, b) => fmt_bin(f, "bvurem", a, b),
         BvTerm::And(a, b) => fmt_bin(f, "bvand", a, b),
         BvTerm::Or(a, b) => fmt_bin(f, "bvor", a, b),
         BvTerm::Xor(a, b) => fmt_bin(f, "bvxor", a, b),
diff --git a/crates/synth-verify/src/translation_validator.rs b/crates/synth-verify/src/translation_validator.rs
index b39fc216..7cd3cf9c 100644
--- a/crates/synth-verify/src/translation_validator.rs
+++ b/crates/synth-verify/src/translation_validator.rs
@@ -382,17 +382,7 @@ impl TranslationValidator {
             WasmOp::I32DivS | WasmOp::I32DivU | WasmOp::I32RemS | WasmOp::I32RemU => {
                 self.verify_div_rem_trap_preservation(wasm_op, arm_ops)
             }
-            // i64 rem_u/rem_s carry a REAL value model now (native
-            // `BvTerm::Urem`/`bvsrem` — VCR-VER, #825/#836): the VC asserts
-            // both the ÷0 trap AND the 64-bit remainder value, so a lowering
-            // that computes the wrong remainder — or writes it to the wrong
-            // register pair — is rejected. i64 div still leaves its 64-bit
-            // quotient symbolic (the full quotient value VC is not well-posed
-            // in QF_BV at that width), so it stays trap-condition-only.
-            WasmOp::I64RemU | WasmOp::I64RemS => {
-                self.verify_i64_rem_value_preservation(wasm_op, arm_ops)
-            }
-            WasmOp::I64DivS | WasmOp::I64DivU => {
+            WasmOp::I64DivS | WasmOp::I64DivU | WasmOp::I64RemS | WasmOp::I64RemU => {
                 self.verify_i64_div_rem_trap_preservation(wasm_op, arm_ops)
             }
             WasmOp::Unreachable => {
@@ -641,119 +631,6 @@ impl TranslationValidator {
         Ok(Self::condition_verdict(&wasm_trap, &arm_trap))
     }
 
-    /// i64 `rem_u`/`rem_s` **value + trap** preservation (VCR-VER, #825/#836).
-    ///
-    /// Unlike [`Self::verify_i64_div_rem_trap_preservation`] (trap-only, used
-    /// for div where the 64-bit quotient value VC is not well-posed), this
-    /// gate asserts the FULL obligation for remainder: on the non-trapping
-    /// path the ARM register pair `R0:R1` must equal the native 64-bit
-    /// unsigned/signed remainder of the operands, AND the ÷0 trap must be
-    /// preserved. It is what makes the [`ArmSemantics`] `I64RemU` model —
-    /// which now builds a real `BvTerm::Urem` term (ordeal 0.12) instead of
-    /// HAVOC — actually load-bearing: a wrong remainder computation, or one
-    /// that writes the answer to the wrong register pair, is now `Invalid`.
-    ///
-    /// # Operand / result convention (the shipped ABI, NOT the op's fields)
-    ///
-    /// The value is READ from the FIXED ABI return registers `R0` (low) /
-    /// `R1` (high) and the operands are SEEDED at the FIXED ABI argument
-    /// registers — dividend `R0:R1`, divisor `R2:R3`. Reading the op's own
-    /// `rd*` fields (or seeding its own `rn*`/`rm*`) would make the VC
-    /// vacuous (read tracks write); anchoring on the ABI is exactly what lets
-    /// a pseudo-op whose destination deviates from `R0:R1` be REJECTED.
-    ///
-    /// # Trap-guarded value (why not a raw `==`)
-    ///
-    /// A bare `arm_value == wasm_value` would also assert the value on the ÷0
-    /// path, where WASM has no value and SMT-LIB `bvurem`-by-0 = the dividend
-    /// (total) — a spurious obligation. Routing through
-    /// [`crate::trap::DefineOrTrap`] + [`crate::trap::prove_trap_equivalence`]
-    /// guards the value clause under non-trap. The single branch-free
-    /// pseudo-op keeps the value ite-free, so no straight-line rewrite is
-    /// needed (unlike the i32 guarded-div machinery).
-    pub fn verify_i64_rem_value_preservation(
-        &self,
-        wasm_op: &WasmOp,
-        arm_ops: &[ArmOp],
-    ) -> Result<ValidationResult, VerificationError> {
-        let Some(div_op) = crate::trap::div_op(wasm_op) else {
-            return Err(VerificationError::UnsupportedOperation(format!(
-                "i64 rem value gate applies to rem only, got {wasm_op:?}"
-            )));
-        };
-        if !matches!(wasm_op, WasmOp::I64RemU | WasmOp::I64RemS) {
-            return Err(VerificationError::UnsupportedOperation(format!(
-                "i64 rem value gate supports i64 rem_u/rem_s only, got {wasm_op:?}"
-            )));
-        }
-
-        // Require the pseudo-op to be present and read its ÷0 guard-elision
-        // field (the selector emits exactly one). The ARM trap term is
-        // reconstructed from this field — NOT from `encode_sequence_br`'s
-        // `may_trap`, which is `false` for a bare pseudo-op (it carries no
-        // expanded `UDF`) — exactly as the i64 trap-only VC does. A lowering
-        // that elides the ÷0 guard without discharging `divisor != 0` yields a
-        // strictly weaker ARM trap and is rejected.
-        let Some((elide_zero, _elide_overflow)) = Self::i64_div_rem_guard_fields(arm_ops) else {
-            return Err(VerificationError::UnsupportedOperation(format!(
-                "i64 rem value gate needs an I64Rem pseudo-op in the sequence, \
-                 got {arm_ops:?}"
-            )));
-        };
-
-        // Four independent 32-bit half-symbols. Seed them at the FIXED ABI
-        // argument registers: dividend lo:hi = R0:R1, divisor lo:hi = R2:R3.
-        let dividend_lo = BV::new_const("input_dividend_lo", 32);
-        let dividend_hi = BV::new_const("input_dividend_hi", 32);
-        let divisor_lo = BV::new_const("input_divisor_lo", 32);
-        let divisor_hi = BV::new_const("input_divisor_hi", 32);
-
-        let mut state = ArmState::new_symbolic();
-        state.set_reg(&Reg::R0, dividend_lo.clone());
-        state.set_reg(&Reg::R1, dividend_hi.clone());
-        state.set_reg(&Reg::R2, divisor_lo.clone());
-        state.set_reg(&Reg::R3, divisor_hi.clone());
-        self.arm_encoder
-            .encode_sequence_br(arm_ops, &mut state)
-            .map_err(VerificationError::UnsupportedOperation)?;
-
-        // ARM result read from the FIXED ABI return pair R0:R1 (concat puts
-        // self in the HIGH bits).
-        let arm_lo = self.arm_encoder.extract_result(&state, &Reg::R0);
-        let arm_hi = self.arm_encoder.extract_result(&state, &Reg::R1);
-        let arm_value = arm_hi.concat(&arm_lo); // 64-bit R1:R0
-
-        // WASM spec side: the 64-bit remainder of the SAME operand symbols.
-        // Both sides feed identical concats, so the valid case is structural.
-        let dividend = dividend_hi.concat(&dividend_lo); // 64-bit
-        let divisor = divisor_hi.concat(&divisor_lo); // 64-bit
-        let wasm_value = match wasm_op {
-            WasmOp::I64RemU => dividend.bvurem(&divisor),
-            WasmOp::I64RemS => dividend.bvsrem(&divisor),
-            _ => unreachable!("guarded above"),
-        };
-        let wasm_trap = crate::trap::trap_div(div_op, &dividend, &divisor);
-
-        // ARM trap: rem's only trap is ÷0; present iff the guard was NOT
-        // elided. rem carries no overflow clause, so `elide_overflow=false`.
-        let arm_may_trap = Self::i64_arm_trap_from_fields(
-            div_op, &dividend, &divisor, elide_zero, /* elide_overflow */ false,
-        );
-
-        let orig = crate::trap::DefineOrTrap {
-            value: wasm_value,
-            may_trap: wasm_trap,
-        };
-        let opt = crate::trap::DefineOrTrap {
-            value: arm_value,
-            may_trap: arm_may_trap,
-        };
-
-        Ok(Self::trap_verdict_to_result(
-            crate::trap::prove_trap_equivalence(&orig, &opt),
-        ))
-    }
-
     /// Locate the i64 div/rem pseudo-op in a sequence and read its guard-elision
     /// fields as `(elide_zero, elide_overflow)`. `div_u`/`rem_s`/`rem_u` have no
     /// overflow guard, so their `elide_overflow` is reported `false`
@@ -2137,146 +2014,6 @@ mod tests {
         });
     }
 
-    // --- i64 rem VALUE model (VCR-VER, #825/#836): native BvTerm::Urem ---
-    //
-    // The i64 rem_u/rem_s VC now asserts the VALUE, not just the trap. Under
-    // the old HAVOC model the register result was an unconstrained fresh
-    // symbol, so ANY lowering (correct, wrong-remainder, wrong-destination)
-    // trivially satisfied a value-only obligation — the model proved nothing.
-    // These tests pin the value model as load-bearing.
-
-    /// Build an i64 rem pseudo-op with a chosen DESTINATION register pair. The
-    /// shipped ABI is `rd = R0:R1`; a lowering that writes elsewhere leaves
-    /// R0:R1 unrelated to the remainder and must be REJECTED by the value VC.
-    fn i64_rem_with_dest(op: &WasmOp, rdlo: Reg, rdhi: Reg) -> Vec<ArmOp> {
-        let arm = match op {
-            WasmOp::I64RemU => ArmOp::I64RemU {
-                rdlo,
-                rdhi,
-                rnlo: Reg::R0,
-                rnhi: Reg::R1,
-                rmlo: Reg::R2,
-                rmhi: Reg::R3,
-                elide_zero_guard: false,
-            },
-            WasmOp::I64RemS => ArmOp::I64RemS {
-                rdlo,
-                rdhi,
-                rnlo: Reg::R0,
-                rnhi: Reg::R1,
-                rmlo: Reg::R2,
-                rmhi: Reg::R3,
-                elide_zero_guard: false,
-            },
-            _ => unreachable!("i64_rem_with_dest: not an i64 rem op"),
-        };
-        vec![arm]
-    }
-
-    /// GREEN: the shipped rem_u/rem_s lowering (`rd = R0:R1`) computes the
-    /// correct 64-bit remainder into the ABI return pair — the value+trap VC
-    /// must be Verified.
-    #[test]
-    fn i64_rem_shipped_value_is_verified() {
-        with_verification_context(|| {
-            let validator = TranslationValidator::new();
-            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
-                let arm_ops = shipped_i64_div_rem(&op, false, false);
-                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
-                assert_eq!(
-                    result,
-                    ValidationResult::Verified,
-                    "GREEN: {op:?} shipped lowering (correct value + ÷0 guard) must be Verified"
-                );
-            }
-        });
-    }
-
-    /// RED / NON-VACUITY (the key gate): a lowering that writes the remainder
-    /// to the WRONG destination pair (`rd = R2:R3` instead of the ABI `R0:R1`)
-    /// leaves R0:R1 holding the (unrelated) input operands, so the ABI return
-    /// pair is NOT the remainder. Under the old HAVOC model this was ACCEPTED
-    /// (the result symbol was unconstrained); the native `BvTerm::Urem` value
-    /// model now REJECTS it. This is the accepted-under-havoc → rejected-now
-    /// discriminator.
-    #[test]
-    fn i64_rem_wrong_destination_register_is_rejected() {
-        with_verification_context(|| {
-            let validator = TranslationValidator::new();
-            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
-                let arm_ops = i64_rem_with_dest(&op, Reg::R2, Reg::R3);
-                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
-                assert!(
-                    matches!(result, ValidationResult::Invalid { .. }),
-                    "RED: {op:?} writing the remainder to R2:R3 (not the ABI R0:R1) \
-                     leaves R0:R1 non-remainder — must be Invalid, got {result:?}"
-                );
-            }
-        });
-    }
-
-    /// NON-VACUITY control: the correct-destination and wrong-destination
-    /// lowerings must give OPPOSITE verdicts. A gate that returned the same
-    /// verdict for both (as the HAVOC model did — both trivially valued) would
-    /// be vacuous.
-    #[test]
-    fn i64_rem_destination_field_is_load_bearing() {
-        with_verification_context(|| {
-            let validator = TranslationValidator::new();
-            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
-                let correct = validator
-                    .verify_trap_preservation(&op, &i64_rem_with_dest(&op, Reg::R0, Reg::R1))
-                    .unwrap();
-                let wrong = validator
-                    .verify_trap_preservation(&op, &i64_rem_with_dest(&op, Reg::R2, Reg::R3))
-                    .unwrap();
-                assert_eq!(correct, ValidationResult::Verified, "{op:?} correct dest");
-                assert!(
-                    matches!(wrong, ValidationResult::Invalid { .. }),
-                    "{op:?} wrong dest"
-                );
-                assert_ne!(
-                    correct, wrong,
-                    "non-vacuity: {op:?} destination register must change the verdict"
-                );
-            }
-        });
-    }
-
-    /// EVIDENCE that the value model closed a real gap: the OLD trap-only VC
-    /// (`verify_i64_div_rem_trap_preservation`, still present for div) ACCEPTS
-    /// the wrong-destination rem lowering — it never reads the value — whereas
-    /// the NEW value VC (`verify_i64_rem_value_preservation`, dispatched by
-    /// `verify_trap_preservation`) REJECTS it. Opposite verdicts from the two
-    /// gates on the same input is the accepted-under-havoc → rejected-now
-    /// proof, made concrete rather than merely narrated.
-    #[test]
-    fn i64_rem_value_model_closes_a_trap_only_gap() {
-        with_verification_context(|| {
-            let validator = TranslationValidator::new();
-            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
-                let wrong = i64_rem_with_dest(&op, Reg::R2, Reg::R3);
-                // Old trap-only path: value/destination invisible → accepted.
-                let trap_only = validator
-                    .verify_i64_div_rem_trap_preservation(&op, &wrong)
-                    .unwrap();
-                assert_eq!(
-                    trap_only,
-                    ValidationResult::Verified,
-                    "the trap-ONLY VC is blind to the wrong destination (this is the \
-                     havoc-era gap): {op:?} expected Verified, got {trap_only:?}"
-                );
-                // New value+trap path: destination is load-bearing → rejected.
-                let value = validator.verify_trap_preservation(&op, &wrong).unwrap();
-                assert!(
-                    matches!(value, ValidationResult::Invalid { .. }),
-                    "the value VC catches it: {op:?} expected Invalid, got {value:?}"
-                );
-                assert_ne!(trap_only, value, "the two gates must disagree ({op:?})");
-            }
-        });
-    }
-
     // --- call_indirect (LIVE at the pseudo-op guard level, #642/#664/#676) ---
 
     fn call_indirect_pseudo(
diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md
index 0f710094..e437a66e 100644
--- a/docs/status/FEATURE_MATRIX.md
+++ b/docs/status/FEATURE_MATRIX.md
@@ -7,7 +7,7 @@
 > stale. All numbers come from [`artifacts/status.json`](../../artifacts/status.json),
 > which is re-derived from source on every run — never hand-edited.
 
-**Workspace version:** 0.49.0
+**Workspace version:** 0.50.0
 
 ---
 
diff --git a/npm/package.json b/npm/package.json
index 6d01a9d6..371eda0b 100644
--- a/npm/package.json
+++ b/npm/package.json
@@ -1,6 +1,6 @@
 {
   "name": "@pulseengine/synth",
-  "version": "0.49.0",
+  "version": "0.50.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"