chore(deps): bump ordeal =0.22.1 -> =0.36.0 and teach synth-verify the five 0.28 derived-op nodes

crates/synth-verify/Cargo.toml

@@ -61,7 +61,26 @@ synth-synthesis = { path = "../synth-synthesis", version = "0.90.0", optional =
 # the encoding is byte-identical at power-of-two widths, so unchanged verdicts
 # are evidence of non-affectedness and ANY changed verdict is the finding.
 # Reasoning alone would not have settled it.
-ordeal = "=0.22.1"
+#
+# 0.36.0 (#1590 lane, v0.91): dependabot's 0.34.0 failed Test + Z3 with 15
+# panics, ONE cause. 0.28 admitted the five formerly-derived ops to the closed
+# fragment as their own nodes (`BvTerm::{Not,Neg,Rotl,Sdiv,Srem}`, each with a
+# Lean-proven blasting rule), and `ordeal::lowering::{bvnot,bvneg,bvrotl,
+# bvsdiv,bvsrem}` now RETURN those nodes instead of a rewrite. The loud
+# catch-all in `canonicalize_bv` fired first, as designed: no verdict was ever
+# minted over an unmodeled node. term.rs/solver.rs now carry arms for all five
+# (ranks APPENDED so no existing operand order moves; none treated as
+# commutative; Z3 oracle maps them to its NATIVE bvnot/bvneg/bvrotl/bvsdiv/
+# bvsrem, so it checks ordeal's composite rules against an independent
+# implementation). Other 0.23..0.36 changes consumed here: 0.32 makes the
+# trusted term-DAG + query re-check run on EVERY `check*` (a trusted rejection
+# degrades to Unknown, never a wrong answer); 0.36 splits the certificate types
+# into `ordeal-cert` (re-exported at the old paths; new lock entry). MEASURED,
+# not assumed: the serial ordeal+Z3 differential over the whole synth-verify
+# suite gives the identical per-test verdict sequence on 0.22.1 and 0.36.0 (182
+# tests, 1283 verdicts, 0 disagreements), with 40 of those queries carrying a
+# Rotl/Sdiv node.
+ordeal = "=0.36.0"
 
 # Z3: optional differential oracle (feature `z3-solver`) — no longer default.
 # Default features only (NO `static-link-z3`/`bundled`): z3-sys links the

crates/synth-verify/src/solver.rs

@@ -283,6 +283,15 @@ mod z3_backend {
             BvTerm::Lshr(a, b) => bv_to_z3(a).bvlshr(&bv_to_z3(b)),
             BvTerm::Ashr(a, b) => bv_to_z3(a).bvashr(&bv_to_z3(b)),
             BvTerm::Rotr(a, b) => bv_to_z3(a).bvrotr(&bv_to_z3(b)),
+            // ordeal 0.28 derived-op nodes -> Z3's NATIVE operators (not the
+            // rewrite), so the oracle checks ordeal's proven composite rules
+            // against an independent implementation of the same SMT-LIB op.
+            // `bvsrem` (sign of the dividend), NOT `bvsmod`.
+            BvTerm::Rotl(a, b) => bv_to_z3(a).bvrotl(&bv_to_z3(b)),
+            BvTerm::Sdiv(a, b) => bv_to_z3(a).bvsdiv(&bv_to_z3(b)),
+            BvTerm::Srem(a, b) => bv_to_z3(a).bvsrem(&bv_to_z3(b)),
+            BvTerm::Not(a) => bv_to_z3(a).bvnot(),
+            BvTerm::Neg(a) => bv_to_z3(a).bvneg(),
             BvTerm::Extract { hi, lo, arg } => bv_to_z3(arg).extract(*hi, *lo),
             BvTerm::Concat(a, b) => bv_to_z3(a).concat(&bv_to_z3(b)),
             BvTerm::ZeroExt { by, arg } => bv_to_z3(arg).zero_ext(*by),

crates/synth-verify/src/term.rs

@@ -82,6 +82,18 @@ fn bv_rank(t: &BvTerm) -> u8 {
         BvTerm::ZeroExt { .. } => 16,
         BvTerm::SignExt { .. } => 17,
         BvTerm::Ite { .. } => 18,
+        // ordeal 0.28 (#192 phase 5) admitted the five formerly-DERIVED ops to
+        // the closed fragment as their own nodes, each with a Lean-proven
+        // blasting rule; `ordeal::lowering::{bvnot,bvneg,bvrotl,bvsdiv,bvsrem}`
+        // now return these nodes instead of a rewrite into the ops above.
+        // Ranks are APPENDED, never interleaved: renumbering would reorder the
+        // operands of every existing commutative node and move every CNF.
+        // Each gets its OWN rank for the reason the `Urem` note gives.
+        BvTerm::Not(..) => 19,
+        BvTerm::Neg(..) => 20,
+        BvTerm::Rotl(..) => 21,
+        BvTerm::Sdiv(..) => 22,
+        BvTerm::Srem(..) => 23,
         // ordeal ≥0.17 seals the term enums (`#[non_exhaustive]`, ordeal#104):
         // a variant is only ever added together with a proven blasting rule
         // and a CHANGELOG callout. synth-verify builds no terms outside the
@@ -150,9 +162,13 @@ fn ord_bv(a: &BvTerm, b: &BvTerm) -> Ordering {
         | (BvTerm::Lshr(a1, a2), BvTerm::Lshr(b1, b2))
         | (BvTerm::Ashr(a1, a2), BvTerm::Ashr(b1, b2))
         | (BvTerm::Rotr(a1, a2), BvTerm::Rotr(b1, b2))
+        | (BvTerm::Rotl(a1, a2), BvTerm::Rotl(b1, b2))
+        | (BvTerm::Sdiv(a1, a2), BvTerm::Sdiv(b1, b2))
+        | (BvTerm::Srem(a1, a2), BvTerm::Srem(b1, b2))
         | (BvTerm::Concat(a1, a2), BvTerm::Concat(b1, b2)) => {
             ord_bv(a1, b1).then_with(|| ord_bv(a2, b2))
         }
+        (BvTerm::Not(a1), BvTerm::Not(b1)) | (BvTerm::Neg(a1), BvTerm::Neg(b1)) => ord_bv(a1, b1),
         (
             BvTerm::Extract {
                 hi: ha,
@@ -285,6 +301,23 @@ fn canonicalize_bv(t: &BvTerm) -> BvTerm {
             let (a, b) = bin(a, b);
             BvTerm::Concat(a, b)
         }
+        // ordeal 0.28 derived-op nodes. None of the five commutes, so the
+        // operands keep their order (`bin`, never `comm`); only the children
+        // are canonicalized.
+        BvTerm::Rotl(a, b) => {
+            let (a, b) = bin(a, b);
+            BvTerm::Rotl(a, b)
+        }
+        BvTerm::Sdiv(a, b) => {
+            let (a, b) = bin(a, b);
+            BvTerm::Sdiv(a, b)
+        }
+        BvTerm::Srem(a, b) => {
+            let (a, b) = bin(a, b);
+            BvTerm::Srem(a, b)
+        }
+        BvTerm::Not(a) => BvTerm::Not(Box::new(canonicalize_bv(a))),
+        BvTerm::Neg(a) => BvTerm::Neg(Box::new(canonicalize_bv(a))),
         BvTerm::Extract { hi, lo, arg } => BvTerm::Extract {
             hi: *hi,
             lo: *lo,
@@ -894,6 +927,19 @@ fn fmt_bv(t: &BvTerm, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         BvTerm::Lshr(a, b) => fmt_bin(f, "bvlshr", a, b),
         BvTerm::Ashr(a, b) => fmt_bin(f, "bvashr", a, b),
         BvTerm::Rotr(a, b) => fmt_bin(f, "bvrotr", a, b),
+        BvTerm::Rotl(a, b) => fmt_bin(f, "bvrotl", a, b),
+        BvTerm::Sdiv(a, b) => fmt_bin(f, "bvsdiv", a, b),
+        BvTerm::Srem(a, b) => fmt_bin(f, "bvsrem", a, b),
+        BvTerm::Not(a) => {
+            write!(f, "(bvnot ")?;
+            fmt_bv(a, f)?;
+            write!(f, ")")
+        }
+        BvTerm::Neg(a) => {
+            write!(f, "(bvneg ")?;
+            fmt_bv(a, f)?;
+            write!(f, ")")
+        }
         BvTerm::Extract { hi, lo, arg } => {
             write!(f, "((_ extract {} {}) ", hi, lo)?;
             fmt_bv(arg, f)?;