feat(verify): #433 — take ordeal 0.33.0 and decide memory/UF goals via Solver::from_sliver

loom-core/Cargo.toml

@@ -63,7 +63,7 @@ features = ["bundled"]
 # `ordeal::trap::DefineOrTrap`. Gated behind `verification` so the default
 # build carries it and the no-verification build stays lean.
 [dependencies.ordeal]
-version = "0.30.0"
+version = "0.33.0"
 optional = true
 
 [lib]

loom-core/src/rule_solver.rs

@@ -1072,10 +1072,13 @@ pub(crate) mod ordeal_backend {
         /// Neither side reads memory: the closed-core `Ne` goal, exactly as
         /// slices 1-2 built it.
         Core(BoolTerm),
-        /// A memory obligation, already eliminated into the closed core by
-        /// the array sliver (eager read-over-write + array congruence). No
-        /// array construct remains; the ordinary blast pipeline decides it.
-        Sliver(Vec<BoolTerm>),
+        /// A memory or call obligation, as a solver built by
+        /// [`ordeal::Solver::from_sliver`]. It holds the closed-core
+        /// elimination (read-over-write + array/UF congruence) AND the
+        /// extended query it came from, so every verdict it returns has first
+        /// passed ordeal's trusted `check_sliver_lowering` (#433): the core it
+        /// decided is provably the elimination of the query loom asked.
+        Sliver(ordeal::Solver),
     }
 
     /// Why an equivalence goal could not be lowered.
@@ -1087,6 +1090,21 @@ pub(crate) mod ordeal_backend {
         Sliver(ordeal::sliver::SliverError),
     }
 
+    /// A [`Solver`] holding the goal `lhs != rhs`, ready for a bounded check.
+    pub(crate) fn solver_for_goal_ne(
+        lhs: &RuleTerm,
+        rhs: &RuleTerm,
+    ) -> Result<ordeal::Solver, GoalError> {
+        Ok(match lower_goal_ne(lhs, rhs)? {
+            GoalLowering::Core(ne) => {
+                let mut solver = ordeal::Solver::new();
+                solver.assert(ne);
+                solver
+            }
+            GoalLowering::Sliver(solver) => solver,
+        })
+    }
+
     /// Lower the goal `lhs != rhs`, routing through the array sliver when
     /// either side reads memory.
     ///
