diff --git a/Cargo.lock b/Cargo.lock index 36bb17d..b079d13 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1827,18 +1827,18 @@ dependencies = [ [[package]] name = "ordeal" -version = "0.30.0" +version = "0.33.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "391c151b0e924055d6f862e88e6c095112e167063edc2adc69c079c23ed5b030" +checksum = "9d1fff0bf87ed543ee012bcd59a9e77432c2384ae2f0ac0d1a949145a2ef7813" dependencies = [ "ordeal-lrat", ] [[package]] name = "ordeal-lrat" -version = "0.30.0" +version = "0.33.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b81494e0e42a394e3bb9994fcaf5a0339b52e3f3602b55542e9fa2046ef2573" +checksum = "662546b0bb34ccf4014e9a69adc6614a26648b0f01acb44e010d27f55a91b18d" [[package]] name = "page_size" diff --git a/loom-core/Cargo.toml b/loom-core/Cargo.toml index 59ac95d..0541711 100644 --- a/loom-core/Cargo.toml +++ b/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] diff --git a/loom-core/src/rule_solver.rs b/loom-core/src/rule_solver.rs index 71b5562..8312b6b 100644 --- a/loom-core/src/rule_solver.rs +++ b/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), + /// 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 { + 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 { 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), } diff --git a/loom-core/src/verify_solver.rs b/loom-core/src/verify_solver.rs index c1dc3f5..0fbbdca 100644 --- a/loom-core/src/verify_solver.rs +++ b/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::` 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))); diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index d428de8..9f14ec3 100644 --- a/safety/requirements/verification.yaml +++ b/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]