fix: bvurem VCs hung — multiplicative native Urem blast + re-proof (#101)

crates/ordeal/src/blast/muldiv.rs

@@ -108,9 +108,29 @@ pub fn blast_udiv(aig: &mut Aig, a: &Word, b: &Word) -> Word {
     blast_udivrem(aig, a, b).0
 }
 
-/// `bvurem` — the remainder half of [`blast_udivrem`].
+/// `bvurem` — MULTIPLICATIVE: `a - (a udiv b) * b` at the circuit level
+/// (issue #101; the unsigned twin of the #97 fix).
+///
+/// The divider's remainder output computes the same function, but a consumer
+/// equivalence VC pits it against a multiplicative model (`a - (a/b)*b` —
+/// synth's rem_u, loom's WASM form), and a divider-remainder-vs-multiplier
+/// cross-circuit proof is exponential: under 1 s on the 0.9.1 derived form
+/// became over 7 m 48 s (killed) on the divider form, per synth's #101
+/// measurements.
+/// This shape aligns structurally with those models (the shared `udiv`
+/// sub-circuit strashes), restoring propagation-speed VCs.
+///
+/// Exact for ALL inputs including division by zero, with no special case:
+/// SMT-LIB `a udiv 0` is all-ones, and `all-ones * 0 = 0`, so the result is
+/// `a - 0 = a` — precisely SMT-LIB `bvurem` by zero.
+///
+/// The term-level op stays native (`BvTerm::Urem`); only its circuit changed.
+/// Kani harnesses (urem_8/32/64) and the exhaustive width-8 evaluator
+/// differential re-verify the new circuit against the same reference.
 pub fn blast_urem(aig: &mut Aig, a: &Word, b: &Word) -> Word {
-    blast_udivrem(aig, a, b).1
+    let q = blast_udiv(aig, a, b);
+    let prod = blast_mul(aig, &q, b);
+    crate::blast::arith::blast_sub(aig, a, &prod)
 }
 
 // The SIGNED forms (`bvsdiv`/`bvsrem`) are deliberately NOT blasted here: they

crates/ordeal/src/blast_kernel.rs

@@ -666,10 +666,12 @@ pub fn blast_udiv(aig: &mut Aig, a: &[Lit], b: &[Lit]) -> Vec<Lit> {
     quo
 }
 
-/// `bvurem` — the remainder half.
+/// `bvurem` — MULTIPLICATIVE: `a - (a udiv b) * b` (issue #101), mirroring
+/// the production rule. Exact including /0 (all-ones * 0 = 0, so a - 0 = a).
 pub fn blast_urem(aig: &mut Aig, a: &[Lit], b: &[Lit]) -> Vec<Lit> {
-    let (_quo, rem) = blast_udivrem(aig, a, b);
-    rem
+    let q = blast_udiv(aig, a, b);
+    let prod = blast_mul(aig, &q, b);
+    blast_sub(aig, a, &prod)
 }
 
 #[cfg(test)]

crates/ordeal/src/lowering.rs

@@ -297,6 +297,29 @@ mod tests {
         );
     }
 
+    /// #101 regression guard: the UNSIGNED twin of #97 — native `Urem`
+    /// against the multiplicative model `a - (a udiv b) * b`, 32-bit
+    /// symbolic. On the divider-remainder blast this exceeded 7 m 48 s
+    /// (synth, killed); multiplicative it is ~5 ms. Same 10 s-deadline
+    /// headroom logic as the #97 guard.
+    #[test]
+    fn urem_vc_against_multiplicative_model_decides_fast() {
+        use crate::{BoolTerm, CheckResult, Solver};
+        let (a, b) = (var("a", 32), var("b", 32));
+        let ours = BvTerm::Urem(Box::new(a.clone()), Box::new(b.clone()));
+        let q = BvTerm::Udiv(Box::new(a.clone()), Box::new(b.clone()));
+        let theirs = BvTerm::Sub(Box::new(a), Box::new(BvTerm::Mul(Box::new(q), Box::new(b))));
+        let mut s = Solver::new();
+        s.assert(BoolTerm::Ne(Box::new(ours), Box::new(theirs)));
+        match s.check_with_deadline(10_000) {
+            CheckResult::Unsat(cert) => cert.recheck().expect("cert must re-check"),
+            other => panic!(
+                "urem VC must decide fast against the multiplicative model; got {other:?} — \
+                 the #101 cross-circuit regression is back"
+            ),
+        }
+    }
+
     /// #97 regression guard: the synth-shaped VC — this crate's srem value
     /// model vs a consumer's multiplicative model (Sdiv + Mls) — must decide
     /// fast at width 32. On the urem-based lowering it exceeded any sane

lean/BlastKernel.lean

@@ -1837,13 +1837,16 @@ def blast_udiv
   ok (quo, aig1)
 
 /-- [blast_kernel::blast_urem]:
-    Source: 'crates/ordeal/src/blast_kernel.rs', lines 670:0-673:1
+    Source: 'crates/ordeal/src/blast_kernel.rs', lines 671:0-675:1
     Visibility: public -/
 def blast_urem
   (aig : Aig) (a : Slice Lit) (b : Slice Lit) :
   Result ((alloc.vec.Vec Lit) × Aig)
   := do
-  let ((_, rem), aig1) ← blast_udivrem aig a b
-  ok (rem, aig1)
+  let (q, aig1) ← blast_udiv aig a b
+  let s := alloc.vec.Vec.deref q
+  let (prod, aig2) ← blast_mul aig1 s b
+  let s1 := alloc.vec.Vec.deref prod
+  blast_sub aig2 a s1
 
 end blast_kernel