Skip to content

feat(#406): multi-memory phase 1 — N wasm memories to N distinct native base regions (VCR-MEM-002) - #749

Merged
avrabe merged 6 commits into
mainfrom
feat/43-multi-memory-ph1
Jul 15, 2026
Merged

feat(#406): multi-memory phase 1 — N wasm memories to N distinct native base regions (VCR-MEM-002)#749
avrabe merged 6 commits into
mainfrom
feat/43-multi-memory-ph1

Conversation

@avrabe

@avrabe avrabe commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

VCR-MEM-002 phase 1 (#406, epic #242): N wasm memories → N distinct native base regions

The meld#300 multi-memory structural-isolation model needs synth to stop dropping the memarg memory index. Pre-#406, every load/store lowered onto the ONE R11 base — a store to memory 1 silently clobbered memory 0, memory k's init data was silently dropped, and memory.size/grow on memory k read memory 0's state.

What ships

  • Honest memidx threading: the decoder wraps any load/store whose memarg targets memory k > 0 in WasmOp::MultiMemory { memory, op } (memory-0 ops stay the bare variants — every existing match arm and frozen byte untouched by construction), with a mirror-pinned memarg_memory_index helper covering exactly convert_operator's memarg arms.
  • Per-memory base regions (--relocatable): memory 0 keeps the runtime R11 base (and __synth_wasm_data under the native-pointer ABI — frozen-safe); memory k > 0 is addressed via its own __synth_wasm_data_<k> symbol (R_ARM_ABS32 literal pool, the dissolved --relocatable objects carry full wasm linmem (64KB .data) + absolute MOVW relocs — MCU-unshippable + link-fragile (gale mutex silicon fault) #345 link-survivable form) defined at the base of a per-memory .synth.wasm_mem_<k> reservation section — PROGBITS with init segments placed (previously silently dropped), NOBITS when pure zero-init.
  • Per-memory memory.size/grow: memory 0 unchanged (R10); memory k's size is the declared constant (grow is always -1 on this backend, so initial == size), grow(k) validates the context then emits the fixed-memory -1.
  • Phase-1 scope: the i32 access family (i32.load/store + 8/16 sign/zero variants) on memory k. Wider/float accesses, --safety-bounds on memory k, and cross-/non-default memory.copy/fill decline loudly, typed and precise — never a silent alias.

Capability matrix (all pinned by crates/synth-cli/tests/multi_memory_406.rs, 13/13)

shape verdict
2 memories, ARM --relocatable GREEN (execution differential, 29/29)
3 memories, ARM --relocatable GREEN (generic over K; NOBITS + PROGBITS)
multi-memory, no --relocatable / self-contained --cortex-m refuse (one R11 base)
multi-memory × --native-pointer-abi refuse (static-region classification is memory-0-only)
multi-memory × --shadow-stack-size refuse (shrinks memory 0's geometry)
multi-memory on riscv / aarch64 refuse (no per-memory base lowering)
cross-memory memory.copy / non-default memory.fill loud-skip naming the op
i64/f32/f64 access on memory k > 0 loud-skip naming the phase-1 scope
non-const data-segment offset on memory k / segment overflowing memory k refuse at decode / emit

Defense in depth: select_default and the optimized path (optimizer_bridge) decline MultiMemory + non-zero memory.size/grow explicitly, so no path can fall back into aliasing.

Evidence

Refs #406, #242 (VCR-MEM-002 phase 1). Phase 2+ (self-contained MPU/PMP regions, cross-memory bulk ops, wide accesses) stays on the roadmap artifact.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe and others added 6 commits July 15, 2026 12:53
… here)

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… phase 1

- compile_all_exports threads extra_memory_data_segments + multi_memory_decline
  from the decoder; module-level LOUD gates (decode decline reason, non-ARM
  backend, self-contained/!--relocatable, --native-pointer-abi,
  --shadow-stack-size) fire before any op is selected.
- CompileConfig.memory_pages populated from the declared memories (indexed by
  memory index; memory-0 lowering never reads it).
- build_relocatable_elf: one reservation section per non-default memory
  (.synth.wasm_mem_<k>, PROGBITS with placed init segments / NOBITS when pure
  zero-init) + a __synth_wasm_data_<k> base symbol, with segment-bounds and
  orphan-segment refusals. Single-memory modules pass empty lists — output
  byte-identical (frozen gate 10/10 green).

VCR-MEM-002 phase 1, #406/#242.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…nct unicorn bases vs wasmtime

29 cases green on the branch (store-both aliasing discriminators, memory-1
init-data peeks, sub-word round-trips, per-memory size/grow); RED on
origin/main (exit 1: the object lacks .synth.wasm_mem_1 — the pre-#406
silent-aliasing object has no per-memory region/symbol). Structural pins:
__synth_wasm_data_1 DEFINED, .synth.wasm_mem_1 PROGBITS == 3 pages with the
init segment placed, every ABS32 reloc in-range, and at least one memory-1
reloc (an object with none is the aliasing bug).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
GREEN: 2- and 3-memory ARM --relocatable objects (per-memory NOBITS/PROGBITS
regions, defined __synth_wasm_data_<k>, init bytes placed, no _0 alias).
REFUSED loudly: no --relocatable, self-contained --cortex-m,
--native-pointer-abi, --shadow-stack-size, riscv, aarch64, cross-memory
memory.copy, non-default memory.fill, i64 access on memory k, non-const
segment offset, overflowing segment.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe
avrabe force-pushed the feat/43-multi-memory-ph1 branch from 85bad1c to dad0261 Compare July 15, 2026 10:54
@avrabe
avrabe merged commit 52676f4 into main Jul 15, 2026
37 checks passed
@avrabe
avrabe deleted the feat/43-multi-memory-ph1 branch July 15, 2026 11:03
@codecov

codecov Bot commented Jul 15, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 83.25688% with 73 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-synthesis/src/instruction_selector.rs 74.42% 56 Missing ⚠️
crates/synth-synthesis/src/optimizer_bridge.rs 47.05% 9 Missing ⚠️
crates/synth-cli/src/main.rs 96.49% 4 Missing ⚠️
crates/synth-core/src/wasm_decoder.rs 95.06% 4 Missing ⚠️

📢 Thoughts on this report? Let us know!

avrabe added a commit that referenced this pull request Jul 30, 2026
…CLOSED

Cold review found the v0.53 assembly was about to ship the SAME defect class as
v0.51 and v0.52, with a new twist: the ledger was defending it.

F1 (BLOCK) — the FEATURE_MATRIX "Honest Summary" cited #881, #882 and #872 as
open residuals. All three were CLOSED by lanes in THIS release. Root cause is a
lane-ordering race: L6's doc-honesty commit landed 2026-07-29 15:28 and said
"honest-summary residual examples now cite the actually-open issues
(#881/#882/#872)" -- true when written; L1 closed #881 fourteen hours later. The
doc-honesty lane ran FIRST and nobody re-swept after the fixes landed. The
document had become self-contradictory: the summary said RV32 br_table still
declines while the backend row three sections up said it lowers. Re-pointed at
genuinely-open issues (#890, #851, #846), verified against `gh issue view`.

F2 (BLOCK) — claims.yaml PINNED the stale "#881" verbatim, so `claim_check`
reported 34/34 while green-confirming a false residual, and correcting the prose
would have turned the gate RED. CLAUDE.md says never fix a red gate by loosening
the ledger; this was the inverse -- a ledger entry that had gone false, so the
gate protected the defect instead of catching it.

The fix is structural, not a re-point: an ISSUE-NUMBER pin goes stale the moment
the issue is fixed, because `verbatim` only asserts the phrase is PRESENT. This
pin has now been wrong twice for exactly that reason (#782, then #881). It now
pins the CAPABILITY GAP -- "single-precision FPUs", the i64-from-f32 decline
that genuinely remains -- which becomes false precisely when the gap closes.
Red-first verified: replacing the phrase reddens SYNTH-F32-F64-VFP (exit 1),
restoring it returns green.

F3 -- three of seven lanes had NO changelog entry, including L4/#872: a
default-on soundness fix that MOVED SHIPPED BYTES (gust_poll 692->696, fact-spec
132->140). A user diffing v0.52->v0.53 output would have found no explanation.
Added L1 (#885), L4 (#888) and L7 (#889) entries, and collapsed a duplicate
`### Added` section that violated the Keep-a-Changelog structure the release
process mandates.

F4 -- README declared "No multi-memory" while the matrix (corrected this
release) says P with a CI-wired differential. Multi-memory phase 1 shipped in
v0.43 (#749); the README line was ~10 releases stale, so v0.53 would have
shipped two documents disagreeing about a capability.

F5 -- the #880 changelog entry claimed every pinned phrase is bound to its
oracle AND that oracle's CI wiring. SYNTH-MATRIX-WCET-COMPOSITION has neither --
the sound-WCET-bound row, one of the most safety-load-bearing claims in the
matrix, is the single exception. Named it rather than softening it away.

F6 -- #872's real remaining hole (a mid-segment `Pop {…,PC}` the segment-local
validator misses) and VCR-DEC-001's (a wrong-return-register rewrite accepted by
`validate_cfg_rewrite` AND VCR-RA-003 both, caught only by execution) existed
only in Rust doc-comments. Both now stated in the matrix and CHANGELOG: the
release was simultaneously OVERSTATING what is open and OMITTING what is.

claim_check 34/34, docs regenerated, render byte-fresh.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Jul 30, 2026
* chore(release): v0.53.0 — "The last mile" (7 lanes)

Version sweep: workspace + all 13 intra-workspace path-dep pins + MODULE.bazel
+ status.json, Cargo.lock refreshed to 0.53.0 (v0.52's cold review caught a
stale lock; no CI job builds --locked, so this one is on the release process).
Docs regenerated once at assembly per #805 -- lanes do not hand-edit generated
artifacts. claim_check 34/34, check_version_pins OK.

CHANGELOG headline added by the coordinator over the 8 lane-written entries.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* fix(release): cold-review blockers — stop citing issues this release CLOSED

Cold review found the v0.53 assembly was about to ship the SAME defect class as
v0.51 and v0.52, with a new twist: the ledger was defending it.

F1 (BLOCK) — the FEATURE_MATRIX "Honest Summary" cited #881, #882 and #872 as
open residuals. All three were CLOSED by lanes in THIS release. Root cause is a
lane-ordering race: L6's doc-honesty commit landed 2026-07-29 15:28 and said
"honest-summary residual examples now cite the actually-open issues
(#881/#882/#872)" -- true when written; L1 closed #881 fourteen hours later. The
doc-honesty lane ran FIRST and nobody re-swept after the fixes landed. The
document had become self-contradictory: the summary said RV32 br_table still
declines while the backend row three sections up said it lowers. Re-pointed at
genuinely-open issues (#890, #851, #846), verified against `gh issue view`.

F2 (BLOCK) — claims.yaml PINNED the stale "#881" verbatim, so `claim_check`
reported 34/34 while green-confirming a false residual, and correcting the prose
would have turned the gate RED. CLAUDE.md says never fix a red gate by loosening
the ledger; this was the inverse -- a ledger entry that had gone false, so the
gate protected the defect instead of catching it.

The fix is structural, not a re-point: an ISSUE-NUMBER pin goes stale the moment
the issue is fixed, because `verbatim` only asserts the phrase is PRESENT. This
pin has now been wrong twice for exactly that reason (#782, then #881). It now
pins the CAPABILITY GAP -- "single-precision FPUs", the i64-from-f32 decline
that genuinely remains -- which becomes false precisely when the gap closes.
Red-first verified: replacing the phrase reddens SYNTH-F32-F64-VFP (exit 1),
restoring it returns green.

F3 -- three of seven lanes had NO changelog entry, including L4/#872: a
default-on soundness fix that MOVED SHIPPED BYTES (gust_poll 692->696, fact-spec
132->140). A user diffing v0.52->v0.53 output would have found no explanation.
Added L1 (#885), L4 (#888) and L7 (#889) entries, and collapsed a duplicate
`### Added` section that violated the Keep-a-Changelog structure the release
process mandates.

F4 -- README declared "No multi-memory" while the matrix (corrected this
release) says P with a CI-wired differential. Multi-memory phase 1 shipped in
v0.43 (#749); the README line was ~10 releases stale, so v0.53 would have
shipped two documents disagreeing about a capability.

F5 -- the #880 changelog entry claimed every pinned phrase is bound to its
oracle AND that oracle's CI wiring. SYNTH-MATRIX-WCET-COMPOSITION has neither --
the sound-WCET-bound row, one of the most safety-load-bearing claims in the
matrix, is the single exception. Named it rather than softening it away.

F6 -- #872's real remaining hole (a mid-segment `Pop {…,PC}` the segment-local
validator misses) and VCR-DEC-001's (a wrong-return-register rewrite accepted by
`validate_cfg_rewrite` AND VCR-RA-003 both, caught only by execution) existed
only in Rust doc-comments. Both now stated in the matrix and CHANGELOG: the
release was simultaneously OVERSTATING what is open and OMITTING what is.

claim_check 34/34, docs regenerated, render byte-fresh.

Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

---------

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant