fix(trap-semantics): unreachable traps on every backend (#665); rv32 rem_s drops the spurious INT_MIN/-1 guard (#666) (#668)

#665 — wasm `unreachable` compiled to a NO-OP on thumb-2 AND rv32 (falls
through instead of trapping, WASM Core §4.4.5). Root cause was ONE decode
drop: `convert_operator` returned `None` for `Unreachable` and
`is_intentionally_ignored` whitelisted it alongside `Nop`, so no backend
ever received the op — the selector trap arms (ARM `UDF #0`, RV32 `ebreak`)
already existed but were dead code. Fix per path:

- decoder (synth-core): `Unreachable` now decodes to `WasmOp::Unreachable`;
  only `Nop` stays intentionally ignorable.
- ARM direct (`select_with_stack`) + `select_default`: existing `UDF #0`
  arms now fire (no change needed).
- ARM optimized path (optimizer_bridge): previously lumped `Unreachable`
  in with Nop as an IR placeholder — now a typed loud-DECLINE to the direct
  selector (the bridge `Opcode` enum has no trap opcode; adding one would
  ripple through the #513 mirror-pinned reg_effect/rewrite_op machinery).
  Same decline-don't-drop pattern as #120 floats / #500 non-tail return.
  No new ArmOp on the optimized path, so the #511 estimator oracle is
  untouched (Udf was already covered by the div-zero guards).
- RV32: existing `ebreak` arm now fires (no change needed).
- aarch64: new `brk #0` encoder + selector arm (was a loud-decline).

#666 — rv32 `i32.rem_s(INT_MIN,-1)` spuriously trapped: the selector shared
div_s's INT_MIN/-1 overflow `ebreak` guard with rem_s via
`bin_with_signed_div_traps`. WASM §4.3.2 defines irem_s(INT_MIN,-1) = 0
with NO trap, and RISC-V M-ext `rem` already returns 0 for the overflow
case (unprivileged spec §7.2), so rem_s now takes plain
`bin_with_zero_trap` — zero-divisor guard KEPT, bare `rem` is exactly
wasm-correct. The pre-existing test `rv32_signed_rem_also_gets_overflow_guard`
pinned the BUG; it is rewritten as the #633-twin fix-guard pins
(`rv32_signed_rem_carries_only_zero_guard_666` +
`rv32_signed_div_still_carries_both_guards_666`), mirroring ARM's
`test_633_i64_rems_has_no_overflow_guard` and the existing i64 RV32 pin.

Oracles (red on origin/main, green here; CI job trap-semantics-oracle):
- scripts/repro/unreachable_665_differential.py — thumb2 + rv32 under
  unicorn vs wasmtime: bare `unreachable` traps, guarded `unreachable`
  taken traps, NOT taken returns normally (non-vacuity). Red on main:
  boom(7,9) "returned" 7 (arg fall-through) on both ISAs. Known gap kept
  visible: rv32 loud-declines the if/else-result-with-unreachable shape
  (#343 arity check) — contract-compliant (never falls through).
- scripts/repro/rem_s_666_differential.py — rv32 trap table:
  rems(INT_MIN,-1)→0 no-trap (red on main: spurious ebreak),
  rems(INT_MIN,1)→0, rems(7,3)→1, rems(-7,3)→-1, rems(7,0) traps,
  divs(INT_MIN,-1) traps, divs(7,0) traps, divs(7,3)→2.

Frozen anchors 10/10 bit-identical (no fixture contains `unreachable` —
verified control_step/flight_seam/flight_seam_flat/signed_div_const).
Workspace tests 108/108 suites green; fmt + clippy -D warnings clean.

Fixes #665
Fixes #666

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Author: avrabe

.github/workflows/ci.yml

@@ -286,6 +286,42 @@ jobs:
       - name: Run two-move execution oracle
         run: python scripts/repro/cmp_select_two_move_differential.py
 
+  trap-semantics-oracle:
+    name: trap-semantics oracle (#665 unreachable + #666 rem_s)
+    # #665: wasm `unreachable` must TRAP (WASM §4.4.5) — it was decoder-dropped
+    # to a no-op on EVERY backend, falling through panic/abort guards. #666:
+    # rv32 rem_s wrongly carried div_s's INT_MIN/-1 ebreak guard —
+    # irem_s(INT_MIN,-1) = 0, no trap (§4.3.2). Both EXECUTION-validated under
+    # unicorn (thumb2 + rv32) against wasmtime ground truth, including the
+    # non-vacuity direction (a guarded `unreachable` NOT taken runs normally;
+    # rem_s zero-divisor + div_s overflow traps are KEPT). Isolated job:
+    # emulation deps pip-installed here ONLY.
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v7
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Cache Cargo dependencies
+        uses: actions/cache@v6
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-
+      - name: Build synth
+        run: cargo build -p synth-cli
+      - uses: actions/setup-python@v6
+        with:
+          python-version: "3.x"
+      - name: Install emulation deps
+        run: pip install wasmtime unicorn pyelftools
+      - name: Run unreachable trap oracle (#665, thumb2 + rv32)
+        run: SYNTH=./target/debug/synth python scripts/repro/unreachable_665_differential.py
+      - name: Run rem_s trap-table oracle (#666, rv32)
+        run: SYNTH=./target/debug/synth python scripts/repro/rem_s_666_differential.py
+
   fact-spec-oracle:
     name: fact-spec elision oracle (#494 phases 2 + 2b)
     # VCR-PERF-002 Phase 2 (#494): the proof-carrying-specialization lever

crates/synth-backend-aarch64/src/encoder.rs

@@ -67,6 +67,13 @@ pub fn ret() -> u32 {
     0xD65F_03C0
 }
 
+/// `brk #imm16` — A64 breakpoint/trap. Used for wasm `unreachable` (#665):
+/// WASM §4.4.5 requires an unconditional trap, the A64 analogue of Thumb-2
+/// `udf #0` / RV32 `ebreak`.
+pub fn brk(imm16: u16) -> u32 {
+    0xD420_0000 | ((imm16 as u32) << 5)
+}
+
 /// Materialize a 32-bit constant into `wd` with `movz` + optional `movk`.
 /// Returns 1 or 2 words.
 pub fn mov_imm32(rd: Reg, value: u32) -> Vec<u32> {

crates/synth-backend-aarch64/src/selector.rs

@@ -79,6 +79,12 @@ pub fn select(ops: &[WasmOp], num_params: u32) -> Result<Vec<u32>, SelectError>
                 }
                 stack.push(dst);
             }
+            // #665: wasm `unreachable` traps unconditionally (WASM §4.4.5) —
+            // emit `brk #0`, the A64 analogue of Thumb-2 `udf #0` / RV32
+            // `ebreak`. It pushes nothing; everything after it is
+            // wasm-validated dead code, and the trailing `End` epilogue after
+            // the trap is harmless.
+            WasmOp::Unreachable => words.push(enc::brk(0)),
             WasmOp::I32Add => binop(&mut words, &mut stack, enc::add)?,
             WasmOp::I32Sub => binop(&mut words, &mut stack, enc::sub)?,
             WasmOp::I32Mul => binop(&mut words, &mut stack, enc::mul)?,

crates/synth-backend-riscv/src/selector.rs

@@ -1553,7 +1553,16 @@ impl Selector {
                 self.bin_with_zero_trap(op, |rd, rs1, rs2| RiscVOp::Divu { rd, rs1, rs2 })?
             }
             I32RemS => {
-                self.bin_with_signed_div_traps(op, |rd, rs1, rs2| RiscVOp::Rem { rd, rs1, rs2 })?
+                // #666: rem_s carries ONLY the zero-divisor guard. WASM §4.3.2
+                // defines irem_s(INT_MIN, -1) = 0 (no trap) — the INT_MIN/-1
+                // overflow trap belongs to div_s alone. The div_s guard was
+                // wrongly shared here, so rem_s(INT_MIN,-1) spuriously
+                // ebreak'd. RISC-V M-ext `rem` already returns 0 for the
+                // overflow case (RISC-V unprivileged spec §7.2, "the remainder
+                // of an overflowing signed division is zero"), so the bare
+                // instruction is exactly wasm-correct. Twin of the ARM #633
+                // fix-guard (test_633_i64_rems_has_no_overflow_guard).
+                self.bin_with_zero_trap(op, |rd, rs1, rs2| RiscVOp::Rem { rd, rs1, rs2 })?
             }
             I32RemU => {
                 self.bin_with_zero_trap(op, |rd, rs1, rs2| RiscVOp::Remu { rd, rs1, rs2 })?
@@ -2130,8 +2139,12 @@ impl Selector {
     }
 
     /// Variant of `bin_with_zero_trap` that also guards `INT_MIN / -1`, which
-    /// `div`/`rem` would silently return as `INT_MIN` / `0` respectively — WASM
-    /// semantics require a trap. See `docs/binary-safety-design.md` §3.3.
+    /// `div` would silently return as `INT_MIN` — WASM `idiv_s` semantics
+    /// require a trap. See `docs/binary-safety-design.md` §3.3.
+    ///
+    /// `div_s` ONLY — never `rem_s` (#666): WASM `irem_s(INT_MIN, -1)` is
+    /// defined as 0 (no trap), and RISC-V `rem` already returns 0 for that
+    /// case, so `rem_s` takes plain [`Self::bin_with_zero_trap`].
     ///
     /// Sequence:
     /// ```text
@@ -6213,8 +6226,15 @@ mod tests {
         assert_eq!(bne_count, 1, "only zero-divisor guard expected for div_u");
     }
 
+    /// #666 fix-guard twin (RV32 analogue of the ARM #633 pin,
+    /// `test_633_i64_rems_has_no_overflow_guard`): i32 `rem_s` must carry ONLY
+    /// the zero-divisor guard — WASM §4.3.2 defines `irem_s(INT_MIN, -1) = 0`
+    /// (no trap), and RISC-V M-ext `rem` already returns 0 for that case, so
+    /// the INT_MIN/-1 `ebreak` belongs to `div_s` alone. This test previously
+    /// pinned the BUG (asserting rem_s got the overflow guard too, which made
+    /// `rem_s(INT_MIN, -1)` spuriously trap).
     #[test]
-    fn rv32_signed_rem_also_gets_overflow_guard() {
+    fn rv32_signed_rem_carries_only_zero_guard_666() {
         let opts = SelectorOptions::wasm_compliant();
         let out = s_with_opts(
             &[
@@ -6235,8 +6255,38 @@ mod tests {
                 }
             )
         });
-        assert!(bne_count >= 3);
-        assert!(count(&out, |op| matches!(op, RiscVOp::Rem { .. })) == 1);
+        assert_eq!(
+            bne_count, 1,
+            "rem_s must emit only the zero-divisor BNE (no INT_MIN/-1 guard): {out:?}"
+        );
+        assert_eq!(
+            count(&out, |op| matches!(op, RiscVOp::Ebreak)),
+            1,
+            "rem_s must emit exactly one ebreak (the zero-divisor trap): {out:?}"
+        );
+        assert_eq!(count(&out, |op| matches!(op, RiscVOp::Rem { .. })), 1);
+    }
+
+    /// #666 twin, other direction: `div_s` KEEPS both guards under
+    /// wasm-compliant options — removing the rem_s over-trap must not weaken
+    /// the div_s overflow trap.
+    #[test]
+    fn rv32_signed_div_still_carries_both_guards_666() {
+        let opts = SelectorOptions::wasm_compliant();
+        let out = s_with_opts(
+            &[
+                WasmOp::LocalGet(0),
+                WasmOp::LocalGet(1),
+                WasmOp::I32DivS,
+                WasmOp::End,
+            ],
+            2,
+            opts,
+        );
+        assert!(
+            count(&out, |op| matches!(op, RiscVOp::Ebreak)) >= 2,
+            "div_s keeps the zero-divisor AND INT_MIN/-1 ebreaks: {out:?}"
+        );
     }
 
     /// Two-arg call: top-of-stack args move to a0 and a1 in source order.

crates/synth-core/src/wasm_decoder.rs

@@ -1042,7 +1042,7 @@ pub struct FunctionOps {
     /// function (diagnostic + symbol absent → link error names it) instead —
     /// the #180/#185 "unsupported op must Err, never silently continue"
     /// contract. `None` once every op decoded or was intentionally ignorable
-    /// (Nop/Unreachable).
+    /// (Nop).
     pub unsupported: Option<String>,
     /// #509: blocktype arity side-table — `(param_count, result_count)` of the
     /// k-th `Block`/`Loop`/`If` op in `ops`, in order of appearance.
@@ -1135,7 +1135,7 @@ fn decode_function_body(
             op_offsets.push(offset as u32);
         } else if unsupported.is_none() && !is_intentionally_ignored(&op) {
             // The op was DROPPED by `convert_operator` (`_ => None`) and is not
-            // an intentional no-op (Nop/Unreachable) — record it so the
+            // an intentional no-op (Nop) — record it so the
             // function is loud-skipped rather than silently miscompiled (#369).
             unsupported = Some(format!("{op:?}"));
         }
@@ -1148,9 +1148,13 @@ fn decode_function_body(
 /// carry no value-affecting semantics for our backend, so dropping them is
 /// correct (NOT a silent miscompile). Everything else that decodes to `None`
 /// is an unsupported op that must loud-skip its function (#369).
+///
+/// #665: `Unreachable` is NOT on this list — it traps (WASM §4.4.5), so it
+/// decodes to `WasmOp::Unreachable` and every backend lowers it to a trap
+/// instruction (or loud-declines). Only `Nop` is genuinely ignorable.
 fn is_intentionally_ignored(op: &wasmparser::Operator) -> bool {
     use wasmparser::Operator::*;
-    matches!(op, Nop | Unreachable)
+    matches!(op, Nop)
 }
 
 /// Convert a wasmparser Operator to our WasmOp enum
@@ -1338,8 +1342,16 @@ fn convert_operator(op: &wasmparser::Operator) -> Option<WasmOp> {
         // End is needed for control flow pattern matching
         End => Some(WasmOp::End),
 
-        // Nop/Unreachable - skip these
-        Nop | Unreachable => None,
+        // #665: `unreachable` MUST reach the backends — WASM Core §4.4.5
+        // requires it to trap unconditionally. It was previously dropped here
+        // (treated like Nop), so every backend compiled it to a no-op and
+        // control FELL THROUGH panic!/abort/unreachable-default guards with
+        // undefined register state. The selector arms (ARM: UDF #0, RV32:
+        // ebreak) already existed; they just never received the op.
+        Unreachable => Some(WasmOp::Unreachable),
+
+        // Nop - skip (genuinely no semantics)
+        Nop => None,
 
         // Drop is needed for br_if pattern matching
         Drop => Some(WasmOp::Drop),

crates/synth-synthesis/src/optimizer_bridge.rs

@@ -2526,15 +2526,31 @@ impl OptimizerBridge {
                     continue;
                 }
 
+                // #665: `unreachable` must TRAP (WASM §4.4.5). The optimized
+                // path's local `Opcode` enum has no trap opcode, and adding
+                // one would ripple through the #513 mirror-pinned
+                // reg_effect/rewrite_op machinery — so decline to the direct
+                // selector, whose `Unreachable` arm emits `UDF #0`. Same
+                // decline-don't-drop pattern as #120 floats and the #500
+                // non-tail `return` (this arm previously lumped `unreachable`
+                // in with Nop as a placeholder — a silent fall-through).
+                WasmOp::Unreachable => {
+                    return Err(synth_core::Error::validation(
+                        "optimized lowering path does not support `unreachable` \
+                         (no trap opcode in the bridge IR); the direct \
+                         instruction selector lowers it to UDF #0 — issue #665",
+                    ));
+                }
+
                 // ===== Stack-neutral control-flow / no-op ops =====
                 //
-                // Nop / Unreachable / Return have no slot_stack effect at
+                // Nop / Return have no slot_stack effect at
                 // this layer (Return's value handling is done later by the
                 // function-epilogue codegen in `ir_to_arm`). They still
                 // emit an IR Nop placeholder so the IR length is in lockstep
                 // with the wasm op index for any downstream pass that
                 // relies on positional alignment.
-                WasmOp::Nop | WasmOp::Unreachable | WasmOp::Return => {
+                WasmOp::Nop | WasmOp::Return => {
                     // #500: `return` is representable here only as a Nop
                     // placeholder — the real epilogue is emitted once at the
                     // function end, and the callee-saved push/pop frame is

scripts/repro/rem_s_666.wat

@@ -0,0 +1,12 @@
+;; #666 — rv32 i32.rem_s(INT_MIN, -1) spuriously trapped.
+;;
+;; WASM Core §4.3.2: irem_s(INT_MIN, -1) = 0, NO trap — only idiv_s traps on
+;; the INT_MIN/-1 overflow. The rv32 selector shared div_s's INT_MIN/-1
+;; ebreak guard with rem_s; RISC-V M-ext `rem` already returns 0 for the
+;; overflow case, so the guard was pure over-trap. Twin of the ARM #633
+;; fix-guard pin.
+(module
+  (func (export "rems") (param i32 i32) (result i32)
+    (i32.rem_s (local.get 0) (local.get 1)))
+  (func (export "divs") (param i32 i32) (result i32)
+    (i32.div_s (local.get 0) (local.get 1))))