plan(v0.62): scope #1145 — per-memory MPU isolation is unreachable BY CONSTRUCTION (10 -> 11)

[avrabe]

Scoping gale's #1145. Every claim reproduced on current main (0.61.0), not just the 0.60.0 they tested.

The structural gap

	multi-memory	MPU programming (RBAR/RASR)
--relocatable	✅ supported	❌ host owns startup, none emitted
self-contained	❌ declined (one R11 base)	✅ synth emits the reset handler

No invocation produces both, so per-memory MPU isolation is unreachable by construction rather than merely unimplemented.

The refusal is right and is not the bug. gale says so first: accepting the flag and emitting no MPU programming would be a silent no-op on a memory-safety control. Nothing here relaxes it.

The bigger finding, noted in passing

Memory 1 has no bounds-check story on any profile. Reproduced:

--safety-bounds software  exit=1  no object  skipping 'read_b'  #952
--safety-bounds mask      exit=1  no object  skipping 'read_b'  #952

So multi-memory phase 1 shipped a real capability (verified: 2 memories, __synth_wasm_data_1 present) that is usable only unchecked — a module touching memory 1 either compiles with no bounds checking at all, or does not compile. That is a compliance-envelope fact, not just an issue, and it outranks the MPU headline.

Downstream

Sole blocker for gale v0.5.0 (gale#138, isolation/multi-tenancy); REQ-OS-MPU-001 needs each tenant's memory in a distinct MPU region. They've been carrying blocked-synth-404 and are re-pointing here.

On gale's preferred option

They offer three and prefer the smallest — emit the region table as data only (__synth_mem_base_N/__synth_mem_size_N) and let the embedder program the MPU. There's precedent (__synth_wasm_data_1 already ships).

Recorded with the cost this release already named: it makes the embedder trusted for a memory-safety control, and RQ-62-VERIFYEMBED exists precisely because the embedder side has no gate — jess conformed to the register contract correctly by luck, twice, and was green both times. An unrefused obligation on a safety control is a larger version of that. If option 3 is taken, it ships with the conformance check, not before it.

The oracle is already written, by gale

a two-tenant image where tenant A writes outside its region and the write lands in tenant B's memory instead of faulting

A red-first execution criterion — exactly what the reach gating rule demands of any increment that widens acceptance.

Refs #1145, #406, #1132

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!