Multi-memory structural isolation: lower N wasm memories to N distinct native bases (memidx-through-IR, cross-memory ops, expose base/size for MPU/PMP)

[avrabe]

Committed lowering path for the dissolved-library-OS isolation model. Cross-repo decision: meld#300 commits to model 2 (multi-memory structural isolation) — meld preserves each component's memory as a distinct region (MemoryStrategy::MultiMemory, tested in meld-core/tests/multi_memory.rs) so the MPU/PMP boundary is the semantic boundary. synth is the remaining gate.

Today (the gap)

synth is single-memory: the memory index is dropped at the IR level (wasm_op.rs load/store variants carry no memory_index), cross-memory memory.copy/memory.fill are loud-skipped (#369-adjacent, wasm_decoder.rs non-zero dst_mem/src_mem → None), and the linear-memory base is a single hardcoded register (R11 = 0x20000000 / 0x20000100). MPU is config-only — mpu_allocator computes region base/size/permissions + init code but nothing is wired into the optimized codegen path (#377).

The work (staged, gated — byte-changing on the load/store path)

1. Carry memidx through the IR — add memory_index to the load/store/memory.* WasmOp variants; stop dropping it in wasm_decoder.rs.
2. Per-memory native bases — place memory[k] at a distinct base; common case pins the function's home memory base in R11 (≈ today's cost), cross-memory access resolves via a per-memory base/size table (synth_memory::MemoryTable, MAX_MEMORIES=8 already exists).
3. Cross-memory ops — emit memory.copy/memory.fill with distinct dst_mem/src_mem explicitly instead of loud-skipping.
4. Expose per-memory base/size — so an embedder programs one MPU/PMP region per memory (the mpu_allocator region machinery already computes base/size/perms; wire it from the per-memory layout — ties to --safety-bounds software/mpu are no-ops on the optimized codegen path (flight-safety: jess pins software for PX4) #377).

Constraints / gating

• Byte-changing codegen ⇒ staged behind frozen-fixture re-freeze (control_step 0x00210A55 / flight_algo 0x07FDF307 / divseam) + the differential oracle + gale on-silicon (the arm regalloc: select_with_stack allocates param registers (r0-r3) for temps/results before live param reads — i64_lowering fuzz class #193/v0.11.16: inlined-callee body after an opaque call reads stale values for divided fields (loom-inlined flight seam) — flat version correct #212/v0.11.17 regression: guard-elision miscompiles fully-dissolved flight_algo (controller tail wrong; control_step OK; was correct in v0.11.16) #215 latent-regalloc lesson). Each step lands gated, never crammed into an idle tick.
• MPU/PMP region cap (~8 on ARMv7-M, PMP similar) bounds practical N — fine for a handful of mutually-distrusting components.
• meld keeps MultiMemory output stable as the lowering target; file against meld if synth hits a structure it can't consume.

Tracked under the VCR-* north-star program (epic #242). Refs: gale#86, gale#404, meld#300, synth#377 (MPU runtime wiring), synth#369 (decoder loud-skip).

[avrabe]

[issue-hunt automation — cross-repo trace sync, not a maintainer decision]

Upstream meld v0.34.0 (2026-06-23) shipped the multi-memory isolation commitment and formalized it as ADR-4 (safety/adr/ADR-4-inter-component-isolation-model.md): model 2 (structural isolation) is the committed dissolved-MCU path, and meld guarantees MemoryStrategy::MultiMemory output stable as synth's lowering target (adjusting only if synth hits a shape it cannot consume). ADR-4 explicitly names this issue's lowering work (synth#404/#369) as the committed remaining gate, anchored on meld's gating tests (test_multi_memory_result_copy_adapter, SR-21/SR-23).

So the cross-repo decision (meld#300, 2026-06-21) is now released + documented upstream — synth is the sole remaining gate. No synth build impact (no cargo dependency on meld).

Status here is unchanged: the synth-side work — (1) carry memidx through the IR, (2) per-memory native bases, (3) explicit cross-memory ops (#369), (4) expose per-memory base/size for one MPU/PMP region each — is byte-changing on the load/store path and stays the staged, gated VCR-MEM-002 track (artifacts/verified-codegen-roadmap.yaml), not an idle-tick increment. The frozen single-memory fixtures (control_step 0x00210A55, flat+inlined flight_algo 0x07FDF307) must stay byte-identical under it — now CI-gated by the frozen-codegen byte gate (#445/#446). VCR-MEM-002 provenance updated to cite ADR-4 + v0.34.0.