feat(#418): bind cabi-arena-realloc natively on the self-contained dissolve — synthesized in-module arena allocator

.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

.gitignore

@@ -72,3 +72,4 @@ result-*
 # Stray ELF/object output at repo root (e.g. `synth compile ... -o output.elf`)
 /*.elf
 output.elf
+__pycache__/

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);
 

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"
+    );
+}

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`