proof: Rocq compile_wasm_to_arm diverges from Rust instruction selector

[avrabe]

Summary

The Rocq proof suite verifies a compile_wasm_to_arm function that differs from what the Rust compiler actually emits in multiple significant ways. The proofs are internally valid but do not establish correctness of the shipped binary.

---

Divergences

1. Division: trap guard elided in proof model

• Rocq (Compilation.v): models I32DivS as a single SDIV Rd, Rn, Rm instruction
• Rust (instruction_selector.rs): emits 4+ instructions — CMP Rm, #0 / BNE / UDF (trap) / SDIV — to guard against division by zero

The proof proves correctness of the one-instruction version, but the compiler ships the multi-instruction version. The trap guard is safety-critical on Cortex-M (SDIV with divisor=0 returns 0 on ARMv7-M, it does not fault).

2. Comparisons: wrong instruction count

• Rocq: models comparisons as 3 instructions — CMP + MOV Rd, #0 + MOVEQ Rd, #1
• Rust: emits only CMP (1 instruction), relying on subsequent branch instructions to consume flags

These are fundamentally different semantics — the Rocq version materializes a boolean in a register, the Rust version sets condition flags.

3. Register allocation model

• Rocq: hardcodes R0, R1, R2 for all operations (source operands always in R0/R1, destination always R0 or R2)
• Rust: uses dynamic register allocation (round-robin in select_default, stack-based in select_with_stack)

This means the register assignment in every proof theorem does not match the actual compiled output.

4. Constant materialization

• Rocq: always uses a single MOVW Rd, #imm (16-bit immediate)
• Rust: selects between MOVW, MVN (bitwise complement), and MOVW + MOVT (for 32-bit constants)

Constants > 16 bits are not representable in the Rocq model at all.

5. i64 operations

• Rocq: explicitly notes i64 is "simplified to 32-bit" — i64 operations are modeled as single-register 32-bit ops
• Rust: uses register pairs (e.g., R0:R1) for 64-bit values with multi-instruction sequences

The proof claims are vacuously true for i64 since the model does not represent the actual computation.

6. WasmSemantics.v catch-all

exec_wasm_instr contains a | _ => Some s catch-all that makes every unmodeled WASM instruction a no-op that succeeds. This means the WASM-side semantics are unfaithful — any instruction not explicitly handled (including all i64 ops) is treated as "do nothing and succeed."

---

Recommendation

Either:

1. Update Compilation.v to emit the same instruction sequences as the Rust compiler (preferred — this makes the proofs meaningful), or
2. Document the abstraction gap explicitly in coq/STATUS.md and restrict correctness claims to "the Rocq model is correct" rather than "the compiler is correct"

The current situation — where the proof suite is presented alongside the compiler with the implication that it establishes compiler correctness — is misleading.