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