feat(verify): model i64.rem_u/rem_s with native BvTerm::Urem/bvsrem (was havoc)

crates/synth-verify/src/arm_semantics.rs

@@ -689,20 +689,73 @@ impl ArmSemantics {
                 state.set_reg(rdhi, BV::new_const("i64_divu_hi", 32));
             }
 
-            ArmOp::I64RemS { rdlo, rdhi, .. } => {
-                // Signed 64-bit remainder (modulo)
-                // Real implementation would require __aeabi_ldivmod or equivalent
-                // For verification, return symbolic values
-                state.set_reg(rdlo, BV::new_const("i64_rems_lo", 32));
-                state.set_reg(rdhi, BV::new_const("i64_rems_hi", 32));
+            ArmOp::I64RemS {
+                rdlo,
+                rdhi,
+                rnlo,
+                rnhi,
+                rmlo,
+                rmhi,
+                ..
+            } => {
+                // Signed 64-bit remainder (modulo). Same shape as I64RemU but
+                // the SIGNED remainder (`bvsrem`, SMT-LIB sign-of-dividend). The
+                // shipped lowering is an `__aeabi_ldivmod` library call; the
+                // value it must produce is exactly the native 64-bit signed
+                // remainder. The value VC (`verify_i64_rem_value_preservation`)
+                // asserts the R0:R1 pair equals it on the non-trapping path.
+                // rem_s traps ONLY on ÷0 (`rem_s(INT64_MIN,-1) == 0`, no
+                // overflow trap).
+                let n_lo = state.get_reg(rnlo).clone();
+                let n_hi = state.get_reg(rnhi).clone();
+                let m_lo = state.get_reg(rmlo).clone();
+                let m_hi = state.get_reg(rmhi).clone();
+
+                let dividend = n_hi.concat(&n_lo); // 64-bit: n_hi:n_lo
+                let divisor = m_hi.concat(&m_lo); // 64-bit: m_hi:m_lo
+                let rem = dividend.bvsrem(&divisor); // native signed rem, 64-bit
+
+                state.set_reg(rdlo, rem.extract(31, 0));
+                state.set_reg(rdhi, rem.extract(63, 32));
             }
 
-            ArmOp::I64RemU { rdlo, rdhi, .. } => {
-                // Unsigned 64-bit remainder (modulo)
-                // Real implementation would require __aeabi_uldivmod or equivalent
-                // For verification, return symbolic values
-                state.set_reg(rdlo, BV::new_const("i64_remu_lo", 32));
-                state.set_reg(rdhi, BV::new_const("i64_remu_hi", 32));
+            ArmOp::I64RemU {
+                rdlo,
+                rdhi,
+                rnlo,
+                rnhi,
+                rmlo,
+                rmhi,
+                ..
+            } => {
+                // Unsigned 64-bit remainder (modulo). ARM32 has no 64-bit
+                // divide instruction — the shipped lowering expands this
+                // pseudo-op to an `__aeabi_uldivmod` library call — but for
+                // translation-validation the *value* the call must produce is
+                // exactly the native 64-bit unsigned remainder. Model it with
+                // the native `BvTerm::Urem` (ordeal 0.12, plumbed via
+                // `BV::bvurem`) instead of a HAVOC constant, so the value VC
+                // (`verify_i64_rem_value_preservation`) proves the register
+                // pair actually equals `dividend % divisor`.
+                //
+                // Compose the 64-bit operands from their register halves
+                // (`concat` puts self in the HIGH bits), take the 64-bit
+                // unsigned remainder, and split back to lo/hi. On a zero
+                // divisor SMT-LIB `bvurem` is total (returns the dividend),
+                // but WASM traps — the value clause is asserted only on the
+                // non-trapping path by the trap-guarded value VC, so this
+                // total model is sound.
+                let n_lo = state.get_reg(rnlo).clone();
+                let n_hi = state.get_reg(rnhi).clone();
+                let m_lo = state.get_reg(rmlo).clone();
+                let m_hi = state.get_reg(rmhi).clone();
+
+                let dividend = n_hi.concat(&n_lo); // 64-bit: n_hi:n_lo
+                let divisor = m_hi.concat(&m_lo); // 64-bit: m_hi:m_lo
+                let rem = dividend.bvurem(&divisor); // native bvurem, 64-bit
+
+                state.set_reg(rdlo, rem.extract(31, 0)); // low 32 bits
+                state.set_reg(rdhi, rem.extract(63, 32)); // high 32 bits
             }
 
             ArmOp::I64And {
@@ -2685,6 +2738,18 @@ impl ArmSemantics {
                 Ok(())
             }
             ArmOp::Strb { .. } | ArmOp::Strh { .. } => Ok(()),
+            // i64 rem_u/rem_s pseudo-ops (VCR-VER, #825/#836): register-only
+            // (they set the `rd*` pair), so they belong in this subset — the
+            // executor delegates to the general value model, which now builds a
+            // real `BvTerm::Urem`/`bvsrem` term. The ÷0 TRAP is NOT derived
+            // here (the bare pseudo-op carries no `UDF`); the VC reconstructs
+            // it from the pseudo-op's `elide_zero_guard` field, exactly like
+            // the i64 trap-only VC. div_u/div_s stay OUT (their 64-bit quotient
+            // value model is havoc — no value VC consumes it).
+            ArmOp::I64RemU { .. } | ArmOp::I64RemS { .. } => {
+                self.encode_op(op, state);
+                Ok(())
+            }
             other => Err(format!(
                 "op {other:?} outside the trap-derivation subset — loud decline"
             )),

crates/synth-verify/src/translation_validator.rs

@@ -382,7 +382,17 @@ impl TranslationValidator {
             WasmOp::I32DivS | WasmOp::I32DivU | WasmOp::I32RemS | WasmOp::I32RemU => {
                 self.verify_div_rem_trap_preservation(wasm_op, arm_ops)
             }
-            WasmOp::I64DivS | WasmOp::I64DivU | WasmOp::I64RemS | WasmOp::I64RemU => {
+            // i64 rem_u/rem_s carry a REAL value model now (native
+            // `BvTerm::Urem`/`bvsrem` — VCR-VER, #825/#836): the VC asserts
+            // both the ÷0 trap AND the 64-bit remainder value, so a lowering
+            // that computes the wrong remainder — or writes it to the wrong
+            // register pair — is rejected. i64 div still leaves its 64-bit
+            // quotient symbolic (the full quotient value VC is not well-posed
+            // in QF_BV at that width), so it stays trap-condition-only.
+            WasmOp::I64RemU | WasmOp::I64RemS => {
+                self.verify_i64_rem_value_preservation(wasm_op, arm_ops)
+            }
+            WasmOp::I64DivS | WasmOp::I64DivU => {
                 self.verify_i64_div_rem_trap_preservation(wasm_op, arm_ops)
             }
             WasmOp::Unreachable => {
@@ -631,6 +641,119 @@ impl TranslationValidator {
         Ok(Self::condition_verdict(&wasm_trap, &arm_trap))
     }
 
+    /// i64 `rem_u`/`rem_s` **value + trap** preservation (VCR-VER, #825/#836).
+    ///
+    /// Unlike [`Self::verify_i64_div_rem_trap_preservation`] (trap-only, used
+    /// for div where the 64-bit quotient value VC is not well-posed), this
+    /// gate asserts the FULL obligation for remainder: on the non-trapping
+    /// path the ARM register pair `R0:R1` must equal the native 64-bit
+    /// unsigned/signed remainder of the operands, AND the ÷0 trap must be
+    /// preserved. It is what makes the [`ArmSemantics`] `I64RemU` model —
+    /// which now builds a real `BvTerm::Urem` term (ordeal 0.12) instead of
+    /// HAVOC — actually load-bearing: a wrong remainder computation, or one
+    /// that writes the answer to the wrong register pair, is now `Invalid`.
+    ///
+    /// # Operand / result convention (the shipped ABI, NOT the op's fields)
+    ///
+    /// The value is READ from the FIXED ABI return registers `R0` (low) /
+    /// `R1` (high) and the operands are SEEDED at the FIXED ABI argument
+    /// registers — dividend `R0:R1`, divisor `R2:R3`. Reading the op's own
+    /// `rd*` fields (or seeding its own `rn*`/`rm*`) would make the VC
+    /// vacuous (read tracks write); anchoring on the ABI is exactly what lets
+    /// a pseudo-op whose destination deviates from `R0:R1` be REJECTED.
+    ///
+    /// # Trap-guarded value (why not a raw `==`)
+    ///
+    /// A bare `arm_value == wasm_value` would also assert the value on the ÷0
+    /// path, where WASM has no value and SMT-LIB `bvurem`-by-0 = the dividend
+    /// (total) — a spurious obligation. Routing through
+    /// [`crate::trap::DefineOrTrap`] + [`crate::trap::prove_trap_equivalence`]
+    /// guards the value clause under non-trap. The single branch-free
+    /// pseudo-op keeps the value ite-free, so no straight-line rewrite is
+    /// needed (unlike the i32 guarded-div machinery).
+    pub fn verify_i64_rem_value_preservation(
+        &self,
+        wasm_op: &WasmOp,
+        arm_ops: &[ArmOp],
+    ) -> Result<ValidationResult, VerificationError> {
+        let Some(div_op) = crate::trap::div_op(wasm_op) else {
+            return Err(VerificationError::UnsupportedOperation(format!(
+                "i64 rem value gate applies to rem only, got {wasm_op:?}"
+            )));
+        };
+        if !matches!(wasm_op, WasmOp::I64RemU | WasmOp::I64RemS) {
+            return Err(VerificationError::UnsupportedOperation(format!(
+                "i64 rem value gate supports i64 rem_u/rem_s only, got {wasm_op:?}"
+            )));
+        }
+
+        // Require the pseudo-op to be present and read its ÷0 guard-elision
+        // field (the selector emits exactly one). The ARM trap term is
+        // reconstructed from this field — NOT from `encode_sequence_br`'s
+        // `may_trap`, which is `false` for a bare pseudo-op (it carries no
+        // expanded `UDF`) — exactly as the i64 trap-only VC does. A lowering
+        // that elides the ÷0 guard without discharging `divisor != 0` yields a
+        // strictly weaker ARM trap and is rejected.
+        let Some((elide_zero, _elide_overflow)) = Self::i64_div_rem_guard_fields(arm_ops) else {
+            return Err(VerificationError::UnsupportedOperation(format!(
+                "i64 rem value gate needs an I64Rem pseudo-op in the sequence, \
+                 got {arm_ops:?}"
+            )));
+        };
+
+        // Four independent 32-bit half-symbols. Seed them at the FIXED ABI
+        // argument registers: dividend lo:hi = R0:R1, divisor lo:hi = R2:R3.
+        let dividend_lo = BV::new_const("input_dividend_lo", 32);
+        let dividend_hi = BV::new_const("input_dividend_hi", 32);
+        let divisor_lo = BV::new_const("input_divisor_lo", 32);
+        let divisor_hi = BV::new_const("input_divisor_hi", 32);
+
+        let mut state = ArmState::new_symbolic();
+        state.set_reg(&Reg::R0, dividend_lo.clone());
+        state.set_reg(&Reg::R1, dividend_hi.clone());
+        state.set_reg(&Reg::R2, divisor_lo.clone());
+        state.set_reg(&Reg::R3, divisor_hi.clone());
+        self.arm_encoder
+            .encode_sequence_br(arm_ops, &mut state)
+            .map_err(VerificationError::UnsupportedOperation)?;
+
+        // ARM result read from the FIXED ABI return pair R0:R1 (concat puts
+        // self in the HIGH bits).
+        let arm_lo = self.arm_encoder.extract_result(&state, &Reg::R0);
+        let arm_hi = self.arm_encoder.extract_result(&state, &Reg::R1);
+        let arm_value = arm_hi.concat(&arm_lo); // 64-bit R1:R0
+
+        // WASM spec side: the 64-bit remainder of the SAME operand symbols.
+        // Both sides feed identical concats, so the valid case is structural.
+        let dividend = dividend_hi.concat(&dividend_lo); // 64-bit
+        let divisor = divisor_hi.concat(&divisor_lo); // 64-bit
+        let wasm_value = match wasm_op {
+            WasmOp::I64RemU => dividend.bvurem(&divisor),
+            WasmOp::I64RemS => dividend.bvsrem(&divisor),
+            _ => unreachable!("guarded above"),
+        };
+        let wasm_trap = crate::trap::trap_div(div_op, &dividend, &divisor);
+
+        // ARM trap: rem's only trap is ÷0; present iff the guard was NOT
+        // elided. rem carries no overflow clause, so `elide_overflow=false`.
+        let arm_may_trap = Self::i64_arm_trap_from_fields(
+            div_op, &dividend, &divisor, elide_zero, /* elide_overflow */ false,
+        );
+
+        let orig = crate::trap::DefineOrTrap {
+            value: wasm_value,
+            may_trap: wasm_trap,
+        };
+        let opt = crate::trap::DefineOrTrap {
+            value: arm_value,
+            may_trap: arm_may_trap,
+        };
+
+        Ok(Self::trap_verdict_to_result(
+            crate::trap::prove_trap_equivalence(&orig, &opt),
+        ))
+    }
+
     /// Locate the i64 div/rem pseudo-op in a sequence and read its guard-elision
     /// fields as `(elide_zero, elide_overflow)`. `div_u`/`rem_s`/`rem_u` have no
     /// overflow guard, so their `elide_overflow` is reported `false`
@@ -2014,6 +2137,146 @@ mod tests {
         });
     }
 
+    // --- i64 rem VALUE model (VCR-VER, #825/#836): native BvTerm::Urem ---
+    //
+    // The i64 rem_u/rem_s VC now asserts the VALUE, not just the trap. Under
+    // the old HAVOC model the register result was an unconstrained fresh
+    // symbol, so ANY lowering (correct, wrong-remainder, wrong-destination)
+    // trivially satisfied a value-only obligation — the model proved nothing.
+    // These tests pin the value model as load-bearing.
+
+    /// Build an i64 rem pseudo-op with a chosen DESTINATION register pair. The
+    /// shipped ABI is `rd = R0:R1`; a lowering that writes elsewhere leaves
+    /// R0:R1 unrelated to the remainder and must be REJECTED by the value VC.
+    fn i64_rem_with_dest(op: &WasmOp, rdlo: Reg, rdhi: Reg) -> Vec<ArmOp> {
+        let arm = match op {
+            WasmOp::I64RemU => ArmOp::I64RemU {
+                rdlo,
+                rdhi,
+                rnlo: Reg::R0,
+                rnhi: Reg::R1,
+                rmlo: Reg::R2,
+                rmhi: Reg::R3,
+                elide_zero_guard: false,
+            },
+            WasmOp::I64RemS => ArmOp::I64RemS {
+                rdlo,
+                rdhi,
+                rnlo: Reg::R0,
+                rnhi: Reg::R1,
+                rmlo: Reg::R2,
+                rmhi: Reg::R3,
+                elide_zero_guard: false,
+            },
+            _ => unreachable!("i64_rem_with_dest: not an i64 rem op"),
+        };
+        vec![arm]
+    }
+
+    /// GREEN: the shipped rem_u/rem_s lowering (`rd = R0:R1`) computes the
+    /// correct 64-bit remainder into the ABI return pair — the value+trap VC
+    /// must be Verified.
+    #[test]
+    fn i64_rem_shipped_value_is_verified() {
+        with_verification_context(|| {
+            let validator = TranslationValidator::new();
+            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
+                let arm_ops = shipped_i64_div_rem(&op, false, false);
+                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
+                assert_eq!(
+                    result,
+                    ValidationResult::Verified,
+                    "GREEN: {op:?} shipped lowering (correct value + ÷0 guard) must be Verified"
+                );
+            }
+        });
+    }
+
+    /// RED / NON-VACUITY (the key gate): a lowering that writes the remainder
+    /// to the WRONG destination pair (`rd = R2:R3` instead of the ABI `R0:R1`)
+    /// leaves R0:R1 holding the (unrelated) input operands, so the ABI return
+    /// pair is NOT the remainder. Under the old HAVOC model this was ACCEPTED
+    /// (the result symbol was unconstrained); the native `BvTerm::Urem` value
+    /// model now REJECTS it. This is the accepted-under-havoc → rejected-now
+    /// discriminator.
+    #[test]
+    fn i64_rem_wrong_destination_register_is_rejected() {
+        with_verification_context(|| {
+            let validator = TranslationValidator::new();
+            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
+                let arm_ops = i64_rem_with_dest(&op, Reg::R2, Reg::R3);
+                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
+                assert!(
+                    matches!(result, ValidationResult::Invalid { .. }),
+                    "RED: {op:?} writing the remainder to R2:R3 (not the ABI R0:R1) \
+                     leaves R0:R1 non-remainder — must be Invalid, got {result:?}"
+                );
+            }
+        });
+    }
+
+    /// NON-VACUITY control: the correct-destination and wrong-destination
+    /// lowerings must give OPPOSITE verdicts. A gate that returned the same
+    /// verdict for both (as the HAVOC model did — both trivially valued) would
+    /// be vacuous.
+    #[test]
+    fn i64_rem_destination_field_is_load_bearing() {
+        with_verification_context(|| {
+            let validator = TranslationValidator::new();
+            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
+                let correct = validator
+                    .verify_trap_preservation(&op, &i64_rem_with_dest(&op, Reg::R0, Reg::R1))
+                    .unwrap();
+                let wrong = validator
+                    .verify_trap_preservation(&op, &i64_rem_with_dest(&op, Reg::R2, Reg::R3))
+                    .unwrap();
+                assert_eq!(correct, ValidationResult::Verified, "{op:?} correct dest");
+                assert!(
+                    matches!(wrong, ValidationResult::Invalid { .. }),
+                    "{op:?} wrong dest"
+                );
+                assert_ne!(
+                    correct, wrong,
+                    "non-vacuity: {op:?} destination register must change the verdict"
+                );
+            }
+        });
+    }
+
+    /// EVIDENCE that the value model closed a real gap: the OLD trap-only VC
+    /// (`verify_i64_div_rem_trap_preservation`, still present for div) ACCEPTS
+    /// the wrong-destination rem lowering — it never reads the value — whereas
+    /// the NEW value VC (`verify_i64_rem_value_preservation`, dispatched by
+    /// `verify_trap_preservation`) REJECTS it. Opposite verdicts from the two
+    /// gates on the same input is the accepted-under-havoc → rejected-now
+    /// proof, made concrete rather than merely narrated.
+    #[test]
+    fn i64_rem_value_model_closes_a_trap_only_gap() {
+        with_verification_context(|| {
+            let validator = TranslationValidator::new();
+            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
+                let wrong = i64_rem_with_dest(&op, Reg::R2, Reg::R3);
+                // Old trap-only path: value/destination invisible → accepted.
+                let trap_only = validator
+                    .verify_i64_div_rem_trap_preservation(&op, &wrong)
+                    .unwrap();
+                assert_eq!(
+                    trap_only,
+                    ValidationResult::Verified,
+                    "the trap-ONLY VC is blind to the wrong destination (this is the \
+                     havoc-era gap): {op:?} expected Verified, got {trap_only:?}"
+                );
+                // New value+trap path: destination is load-bearing → rejected.
+                let value = validator.verify_trap_preservation(&op, &wrong).unwrap();
+                assert!(
+                    matches!(value, ValidationResult::Invalid { .. }),
+                    "the value VC catches it: {op:?} expected Invalid, got {value:?}"
+                );
+                assert_ne!(trap_only, value, "the two gates must disagree ({op:?})");
+            }
+        });
+    }
+
     // --- call_indirect (LIVE at the pseudo-op guard level, #642/#664/#676) ---
 
     fn call_indirect_pseudo(