Improve instruction selector: explicit WASM value stack tracking for deterministic register assignment

[avrabe]

Overview

The InstructionSelector in crates/synth-synthesis/src/instruction_selector.rs is designed as a transpiler (WASM → readable ARM assembly), not a full AOT compiler. This is a great architectural choice for safety-critical embedded targets — it keeps the output deterministic, traceable, and auditable. This issue captures a set of improvements that would make the implementation fully consistent with that transpiler design intent.

---

Current Situation

The select_default path allocates registers via a round-robin counter (next_reg % 10) independent of the WASM value stack state. This means:

• The registers assigned to rd, rn, rm have no defined relationship to actual WASM stack operands
• Register assignment is non-deterministic across calls (depends on next_reg state)
• The select_with_stack path does the right thing, but select_default is used as the fallback for all unmatched ops

Additionally, two Replacement variants produce silent Nop output instead of an explicit error:

Replacement::Var(_var_name) => Ok(vec![ArmOp::Nop]), // Placeholder
Replacement::Inline => Ok(vec![ArmOp::Nop]),          // Placeholder

---

Proposed Improvements

1. Explicit WASM Value Stack Tracker

Since WASM is a typed stack machine with statically known maximum stack depth (enforced by validation), each stack slot can be mapped to a fixed ARM register deterministically:

struct ValueStack {
    slots: Vec<Reg>, // index = WASM stack depth, value = assigned ARM register
}

impl ValueStack {
    fn pop(&mut self) -> Reg { self.slots.pop().expect("stack underflow") }
    fn push(&mut self, r: Reg) { self.slots.push(r) }
    fn peek(&self) -> Reg { *self.slots.last().expect("empty stack") }
}

This makes every generated ARM instruction's register choice directly traceable to a WASM stack position — exactly what a transpiler output should provide.

2. Static Stack-Slot-to-Register Mapping

For shallow WASM stacks (depth ≤ 10, which covers the vast majority of real WASM functions), a simple deterministic mapping suffices:

fn stack_depth_to_reg(depth: usize) -> Reg {
    ALLOCATABLE_REGS[depth] // bounded by WASM validation
}

No graph coloring, no linear scan needed — the transpiler goal means correctness and traceability matter more than optimal register reuse.

3. Explicit Errors for Unimplemented Replacement Variants

Replace silent Nop placeholders with proper errors:

Replacement::Var(name) => Err(Error::unimplemented(
    format!("Replacement::Var({name}) is not yet implemented")
)),
Replacement::Inline => Err(Error::unimplemented(
    "Replacement::Inline is not yet implemented"
)),

This ensures unimplemented paths fail loudly rather than silently producing incorrect output.

4. Unify select and select_with_stack

Once the value stack is tracked explicitly, select_default can use the same stack state as select_with_stack, eliminating the dual-path divergence.

---

Why This Matters

As a transpiler targeting safety-critical Cortex-M systems, each line of generated ARM assembly should have a clear, verifiable origin in the WASM source. Deterministic register assignment is a prerequisite for output auditability — which in turn supports the formal verification goals of the project (Rocq proofs, contract annotations).

---

Acceptance Criteria

• select_default reads operand registers from an explicit ValueStack rather than from alloc_reg()
• Register assignment for a given WASM op sequence is deterministic (same input → same output, independent of prior state)
• Replacement::Var and Replacement::Inline return Err(...) instead of Nop
• Existing tests continue to pass
• New test: verify register assignment for I32Add sequence matches expected stack-slot mapping

[avrabe]

Additional miscompilation paths found in audit

Issue #72 correctly identifies the round-robin register allocation and silent NOP placeholders. The following additional miscompilation paths were found in select_default that are not covered here:

1. LocalGet/LocalSet ignores the local index

In instruction_selector.rs (~lines 648-656), LocalGet and LocalSet always use SP+0 regardless of which local variable index is specified. This means all locals alias to the same stack slot — reads/writes to local 0, local 1, local 5, etc. all access the same memory location.

2. I32DivS missing INT_MIN/-1 overflow trap

In instruction_selector.rs (~lines 749-766), I32DivS guards against division by zero but does not check for the INT_MIN / -1 overflow case. On ARMv7-M, SDIV of 0x80000000 / -1 returns 0x80000000 (wraps silently) rather than trapping. The WASM spec requires a trap for this case.

3. i64 Load/Store bypass bounds checking

In instruction_selector.rs (~lines 1342-1356), 64-bit memory loads and stores do not perform bounds checking. The 32-bit load/store paths have bounds checks, but the i64 variants emit direct LDR/STR pairs without verifying the memory access is in-bounds.

Impact

These are in select_default which is the fallback for unmatched ops. select_with_stack handles most cases correctly, but any operation that falls through to select_default hits these paths. The recommendation from #72 to unify the paths (or remove select_default entirely) would address all of these.