diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c03bf719..d58790c7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -1467,3 +1467,38 @@ jobs:
           SYNTH: ./target/debug/synth
           EXTRA_SYNTH_FLAGS: "--stack-layout low"
         run: python scripts/repro/i64_global_init_649_differential.py
+
+  # #418: self-contained binding of the meld-dissolve embedder import
+  # `env::__cabi_arena_realloc` — the compile must yield an ET_EXEC image
+  # (not a "link me" ET_REL) whose synthesized arena allocator EXECUTES the
+  # canonical-ABI realloc contract identically to a wasmtime host arena
+  # (pointer-independent observables; exhaustion traps on both sides). The
+  # `--relocatable` undefined-symbol seam (#420) is asserted untouched by
+  # cabi_arena_realloc_linkability_418.rs in the `test` job.
+  arena-bind-418-oracle:
+    name: "#418 arena-bind self-contained execution oracle"
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Cache Cargo dependencies
+        uses: actions/cache@v6
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-
+      - name: Build synth
+        run: cargo build -p synth-cli
+      - uses: actions/setup-python@v6
+        with:
+          python-version: "3.x"
+      - name: Install emulation deps
+        run: pip install wasmtime unicorn pyelftools
+      - name: Run the #418 arena-bind execution differential
+        env:
+          SYNTH: ./target/debug/synth
+        run: python scripts/repro/cabi_arena_bind_418_differential.py
diff --git a/.gitignore b/.gitignore
index b0578e11..d886e0eb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -72,3 +72,4 @@ result-*
 # Stray ELF/object output at repo root (e.g. `synth compile ... -o output.elf`)
 /*.elf
 output.elf
+__pycache__/
diff --git a/Cargo.lock b/Cargo.lock
index 36a4c90c..605d3e88 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1205,6 +1205,7 @@ dependencies = [
  "serde_json",
  "sha2 0.11.0",
  "thiserror",
+ "wasm-encoder 0.253.0",
  "wasmparser 0.253.0",
  "wat",
 ]
diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs
index 1df8a7b1..41b06075 100644
--- a/crates/synth-cli/src/main.rs
+++ b/crates/synth-cli/src/main.rs
@@ -337,6 +337,13 @@ enum Commands {
         #[arg(long)]
         native_pointer_abi: bool,
 
+        /// #418: keep a sole `env::__cabi_arena_realloc` import an EXTERNAL
+        /// symbol (ET_REL, host-linked) instead of binding it to a synthesized
+        /// in-image arena allocator on the self-contained Cortex-M path — the
+        /// pinned opt-out restoring the pre-binding pass-through.
+        #[arg(long)]
+        no_bind_cabi_arena: bool,
+
         /// Emit a CycloneDX 1.5 SBOM for the compiled ELF. With a path, writes
         /// there; as a bare flag (`--sbom`) writes `<output>.cdx.json` next to
         /// the ELF. The SBOM documents the synth compiler, the input WASM, the
@@ -595,6 +602,7 @@ fn main() -> Result<()> {
             builtins,
             relocatable,
             native_pointer_abi,
+            no_bind_cabi_arena,
             sbom,
             sign_output,
             shadow_stack_size,
@@ -674,6 +682,7 @@ fn main() -> Result<()> {
                 &target_spec,
                 relocatable,
                 native_pointer_abi,
+                no_bind_cabi_arena,
                 sbom_path,
                 sign_output,
                 shadow_stack_size,
@@ -1407,6 +1416,8 @@ fn compile_command(
     target_spec: &TargetSpec,
     relocatable: bool,
     native_pointer_abi: bool,
+    // #418: `--no-bind-cabi-arena` — keep the arena import an external symbol.
+    no_bind_cabi_arena: bool,
     sbom_path: Option<PathBuf>,
     sign_output: bool,
     shadow_stack_size: Option<u32>,
@@ -1470,6 +1481,7 @@ fn compile_command(
             target_spec,
             relocatable,
             native_pointer_abi,
+            no_bind_cabi_arena,
             sbom_path,
             sign_output,
             shadow_stack_size,
@@ -2510,6 +2522,9 @@ fn compile_all_exports(
     target_spec: &TargetSpec,
     relocatable: bool,
     native_pointer_abi: bool,
+    // #418: `--no-bind-cabi-arena` — keep a sole `env::__cabi_arena_realloc`
+    // import an external symbol instead of binding it in-image.
+    no_bind_cabi_arena: bool,
     sbom_path: Option<PathBuf>,
     sign_output: bool,
     shadow_stack_size: Option<u32>,
@@ -2711,6 +2726,45 @@ fn compile_all_exports(
         // Run Loom optimizer if --loom is enabled
         let wasm_bytes = maybe_run_loom(loom, wasm_bytes)?;
 
+        // #418: on the SELF-CONTAINED Cortex-M path, bind a sole passed-through
+        // `env::__cabi_arena_realloc` embedder import (the wit-bindgen
+        // `cabi-realloc-extern` / meld-dissolve shape) to a synthesized
+        // in-module arena allocator, so the compile yields a fully
+        // self-contained image instead of degrading to an ET_REL "link me
+        // with the Kiln bridge" object. The `--relocatable` host-link seam is
+        // UNTOUCHED (#420 contract: undefined `__cabi_arena_realloc` symbol,
+        // TCB-bound at native link), as is `--native-pointer-abi` (its
+        // SP-global register promotion could misidentify the appended arena
+        // cursor global). Modules without the import pass through
+        // byte-identically. Pinned opt-out: `--no-bind-cabi-arena`.
+        let wasm_bytes = if cortex_m
+            && !relocatable
+            && !native_pointer_abi
+            && backend.name() == "arm"
+            && !no_bind_cabi_arena
+        {
+            match synth_core::arena_bind::bind_cabi_arena_realloc(&wasm_bytes)? {
+                synth_core::arena_bind::ArenaBind::Bound(b) => {
+                    info!(
+                        "#418: bound env::__cabi_arena_realloc to a synthesized in-image \
+                         arena allocator: wasm [0x{:x}, 0x{:x}) ({} bytes, traps on \
+                         exhaustion; opt-out --no-bind-cabi-arena)",
+                        b.arena_base,
+                        b.arena_end,
+                        b.arena_end - b.arena_base
+                    );
+                    b.bytes
+                }
+                synth_core::arena_bind::ArenaBind::KeptHostSeam(reason) => {
+                    info!("#418: env::__cabi_arena_realloc NOT bound: {reason}");
+                    wasm_bytes
+                }
+                synth_core::arena_bind::ArenaBind::NoArenaImport => wasm_bytes,
+            }
+        } else {
+            wasm_bytes
+        };
+
         let module = decode_wasm_module(&wasm_bytes).context("Failed to decode WASM module")?;
         sbom_wasm_bytes = Some(wasm_bytes);
 
diff --git a/crates/synth-cli/tests/cabi_arena_bind_418.rs b/crates/synth-cli/tests/cabi_arena_bind_418.rs
new file mode 100644
index 00000000..2b774f3b
--- /dev/null
+++ b/crates/synth-cli/tests/cabi_arena_bind_418.rs
@@ -0,0 +1,181 @@
+//! synth#418 — SELF-CONTAINED binding of `env::__cabi_arena_realloc`.
+//!
+//! Companion to `cabi_arena_realloc_linkability_418.rs` (which locks the
+//! `--relocatable` seam: an UNDEFINED symbol the TCB satisfies at native
+//! link). This file locks the OTHER half of #418: on the default
+//! self-contained Cortex-M path a sole arena import is bound to a synthesized
+//! in-module allocator, producing an ET_EXEC image with no external seam —
+//! plus the decline matrix around that binding. Execution correctness is
+//! gated by `scripts/repro/cabi_arena_bind_418_differential.py` (CI job
+//! `arena-bind-418-oracle`).
+
+use std::path::PathBuf;
+use std::process::Command;
+
+use object::read::elf::ElfFile32;
+use object::{Object, ObjectSymbol};
+
+fn synth() -> &'static str {
+    env!("CARGO_BIN_EXE_synth")
+}
+
+fn fixture() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../..")
+        .join("scripts/repro/cabi_arena_bind.wat")
+}
+
+/// ELF e_type from the raw header (1 = ET_REL, 2 = ET_EXEC).
+fn e_type(data: &[u8]) -> u16 {
+    u16::from_le_bytes([data[16], data[17]])
+}
+
+fn compile(args: &[&str], out: &str) -> std::process::Output {
+    let mut cmd = Command::new(synth());
+    cmd.args(["compile", fixture().to_str().unwrap()])
+        .args(args)
+        .args(["--target", "cortex-m3", "--all-exports", "-o", out])
+        // The binding log line is part of the asserted surface below;
+        // INFO-level tracing is off by default in a non-TTY test run.
+        .env("RUST_LOG", "info");
+    cmd.output().expect("run synth")
+}
+
+fn has_undefined_arena(data: &[u8]) -> bool {
+    let obj = ElfFile32::<object::Endianness>::parse(data).expect("parse ELF");
+    obj.symbols()
+        .any(|s| s.name() == Ok("__cabi_arena_realloc") && s.is_undefined())
+}
+
+/// Default self-contained compile: the arena import is BOUND — the output is
+/// an executable image with no `__cabi_arena_realloc` seam left.
+#[test]
+fn self_contained_binds_arena_import_418() {
+    let out = "/tmp/cabi_arena_bind_418_default.elf";
+    let r = compile(&[], out);
+    assert!(
+        r.status.success(),
+        "compile failed: {}",
+        String::from_utf8_lossy(&r.stderr)
+    );
+    // tracing INFO may land on either stream depending on subscriber config.
+    let logs = format!(
+        "{}{}",
+        String::from_utf8_lossy(&r.stdout),
+        String::from_utf8_lossy(&r.stderr)
+    );
+    assert!(
+        logs.contains("#418: bound env::__cabi_arena_realloc"),
+        "expected the #418 binding log line, got: {logs}"
+    );
+    let data = std::fs::read(out).unwrap();
+    assert_eq!(
+        e_type(&data),
+        2,
+        "bound module must be a self-contained ET_EXEC image, not a link-me object"
+    );
+    assert!(
+        !has_undefined_arena(&data),
+        "no undefined __cabi_arena_realloc may remain in the bound image"
+    );
+}
+
+/// The pinned opt-out restores the pass-through: ET_REL with the undefined
+/// external symbol (the embedder seam), byte-compatible with the old behavior.
+#[test]
+fn opt_out_restores_external_seam_418() {
+    let out = "/tmp/cabi_arena_bind_418_optout.elf";
+    let r = compile(&["--no-bind-cabi-arena"], out);
+    assert!(
+        r.status.success(),
+        "compile failed: {}",
+        String::from_utf8_lossy(&r.stderr)
+    );
+    let data = std::fs::read(out).unwrap();
+    assert_eq!(
+        e_type(&data),
+        1,
+        "opt-out must produce ET_REL (host-linked)"
+    );
+    assert!(
+        has_undefined_arena(&data),
+        "opt-out must keep __cabi_arena_realloc an UNDEFINED external symbol"
+    );
+}
+
+/// `--relocatable` keeps the #420 layering untouched: synth references, the
+/// TCB provides, the linker binds — no in-image allocator.
+#[test]
+fn relocatable_keeps_tcb_seam_418() {
+    let out = "/tmp/cabi_arena_bind_418_reloc.elf";
+    let r = compile(&["--relocatable"], out);
+    assert!(
+        r.status.success(),
+        "compile failed: {}",
+        String::from_utf8_lossy(&r.stderr)
+    );
+    let data = std::fs::read(out).unwrap();
+    assert_eq!(e_type(&data), 1);
+    assert!(
+        has_undefined_arena(&data),
+        "--relocatable must keep the undefined TCB-bound symbol (#420 contract)"
+    );
+}
+
+/// A wrong-signature arena import is NOT the documented contract: the compile
+/// refuses loudly instead of guessing an ABI (honest degradation).
+#[test]
+fn wrong_signature_declines_loudly_418() {
+    let wat = r#"(module
+      (import "env" "__cabi_arena_realloc" (func $a (param i32 i32) (result i32)))
+      (memory 1)
+      (func (export "f") (param i32 i32) (result i32)
+        local.get 0 local.get 1 call $a))"#;
+    let path = std::env::temp_dir().join("cabi_arena_bind_418_bad_sig.wat");
+    std::fs::write(&path, wat).unwrap();
+    let out = "/tmp/cabi_arena_bind_418_bad_sig.elf";
+    let r = Command::new(synth())
+        .args(["compile", path.to_str().unwrap()])
+        .args(["--target", "cortex-m3", "--all-exports", "-o", out])
+        .output()
+        .expect("run synth");
+    assert!(!r.status.success(), "wrong-signature bind must fail loudly");
+    let stderr = String::from_utf8_lossy(&r.stderr);
+    assert!(
+        stderr.contains("#418") && stderr.contains("signature"),
+        "expected the precise #418 signature decline, got: {stderr}"
+    );
+}
+
+/// With OTHER imports alongside the arena import the module cannot
+/// self-contain — the arena import stays on the host-linked seam (pass-through
+/// to ET_REL, undefined symbol), never a half-bound hybrid.
+#[test]
+fn other_imports_keep_host_seam_418() {
+    let wat = r#"(module
+      (import "env" "k_spin_lock" (func (param i32)))
+      (import "env" "__cabi_arena_realloc"
+        (func $a (param i32 i32 i32 i32) (result i32)))
+      (memory 1)
+      (func (export "f") (param i32 i32 i32 i32) (result i32)
+        local.get 0 local.get 1 local.get 2 local.get 3 call $a))"#;
+    let path = std::env::temp_dir().join("cabi_arena_bind_418_mixed.wat");
+    std::fs::write(&path, wat).unwrap();
+    let out = "/tmp/cabi_arena_bind_418_mixed.elf";
+    let r = Command::new(synth())
+        .args(["compile", path.to_str().unwrap()])
+        .args(["--target", "cortex-m3", "--all-exports", "-o", out])
+        .output()
+        .expect("run synth");
+    assert!(
+        r.status.success(),
+        "mixed-import module must still compile (host-linked): {}",
+        String::from_utf8_lossy(&r.stderr)
+    );
+    let data = std::fs::read(out).unwrap();
+    assert_eq!(e_type(&data), 1, "mixed imports keep the ET_REL host seam");
+    assert!(
+        has_undefined_arena(&data),
+        "the arena import must stay an undefined external alongside other imports"
+    );
+}
diff --git a/crates/synth-core/Cargo.toml b/crates/synth-core/Cargo.toml
index ca2c6a41..eb9d33c4 100644
--- a/crates/synth-core/Cargo.toml
+++ b/crates/synth-core/Cargo.toml
@@ -17,6 +17,10 @@ sha2.workspace = true
 thiserror.workspace = true
 anyhow.workspace = true
 wasmparser.workspace = true
+# #418: the arena-bind rewrite (replace the sole `env::__cabi_arena_realloc`
+# import with a synthesized in-module arena allocator). Already listed in the
+# hand-written crates/BUILD.bazel synth-core deps.
+wasm-encoder.workspace = true
 # VCR-DBG-001 Tier-1 step 4 (#394, #242) — the DWARF READER (parse the input
 # wasm's `.debug_line`) and the EMITTER (write the ARM `.debug_line` bytes) are
 # PRODUCTION now, behind the `--debug-line` flag. Bazel's `from_cargo`
diff --git a/crates/synth-core/src/arena_bind.rs b/crates/synth-core/src/arena_bind.rs
new file mode 100644
index 00000000..9d36b408
--- /dev/null
+++ b/crates/synth-core/src/arena_bind.rs
@@ -0,0 +1,715 @@
+//! #418 — bind the passed-through embedder import `env::__cabi_arena_realloc`
+//! to a synthesized in-module arena allocator, unlocking the fully
+//! SELF-CONTAINED dissolve.
+//!
+//! ## The seam this closes
+//!
+//! The BYO-OS lean-MCU dissolve (gale#89) builds grow-free components with the
+//! wit-bindgen `cabi-realloc-extern` feature: `cabi_realloc` stays exported but
+//! its body routes to an embedder-provided `env::__cabi_arena_realloc` import.
+//! On the `--relocatable` host-link path that import is DELIBERATELY left as an
+//! undefined symbol the TCB's native allocator satisfies at link (#420 locks
+//! that layering — nothing here changes it). But on the default SELF-CONTAINED
+//! path the same import previously degraded the compile to an ET_REL "link me
+//! with the Kiln bridge" object: the one unresolved seam blocking a fully
+//! self-contained image.
+//!
+//! ## The binding (a wasm→wasm rewrite, not new codegen)
+//!
+//! When the arena import is the module's ONLY import, replace it with a
+//! DEFINED WebAssembly function implementing the #418 contract, compiled
+//! through synth's ordinary pipeline like any other module function:
+//!
+//! - signature `(old_ptr, old_len, align, new_len) -> ptr` (`i32×4 → i32`);
+//! - `old_len == 0 && new_len == 0` → return `align` verbatim;
+//! - bump allocation from a fresh mutable cursor global (appended at the end
+//!   of the global index space), aligned up per call;
+//! - realloc preserves `min(old_len, new_len)` bytes (byte-copy loop);
+//! - BOUNDED arena `[arena_base, arena_end)` — exhaustion (or a zero /
+//!   non-power-of-two-shaped `align` wrap) executes `unreachable`, i.e. traps,
+//!   and NEVER calls `memory.grow`.
+//!
+//! `arena_base` mirrors the shipped used-extent rule (`main.rs` #237/#354):
+//! `max(data_end, every i32-const global init ≤ linmem)` — the latter covers
+//! both the `__stack_pointer` class and wasm-ld's `__data_end`/`__heap_base`
+//! layout globals — rounded up to 16 (floor 16 so the allocator never returns
+//! a null-looking pointer). `arena_end` = the initial linear-memory size
+//! (grow-free modules never extend it).
+//!
+//! ## Why the rewrite is index-preserving
+//!
+//! The wasm function index space is imports-first. Removing the SOLE function
+//! import and prepending the allocator as the FIRST defined function gives it
+//! the import's old index — every `call`, `ref.func`, export, and element
+//! entry keeps its meaning without any remapping. Untouched sections are
+//! copied byte-for-byte; only import (dropped), function/code (one entry
+//! prepended) and global (one entry appended) change.
+
+use anyhow::{Context, Result, bail};
+use wasm_encoder::{BlockType, Function, MemArg, ValType};
+use wasmparser::{Parser, Payload};
+
+/// The core-module field name of the embedder arena import (#418). The kebab
+/// `cabi-arena-realloc` is component-surface only and never reaches synth.
+pub const ARENA_IMPORT_MODULE: &str = "env";
+pub const ARENA_IMPORT_FIELD: &str = "__cabi_arena_realloc";
+
+/// Outcome of [`bind_cabi_arena_realloc`].
+#[derive(Debug)]
+pub enum ArenaBind {
+    /// No arena import in the module — silent byte-identical pass-through
+    /// (the overwhelmingly common case; not worth a log line).
+    NoArenaImport,
+    /// The arena import is present but the module keeps the host-linked
+    /// seam (reason worth logging); byte-identical pass-through.
+    KeptHostSeam(&'static str),
+    /// The import was bound: compile `bytes` instead of the input.
+    Bound(BoundArena),
+}
+
+/// A successful #418 binding.
+#[derive(Debug)]
+pub struct BoundArena {
+    /// The rewritten module (arena import replaced by a defined allocator).
+    pub bytes: Vec<u8>,
+    /// First allocatable wasm address (16-aligned, above all statics).
+    pub arena_base: u32,
+    /// One past the last allocatable wasm address (= initial memory size).
+    pub arena_end: u32,
+}
+
+/// Everything learned in the analysis pass.
+struct Scan {
+    /// (import type index) when `env::__cabi_arena_realloc` is present.
+    arena_type_idx: Option<u32>,
+    /// Whether the arena import's declared type is `(i32×4) -> i32`.
+    arena_sig_ok: bool,
+    total_imports: u32,
+    /// Initial pages of memory 0, if declared (None = no memory).
+    memory_pages: Option<u64>,
+    memory64: bool,
+    defined_globals: u32,
+    /// Max `off + len` over active i32-const-offset segments on memory 0.
+    data_end: u32,
+    /// A data segment whose offset synth cannot evaluate statically.
+    non_const_data_offset: bool,
+    /// Max i32-const global init (any mutability) — the `__stack_pointer` /
+    /// `__heap_base` / `__data_end` class, filtered to `<= linmem` later.
+    global_inits: Vec<u32>,
+    has_function_section: bool,
+    has_code_section: bool,
+}
+
+fn scan(wasm: &[u8]) -> Result<Scan> {
+    let mut s = Scan {
+        arena_type_idx: None,
+        arena_sig_ok: false,
+        total_imports: 0,
+        memory_pages: None,
+        memory64: false,
+        defined_globals: 0,
+        data_end: 0,
+        non_const_data_offset: false,
+        global_inits: Vec::new(),
+        has_function_section: false,
+        has_code_section: false,
+    };
+    let mut func_types: Vec<bool> = Vec::new(); // per type index: is (i32×4)->i32
+    for payload in Parser::new(0).parse_all(wasm) {
+        match payload.context("parse wasm (#418 arena-bind scan)")? {
+            Payload::TypeSection(reader) => {
+                for rec_group in reader {
+                    for sub_ty in rec_group.context("parse type section (#418)")?.types() {
+                        let ok = match &sub_ty.composite_type.inner {
+                            wasmparser::CompositeInnerType::Func(f) => {
+                                f.params().len() == 4
+                                    && f.params().iter().all(|t| *t == wasmparser::ValType::I32)
+                                    && f.results() == [wasmparser::ValType::I32]
+                            }
+                            _ => false,
+                        };
+                        func_types.push(ok);
+                    }
+                }
+            }
+            Payload::ImportSection(reader) => {
+                // wasmparser 0.221+ compact-imports grouping: flatten back to
+                // individual `Import`s (same idiom as wasm_decoder.rs).
+                for import in reader.into_imports() {
+                    let import = import.context("parse import (#418)")?;
+                    s.total_imports += 1;
+                    if import.module == ARENA_IMPORT_MODULE
+                        && import.name == ARENA_IMPORT_FIELD
+                        && let wasmparser::TypeRef::Func(type_idx) = import.ty
+                    {
+                        s.arena_type_idx = Some(type_idx);
+                        s.arena_sig_ok =
+                            func_types.get(type_idx as usize).copied().unwrap_or(false);
+                    }
+                }
+            }
+            Payload::MemorySection(reader) => {
+                for (i, mem) in reader.into_iter().enumerate() {
+                    let mem = mem.context("parse memory (#418)")?;
+                    if i == 0 {
+                        s.memory_pages = Some(mem.initial);
+                        s.memory64 = mem.memory64;
+                    }
+                }
+            }
+            Payload::GlobalSection(reader) => {
+                for global in reader {
+                    let global = global.context("parse global (#418)")?;
+                    s.defined_globals += 1;
+                    // i32.const inits mark the static layout (SP top,
+                    // __heap_base/__data_end) — mirror the used-extent rule.
+                    let mut ops = global.init_expr.get_operators_reader();
+                    if let Ok(wasmparser::Operator::I32Const { value }) = ops.read()
+                        && value > 0
+                    {
+                        s.global_inits.push(value as u32);
+                    }
+                }
+            }
+            Payload::DataSection(reader) => {
+                for seg in reader {
+                    let seg = seg.context("parse data segment (#418)")?;
+                    if let wasmparser::DataKind::Active {
+                        memory_index,
+                        offset_expr,
+                    } = seg.kind
+                    {
+                        if memory_index != 0 {
+                            continue; // multi-memory declines self-contained anyway
+                        }
+                        let mut ops = offset_expr.get_operators_reader();
+                        match ops.read() {
+                            Ok(wasmparser::Operator::I32Const { value }) => {
+                                let end = (value as u32).saturating_add(seg.data.len() as u32);
+                                s.data_end = s.data_end.max(end);
+                            }
+                            _ => s.non_const_data_offset = true,
+                        }
+                    }
+                }
+            }
+            Payload::FunctionSection(_) => s.has_function_section = true,
+            Payload::CodeSectionStart { .. } => s.has_code_section = true,
+            _ => {}
+        }
+    }
+    Ok(s)
+}
+
+/// Encode the allocator body (the #418 contract — see module docs).
+///
+/// Params: 0 = old_ptr, 1 = old_len, 2 = align, 3 = new_len.
+/// Locals: 4 = aligned, 5 = end, 6 = n (copy length), 7 = i.
+fn allocator_body(cursor_global: u32, arena_end: u32) -> Function {
+    let mem = MemArg {
+        offset: 0,
+        align: 0,
+        memory_index: 0,
+    };
+    let mut f = Function::new([(4, ValType::I32)]);
+    // contract: old_len == 0 && new_len == 0 -> return align verbatim
+    f.instructions()
+        .local_get(1)
+        .i32_eqz()
+        .local_get(3)
+        .i32_eqz()
+        .i32_and()
+        .if_(BlockType::Empty)
+        .local_get(2)
+        .return_()
+        .end()
+        // align == 0 is contract-violating input (power of two >= 1): trap
+        // rather than compute a wrapped mask.
+        .local_get(2)
+        .i32_eqz()
+        .if_(BlockType::Empty)
+        .unreachable()
+        .end()
+        // aligned = (cursor + align - 1) & ~(align - 1)
+        .global_get(cursor_global)
+        .local_get(2)
+        .i32_add()
+        .i32_const(1)
+        .i32_sub()
+        .local_get(2)
+        .i32_const(1)
+        .i32_sub()
+        .i32_const(-1)
+        .i32_xor()
+        .i32_and()
+        .local_set(4)
+        // unsigned wrap while rounding up -> trap
+        .local_get(4)
+        .global_get(cursor_global)
+        .i32_lt_u()
+        .if_(BlockType::Empty)
+        .unreachable()
+        .end()
+        // end = aligned + new_len; unsigned wrap -> trap
+        .local_get(4)
+        .local_get(3)
+        .i32_add()
+        .local_tee(5)
+        .local_get(4)
+        .i32_lt_u()
+        .if_(BlockType::Empty)
+        .unreachable()
+        .end()
+        // BOUNDED arena: end > arena_end -> trap (never memory.grow)
+        .local_get(5)
+        .i32_const(arena_end as i32)
+        .i32_gt_u()
+        .if_(BlockType::Empty)
+        .unreachable()
+        .end()
+        // commit the bump
+        .local_get(5)
+        .global_set(cursor_global)
+        // n = min(old_len, new_len) — realloc preserves the prefix
+        .local_get(1)
+        .local_get(3)
+        .local_get(1)
+        .local_get(3)
+        .i32_lt_u()
+        .select()
+        .local_set(6)
+        // byte-copy loop: dst = aligned + i, src = old_ptr + i, i < n
+        .block(BlockType::Empty)
+        .loop_(BlockType::Empty)
+        .local_get(7)
+        .local_get(6)
+        .i32_ge_u()
+        .br_if(1)
+        .local_get(4)
+        .local_get(7)
+        .i32_add()
+        .local_get(0)
+        .local_get(7)
+        .i32_add()
+        .i32_load8_u(mem)
+        .i32_store8(mem)
+        .local_get(7)
+        .i32_const(1)
+        .i32_add()
+        .local_set(7)
+        .br(0)
+        .end()
+        .end()
+        .local_get(4)
+        .end();
+    f
+}
+
+/// Read a LEB128 u32 from `bytes`, returning (value, length).
+fn read_uleb(bytes: &[u8]) -> Result<(u32, usize)> {
+    let mut value: u32 = 0;
+    let mut shift = 0;
+    for (i, &b) in bytes.iter().enumerate().take(5) {
+        value |= u32::from(b & 0x7F) << shift;
+        if b & 0x80 == 0 {
+            return Ok((value, i + 1));
+        }
+        shift += 7;
+    }
+    bail!("malformed LEB128 count in section (#418)");
+}
+
+fn write_uleb(mut value: u32, out: &mut Vec<u8>) {
+    loop {
+        let mut b = (value & 0x7F) as u8;
+        value >>= 7;
+        if value != 0 {
+            b |= 0x80;
+        }
+        out.push(b);
+        if value == 0 {
+            return;
+        }
+    }
+}
+
+fn write_sleb(mut value: i32, out: &mut Vec<u8>) {
+    loop {
+        let b = (value & 0x7F) as u8;
+        value >>= 7;
+        let sign = b & 0x40;
+        if (value == 0 && sign == 0) || (value == -1 && sign != 0) {
+            out.push(b);
+            return;
+        }
+        out.push(b | 0x80);
+    }
+}
+
+/// A raw section body with one entry PREPENDED (count bumped, existing
+/// entries byte-copied verbatim).
+fn prepend_entry(contents: &[u8], entry: &[u8]) -> Result<Vec<u8>> {
+    let (count, len) = read_uleb(contents)?;
+    let mut out = Vec::with_capacity(contents.len() + entry.len() + 1);
+    write_uleb(count + 1, &mut out);
+    out.extend_from_slice(entry);
+    out.extend_from_slice(&contents[len..]);
+    Ok(out)
+}
+
+/// A raw section body with one entry APPENDED (count bumped, existing
+/// entries byte-copied verbatim).
+fn append_entry(contents: &[u8], entry: &[u8]) -> Result<Vec<u8>> {
+    let (count, len) = read_uleb(contents)?;
+    let mut out = Vec::with_capacity(contents.len() + entry.len() + 1);
+    write_uleb(count + 1, &mut out);
+    out.extend_from_slice(&contents[len..]);
+    out.extend_from_slice(entry);
+    Ok(out)
+}
+
+/// The encoded cursor global entry: `(global (mut i32) (i32.const base))`.
+fn cursor_global_entry(arena_base: u32) -> Vec<u8> {
+    let mut e = vec![0x7F, 0x01, 0x41]; // valtype i32, mutable, i32.const
+    write_sleb(arena_base as i32, &mut e);
+    e.push(0x0B); // end
+    e
+}
+
+/// Bind a sole `env::__cabi_arena_realloc` function import to a synthesized
+/// in-module arena allocator (#418). See the module docs for the contract.
+///
+/// - `Ok(NoArenaImport)` / `Ok(KeptHostSeam)` — pass the original bytes
+///   through byte-identically (the latter: arena import present but the
+///   module has OTHER imports too, so it cannot self-contain regardless).
+/// - `Ok(Bound)` — compile the returned bytes instead.
+/// - `Err` — the arena import is present and this is the self-contained
+///   path, but the module is not soundly bindable: refuse LOUDLY rather
+///   than emit a silently-degraded object.
+pub fn bind_cabi_arena_realloc(wasm: &[u8]) -> Result<ArenaBind> {
+    let s = scan(wasm)?;
+    let Some(arena_type_idx) = s.arena_type_idx else {
+        return Ok(ArenaBind::NoArenaImport);
+    };
+    if s.total_imports > 1 {
+        // Other embedder imports remain — the image cannot self-contain, so
+        // the arena import stays on the documented pass-through seam
+        // (undefined symbol, host-linked) alongside them.
+        return Ok(ArenaBind::KeptHostSeam(
+            "module has other imports — keeping the host-linked seam",
+        ));
+    }
+    if !s.arena_sig_ok {
+        bail!(
+            "#418: env::{ARENA_IMPORT_FIELD} is imported with a signature \
+             other than (i32, i32, i32, i32) -> i32 — not the canonical-ABI \
+             arena realloc contract; refusing to bind (compile with \
+             --no-bind-cabi-arena to keep it an external symbol)"
+        );
+    }
+    let Some(pages) = s.memory_pages else {
+        bail!(
+            "#418: cannot bind env::{ARENA_IMPORT_FIELD}: the module declares \
+             no linear memory to allocate from"
+        );
+    };
+    if s.memory64 {
+        bail!("#418: cannot bind env::{ARENA_IMPORT_FIELD}: memory64 module");
+    }
+    if s.non_const_data_offset {
+        bail!(
+            "#418: cannot bind env::{ARENA_IMPORT_FIELD}: a data segment has \
+             a non-constant offset, so the static-data extent (the arena \
+             floor) cannot be derived soundly"
+        );
+    }
+    if !s.has_function_section || !s.has_code_section {
+        bail!(
+            "#418: cannot bind env::{ARENA_IMPORT_FIELD}: the module defines \
+             no functions (nothing synth could route the binding through)"
+        );
+    }
+
+    let arena_end: u32 = u32::try_from(pages.saturating_mul(64 * 1024))
+        .unwrap_or(u32::MAX)
+        .min(0xFFFF_0000);
+    // Arena floor: above every byte the module statically claims — active
+    // data segments plus the i32-const global-init class (__stack_pointer
+    // top, wasm-ld's __heap_base/__data_end), mirroring the shipped
+    // used-extent rule. Floor 16, rounded up to 16.
+    let global_top = s
+        .global_inits
+        .iter()
+        .copied()
+        .filter(|&v| v <= arena_end)
+        .max()
+        .unwrap_or(0);
+    let arena_base = s.data_end.max(global_top).max(16).next_multiple_of(16);
+    if arena_base >= arena_end {
+        bail!(
+            "#418: cannot bind env::{ARENA_IMPORT_FIELD}: the static layout \
+             (data + stack + wasm-ld layout globals) extends to {arena_base} \
+             bytes but linear memory is only {arena_end} bytes — no arena \
+             region left; every allocation would trap"
+        );
+    }
+
+    // The cursor global goes at the END of the global index space; with the
+    // sole import removed there are no imported globals, so its index is the
+    // defined-global count.
+    let cursor_global = s.defined_globals;
+    let mut body = Vec::new();
+    wasm_encoder::Encode::encode(&allocator_body(cursor_global, arena_end), &mut body);
+
+    // ── Rewrite pass: byte-copy everything except the four touched sections.
+    let mut module = wasm_encoder::Module::new();
+    let mut global_emitted = false;
+    let mut function_emitted = false;
+    // Insert the (possibly missing) global section at its canonical position:
+    // just before the first section that must FOLLOW it.
+    let ensure_globals = |module: &mut wasm_encoder::Module, emitted: &mut bool| {
+        if !*emitted {
+            let mut out = Vec::new();
+            write_uleb(1, &mut out);
+            out.extend_from_slice(&cursor_global_entry(arena_base));
+            module.section(&wasm_encoder::RawSection {
+                id: wasm_encoder::SectionId::Global as u8,
+                data: &out,
+            });
+            *emitted = true;
+        }
+    };
+
+    for payload in Parser::new(0).parse_all(wasm) {
+        let payload = payload.context("parse wasm (#418 arena-bind rewrite)")?;
+        match &payload {
+            Payload::Version { .. } | Payload::End(_) => {}
+            Payload::ImportSection(_) => {
+                // The sole import is the arena import — drop the section.
+            }
+            Payload::FunctionSection(reader) => {
+                let mut entry = Vec::new();
+                write_uleb(arena_type_idx, &mut entry);
+                let contents = &wasm[reader.range()];
+                module.section(&wasm_encoder::RawSection {
+                    id: wasm_encoder::SectionId::Function as u8,
+                    data: &prepend_entry(contents, &entry)?,
+                });
+                function_emitted = true;
+            }
+            Payload::GlobalSection(reader) => {
+                let contents = &wasm[reader.range()];
+                module.section(&wasm_encoder::RawSection {
+                    id: wasm_encoder::SectionId::Global as u8,
+                    data: &append_entry(contents, &cursor_global_entry(arena_base))?,
+                });
+                global_emitted = true;
+            }
+            Payload::ExportSection(_)
+            | Payload::StartSection { .. }
+            | Payload::ElementSection(_)
+            | Payload::DataCountSection { .. }
+            | Payload::DataSection(_) => {
+                ensure_globals(&mut module, &mut global_emitted);
+                copy_raw(&mut module, &payload, wasm)?;
+            }
+            Payload::CodeSectionStart { range, .. } => {
+                ensure_globals(&mut module, &mut global_emitted);
+                // `range` spans the full section contents (count + bodies);
+                // `size` would EXCLUDE the count leb — do not use it here.
+                let contents = &wasm[range.clone()];
+                module.section(&wasm_encoder::RawSection {
+                    id: wasm_encoder::SectionId::Code as u8,
+                    data: &prepend_entry(contents, &body)?,
+                });
+            }
+            Payload::CodeSectionEntry(_) => {} // consumed via CodeSectionStart
+            other => copy_raw(&mut module, other, wasm)?,
+        }
+    }
+    if !function_emitted {
+        bail!("#418 internal: function section not re-emitted"); // unreachable: scanned above
+    }
+
+    let bytes = module.finish();
+    // Internal gate: the rewrite must be a VALID module — a malformed rewrite
+    // here would otherwise surface as a confusing decode error downstream.
+    wasmparser::Validator::new()
+        .validate_all(&bytes)
+        .context("#418 internal: arena-bind rewrite produced an invalid module (bug)")?;
+    Ok(ArenaBind::Bound(BoundArena {
+        bytes,
+        arena_base,
+        arena_end,
+    }))
+}
+
+/// Byte-copy one section verbatim.
+fn copy_raw(module: &mut wasm_encoder::Module, payload: &Payload<'_>, wasm: &[u8]) -> Result<()> {
+    let Some((id, range)) = payload.as_section() else {
+        bail!("#418 internal: unhandled non-section payload {payload:?}");
+    };
+    module.section(&wasm_encoder::RawSection {
+        id,
+        data: &wasm[range],
+    });
+    Ok(())
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    fn fixture() -> Vec<u8> {
+        wat::parse_str(
+            r#"(module
+                 (import "env" "__cabi_arena_realloc"
+                   (func $arena (param i32 i32 i32 i32) (result i32)))
+                 (memory (export "memory") 1)
+                 (global $sp (mut i32) (i32.const 4096))
+                 (global (export "__heap_base") i32 (i32.const 6144))
+                 (data (i32.const 5120) "0123456789abcdef")
+                 (func (export "cabi_realloc") (param i32 i32 i32 i32) (result i32)
+                   local.get 0 local.get 1 local.get 2 local.get 3 call $arena))"#,
+        )
+        .unwrap()
+    }
+
+    #[test]
+    fn binds_sole_arena_import() {
+        let ArenaBind::Bound(b) = bind_cabi_arena_realloc(&fixture()).unwrap() else {
+            panic!("expected Bound");
+        };
+        // base above data end (5136) and __heap_base (6144), 16-aligned
+        assert_eq!(b.arena_base, 6144);
+        assert_eq!(b.arena_end, 65536);
+        // no imports remain; index space preserved (cabi_realloc still calls
+        // function 0, which is now the DEFINED allocator).
+        let mut num_imports = 0;
+        let mut num_funcs = 0;
+        let mut num_globals = 0;
+        for p in Parser::new(0).parse_all(&b.bytes) {
+            match p.unwrap() {
+                Payload::ImportSection(r) => num_imports += r.count(),
+                Payload::FunctionSection(r) => num_funcs = r.count(),
+                Payload::GlobalSection(r) => num_globals = r.count(),
+                _ => {}
+            }
+        }
+        assert_eq!(num_imports, 0);
+        assert_eq!(num_funcs, 2); // allocator + cabi_realloc
+        assert_eq!(num_globals, 3); // sp, __heap_base, cursor
+    }
+
+    #[test]
+    fn bound_module_executes_contract() {
+        // The rewritten module must satisfy the #418 contract under a real
+        // wasm interpreter — validated structurally here (full execution
+        // differential: scripts/repro/cabi_arena_bind_418_differential.py).
+        let ArenaBind::Bound(b) = bind_cabi_arena_realloc(&fixture()).unwrap() else {
+            panic!("expected Bound");
+        };
+        wasmparser::Validator::new().validate_all(&b.bytes).unwrap();
+    }
+
+    #[test]
+    fn no_arena_import_passes_through() {
+        let wasm =
+            wat::parse_str(r#"(module (memory 1) (func (export "f") (result i32) i32.const 7))"#)
+                .unwrap();
+        assert!(matches!(
+            bind_cabi_arena_realloc(&wasm).unwrap(),
+            ArenaBind::NoArenaImport
+        ));
+    }
+
+    #[test]
+    fn other_imports_keep_host_seam() {
+        let wasm = wat::parse_str(
+            r#"(module
+                 (import "env" "k_spin_lock" (func (param i32)))
+                 (import "env" "__cabi_arena_realloc"
+                   (func $arena (param i32 i32 i32 i32) (result i32)))
+                 (memory 1)
+                 (func (export "f") (param i32 i32 i32 i32) (result i32)
+                   local.get 0 local.get 1 local.get 2 local.get 3 call $arena))"#,
+        )
+        .unwrap();
+        assert!(matches!(
+            bind_cabi_arena_realloc(&wasm).unwrap(),
+            ArenaBind::KeptHostSeam(_)
+        ));
+    }
+
+    #[test]
+    fn wrong_signature_declines_loudly() {
+        let wasm = wat::parse_str(
+            r#"(module
+                 (import "env" "__cabi_arena_realloc"
+                   (func $arena (param i32 i32) (result i32)))
+                 (memory 1)
+                 (func (export "f") (param i32 i32) (result i32)
+                   local.get 0 local.get 1 call $arena))"#,
+        )
+        .unwrap();
+        let err = bind_cabi_arena_realloc(&wasm).unwrap_err().to_string();
+        assert!(err.contains("#418"), "{err}");
+        assert!(err.contains("signature"), "{err}");
+    }
+
+    #[test]
+    fn no_memory_declines_loudly() {
+        let wasm = wat::parse_str(
+            r#"(module
+                 (import "env" "__cabi_arena_realloc"
+                   (func $arena (param i32 i32 i32 i32) (result i32)))
+                 (func (export "f") (result i32)
+                   i32.const 0 i32.const 0 i32.const 8 i32.const 4 call $arena))"#,
+        )
+        .unwrap();
+        let err = bind_cabi_arena_realloc(&wasm).unwrap_err().to_string();
+        assert!(err.contains("no linear memory"), "{err}");
+    }
+
+    #[test]
+    fn full_static_layout_declines_loudly() {
+        // __heap_base == memory size: no arena region left.
+        let wasm = wat::parse_str(
+            r#"(module
+                 (import "env" "__cabi_arena_realloc"
+                   (func $arena (param i32 i32 i32 i32) (result i32)))
+                 (memory 1)
+                 (global (export "__heap_base") i32 (i32.const 65536))
+                 (func (export "f") (result i32)
+                   i32.const 0 i32.const 0 i32.const 8 i32.const 4 call $arena))"#,
+        )
+        .unwrap();
+        let err = bind_cabi_arena_realloc(&wasm).unwrap_err().to_string();
+        assert!(err.contains("no arena region left"), "{err}");
+    }
+
+    #[test]
+    fn module_without_globals_gets_global_section() {
+        let wasm = wat::parse_str(
+            r#"(module
+                 (import "env" "__cabi_arena_realloc"
+                   (func $arena (param i32 i32 i32 i32) (result i32)))
+                 (memory 1)
+                 (data (i32.const 64) "xyzw")
+                 (func (export "f") (result i32)
+                   i32.const 0 i32.const 0 i32.const 8 i32.const 4 call $arena))"#,
+        )
+        .unwrap();
+        let ArenaBind::Bound(b) = bind_cabi_arena_realloc(&wasm).unwrap() else {
+            panic!("expected Bound");
+        };
+        assert_eq!(b.arena_base, 80); // data end 68 -> 16-aligned
+        let mut num_globals = 0;
+        for p in Parser::new(0).parse_all(&b.bytes) {
+            if let Payload::GlobalSection(r) = p.unwrap() {
+                num_globals = r.count();
+            }
+        }
+        assert_eq!(num_globals, 1);
+    }
+}
diff --git a/crates/synth-core/src/lib.rs b/crates/synth-core/src/lib.rs
index 1571f4e4..68621bf9 100644
--- a/crates/synth-core/src/lib.rs
+++ b/crates/synth-core/src/lib.rs
@@ -4,6 +4,7 @@
 //! including representations for WebAssembly components, modules, and the intermediate
 //! representation (IR) used for synthesis.
 
+pub mod arena_bind;
 pub mod backend;
 pub mod component;
 pub mod dwarf_line;
diff --git a/scripts/repro/cabi_arena_bind.wat b/scripts/repro/cabi_arena_bind.wat
new file mode 100644
index 00000000..78f44fda
--- /dev/null
+++ b/scripts/repro/cabi_arena_bind.wat
@@ -0,0 +1,75 @@
+;; #418 — the wit-bindgen `cabi-realloc-extern` / meld-dissolve shape:
+;; `cabi_realloc` stays exported but routes to the embedder-provided
+;; `env::__cabi_arena_realloc` arena import (grow-free — no memory.grow).
+;;
+;; Layout mirrors a Rust/wasm-ld component: mutable __stack_pointer global,
+;; exported __data_end/__heap_base layout globals, an active data segment.
+;; synth's self-contained binding must place its arena ABOVE all of these.
+;;
+;; The test exports return POINTER-INDEPENDENT observables (preserved
+;; contents, disjointness, alignment residue, the (0,0,align,0) -> align
+;; contract case), so the differential passes only on contract-conformant
+;; allocator SEMANTICS — never on both sides happening to pick the same base.
+(module
+  (import "env" "__cabi_arena_realloc"
+    (func $arena (param i32 i32 i32 i32) (result i32)))
+  (memory (export "memory") 1)
+  (global $__stack_pointer (mut i32) (i32.const 4096))
+  (global $__data_end i32 (i32.const 5136))
+  (global $__heap_base i32 (i32.const 6144))
+  (export "__data_end" (global 1))
+  (export "__heap_base" (global 2))
+  (data (i32.const 5120) "\01\02\03\04\05\06\07\08\09\0a\0b\0c\0d\0e\0f\10")
+
+  ;; canonical realloc, routed to the arena (the cabi-realloc-extern body)
+  (func (export "cabi_realloc") (param i32 i32 i32 i32) (result i32)
+    local.get 0
+    local.get 1
+    local.get 2
+    local.get 3
+    call $arena)
+
+  ;; contract: old_len == 0 && new_len == 0 -> returns align verbatim
+  (func (export "case_zero") (param i32) (result i32)
+    i32.const 0
+    i32.const 0
+    local.get 0
+    i32.const 0
+    call $arena)
+
+  ;; RawVec-grow: alloc 4, store, realloc to 8 — old contents PRESERVED
+  (func (export "grow_preserves") (result i32)
+    (local i32 i32)
+    (local.set 0
+      (call $arena (i32.const 0) (i32.const 0) (i32.const 4) (i32.const 4)))
+    (i32.store (local.get 0) (i32.const 0x11223344))
+    (local.set 1
+      (call $arena (local.get 0) (i32.const 4) (i32.const 4) (i32.const 8)))
+    (i32.store offset=4 (local.get 1) (i32.const 0x55667788))
+    (i32.add
+      (i32.load (local.get 1))
+      (i32.load offset=4 (local.get 1))))
+
+  ;; two live allocations must not alias
+  (func (export "disjoint") (result i32)
+    (local i32 i32)
+    (local.set 0
+      (call $arena (i32.const 0) (i32.const 0) (i32.const 4) (i32.const 4)))
+    (i32.store (local.get 0) (i32.const 7))
+    (local.set 1
+      (call $arena (i32.const 0) (i32.const 0) (i32.const 4) (i32.const 4)))
+    (i32.store (local.get 1) (i32.const 9))
+    (i32.add
+      (i32.mul (i32.load (local.get 0)) (i32.const 100))
+      (i32.load (local.get 1))))
+
+  ;; returned pointer honors the requested alignment (residue must be 0)
+  (func (export "align_ok") (param i32) (result i32)
+    (i32.and
+      (call $arena (i32.const 0) (i32.const 0) (local.get 0) (i32.const 3))
+      (i32.sub (local.get 0) (i32.const 1))))
+
+  ;; bounded arena: exhaustion TRAPS (never memory.grow)
+  (func (export "exhaust") (result i32)
+    (call $arena (i32.const 0) (i32.const 0) (i32.const 4) (i32.const 0x40000000)))
+)
diff --git a/scripts/repro/cabi_arena_bind_418_differential.py b/scripts/repro/cabi_arena_bind_418_differential.py
new file mode 100644
index 00000000..18368dc7
--- /dev/null
+++ b/scripts/repro/cabi_arena_bind_418_differential.py
@@ -0,0 +1,235 @@
+#!/usr/bin/env python3
+"""#418 — self-contained binding of `env::__cabi_arena_realloc` (the meld
+dissolve gap): EXECUTION differential vs wasmtime.
+
+The wit-bindgen `cabi-realloc-extern` shape imports the canonical-ABI arena
+allocator from the embedder. The `--relocatable` seam is locked (#420: an
+UNDEFINED `__cabi_arena_realloc` symbol the TCB link satisfies) — but a
+SELF-CONTAINED dissolve (default compile, no host linker) previously degraded
+to an ET_REL "link me with the Kiln bridge" object: the arena import was the
+one unresolved seam blocking a fully self-contained image.
+
+This gate asserts the bound behavior end to end:
+  1. the default self-contained compile of the fixture produces ET_EXEC (an
+     executable image, not a link-me object) — RED before the #418 binding;
+  2. every export EXECUTES under unicorn (image's own startup runs first:
+     R9/R10/R11 init, globals table, #758 data copy) and matches wasmtime
+     ground truth, where the import is satisfied by a HOST arena allocator
+     implementing the #418 contract (old_len==0 && new_len==0 -> align;
+     bump allocation; realloc preserves min(old,new) bytes; bounded, traps
+     on exhaustion — never memory.grow);
+  3. the host arena deliberately uses a DIFFERENT base than synth's, so only
+     pointer-INDEPENDENT semantics can pass (no base-coincidence green);
+  4. the exhaustion case must TRAP on BOTH sides.
+
+Run (needs wasmtime + unicorn + pyelftools):
+  SYNTH=./target/debug/synth python scripts/repro/cabi_arena_bind_418_differential.py
+Exits nonzero on any mismatch.
+"""
+
+import os
+import subprocess
+import sys
+from pathlib import Path
+
+import wasmtime
+from elftools.elf.elffile import ELFFile
+from unicorn import UC_ARCH_ARM, UC_MODE_THUMB, Uc, UcError
+from unicorn.arm_const import (
+    UC_ARM_REG_LR,
+    UC_ARM_REG_PC,
+    UC_ARM_REG_R0,
+    UC_ARM_REG_R1,
+    UC_ARM_REG_R2,
+    UC_ARM_REG_R3,
+    UC_ARM_REG_R11,
+    UC_ARM_REG_SP,
+)
+
+WAT = Path(__file__).with_name("cabi_arena_bind.wat")
+SYNTH = os.environ.get("SYNTH", "./target/release/synth")
+
+# (export, args, traps) — every observable is pointer-independent.
+CASES = [
+    ("case_zero", (8,), False),
+    ("case_zero", (1,), False),
+    ("grow_preserves", (), False),
+    ("disjoint", (), False),
+    ("align_ok", (16,), False),
+    ("exhaust", (), True),
+]
+
+SENTINELS = (0xDEADBEEF, 0xCAFEF00D, 0x5A5A5A5A, 0xA0A0A0A0)
+
+FLASH_BASE = 0x0000_0000
+FLASH_SIZE = 0x40000
+RET_STUB = 0x3F000  # inside the flash map, far above the image
+RAM_BASE = 0x2000_0000
+RAM_SIZE = 0x20_0000
+
+# Host arena base — deliberately NOT synth's derived base (6144), so equal
+# results can only come from contract-conformant semantics, never from both
+# sides picking the same addresses.
+HOST_ARENA_BASE = 0x8000
+
+
+def compile_self_contained(out):
+    r = subprocess.run(
+        [SYNTH, "compile", str(WAT), "-o", out, "-b", "arm",
+         "--target", "cortex-m3", "--all-exports"],
+        capture_output=True, text=True,
+    )
+    if r.returncode != 0:
+        sys.exit(f"compile failed: {r.stderr}")
+    return r.stderr
+
+
+def load_image(elf_path):
+    f = ELFFile(open(elf_path, "rb"))
+    if f.header.e_type != "ET_EXEC":
+        sys.exit(
+            f"RED (#418): expected a self-contained ET_EXEC image, got "
+            f"{f.header.e_type} — the arena import still degrades the "
+            f"dissolve to a link-me object"
+        )
+    blobs = []  # (addr, bytes)
+    syms = {}
+    for s in f.iter_sections():
+        if s.header.sh_type == "SHT_SYMTAB":
+            for sym in s.iter_symbols():
+                if sym.name:
+                    syms[sym.name] = sym["st_value"]
+        if s.header.sh_flags & 0x2 and s.header.sh_type == "SHT_PROGBITS":
+            blobs.append((s["sh_addr"], s.data()))
+    if not blobs:
+        sys.exit("no allocatable PROGBITS sections found")
+    return blobs, syms
+
+
+# ---------------------------------------------------------------- wasmtime
+def host_arena_instance():
+    """Instantiate the ORIGINAL module with a host arena implementing the
+    #418 contract over the instance's own linear memory."""
+    eng = wasmtime.Engine()
+    mod = wasmtime.Module(eng, WAT.read_bytes())
+    store = wasmtime.Store(eng)
+    state = {"cur": HOST_ARENA_BASE}
+
+    def realloc(caller, old_ptr, old_len, align, new_len):
+        mem = caller.get("memory")
+        # contract: old_len == 0 && new_len == 0 -> return align
+        if old_len == 0 and new_len == 0:
+            return align
+        if align <= 0 or (align & (align - 1)):
+            raise wasmtime.Trap("bad align")
+        size = mem.data_len(caller)
+        aligned = (state["cur"] + align - 1) & ~(align - 1)
+        end = aligned + new_len
+        if end > size:
+            # bounded arena: trap on exhaustion, never memory.grow
+            raise wasmtime.Trap("arena exhausted")
+        state["cur"] = end
+        n = min(old_len, new_len)
+        if n:
+            mem.write(caller, bytes(mem.read(caller, old_ptr, old_ptr + n)),
+                      aligned)
+        return aligned
+
+    ty = wasmtime.FuncType([wasmtime.ValType.i32()] * 4,
+                           [wasmtime.ValType.i32()])
+    func = wasmtime.Func(store, ty, realloc, access_caller=True)
+    inst = wasmtime.Instance(store, mod, [func])
+    return store, inst
+
+
+def wasm_result(func, args):
+    store, inst = host_arena_instance()  # fresh arena per case
+    f = inst.exports(store)[func]
+    try:
+        return f(store, *args) & 0xFFFFFFFF, False
+    except (wasmtime.WasmtimeError, wasmtime.Trap):
+        return None, True
+
+
+# ----------------------------------------------------------------- unicorn
+def fresh_machine(blobs, syms):
+    """Map the image and run its OWN startup (reset vector -> stop at the
+    first laid-out function): R10/R11/R9 init, R9 globals-table
+    materialization (the arena cursor global!), #758 data ROM->RAM copy."""
+    mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB)
+    mu.mem_map(FLASH_BASE, FLASH_SIZE)
+    mu.mem_map(RAM_BASE, RAM_SIZE)
+    for addr, data in blobs:
+        mu.mem_write(addr, bytes(data))
+    mu.mem_write(RET_STUB, b"\x00\xbf\x00\xbf")  # nop; nop
+    image = blobs[0][1]
+    sp_init = int.from_bytes(image[0:4], "little")
+    reset = int.from_bytes(image[4:8], "little")
+    # First COMPILED function (the startup's final jump target) — exclude the
+    # image-infrastructure symbols, or `min` lands on Reset_Handler and the
+    # startup never executes (a vacuous machine: R9/R10/R11 all zero).
+    infra = {"Reset_Handler", "Default_Handler", "Trap_Handler",
+             "__linear_memory_base"}
+    first_func = min(v for k, v in syms.items() if k not in infra) & ~1
+    mu.reg_write(UC_ARM_REG_SP, sp_init)
+    mu.emu_start(reset, first_func, timeout=5_000_000)
+    if mu.reg_read(UC_ARM_REG_PC) & ~1 != first_func:
+        sys.exit(
+            f"startup did not reach the first function "
+            f"(pc={mu.reg_read(UC_ARM_REG_PC):#x}, want {first_func:#x})"
+        )
+    # Anti-vacuity: the startup must have established the linmem base in R11.
+    r11 = mu.reg_read(UC_ARM_REG_R11)
+    if r11 != syms["__linear_memory_base"]:
+        sys.exit(f"startup left R11={r11:#x}, want __linear_memory_base")
+    return mu, sp_init
+
+
+def arm_result(blobs, syms, func, args):
+    mu, sp_init = fresh_machine(blobs, syms)  # fresh arena per case
+    regs = (UC_ARM_REG_R0, UC_ARM_REG_R1, UC_ARM_REG_R2, UC_ARM_REG_R3)
+    for reg, sent in zip(regs, SENTINELS):
+        mu.reg_write(reg, sent)  # anti-vacuity: caller residue
+    for reg, val in zip(regs, args):
+        mu.reg_write(reg, val)
+    mu.reg_write(UC_ARM_REG_SP, sp_init)
+    mu.reg_write(UC_ARM_REG_LR, RET_STUB | 1)
+    try:
+        mu.emu_start((syms[func] & ~1) | 1, RET_STUB, timeout=5_000_000)
+    except UcError:
+        return None, True  # UDF -> invalid-instruction exception = trap
+    if mu.reg_read(UC_ARM_REG_PC) & ~1 != RET_STUB:
+        return None, True  # stopped elsewhere (fault-shaped)
+    return mu.reg_read(UC_ARM_REG_R0) & 0xFFFFFFFF, False
+
+
+def main():
+    if not os.path.exists(SYNTH):
+        sys.exit(f"{SYNTH} not found — build synth first")
+    elf = "/tmp/cabi_arena_bind_418.elf"
+    compile_self_contained(elf)
+    blobs, syms = load_image(elf)
+
+    fails = 0
+    for func, args, want_trap in CASES:
+        gt, gt_trap = wasm_result(func, args)
+        got, got_trap = arm_result(blobs, syms, func, args)
+        if want_trap:
+            ok = gt_trap and got_trap
+            show = f"trap(wasmtime)={gt_trap} trap(arm)={got_trap}"
+        else:
+            ok = (not gt_trap) and (not got_trap) and got == gt
+            show = (
+                f"= {got if got is None else hex(got)}  "
+                f"(wasmtime: {gt if gt is None else hex(gt)})"
+            )
+        if not ok:
+            fails += 1
+        print(f"{'OK  ' if ok else 'FAIL'} {func}{args} {show}")
+
+    print("ORACLE:", "PASS" if fails == 0 else f"FAIL ({fails})")
+    sys.exit(1 if fails else 0)
+
+
+if __name__ == "__main__":
+    main()