--safety-bounds software/mpu are no-ops on the optimized codegen path (flight-safety: jess pins software for PX4)

[avrabe]

[synth maintainer side — issue-hunt loop] Surfaced while resolving #374 (jess will pin --safety-bounds software for the Pixhawk 6X-RT flight target). Verified, integrator-facing.

Summary

--safety-bounds {software,mpu} has no effect on the optimized codegen path — the path that lowers the bulk of a flight loop's i32/i64 loads and stores. They emit byte-identical code to none.

Evidence (cortex-m4, local.get 0; i32.const 7; i32.add; local.get 1; i32.store — a non-foldable dynamic address)

$ for m in none mpu software; do synth compile bc.wat --safety-bounds $m ...; done
none:     st = 8 instrs   (movs; adds; movw; movt; add.w ip; str.w; mov; bx)
mpu:      st = 8 instrs   (byte-identical)
software: st = 8 instrs   (byte-identical)

All three are movw/movt/add.w ip/str.w [ip] with no bounds check and no MPU region programming. mpu/software do write a .safety-manifest.json, but the codegen does not enforce it.

Where checks do get emitted

Inline software bounds (CMP/trap) are emitted only via the direct selector (select_with_stack) — i.e. only for ops the optimizer declines: bulk-memory (#374, via inline UDF), full-width i64 (#372), floats. Even there, the legacy Bhs Trap_Handler form (i32/i64 store/load helpers) resolves to an offset-0 fallthrough in a self-contained image (the Trap_Handler branch is only relocated under --relocatable); #374's bulk-mem switched to an inline UDF to trap correctly.

Impact

• A flight build pinned to --safety-bounds software gets inline memory protection only on declined ops, not the main i32/i32.store/i64 memory path. The integrator may reasonably believe software bounds-checks all memory access; today it does not.
• --safety-bounds mpu emits no MPU region programming at all — if memory protection is wanted, it must come from a separate platform MPU config (Zephyr/PX4-side), not synth.

Not a #374 blocker

#374's bulk-mem does trap correctly (direct selector + inline UDF, 16/16 differential). This is pre-existing and orthogonal — but must be resolved before a flight config relies on the flag.

Fix direction (to scope)

Either (a) make the optimized path honor BoundsCheckConfig (emit inline checks / real MPU MPU_RBAR/MPU_RASR programming), or (b) make --safety-bounds {software,mpu} an error on the optimized path until implemented (honest, like the GI-FPU-001 loud-skip contract) rather than silently emitting unchecked code with a manifest that claims otherwise. Also unify the trap mechanism: the direct-selector Bhs Trap_Handler is a self-contained no-op (use inline UDF like #374).

Filing as the tracking issue for the binary-safety "Phase 1" gap; will scope a rivet requirement.

[avrabe]

[synth maintainer side — issue-hunt triage, cross-link] Recording a second downstream consumer for release-planning: gale#86 (BYO-OS optional per-component MPU/PMP isolation) names this issue as its known blocker — --safety-bounds {software,mpu} being a no-op on the optimized codegen path is what stops the dissolved library-OS mode from containing a co-located untrusted component. So #377 now has two consumers: jess's PX4 --safety-bounds software pin (the original surfacing) and gale's BYO-OS isolation TCB.

No scope change — the fix is the same (make --safety-bounds effective on the optimized path), and it stays a deliberate byte-changing flight-path change (emitting bounds checks where there are none today), gated on re-freeze + differential + on-silicon confirmation, not folded into a routine pass. Flagging the accumulating demand so it ranks correctly in the next feature-release scoping.