diff --git a/source/air/src/context.rs b/source/air/src/context.rs index 9be7cf77c2..c18b6904be 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -650,6 +650,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 { @@ -746,6 +753,9 @@ impl Context { egraph_focus: None, last_egraph: None, inject_equality: None, + speculation: None, + last_speculation: None, + speculation_supported: None, branch_profile: false, last_branch_profile: None, solver, @@ -1198,6 +1208,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); @@ -1460,7 +1538,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 d6437dc260..81acd8d1b0 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; pub mod twin; #[macro_use] @@ -27,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 8b325db4fa..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, @@ -244,6 +247,22 @@ 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. 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"); let smt_init_start_time = std::time::Instant::now(); let smt_data = context.smt_log.take_pipe_data(); @@ -267,6 +286,10 @@ pub(crate) fn smt_check_assertion<'ctx>( ); } } + } 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( crate::messages::MessageLevel::Warning, @@ -277,6 +300,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); } @@ -327,6 +358,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.branch_profile { // in the same batch, right after the answer it describes context.smt_log.log_get_info("branch-profile"); @@ -398,6 +434,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; let mut branch_profile = None; let mut check_effort = None; let mut strategy_rung = None; @@ -435,6 +472,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 context.branch_profile && line.starts_with("(:branch-profile ") { branch_profile = Some(parse_branch_profile(&line)); } else if context.branch_profile && branch_profile.is_none() && line == "unsupported" { @@ -495,6 +534,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() + })); + } context.last_branch_profile = branch_profile; context.last_check_effort = check_effort; if egraph_asked { @@ -714,7 +760,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 == ')') => { @@ -824,7 +870,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)) } @@ -832,7 +878,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..f5949fc81e --- /dev/null +++ b/source/air/src/speculate.rs @@ -0,0 +1,536 @@ +//! 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: 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 + 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/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 df6d94bbfa..5313a8f120 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -34,6 +34,16 @@ //! 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. +//! //! An `ablate` request delta-debugs a retained query's axioms and hypotheses //! (see `air::bisect`). Its declaration-prefix axioms are asserted below the //! query's scope, so the solver's journal is popped back to the prelude and @@ -51,7 +61,7 @@ mod twin; 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, }; @@ -59,10 +69,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}; @@ -145,8 +157,8 @@ impl QueryKind { pub(crate) struct QueryJournal { /// The bucket's context from before the journal began (fuel constants, /// datatypes, function declarations, module-level broadcast groups). - /// Never replayed: it lives below every scope. Kept so a twin can find - /// what it declares. + /// Never replayed: it lives below every scope. Kept so a twin or a + /// speculative probe can find what it declares. base: Vec, contexts: Vec>, queries: Vec, @@ -172,6 +184,7 @@ const COMMANDS: &[&str] = &[ "inst_graph", "ladder", "twin", + "speculate", ]; #[derive(Deserialize)] @@ -238,6 +251,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, + }, /// Try a proposed assertion `P` at one goal of the query: is `P` /// provable there, and does the goal hold once `P` is assumed there /// (see `air::scaffold`). Each check runs in the query's own scope. @@ -739,6 +768,13 @@ enum Response<'a> { #[serde(flatten)] outcome: Box, }, + Speculated { + session: &'a str, + bucket: BucketIndex, + query: QueryId, + #[serde(flatten)] + outcome: Box, + }, Twin { session: &'a str, bucket: BucketIndex, @@ -2112,6 +2148,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> { @@ -2126,26 +2165,43 @@ 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, 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, 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 None; + return false; } // SSA symbols are plain SMT-LIB symbols, never quoted, so splitting // on parentheses and spaces finds every one. @@ -2153,15 +2209,19 @@ 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; + } + if self.live.and_then(|live| live.get(base)).is_some_and(|here| here != atom) { + 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. @@ -2378,7 +2438,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, @@ -2414,212 +2479,1715 @@ fn serve_egraph( Ok(Ok(EgraphOutcome { before, summary, equalities, injection })) } -/// What a scaffold request asks. -struct ScaffoldRequest { - assert: String, - assert_id: Option>, - goal: Option, - goal_only: bool, +/// 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 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) } -/// What one check cost, as cvc5's `(get-info :check-effort)` reported it. -#[derive(Clone, Copy, Serialize)] -struct CheckCost { - /// Resource units: the units of the query's rlimit budget. Not comparable - /// unit for unit between consecutive checks on one solver: cvc5's - /// rewriter and term caches survive `pop`, so a check after another of - /// like work spends fewer. - resource_units: u64, - instantiations: u64, - inst_rounds: u64, +/// 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 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 { + /// 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 }, } -/// One check of a scaffold request. +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 ScaffoldRun { +struct SpeculationRun { result: QueryResult, - /// The solver's reason for giving up (`incomplete`, `resourceout`, ...). - #[serde(skip_serializing_if = "Option::is_none")] - reason: Option, elapsed_ms: u128, - /// None from a cvc5 that does not report `:check-effort`. - cost: Option, - /// For the query's own check: how many checks followed it to find the - /// earliest failing goal, as Verus does before reporting one. Their - /// time and cost are not in this run's. + /// 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")] - rechecks: Option, + 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, } -/// The goal a scaffold request placed `P` before. #[derive(Serialize)] -struct ScaffoldTarget { - /// Empty for a goal Verus emits without an assert id (a loop invariant - /// at the end of the loop body, `decreases`); `goal` addresses it. - assert_id: Vec, - /// Its index among the query's asserts, which a request's `goal` names. - goal: usize, - /// `requested`; `first_failure`, the earliest goal the query's check - /// fails at, found as Verus finds the error it reports first; or - /// after a resource limit, which names no goal, `first_failing_alone`, - /// the first goal whose check alone failed. - chosen: &'static str, - /// How many goals were checked alone to find it. +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")] - goals_probed: Option, - /// The goal's error message, such as `assertion failed`. - description: String, span: Option, - labels: Vec, - /// How often the goal occurs; `P` is placed before each occurrence. - occurrences: usize, - /// The span `placement` refers to, when it refers to one: the goal's own; - /// for a postcondition at an early `return`, the return's ("at this - /// exit"); for one at the end of the body, the "end of the function body" - /// label's (the body's final expression, or with none the function). - insert_before: Option, - /// Where `assert(P);` goes in the source: `before_span`, right before - /// `insert_before` (a postcondition at an early `return` included); - /// `end_of_body`, at the end of the function body (a postcondition - /// checked there); `end_of_loop_body` or `before_loop` (a loop - /// invariant, checked there, which no span names); `end_of_proof_block` - /// (the claim of `assert ... by`, checked after that block's steps; a - /// goal among the steps is `before_span`). - placement: &'static str, + /// 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>, } -/// The goal's check with `P` assumed, less its check alone, run in that -/// order on the same solver. Instantiations are the steadier comparator: -/// resource units are not comparable between consecutive checks, since -/// cvc5's rewriter and term caches survive `pop`, so the later check of -/// like work spends fewer units and `rlimit_delta` reads low. #[derive(Serialize)] -struct MarginalCost { - instantiations_delta: i64, - /// In resource units, the units of the query's rlimit budget; biased low - /// by the caches the earlier checks warmed. - rlimit_delta: i64, +struct DirectedInstance { + qid: String, + terms: Vec, + smt_terms: Vec, + /// how cvc5 tags every instantiation a hypothesis made + inference_id: &'static str, } -/// What the goal's check under `P` drew on, from provenance: the hypotheses -/// that reached the solver in that check, and the quantifiers it -/// instantiated. Not an unsat core: the refutation need not have used every -/// one of them. #[derive(Serialize)] -struct ScaffoldWhy { - /// The hypotheses (`requires`, type invariants, ...) in the check. - explains_goal: Vec, - /// The quantifiers instantiated, those with a source span or defining a - /// function first, at most 12. - closing_quantifiers: Vec, - closing_quantifiers_omitted: usize, +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 ScaffoldReport { - target: ScaffoldTarget, - /// `P` as it was checked, rendered back from AIR as source. - lowered_as: String, - /// Names with more than one reading, and the reading taken. - choices: Vec, - /// The query's own check, run to find the goal when none was named. +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 funnel refused the directed + /// 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")] + 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")] - query_check: Option, - /// The goal alone: every other goal assumed, nothing added. - baseline: ScaffoldRun, - /// `P` asserted in place of the goal. Absent under `goal_only`. - p_provable: Option, - /// The goal with `P` assumed right before it. - goal_given_p: ScaffoldRun, - /// `scaffold`, `true_but_unhelpful`, `helpful_but_unprovable`, - /// `dead_end`, `goal_already_holds`, or under `goal_only` - /// `goal_closes_given_p` / `goal_open_given_p`. When a check the case - /// turns on runs out of budget, which proves nothing either way: - /// `helpful_but_undecided` (the goal closes under `P`; `P`'s check ran - /// out), `unhelpful_and_undecided` (the goal stays open under `P`; `P`'s - /// check ran out), `undecided` (the goal's check under `P` ran out), or - /// under `goal_only` `goal_undecided_given_p`. - case: &'static str, - marginal_cost: Option, - /// When the goal closed under `P` in a provenance session: what that - /// check had and instantiated, not a core. - why: Option, - /// Why the goal stayed open under `P`, when the solver gave up. - residual: Option, - /// `assert(P);` to add before `target.insert_before`, when the goal - /// closes under `P` (and `P` is provable, unless `goal_only`). verus_snippet: Option, - /// The solver's assertion stack before and after every check: equal, or - /// the session would have ended. - stack_levels: 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, + /// 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, + /// 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, } -struct ArmOutcome { - run: ScaffoldRun, - assert_id: Option>, - /// The failing goal's error message, which names a goal without an id. - error: Option, - provenance: Option, - unknown: Option, +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(), + readings: Vec::new(), + eliminated: Vec::new(), + caveat: SPECULATION_CAVEAT, + elapsed_ms: 0, + restore_ms: 0, + } + } } -/// Check `query` once in the retained query's scope and finish it. With -/// `earliest`, a failure is followed by checks for a failing goal before it, -/// as Verus runs them before reporting, until none is left: the goal named -/// is then the earliest failing one, not whichever the model showed first. -/// `Ok(Err)` is a refusal (the query did not type-check, so no scope was -/// opened). -fn scaffold_check( - air: &mut Context, - query: &Query, - rlimit: f32, - set_rlimit: &impl Fn(&mut Context, f32), - earliest: bool, -) -> io::Result> { - set_rlimit(air, rlimit); - let start = Instant::now(); - let outcome = air.check_valid( - &VirMessageInterface {}, - &QueryDiagnostics::default(), - query, - QueryContext::default(), - ); - let elapsed_ms = start.elapsed().as_millis(); - let provenance = air.take_provenance(); - let unknown = air.take_unknown_reason(); - let effort = air.take_check_effort(); - drop(air.take_matching_loops()); - drop(air.take_difficulty()); - drop(air.take_inst_pressure()); - drop(air.take_nl_frontier()); - let (result, mut assert_id, mut error, has_model) = match outcome { - ValidityResult::Valid(_) => (QueryResult::Valid, None, None, false), - ValidityResult::Invalid(model, error, id) => { - (QueryResult::Invalid, id.map(|id| (*id).clone()), error, model.is_some()) - } - ValidityResult::Canceled => (QueryResult::ResourceLimit, None, None, false), - // A query that fails to type-check opens no scope to finish. - ValidityResult::TypeError(error) => { - return Ok(Err(format!("AIR rejected the assertion as lowered: {error}"))); +/// 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(" ")) } - ValidityResult::UnexpectedOutput(error) => return Err(io::Error::other(error)), - }; - let mut rechecks = None; - // A recheck needs the model of the failure before it. - if earliest && has_model { - let mut count = 0; - loop { - count += 1; - let again = - air.check_valid_again(&QueryDiagnostics::default(), true, QueryContext::default()); - drop(air.take_provenance()); - drop(air.take_unknown_reason()); - drop(air.take_check_effort()); - drop(air.take_matching_loops()); - drop(air.take_difficulty()); - drop(air.take_inst_pressure()); + } +} + +/// `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 +/// (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, + 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) => { + 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(_) => {} + } + } + for (ssa, (variable, _)) in versions { + if let Some(sort) = out.constants.get(variable).cloned() { + out.constants.insert(ssa.clone(), sort); + } + } + out + } + + fn declares(&self, symbol: &str) -> bool { + self.constants.contains_key(symbol) || self.functions.contains_key(symbol) + } +} + +/// 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. 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%`). 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<'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 &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 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(target.clone()); + by_source.entry(source).or_default().insert(target); + } + } + 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()); + } + // 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) { + 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.function(&head).is_some().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.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, + }; + 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.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())) + } + "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 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, + names: &[&SourceNames], +) -> Result, (&'static str, String)> { + let qid = &quantifier.qid; + match request { + HypothesisRequest::Instantiation { subst, .. } => { + 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(( + "mismatch", + format!("{qid} binds no variable {name}; it binds {}", binders.join(", ")), + )); + }; + 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, _)| !seen.contains(smt.as_str())) + .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(", ") + ), + )); + } + 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, readings)) + } + HypothesisRequest::TriggerPattern { pattern, .. } => { + let pattern: Vec = pattern + .terms() + .into_iter() + .map(|term| { + read_term(term, None, lowering, reader, &mut readings).map(|node| flat(&node)) + }) + .collect::>() + .map_err(|e| ("could_not_lower", e))?; + 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(), readings)) + } + } +} + +/// `(=> 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, 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, Option)> { + 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, 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)), + }; + 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, failed_at)) +} + +/// 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; + // 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()) + }; + 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(); + 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 what its names mean, 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() + )); + 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)); + }; + outcome.quantifier = Some(describe_quantifier(&quantifier, symbols, &unversioned)); + 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}."); + outcome.reason = Some(reason); + outcome.elapsed_ms = start.elapsed().as_millis(); + return Ok(Ok(outcome)); + } + } + } + + 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((request, quantifier, meant)) = target else { + 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). {note}", + result_name(before_result) + ); + outcome.elapsed_ms = start.elapsed().as_millis(); + return Ok(Ok(outcome)); + }; + + // 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)); + } + }; + + // 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)?; + match (&mut lowered, unbound_variable(&reply)) { + (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)); + 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, 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 + .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 && 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, .. } => { + 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| { + // 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 + .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 + )), + ("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(), + ), + 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)) +} + +/// What a scaffold request asks. +struct ScaffoldRequest { + assert: String, + assert_id: Option>, + goal: Option, + goal_only: bool, +} + +/// What one check cost, as cvc5's `(get-info :check-effort)` reported it. +#[derive(Clone, Copy, Serialize)] +struct CheckCost { + /// Resource units: the units of the query's rlimit budget. Not comparable + /// unit for unit between consecutive checks on one solver: cvc5's + /// rewriter and term caches survive `pop`, so a check after another of + /// like work spends fewer. + resource_units: u64, + instantiations: u64, + inst_rounds: u64, +} + +/// One check of a scaffold request. +#[derive(Serialize)] +struct ScaffoldRun { + result: QueryResult, + /// The solver's reason for giving up (`incomplete`, `resourceout`, ...). + #[serde(skip_serializing_if = "Option::is_none")] + reason: Option, + elapsed_ms: u128, + /// None from a cvc5 that does not report `:check-effort`. + cost: Option, + /// For the query's own check: how many checks followed it to find the + /// earliest failing goal, as Verus does before reporting one. Their + /// time and cost are not in this run's. + #[serde(skip_serializing_if = "Option::is_none")] + rechecks: Option, +} + +/// The goal a scaffold request placed `P` before. +#[derive(Serialize)] +struct ScaffoldTarget { + /// Empty for a goal Verus emits without an assert id (a loop invariant + /// at the end of the loop body, `decreases`); `goal` addresses it. + assert_id: Vec, + /// Its index among the query's asserts, which a request's `goal` names. + goal: usize, + /// `requested`; `first_failure`, the earliest goal the query's check + /// fails at, found as Verus finds the error it reports first; or + /// after a resource limit, which names no goal, `first_failing_alone`, + /// the first goal whose check alone failed. + chosen: &'static str, + /// How many goals were checked alone to find it. + #[serde(skip_serializing_if = "Option::is_none")] + goals_probed: Option, + /// The goal's error message, such as `assertion failed`. + description: String, + span: Option, + labels: Vec, + /// How often the goal occurs; `P` is placed before each occurrence. + occurrences: usize, + /// The span `placement` refers to, when it refers to one: the goal's own; + /// for a postcondition at an early `return`, the return's ("at this + /// exit"); for one at the end of the body, the "end of the function body" + /// label's (the body's final expression, or with none the function). + insert_before: Option, + /// Where `assert(P);` goes in the source: `before_span`, right before + /// `insert_before` (a postcondition at an early `return` included); + /// `end_of_body`, at the end of the function body (a postcondition + /// checked there); `end_of_loop_body` or `before_loop` (a loop + /// invariant, checked there, which no span names); `end_of_proof_block` + /// (the claim of `assert ... by`, checked after that block's steps; a + /// goal among the steps is `before_span`). + placement: &'static str, +} + +/// The goal's check with `P` assumed, less its check alone, run in that +/// order on the same solver. Instantiations are the steadier comparator: +/// resource units are not comparable between consecutive checks, since +/// cvc5's rewriter and term caches survive `pop`, so the later check of +/// like work spends fewer units and `rlimit_delta` reads low. +#[derive(Serialize)] +struct MarginalCost { + instantiations_delta: i64, + /// In resource units, the units of the query's rlimit budget; biased low + /// by the caches the earlier checks warmed. + rlimit_delta: i64, +} + +/// What the goal's check under `P` drew on, from provenance: the hypotheses +/// that reached the solver in that check, and the quantifiers it +/// instantiated. Not an unsat core: the refutation need not have used every +/// one of them. +#[derive(Serialize)] +struct ScaffoldWhy { + /// The hypotheses (`requires`, type invariants, ...) in the check. + explains_goal: Vec, + /// The quantifiers instantiated, those with a source span or defining a + /// function first, at most 12. + closing_quantifiers: Vec, + closing_quantifiers_omitted: usize, +} + +#[derive(Serialize)] +struct ScaffoldReport { + target: ScaffoldTarget, + /// `P` as it was checked, rendered back from AIR as source. + lowered_as: String, + /// Names with more than one reading, and the reading taken. + choices: Vec, + /// The query's own check, run to find the goal when none was named. + #[serde(skip_serializing_if = "Option::is_none")] + query_check: Option, + /// The goal alone: every other goal assumed, nothing added. + baseline: ScaffoldRun, + /// `P` asserted in place of the goal. Absent under `goal_only`. + p_provable: Option, + /// The goal with `P` assumed right before it. + goal_given_p: ScaffoldRun, + /// `scaffold`, `true_but_unhelpful`, `helpful_but_unprovable`, + /// `dead_end`, `goal_already_holds`, or under `goal_only` + /// `goal_closes_given_p` / `goal_open_given_p`. When a check the case + /// turns on runs out of budget, which proves nothing either way: + /// `helpful_but_undecided` (the goal closes under `P`; `P`'s check ran + /// out), `unhelpful_and_undecided` (the goal stays open under `P`; `P`'s + /// check ran out), `undecided` (the goal's check under `P` ran out), or + /// under `goal_only` `goal_undecided_given_p`. + case: &'static str, + marginal_cost: Option, + /// When the goal closed under `P` in a provenance session: what that + /// check had and instantiated, not a core. + why: Option, + /// Why the goal stayed open under `P`, when the solver gave up. + residual: Option, + /// `assert(P);` to add before `target.insert_before`, when the goal + /// closes under `P` (and `P` is provable, unless `goal_only`). + verus_snippet: Option, + /// The solver's assertion stack before and after every check: equal, or + /// the session would have ended. + stack_levels: Option, + elapsed_ms: u128, + restore_ms: u128, +} + +struct ArmOutcome { + run: ScaffoldRun, + assert_id: Option>, + /// The failing goal's error message, which names a goal without an id. + error: Option, + provenance: Option, + unknown: Option, +} + +/// Check `query` once in the retained query's scope and finish it. With +/// `earliest`, a failure is followed by checks for a failing goal before it, +/// as Verus runs them before reporting, until none is left: the goal named +/// is then the earliest failing one, not whichever the model showed first. +/// `Ok(Err)` is a refusal (the query did not type-check, so no scope was +/// opened). +fn scaffold_check( + air: &mut Context, + query: &Query, + rlimit: f32, + set_rlimit: &impl Fn(&mut Context, f32), + earliest: bool, +) -> io::Result> { + set_rlimit(air, rlimit); + let start = Instant::now(); + let outcome = air.check_valid( + &VirMessageInterface {}, + &QueryDiagnostics::default(), + query, + QueryContext::default(), + ); + let elapsed_ms = start.elapsed().as_millis(); + let provenance = air.take_provenance(); + let unknown = air.take_unknown_reason(); + let effort = air.take_check_effort(); + drop(air.take_matching_loops()); + drop(air.take_difficulty()); + drop(air.take_inst_pressure()); + drop(air.take_nl_frontier()); + let (result, mut assert_id, mut error, has_model) = match outcome { + ValidityResult::Valid(_) => (QueryResult::Valid, None, None, false), + ValidityResult::Invalid(model, error, id) => { + (QueryResult::Invalid, id.map(|id| (*id).clone()), error, model.is_some()) + } + ValidityResult::Canceled => (QueryResult::ResourceLimit, None, None, false), + // A query that fails to type-check opens no scope to finish. + ValidityResult::TypeError(error) => { + return Ok(Err(format!("AIR rejected the assertion as lowered: {error}"))); + } + ValidityResult::UnexpectedOutput(error) => return Err(io::Error::other(error)), + }; + let mut rechecks = None; + // A recheck needs the model of the failure before it. + if earliest && has_model { + let mut count = 0; + loop { + count += 1; + let again = + air.check_valid_again(&QueryDiagnostics::default(), true, QueryContext::default()); + drop(air.take_provenance()); + drop(air.take_unknown_reason()); + drop(air.take_check_effort()); + drop(air.take_matching_loops()); + drop(air.take_difficulty()); + drop(air.take_inst_pressure()); drop(air.take_nl_frontier()); match again { ValidityResult::Invalid(model, again_error, id) => { @@ -2807,17 +4375,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); @@ -2825,6 +4383,7 @@ fn scaffold_arms( names: symbols.source_names(), crate_name: symbols.crate_name(), locals, + bound: Vec::new(), declared: &declared, occurrences: &occurrences, }; @@ -3497,6 +5056,7 @@ impl Server { | Request::Bisect { session: requested, .. } | Request::Ablate { session: requested, .. } | Request::Egraph { session: requested, .. } + | Request::Speculate { session: requested, .. } | Request::Scaffold { session: requested, .. } | Request::Close { session: requested } | Request::InstGraph { session: requested, .. } @@ -3700,6 +5260,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::Twin { bucket: bucket_id, query: id, edit, limit, recheck_base, .. } => { @@ -4590,6 +6188,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")]); @@ -4651,6 +6250,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(), @@ -4664,6 +6264,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(); @@ -4672,6 +6293,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. @@ -4689,6 +6311,168 @@ 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 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))"); + 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!))"); + } + + /// 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 + /// 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(); + 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/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 e430da9a6f..c42664f14e 100644 --- a/source/rust_verify_test/tests/resident.rs +++ b/source/rust_verify_test/tests/resident.rs @@ -1576,6 +1576,235 @@ 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] +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()); + } +} + const SCAFFOLD_SOURCE: &str = r#" use vstd::prelude::*; verus! { @@ -2038,6 +2267,149 @@ 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); + } + + 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)); + } +} +"#; + +/// 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] +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}"); + + // 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"}))); + 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" + ); + 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 @@ -2868,7 +3240,8 @@ fn resident_ready_lists_the_requests_it_serves() { "close", "inst_graph", "ladder", - "twin" + "twin", + "speculate" ], "{ready}" ); @@ -2877,7 +3250,7 @@ fn resident_ready_lists_the_requests_it_serves() { for command in &commands { let request = match command.as_str() { "list" | "close" => json!({"command": command, "session": "stale"}), - "check" | "egraph" | "ladder" => { + "check" | "egraph" | "ladder" | "speculate" => { json!({"command": command, "session": "stale", "bucket": 0, "query": 0}) } "bisect" => { 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"