@@ -1097,8 +1115,14 @@ pub(crate) mod ordeal_backend {
     /// instead of a hang (loom#347 is exactly that failure mode), and an
     /// out-of-sliver query must surface as a REFUSAL the seam can defer to
     /// the incumbent on, not as an undecided verdict the call site turns
-    /// into a revert. Lowering here and asserting the core ourselves keeps
-    /// both properties.
+    /// into a revert. `Solver::from_sliver` (ordeal#236) keeps both
+    /// properties: the refusal is an `Err`, and every bound applies to the
+    /// solver it returns.
+    ///
+    /// Nor `ordeal::sliver::lower` with the core asserted by hand, which is
+    /// what this did until #433: a solver built that way never runs the
+    /// trusted `check_sliver_lowering`, so a verdict would rest on an
+    /// unchecked elimination.
     pub(crate) fn lower_goal_ne(lhs: &RuleTerm, rhs: &RuleTerm) -> Result<GoalLowering, GoalError> {
         let l = lower_ext(lhs).map_err(GoalError::Gap)?;
         let r = lower_ext(rhs).map_err(GoalError::Gap)?;
@@ -1108,7 +1132,7 @@ pub(crate) mod ordeal_backend {
             (ExtBvTerm::Core(a), ExtBvTerm::Core(b)) => {
                 Ok(GoalLowering::Core(BoolTerm::Ne(Box::new(a), Box::new(b))))
             }
-            (a, b) => ordeal::sliver::lower(&[ExtBoolTerm::Ne(a, b)])
+            (a, b) => ordeal::Solver::from_sliver(&[ExtBoolTerm::Ne(a, b)])
                 .map(GoalLowering::Sliver)
                 .map_err(GoalError::Sliver),
         }

loom-core/src/verify_solver.rs

@@ -830,27 +830,16 @@ impl BoundedOrdealSolver {
 #[cfg(feature = "verification")]
 impl RuleSolver for BoundedOrdealSolver {
     fn prove_rule_equiv(&self, lhs: &RuleTerm, rhs: &RuleTerm) -> RuleVerdict {
-        use crate::rule_solver::ordeal_backend::{
-            GoalLowering, lower_goal_ne, render_ordeal_model,
-        };
-        use ordeal::{CheckResult, Solver};
-
-        let mut solver = Solver::new();
-        match lower_goal_ne(lhs, rhs) {
-            Ok(GoalLowering::Core(ne)) => solver.assert(ne),
-            // The sliver has already eliminated every array construct; what
-            // is asserted here is closed-core, and the deadline below
-            // governs it exactly as it governs a pure obligation.
-            Ok(GoalLowering::Sliver(core)) => {
-                for assertion in core {
-                    solver.assert(assertion);
-                }
-            }
+        use crate::rule_solver::ordeal_backend::{render_ordeal_model, solver_for_goal_ne};
+        use ordeal::CheckResult;
+
+        let solver = match solver_for_goal_ne(lhs, rhs) {
+            Ok(solver) => solver,
             // `decide_bv_equivalence` gates this case and defers instead, so
             // reaching it means the obligation came from somewhere else.
             // `Unknown` is the conservative answer either way.
             Err(_) => return RuleVerdict::Unknown,
-        }
+        };
         match solver.check_with_deadline(self.timeout_ms) {
             CheckResult::Unsat(cert) => match cert.recheck() {
                 Ok(()) => RuleVerdict::Proven,
@@ -1815,6 +1804,66 @@ mod tests {
     /// disjunction this seam builds would over-approximate and silently
     /// reject correct transforms, so the obligation is declined instead —
     /// the same scope discipline slice 1 applied to memory.
+    /// #433 / ordeal#247: a query variable must never be identified with the
+    /// sliver's own fresh variable for a read.
+    ///
+    /// ordeal < 0.32.1 named the fresh variable for a concrete read
+    /// `$sel:<array>:<index>` without checking the query's own names, so a
+    /// query variable spelled that way was silently unified with the read and
+    /// `select(memory, 5) != $sel:memory:5` — satisfiable, the two are
+    /// independent — came back as a CERTIFIED `Unsat`. This drives the exact
+    /// counterexample through the production solver.
+    ///
+    /// loom's own variable names cannot start with `$` (every Z3 name it
+    /// creates begins with a literal letter), so production was not exposed;
+    /// this pins the fix so a future pin or name scheme cannot reopen it.
+    #[test]
+    fn a_query_variable_cannot_masquerade_as_a_sliver_read() {
+        use crate::rule_solver::RuleArray;
+        let read = RuleTerm::Select {
+            array: Box::new(RuleArray::Var {
+                name: "memory".into(),
+            }),
+            index: Box::new(k(5, 32)),
+        };
+        let impostor = v("$sel:memory:5", 8);
+        let verdict = BoundedOrdealSolver::from_env().prove_rule_equiv(&read, &impostor);
+        assert!(
+            matches!(verdict, RuleVerdict::Disproven(_)),
+            "a read and an independent variable are NOT equal; got {verdict:?}"
+        );
+    }
+
+    /// #433: a memory or call obligation must be decided by a solver built
+    /// with `Solver::from_sliver`. From ordeal 0.33.0 only such a solver runs
+    /// the trusted, Lean-proven `check_sliver_lowering` before it returns a
+    /// verdict, which proves that the closed core it decides is exactly the
+    /// read-over-write and congruence elimination of the query loom asked.
+    /// Lowering by hand and asserting the core skips that check.
+    /// `is_sliver()` reports which entry point built the solver. A pure
+    /// obligation has nothing to eliminate and must stay on the plain path.
+    #[test]
+    fn memory_obligations_are_decided_on_the_proven_sliver_path() {
+        use crate::rule_solver::RuleArray;
+        use crate::rule_solver::ordeal_backend::solver_for_goal_ne;
+        let read = |at: u128| RuleTerm::Select {
+            array: Box::new(RuleArray::Var {
+                name: "memory".into(),
+            }),
+            index: Box::new(k(at, 32)),
+        };
+        let memory = solver_for_goal_ne(&read(5), &read(6)).expect("in the sliver");
+        assert!(
+            memory.is_sliver(),
+            "a memory obligation was decided on a solver that skips check_sliver_lowering"
+        );
+        let pure = solver_for_goal_ne(&v("x", 32), &v("y", 32)).expect("closed core");
+        assert!(
+            !pure.is_sliver(),
+            "a pure obligation has no sliver to check"
+        );
+    }
+
     #[test]
     fn a_division_under_a_conditional_is_refused_not_approximated() {
         let cond = RuleBool::Eq(Box::new(v("c", 32)), Box::new(k(0, 32)));

safety/requirements/verification.yaml

@@ -927,7 +927,7 @@ artifacts:
         - run: cargo test --release --lib -p loom-core --features verification -- slice3_a_pure_call_is_not_a_constant
         - run: cargo test --release --lib -p loom-core --features verification -- slice3_one_name_two_signatures_is_refused
         - run: cargo test --release --lib -p loom-core --features verification -- out_of_fragment_obligations_are_refused
-        - run: "LOOM_VERIFY_BACKEND=both cargo test --release --lib -p loom-core --features verification 2>&1 | tee /dev/stderr | grep -qE '^test result: ok\\. 566 passed'"
+        - run: "LOOM_VERIFY_BACKEND=both cargo test --release --lib -p loom-core --features verification 2>&1 | tee /dev/stderr | grep -qE '^test result: ok\\. 568 passed'"
     status: verified
     release: v1.5.0
     tags: [v150, verification, solver-migration]