From 6c109f28d5cf3f4383c2cd924970be093fae559f Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Tue, 15 Sep 2026 01:59:35 -0400 Subject: [PATCH 1/6] Add resident speculate: test an instantiation hypothesis on a retained query A `speculate` request checks a retained query as usual, observed for matching loops, then again with one hypothesis sent in the query's own scope through cvc5's `(speculate ...)`: instantiate a quantifier at given terms, give it one more trigger, or refuse its instantiations that fit a fingerprint. `(get-info :speculation)` is read in the same batch, and finish_query pops the hypothesis with the scope. The reply says whether the hypothesis closed the query (failed before, held after, failed again on a recheck, since queries near the resource limit flip between checks of their own), whether it introduced a matching loop, the instances it made (LLM_DIRECTED), and source to paste: an assert of the instance with its type guards dropped, or a #![trigger ...] annotation. Without a hypothesis it lists the quantifiers written in source that the query's scope asserts. Terms may be Verus expressions or SMT terms. air::speculate finds the quantifier by qid in the retained AIR; the lowering resolves source names among the scope's declarations and boxes into Poly (or unboxes) where a function or variable takes the other. The journal now keeps the bucket's setup batches, which the solver held below its scopes, so declarations there can be read. A term cvc5 cannot read is refused in the early flush, before any check-sat. Co-Authored-By: Claude Opus 5 (1M context) --- source/air/src/context.rs | 80 +- source/air/src/lib.rs | 1 + source/air/src/smt_verify.rs | 41 +- source/air/src/speculate.rs | 532 ++++++++ source/rust_verify/src/resident.rs | 1381 ++++++++++++++++++++- source/rust_verify/src/verifier.rs | 12 + source/rust_verify_test/tests/resident.rs | 238 +++- 7 files changed, 2264 insertions(+), 21 deletions(-) create mode 100644 source/air/src/speculate.rs diff --git a/source/air/src/context.rs b/source/air/src/context.rs index 1c0161056c..185092d26c 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -556,6 +556,13 @@ pub struct Context { /// An equality to assert in the next query's scope just before its first /// `check-sat` (cvc5 only). pub(crate) inject_equality: Option<(sise::TreeNode, sise::TreeNode)>, + /// A hypothesis to send in the next query's scope just before its first + /// `check-sat` (cvc5 only, see `speculate`). + pub(crate) speculation: Option, + /// cvc5's reply to the last hypothesis sent, until the caller takes it. + pub(crate) last_speculation: Option, + /// Whether this solver serves `(speculate ...)`, once asked. + speculation_supported: Option, } impl Context { @@ -647,6 +654,9 @@ impl Context { egraph_focus: None, last_egraph: None, inject_equality: None, + speculation: None, + last_speculation: None, + speculation_supported: None, solver, }; context.axiom_infos.push_scope(false); @@ -962,6 +972,74 @@ impl Context { Ok(()) } + /// Whether this solver serves `(speculate ...)`, which it does if it + /// answers `(get-info :speculation)`; asked once (cvc5 only). A solver + /// without the command would end at it, so ask before `set_speculation`. + pub fn supports_speculation(&mut self) -> bool { + if !matches!(self.solver, SmtSolver::Cvc5) { + return false; + } + if let Some(supported) = self.speculation_supported { + return supported; + } + self.ensure_started(); + self.smt_log.log_get_info("speculation"); + let smt_data = self.smt_log.take_pipe_data(); + let lines = self.get_smt_process().send_commands(smt_data); + let supported = lines.iter().any(|line| line.starts_with("(:speculation ")); + self.speculation_supported = Some(supported); + supported + } + + /// Send `request` in the next query's scope, after its assertions and + /// just before its first `check-sat`, and read `(get-info :speculation)` + /// right after that check (cvc5 with `supports_speculation` only). + /// `finish_query` pops the hypothesis with the scope. Take the reply with + /// `take_speculation`; when cvc5 refused the command, the reply carries + /// its error and the check answers `Canceled` without a `check-sat`. + /// `None` also drops a request that a check which never reached the + /// solver left behind. + pub fn set_speculation(&mut self, request: Option) { + assert!(request.is_none() || matches!(self.solver, SmtSolver::Cvc5)); + self.speculation = request; + } + + /// The reply to the hypothesis of the most recent query, if one was sent; + /// each call returns it once. + pub fn take_speculation(&mut self) -> Option { + self.last_speculation.take().map(|mut reply| { + reply.variable_versions = self.variable_versions.clone(); + reply + }) + } + + /// The universal quantifier named `qid` that `decls` or `query` asserts, + /// as the solver is sent it, the query's own first. + pub fn find_quantifier<'a>( + &self, + decls: impl Iterator, + query: &Query, + qid: &str, + ) -> Option { + let printer = + crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone()); + crate::speculate::find_quantifier(decls, query, qid, &printer) + } + + /// The universal quantifiers `decls` and `query` assert that `keep` + /// accepts, by qid and whether the query asserts them, as the solver is + /// sent them: the query's own first, each qid once. + pub fn quantifiers<'a>( + &self, + decls: impl Iterator, + query: &Query, + keep: impl Fn(&str, bool) -> bool, + ) -> Vec { + let printer = + crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone()); + crate::speculate::quantifiers(decls, query, &printer, keep) + } + pub fn set_profile_with_logfile_name(&mut self, file_name: String) { assert!(matches!(self.state, ContextState::NotStarted)); self.profile_logfile_name = Some(file_name); @@ -1220,7 +1298,7 @@ impl Context { }; let (query, snapshots, local_vars, variable_versions) = crate::var_to_const::lower_query( &query, - self.provenance || self.egraph_request.is_some(), + self.provenance || self.egraph_request.is_some() || self.speculation.is_some(), ); self.variable_versions = variable_versions; self.air_middle_log.log_query(&query); diff --git a/source/air/src/lib.rs b/source/air/src/lib.rs index 4c23e10dc0..2ef814c998 100644 --- a/source/air/src/lib.rs +++ b/source/air/src/lib.rs @@ -13,6 +13,7 @@ pub mod profiler; pub mod remove_asserts; pub mod scope_map; pub mod smt_process; +pub mod speculate; #[macro_use] pub mod printer; diff --git a/source/air/src/smt_verify.rs b/source/air/src/smt_verify.rs index 715882fcea..2f829dbf76 100644 --- a/source/air/src/smt_verify.rs +++ b/source/air/src/smt_verify.rs @@ -239,6 +239,16 @@ pub(crate) fn smt_check_assertion<'ctx>( None }; + // A hypothesis goes in the query's scope before the flush below, so that a + // term cvc5 cannot read is refused there, before any check-sat. Only the + // query's first check sends it: later rounds share its scope. + let speculation = context.speculation.take(); + if let Some(request) = &speculation { + context.last_speculation = None; + context.smt_log.log_node(&request.to_node()); + } + let mut speculation_refused = None; + context.smt_log.log_get_info("version"); let smt_init_start_time = std::time::Instant::now(); let smt_data = context.smt_log.take_pipe_data(); @@ -262,6 +272,8 @@ pub(crate) fn smt_check_assertion<'ctx>( ); } } + } else if speculation.is_some() && line.starts_with("(error") { + speculation_refused = Some(line); } else if context.ignore_unexpected_smt { diagnostics.report(&context.message_interface.bare( crate::messages::MessageLevel::Warning, @@ -272,6 +284,14 @@ pub(crate) fn smt_check_assertion<'ctx>( } } + // cvc5 could not read the hypothesis, so there is nothing to check. + if let Some(error) = speculation_refused { + context.last_speculation = + Some(crate::speculate::SpeculationReply { error: Some(error), ..Default::default() }); + context.state = ContextState::Canceled; + return ValidityResult::Canceled; + } + if let Some(disabled_expr) = disabled_expr { context.smt_log.log_assert(&None, &None, &disabled_expr); } @@ -314,6 +334,11 @@ pub(crate) fn smt_check_assertion<'ctx>( // in the same batch, right after the answer it describes context.smt_log.log_get_info("inst-pressure"); } + if speculation.is_some() { + // in the same batch, right after the answer it describes and before + // the scope holding the hypothesis is popped + context.smt_log.log_get_info("speculation"); + } if context.provenance { // in the same batch: the tag lists arrive after the result and the // instantiation dump, before the sentinel @@ -363,6 +388,7 @@ pub(crate) fn smt_check_assertion<'ctx>( let mut nl_frontier = None; let mut egraph_lines: Vec = Vec::new(); let mut inst_pressure = None; + let mut speculation_reply = None; for line in smt_output { // The e-graph reply, or the solver's refusal of the request, is the // batch's last: every line from its first on belongs to it. @@ -397,6 +423,8 @@ pub(crate) fn smt_check_assertion<'ctx>( // a cvc5 without the key; say so rather than fail the query inst_pressure = Some(crate::context::InstPressure { unparsed: Some(line), ..Default::default() }); + } else if speculation.is_some() && line.starts_with("(:speculation (") { + speculation_reply = Some(crate::speculate::parse_speculation(&line)); } else if line == "unsat" { assert!(unsat == None); unsat = Some(SmtOutput::Unsat); @@ -436,6 +464,13 @@ pub(crate) fn smt_check_assertion<'ctx>( context.last_nl_frontier = nl_frontier; context.last_difficulty = difficulty; context.last_inst_pressure = inst_pressure; + if speculation.is_some() { + context.last_speculation = + Some(speculation_reply.unwrap_or_else(|| crate::speculate::SpeculationReply { + unparsed: Some("no (:speculation ...) reply".to_string()), + ..Default::default() + })); + } if egraph_asked { context.last_egraph = Some(parse_egraph_lines(&egraph_lines)); } @@ -653,7 +688,7 @@ pub(crate) fn parse_nl_frontier(line: &str) -> crate::context::NlFrontier { /// A reply subterm as text: lists re-joined, quoted symbols unquoted (see /// `bar_symbols_as_strings`), unless whitespace or parentheses in one mean /// only its bars keep it one symbol. -fn sexp_text(node: &sise::TreeNode) -> String { +pub(crate) fn sexp_text(node: &sise::TreeNode) -> String { match node { sise::TreeNode::Atom(a) => match a.strip_prefix('"').and_then(|t| t.strip_suffix('"')) { Some(t) if t.contains(|c: char| c.is_whitespace() || c == '(' || c == ')') => { @@ -763,7 +798,7 @@ fn parse_nl_atom(node: &sise::TreeNode) -> Option { /// A count from a solver reply. cvc5 prints arbitrary-precision integers, so /// one too large for u64 saturates rather than fails. -fn difficulty_count(v: &str) -> Option { +pub(crate) fn difficulty_count(v: &str) -> Option { (!v.is_empty() && v.bytes().all(|b| b.is_ascii_digit())) .then(|| v.parse::().unwrap_or(u64::MAX)) } @@ -771,7 +806,7 @@ fn difficulty_count(v: &str) -> Option { /// cvc5 quotes a symbol that needs it as `|...|`, which sise cannot read, so /// spell each one as a sise string. A symbol that cannot be a sise string /// (it holds `"` or `\`) is left alone, and the reply stays unparsed. -fn bar_symbols_as_strings(line: &str) -> String { +pub(crate) fn bar_symbols_as_strings(line: &str) -> String { let mut out = String::with_capacity(line.len()); let mut rest = line; while let Some(start) = rest.find('|') { diff --git a/source/air/src/speculate.rs b/source/air/src/speculate.rs new file mode 100644 index 0000000000..83e3645a50 --- /dev/null +++ b/source/air/src/speculate.rs @@ -0,0 +1,532 @@ +//! Speculative probes (cvc5 only): a hypothesis about quantifier +//! instantiation, held in one query's scope, and what cvc5 reported it did. +//! +//! A probe is an ordinary check of a query with one `(speculate ...)` command +//! sent in the query's own scope, just before its first `check-sat`, and +//! `(get-info :speculation)` read right after it. `finish_query` pops the +//! scope, and cvc5 keeps every hypothesis and everything it installed in +//! that scope's user context, so nothing of the probe outlives the check. +//! +//! The terms of a hypothesis are sent as strings, which cvc5 parses one at a +//! time: a term that names a symbol the scope does not declare fails the +//! command with an error, before any `check-sat`, instead of ending the +//! solver as a bad term elsewhere in the stream would. + +use crate::ast::{BindX, Decl, DeclX, Expr, ExprX, Quant, Query}; +use crate::context::VariableVersions; +use crate::printer::Printer; +use sise::TreeNode as Node; +use std::collections::HashMap; + +/// What a probe adds to its query's scope. +#[derive(Clone, Debug)] +pub enum Hypothesis { + /// Nothing: the check is observed for matching loops. + Observe, + /// Instantiate the quantifiers named `qid` once, with a term, in the + /// solver's spelling, for each variable, by its name on the wire. + Instantiate { qid: String, subst: Vec<(String, String)> }, + /// Match the quantifiers named `qid` with one more trigger, whose terms + /// are over the variables `vars` (name and sort, as on the wire). + Trigger { qid: String, vars: Vec<(String, Node)>, pattern: Vec }, + /// Refuse the instantiations of the quantifiers named `qid` whose terms, + /// or trigger instance, match `fingerprint` (holes `_`, `_`, `#`). + Block { qid: String, fingerprint: String }, +} + +#[derive(Clone, Debug)] +pub struct SpeculationRequest { + pub hypothesis: Hypothesis, + /// The depth rises that make a matching loop; cvc5's default when `None`. + pub loop_threshold: Option, +} + +/// A string literal cvc5 reads back as `text`: quoted, `"` doubled. Line +/// breaks become spaces, so the command stays on one line. +fn string_atom(text: &str) -> Node { + let flat: String = text.chars().map(|c| if c.is_whitespace() { ' ' } else { c }).collect(); + Node::Atom(format!("\"{}\"", flat.replace('"', "\"\""))) +} + +fn atom(text: &str) -> Node { + Node::Atom(text.to_string()) +} + +impl SpeculationRequest { + /// The `(speculate ...)` command for this request. + pub(crate) fn to_node(&self) -> Node { + let mut items = vec![atom("speculate")]; + match &self.hypothesis { + Hypothesis::Observe => items.push(atom(":observe")), + Hypothesis::Instantiate { qid, subst } => { + items.extend([atom(":instantiate"), atom(qid)]); + items.push(Node::List( + subst + .iter() + .map(|(name, term)| Node::List(vec![atom(name), string_atom(term)])) + .collect(), + )); + } + Hypothesis::Trigger { qid, vars, pattern } => { + items.extend([atom(":trigger"), atom(qid)]); + items.push(Node::List( + vars.iter() + .map(|(name, sort)| Node::List(vec![atom(name), sort.clone()])) + .collect(), + )); + items.push(Node::List(pattern.iter().map(|p| string_atom(p)).collect())); + } + Hypothesis::Block { qid, fingerprint } => { + items.extend([atom(":block"), atom(qid), string_atom(fingerprint)]); + } + } + if let Some(threshold) = self.loop_threshold { + items.extend([atom(":loop-threshold"), atom(&threshold.to_string())]); + } + Node::List(items) + } +} + +/// What cvc5 reported a hypothesis did, from `(get-info :speculation)`. +#[derive(Clone, Debug, Default)] +pub struct HypothesisReport { + /// `observe`, `instantiate`, `trigger` or `block` + pub kind: String, + pub qid: String, + /// `applied`, `rejected` (the instantiation funnel refused the directed + /// instance), `mismatch` (the variables do not fit), `unusable` (the + /// pattern cannot be a trigger), `no-quantifier` or `pending` (no + /// instantiation round ran) + pub status: String, + pub reason: Option, + /// how many asserted quantifiers have the qid + pub quantifiers: u64, + /// instantiations it made, and directed ones the funnel refused + pub added: u64, + pub rejected: u64, + /// instantiations a block refused + pub blocked: u64, + /// term vectors it made, or refused for a block, the first few + pub instances: Vec>, + /// the instances' bodies (instantiate) + pub bodies: Vec, + /// the pattern over the quantifier's variables (trigger) + pub pattern: Vec, + /// the quantifier with the pattern as its only one (trigger) + pub materialized: Vec, + pub fingerprint: Option, +} + +/// A quantifier whose instantiating terms kept getting deeper, round after +/// round, in the probed check. +#[derive(Clone, Debug, Default)] +pub struct LoopReport { + pub qid: String, + pub instantiations: u64, + /// of them directed by the hypothesis + pub directed: u64, + pub rounds: u64, + /// rounds in which its deepest instantiating term got deeper than before + pub rises: u64, + pub first_depth: u64, + pub max_depth: u64, + pub first_round: u64, + pub last_round: u64, +} + +/// cvc5's reply to `(get-info :speculation)` after a probe's `check-sat`, or +/// its refusal of the `(speculate ...)` command. +#[derive(Clone, Debug, Default)] +pub struct SpeculationReply { + pub active: bool, + /// instantiation rounds the check ran + pub rounds: u64, + pub loop_threshold: u64, + pub hypotheses: Vec, + pub loops: Vec, + /// The solver's refusal of the command, `(error "...")`, when it could + /// not read a term or the fingerprint. The query was not checked. + pub error: Option, + /// The reply, when it did not parse. + pub unparsed: Option, + /// SSA symbol -> original AIR variable and assignment version, recorded by lowering. + pub variable_versions: VariableVersions, +} + +/// The contents of a string literal cvc5 printed: unquoted, `""` read as `"`. +fn unquote(text: &str) -> String { + match text.strip_prefix('"').and_then(|t| t.strip_suffix('"')) { + Some(inner) => inner.replace("\"\"", "\""), + None => text.to_string(), + } +} + +/// A string or symbol value of a reply, as its text: `sexp_text` would put +/// one holding a space back between bars. +fn text(node: &Node) -> String { + match node { + Node::Atom(atom) => unquote(atom), + Node::List(_) => crate::smt_verify::sexp_text(node), + } +} + +fn terms(node: &Node) -> Option> { + match node { + Node::List(items) => Some(items.iter().map(crate::smt_verify::sexp_text).collect()), + Node::Atom(_) => None, + } +} + +fn vectors(node: &Node) -> Option>> { + match node { + Node::List(items) => items.iter().map(terms).collect(), + Node::Atom(_) => None, + } +} + +fn count(node: &Node) -> Option { + match node { + Node::Atom(a) => crate::smt_verify::difficulty_count(a), + Node::List(_) => None, + } +} + +fn parse_hypothesis(node: &Node) -> Option { + let Node::List(items) = node else { return None }; + let (Node::Atom(kind), fields) = items.split_first()? else { return None }; + let mut h = HypothesisReport { kind: kind.clone(), ..Default::default() }; + for pair in fields.chunks(2) { + let [Node::Atom(key), value] = pair else { return None }; + match key.as_str() { + ":qid" => h.qid = text(value), + ":status" => h.status = text(value), + ":reason" => h.reason = Some(text(value)), + ":fingerprint" => h.fingerprint = Some(text(value)), + ":quantifiers" => h.quantifiers = count(value)?, + ":added" => h.added = count(value)?, + ":rejected" => h.rejected = count(value)?, + ":blocked" => h.blocked = count(value)?, + ":instances" | ":examples" => h.instances = vectors(value)?, + ":bodies" => h.bodies = terms(value)?, + ":pattern" => h.pattern = terms(value)?, + ":materialized" => h.materialized = terms(value)?, + _ => {} + } + } + Some(h) +} + +fn parse_loop(node: &Node) -> Option { + let Node::List(items) = node else { return None }; + let (Node::Atom(head), fields) = items.split_first()? else { return None }; + if head != "loop" { + return None; + } + let mut l = LoopReport::default(); + for pair in fields.chunks(2) { + let [Node::Atom(key), value] = pair else { return None }; + match key.as_str() { + ":qid" => l.qid = text(value), + ":instantiations" => l.instantiations = count(value)?, + ":directed" => l.directed = count(value)?, + ":rounds" => l.rounds = count(value)?, + ":rises" => l.rises = count(value)?, + ":first-depth" => l.first_depth = count(value)?, + ":max-depth" => l.max_depth = count(value)?, + ":first-round" => l.first_round = count(value)?, + ":last-round" => l.last_round = count(value)?, + _ => {} + } + } + Some(l) +} + +/// Parse `(:speculation (:active B :rounds N :loop-threshold N :hypotheses +/// (H ...) :loops (L ...)))`. A reply that does not parse is kept whole in +/// `unparsed`. +pub(crate) fn parse_speculation(line: &str) -> SpeculationReply { + let mut out = SpeculationReply::default(); + let text = crate::smt_verify::bar_symbols_as_strings(line); + let mut parser = sise::Parser::new(&text); + let parsed = (|| { + let Ok(Node::List(items)) = sise::parse_tree(&mut parser) else { return None }; + let [Node::Atom(head), Node::List(fields)] = &items[..] else { return None }; + if head != ":speculation" { + return None; + } + for pair in fields.chunks(2) { + let [Node::Atom(key), value] = pair else { return None }; + match (key.as_str(), value) { + (":active", Node::Atom(v)) => out.active = v == "true", + (":rounds", v) => out.rounds = count(v)?, + (":loop-threshold", v) => out.loop_threshold = count(v)?, + (":hypotheses", Node::List(hs)) => { + out.hypotheses = hs.iter().map(parse_hypothesis).collect::>()? + } + (":loops", Node::List(ls)) => { + out.loops = ls.iter().map(parse_loop).collect::>()? + } + _ => {} + } + } + Some(()) + })(); + if parsed.is_none() { + out = SpeculationReply { unparsed: Some(line.to_string()), ..Default::default() }; + } + out +} + +/// A quantifier a query's scope asserts, as the solver is sent it. +#[derive(Clone, Debug)] +pub struct QuantifierSmt { + pub qid: String, + /// Each variable's name and sort. + pub binders: Vec<(String, Node)>, + /// Each trigger, as its terms. + pub triggers: Vec>, + /// The body, without the trigger and qid attributes. + pub body: Node, + /// Whether the query itself, rather than a declaration before it, + /// asserts it. + pub in_query: bool, +} + +impl QuantifierSmt { + /// The body with each variable in `subst` replaced by its term. + pub fn instance(&self, subst: &HashMap) -> Node { + substitute(&self.body, subst) + } + + /// Each trigger with each variable in `subst` replaced by its term. + pub fn trigger_instances(&self, subst: &HashMap) -> Vec> { + self.triggers + .iter() + .map(|trigger| trigger.iter().map(|term| substitute(term, subst)).collect()) + .collect() + } +} + +/// The names a binder list `((x T) ...)` binds. +fn bound_names(binders: &Node) -> Vec { + match binders { + Node::List(items) => items + .iter() + .filter_map(|b| match b { + Node::List(pair) => match pair.first() { + Some(Node::Atom(name)) => Some(name.clone()), + _ => None, + }, + _ => None, + }) + .collect(), + Node::Atom(_) => Vec::new(), + } +} + +/// `node` with each free occurrence of a name in `subst` replaced by its +/// term. A binder (`forall`, `exists`, `lambda`, `choose`, `let`) shadows the +/// names it binds within its scope. +pub fn substitute(node: &Node, subst: &HashMap) -> Node { + match node { + Node::Atom(a) => subst.get(a).cloned().unwrap_or_else(|| node.clone()), + Node::List(items) => { + if let [Node::Atom(head), binders, rest @ ..] = &items[..] { + let quantifier = matches!(head.as_str(), "forall" | "exists" | "lambda" | "choose"); + if quantifier || head == "let" { + let shadowed = bound_names(binders); + let inner: HashMap = subst + .iter() + .filter(|(name, _)| !shadowed.contains(name)) + .map(|(name, term)| (name.clone(), term.clone())) + .collect(); + // a let's bound terms see the outer names + let binders = match (head.as_str(), binders) { + ("let", Node::List(pairs)) => Node::List( + pairs + .iter() + .map(|pair| match pair { + Node::List(p) if p.len() == 2 => { + Node::List(vec![p[0].clone(), substitute(&p[1], subst)]) + } + other => other.clone(), + }) + .collect(), + ), + _ => binders.clone(), + }; + let mut out = vec![items[0].clone(), binders]; + out.extend(rest.iter().map(|n| substitute(n, &inner))); + return Node::List(out); + } + } + Node::List(items.iter().map(|n| substitute(n, subst)).collect()) + } + } +} + +/// Every universal quantifier under `expr` with a qid, in the order met. +fn quantifiers_in(expr: &Expr, found: &mut Vec) { + let expr = crate::smt_verify::elim_zero_args_expr(expr); + crate::visitor::map_expr_visitor(&expr, &mut |e| { + if let ExprX::Bind(bind, _) = &**e { + if let BindX::Quant(Quant::Forall, _, _, Some(_)) = &**bind { + found.push(e.clone()); + } + } + e.clone() + }); +} + +/// The universal quantifiers with a qid that `decls` and `query` assert, +/// the query's own first, then the declarations' from the last: each with +/// whether the query asserts it. +fn all_quantifiers<'a>(decls: impl Iterator, query: &Query) -> Vec<(Expr, bool)> { + let mut declared = Vec::new(); + for decl in decls { + if let DeclX::Axiom(axiom) = &**decl { + quantifiers_in(&axiom.expr, &mut declared); + } + } + let mut own = Vec::new(); + for decl in query.local.iter() { + if let DeclX::Axiom(axiom) = &**decl { + quantifiers_in(&axiom.expr, &mut own); + } + } + crate::visitor::map_stmt_expr_visitor(&query.assertion, &mut |e| { + quantifiers_in(e, &mut own); + e.clone() + }); + let own = own.into_iter().rev().map(|e| (e, true)); + own.chain(declared.into_iter().rev().map(|e| (e, false))).collect() +} + +fn qid_of(expr: &Expr) -> Option<&str> { + match &**expr { + ExprX::Bind(bind, _) => match &**bind { + BindX::Quant(_, _, _, Some(qid)) => Some(qid.as_str()), + _ => None, + }, + _ => None, + } +} + +fn describe(expr: &Expr, in_query: bool, printer: &Printer) -> Option { + let ExprX::Bind(bind, body) = &**expr else { return None }; + let BindX::Quant(Quant::Forall, binders, triggers, Some(qid)) = &**bind else { return None }; + Some(QuantifierSmt { + qid: qid.to_string(), + binders: binders.iter().map(|b| (b.name.to_string(), printer.typ_to_node(&b.a))).collect(), + triggers: triggers + .iter() + .map(|t| t.iter().map(|term| printer.expr_to_node(term)).collect()) + .collect(), + body: printer.expr_to_node(body), + in_query, + }) +} + +/// The quantifier named `qid` that `decls` or `query` asserts, preferring +/// the query's own. `None` if neither does. +pub(crate) fn find_quantifier<'a>( + decls: impl Iterator, + query: &Query, + qid: &str, + printer: &Printer, +) -> Option { + all_quantifiers(decls, query) + .iter() + .find(|(e, _)| qid_of(e) == Some(qid)) + .and_then(|(e, in_query)| describe(e, *in_query, printer)) +} + +/// The universal quantifiers `decls` and `query` assert that `keep` accepts +/// by qid and whether the query asserts them: the query's own first, each +/// qid once. +pub(crate) fn quantifiers<'a>( + decls: impl Iterator, + query: &Query, + printer: &Printer, + keep: impl Fn(&str, bool) -> bool, +) -> Vec { + let mut seen = std::collections::HashSet::new(); + all_quantifiers(decls, query) + .iter() + .filter(|(e, in_query)| { + qid_of(e).is_some_and(|qid| keep(qid, *in_query) && seen.insert(qid.to_string())) + }) + .filter_map(|(e, in_query)| describe(e, *in_query, printer)) + .collect() +} + +#[cfg(test)] +mod tests { + use super::*; + + fn tree(text: &str) -> Node { + sise::parse_tree(&mut sise::Parser::new(text)).unwrap() + } + + #[test] + fn requests_send_terms_as_strings() { + let request = SpeculationRequest { + hypothesis: Hypothesis::Instantiate { + qid: "user_f_1".into(), + subst: vec![("x$".into(), "(f \"a\"\nb)".into())], + }, + loop_threshold: Some(3), + }; + let printer = crate::printer::node_to_string; + assert_eq!( + printer(&request.to_node()), + r#"(speculate :instantiate user_f_1 ((x$ "(f ""a"" b)")) :loop-threshold 3)"# + ); + let trigger = SpeculationRequest { + hypothesis: Hypothesis::Trigger { + qid: "q".into(), + vars: vec![("i".into(), tree("Int"))], + pattern: vec!["(f i)".into()], + }, + loop_threshold: None, + }; + assert_eq!(printer(&trigger.to_node()), r#"(speculate :trigger q ((i Int)) ("(f i)"))"#); + } + + #[test] + fn replies_parse_hypotheses_and_loops() { + let reply = parse_speculation( + r#"(:speculation (:active true :rounds 4 :loop-threshold 5 :hypotheses ((observe) (instantiate :qid ax_f :status mismatch :reason "no term for ""i""" :quantifiers 1 :added 0 :rejected 0 :instances ((a (g b))) :bodies ((not (<= (f a) 0))))) :loops ((loop :qid |a b| :instantiations 9 :directed 1 :rounds 6 :rises 5 :first-depth 1 :max-depth 6 :first-round 1 :last-round 6))))"#, + ); + assert!(reply.unparsed.is_none(), "{:?}", reply); + assert!(reply.active); + assert_eq!((reply.rounds, reply.loop_threshold), (4, 5)); + assert_eq!(reply.hypotheses.len(), 2); + assert_eq!(reply.hypotheses[0].kind, "observe"); + let h = &reply.hypotheses[1]; + assert_eq!( + (h.kind.as_str(), h.qid.as_str(), h.status.as_str()), + ("instantiate", "ax_f", "mismatch") + ); + assert_eq!(h.reason.as_deref(), Some("no term for \"i\"")); + assert_eq!(h.instances, vec![vec!["a".to_string(), "(g b)".to_string()]]); + assert_eq!(h.bodies, vec!["(not (<= (f a) 0))".to_string()]); + assert_eq!(reply.loops.len(), 1); + assert_eq!((reply.loops[0].qid.as_str(), reply.loops[0].rises), ("a b", 5)); + let bad = parse_speculation("(:speculation (:rounds x))"); + assert!(bad.unparsed.is_some()); + } + + #[test] + fn substitution_respects_binders() { + let subst = HashMap::from([("x".to_string(), tree("(g a)"))]); + let substituted = substitute( + &tree("(and (f x) (forall ((x Int)) (f x)) (let ((y x) (x 1)) (h x y)))"), + &subst, + ); + assert_eq!( + substituted, + tree("(and (f (g a)) (forall ((x Int)) (f x)) (let ((y (g a)) (x 1)) (h x y)))") + ); + } +} diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index 5e4aa0272c..ee07238fdc 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -33,10 +33,20 @@ //! one the solver itself reported for the same query, never text from the //! caller, and it is popped with the query's scope. Neither verdict is a //! `checked` one, and neither check saves a certificate. +//! +//! A `speculate` request checks a retained query as usual, observed for +//! matching loops, then again with one hypothesis about quantifier +//! instantiation sent in the query's own scope: instantiate a quantifier at +//! given terms, give it one more trigger, or refuse its instantiations that +//! match a fingerprint (see `air::speculate`). cvc5 holds the hypothesis in +//! that scope's user context, which the check pops. The reply says whether +//! the hypothesis closed the query (it failed without it, and again right +//! after), whether it introduced a matching loop, and what source to paste. +//! No probe verdict is a `checked` one, and no probe saves a certificate. use crate::buckets::BucketId; use crate::commands::{QueryOp, Style}; -use air::ast::{CommandX, Commands, Query}; +use air::ast::{CommandX, Commands, Decl, DeclX, Query}; use air::context::{ Context, EgraphReply, EgraphRequest, QueryContext, SmtSolver, ValidityResult, VariableVersions, }; @@ -44,10 +54,12 @@ use air::inst_graph::{GraphFilter, GraphOp, GraphReply, GraphSummary, Site}; use air::instantiations::ImportInstantiations; use air::messages::{ArcDynMessage, Diagnostics, MessageLevel}; use air::profiler::InstantiationGraph; +use air::speculate::{Hypothesis, QuantifierSmt, SpeculationReply, SpeculationRequest}; use serde::{Deserialize, Serialize}; +use sise::TreeNode; use std::borrow::Cow; use std::cell::RefCell; -use std::collections::{BTreeSet, HashMap, HashSet}; +use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::io::{self, BufRead, Read, Write}; use std::sync::Mutex; use std::sync::atomic::{AtomicUsize, Ordering}; @@ -133,6 +145,11 @@ pub(crate) struct QueryJournal { applied: usize, /// Whether a query has been recorded since the open scope began. recorded_in_scope: bool, + /// The declarations the solver held before the journal's first scope + /// (the bucket's fuel, traits, datatypes and function declarations, or a + /// spun-off query's whole context). Kept only to be read: they sit below + /// every scope, so they are never replayed. + base: Vec, } /// The requests this worker serves, as `ready` reports them. A client reads @@ -141,7 +158,8 @@ pub(crate) struct QueryJournal { /// as it does a malformed one. Every `Request` variant belongs here, in the /// protocol's snake case, which `resident_ready_lists_the_requests_it_serves` /// checks by sending each one. -const COMMANDS: &[&str] = &["list", "check", "bisect", "egraph", "close", "inst_graph"]; +const COMMANDS: &[&str] = + &["list", "check", "bisect", "egraph", "close", "inst_graph", "speculate"]; #[derive(Deserialize)] #[serde(tag = "command", rename_all = "snake_case", deny_unknown_fields)] @@ -186,6 +204,22 @@ enum Request { #[serde(default)] inject: Option, }, + /// Check the query as usual, then again with one hypothesis about + /// quantifier instantiation in its scope (see `air::speculate`). + Speculate { + session: String, + bucket: BucketIndex, + query: QueryId, + /// Without one, the query is checked once and the quantifiers + /// written in source that its scope asserts are listed. + #[serde(default)] + hypothesis: Option, + /// The rounds in which a quantifier's instantiating terms get + /// deeper that make a matching loop, 1 to `MAX_LOOP_THRESHOLD`; + /// cvc5's default (5) when absent. + #[serde(default)] + loop_threshold: Option, + }, Close { session: String, }, @@ -597,6 +631,13 @@ enum Response<'a> { #[serde(flatten)] outcome: Box, }, + Speculated { + session: &'a str, + bucket: BucketIndex, + query: QueryId, + #[serde(flatten)] + outcome: Box, + }, Error { message: &'a str, }, @@ -1158,15 +1199,24 @@ impl<'a> QueryNames<'a> { } /// `assert(lhs == rhs);` to add to the source, when that assert says what - /// the equality says: it is entailed, both sides render as source, and no - /// variable appears in it at two assignment versions. + /// the equality says: it is entailed, and both sides paste as source. fn verus_assert(&self, equality: &air::context::EgraphEquality) -> Option { - if equality.level != "entailed" { + if equality.level != "entailed" || !self.pasteable(&[&equality.lhs, &equality.rhs]) { return None; } - let terms = [equality.lhs.as_str(), equality.rhs.as_str()]; + Some(format!( + "assert({} == {});", + self.render_plain(&equality.lhs), + self.render_plain(&equality.rhs) + )) + } + + /// Whether `terms` paste as source together: each renders as source, and + /// no variable appears in them at two assignment versions, which would + /// read alike. + fn pasteable(&self, terms: &[&str]) -> bool { if !terms.iter().all(|term| vir::air_names::renders_as_source(&self.plain, term)) { - return None; + return false; } // SSA symbols are plain SMT-LIB symbols, never quoted, so splitting // on parentheses and spaces finds every one. @@ -1174,15 +1224,16 @@ impl<'a> QueryNames<'a> { for atom in terms.iter().flat_map(|term| term.split(['(', ')', ' ', '\n'])) { if let Some((base, version)) = self.versions.get(atom) { if *version_of.entry(base.as_str()).or_insert(*version) != *version { - return None; + return false; } } } - Some(format!( - "assert({} == {});", - vir::air_names::render_term(&self.plain, &equality.lhs), - vir::air_names::render_term(&self.plain, &equality.rhs) - )) + true + } + + /// A term as source to paste. + fn render_plain(&self, term: &str) -> String { + vir::air_names::render_term(&self.plain, term) } /// Where the quantifiers a proof relies on among `qids` are written. @@ -1435,9 +1486,1196 @@ fn serve_egraph( Ok(Ok(EgraphOutcome { before, summary, equalities, injection })) } +/// The most rounds of rising depth a probe may ask to make a matching loop. +const MAX_LOOP_THRESHOLD: u32 = 1000; +/// The most quantifiers a probe lists as candidates. +const MAX_CANDIDATES: usize = 40; + +const SPECULATION_CAVEAT: &str = "The hypothesis was sent in the query's own scope and popped right after the check, so the session's solver state is unchanged. A closed verdict is not a verification result: paste the snippet into the source and verify it normally."; + +/// A hypothesis as a `speculate` request names it. A term is an SMT term in +/// the solver's spelling, as the `smt_*` fields of other replies give them, +/// or with symbols named by their source names instead, which are looked up +/// among the query's declarations. A variable of the quantifier may be +/// named either way. +#[derive(Deserialize)] +#[serde(rename_all = "snake_case", deny_unknown_fields)] +enum HypothesisRequest { + /// Instantiate the quantifier once, with a term for each variable. + Instantiation { qid: String, subst: BTreeMap }, + /// Match the quantifier with one more trigger, whose terms are over its + /// variables. + TriggerPattern { qid: String, pattern: OneOrMore }, + /// Refuse the quantifier's instantiations whose terms, or trigger + /// instance, match the fingerprint: an SMT term whose holes `_`, `_` + /// and `#` match any term, as a matching loop's `step` is written. + BlockCycle { qid: String, fingerprint: String }, +} + +impl HypothesisRequest { + fn qid(&self) -> &str { + match self { + Self::Instantiation { qid, .. } + | Self::TriggerPattern { qid, .. } + | Self::BlockCycle { qid, .. } => qid, + } + } + + fn name(&self) -> &'static str { + match self { + Self::Instantiation { .. } => "instantiation", + Self::TriggerPattern { .. } => "trigger_pattern", + Self::BlockCycle { .. } => "block_cycle", + } + } +} + +/// One term, or a multi-trigger's several. +#[derive(Deserialize)] +#[serde(untagged)] +enum OneOrMore { + One(String), + More(Vec), +} + +impl OneOrMore { + fn terms(&self) -> Vec<&str> { + match self { + Self::One(term) => vec![term.as_str()], + Self::More(terms) => terms.iter().map(String::as_str).collect(), + } + } +} + +/// One check a probe made. Never a verification result. +#[derive(Serialize)] +struct SpeculationRun { + result: QueryResult, + elapsed_ms: u128, + /// cvc5's instantiation rounds + rounds: u64, + /// Quantifiers whose instantiating terms got deeper in at least the + /// loop threshold of rounds: matching loops. + loops: Vec, +} + +#[derive(Clone, Serialize)] +struct ResolvedSpeculationLoop { + qid: String, + /// the function it belongs to, and for a quantifier written in source, + /// where + #[serde(skip_serializing_if = "Option::is_none")] + function: Option, + #[serde(skip_serializing_if = "Option::is_none")] + span: Option, + instantiations: u64, + /// of them directed by the hypothesis + directed: u64, + rounds: u64, + /// rounds in which its deepest instantiating term got deeper + rises: u64, + first_depth: u64, + max_depth: u64, +} + +#[derive(Serialize)] +struct BinderDescription { + /// in source spelling, when the encoder recorded one + name: String, + /// as the solver spells it + smt_name: String, + sort: String, +} + +/// A quantifier the query's scope asserts. +#[derive(Serialize)] +struct QuantifierDescription { + qid: String, + #[serde(skip_serializing_if = "Option::is_none")] + function: Option, + #[serde(skip_serializing_if = "Option::is_none")] + span: Option, + /// The query asserts it itself (a `requires`, an `assert forall`) + /// rather than a declaration before it (a broadcast lemma, a spec + /// function's definition, the prelude). + in_query: bool, + binders: Vec, + /// each trigger's terms, in source spelling and as the solver spells them + triggers: Vec>, + smt_triggers: Vec>, +} + +#[derive(Serialize)] +struct DirectedInstance { + qid: String, + terms: Vec, + smt_terms: Vec, + /// how cvc5 tags every instantiation a hypothesis made + inference_id: &'static str, +} + +#[derive(Serialize)] +struct NewProvenance { + /// The instantiations the hypothesis made, the first 20. A directed + /// instance is the one requested; a trigger's are all it matched, not + /// only those the proof used. + closing_instantiations: Vec, + extra_inst_count: u64, +} + +/// What a `speculate` request found. +#[derive(Serialize)] +struct SpeculationOutcome { + /// `instantiation`, `trigger_pattern`, `block_cycle`, or `none` + hypothesis: &'static str, + #[serde(skip_serializing_if = "Option::is_none")] + qid: Option, + /// The quantifier the hypothesis names, as the query's scope asserts it. + #[serde(skip_serializing_if = "Option::is_none")] + quantifier: Option, + /// The query checked with nothing added. + #[serde(skip_serializing_if = "Option::is_none")] + before: Option, + /// The query checked with the hypothesis. + #[serde(skip_serializing_if = "Option::is_none")] + after: Option, + /// `applied`; `rejected` (the instantiation was made already); `mismatch` + /// (the terms do not fit the variables); `unusable` (the pattern cannot + /// be a trigger); `no_quantifier`; `could_not_lower` (a term the solver + /// cannot read); `pending` (no instantiation round ran) + #[serde(skip_serializing_if = "Option::is_none")] + status: Option, + #[serde(skip_serializing_if = "Option::is_none")] + reason: Option, + /// The query failed without the hypothesis, before and again right + /// after, and holds with it. + closed: bool, + /// The check without the hypothesis, run again after one that closed. + #[serde(skip_serializing_if = "Option::is_none")] + recheck: Option, + /// Whether the check with the hypothesis has a matching loop that the + /// check without it does not. + #[serde(skip_serializing_if = "Option::is_none")] + introduced_loop: Option, + #[serde(skip_serializing_if = "Vec::is_empty")] + new_loops: Vec, + #[serde(skip_serializing_if = "Option::is_none")] + new_provenance: Option, + /// Instantiations a block refused, and the first few refused vectors. + #[serde(skip_serializing_if = "Option::is_none")] + blocked: Option, + #[serde(skip_serializing_if = "Vec::is_empty")] + blocked_examples: Vec>, + /// Source to paste when the hypothesis closed the query: an `assert` + /// of the directed instance, or a trigger annotation. + #[serde(skip_serializing_if = "Option::is_none")] + verus_snippet: Option, + /// For a trigger, an `assert` of one instance it made, which needs no + /// change to the quantifier. + #[serde(skip_serializing_if = "Option::is_none")] + fallback_snippet: Option, + #[serde(skip_serializing_if = "Option::is_none")] + suggestion: Option, + notes: String, + /// Quantifiers written in source that the query's scope asserts, the + /// query's own first, when the request named none or one not there. + #[serde(skip_serializing_if = "Vec::is_empty")] + candidates: Vec, + caveat: &'static str, + elapsed_ms: u128, + restore_ms: u128, +} + +impl SpeculationOutcome { + fn new(hypothesis: &'static str, qid: Option) -> Self { + Self { + hypothesis, + qid, + quantifier: None, + before: None, + after: None, + status: None, + reason: None, + closed: false, + recheck: None, + introduced_loop: None, + new_loops: Vec::new(), + new_provenance: None, + blocked: None, + blocked_examples: Vec::new(), + verus_snippet: None, + fallback_snippet: None, + suggestion: None, + notes: String::new(), + candidates: Vec::new(), + caveat: SPECULATION_CAVEAT, + elapsed_ms: 0, + restore_ms: 0, + } + } +} + +/// A term on one line, as the solver spells it. +fn flat(node: &TreeNode) -> String { + match node { + TreeNode::Atom(atom) => atom.clone(), + TreeNode::List(items) => { + format!("({})", items.iter().map(flat).collect::>().join(" ")) + } + } +} + +/// `text` as one term, if it is exactly one. +fn parse_term(text: &str) -> Option { + let mut parser = sise::Parser::new(text); + let node = sise::parse_tree(&mut parser).ok()?; + parser.finish().ok()?; + Some(node) +} + +fn result_name(result: QueryResult) -> &'static str { + match result { + QueryResult::Valid => "valid", + QueryResult::Invalid => "invalid", + QueryResult::ResourceLimit => "resource_limit", + } +} + +/// Whether the solver reads an atom as itself: a numeral, a Boolean, a +/// string or a bit-vector literal. +fn is_literal(atom: &str) -> bool { + atom == "true" + || atom == "false" + || atom.starts_with('"') + || atom.starts_with('#') + || (!atom.is_empty() && atom.bytes().all(|b| b.is_ascii_digit() || b == b'.')) +} + +/// The sort the solver is sent for an AIR type. +fn sort_name(typ: &air::ast::Typ) -> String { + use air::ast::TypX; + match &**typ { + TypX::Bool => "Bool".to_owned(), + TypX::Int => "Int".to_owned(), + TypX::Real => "Real".to_owned(), + TypX::Fun => "Fun".to_owned(), + TypX::Named(name) => name.to_string(), + TypX::BitVec(bits) => format!("(_ BitVec {bits})"), + TypX::Float { exp_bits, sig_bits } => format!("(_ FloatingPoint {exp_bits} {sig_bits})"), + } +} + +/// The sort Verus boxes values into. +const POLY: &str = "Poly"; + +/// What the query's scope declares, with sorts: constants and variables, +/// and functions (datatype constructors and fields included) with their +/// argument and result sorts. +#[derive(Default)] +struct Declarations { + constants: HashMap, + functions: HashMap, String)>, +} + +impl Declarations { + fn of(decls: &[&Decl], query: &Query) -> Self { + let mut out = Self::default(); + // The prelude reaches each solver directly, never through the + // journal, so its boxes for integers and booleans are named here; + // a datatype's are the bucket's own declarations. + for (f, arg, result) in [ + (vir::def::BOX_INT, "Int", POLY), + (vir::def::BOX_BOOL, "Bool", POLY), + (vir::def::UNBOX_INT, POLY, "Int"), + (vir::def::UNBOX_BOOL, POLY, "Bool"), + ] { + out.functions.insert(f.to_owned(), (vec![arg.to_owned()], result.to_owned())); + } + for decl in decls.iter().copied().chain(query.local.iter()) { + match &**decl { + DeclX::Const(x, typ) | DeclX::Var(x, typ) => { + out.constants.insert(x.to_string(), sort_name(typ)); + } + DeclX::Fun(x, typs, typ) => { + let args = typs.iter().map(sort_name).collect(); + out.functions.insert(x.to_string(), (args, sort_name(typ))); + } + DeclX::Datatypes(datatypes) => { + for datatype in datatypes.iter() { + let sort = datatype.name.to_string(); + for variant in datatype.a.iter() { + let fields: Vec = + variant.a.iter().map(|field| sort_name(&field.a)).collect(); + out.functions.insert(variant.name.to_string(), (fields, sort.clone())); + for field in variant.a.iter() { + out.functions.insert( + field.name.to_string(), + (vec![sort.clone()], sort_name(&field.a)), + ); + } + } + } + } + DeclX::Sort(_) | DeclX::Axiom(_) => {} + } + } + out + } + + fn declares(&self, symbol: &str) -> bool { + self.constants.contains_key(symbol) || self.functions.contains_key(symbol) + } +} + +/// Turns the terms of a hypothesis into the solver's spelling: names +/// resolved, and values boxed into `Poly` or unboxed out of it where a +/// function, operator or variable takes the other, as Verus's encoding does. +struct Lowering { + /// A variable of the quantifier, by its own name and by its source + /// name: its own name. + binders: HashMap, + /// Each variable's sort, by its own name. + binder_sorts: HashMap, + declared: Declarations, + /// A declared symbol by its source name, whole and by its last path + /// segment. Only symbols an encoder minted for the name itself count, + /// not the helpers named after it (a function's `req%`, `ens%`). + by_source: HashMap>, +} + +impl Lowering { + fn new(quantifier: &QuantifierSmt, declared: Declarations, names: &[&SourceNames]) -> Self { + let mut binders: HashMap = + quantifier.binders.iter().map(|(smt, _)| (smt.clone(), smt.clone())).collect(); + let binder_sorts = + quantifier.binders.iter().map(|(smt, sort)| (smt.clone(), flat(sort))).collect(); + let mut by_source: HashMap> = HashMap::new(); + let symbols: Vec<&String> = + declared.constants.keys().chain(declared.functions.keys()).collect(); + for names in names { + for (smt, _) in &quantifier.binders { + if let Some(source) = vir::air_names::source_symbol(names, smt) { + binders.entry(source).or_insert_with(|| smt.clone()); + } + } + for &symbol in &symbols { + // A call head is recorded under its whole symbol, `?` and all, + // which `source_symbol` strips before looking up. + let source = match names.get(symbol.as_str()) { + Some(name) => Some(name.name().to_owned()), + None => symbol + .strip_suffix(vir::def::AIR_GLOBAL_SUFFIX) + .filter(|stem| names.contains_key(*stem)) + .and_then(|_| vir::air_names::source_symbol(names, symbol)), + }; + let Some(source) = source else { continue }; + let last = source.rsplit("::").next().unwrap_or(&source).to_string(); + by_source.entry(last).or_default().insert(symbol.clone()); + by_source.entry(source).or_default().insert(symbol.clone()); + } + } + Self { binders, binder_sorts, declared, by_source } + } + + fn atom(&self, atom: &str) -> Result { + if let Some(binder) = self.binders.get(atom) { + return Ok(binder.clone()); + } + if self.declared.declares(atom) || is_literal(atom) { + return Ok(atom.to_string()); + } + match self.by_source.get(atom) { + Some(symbols) if symbols.len() == 1 => Ok(symbols.iter().next().unwrap().clone()), + Some(symbols) => Err(format!( + "`{atom}` could name any of {}; write the one meant", + symbols.iter().cloned().collect::>().join(", ") + )), + // an operator, a hole, or a symbol the solver declared itself + None => Ok(atom.to_string()), + } + } + + fn node(&self, node: &TreeNode) -> Result { + match node { + TreeNode::Atom(atom) => Ok(TreeNode::Atom(self.atom(atom)?)), + TreeNode::List(items) => { + Ok(TreeNode::List(items.iter().map(|n| self.node(n)).collect::>()?)) + } + } + } + + /// `term`, in the solver's spelling and boxed or unboxed to `want` when + /// that is its sort's counterpart. + fn term_as(&self, text: &str, want: Option<&str>) -> Result { + let (node, sort) = self.typed(&self.term(text)?); + Ok(self.coerce(node, sort.as_deref(), want)) + } + + /// The function that boxes a value of `sort` into `Poly`, or unboxes it. + fn boxing(&self, sort: &str, unbox: bool) -> Option { + let head = match (sort, unbox) { + ("Int", false) => vir::def::BOX_INT.to_owned(), + ("Bool", false) => vir::def::BOX_BOOL.to_owned(), + ("Int", true) => vir::def::UNBOX_INT.to_owned(), + ("Bool", true) => vir::def::UNBOX_BOOL.to_owned(), + (_, false) => format!("{}{sort}", vir::def::PREFIX_BOX), + (_, true) => format!("{}{sort}", vir::def::PREFIX_UNBOX), + }; + self.declared.functions.contains_key(&head).then_some(head) + } + + /// `node`, of sort `have`, as a value of sort `want`: boxed or unboxed + /// when one of them is `Poly`, else as it is. + fn coerce(&self, node: TreeNode, have: Option<&str>, want: Option<&str>) -> TreeNode { + let head = match (have, want) { + (Some(have), Some(want)) if have != want && want == POLY => self.boxing(have, false), + (Some(have), Some(want)) if have != want && have == POLY => self.boxing(want, true), + _ => None, + }; + match head { + Some(head) => TreeNode::List(vec![TreeNode::Atom(head), node]), + None => node, + } + } + + /// `node` with its arguments coerced to the sorts its functions and + /// operators take, and its own sort, when that can be told. + fn typed(&self, node: &TreeNode) -> (TreeNode, Option) { + let items = match node { + TreeNode::Atom(atom) => { + let sort = self + .binder_sorts + .get(atom) + .or_else(|| self.declared.constants.get(atom)) + .cloned() + .or_else(|| match atom.as_str() { + "true" | "false" => Some("Bool".to_owned()), + _ if !atom.is_empty() && atom.bytes().all(|b| b.is_ascii_digit()) => { + Some("Int".to_owned()) + } + _ => None, + }); + return (node.clone(), sort); + } + TreeNode::List(items) => items, + }; + let Some((TreeNode::Atom(head), args)) = items.split_first() else { + return (node.clone(), None); + }; + let typed: Vec<(TreeNode, Option)> = args.iter().map(|a| self.typed(a)).collect(); + let all = |sort: &str| vec![Some(sort.to_owned()); typed.len()]; + let (wants, sort): (Vec>, Option) = + match self.declared.functions.get(head) { + Some((params, result)) if params.len() == typed.len() => { + (params.iter().cloned().map(Some).collect(), Some(result.clone())) + } + Some(_) => (vec![None; typed.len()], None), + None => match head.as_str() { + "+" | "-" | "*" | "div" | "mod" => (all("Int"), Some("Int".to_owned())), + "<" | "<=" | ">" | ">=" => (all("Int"), Some("Bool".to_owned())), + "and" | "or" | "not" | "=>" => (all("Bool"), Some("Bool".to_owned())), + // both sides alike: boxed if either is + "=" | "distinct" => { + let boxed = typed.iter().any(|(_, s)| s.as_deref() == Some(POLY)); + let side = if boxed { Some(POLY.to_owned()) } else { None }; + (vec![side; typed.len()], Some("Bool".to_owned())) + } + "ite" if typed.len() == 3 => { + let boxed = typed[1..].iter().any(|(_, s)| s.as_deref() == Some(POLY)); + let branch = if boxed { Some(POLY.to_owned()) } else { typed[1].1.clone() }; + (vec![Some("Bool".to_owned()), branch.clone(), branch.clone()], branch) + } + _ => (vec![None; typed.len()], None), + }, + }; + let mut out = vec![TreeNode::Atom(head.clone())]; + for ((arg, have), want) in typed.into_iter().zip(wants) { + out.push(self.coerce(arg, have.as_deref(), want.as_deref())); + } + (TreeNode::List(out), sort) + } + + /// An SMT term (one symbol, or starting with `(`) or a Verus expression + /// (see `surface_term`), in the solver's spelling. + fn term(&self, text: &str) -> Result { + let text = text.trim(); + let node = match parse_term(text) { + Some(node @ TreeNode::Atom(_)) => node, + Some(node) if text.starts_with('(') => node, + _ if text.starts_with('(') && !text.contains(',') => { + return Err(format!("not a single SMT term: {text}")); + } + _ => surface_term(text)?, + }; + self.node(&node) + } +} + +/// A Verus expression as an SMT term: calls `f(a, b)` and paths, variables, +/// numerals, `true` and `false`, parentheses, and the operators `!` and unary +/// `-`, `* / %`, `+ -`, `< <= > >= == !=`, `&&`, `||` and `==>`, loosest +/// last. Names stay as written, for `Lowering` to resolve; `#0` and `_0` are +/// names too, so a fingerprint's holes survive. +fn surface_term(text: &str) -> Result { + let chars: Vec = text.chars().collect(); + let name_char = |c: char| c.is_ascii_alphanumeric() || c == '_' || c == '#' || c == '@'; + let mut tokens = Vec::new(); + let mut i = 0; + while i < chars.len() { + let c = chars[i]; + if c.is_whitespace() { + i += 1; + } else if name_char(c) { + let start = i; + while i < chars.len() { + if name_char(chars[i]) { + i += 1; + } else if chars[i] == ':' && chars.get(i + 1) == Some(&':') { + i += 2; + } else { + break; + } + } + tokens.push(chars[start..i].iter().collect::()); + } else { + let rest: String = chars[i..].iter().take(3).collect(); + let op = ["==>", "==", "!=", "<=", ">=", "&&", "||"] + .into_iter() + .find(|op| rest.starts_with(op)) + .map(str::to_string) + .or_else(|| "(),+-*/%<>!".contains(c).then(|| c.to_string())) + .ok_or_else(|| format!("unexpected `{c}` in {text}"))?; + i += op.chars().count(); + tokens.push(op); + } + } + let mut parser = Surface { tokens, pos: 0 }; + let node = parser.binary(0)?; + match parser.tokens.get(parser.pos) { + None => Ok(node), + Some(token) => Err(format!("unexpected `{token}` in {text}")), + } +} + +struct Surface { + tokens: Vec, + pos: usize, +} + +impl Surface { + fn peek(&self) -> Option<&str> { + self.tokens.get(self.pos).map(String::as_str) + } + + fn next(&mut self) -> Result { + let token = self.tokens.get(self.pos).cloned().ok_or("the expression ends too soon")?; + self.pos += 1; + Ok(token) + } + + fn binary(&mut self, min: u8) -> Result { + let mut lhs = self.unary()?; + while let Some(op) = self.peek() { + let (precedence, right) = match op { + "==>" => (1, true), + "||" => (2, false), + "&&" => (3, false), + "==" | "!=" | "<" | "<=" | ">" | ">=" => (4, false), + "+" | "-" => (5, false), + "*" | "/" | "%" => (6, false), + _ => break, + }; + if precedence < min { + break; + } + let op = self.next()?; + let rhs = self.binary(if right { precedence } else { precedence + 1 })?; + let atom = |s: &str| TreeNode::Atom(s.to_string()); + lhs = match op.as_str() { + "!=" => { + TreeNode::List(vec![atom("not"), TreeNode::List(vec![atom("="), lhs, rhs])]) + } + _ => { + let head = match op.as_str() { + "==" => "=", + "&&" => "and", + "||" => "or", + "==>" => "=>", + "/" => "div", + "%" => "mod", + other => other, + }; + TreeNode::List(vec![atom(head), lhs, rhs]) + } + }; + } + Ok(lhs) + } + + fn unary(&mut self) -> Result { + let head = match self.peek() { + Some("!") => "not", + Some("-") => "-", + _ => return self.primary(), + }; + self.pos += 1; + Ok(TreeNode::List(vec![TreeNode::Atom(head.to_string()), self.unary()?])) + } + + fn primary(&mut self) -> Result { + let token = self.next()?; + if token == "(" { + let inner = self.binary(0)?; + return match self.next()?.as_str() { + ")" => Ok(inner), + other => Err(format!("expected `)`, found `{other}`")), + }; + } + if !token.starts_with(|c: char| c.is_ascii_alphanumeric() || c == '_' || c == '#') { + return Err(format!("unexpected `{token}`")); + } + if self.peek() != Some("(") { + return Ok(TreeNode::Atom(token)); + } + self.pos += 1; + let mut items = vec![TreeNode::Atom(token)]; + if self.peek() == Some(")") { + self.pos += 1; + } else { + loop { + items.push(self.binary(0)?); + match self.next()?.as_str() { + "," => {} + ")" => break, + other => return Err(format!("expected `,` or `)`, found `{other}`")), + } + } + } + // a call without arguments is the constant itself + Ok(if items.len() == 1 { items.pop().unwrap() } else { TreeNode::List(items) }) + } +} + +/// The hypothesis in the solver's spelling, and for an instantiation, its +/// term for each variable; or why it cannot be sent. +fn lower_hypothesis( + request: &HypothesisRequest, + quantifier: &QuantifierSmt, + lowering: &Lowering, +) -> Result<(Hypothesis, HashMap), (&'static str, String)> { + let qid = quantifier.qid.clone(); + match request { + HypothesisRequest::Instantiation { subst, .. } => { + let mut terms: HashMap = HashMap::new(); + for (name, text) in subst { + let Some(smt) = lowering.binders.get(name.as_str()) else { + let binders: Vec<&str> = + quantifier.binders.iter().map(|(smt, _)| smt.as_str()).collect(); + return Err(( + "mismatch", + format!("{qid} binds no variable {name}; it binds {}", binders.join(", ")), + )); + }; + let sort = lowering.binder_sorts.get(smt).map(String::as_str); + let term = lowering.term_as(text, sort).map_err(|e| ("could_not_lower", e))?; + if terms.insert(smt.clone(), term).is_some() { + return Err(("mismatch", format!("two terms for the variable {smt}"))); + } + } + let missing: Vec = quantifier + .binders + .iter() + .filter(|(smt, _)| !terms.contains_key(smt)) + .map(|(smt, sort)| format!("{smt} ({})", flat(sort))) + .collect(); + if !missing.is_empty() { + return Err(( + "mismatch", + format!( + "no term for {}: every variable needs one, type variables included", + missing.join(", ") + ), + )); + } + let subst = quantifier + .binders + .iter() + .map(|(smt, _)| (smt.clone(), flat(&terms[smt]))) + .collect(); + Ok((Hypothesis::Instantiate { qid, subst }, terms)) + } + HypothesisRequest::TriggerPattern { pattern, .. } => { + let pattern: Vec = pattern + .terms() + .into_iter() + .map(|term| lowering.term_as(term, None).map(|node| flat(&node))) + .collect::>() + .map_err(|e| ("could_not_lower", e))?; + if pattern.is_empty() { + return Err(("mismatch", "the pattern has no terms".to_string())); + } + Ok(( + Hypothesis::Trigger { qid, vars: quantifier.binders.clone(), pattern }, + HashMap::new(), + )) + } + HypothesisRequest::BlockCycle { fingerprint, .. } => { + let fingerprint = + flat(&lowering.term_as(fingerprint, None).map_err(|e| ("could_not_lower", e))?); + Ok((Hypothesis::Block { qid, fingerprint }, HashMap::new())) + } + } +} + +/// `(=> G P)` without the `has_type` conjuncts of `G`, which a term of the +/// variable's type satisfies and source never writes. +fn without_type_guards(node: &TreeNode) -> TreeNode { + let guard = |n: &TreeNode| { + matches!(n, TreeNode::List(items) + if matches!(items.first(), Some(TreeNode::Atom(head)) if head == vir::def::HAS_TYPE)) + }; + let TreeNode::List(items) = node else { return node.clone() }; + let [TreeNode::Atom(implies), hypothesis, conclusion] = &items[..] else { + return node.clone(); + }; + if implies != "=>" { + return node.clone(); + } + let kept: Vec = match hypothesis { + TreeNode::List(conjuncts) if matches!(conjuncts.first(), Some(TreeNode::Atom(head)) if head == "and") => { + conjuncts[1..].iter().filter(|n| !guard(n)).cloned().collect() + } + n if guard(n) => Vec::new(), + n => vec![n.clone()], + }; + let atom = |s: &str| TreeNode::Atom(s.to_string()); + match kept.len() { + 0 => conclusion.clone(), + 1 => TreeNode::List(vec![atom("=>"), kept[0].clone(), conclusion.clone()]), + _ => { + let and = TreeNode::List(std::iter::once(atom("and")).chain(kept).collect()); + TreeNode::List(vec![atom("=>"), and, conclusion.clone()]) + } + } +} + +/// `assert();` when that pastes as source; else an assert +/// that mentions the instance of one of the quantifier's triggers, which +/// makes it fire at those terms. +fn instance_assert( + quantifier: &QuantifierSmt, + subst: &HashMap, + names: &QueryNames, +) -> Option { + let body = flat(&without_type_guards(&quantifier.instance(subst))); + if names.pasteable(&[&body]) { + return Some(format!("assert({});", names.render_plain(&body))); + } + quantifier.trigger_instances(subst).iter().find_map(|trigger| { + let terms: Vec = trigger.iter().map(flat).collect(); + let refs: Vec<&str> = terms.iter().map(String::as_str).collect(); + names.pasteable(&refs).then(|| { + let mentions: Vec = terms + .iter() + .map(|term| { + let term = names.render_plain(term); + format!("{term} == {term}") + }) + .collect(); + format!("assert({});", mentions.join(" && ")) + }) + }) +} + +fn describe_quantifier( + quantifier: &QuantifierSmt, + symbols: Option<&crate::provenance::Symbols>, + names: &QueryNames, +) -> QuantifierDescription { + let site = symbols.and_then(|symbols| symbols.quantifier_site(&quantifier.qid)); + QuantifierDescription { + qid: quantifier.qid.clone(), + function: site.map(|(function, _)| function.to_owned()), + span: site.and_then(|(_, span)| span.map(str::to_owned)), + in_query: quantifier.in_query, + binders: quantifier + .binders + .iter() + .map(|(smt, sort)| BinderDescription { + name: vir::air_names::source_symbol(&names.shown, smt) + .unwrap_or_else(|| smt.clone()), + smt_name: smt.clone(), + sort: flat(sort), + }) + .collect(), + triggers: quantifier + .triggers + .iter() + .map(|trigger| trigger.iter().map(|term| names.show(&flat(term))).collect()) + .collect(), + smt_triggers: quantifier + .triggers + .iter() + .map(|trigger| trigger.iter().map(flat).collect()) + .collect(), + } +} + +fn speculation_run( + result: QueryResult, + elapsed_ms: u128, + reply: &SpeculationReply, + symbols: Option<&crate::provenance::Symbols>, +) -> SpeculationRun { + SpeculationRun { + result, + elapsed_ms, + rounds: reply.rounds, + loops: reply + .loops + .iter() + .map(|l| { + let site = symbols.and_then(|symbols| symbols.quantifier_site(&l.qid)); + ResolvedSpeculationLoop { + qid: l.qid.clone(), + function: site.map(|(function, _)| function.to_owned()), + span: site.and_then(|(_, span)| span.map(str::to_owned)), + instantiations: l.instantiations, + directed: l.directed, + rounds: l.rounds, + rises: l.rises, + first_depth: l.first_depth, + max_depth: l.max_depth, + } + }) + .collect(), + } +} + +/// Check a retained query with `hypothesis` in its scope, and read what cvc5 +/// reported about it. Rounds for further errors are not run, and nothing is +/// saved as a certificate. The caller has restored the query's prefix. +fn speculation_check( + air: &mut Context, + query: &RetainedQuery, + hypothesis: Hypothesis, + loop_threshold: Option, + set_rlimit: &impl Fn(&mut Context, f32), +) -> io::Result<(QueryResult, u128, SpeculationReply)> { + set_rlimit(air, query.rlimit); + air.set_speculation(Some(SpeculationRequest { hypothesis, loop_threshold })); + let start = Instant::now(); + let outcome = air.check_valid( + &VirMessageInterface {}, + &QueryDiagnostics::default(), + &query.query, + QueryContext::default(), + ); + let elapsed_ms = start.elapsed().as_millis(); + // a check that never reached the solver leaves the request behind + air.set_speculation(None); + let reply = air.take_speculation(); + drop(air.take_provenance()); + drop(air.take_unknown_reason()); + drop(air.take_matching_loops()); + drop(air.take_difficulty()); + drop(air.take_inst_pressure()); + let result = match outcome { + ValidityResult::Valid(_) => QueryResult::Valid, + ValidityResult::Invalid(..) => QueryResult::Invalid, + ValidityResult::Canceled => QueryResult::ResourceLimit, + ValidityResult::TypeError(error) => return Err(io::Error::other(error.to_string())), + ValidityResult::UnexpectedOutput(error) => return Err(io::Error::other(error)), + }; + air.finish_query(); + let reply = reply.unwrap_or_else(|| SpeculationReply { + unparsed: Some("the check did not reach check-sat".to_owned()), + ..SpeculationReply::default() + }); + Ok((result, elapsed_ms, reply)) +} + +/// cvc5's `(error "...")` as its message. +fn error_message(line: &str) -> String { + line.strip_prefix("(error \"") + .and_then(|rest| rest.strip_suffix("\")")) + .map(|message| message.replace("\"\"", "\"")) + .unwrap_or_else(|| line.to_owned()) +} + +/// Serve a `speculate` request for one query of `bucket`, whose address the +/// caller has checked. `Ok(Err(_))` is a refusal to report; `Err` ends the +/// session. +fn serve_speculate( + bucket: &RetainedBucket, + id: QueryId, + hypothesis: Option, + loop_threshold: Option, + set_rlimit: &impl Fn(&mut Context, f32), +) -> io::Result> { + let mut state = + bucket.state.lock().map_err(|_| io::Error::other("resident bucket poisoned"))?; + let (solver, local) = bucket.addresses[id.0]; + let SolverState { air, journal } = &mut state[solver]; + if !matches!(air.get_solver(), SmtSolver::Cvc5) { + return Ok(Err("speculative probes need cvc5")); + } + let prefix = journal.queries[local].prefix; + let restore_start = Instant::now(); + journal.restore_prefix(air, prefix)?; + let restore_ms = restore_start.elapsed().as_millis(); + if !air.supports_speculation() { + return Ok(Err( + "this cvc5 does not serve speculative probes: it needs (speculate ...) and (get-info :speculation)", + )); + } + let start = Instant::now(); + let query = &journal.queries[local]; + let decls: Vec<&Decl> = journal + .base + .iter() + .chain(journal.contexts[..prefix].iter().flatten()) + .flat_map(|batch| batch.iter()) + .filter_map(|command| match &**command { + CommandX::Global(decl) => Some(decl), + _ => None, + }) + .collect(); + let symbols = bucket.symbols.as_ref(); + let no_versions = VariableVersions::new(); + let empty = SourceNames::new(); + let unversioned = QueryNames::new(symbols, &no_versions, &empty); + let mut outcome = SpeculationOutcome::new( + hypothesis.as_ref().map_or("none", HypothesisRequest::name), + hypothesis.as_ref().map(|h| h.qid().to_owned()), + ); + outcome.restore_ms = restore_ms; + let candidates = |air: &Context| -> Vec { + let written = |qid: &str, in_query: bool| { + in_query + || symbols + .and_then(|symbols| symbols.quantifier_site(qid)) + .is_some_and(|(_, span)| span.is_some()) + }; + air.quantifiers(decls.iter().copied(), &query.query, written) + .iter() + .take(MAX_CANDIDATES) + .map(|q| describe_quantifier(q, symbols, &unversioned)) + .collect() + }; + + // The quantifier the hypothesis names, and the hypothesis in the + // solver's spelling, or why nothing will be checked. + let mut target = None; + if let Some(request) = &hypothesis { + let Some(quantifier) = + air.find_quantifier(decls.iter().copied(), &query.query, request.qid()) + else { + outcome.status = Some("no_quantifier".to_owned()); + outcome.reason = Some(format!( + "no quantifier named {} is asserted in this query's scope", + request.qid() + )); + outcome.candidates = candidates(air); + outcome.notes = "Nothing was checked. The candidates are the quantifiers written in source that this query's scope asserts.".to_owned(); + outcome.elapsed_ms = start.elapsed().as_millis(); + return Ok(Ok(outcome)); + }; + outcome.quantifier = Some(describe_quantifier(&quantifier, symbols, &unversioned)); + let lowering = Lowering::new( + &quantifier, + Declarations::of(&decls, &query.query), + &[&unversioned.shown, &unversioned.plain], + ); + match lower_hypothesis(request, &quantifier, &lowering) { + Ok((lowered, subst)) => target = Some((quantifier, lowered, subst)), + Err((status, reason)) => { + outcome.status = Some(status.to_owned()); + outcome.notes = format!("Nothing was checked: {reason}."); + outcome.reason = Some(reason); + outcome.elapsed_ms = start.elapsed().as_millis(); + return Ok(Ok(outcome)); + } + } + } + + let (before_result, before_ms, before_reply) = + speculation_check(air, query, Hypothesis::Observe, loop_threshold, set_rlimit)?; + let before = speculation_run(before_result, before_ms, &before_reply, symbols); + let before_loops: HashSet = before.loops.iter().map(|l| l.qid.clone()).collect(); + let before_loop_count = before.loops.len(); + outcome.before = Some(before); + let Some((quantifier, lowered, subst)) = target else { + outcome.candidates = candidates(air); + outcome.notes = format!( + "No hypothesis: the query was checked as usual and answers {}, with {before_loop_count} matching loop(s). The candidates are the quantifiers written in source that its scope asserts.", + result_name(before_result) + ); + outcome.elapsed_ms = start.elapsed().as_millis(); + return Ok(Ok(outcome)); + }; + + let (after_result, after_ms, after_reply) = + speculation_check(air, query, lowered.clone(), loop_threshold, set_rlimit)?; + if let Some(error) = &after_reply.error { + outcome.status = Some("could_not_lower".to_owned()); + outcome.reason = Some(error_message(error)); + outcome.notes = "cvc5 could not read the hypothesis in the query's scope, so the query was not checked with it.".to_owned(); + outcome.elapsed_ms = start.elapsed().as_millis(); + return Ok(Ok(outcome)); + } + let report = + after_reply.hypotheses.iter().find(|h| h.kind != "observe").cloned().unwrap_or_default(); + outcome.status = Some(report.status.replace('-', "_")); + outcome.reason = report.reason.clone(); + let after = speculation_run(after_result, after_ms, &after_reply, symbols); + outcome.new_loops = + after.loops.iter().filter(|l| !before_loops.contains(&l.qid)).cloned().collect(); + outcome.introduced_loop = Some(!outcome.new_loops.is_empty()); + let after_loop_count = after.loops.len(); + outcome.after = Some(after); + // A query near its resource limit can flip between two checks of its + // own, so a close counts only if the query still fails right after. + let mut closed = before_result != QueryResult::Valid && after_result == QueryResult::Valid; + if closed { + let (result, elapsed_ms, reply) = + speculation_check(air, query, Hypothesis::Observe, loop_threshold, set_rlimit)?; + closed = result != QueryResult::Valid; + outcome.recheck = Some(speculation_run(result, elapsed_ms, &reply, symbols)); + } + outcome.closed = closed; + + // Source for the check's terms, SSA versions included. + let names = QueryNames::new(symbols, &after_reply.variable_versions, &empty); + if !matches!(lowered, Hypothesis::Block { .. }) { + outcome.new_provenance = Some(NewProvenance { + closing_instantiations: report + .instances + .iter() + .map(|terms| DirectedInstance { + qid: quantifier.qid.clone(), + terms: terms.iter().map(|term| names.show(term)).collect(), + smt_terms: terms.clone(), + inference_id: "LLM_DIRECTED", + }) + .collect(), + extra_inst_count: report.added, + }); + } + let at = symbols + .and_then(|symbols| symbols.quantifier_site(&quantifier.qid)) + .and_then(|(_, span)| span) + .map(|span| format!(" at {span}")) + .unwrap_or_default(); + match &lowered { + Hypothesis::Instantiate { .. } => { + if closed { + outcome.verus_snippet = instance_assert(&quantifier, &subst, &names); + } + } + Hypothesis::Trigger { pattern, .. } => { + let refs: Vec<&str> = pattern.iter().map(String::as_str).collect(); + if closed && names.pasteable(&refs) { + let rendered: Vec = refs.iter().map(|p| names.render_plain(p)).collect(); + let annotation = format!("#![trigger {}]", rendered.join(", ")); + outcome.suggestion = Some(format!("add {annotation} to the quantifier{at}")); + outcome.verus_snippet = Some(annotation); + } + if closed { + // an instance the trigger made, asserted, which needs no + // change to the quantifier + outcome.fallback_snippet = report.instances.first().and_then(|terms| { + let parsed: Option> = + terms.iter().map(|term| parse_term(term)).collect(); + let subst: HashMap = quantifier + .binders + .iter() + .map(|(smt, _)| smt.clone()) + .zip(parsed?) + .collect(); + instance_assert(&quantifier, &subst, &names) + }); + } + } + Hypothesis::Block { fingerprint, .. } => { + outcome.blocked = Some(report.blocked); + outcome.blocked_examples = report + .instances + .iter() + .map(|terms| terms.iter().map(|term| names.show(term)).collect()) + .collect(); + if closed { + outcome.suggestion = Some(format!( + "the quantifier{at} stops looping once its instantiations matching {} are refused: give it a trigger that cannot match that shape", + names.show(fingerprint) + )); + } + } + Hypothesis::Observe => {} + } + + let mut notes = Vec::new(); + let (with, without) = (result_name(after_result), result_name(before_result)); + match (report.status.as_str(), &lowered) { + ("applied", Hypothesis::Instantiate { .. }) => notes.push(format!( + "The directed instance was added; the query answers {with} with it and {without} without it." + )), + ("applied", Hypothesis::Trigger { .. }) => notes.push(format!( + "The speculative trigger matched {} instantiation(s); the query answers {with} with it and {without} without it.", + report.added + )), + ("applied", Hypothesis::Block { .. }) => notes.push(format!( + "{} instantiation(s) matching the fingerprint were refused; the query answers {with} with the block and {without} without it.", + report.blocked + )), + (status, _) => notes.push(format!( + "The hypothesis did not apply ({}{}); the query answers {with}.", + status.replace('-', "_"), + report.reason.as_deref().map(|r| format!(": {r}")).unwrap_or_default() + )), + } + match &outcome.recheck { + Some(recheck) if recheck.result == QueryResult::Valid => notes.push( + "Checked again without the hypothesis, the query passed: it is near its resource limit, so the close is not the hypothesis's and is not reported.".to_owned(), + ), + Some(_) => notes.push( + "Checked again without the hypothesis, the query still fails, so the close is the hypothesis's.".to_owned(), + ), + None => {} + } + if !outcome.new_loops.is_empty() { + let qids: Vec<&str> = outcome.new_loops.iter().map(|l| l.qid.as_str()).collect(); + notes.push(format!( + "It introduced a matching loop: {} kept being instantiated on deeper terms.", + qids.join(", ") + )); + } else if after_loop_count > 0 { + notes.push( + "It introduced no matching loop; the check without it had the same ones.".to_owned(), + ); + } else { + notes.push("No quantifier kept being instantiated on deeper terms.".to_owned()); + } + outcome.notes = notes.join(" "); + outcome.elapsed_ms = start.elapsed().as_millis(); + Ok(Ok(outcome)) +} + impl QueryJournal { pub(crate) fn new() -> Self { - Self { contexts: Vec::new(), queries: Vec::new(), applied: 0, recorded_in_scope: false } + Self { + contexts: Vec::new(), + queries: Vec::new(), + applied: 0, + recorded_in_scope: false, + base: Vec::new(), + } + } + + /// Keep a batch the solver already holds below the journal's scopes, for + /// requests that read the declarations a query stands on. + pub(crate) fn record_base(&mut self, commands: Commands) { + self.base.push(commands); } /// Retain the next declaration batch, opening a scope when one is needed. @@ -1645,6 +2883,7 @@ impl Server { | Request::Check { session: requested, .. } | Request::Bisect { session: requested, .. } | Request::Egraph { session: requested, .. } + | Request::Speculate { session: requested, .. } | Request::Close { session: requested } | Request::InstGraph { session: requested, .. } if requested != session => @@ -1768,6 +3007,44 @@ impl Server { Err(error) => return fatal(&mut output, error), } } + Request::Speculate { + bucket: bucket_id, + query: id, + hypothesis, + loop_threshold, + .. + } => { + let Some(bucket) = self.buckets.get(bucket_id.0) else { + send(&mut output, &Response::Error { message: "unknown bucket" })?; + continue; + }; + if bucket.queries.get(id.0).is_none() { + send(&mut output, &Response::Error { message: "unknown query" })?; + continue; + } + if loop_threshold.is_some_and(|n| n == 0 || n > MAX_LOOP_THRESHOLD) { + send( + &mut output, + &Response::Error { + message: "loop_threshold must be between 1 and 1000", + }, + )?; + continue; + } + match serve_speculate(bucket, id, hypothesis, loop_threshold, &set_rlimit) { + Ok(Ok(outcome)) => send( + &mut output, + &Response::Speculated { + session, + bucket: bucket_id, + query: id, + outcome: Box::new(outcome), + }, + )?, + Ok(Err(message)) => send(&mut output, &Response::Error { message })?, + Err(error) => return fatal(&mut output, error), + } + } Request::Check { bucket: bucket_id, query: id, .. } => { let Some(bucket) = self.buckets.get(bucket_id.0) else { send(&mut output, &Response::Error { message: "unknown bucket" })?; @@ -2541,6 +3818,80 @@ mod tests { } } + /// A hypothesis's terms may be Verus expressions; they become the SMT + /// terms the solver reads, names still as written. + #[test] + fn surface_expressions_become_smt_terms() { + let smt = |text: &str| flat(&surface_term(text).unwrap()); + assert_eq!(smt("decode(encode(k))"), "(decode (encode k))"); + assert_eq!( + smt("f(a + 1, b) == 2 && !g(x) || h(-y) % 3 != 0"), + "(or (and (= (f (+ a 1) b) 2) (not (g x))) (not (= (mod (h (- y)) 3) 0)))" + ); + assert_eq!(smt("x ==> y ==> z"), "(=> x (=> y z))"); + assert_eq!(smt("a - b - c"), "(- (- a b) c)"); + assert_eq!(smt("crate::m::f(x@1, #0, _)"), "(crate::m::f x@1 #0 _)"); + assert_eq!(smt("(a * (b / c))"), "(* a (div b c))"); + for bad in ["f(a", "f(a,)", "a +", "a $ b", "(a) b"] { + assert!(surface_term(bad).is_err(), "{bad}"); + } + } + + /// Verus boxes a quantifier's variables and a spec function's arguments + /// into `Poly`, so a term for one is boxed when its sort is concrete, and + /// a source name is looked up among the scope's declarations. + #[test] + fn lowering_boxes_values_where_poly_is_taken() { + let tree = |text: &str| parse_term(text).unwrap(); + let quantifier = QuantifierSmt { + qid: "user_q_0".to_owned(), + binders: vec![("i$".to_owned(), tree("Poly"))], + triggers: vec![vec![tree("(m!f.? i$)")]], + body: tree("(> (%I (m!f.? i$)) 0)"), + in_query: true, + }; + let mut declared = Declarations::default(); + declared.constants.insert("a!".to_owned(), "Int".to_owned()); + for (f, args, result) in [ + ("m!f.?", vec![POLY], "Int"), + ("m!s.?", vec![POLY], "Int"), + (vir::def::BOX_INT, vec!["Int"], POLY), + (vir::def::UNBOX_INT, vec![POLY], "Int"), + ] { + let args = args.into_iter().map(str::to_owned).collect(); + declared.functions.insert(f.to_owned(), (args, result.to_owned())); + } + let mut names = SourceNames::new(); + for (symbol, name) in [("a!", "a"), ("i$", "i"), ("m!f.", "m::f"), ("m!s.", "m::s")] { + names.insert(symbol.to_owned(), vir::air_names::SourceName::Symbol(name.to_owned())); + } + let lowering = Lowering::new(&quantifier, declared, &[&names]); + let lower = |text: &str, want: Option<&str>| flat(&lowering.term_as(text, want).unwrap()); + assert_eq!(lower("a", Some(POLY)), "(I a!)"); + assert_eq!(lower("a + 1", Some(POLY)), "(I (+ a! 1))"); + assert_eq!(lower("f(i)", None), "(m!f.? i$)"); + assert_eq!(lower("s(s(a))", Some(POLY)), "(I (m!s.? (I (m!s.? (I a!)))))"); + assert_eq!(lower("f(i) > 0", None), "(> (m!f.? i$) 0)"); + // a hole has no sort, so it is left as it is + assert_eq!(lower("f(s(_))", None), "(m!f.? (I (m!s.? _)))"); + assert_eq!(lower("(m!f.? (I a!))", Some("Int")), "(m!f.? (I a!))"); + } + + #[test] + fn type_guards_are_dropped_from_an_instance() { + let node = |text: &str| parse_term(text).unwrap(); + let guard = format!("({} x T)", vir::def::HAS_TYPE); + assert_eq!( + flat(&without_type_guards(&node(&format!("(=> {guard} (> (f x) 0))")))), + "(> (f x) 0)" + ); + assert_eq!( + flat(&without_type_guards(&node(&format!("(=> (and {guard} (p x)) (q x))")))), + "(=> (p x) (q x))" + ); + assert_eq!(flat(&without_type_guards(&node("(or a b)"))), "(or a b)"); + } + #[test] fn equality_ids_name_the_terms_in_order() { assert_eq!(equality_id("(f b)", "c"), equality_id("(f b)", "c")); diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index 005f4b8c28..5149da7356 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -1798,6 +1798,11 @@ impl Verifier { self.run_command_batches(bucket_id, reporter, &mut air_context, &bucket_context); let mut resident = self.args.resident.then(crate::resident::QueryJournal::new); + if let Some(journal) = &mut resident { + for batch in &bucket_context { + journal.record_base(batch.commands.clone()); + } + } let mut resident_spinoffs = Vec::new(); let bucket = self.get_bucket(bucket_id); @@ -1924,6 +1929,13 @@ impl Verifier { let mut spinoff_journal = (retain_queries && do_spinoff) .then(crate::resident::QueryJournal::new); + // The spun-off solver is set up with the whole + // bucket context so far, below the journal. + if let Some(journal) = &mut spinoff_journal { + for batch in &bucket_context { + journal.record_base(batch.commands.clone()); + } + } let profile_file_name = if *profile_rerun || ((self.args.profile_all || self.args.capture_profiles) diff --git a/source/rust_verify_test/tests/resident.rs b/source/rust_verify_test/tests/resident.rs index b2fe994323..b322dd26d9 100644 --- a/source/rust_verify_test/tests/resident.rs +++ b/source/rust_verify_test/tests/resident.rs @@ -662,6 +662,236 @@ fn resident_egraph_lists_and_injects_equalities() { } } +const SPECULATE_SOURCE: &str = r#" +use vstd::prelude::*; +verus! { + spec fn f(x: int) -> int; + spec fn g(x: int) -> int; + spec fn h(x: int) -> int; + spec fn s(x: int) -> int; + + proof fn speculate_target(a: int) + requires forall|i: int| #![trigger g(i)] g(i) > 0 && f(i) > 0, + { + assert(f(a) > 0); + } + + proof fn speculate_loop(a: int) + requires forall|x: int| #![trigger h(x)] h(x) > h(s(x)), h(a) > 100, + { + assert(h(a) < 0); + } + + proof fn speculate_introduces(a: int) + requires forall|x: int| #![trigger g(x)] h(x) > h(s(x)), h(a) > 0, + { + assert(h(a) < 0); + } +} +"#; + +/// A small budget, so the looping queries give up quickly. Set +/// `RESIDENT_NO_SOLVER_VERSION_CHECK` to run against a cvc5 build whose +/// version differs from the pinned release. +fn speculate_options() -> Vec<&'static str> { + let mut options = vec!["--rlimit", "2"]; + if std::env::var_os("RESIDENT_NO_SOLVER_VERSION_CHECK").is_some() { + options.extend(["-V", "no-solver-version-check"]); + } + options +} + +fn probe( + worker: &mut Worker, + session: &Value, + query: &Value, + hypothesis: Option, +) -> Value { + let mut request = + json!({"command": "speculate", "session": session, "bucket": 0, "query": query}); + if let Some(hypothesis) = hypothesis { + request["hypothesis"] = hypothesis; + } + worker.send(request) +} + +/// The quantifier written in `function`'s own query, from a probe without a +/// hypothesis, which lists them. +fn own_quantifier(worker: &mut Worker, session: &Value, query: &Value) -> Value { + let listed = probe(worker, session, query, None); + assert_eq!(listed["event"], "speculated", "{listed}"); + assert_eq!(listed["hypothesis"], "none", "{listed}"); + listed["candidates"] + .as_array() + .unwrap() + .iter() + .find(|q| q["in_query"] == true) + .unwrap_or_else(|| panic!("no quantifier of the query: {}", listed)) + .clone() +} + +/// A `speculate` request checks a query as usual, then again with one +/// hypothesis in the query's own scope. A directed instance that closes the +/// goal comes back with an assert that, pasted into the source, verifies; a +/// speculative trigger with an annotation that, pasted, verifies too. A block +/// of a matching loop's later rungs ends the loop, and a trigger that makes a +/// quantifier feed itself is reported as introducing one. A hypothesis that +/// names no quantifier, a variable the quantifier lacks, or a term the solver +/// cannot read, is refused in the reply. Afterwards the query rechecks as it +/// did before, and no probe launched a solver: the probes are the pasted +/// source's differential check and the session's state check. +#[test] +#[ignore = "needs cvc5 with (speculate ...) (BasisResearch/cvc5 kg/speculative-probe); un-ignore when the pin moves"] +fn resident_speculate_probes_and_leaves_the_session_unchanged() { + let options = speculate_options(); + let mut worker = Worker::start(SPECULATE_SOURCE, &options); + let ready = worker.receive(); + assert_eq!(ready["event"], "ready", "{ready}"); + let session = ready["session"].clone(); + let target = query_id(&ready, "::speculate_target"); + let first = + worker.send(json!({"command": "check", "session": session, "bucket": 0, "query": target})); + assert_eq!(first["result"], "invalid", "{first}"); + + // Listed without a hypothesis: the requires, with its variable. + let quantifier = own_quantifier(&mut worker, &session, &target); + assert_eq!(quantifier["binders"][0]["name"], "i", "{quantifier}"); + assert!(quantifier["triggers"][0][0].as_str().unwrap().ends_with("g(i)"), "{}", quantifier); + let qid = quantifier["qid"].clone(); + + // A directed instance at i := a closes the goal, and the query still + // fails right after without it. + let instantiation = json!({"instantiation": {"qid": qid, "subst": {"i": "a"}}}); + let probed = probe(&mut worker, &session, &target, Some(instantiation)); + assert_eq!(probed["status"], "applied", "{probed}"); + assert_eq!(probed["before"]["result"], "invalid", "{probed}"); + assert_eq!(probed["after"]["result"], "valid", "{probed}"); + assert_eq!(probed["recheck"]["result"], "invalid", "{probed}"); + assert_eq!(probed["closed"], true, "{probed}"); + assert_eq!(probed["introduced_loop"], false, "{probed}"); + let instance = &probed["new_provenance"]["closing_instantiations"][0]; + assert_eq!(instance["inference_id"], "LLM_DIRECTED", "{probed}"); + assert_eq!(instance["terms"], json!(["a"]), "{probed}"); + // The assert it offers verifies the function once pasted before the goal. + let pasted = probed["verus_snippet"].as_str().unwrap(); + assert!(pasted.starts_with("assert(") && pasted.contains("crate::f(a)"), "{}", probed); + let source = SPECULATE_SOURCE + .replace("assert(f(a) > 0);", &format!("{pasted}\n assert(f(a) > 0);")); + let mut paste_worker = Worker::start(&source, &options); + let paste_ready = paste_worker.receive(); + let pasted_check = paste_worker.send(json!({"command": "check", + "session": paste_ready["session"], "bucket": 0, + "query": query_id(&paste_ready, "::speculate_target")})); + assert_eq!(pasted_check["result"], "valid", "{pasted_check}"); + paste_worker.send(json!({"command": "close", "session": paste_ready["session"]})); + paste_worker.finish(false); + + // A speculative trigger f(i) matches the goal's f(a); its annotation, + // added to the quantifier, verifies the function. + let trigger = json!({"trigger_pattern": {"qid": qid, "pattern": "f(i)"}}); + let triggered = probe(&mut worker, &session, &target, Some(trigger)); + assert_eq!(triggered["status"], "applied", "{triggered}"); + assert_eq!(triggered["closed"], true, "{triggered}"); + let annotation = triggered["verus_snippet"].as_str().unwrap(); + assert!(annotation.starts_with("#![trigger ") && annotation.contains("f(i)"), "{}", triggered); + assert!( + triggered["fallback_snippet"].as_str().unwrap().starts_with("assert("), + "{}", + triggered + ); + let source = SPECULATE_SOURCE + .replace("#![trigger g(i)] g(i) > 0", &format!("#![trigger g(i)] {annotation} g(i) > 0")); + let mut paste_worker = Worker::start(&source, &options); + let paste_ready = paste_worker.receive(); + let pasted_check = paste_worker.send(json!({"command": "check", + "session": paste_ready["session"], "bucket": 0, + "query": query_id(&paste_ready, "::speculate_target")})); + assert_eq!(pasted_check["result"], "valid", "{pasted_check}"); + paste_worker.send(json!({"command": "close", "session": paste_ready["session"]})); + paste_worker.finish(false); + + // Refusals leave the query unchecked and the session serving. + let missing = probe( + &mut worker, + &session, + &target, + Some(json!({"instantiation": {"qid": "user_nothing_0", "subst": {"i": "a"}}})), + ); + assert_eq!(missing["status"], "no_quantifier", "{missing}"); + assert!(missing["before"].is_null(), "{}", missing); + assert!(!missing["candidates"].as_array().unwrap().is_empty(), "{}", missing); + let unbound = probe( + &mut worker, + &session, + &target, + Some(json!({"instantiation": {"qid": qid, "subst": {"j": "a"}}})), + ); + assert_eq!(unbound["status"], "mismatch", "{unbound}"); + let unreadable = probe( + &mut worker, + &session, + &target, + Some(json!({"instantiation": {"qid": qid, "subst": {"i": "nothing_declared(a)"}}})), + ); + assert_eq!(unreadable["status"], "could_not_lower", "{unreadable}"); + assert!(unreadable["reason"].as_str().unwrap().contains("nothing_declared"), "{}", unreadable); + let refused = worker.send(json!({"command": "speculate", "session": session, "bucket": 0, + "query": target, "loop_threshold": 0})); + assert_eq!(refused["event"], "error", "{refused}"); + + // The loop h(x) > h(s(x)) climbs until the budget runs out; blocked from + // its third rung on, it stops. + let looping = query_id(&ready, "::speculate_loop"); + let loop_quantifier = own_quantifier(&mut worker, &session, &looping); + let loop_qid = loop_quantifier["qid"].clone(); + let blocked = probe( + &mut worker, + &session, + &looping, + Some(json!({"block_cycle": {"qid": loop_qid, "fingerprint": "h(s(s(_)))"}})), + ); + assert_eq!(blocked["status"], "applied", "{blocked}"); + let has_loop = + |run: &Value| run["loops"].as_array().unwrap().iter().any(|l| l["qid"] == loop_qid); + assert!(has_loop(&blocked["before"]), "{}", blocked); + assert!(!has_loop(&blocked["after"]), "{}", blocked); + assert!(blocked["blocked"].as_u64().unwrap() > 0, "{}", blocked); + assert_eq!(blocked["introduced_loop"], false, "{blocked}"); + + // The same shape of quantifier, triggered on g, never fires; given the + // trigger h(x), it climbs. + let introducing = query_id(&ready, "::speculate_introduces"); + let intro_quantifier = own_quantifier(&mut worker, &session, &introducing); + let intro_qid = intro_quantifier["qid"].clone(); + let climbing = probe( + &mut worker, + &session, + &introducing, + Some(json!({"trigger_pattern": {"qid": intro_qid, "pattern": "h(x)"}})), + ); + assert_eq!(climbing["status"], "applied", "{climbing}"); + assert_eq!(climbing["introduced_loop"], true, "{climbing}"); + assert!( + climbing["new_loops"].as_array().unwrap().iter().any(|l| l["qid"] == intro_qid), + "{}", + climbing + ); + assert_eq!(climbing["closed"], false, "{climbing}"); + + // Nothing of the probes is left behind. + let last = + worker.send(json!({"command": "check", "session": session, "bucket": 0, "query": target})); + assert_eq!(last["result"], first["result"], "{last}"); + assert_eq!(last["diagnostics"], first["diagnostics"], "{last}"); + assert_eq!(worker.send(json!({"command": "close", "session": session}))["event"], "closed"); + worker.finish(false); + let launches = fs::read_to_string(worker.dir.path().join("launches")).unwrap(); + assert_eq!(launches.lines().count(), 1, "{launches}"); + for log in smt_logs(worker.dir.path()) { + assert_eq!(log.matches("(push").count(), log.matches("(pop").count()); + } +} + /// With instantiation replay, every resident check that proves its query /// saves its instantiations, and a recheck of a query with saved ones first /// tries them alone (`:only`), falling back to the ordinary check unless that @@ -1480,13 +1710,17 @@ fn resident_ready_lists_the_requests_it_serves() { .iter() .map(|command| command.as_str().unwrap().to_owned()) .collect(); - assert_eq!(commands, ["list", "check", "bisect", "egraph", "close", "inst_graph"], "{ready}"); + assert_eq!( + commands, + ["list", "check", "bisect", "egraph", "close", "inst_graph", "speculate"], + "{ready}" + ); // Each listed request parses: a stale session is refused as a session, // not as an unknown request, so the list cannot drift from `Request`. for command in &commands { let request = match command.as_str() { "list" | "close" => json!({"command": command, "session": "stale"}), - "check" | "egraph" => { + "check" | "egraph" | "speculate" => { json!({"command": command, "session": "stale", "bucket": 0, "query": 0}) } "bisect" => { From d2dcec3b6b2fb768792559e0931661aac3be338f Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Tue, 15 Sep 2026 07:42:51 -0400 Subject: [PATCH 2/6] Say when the candidate listing is cut at forty The listing stops at MAX_CANDIDATES but read as complete; every toyDB query hit the cap. The note now gives the count listed and the count the scope asserts. Co-Authored-By: Claude Opus 5 (1M context) --- source/rust_verify/src/resident.rs | 30 +++++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index ee07238fdc..65d20bb54f 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -2450,18 +2450,32 @@ fn serve_speculate( hypothesis.as_ref().map(|h| h.qid().to_owned()), ); outcome.restore_ms = restore_ms; - let candidates = |air: &Context| -> Vec { + // The first MAX_CANDIDATES quantifiers written in source, and a sentence + // saying so when the scope asserts more. + let candidates = |air: &Context| -> (Vec, String) { let written = |qid: &str, in_query: bool| { in_query || symbols .and_then(|symbols| symbols.quantifier_site(qid)) .is_some_and(|(_, span)| span.is_some()) }; - air.quantifiers(decls.iter().copied(), &query.query, written) + let all = air.quantifiers(decls.iter().copied(), &query.query, written); + let listed: Vec = all .iter() .take(MAX_CANDIDATES) .map(|q| describe_quantifier(q, symbols, &unversioned)) - .collect() + .collect(); + let note = if listed.len() < all.len() { + format!( + "The candidates are the first {} of the {} quantifiers written in source that this query's scope asserts.", + listed.len(), + all.len() + ) + } else { + "The candidates are the quantifiers written in source that this query's scope asserts." + .to_owned() + }; + (listed, note) }; // The quantifier the hypothesis names, and the hypothesis in the @@ -2476,8 +2490,9 @@ fn serve_speculate( "no quantifier named {} is asserted in this query's scope", request.qid() )); - outcome.candidates = candidates(air); - outcome.notes = "Nothing was checked. The candidates are the quantifiers written in source that this query's scope asserts.".to_owned(); + let (listed, note) = candidates(air); + outcome.candidates = listed; + outcome.notes = format!("Nothing was checked. {note}"); outcome.elapsed_ms = start.elapsed().as_millis(); return Ok(Ok(outcome)); }; @@ -2506,9 +2521,10 @@ fn serve_speculate( let before_loop_count = before.loops.len(); outcome.before = Some(before); let Some((quantifier, lowered, subst)) = target else { - outcome.candidates = candidates(air); + let (listed, note) = candidates(air); + outcome.candidates = listed; outcome.notes = format!( - "No hypothesis: the query was checked as usual and answers {}, with {before_loop_count} matching loop(s). The candidates are the quantifiers written in source that its scope asserts.", + "No hypothesis: the query was checked as usual and answers {}, with {before_loop_count} matching loop(s). {note}", result_name(before_result) ); outcome.elapsed_ms = start.elapsed().as_millis(); From a493da723780d5b09527400f483112e916e45579 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Tue, 15 Sep 2026 14:43:30 -0400 Subject: [PATCH 3/6] Speculate: read terms at the goal, and paste nothing stale Review fixes. An instantiation's terms stand outside the quantifier, so they no longer resolve names through its variables: a parameter the quantifier shadows is the parameter. A hypothesis's terms are now read after the check without it, at the goal it failed at (the last goal when it names none): Verus terms through the scaffold lowerer, which reads method calls, indexing, casts and old, then as the lowered query reads them there (air::GoalScope), so a mutable local is its version at the goal. SMT-spelled terms map a variable's AIR name to the same version, declare every version, and ask the AIR context about the prelude's functions instead of seeding four boxes by hand, so (Add a! 1) is boxed. A snippet no longer names a variable at another version than the one where it is pasted; QueryNames::pasteable checks the versions live at the goal, for speculate and for the egraph's verus_assert alike. An echoed marker precedes (speculate ...), so only an error after it counts as the hypothesis refused. The status docs name the three reasons for rejected. Co-Authored-By: Claude Opus 5 (1M context) --- source/air/src/lib.rs | 1 + source/air/src/smt_verify.rs | 15 +- source/air/src/var_to_const.rs | 114 +++- source/rust_verify/src/resident.rs | 612 +++++++++++++++++----- source/rust_verify/src/scaffold.rs | 43 +- source/rust_verify_test/tests/resident.rs | 122 +++++ 6 files changed, 762 insertions(+), 145 deletions(-) diff --git a/source/air/src/lib.rs b/source/air/src/lib.rs index 609a3a9dd8..81acd8d1b0 100644 --- a/source/air/src/lib.rs +++ b/source/air/src/lib.rs @@ -28,6 +28,7 @@ mod tests; mod typecheck; mod util; mod var_to_const; +pub use var_to_const::GoalScope; mod visitor; #[cfg(feature = "singular")] diff --git a/source/air/src/smt_verify.rs b/source/air/src/smt_verify.rs index af0836fdea..23603dd219 100644 --- a/source/air/src/smt_verify.rs +++ b/source/air/src/smt_verify.rs @@ -200,6 +200,9 @@ pub type ReportLongRunning<'a> = (std::time::Duration, Box () + 'a>); const GET_VERSION_RESPONSE_PREFIX: &str = "(:version"; +/// Echoed just before a `(speculate ...)` command: the early flush's output +/// after it is the command's. +const SPECULATION_MARKER: &str = "air-speculate"; pub(crate) fn smt_check_assertion<'ctx>( context: &mut Context, @@ -246,12 +249,18 @@ pub(crate) fn smt_check_assertion<'ctx>( // A hypothesis goes in the query's scope before the flush below, so that a // term cvc5 cannot read is refused there, before any check-sat. Only the - // query's first check sends it: later rounds share its scope. + // query's first check sends it: later rounds share its scope. An echoed + // marker goes first, so that only an error after it is the hypothesis's. let speculation = context.speculation.take(); if let Some(request) = &speculation { context.last_speculation = None; + context.smt_log.log_node(&sise::TreeNode::List(vec![ + sise::TreeNode::Atom("echo".to_string()), + sise::TreeNode::Atom(format!("\"{SPECULATION_MARKER}\"")), + ])); context.smt_log.log_node(&request.to_node()); } + let mut past_speculation_marker = false; let mut speculation_refused = None; context.smt_log.log_get_info("version"); @@ -277,7 +286,9 @@ pub(crate) fn smt_check_assertion<'ctx>( ); } } - } else if speculation.is_some() && line.starts_with("(error") { + } else if speculation.is_some() && line.trim_matches('"') == SPECULATION_MARKER { + past_speculation_marker = true; + } else if past_speculation_marker && line.starts_with("(error") { speculation_refused = Some(line); } else if context.ignore_unexpected_smt { diagnostics.report(&context.message_interface.bare( diff --git a/source/air/src/var_to_const.rs b/source/air/src/var_to_const.rs index d7da7bd807..7a5a6f18b8 100644 --- a/source/air/src/var_to_const.rs +++ b/source/air/src/var_to_const.rs @@ -1,6 +1,7 @@ // Replace declare-var and assign with declare-const and assume use crate::ast::{ - Axiom, BinaryOp, Decl, DeclX, Expr, ExprX, Ident, Query, QueryX, Snapshots, Stmt, StmtX, Typ, + AssertId, Axiom, BinaryOp, Decl, DeclX, Expr, ExprX, Ident, Query, QueryX, Snapshots, Stmt, + StmtX, Typ, }; use crate::ast_util::string_var; use indexmap::IndexMap; @@ -125,6 +126,46 @@ struct LowerStmtState { all_snapshots: Snapshots, variable_versions: crate::context::VariableVersions, record_versions: bool, + /// When kept, each assert reached, with the versions and snapshots in + /// force there. + goal_scopes: Option, GoalScope)>>, +} + +/// The variable versions and snapshots in force at one assert of a query: +/// what a variable, or `old` of one, reads as there once the query is +/// lowered. +#[derive(Clone, Debug, Default)] +pub struct GoalScope { + versions: IndexMap, + snapshots: Snapshots, +} + +impl GoalScope { + /// Where `query` reaches the assert with id `goal`, its first + /// occurrence; without a `goal`, or when no assert has it, the query's + /// last assert; before any statement when it has none. + pub fn of(query: &Query, goal: Option<&AssertId>) -> Self { + let (_, _, _, _, entry, scopes) = lower_query_with(query, false, true); + let scopes = scopes.unwrap_or_default(); + let wanted = goal.and_then(|goal| { + scopes.iter().find(|(id, _)| id.as_ref().is_some_and(|id| **id == **goal)) + }); + match wanted.or(scopes.last()) { + Some((_, scope)) => scope.clone(), + None => entry, + } + } + + /// `expr` as the lowered query reads it here: each variable at its + /// version, and `old(x)` at the snapshot's. + pub fn lower_expr(&self, expr: &Expr) -> Expr { + lower_expr(&self.versions, &self.snapshots, expr) + } + + /// Each variable's symbol here, by its AIR name. + pub fn live(&self) -> HashMap { + self.versions.iter().map(|(x, n)| (x.to_string(), rename_var(x, *n))).collect() + } } fn lower_stmt( @@ -138,7 +179,14 @@ fn lower_stmt( lower_expr_visitor(versions, snapshots, e) }); match &*stmt { - StmtX::Assume(_) | StmtX::Assert(..) => stmt, + StmtX::Assume(_) => stmt, + StmtX::Assert(id, ..) => { + if let Some(scopes) = &mut state.goal_scopes { + let scope = GoalScope { versions: versions.clone(), snapshots: snapshots.clone() }; + scopes.push((id.clone(), scope)); + } + stmt + } StmtX::Havoc(x) | StmtX::Assign(x, _) => { let n = find_version(&versions, x); let typ = types[x].clone(); @@ -228,6 +276,25 @@ pub(crate) fn lower_query( query: &Query, record_versions: bool, ) -> (Query, Snapshots, Vec, crate::context::VariableVersions) { + let (query, snapshots, local_vars, versions, _, _) = + lower_query_with(query, record_versions, false); + (query, snapshots, local_vars, versions) +} + +/// `lower_query`, and the scope before the first statement, and with +/// `record_goal_scopes` the scope at each assert reached. +fn lower_query_with( + query: &Query, + record_versions: bool, + record_goal_scopes: bool, +) -> ( + Query, + Snapshots, + Vec, + crate::context::VariableVersions, + GoalScope, + Option, GoalScope)>>, +) { let QueryX { local, assertion } = &**query; let mut decls: Vec = Vec::new(); let mut versions: IndexMap = IndexMap::new(); @@ -271,7 +338,9 @@ pub(crate) fn lower_query( all_snapshots, variable_versions, record_versions, + goal_scopes: record_goal_scopes.then(Vec::new), }; + let entry = GoalScope { versions: versions.clone(), snapshots: snapshots.clone() }; let assertion = lower_stmt(&mut state, &mut versions, &mut snapshots, &types, assertion); let local = Arc::new(state.decls); ( @@ -279,6 +348,8 @@ pub(crate) fn lower_query( state.all_snapshots, local_vars, state.variable_versions, + entry, + state.goal_scopes, ) } @@ -309,4 +380,43 @@ mod tests { lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), false); assert!(versions.is_empty()); } + + /// A variable reads as the version in force at the assert asked about, + /// else at the last assert. + #[test] + fn goal_scopes_read_variables_where_the_goal_is() { + let name = Arc::new("y@".to_string()); + let var = Arc::new(ExprX::Var(name.clone())); + let assert = |id: u64| { + Arc::new(StmtX::Assert( + Some(Arc::new(vec![id])), + crate::messages::MessageInterface::empty(&crate::messages::AirMessageInterface {}), + None, + var.clone(), + )) + }; + let query = Arc::new(QueryX { + local: Arc::new(vec![Arc::new(DeclX::Var( + name.clone(), + Arc::new(crate::ast::TypX::Int), + ))]), + assertion: Arc::new(StmtX::Block(Arc::new(vec![ + assert(0), + Arc::new(StmtX::Havoc(name.clone())), + assert(1), + Arc::new(StmtX::Havoc(name.clone())), + ]))), + }); + let read = |goal: Option| { + let scope = GoalScope::of(&query, goal.as_ref()); + match &*scope.lower_expr(&var) { + ExprX::Var(x) => (x.to_string(), scope.live()["y@"].clone()), + other => panic!("{:?}", other), + } + }; + assert_eq!(read(Some(Arc::new(vec![0]))), ("y@0".to_string(), "y@0".to_string())); + assert_eq!(read(Some(Arc::new(vec![1]))), ("y@1".to_string(), "y@1".to_string())); + assert_eq!(read(None), ("y@1".to_string(), "y@1".to_string())); + assert_eq!(read(Some(Arc::new(vec![7]))), ("y@1".to_string(), "y@1".to_string())); + } } diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index 144cb613c6..d1f921c83b 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -1423,6 +1423,9 @@ struct QueryNames<'a> { /// Each SSA symbol's variable and version. Two versions of one variable /// read alike in `plain`, so an assert naming both cannot be pasted. versions: &'a VariableVersions, + /// Each variable's SSA symbol where a snippet goes, by its AIR name. A + /// snippet naming another version of it would read as this one there. + live: Option<&'a HashMap>, } impl<'a> QueryNames<'a> { @@ -1437,16 +1440,23 @@ impl<'a> QueryNames<'a> { shown: symbols.query_names(versions, true), plain: symbols.paste_names(versions), versions, + live: None, }, None => Self { symbols: None, shown: Cow::Borrowed(empty), plain: Cow::Borrowed(empty), versions, + live: None, }, } } + /// These names, for snippets pasted where each variable is `live`'s. + fn at(self, live: &'a HashMap) -> Self { + Self { live: Some(live), ..self } + } + /// `assert(lhs == rhs);` to add to the source, when that assert says what /// the equality says: it is entailed, and both sides paste as source. fn verus_assert(&self, equality: &air::context::EgraphEquality) -> Option { @@ -1460,9 +1470,10 @@ impl<'a> QueryNames<'a> { )) } - /// Whether `terms` paste as source together: each renders as source, and - /// no variable appears in them at two assignment versions, which would - /// read alike. + /// Whether `terms` paste as source together: each renders as source, no + /// variable appears in them at two assignment versions, which would read + /// alike, and none at a version other than the one where the snippet + /// goes, which it would read as. fn pasteable(&self, terms: &[&str]) -> bool { if !terms.iter().all(|term| vir::air_names::renders_as_source(&self.plain, term)) { return false; @@ -1475,6 +1486,9 @@ impl<'a> QueryNames<'a> { if *version_of.entry(base.as_str()).or_insert(*version) != *version { return false; } + if self.live.and_then(|live| live.get(base)).is_some_and(|here| here != atom) { + return false; + } } } true @@ -1699,7 +1713,12 @@ fn serve_egraph( let query = &journal.queries[local]; let (before, reading) = egraph_check(air, query, None, set_rlimit)?; let empty = SourceNames::new(); - let names = QueryNames::new(bucket.symbols.as_ref(), &reading.variable_versions, &empty); + // An assert goes before the goal the check failed at (the query's last + // goal when it names none), where each variable holds the version then. + let goal = before.assert_id.clone().map(std::sync::Arc::new); + let live = air::GoalScope::of(&query.query, goal.as_ref()).live(); + let names = + QueryNames::new(bucket.symbols.as_ref(), &reading.variable_versions, &empty).at(&live); let (listed, hidden) = names.resolve(&reading); let injection = match inject { None => None, @@ -1742,11 +1761,15 @@ const MAX_CANDIDATES: usize = 40; const SPECULATION_CAVEAT: &str = "The hypothesis was sent in the query's own scope and popped right after the check, so the session's solver state is unchanged. A closed verdict is not a verification result: paste the snippet into the source and verify it normally."; -/// A hypothesis as a `speculate` request names it. A term is an SMT term in -/// the solver's spelling, as the `smt_*` fields of other replies give them, -/// or with symbols named by their source names instead, which are looked up -/// among the query's declarations. A variable of the quantifier may be -/// named either way. +/// A hypothesis as a `speculate` request names it. A term is a Verus +/// expression, read as a scaffold request reads an assertion (see +/// `crate::scaffold`) at the goal the query's check fails at, so a mutable +/// local reads as its value there; or an SMT term in the solver's spelling, +/// as the `smt_*` fields of other replies give them. An instantiation's +/// terms stand where the quantifier is instantiated, so they never name its +/// variables; a trigger's are over its variables, which shadow locals of the +/// same name. A variable of the quantifier may be named by its source name +/// or its own. #[derive(Deserialize)] #[serde(rename_all = "snake_case", deny_unknown_fields)] enum HypothesisRequest { @@ -1888,9 +1911,12 @@ struct SpeculationOutcome { /// The query checked with the hypothesis. #[serde(skip_serializing_if = "Option::is_none")] after: Option, - /// `applied`; `rejected` (the instantiation was made already); `mismatch` - /// (the terms do not fit the variables); `unusable` (the pattern cannot - /// be a trigger); `no_quantifier`; `could_not_lower` (a term the solver + /// `applied`; `rejected` (the instantiation funnel refused the directed + /// instance: it was made already, it is a lemma already sent, or the + /// instantiation level limit refused a term; `reason` says which); + /// `mismatch` (the terms do not fit the variables); `unusable` (the + /// pattern cannot be a trigger); `no_quantifier`; `could_not_lower` (a + /// term that cannot be read in the query's scope, or that the solver /// cannot read); `pending` (no instantiation round ran) #[serde(skip_serializing_if = "Option::is_none")] status: Option, @@ -1930,6 +1956,10 @@ struct SpeculationOutcome { /// query's own first, when the request named none or one not there. #[serde(skip_serializing_if = "Vec::is_empty")] candidates: Vec, + /// How names in the hypothesis's Verus terms were read, where more than + /// one reading was possible. + #[serde(skip_serializing_if = "Vec::is_empty")] + readings: Vec, caveat: &'static str, elapsed_ms: u128, restore_ms: u128, @@ -1957,6 +1987,7 @@ impl SpeculationOutcome { suggestion: None, notes: String::new(), candidates: Vec::new(), + readings: Vec::new(), caveat: SPECULATION_CAVEAT, elapsed_ms: 0, restore_ms: 0, @@ -2017,29 +2048,27 @@ fn sort_name(typ: &air::ast::Typ) -> String { /// The sort Verus boxes values into. const POLY: &str = "Poly"; -/// What the query's scope declares, with sorts: constants and variables, -/// and functions (datatype constructors and fields included) with their -/// argument and result sorts. +/// What the query's scope declares, with sorts: constants and variables +/// (each version of a variable too), and functions (datatype constructors +/// and fields included) with their argument and result sorts. The prelude +/// reaches each solver outside the journal; `Lowering` asks the AIR +/// context about its names. #[derive(Default)] struct Declarations { constants: HashMap, functions: HashMap, String)>, + /// Each variable's SSA symbol at the goal, by its AIR name. + live: HashMap, } impl Declarations { - fn of(decls: &[&Decl], query: &Query) -> Self { - let mut out = Self::default(); - // The prelude reaches each solver directly, never through the - // journal, so its boxes for integers and booleans are named here; - // a datatype's are the bucket's own declarations. - for (f, arg, result) in [ - (vir::def::BOX_INT, "Int", POLY), - (vir::def::BOX_BOOL, "Bool", POLY), - (vir::def::UNBOX_INT, POLY, "Int"), - (vir::def::UNBOX_BOOL, POLY, "Bool"), - ] { - out.functions.insert(f.to_owned(), (vec![arg.to_owned()], result.to_owned())); - } + fn of( + decls: &[&Decl], + query: &Query, + live: HashMap, + versions: &VariableVersions, + ) -> Self { + let mut out = Self { live, ..Self::default() }; for decl in decls.iter().copied().chain(query.local.iter()) { match &**decl { DeclX::Const(x, typ) | DeclX::Var(x, typ) => { @@ -2068,6 +2097,11 @@ impl Declarations { DeclX::Sort(_) | DeclX::Axiom(_) => {} } } + for (ssa, (variable, _)) in versions { + if let Some(sort) = out.constants.get(variable).cloned() { + out.constants.insert(ssa.clone(), sort); + } + } out } @@ -2076,37 +2110,60 @@ impl Declarations { } } -/// Turns the terms of a hypothesis into the solver's spelling: names -/// resolved, and values boxed into `Poly` or unboxed out of it where a -/// function, operator or variable takes the other, as Verus's encoding does. -struct Lowering { +/// Each of `binders`, by its own name and by its source name: its own name. +fn binder_names(binders: &[(String, TreeNode)], names: &[&SourceNames]) -> HashMap { + let mut out: HashMap = + binders.iter().map(|(smt, _)| (smt.clone(), smt.clone())).collect(); + for names in names { + for (smt, _) in binders { + if let Some(source) = vir::air_names::source_symbol(names, smt) { + out.entry(source).or_insert_with(|| smt.clone()); + } + } + } + out +} + +/// SMT-LIB's own operators, which head an SMT term rather than a call. +const SMT_OPERATORS: &[&str] = &[ + "+", "-", "*", "/", "div", "mod", "<", "<=", ">", ">=", "=", "distinct", "and", "or", "not", + "=>", "ite", "_", +]; + +/// Turns the terms of a hypothesis written in the solver's spelling, and its +/// fingerprints, into terms the solver reads: names resolved, and values +/// boxed into `Poly` or unboxed out of it where a function, operator or +/// variable takes the other, as Verus's encoding does. +struct Lowering<'a> { /// A variable of the quantifier, by its own name and by its source - /// name: its own name. + /// name: its own name. Empty for terms that stand outside it. binders: HashMap, /// Each variable's sort, by its own name. binder_sorts: HashMap, declared: Declarations, /// A declared symbol by its source name, whole and by its last path /// segment. Only symbols an encoder minted for the name itself count, - /// not the helpers named after it (a function's `req%`, `ens%`). + /// not the helpers named after it (a function's `req%`, `ens%`). A + /// variable counts as its symbol at the goal. by_source: HashMap>, + /// What the AIR context declares a name as: the prelude's names. + context: &'a dyn Fn(&str) -> Option, } -impl Lowering { - fn new(quantifier: &QuantifierSmt, declared: Declarations, names: &[&SourceNames]) -> Self { - let mut binders: HashMap = - quantifier.binders.iter().map(|(smt, _)| (smt.clone(), smt.clone())).collect(); - let binder_sorts = - quantifier.binders.iter().map(|(smt, sort)| (smt.clone(), flat(sort))).collect(); +impl<'a> Lowering<'a> { + /// `binders` are the quantifier's variables when the terms are over + /// them (a trigger), and none when they stand outside it. + fn new( + binders: &[(String, TreeNode)], + declared: Declarations, + names: &[&SourceNames], + context: &'a dyn Fn(&str) -> Option, + ) -> Self { + let binder_sorts = binders.iter().map(|(smt, sort)| (smt.clone(), flat(sort))).collect(); let mut by_source: HashMap> = HashMap::new(); let symbols: Vec<&String> = declared.constants.keys().chain(declared.functions.keys()).collect(); for names in names { - for (smt, _) in &quantifier.binders { - if let Some(source) = vir::air_names::source_symbol(names, smt) { - binders.entry(source).or_insert_with(|| smt.clone()); - } - } for &symbol in &symbols { // A call head is recorded under its whole symbol, `?` and all, // which `source_symbol` strips before looking up. @@ -2118,19 +2175,73 @@ impl Lowering { .and_then(|_| vir::air_names::source_symbol(names, symbol)), }; let Some(source) = source else { continue }; + let target = declared.live.get(symbol).unwrap_or(symbol).clone(); let last = source.rsplit("::").next().unwrap_or(&source).to_string(); - by_source.entry(last).or_default().insert(symbol.clone()); - by_source.entry(source).or_default().insert(symbol.clone()); + by_source.entry(last).or_default().insert(target.clone()); + by_source.entry(source).or_default().insert(target); } } - Self { binders, binder_sorts, declared, by_source } + Self { binders: binder_names(binders, names), binder_sorts, declared, by_source, context } + } + + /// A function's argument and result sorts, the journal's declarations + /// first, then the AIR context's. + fn function(&self, head: &str) -> Option<(Vec, String)> { + self.declared.functions.get(head).cloned().or_else(|| match (self.context)(head) { + Some(air::context::Declared::Fun(params, ret)) => { + Some((params.iter().map(sort_name).collect(), sort_name(&ret))) + } + _ => None, + }) + } + + /// A symbol's sort, when it is a variable or constant. + fn constant(&self, atom: &str) -> Option { + self.binder_sorts.get(atom).or_else(|| self.declared.constants.get(atom)).cloned().or_else( + || match (self.context)(atom) { + Some(air::context::Declared::Var(typ)) => Some(sort_name(&typ)), + _ => None, + }, + ) + } + + fn known(&self, atom: &str) -> bool { + self.binder_sorts.contains_key(atom) + || self.declared.declares(atom) + || self.declared.live.contains_key(atom) + || (self.context)(atom).is_some() + } + + /// Whether `text` is a Verus expression rather than an SMT term. An SMT + /// term is a symbol the scope or the solver declares, or one no Rust + /// name could be (`$`, `a!`); or an application headed by an SMT + /// operator or a declared function. + fn reads_as_verus(&self, text: &str) -> bool { + let text = text.trim(); + match parse_term(text) { + Some(TreeNode::Atom(atom)) => { + !self.known(&atom) + && atom.chars().all(|c| c.is_ascii_alphanumeric() || "_:@".contains(c)) + } + Some(TreeNode::List(items)) if text.starts_with('(') => match items.first() { + Some(TreeNode::Atom(head)) => { + !(self.known(head) || SMT_OPERATORS.contains(&head.as_str())) + } + _ => true, + }, + _ => true, + } } fn atom(&self, atom: &str) -> Result { if let Some(binder) = self.binders.get(atom) { return Ok(binder.clone()); } - if self.declared.declares(atom) || is_literal(atom) { + // a variable, spelled as AIR declares it, is its symbol at the goal + if let Some(live) = self.declared.live.get(atom) { + return Ok(live.clone()); + } + if self.known(atom) || is_literal(atom) { return Ok(atom.to_string()); } match self.by_source.get(atom) { @@ -2170,7 +2281,7 @@ impl Lowering { (_, false) => format!("{}{sort}", vir::def::PREFIX_BOX), (_, true) => format!("{}{sort}", vir::def::PREFIX_UNBOX), }; - self.declared.functions.contains_key(&head).then_some(head) + self.function(&head).is_some().then_some(head) } /// `node`, of sort `have`, as a value of sort `want`: boxed or unboxed @@ -2192,18 +2303,13 @@ impl Lowering { fn typed(&self, node: &TreeNode) -> (TreeNode, Option) { let items = match node { TreeNode::Atom(atom) => { - let sort = self - .binder_sorts - .get(atom) - .or_else(|| self.declared.constants.get(atom)) - .cloned() - .or_else(|| match atom.as_str() { - "true" | "false" => Some("Bool".to_owned()), - _ if !atom.is_empty() && atom.bytes().all(|b| b.is_ascii_digit()) => { - Some("Int".to_owned()) - } - _ => None, - }); + let sort = self.constant(atom).or_else(|| match atom.as_str() { + "true" | "false" => Some("Bool".to_owned()), + _ if !atom.is_empty() && atom.bytes().all(|b| b.is_ascii_digit()) => { + Some("Int".to_owned()) + } + _ => None, + }); return (node.clone(), sort); } TreeNode::List(items) => items, @@ -2213,30 +2319,29 @@ impl Lowering { }; let typed: Vec<(TreeNode, Option)> = args.iter().map(|a| self.typed(a)).collect(); let all = |sort: &str| vec![Some(sort.to_owned()); typed.len()]; - let (wants, sort): (Vec>, Option) = - match self.declared.functions.get(head) { - Some((params, result)) if params.len() == typed.len() => { - (params.iter().cloned().map(Some).collect(), Some(result.clone())) + let (wants, sort): (Vec>, Option) = match self.function(head) { + Some((params, result)) if params.len() == typed.len() => { + (params.into_iter().map(Some).collect(), Some(result)) + } + Some(_) => (vec![None; typed.len()], None), + None => match head.as_str() { + "+" | "-" | "*" | "div" | "mod" => (all("Int"), Some("Int".to_owned())), + "<" | "<=" | ">" | ">=" => (all("Int"), Some("Bool".to_owned())), + "and" | "or" | "not" | "=>" => (all("Bool"), Some("Bool".to_owned())), + // both sides alike: boxed if either is + "=" | "distinct" => { + let boxed = typed.iter().any(|(_, s)| s.as_deref() == Some(POLY)); + let side = if boxed { Some(POLY.to_owned()) } else { None }; + (vec![side; typed.len()], Some("Bool".to_owned())) } - Some(_) => (vec![None; typed.len()], None), - None => match head.as_str() { - "+" | "-" | "*" | "div" | "mod" => (all("Int"), Some("Int".to_owned())), - "<" | "<=" | ">" | ">=" => (all("Int"), Some("Bool".to_owned())), - "and" | "or" | "not" | "=>" => (all("Bool"), Some("Bool".to_owned())), - // both sides alike: boxed if either is - "=" | "distinct" => { - let boxed = typed.iter().any(|(_, s)| s.as_deref() == Some(POLY)); - let side = if boxed { Some(POLY.to_owned()) } else { None }; - (vec![side; typed.len()], Some("Bool".to_owned())) - } - "ite" if typed.len() == 3 => { - let boxed = typed[1..].iter().any(|(_, s)| s.as_deref() == Some(POLY)); - let branch = if boxed { Some(POLY.to_owned()) } else { typed[1].1.clone() }; - (vec![Some("Bool".to_owned()), branch.clone(), branch.clone()], branch) - } - _ => (vec![None; typed.len()], None), - }, - }; + "ite" if typed.len() == 3 => { + let boxed = typed[1..].iter().any(|(_, s)| s.as_deref() == Some(POLY)); + let branch = if boxed { Some(POLY.to_owned()) } else { typed[1].1.clone() }; + (vec![Some("Bool".to_owned()), branch.clone(), branch.clone()], branch) + } + _ => (vec![None; typed.len()], None), + }, + }; let mut out = vec![TreeNode::Atom(head.clone())]; for ((arg, have), want) in typed.into_iter().zip(wants) { out.push(self.coerce(arg, have.as_deref(), want.as_deref())); @@ -2405,19 +2510,85 @@ impl Surface { } } -/// The hypothesis in the solver's spelling, and for an instantiation, its -/// term for each variable; or why it cannot be sent. -fn lower_hypothesis( +/// The AIR type of a sort as the solver is sent it. +fn typ_of_sort(sort: &str) -> air::ast::Typ { + use air::ast::TypX; + std::sync::Arc::new(match sort { + "Int" => TypX::Int, + "Bool" => TypX::Bool, + "Real" => TypX::Real, + other => TypX::Named(std::sync::Arc::new(other.to_owned())), + }) +} + +/// A query's local constants and variables, with their types. +fn query_locals(query: &Query) -> Vec<(air::ast::Ident, air::ast::Typ)> { + query + .local + .iter() + .filter_map(|decl| match &**decl { + DeclX::Const(x, typ) | DeclX::Var(x, typ) => Some((x.clone(), typ.clone())), + _ => None, + }) + .collect() +} + +/// Reads a hypothesis's Verus terms as a scaffold request reads an assertion, +/// then as the lowered query reads them at the goal: each mutable local at +/// its version there. +struct VerusReader<'e> { + env: crate::scaffold::Env<'e>, + goal: &'e air::GoalScope, + printer: air::printer::Printer, +} + +impl VerusReader<'_> { + fn read( + &self, + text: &str, + want: Option<&str>, + readings: &mut Vec, + ) -> Result { + let want = want.map(typ_of_sort); + let lowered = crate::scaffold::lower_term(text, &self.env, want.as_ref())?; + readings.extend(lowered.choices); + Ok(self.printer.expr_to_node(&self.goal.lower_expr(&lowered.expr))) + } +} + +/// A term of a hypothesis, of sort `want` when given, in the solver's +/// spelling: a Verus expression through `reader` (when source names were +/// recorded), else as `lowering` reads SMT terms. +fn read_term( + text: &str, + want: Option<&str>, + lowering: &Lowering, + reader: Option<&VerusReader>, + readings: &mut Vec, +) -> Result { + match reader { + Some(reader) if lowering.reads_as_verus(text) => reader.read(text, want, readings), + _ => lowering.term_as(text, want), + } +} + +/// Whether `request` fits `quantifier`, checked before any solver time is +/// spent: an instantiation names each variable once, by its own name or its +/// source name, and a trigger has terms. For an instantiation, the variable +/// each name means. +fn check_hypothesis( request: &HypothesisRequest, quantifier: &QuantifierSmt, - lowering: &Lowering, -) -> Result<(Hypothesis, HashMap), (&'static str, String)> { - let qid = quantifier.qid.clone(); + names: &[&SourceNames], +) -> Result, (&'static str, String)> { + let qid = &quantifier.qid; match request { HypothesisRequest::Instantiation { subst, .. } => { - let mut terms: HashMap = HashMap::new(); - for (name, text) in subst { - let Some(smt) = lowering.binders.get(name.as_str()) else { + let binders = binder_names(&quantifier.binders, names); + let mut meant: HashMap = HashMap::new(); + let mut seen: HashSet<&str> = HashSet::new(); + for name in subst.keys() { + let Some(smt) = binders.get(name.as_str()) else { let binders: Vec<&str> = quantifier.binders.iter().map(|(smt, _)| smt.as_str()).collect(); return Err(( @@ -2425,16 +2596,15 @@ fn lower_hypothesis( format!("{qid} binds no variable {name}; it binds {}", binders.join(", ")), )); }; - let sort = lowering.binder_sorts.get(smt).map(String::as_str); - let term = lowering.term_as(text, sort).map_err(|e| ("could_not_lower", e))?; - if terms.insert(smt.clone(), term).is_some() { + if !seen.insert(smt.as_str()) { return Err(("mismatch", format!("two terms for the variable {smt}"))); } + meant.insert(name.clone(), smt.clone()); } let missing: Vec = quantifier .binders .iter() - .filter(|(smt, _)| !terms.contains_key(smt)) + .filter(|(smt, _)| !seen.contains(smt.as_str())) .map(|(smt, sort)| format!("{smt} ({})", flat(sort))) .collect(); if !missing.is_empty() { @@ -2446,32 +2616,67 @@ fn lower_hypothesis( ), )); } + Ok(meant) + } + HypothesisRequest::TriggerPattern { pattern, .. } if pattern.terms().is_empty() => { + Err(("mismatch", "the pattern has no terms".to_string())) + } + HypothesisRequest::TriggerPattern { .. } | HypothesisRequest::BlockCycle { .. } => { + Ok(HashMap::new()) + } + } +} + +/// The hypothesis in the solver's spelling, for an instantiation its term +/// for each variable, and how names were read where several readings were +/// possible; or why it cannot be sent. `meant` is `check_hypothesis`'s. +fn lower_hypothesis( + request: &HypothesisRequest, + quantifier: &QuantifierSmt, + meant: &HashMap, + lowering: &Lowering, + reader: Option<&VerusReader>, +) -> Result<(Hypothesis, HashMap, Vec), (&'static str, String)> { + let qid = quantifier.qid.clone(); + let mut readings = Vec::new(); + match request { + HypothesisRequest::Instantiation { subst, .. } => { + let mut terms: HashMap = HashMap::new(); + for (name, text) in subst { + let smt = &meant[name]; + let sort = quantifier.binders.iter().find(|(v, _)| v == smt).map(|(_, s)| flat(s)); + let term = read_term(text, sort.as_deref(), lowering, reader, &mut readings) + .map_err(|e| ("could_not_lower", e))?; + terms.insert(smt.clone(), term); + } let subst = quantifier .binders .iter() .map(|(smt, _)| (smt.clone(), flat(&terms[smt]))) .collect(); - Ok((Hypothesis::Instantiate { qid, subst }, terms)) + Ok((Hypothesis::Instantiate { qid, subst }, terms, readings)) } HypothesisRequest::TriggerPattern { pattern, .. } => { let pattern: Vec = pattern .terms() .into_iter() - .map(|term| lowering.term_as(term, None).map(|node| flat(&node))) + .map(|term| { + read_term(term, None, lowering, reader, &mut readings).map(|node| flat(&node)) + }) .collect::>() .map_err(|e| ("could_not_lower", e))?; - if pattern.is_empty() { - return Err(("mismatch", "the pattern has no terms".to_string())); - } Ok(( Hypothesis::Trigger { qid, vars: quantifier.binders.clone(), pattern }, HashMap::new(), + readings, )) } HypothesisRequest::BlockCycle { fingerprint, .. } => { + // A fingerprint's holes are no Verus, so it is read as SMT or in + // the small surface syntax `surface_term` reads. let fingerprint = flat(&lowering.term_as(fingerprint, None).map_err(|e| ("could_not_lower", e))?); - Ok((Hypothesis::Block { qid, fingerprint }, HashMap::new())) + Ok((Hypothesis::Block { qid, fingerprint }, HashMap::new(), readings)) } } } @@ -2602,15 +2807,16 @@ fn speculation_run( } /// Check a retained query with `hypothesis` in its scope, and read what cvc5 -/// reported about it. Rounds for further errors are not run, and nothing is -/// saved as a certificate. The caller has restored the query's prefix. +/// reported about it, and the goal it failed at, if it names one. Rounds for +/// further errors are not run, and nothing is saved as a certificate. The +/// caller has restored the query's prefix. fn speculation_check( air: &mut Context, query: &RetainedQuery, hypothesis: Hypothesis, loop_threshold: Option, set_rlimit: &impl Fn(&mut Context, f32), -) -> io::Result<(QueryResult, u128, SpeculationReply)> { +) -> io::Result<(QueryResult, u128, SpeculationReply, Option)> { set_rlimit(air, query.rlimit); air.set_speculation(Some(SpeculationRequest { hypothesis, loop_threshold })); let start = Instant::now(); @@ -2629,10 +2835,10 @@ fn speculation_check( drop(air.take_matching_loops()); drop(air.take_difficulty()); drop(air.take_inst_pressure()); - let result = match outcome { - ValidityResult::Valid(_) => QueryResult::Valid, - ValidityResult::Invalid(..) => QueryResult::Invalid, - ValidityResult::Canceled => QueryResult::ResourceLimit, + let (result, failed_at) = match outcome { + ValidityResult::Valid(_) => (QueryResult::Valid, None), + ValidityResult::Invalid(_, _, id) => (QueryResult::Invalid, id), + ValidityResult::Canceled => (QueryResult::ResourceLimit, None), ValidityResult::TypeError(error) => return Err(io::Error::other(error.to_string())), ValidityResult::UnexpectedOutput(error) => return Err(io::Error::other(error)), }; @@ -2641,7 +2847,7 @@ fn speculation_check( unparsed: Some("the check did not reach check-sat".to_owned()), ..SpeculationReply::default() }); - Ok((result, elapsed_ms, reply)) + Ok((result, elapsed_ms, reply, failed_at)) } /// cvc5's `(error "...")` as its message. @@ -2727,8 +2933,8 @@ fn serve_speculate( (listed, note) }; - // The quantifier the hypothesis names, and the hypothesis in the - // solver's spelling, or why nothing will be checked. + // The quantifier the hypothesis names, and what its names mean, or why + // nothing will be checked. let mut target = None; if let Some(request) = &hypothesis { let Some(quantifier) = @@ -2746,13 +2952,8 @@ fn serve_speculate( return Ok(Ok(outcome)); }; outcome.quantifier = Some(describe_quantifier(&quantifier, symbols, &unversioned)); - let lowering = Lowering::new( - &quantifier, - Declarations::of(&decls, &query.query), - &[&unversioned.shown, &unversioned.plain], - ); - match lower_hypothesis(request, &quantifier, &lowering) { - Ok((lowered, subst)) => target = Some((quantifier, lowered, subst)), + match check_hypothesis(request, &quantifier, &[&unversioned.shown, &unversioned.plain]) { + Ok(meant) => target = Some((request, quantifier, meant)), Err((status, reason)) => { outcome.status = Some(status.to_owned()); outcome.notes = format!("Nothing was checked: {reason}."); @@ -2763,13 +2964,13 @@ fn serve_speculate( } } - let (before_result, before_ms, before_reply) = + let (before_result, before_ms, before_reply, failed_at) = speculation_check(air, query, Hypothesis::Observe, loop_threshold, set_rlimit)?; let before = speculation_run(before_result, before_ms, &before_reply, symbols); let before_loops: HashSet = before.loops.iter().map(|l| l.qid.clone()).collect(); let before_loop_count = before.loops.len(); outcome.before = Some(before); - let Some((quantifier, lowered, subst)) = target else { + let Some((request, quantifier, meant)) = target else { let (listed, note) = candidates(air); outcome.candidates = listed; outcome.notes = format!( @@ -2780,7 +2981,66 @@ fn serve_speculate( return Ok(Ok(outcome)); }; - let (after_result, after_ms, after_reply) = + // The terms are read at the goal the check failed at (the query's last + // goal when it names none), where each mutable local holds the version + // a pasted snippet will see. + let goal = air::GoalScope::of(&query.query, failed_at.as_ref()); + let live = goal.live(); + let lowered = { + let context: &Context = air; + let declared = |name: &str| context.declared(name); + // A trigger's terms are over the quantifier's variables; the other + // hypotheses' terms stand outside it. + let binders: &[(String, TreeNode)] = match request { + HypothesisRequest::TriggerPattern { .. } => &quantifier.binders, + _ => &[], + }; + let lowering = Lowering::new( + binders, + Declarations::of(&decls, &query.query, live.clone(), &before_reply.variable_versions), + &[&unversioned.shown, &unversioned.plain], + &declared, + ); + let occurrences = air::scaffold::occurrences(&query.query); + let reader = symbols.map(|symbols| VerusReader { + env: crate::scaffold::Env { + names: symbols.source_names(), + crate_name: symbols.crate_name(), + locals: query_locals(&query.query), + bound: binders + .iter() + .map(|(smt, sort)| (std::sync::Arc::new(smt.clone()), typ_of_sort(&flat(sort)))) + .collect(), + declared: &declared, + occurrences: &occurrences, + }, + goal: &goal, + printer: air::printer::Printer::new( + std::sync::Arc::new(VirMessageInterface {}), + true, + SmtSolver::Cvc5, + ), + }); + lower_hypothesis(request, &quantifier, &meant, &lowering, reader.as_ref()) + }; + let (lowered, subst) = match lowered { + Ok((lowered, subst, readings)) => { + outcome.readings = readings; + (lowered, subst) + } + Err((status, reason)) => { + outcome.status = Some(status.to_owned()); + outcome.notes = format!( + "The query was checked as usual and answers {}, but not with the hypothesis: {reason}.", + result_name(before_result) + ); + outcome.reason = Some(reason); + outcome.elapsed_ms = start.elapsed().as_millis(); + return Ok(Ok(outcome)); + } + }; + + let (after_result, after_ms, after_reply, _) = speculation_check(air, query, lowered.clone(), loop_threshold, set_rlimit)?; if let Some(error) = &after_reply.error { outcome.status = Some("could_not_lower".to_owned()); @@ -2803,15 +3063,16 @@ fn serve_speculate( // own, so a close counts only if the query still fails right after. let mut closed = before_result != QueryResult::Valid && after_result == QueryResult::Valid; if closed { - let (result, elapsed_ms, reply) = + let (result, elapsed_ms, reply, _) = speculation_check(air, query, Hypothesis::Observe, loop_threshold, set_rlimit)?; closed = result != QueryResult::Valid; outcome.recheck = Some(speculation_run(result, elapsed_ms, &reply, symbols)); } outcome.closed = closed; - // Source for the check's terms, SSA versions included. - let names = QueryNames::new(symbols, &after_reply.variable_versions, &empty); + // Source for the check's terms, SSA versions included, to paste at the + // goal the terms were read at. + let names = QueryNames::new(symbols, &after_reply.variable_versions, &empty).at(&live); if !matches!(lowered, Hypothesis::Block { .. }) { outcome.new_provenance = Some(NewProvenance { closing_instantiations: report @@ -3316,17 +3577,7 @@ fn scaffold_arms( } // Read P before any check, so a refusal costs no solver time. let occurrences = air::scaffold::occurrences(&query.query); - let locals: Vec<_> = query - .query - .local - .iter() - .filter_map(|decl| match &**decl { - air::ast::DeclX::Const(x, typ) | air::ast::DeclX::Var(x, typ) => { - Some((x.clone(), typ.clone())) - } - _ => None, - }) - .collect(); + let locals = query_locals(&query.query); let lowered = { let context: &Context = air; let declared = |name: &str| context.declared(name); @@ -3334,6 +3585,7 @@ fn scaffold_arms( names: symbols.source_names(), crate_name: symbols.crate_name(), locals, + bound: Vec::new(), declared: &declared, occurrences: &occurrences, }; @@ -5038,6 +5290,7 @@ mod tests { shown: Cow::Borrowed(&recorded), plain: Cow::Borrowed(&recorded), versions: &versions, + live: None, }; // Three classes, {a, b}, {c, d} and {e, f}; the second reading loses the last. let before = reading(&[("a", "b"), ("c", "d"), ("e", "f")]); @@ -5099,6 +5352,7 @@ mod tests { shown: Cow::Borrowed(&shown), plain: Cow::Borrowed(&plain), versions: &versions, + live: None, }; assert_eq!( names.verus_assert(&equality("z@1", "(+ x 1)", "entailed", &[])).as_deref(), @@ -5112,6 +5366,27 @@ mod tests { assert_eq!(names.verus_assert(&equality("z@1", "tmp", "entailed", &[])), None); } + /// Pasted where `z` holds its second version, an assert naming the first + /// would read as the second. + #[test] + fn pasted_asserts_name_variables_at_their_version_where_pasted() { + let (plain, shown, versions) = versioned_names(); + let live = HashMap::from([("z".to_string(), "z@1".to_string())]); + let names = QueryNames { + symbols: None, + shown: Cow::Borrowed(&shown), + plain: Cow::Borrowed(&plain), + versions: &versions, + live: None, + } + .at(&live); + assert_eq!( + names.verus_assert(&equality("z@1", "(+ x 1)", "entailed", &[])).as_deref(), + Some("assert(z == (x + 1));") + ); + assert_eq!(names.verus_assert(&equality("z@0", "(+ x 1)", "entailed", &[])), None); + } + #[test] fn differently_spelled_duplicates_merge_whichever_comes_first() { let (plain, shown, versions) = versioned_names(); @@ -5120,6 +5395,7 @@ mod tests { shown: Cow::Borrowed(&shown), plain: Cow::Borrowed(&plain), versions: &versions, + live: None, }; // The same equality in two spellings, as between a boxed and an // unboxed term; only the second has a quantifier instantiated with it. @@ -5184,7 +5460,8 @@ mod tests { for (symbol, name) in [("a!", "a"), ("i$", "i"), ("m!f.", "m::f"), ("m!s.", "m::s")] { names.insert(symbol.to_owned(), vir::air_names::SourceName::Symbol(name.to_owned())); } - let lowering = Lowering::new(&quantifier, declared, &[&names]); + let nothing = |_: &str| None; + let lowering = Lowering::new(&quantifier.binders, declared, &[&names], ¬hing); let lower = |text: &str, want: Option<&str>| flat(&lowering.term_as(text, want).unwrap()); assert_eq!(lower("a", Some(POLY)), "(I a!)"); assert_eq!(lower("a + 1", Some(POLY)), "(I (+ a! 1))"); @@ -5196,6 +5473,63 @@ mod tests { assert_eq!(lower("(m!f.? (I a!))", Some("Int")), "(m!f.? (I a!))"); } + /// Terms that stand outside the quantifier never name its variables; a + /// mutable local reads as its symbol at the goal; the prelude's + /// functions come from the AIR context; and SMT spelling is told apart + /// from Verus. + #[test] + fn lowering_reads_ground_terms_at_the_goal() { + let int = || std::sync::Arc::new(air::ast::TypX::Int); + let quantifier_binders = vec![("i$".to_owned(), parse_term("Poly").unwrap())]; + let mut declared = Declarations { + live: HashMap::from([("y@".to_owned(), "y@1".to_owned())]), + ..Declarations::default() + }; + for (constant, sort) in [("i!", "Int"), ("a!", "Int"), ("y@", "Int"), ("y@1", "Int")] { + declared.constants.insert(constant.to_owned(), sort.to_owned()); + } + let mut names = SourceNames::new(); + for (symbol, name) in [("i!", "i"), ("i$", "i"), ("a!", "a"), ("y@", "y")] { + names.insert(symbol.to_owned(), vir::air_names::SourceName::Symbol(name.to_owned())); + } + let context = |name: &str| match name { + "Add" => { + Some(air::context::Declared::Fun(std::sync::Arc::new(vec![int(), int()]), int())) + } + "I" => Some(air::context::Declared::Fun( + std::sync::Arc::new(vec![int()]), + typ_of_sort(POLY), + )), + _ => None, + }; + // an instantiation's terms: `i` is the parameter, not the variable + let ground = Lowering::new(&[], declared, &[&names], &context); + let lower = |text: &str| flat(&ground.term_as(text, Some(POLY)).unwrap()); + assert_eq!(lower("i"), "(I i!)"); + assert_eq!(lower("y"), "(I y@1)"); + assert_eq!(lower("y@"), "(I y@1)"); + assert_eq!(lower("(Add a! 1)"), "(I (Add a! 1))"); + // SMT spelling or Verus + for (text, verus) in [ + ("a + 1", true), + ("(a + 1)", true), + ("s.len() - 1", true), + ("i", true), + ("(Add a! 1)", false), + ("i!", false), + ("y@1", false), + ("$", false), + ("(= a! 1)", false), + ] { + assert_eq!(ground.reads_as_verus(text), verus, "{text}"); + } + // a trigger's terms: `i` is the variable + let mut declared = Declarations::default(); + declared.constants.insert("i!".to_owned(), "Int".to_owned()); + let over = Lowering::new(&quantifier_binders, declared, &[&names], &context); + assert_eq!(flat(&over.term_as("i", None).unwrap()), "i$"); + } + #[test] fn type_guards_are_dropped_from_an_instance() { let node = |text: &str| parse_term(text).unwrap(); diff --git a/source/rust_verify/src/scaffold.rs b/source/rust_verify/src/scaffold.rs index 3b58648bef..e5c3eb442d 100644 --- a/source/rust_verify/src/scaffold.rs +++ b/source/rust_verify/src/scaffold.rs @@ -468,6 +468,9 @@ pub(crate) struct Env<'a> { pub crate_name: &'a str, /// The query's local constants and variables, with their sorts. pub locals: Vec<(Ident, Typ)>, + /// Variables bound around the text (a quantifier's), with their sorts, + /// which shadow the locals of the same source name. + pub bound: Vec<(Ident, Typ)>, /// What the solver context has declared a global name as. pub declared: &'a dyn Fn(&str) -> Option, /// What the query's own text uses. @@ -494,6 +497,23 @@ pub(crate) fn lower(text: &str, env: &Env) -> Result { Ok(Lowered { expr, choices }) } +/// A term written as Verus source, read as `lower` reads an assertion, and +/// boxed or unboxed to `want` when that is given. +pub(crate) fn lower_term(text: &str, env: &Env, want: Option<&Typ>) -> Result { + let ast = parse(text)?; + let mut lowerer = Lowerer { env, choices: Vec::new() }; + let (expr, typ) = lowerer.lower(&ast)?; + let expr = match want { + Some(want) => lowerer.coerce(expr, &typ, want).map_err(|_| { + format!("the term is a {}, where a {} is wanted", sort_name(&typ), sort_name(want)) + })?, + None => expr, + }; + let mut seen = std::collections::HashSet::new(); + let choices = lowerer.choices.into_iter().filter(|c| seen.insert(c.clone())).collect(); + Ok(Lowered { expr, choices }) +} + fn sort_name(typ: &Typ) -> String { match &**typ { TypX::Bool => "bool".to_owned(), @@ -789,6 +809,17 @@ impl<'e, 'a> Lowerer<'e, 'a> { /// The local `name` names: its recorded source name is `name`, or `name` /// with a binding number when shadowing renumbered it. fn local(&mut self, name: &str) -> Option<(Ident, Typ)> { + for (x, typ) in &self.env.bound { + let recorded = self + .env + .names + .get(&**x) + .map(|n| n.name().to_owned()) + .or_else(|| source_symbol(self.env.names, x)); + if **x == name || recorded.as_deref() == Some(name) { + return Some((x.clone(), typ.clone())); + } + } let binding = format!("{name} (binding "); let mut found: Vec<(u64, bool, &(Ident, Typ))> = Vec::new(); for local in &self.env.locals { @@ -1541,6 +1572,7 @@ mod tests { names: &names, crate_name: "k", locals, + bound: Vec::new(), declared: &declared, occurrences: &occurrences, }; @@ -1650,6 +1682,7 @@ mod tests { names: &names, crate_name: "k", locals, + bound: Vec::new(), declared: &declared, occurrences: &occurrences, }; @@ -1688,8 +1721,14 @@ mod tests { // a generic function applied nowhere in the query let (names, locals, _) = env_parts(); let none = Occurrences::default(); - let env = - Env { names: &names, crate_name: "k", locals, declared: &declared, occurrences: &none }; + let env = Env { + names: &names, + crate_name: "k", + locals, + bound: Vec::new(), + declared: &declared, + occurrences: &none, + }; let error = lower("Seq::len(v) > 0", &env).err().unwrap(); assert!(error.contains("never applies"), "{error}"); let _ = HashMap::<(), ()>::new(); diff --git a/source/rust_verify_test/tests/resident.rs b/source/rust_verify_test/tests/resident.rs index 69396b129c..f1e9a4a358 100644 --- a/source/rust_verify_test/tests/resident.rs +++ b/source/rust_verify_test/tests/resident.rs @@ -1765,6 +1765,128 @@ fn resident_scaffold_says_why_under_provenance() { worker.finish(false); } +const SPECULATE_GOAL_SOURCE: &str = r#" +use vstd::prelude::*; +verus! { + spec fn f(x: int) -> int; + spec fn g(x: int) -> int; + + proof fn shadowed(i: int) + requires forall|i: int| #![trigger g(i)] g(i) > 0 && f(i) > 0, + { + assert(f(i) > 0); + } + + proof fn reassigned(a: int) + requires forall|i: int| #![trigger g(i)] g(i) > 0 && f(i) > 0, + { + let mut y = a; + y = y + 1; + assert(f(y) > 0); + } + + proof fn last_of(s: Seq) + requires s.len() > 0, forall|i: int| #![trigger g(i)] 0 <= i < s.len() ==> s[i] > 0, + { + assert(s[s.len() - 1] > 0); + } +} +"#; + +/// The options for a cvc5 build whose version differs from the pinned +/// release, without `speculate_options`' small budget. +fn version_options() -> Vec<&'static str> { + match std::env::var_os("RESIDENT_NO_SOLVER_VERSION_CHECK") { + Some(_) => vec!["-V", "no-solver-version-check"], + None => Vec::new(), + } +} + +/// A probe of the quantifier in `function`'s own query. +fn probe_own( + worker: &mut Worker, + ready: &Value, + function: &str, + hypothesis: impl FnOnce(&Value) -> Value, +) -> Value { + let session = ready["session"].clone(); + let query = query_id(ready, function); + let qid = own_quantifier(worker, &session, &query)["qid"].clone(); + probe(worker, &session, &query, Some(hypothesis(&qid))) +} + +/// `function`'s check in a fresh worker on `source`. +fn cold_check(source: &str, function: &str, options: &[&str]) -> Value { + let mut worker = Worker::start(source, options); + let ready = worker.receive(); + let checked = worker.send(json!({"command": "check", "session": ready["session"], + "bucket": 0, "query": query_id(&ready, function)})); + worker.send(json!({"command": "close", "session": ready["session"]})); + worker.finish(false); + checked +} + +/// A hypothesis's terms are read at the goal the query fails at. An +/// instantiation's never name the quantifier's own variable, so a parameter +/// it shadows is the parameter; a mutable local reads as its value there; +/// Verus method calls and the prelude's arithmetic in SMT spelling are +/// read; and a snippet names no variable at another version than the +/// goal's, so pasted before the goal it verifies. +#[test] +#[ignore = "needs cvc5 with (speculate ...) (BasisResearch/cvc5 kg/speculative-probe); un-ignore when the pin moves"] +fn resident_speculate_reads_terms_at_the_goal() { + let options = version_options(); + let mut worker = Worker::start(SPECULATE_GOAL_SOURCE, &options); + let ready = worker.receive(); + assert_eq!(ready["event"], "ready", "{ready}"); + let instantiation = + |subst: Value| move |qid: &Value| json!({"instantiation": {"qid": qid, "subst": subst}}); + + let shadowed = probe_own(&mut worker, &ready, "::shadowed", instantiation(json!({"i": "i"}))); + assert_eq!(shadowed["closed"], true, "{shadowed}"); + assert!(shadowed["verus_snippet"].as_str().unwrap().contains("crate::f(i)"), "{}", shadowed); + + let local = probe_own(&mut worker, &ready, "::reassigned", instantiation(json!({"i": "y"}))); + assert_eq!(local["status"], "applied", "{local}"); + assert_eq!(local["closed"], true, "{local}"); + let pasted = local["verus_snippet"].as_str().unwrap(); + assert!(pasted.contains("crate::f(y)"), "{}", local); + let source = SPECULATE_GOAL_SOURCE + .replace("assert(f(y) > 0);", &format!("{pasted}\n assert(f(y) > 0);")); + assert_eq!(cold_check(&source, "::reassigned", &options)["result"], "valid"); + + let spelled = + probe_own(&mut worker, &ready, "::reassigned", instantiation(json!({"i": "(Add a! 1)"}))); + assert_eq!(spelled["closed"], true, "{spelled}"); + + // The trigger matches the goal's term as cvc5 holds it, over the first + // version of `y`; an assert of it could only paste as a claim about + // the second, so it is offered only when it names none. + let triggered = probe_own( + &mut worker, + &ready, + "::reassigned", + |qid| json!({"trigger_pattern": {"qid": qid, "pattern": "f(i)"}}), + ); + assert_eq!(triggered["closed"], true, "{triggered}"); + if let Some(fallback) = triggered["fallback_snippet"].as_str() { + let source = SPECULATE_GOAL_SOURCE + .replace("assert(f(y) > 0);", &format!("{fallback}\n assert(f(y) > 0);")); + assert_eq!(cold_check(&source, "::reassigned", &options)["result"], "valid", "{fallback}"); + } + + let method = + probe_own(&mut worker, &ready, "::last_of", instantiation(json!({"i": "s.len() - 1"}))); + assert_eq!(method["status"], "applied", "{method}"); + assert_eq!(method["closed"], true, "{method}"); + + assert_eq!( + worker.send(json!({"command": "close", "session": ready["session"]}))["event"], + "closed" + ); + worker.finish(false); +} + /// With instantiation replay, every resident check that proves its query /// saves its instantiations, and a recheck of a query with saved ones first /// tries them alone (`:only`), falling back to the ordinary check unless that From f553280b82fcf5055c0d2e9490caf5dacc926860 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Tue, 15 Sep 2026 15:36:24 -0400 Subject: [PATCH 4/6] Speculate: send an instance without the variables cvc5 eliminated cvc5 eliminates a variable an equality in a formula's body fixes, and the formula it holds then binds the rest; since da4b2b0073 it keeps the :qid, and answers an instantiation that names the eliminated variable with mismatch. The resident now sends the instance again without each variable cvc5 reports unbound, lists them in eliminated, and offers as the snippet the instance cvc5 made, since the requested term for an eliminated variable need not be the one its equality fixes. A trigger's fallback is built only when its terms line up with the variables. A no_quantifier answer for a formula the scope asserts now says why: cvc5 registers alpha-equivalent formulas once, under the first qid. The status docs name the fourth rejected reason (the instance simplifies to true) and what pending means since 47d666d. Co-Authored-By: Claude Opus 5 (1M context) --- source/air/src/speculate.rs | 10 ++- source/rust_verify/src/resident.rs | 83 ++++++++++++++++++++--- source/rust_verify_test/tests/resident.rs | 21 ++++++ 3 files changed, 102 insertions(+), 12 deletions(-) diff --git a/source/air/src/speculate.rs b/source/air/src/speculate.rs index 83e3645a50..f5949fc81e 100644 --- a/source/air/src/speculate.rs +++ b/source/air/src/speculate.rs @@ -94,9 +94,13 @@ pub struct HypothesisReport { pub kind: String, pub qid: String, /// `applied`, `rejected` (the instantiation funnel refused the directed - /// instance), `mismatch` (the variables do not fit), `unusable` (the - /// pattern cannot be a trigger), `no-quantifier` or `pending` (no - /// instantiation round ran) + /// instance: it was made already, it is a lemma already sent, it + /// simplifies to true, or the instantiation level limit refused a term), + /// `mismatch` (the variables do not fit), `unusable` (the pattern cannot + /// be a trigger), `no-quantifier` (applied, but no asserted formula has + /// the qid) or `pending` (no instantiation round reached e-matching, for + /// instance because conflict-based instantiation closed every check + /// first) pub status: String, pub reason: Option, /// how many asserted quantifiers have the qid diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index d5a293407f..347b135062 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -1754,6 +1754,10 @@ fn serve_egraph( Ok(Ok(EgraphOutcome { before, summary, equalities, injection })) } +/// How cvc5 begins the `mismatch` reason for a variable its formula no +/// longer binds. +const UNBOUND_VARIABLE: &str = "the formula binds no variable named "; + /// The most rounds of rising depth a probe may ask to make a matching loop. const MAX_LOOP_THRESHOLD: u32 = 1000; /// The most quantifiers a probe lists as candidates. @@ -1912,12 +1916,15 @@ struct SpeculationOutcome { #[serde(skip_serializing_if = "Option::is_none")] after: Option, /// `applied`; `rejected` (the instantiation funnel refused the directed - /// instance: it was made already, it is a lemma already sent, or the - /// instantiation level limit refused a term; `reason` says which); - /// `mismatch` (the terms do not fit the variables); `unusable` (the - /// pattern cannot be a trigger); `no_quantifier`; `could_not_lower` (a - /// term that cannot be read in the query's scope, or that the solver - /// cannot read); `pending` (no instantiation round ran) + /// instance: it was made already, it is a lemma already sent, it + /// simplifies to true, or the instantiation level limit refused a term; + /// `reason` says which); `mismatch` (the terms do not fit the + /// variables); `unusable` (the pattern cannot be a trigger); + /// `no_quantifier` (cvc5 holds no formula with the qid, see `notes`); + /// `could_not_lower` (a term that cannot be read in the query's scope, + /// or that the solver cannot read); `pending` (no instantiation round + /// reached e-matching, for instance because conflict-based + /// instantiation closed every check first) #[serde(skip_serializing_if = "Option::is_none")] status: Option, #[serde(skip_serializing_if = "Option::is_none")] @@ -1960,6 +1967,11 @@ struct SpeculationOutcome { /// one reading was possible. #[serde(skip_serializing_if = "Vec::is_empty")] readings: Vec, + /// Variables of the quantifier that cvc5 eliminated before the search + /// (an equality in its body fixes each), so the formula it holds no + /// longer binds them; the directed instance was sent without them. + #[serde(skip_serializing_if = "Vec::is_empty")] + eliminated: Vec, caveat: &'static str, elapsed_ms: u128, restore_ms: u128, @@ -1988,6 +2000,7 @@ impl SpeculationOutcome { notes: String::new(), candidates: Vec::new(), readings: Vec::new(), + eliminated: Vec::new(), caveat: SPECULATION_CAVEAT, elapsed_ms: 0, restore_ms: 0, @@ -3040,8 +3053,35 @@ fn serve_speculate( } }; - let (after_result, after_ms, after_reply, _) = - speculation_check(air, query, lowered.clone(), loop_threshold, set_rlimit)?; + // cvc5 eliminates a variable an equality in the formula's body fixes + // (`x == y ==> ...`), and the formula it holds then no longer binds it. + // An instantiation that names one is sent again without it: the + // instance cvc5 makes is the rest's, with the equality's term for it. + let mut lowered = lowered; + let mut eliminated_smt: Vec = Vec::new(); + let (after_result, after_ms, after_reply) = loop { + let (result, ms, reply, _) = + speculation_check(air, query, lowered.clone(), loop_threshold, set_rlimit)?; + let unbound = reply + .hypotheses + .iter() + .find(|h| h.kind == "instantiate" && h.status == "mismatch") + .and_then(|h| h.reason.as_deref()?.strip_prefix(UNBOUND_VARIABLE)) + .map(str::to_owned); + match (&mut lowered, unbound) { + (Hypothesis::Instantiate { subst, .. }, Some(name)) + if subst.len() > 1 && subst.iter().any(|(v, _)| *v == name) => + { + subst.retain(|(v, _)| *v != name); + eliminated_smt.push(name); + } + _ => break (result, ms, reply), + } + }; + outcome.eliminated = eliminated_smt + .iter() + .map(|smt| vir::air_names::source_symbol(&unversioned.shown, smt).unwrap_or(smt.clone())) + .collect(); if let Some(error) = &after_reply.error { outcome.status = Some("could_not_lower".to_owned()); outcome.reason = Some(error_message(error)); @@ -3095,8 +3135,18 @@ fn serve_speculate( .unwrap_or_default(); match &lowered { Hypothesis::Instantiate { .. } => { - if closed { + if closed && eliminated_smt.is_empty() { outcome.verus_snippet = instance_assert(&quantifier, &subst, &names); + } else if closed { + // The requested term for an eliminated variable may not be + // the one its equality fixes, so the snippet is the instance + // cvc5 made, when that pastes. + outcome.verus_snippet = report.bodies.first().and_then(|body| { + let body = flat(&without_type_guards(&parse_term(body)?)); + names + .pasteable(&[&body]) + .then(|| format!("assert({});", names.render_plain(&body))) + }); } } Hypothesis::Trigger { pattern, .. } => { @@ -3111,6 +3161,11 @@ fn serve_speculate( // an instance the trigger made, asserted, which needs no // change to the quantifier outcome.fallback_snippet = report.instances.first().and_then(|terms| { + // after cvc5 eliminated a variable, the terms no longer + // line up with the quantifier's variables + if terms.len() != quantifier.binders.len() { + return None; + } let parsed: Option> = terms.iter().map(|term| parse_term(term)).collect(); let subst: HashMap = quantifier @@ -3154,12 +3209,22 @@ fn serve_speculate( "{} instantiation(s) matching the fingerprint were refused; the query answers {with} with the block and {without} without it.", report.blocked )), + ("no-quantifier", _) => notes.push(format!( + "cvc5 holds no formula with this qid, though the query's scope asserts it: cvc5 registers alpha-equivalent formulas once, under the first one's qid, and drops a formula that rewrites away. The query answers {with}." + )), (status, _) => notes.push(format!( "The hypothesis did not apply ({}{}); the query answers {with}.", status.replace('-', "_"), report.reason.as_deref().map(|r| format!(": {r}")).unwrap_or_default() )), } + if !outcome.eliminated.is_empty() { + notes.push(format!( + "cvc5 eliminated {} from the formula (an equality in its body fixes it), so the instance was sent without it{}.", + outcome.eliminated.join(", "), + if closed { "; the snippet asserts the instance cvc5 made" } else { "" } + )); + } match &outcome.recheck { Some(recheck) if recheck.result == QueryResult::Valid => notes.push( "Checked again without the hypothesis, the query passed: it is near its resource limit, so the close is not the hypothesis's and is not reported.".to_owned(), diff --git a/source/rust_verify_test/tests/resident.rs b/source/rust_verify_test/tests/resident.rs index 4894170eb4..8cf4932888 100644 --- a/source/rust_verify_test/tests/resident.rs +++ b/source/rust_verify_test/tests/resident.rs @@ -1842,6 +1842,15 @@ verus! { { assert(s[s.len() - 1] > 0); } + + spec fn p(x: A) -> bool; + spec fn r(x: A, y: A) -> bool; + + proof fn eliminated(a: A) + requires forall|x: A, y: A| #![trigger r(x, y)] x == y ==> p(x), + { + assert(p(a)); + } } "#; @@ -1932,6 +1941,18 @@ fn resident_speculate_reads_terms_at_the_goal() { assert_eq!(method["status"], "applied", "{method}"); assert_eq!(method["closed"], true, "{method}"); + // `x == y` lets cvc5 eliminate one of the variables; the instance goes + // without it, and a snippet offered is the instance cvc5 made. + let eliminated = + probe_own(&mut worker, &ready, "::eliminated", instantiation(json!({"x": "a", "y": "a"}))); + println!("eliminated: {eliminated}"); + assert_eq!(eliminated["closed"], true, "{eliminated}"); + if let Some(snippet) = eliminated["verus_snippet"].as_str() { + let source = SPECULATE_GOAL_SOURCE + .replace("assert(p(a));", &format!("{snippet}\n assert(p(a));")); + assert_eq!(cold_check(&source, "::eliminated", &options)["result"], "valid", "{snippet}"); + } + assert_eq!( worker.send(json!({"command": "close", "session": ready["session"]}))["event"], "closed" From 2ba14e615802a249049de6c85e8cb29b74d1a12e Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Tue, 15 Sep 2026 15:44:42 -0400 Subject: [PATCH 5/6] Test reading an eliminated variable from cvc5's refusal The Verus fixture's equality guard is between boxed values under type guards, and cvc5 keeps both of its variables, so the retry is covered by a unit test of unbound_variable; the fixture's comment says so. Co-Authored-By: Claude Opus 5 (1M context) --- source/rust_verify/src/resident.rs | 49 +++++++++++++++++++---- source/rust_verify_test/tests/resident.rs | 5 ++- 2 files changed, 45 insertions(+), 9 deletions(-) diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index eb9bcbe052..5313a8f120 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -2483,6 +2483,17 @@ fn serve_egraph( /// longer binds. const UNBOUND_VARIABLE: &str = "the formula binds no variable named "; +/// The variable an instantiation named that cvc5's formula no longer binds, +/// when cvc5 refused the instance for that. +fn unbound_variable(reply: &SpeculationReply) -> Option { + reply + .hypotheses + .iter() + .find(|h| h.kind == "instantiate" && h.status == "mismatch") + .and_then(|h| h.reason.as_deref()?.strip_prefix(UNBOUND_VARIABLE)) + .map(str::to_owned) +} + /// The most rounds of rising depth a probe may ask to make a matching loop. const MAX_LOOP_THRESHOLD: u32 = 1000; /// The most quantifiers a probe lists as candidates. @@ -3787,13 +3798,7 @@ fn serve_speculate( let (after_result, after_ms, after_reply) = loop { let (result, ms, reply, _) = speculation_check(air, query, lowered.clone(), loop_threshold, set_rlimit)?; - let unbound = reply - .hypotheses - .iter() - .find(|h| h.kind == "instantiate" && h.status == "mismatch") - .and_then(|h| h.reason.as_deref()?.strip_prefix(UNBOUND_VARIABLE)) - .map(str::to_owned); - match (&mut lowered, unbound) { + match (&mut lowered, unbound_variable(&reply)) { (Hypothesis::Instantiate { subst, .. }, Some(name)) if subst.len() > 1 && subst.iter().any(|(v, _)| *v == name) => { @@ -6366,6 +6371,36 @@ mod tests { assert_eq!(lower("(m!f.? (I a!))", Some("Int")), "(m!f.? (I a!))"); } + /// cvc5's refusal of an instance for a variable its formula no longer + /// binds names the variable to send the instance again without; no + /// other refusal does. + #[test] + fn an_eliminated_variable_is_read_from_the_refusal() { + let reply = |kind: &str, status: &str, reason: &str| SpeculationReply { + hypotheses: vec![ + air::speculate::HypothesisReport { kind: "observe".into(), ..Default::default() }, + air::speculate::HypothesisReport { + kind: kind.into(), + status: status.into(), + reason: Some(reason.into()), + ..Default::default() + }, + ], + ..Default::default() + }; + let unbound = format!("{UNBOUND_VARIABLE}y$"); + assert_eq!( + unbound_variable(&reply("instantiate", "mismatch", &unbound)).as_deref(), + Some("y$") + ); + assert_eq!( + unbound_variable(&reply("instantiate", "mismatch", "no term for the variable x$")), + None + ); + assert_eq!(unbound_variable(&reply("instantiate", "rejected", &unbound)), None); + assert_eq!(unbound_variable(&reply("trigger", "mismatch", &unbound)), None); + } + /// Terms that stand outside the quantifier never name its variables; a /// mutable local reads as its symbol at the goal; the prelude's /// functions come from the AIR context; and SMT spelling is told apart diff --git a/source/rust_verify_test/tests/resident.rs b/source/rust_verify_test/tests/resident.rs index 2f4f8c811d..95963f96e1 100644 --- a/source/rust_verify_test/tests/resident.rs +++ b/source/rust_verify_test/tests/resident.rs @@ -2392,11 +2392,12 @@ fn resident_speculate_reads_terms_at_the_goal() { assert_eq!(method["status"], "applied", "{method}"); assert_eq!(method["closed"], true, "{method}"); - // `x == y` lets cvc5 eliminate one of the variables; the instance goes + // A generic quantifier with an equality guard. cvc5 at da4b2b0073 keeps + // both variables of this one (the equality is between boxed values + // under type guards); where it eliminates one, the instance goes // without it, and a snippet offered is the instance cvc5 made. let eliminated = probe_own(&mut worker, &ready, "::eliminated", instantiation(json!({"x": "a", "y": "a"}))); - println!("eliminated: {eliminated}"); assert_eq!(eliminated["closed"], true, "{eliminated}"); if let Some(snippet) = eliminated["verus_snippet"].as_str() { let source = SPECULATE_GOAL_SOURCE From 8a07d6510b76f4f10b178335d496739f27ef398f Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Tue, 15 Sep 2026 16:20:35 -0400 Subject: [PATCH 6/6] Pin cvc5 to the release with (speculate ...), and run the speculate tests basis-e68dc63e37 is BasisResearch/cvc5 main at the merge of #14, which serves (speculate ...) and (get-info :speculation), and after #11, which reports :branch-profile. The two speculate tests are no longer ignored. Co-Authored-By: Claude Opus 5 (1M context) --- source/rust_verify_test/tests/resident.rs | 2 -- tools/common/solvers.toml | 22 ++++++++++++---------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/source/rust_verify_test/tests/resident.rs b/source/rust_verify_test/tests/resident.rs index 95963f96e1..c42664f14e 100644 --- a/source/rust_verify_test/tests/resident.rs +++ b/source/rust_verify_test/tests/resident.rs @@ -1655,7 +1655,6 @@ fn own_quantifier(worker: &mut Worker, session: &Value, query: & /// did before, and no probe launched a solver: the probes are the pasted /// source's differential check and the session's state check. #[test] -#[ignore = "needs cvc5 with (speculate ...) (BasisResearch/cvc5 kg/speculative-probe); un-ignore when the pin moves"] fn resident_speculate_probes_and_leaves_the_session_unchanged() { let options = speculate_options(); let mut worker = Worker::start(SPECULATE_SOURCE, &options); @@ -2345,7 +2344,6 @@ fn cold_check(source: &str, function: &str, options: &[&str]) -> Value { /// read; and a snippet names no variable at another version than the /// goal's, so pasted before the goal it verifies. #[test] -#[ignore = "needs cvc5 with (speculate ...) (BasisResearch/cvc5 kg/speculative-probe); un-ignore when the pin moves"] fn resident_speculate_reads_terms_at_the_goal() { let options = version_options(); let mut worker = Worker::start(SPECULATE_GOAL_SOURCE, &options); diff --git a/tools/common/solvers.toml b/tools/common/solvers.toml index 452338f0ed..6a2f88589c 100644 --- a/tools/common/solvers.toml +++ b/tools/common/solvers.toml @@ -29,22 +29,24 @@ asset_x86_linux = "z3-x86-linux" sha256_x86_linux = "99f5433928fa62adc3a19207d97b14111d62964e26b10b37d286f9e641e0dfbf" [cvc5] -# Fork `main` at 79e8830406: carries `:assert-id` provenance tags through +# Fork `main` at e68dc63e37: carries `:assert-id` provenance tags through # preprocessing, answers `(get-assertion-sources)`, saves, restores, exports # and imports quantifier instantiations (resident certificates), lists what # the e-graph holds after a check (`(get-egraph-equalities)`), reports # matching loops, per-quantifier instantiation pressure, per-assertion # difficulty, why a check gave up (`:incomplete-id`, its culprit # quantifiers), the nonlinear terms refinement could not settle -# (`:nl-frontier`) and what the last check-sat cost (`:check-effort`) -# through `(get-info ...)`, records the instantiation graph of a check -# (`--inst-graph`, `(get-instantiation-graph)`), and runs one quantifier -# instantiation strategy for a check-sat (`--quant-ladder`, -# `:quant-strategy`, `(get-info :strategy-rung)`). -version = "1.3.5.dev+main@79e8830" +# (`:nl-frontier`), what the last check-sat cost (`:check-effort`) and +# where its resources went (`:branch-profile`) through `(get-info ...)`, +# records the instantiation graph of a check (`--inst-graph`, +# `(get-instantiation-graph)`), runs one quantifier instantiation strategy +# for a check-sat (`--quant-ladder`, `:quant-strategy`, +# `(get-info :strategy-rung)`), and tests an instantiation hypothesis in +# one scope (`(speculate ...)`, `(get-info :speculation)`). +version = "1.3.5.dev+main@e68dc63" repo = "BasisResearch/cvc5" -tag = "basis-79e8830406" +tag = "basis-e68dc63e37" asset_arm64_macos = "cvc5-arm64-macos" -sha256_arm64_macos = "61138a1301b2a54b6ed03ada47a6b3b75d433d298c32fdbdd92edd00bfd1e957" +sha256_arm64_macos = "12a465c5f684e8b3a7170580047f6a66a517e86c10ea7dc484e74d0a3f78adc3" asset_x86_linux = "cvc5-x86-linux" -sha256_x86_linux = "e5c2b763c1d20e66fcc23f060b8bcc5c7372ec7afeb7d11ffdd394b7895b31c2" +sha256_x86_linux = "66aa2969667607a4852377cb39b1561b315aecd4045ab554f06e576fa95e3920"