thumb-2: i32.shl/shr_s/shr_u don't mask the shift amount mod 32 — amounts >=32 silently compile to 0 (VCR-SEL regression; Rocq ARM model masks like WASM so proof is vacuous)

[avrabe]

Summary

The thumb-2 (ARMv7-M) lowering for i32.shl, i32.shr_s, and i32.shr_u emits a bare register shift (LSL.W/ASR.W/LSR.W Rd, Rn, Rm) with no masking of the shift amount. On ARMv7-M, register-controlled shifts take the amount from Rm[7:0] and produce 0 (LSL/LSR) or the sign (ASR) when the amount is ≥ 32. WebAssembly requires the shift amount to be reduced modulo 32 (k = amount mod 32). Therefore any i32 shift whose amount is ≥ 32 — whether a constant or a runtime value — silently miscompiles.

This is a silent wrong-code bug (no trap, no diagnostic). The i64 shift path is unaffected (it correctly emits AND Rx, #0x3f); only the i32 rules regressed.

The regression came in with VCR-SEL-001 increment 2 (commit c778197, PR #639, epic #242): the old hand-written selector masked the amount with AND Rm, #31; the new verified-selector DSL rules dropped it. Worse, the generated rules carry a Rocq "Qed" correctness obligation that is vacuous against real hardware (details below).

Found by qemu thumb EXECUTION cross-checked against wasmtime 42.

Repro

(module
  (func (export "shl32")   (param i32) (result i32) (local.get 0) (i32.const 32)  (i32.shl))
  (func (export "shl33")   (param i32) (result i32) (local.get 0) (i32.const 33)  (i32.shl))
  (func (export "shl300")  (param i32) (result i32) (local.get 0) (i32.const 300) (i32.shl))
  (func (export "shr300")  (param i32) (result i32) (local.get 0) (i32.const 300) (i32.shr_u))
  (func (export "sar300")  (param i32) (result i32) (local.get 0) (i32.const 300) (i32.shr_s))
  (func (export "shl_var") (param i32 i32) (result i32) (local.get 0) (local.get 1) (i32.shl))
)

Compile: synth compile shift.wat -t cortex-m3 --all-exports --relocatable -o shift.o (synth 0.37.0). Result is identical with/without --optimize/--no-optimize.

Disassembly (llvm-objdump --triple=thumbv7m) — note the missing mask:

<shl_var>:  fa00 f201   lsl.w  r2, r0, r1          ; no AND r1,#31
<shl300>:   f240 112c   movw   r1, #0x12c          ; 300
            fa00 f201   lsl.w  r2, r0, r1          ; ARM uses r1[7:0]=44 -> 0

Compare the i64 path, which is correct:

<i64shl80>: ... f002 023f   and  r2, r2, #0x3f     ; i64 masks mod 64

Execution (qemu-system-arm lm3s6965evb) vs wasmtime 42

call	WASM spec (amount mod 32)	wasmtime 42	synth on qemu
shl32(1)	32 mod 32 = 0 → 1	1	0
shl33(1)	33 mod 32 = 1 → 2	2	0
shl300(1)	300 mod 32 = 12 → 4096	4096	0
shr300(0x80000000)	u >> 12 = 0x80000	524288	0
sar300(0x40000000)	0x40000000 >> 12	262144	0
shl_var(1, 33)	1 << 1	2	0

Spec citation

WebAssembly Core Specification, numeric instructions, ishl_N / ishr_u_N / ishr_s_N: "Let k be i₂ modulo N." For i32, N = 32. The amount is always reduced mod 32; there is no valid amount that yields 0 for a nonzero operand under <<.

Root cause

crates/synth-synthesis/src/sel_dsl/generated.rs:

pub fn rule_i32_shl(rd: Reg, rn: Reg, rm: Reg)   -> Vec<ArmOp> { vec![ArmOp::LslReg { rd, rn, rm }] }
pub fn rule_i32_shr_s(rd: Reg, rn: Reg, rm: Reg) -> Vec<ArmOp> { vec![ArmOp::AsrReg { rd, rn, rm }] }
pub fn rule_i32_shr_u(rd: Reg, rn: Reg, rm: Reg) -> Vec<ArmOp> { vec![ArmOp::LsrReg { rd, rn, rm }] }

No mask is applied. A correct lowering must reduce the amount mod 32 first (e.g. AND Rt, Rm, #31; LSL.W Rd, Rn, Rt), which the pre-VCR-SEL selector did.

(i32.rotr/i32.rotl are fine: register ROR is naturally mod-32, and the rotate-by-32-k idiom preserves that.)

Proof-soundness gap (verified-codegen model is unfaithful)

The generated rules claim a Rocq theorem rule_i32_shl_correct (Qed). It is vacuous because the ARM model masks like WASM does. In coq/Synth/ARM/ArmSemantics.v:

(* Shift operations — register (shift amount in Rm, masked to 0-31 by I32.shl etc.) *)
| LSL_reg rd rn rm =>
    let v := get_reg s rn in
    let shift_amt := get_reg s rm in
    Some (set_reg s rd (I32.shl v shift_amt))    (* <-- I32.shl masks mod 32 *)

and coq/Synth/Common/Integers.v:

Definition shl (x y : int) : int := repr (Z.shiftl x (unsigned y mod 32)).

So the Rocq LSL_reg semantics model an ARM register shift as x << (amount mod 32), which is not how ARMv7-M behaves (LSL(register) uses Rm[7:0] and yields 0 for amounts ≥ 32). VcrSelRules.v even comments: "the shift amount is masked mod 32 by the I32 semantics of LSL_reg/LSR_reg/ASR_reg/ROR_reg, matching WASM" — that assumption is false for the non-rotate shifts. The proof should be discharged against a faithful ARM shift semantics (Rm[7:0], saturate-to-0 at ≥ 32), which would fail for the bare-shift rule and force the mask back in.

Fix

Re-insert the AND Rm, #31 (mod-32 mask) into rule_i32_shl/rule_i32_shr_s/rule_i32_shr_u, and correct the LSL_reg/LSR_reg/ASR_reg ARM semantics in ArmSemantics.v to model Rm[7:0] (so the proof re-obligates the mask).

Environment: synth 0.37.0, cortex-m3, qemu-system-arm lm3s6965evb, wasmtime 42.0.1.

[avrabe]

Independently confirmed via qemu execution on fresh 0.37.0 — and a useful refinement for locating the regression: it is specific to the VCR-SEL DSL path (--all-exports / multi-function compile). The old single-function selector (-n f) still masks correctly, which pins the drop to the DSL migration you identified.

Contrast on the same 0.37.0 binary:

# --all-exports (VCR-SEL DSL)  -> NO mask, wrong:
<f>: movw r1,#0x20 ; lsl.w r2,r0,r1        ; shl(x,32) -> ARM uses r1[7:0]=32 -> 0
# -n f (old selector)          -> masks, correct:
<f>: and r12,r1,#0x1f ; lsl.w r4,r0,r12    ; shl(x,var) mod 32

Execution (full-image qemu, --all-exports): shl(1,32)=0, shl(1,var=33)=0 vs wasmtime 1/2; in-range control shl(1,31)=-2147483648 correct. So a real, silent, path-specific regression — any multi-function module (the normal case) shifting by a runtime amount that can reach ≥32 is affected.

Note for whoever tests the fix: the campaign's older "shift masking correct" result was on the -n f path, so a -n f repro will not reproduce this — use --all-exports.

[avrabe]

Triage confirmed — reproduced at byte level on main (v0.37.0) (maintainer loop): shl_var emits b510 fa00f201 4610 bd10 — bare LSL.W r2,r0,r1, no AND #31. Your analysis is accepted in full, including the vacuity claim: ArmSemantics.v models register shifts with WASM's mod-32 semantics while ARMv7-M uses Rm[7:0] — and the ISA bridge (PR #671) had documented this exact divergence as gaps 6–7 with an 'unreachable via WASM masking' judgment that the DSL rules invalidated. The bridge caught the model bug; the reachability judgment was wrong. Rotates are unaffected (rotation is cyclic, Rm[7:0] mod 32 ≡ WASM semantics — will pin with a test).

Fix landing today, directly: (1) constant amounts fold mod 32 at selection (zero extra bytes, most code unaffected); (2) runtime amounts get the AND #31 back in BOTH the hand-written arms and the DSL rule sequences; (3) the three rule proofs updated for the masked sequence (still discharge under the current model since mask∘mod32 ≡ mod32); (4) the HONEST model fix — Rm[7:0] semantics per bridge gaps 6–7, making the proofs non-vacuous — is the named follow-up (it re-lands with the flat-executor upgrade already in flight). Red→green from your exact repro table. If any frozen fixture contains a runtime-amount i32 shift its bytes change deliberately with the refreeze ritual.