From 8b174cdb1a155201d047d2b25230bb2d311cb1f9 Mon Sep 17 00:00:00 2001 From: Matthew Dwyer Date: Mon, 21 Sep 2026 12:43:52 -0400 Subject: [PATCH 1/7] verification observer: observation interface for the VIR->AIR->SMT lowering MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three observer traits each with default (no-op) methods let external tooling observe the verification pipeline without modifying Verus: - VirObserver (vir/src/vir_observer.rs): VIR->AIR lowering events — havoc, assign, branch/break merges, for-loops, quantifier and choose binders, reveal strings, function boundaries — and an optional assert-id supplier. - AirObserver (air/src/air_observer.rs): AIR passes — the lowered query (after variable versioning, before block-to-assert), version creation with its origin, lambda/choose/axiom declarations. - QueryResultObserver (air/src/query_result_observer.rs): the result of each solver call. On Invalid: the parsed counterexample model and a live boolean evaluator over the still-open solver model, plus the failing assert id. On Valid: the assert ids the query discharged and the solver's usage info (unsat core, when enabled). On Timeout: the assert id. Each trait has a single optional registration slot; when nothing is registered every hook is a no-op. The Invalid path is split so the solver model stays open through the callback; the label-disable step still runs afterwards with or without an observer. block_to_assert::lower_query is made pub so a consumer can apply the same final lowering the solver sees. Test infrastructure (test-only, behind --observers=): recording observers that emit an OBSERVER: note; a shared corpus of small programs each exercising a verification-condition (VC) shape (rust_verify_test/tests/vc_shapes); and an end-to-end suite that asserts expected values for callback payloads. In addition to coverage of VC shape, the test infrastructure varies loop-isolation settings, checks payload delivery on both valid and invalid verification results, and checks behavior neutrality by verifying every corpus program with and without observers by requiring identical outcomes. Assisted-by: kiro_cli:claude-fable-5 [Cherry-picked from verus-lang/verus#2965 (9bccfb486) onto the BasisResearch fork. Conflicts resolved against the fork's own changes: var_to_const::lower_query keeps the fork's version recording and goal scopes and takes the observer as a third argument; the failing-assertion label is still disabled after the Invalid callback, with the fork's three-argument log_assert; config.rs, the test harness and verifier.rs keep both sides' options and bucket teardown. One change to the PR's interface: observer handles are Arc> (the AirObserverHandle, QueryResultObserverHandle and VirObserverHandle aliases) and the traits require Send, instead of Rc>. The fork's resident sessions keep air::Context values in a Mutex served from other threads, so a Context holding an Rc does not compile here.] Co-Authored-By: Claude Opus 5.5 (1M context) --- source/air/src/air_observer.rs | 63 + source/air/src/ast.rs | 4 +- source/air/src/bisect.rs | 2 +- source/air/src/block_to_assert.rs | 7 +- source/air/src/closure.rs | 12 + source/air/src/context.rs | 63 +- source/air/src/lib.rs | 3 + source/air/src/query_result_observer.rs | 70 ++ source/air/src/smt_verify.rs | 65 +- source/air/src/var_to_const.rs | 61 +- source/rust_verify/src/config.rs | 9 + source/rust_verify/src/lib.rs | 1 + source/rust_verify/src/test_observer.rs | 609 ++++++++++ source/rust_verify/src/verifier.rs | 82 ++ source/rust_verify_test/tests/common/mod.rs | 11 + source/rust_verify_test/tests/observer.rs | 1062 +++++++++++++++++ .../rust_verify_test/tests/vc_shapes/mod.rs | 381 ++++++ source/vir/src/context.rs | 52 + source/vir/src/lib.rs | 1 + source/vir/src/sst_to_air.rs | 109 +- source/vir/src/vir_observer.rs | 179 +++ 21 files changed, 2810 insertions(+), 36 deletions(-) create mode 100644 source/air/src/air_observer.rs create mode 100644 source/air/src/query_result_observer.rs create mode 100644 source/rust_verify/src/test_observer.rs create mode 100644 source/rust_verify_test/tests/observer.rs create mode 100644 source/rust_verify_test/tests/vc_shapes/mod.rs create mode 100644 source/vir/src/vir_observer.rs diff --git a/source/air/src/air_observer.rs b/source/air/src/air_observer.rs new file mode 100644 index 0000000000..4685ce34ca --- /dev/null +++ b/source/air/src/air_observer.rs @@ -0,0 +1,63 @@ +//! AIR-level verification pipeline observer. +//! +//! Defines `AirObserver` — the interface for observing the AIR-level +//! verification pipeline: query lowering, WP version creation, and lambda / +//! choose / axiom declarations. +//! +//! This trait is independent: it does **not** require any other observer +//! trait. Query *results* are observed separately via `QueryResultObserver` +//! (`query_result_observer.rs`), and VIR→AIR lowering via `VirObserver` +//! (`vir/src/vir_observer.rs`). A consumer implements only the traits it needs. + +use crate::ast::{Decl, Expr, Ident, Query, Snapshots}; +use std::any::Any; + +/// Origin of a WP versioned constant created during `lower_query`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum VersionOrigin { + /// From a `StmtX::Havoc` — unconstrained new version (loop entry). + Havoc, + /// From a `StmtX::Assign` — constrained new version (= rhs). + Assign, + /// Phantom version from Switch branch reconciliation. + BranchMerge, + /// Phantom version from Breakable break reconciliation. + BreakMerge, +} + +/// Observer for the AIR-level verification pipeline. +/// +/// All methods have default no-op implementations except `as_any` +/// and `as_any_mut` which must be implemented (trivially: `self`). +pub trait AirObserver: Any + Send { + /// A verification query has been lowered (variables → versioned constants). + fn on_query_lowered(&mut self, _query: &Query, _snapshots: &Snapshots, _local_vars: &[Decl]) {} + + /// Called from `lower_query` at the moment a new WP version is created. + /// + /// For `Havoc`/`Assign` origins, the Nth call for base variable `x` + /// corresponds to the Nth VIR-level `on_havoc` or `on_assign` callback + /// for `x`. For merge origins, the call corresponds to the most recent + /// `on_branch_merge` or `on_break_merge` callback. + /// + /// See `VersionCorrelator` in `vir/src/vir_observer.rs` for a shared helper + /// that correlates these callbacks with VIR-level data. + fn on_wp_version_created(&mut self, _versioned: &Ident, _kind: VersionOrigin) {} + + /// A lambda definition was declared (%%lambda%%N). + fn on_lambda_decl(&mut self, _name: &Ident, _params: &[Ident], _body: &Expr) {} + + /// A choose binder name was declared (%%choose%%N). + fn on_choose_decl(&mut self, _name: &Ident, _binder_name: &Ident) {} + + /// An axiom declaration was processed (for accumulating function definitions). + fn on_axiom_decl(&mut self, _expr: &Expr) {} + + fn as_any(&self) -> &dyn Any; + fn as_any_mut(&mut self) -> &mut dyn Any; +} + +/// A shared handle to an `AirObserver`. `Arc>` rather than +/// `Rc>` because an `air::Context` holding one must stay `Send`: +/// resident sessions keep contexts in a `Mutex` served from other threads. +pub type AirObserverHandle = std::sync::Arc>; diff --git a/source/air/src/ast.rs b/source/air/src/ast.rs index c2325c9b0c..8d99352dba 100644 --- a/source/air/src/ast.rs +++ b/source/air/src/ast.rs @@ -9,8 +9,8 @@ pub type TypeError = String; pub type Ident = Arc; -pub(crate) type Snapshot = IndexMap; -pub(crate) type Snapshots = HashMap; +pub type Snapshot = IndexMap; +pub type Snapshots = HashMap; pub type Typ = Arc; pub type Typs = Arc>; diff --git a/source/air/src/bisect.rs b/source/air/src/bisect.rs index fb35417d93..06bce638f6 100644 --- a/source/air/src/bisect.rs +++ b/source/air/src/bisect.rs @@ -337,7 +337,7 @@ pub struct ProbeDetail { /// its switch (declared among the query's locals). fn prepare(context: &mut Context, query: &Query) -> Result<(Query, Vec), TypeError> { let query = crate::typecheck::check_query(context, query)?; - let (query, _, _, _) = crate::var_to_const::lower_query(&query, false); + let (query, _, _, _) = crate::var_to_const::lower_query(&query, false, None); let mut facts = Vec::new(); let assertion = mark_facts(&query.assertion, &mut facts); let mut local = (*query.local).clone(); diff --git a/source/air/src/block_to_assert.rs b/source/air/src/block_to_assert.rs index d6f4b89f06..da39c25919 100644 --- a/source/air/src/block_to_assert.rs +++ b/source/air/src/block_to_assert.rs @@ -77,7 +77,12 @@ fn stmt_to_expr(label_n: &mut u64, locals: &mut Vec, stmt: &Stmt, pred: Ex } } -pub(crate) fn lower_query( +/// Lower a block-structured query to assert form. +/// +/// Re-exported as `air::lower_query` so a consumer that reconstructs the verification +/// condition can apply the same lowering the solver sees. `AirObserver::on_query_lowered` +/// fires before this step. +pub fn lower_query( message_interface: &dyn crate::messages::MessageInterface, query: &Query, ) -> Query { diff --git a/source/air/src/closure.rs b/source/air/src/closure.rs index b4a3673e07..b1838273b8 100644 --- a/source/air/src/closure.rs +++ b/source/air/src/closure.rs @@ -314,6 +314,10 @@ fn simplify_lambda( let closure_fun = Arc::new(name); ctxt.lambda_count += 1; let _ = ctxt.lambda_map.insert(closure, closure_fun.clone()); + if let Some(obs) = &ctxt.air_observer { + let params: Vec = binders.iter().map(|b| b.name.clone()).collect(); + obs.lock().unwrap().on_lambda_decl(&closure_fun, ¶ms, &e1); + } // f(holes): (Fun (t_params) t_body) let decl = Arc::new(DeclX::Fun(closure_fun.clone(), holes.clone(), typ.clone())); @@ -418,6 +422,14 @@ fn simplify_choose( let closure_fun = Arc::new(name); ctxt.choose_count += 1; let _ = ctxt.choose_map.insert(closure, closure_fun.clone()); + if let Some(obs) = &ctxt.air_observer { + let binder_name = binders + .iter() + .next() + .map(|b| b.name.clone()) + .unwrap_or_else(|| Arc::new("_".to_string())); + obs.lock().unwrap().on_choose_decl(&closure_fun, &binder_name); + } // f(holes): typ_body let decl = Arc::new(DeclX::Fun(closure_fun.clone(), holes.clone(), typ_body.clone())); diff --git a/source/air/src/context.rs b/source/air/src/context.rs index dd5fbef16b..7d47f6c0e1 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -541,6 +541,11 @@ pub struct Context { name_counters: Vec, pub(crate) typing: Typing, pub(crate) debug: bool, + pub(crate) air_observer: + Option, + pub(crate) query_result_observer: Option< + crate::query_result_observer::QueryResultObserverHandle, + >, pub(crate) ignore_unexpected_smt: bool, pub(crate) rlimit: u32, pub(crate) air_initial_log: Emitter, @@ -687,6 +692,8 @@ impl Context { solver: solver.clone(), }, debug: false, + air_observer: None, + query_result_observer: None, ignore_unexpected_smt: false, rlimit: 0, air_initial_log: Emitter::new( @@ -806,6 +813,19 @@ impl Context { self.get_smt_process().send_commands(smt_data) } + /// Register observers for AIR passes and for solver results. Either may be `None`; + /// with none registered every observer hook is a no-op. + pub fn set_observers( + &mut self, + air_observer: Option, + query_result_observer: Option< + crate::query_result_observer::QueryResultObserverHandle, + >, + ) { + self.air_observer = air_observer; + self.query_result_observer = query_result_observer; + } + pub fn set_air_initial_log(&mut self, writer: Box) { self.air_initial_log.set_log(Some(writer)); } @@ -1555,11 +1575,22 @@ impl Context { return ValidityResult::TypeError(err); } }; - let (query, snapshots, local_vars, variable_versions) = crate::var_to_const::lower_query( - &query, - self.provenance || self.egraph_request.is_some() || self.speculation.is_some(), - ); + let (query, snapshots, local_vars, variable_versions) = { + // Scope the borrow so it is released before `on_query_lowered` below + // (both use the same shared observer handle — no reentrant borrow). + let mut guard = self.air_observer.as_ref().map(|o| o.lock().unwrap()); + let obs_ref = + guard.as_mut().map(|g| &mut **g as &mut dyn crate::air_observer::AirObserver); + crate::var_to_const::lower_query( + &query, + self.provenance || self.egraph_request.is_some() || self.speculation.is_some(), + obs_ref, + ) + }; self.variable_versions = variable_versions; + if let Some(o) = &self.air_observer { + o.lock().unwrap().on_query_lowered(&query, &snapshots, &local_vars); + } self.air_middle_log.log_query(&query); let query = crate::block_to_assert::lower_query(message_interface, &query); self.air_final_log.log_query(&query); @@ -1624,10 +1655,28 @@ impl Context { self.smt_log.log_eval(expr); let smt_data = self.smt_log.take_pipe_data(); let smt_output = self.get_smt_process().send_commands(smt_data); - if smt_output.len() != 1 { - panic!("unexpected output from SMT eval {:?}", smt_output); + if smt_output.len() == 1 { + smt_output[0].clone() + } else { + // The solver prints multi-line output for compound model values (quantified + // formulas, algebraic data type constructors). These are never simple booleans, + // so return a value that callers will treat as unknown. + "unknown".to_string() + } + } + + /// Evaluate an AIR expression against the current solver model as a boolean. + /// Returns `Some(true)` / `Some(false)` if the solver returns a boolean, + /// `None` if the expression is non-boolean or evaluation fails. + pub fn evaluate_bool(&mut self, expr: &crate::ast::Expr) -> Option { + let printer = + crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone()); + let node = printer.expr_to_node(expr); + match self.eval_expr(node).as_str() { + "true" => Some(true), + "false" => Some(false), + _ => None, } - smt_output[0].clone() } pub fn command( diff --git a/source/air/src/lib.rs b/source/air/src/lib.rs index 81acd8d1b0..7c2e5b8e3e 100644 --- a/source/air/src/lib.rs +++ b/source/air/src/lib.rs @@ -1,3 +1,4 @@ +pub mod air_observer; pub mod ast; pub mod ast_util; pub mod bisect; @@ -10,6 +11,7 @@ pub mod messages; pub mod model; pub mod parser; pub mod profiler; +pub mod query_result_observer; pub mod remove_asserts; pub mod scope_map; pub mod smt_process; @@ -21,6 +23,7 @@ pub mod printer; pub mod scaffold; mod block_to_assert; +pub use block_to_assert::lower_query; mod closure; pub mod def; mod smt_verify; diff --git a/source/air/src/query_result_observer.rs b/source/air/src/query_result_observer.rs new file mode 100644 index 0000000000..a14fc207fd --- /dev/null +++ b/source/air/src/query_result_observer.rs @@ -0,0 +1,70 @@ +//! Query-result observer. +//! +//! Defines `QueryResultObserver` — the interface for observing the outcome of +//! each verification query (`Invalid` / `Valid` / `Timeout`), including live +//! model evaluation on `Invalid`. +//! +//! This trait is independent: it does **not** require `AirObserver` or +//! `VirObserver`. A consumer that only cares about verification outcomes +//! implements this trait alone. +//! +//! **`Invalid` is an interactive, live-window callback** — the one deliberate +//! exception to "observers are passive." Alongside the counterexample model +//! (`model_defs`), it hands the observer `eval_bool_expr`, a closure that +//! evaluates a boolean AIR expression against the *live* solver model. The model is +//! only valid for the duration of the callback: the core discovers the failing +//! assertion, invokes the observer, and only then disables the assertion label +//! (which invalidates the model); see `smt_check_assertion` in `smt_verify.rs`. + +use crate::ast::{Expr, Ident}; +use crate::messages::ArcDynMessage as Message; +use crate::model::ModelDef; +use std::any::Any; +use std::collections::HashMap; + +/// Verification result passed to the observer after each query. +pub enum CheckValidResult<'a> { + Invalid { + /// The parsed counterexample model (concrete symbol assignments). + /// Built by the core for its own error reporting; exposed here for free. + model_defs: &'a HashMap, + /// Evaluate a boolean AIR expression against the live solver model. + /// Returns `Some(bool)` for a boolean result, `None` for a non-boolean + /// expression or one the model cannot evaluate. Valid only during this + /// callback (the model is torn down afterward). + eval_bool_expr: &'a mut dyn FnMut(&Expr) -> Option, + assert_id: &'a Option, + error: &'a Message, + }, + /// The query was discharged (unsat). Carries the ids of every assertion the query + /// checked, so a consumer can attribute the success to specific obligations. There is no + /// model: nothing to evaluate against. + Valid { + assert_ids: &'a [Option], + /// What the solver used to discharge the query (currently the unsat core as the set + /// of named axioms), when usage reporting is enabled (`-V axiom-usage-info`); + /// `UsageInfo::None` otherwise. Computed by the core for its own reporting and exposed + /// here for free. The type is the core's own, so richer usage data can be added there + /// without changing this interface. + usage_info: &'a crate::context::UsageInfo, + }, + Timeout { + assert_id: &'a Option, + }, +} + +/// Observer for verification query results. +/// +/// The single callback fires once per query after the solver returns. All +/// methods except `as_any`/`as_any_mut` have default no-op implementations. +pub trait QueryResultObserver: Any + Send { + /// A verification query completed with a result. + fn on_check_valid_result(&mut self, _result: &mut CheckValidResult) {} + + fn as_any(&self) -> &dyn Any; + fn as_any_mut(&mut self) -> &mut dyn Any; +} + +/// A shared handle to a `QueryResultObserver`; `Arc>` for the reason +/// given at `AirObserverHandle`. +pub type QueryResultObserverHandle = std::sync::Arc>; diff --git a/source/air/src/smt_verify.rs b/source/air/src/smt_verify.rs index aa36f01eaf..f1b21efef2 100644 --- a/source/air/src/smt_verify.rs +++ b/source/air/src/smt_verify.rs @@ -112,6 +112,9 @@ pub(crate) fn smt_add_decl<'ctx>(context: &mut Context, decl: &Decl) { let mut infos: Vec = Vec::new(); let mut axiom_infos: Vec = Vec::new(); let labeled_expr = label_asserts(context, &mut infos, &mut axiom_infos, &expr); + if let Some(obs) = &context.air_observer { + obs.lock().unwrap().on_axiom_decl(&labeled_expr); + } for info in axiom_infos { crate::typecheck::add_decl(context, &info.decl, true).unwrap(); context @@ -637,6 +640,14 @@ pub(crate) fn smt_check_assertion<'ctx>( match reason.expect("expected :reason-unknown") { SmtReasonUnknown::Canceled | SmtReasonUnknown::Unknown => { context.state = ContextState::Canceled; + // Notify observer of timeout/cancellation + if let Some(obs) = &context.query_result_observer { + obs.lock().unwrap().on_check_valid_result( + &mut crate::query_result_observer::CheckValidResult::Timeout { + assert_id: &None, + }, + ); + } ResultDetermination::Determined(ValidityResult::Canceled) } SmtReasonUnknown::Incomplete => ResultDetermination::Undetermined(false), @@ -673,6 +684,17 @@ pub(crate) fn smt_check_assertion<'ctx>( crate::context::UsageInfo::None }; + if let Some(obs) = &context.query_result_observer { + let assert_ids: Vec> = + infos.iter().map(|info| info.assert_id.clone()).collect(); + obs.lock().unwrap().on_check_valid_result( + &mut crate::query_result_observer::CheckValidResult::Valid { + assert_ids: &assert_ids, + usage_info: &usage_info, + }, + ); + } + ValidityResult::Valid(usage_info) } ResultDetermination::Undetermined(false) => { @@ -1912,17 +1934,21 @@ fn smt_get_model( for def in model.iter() { model_defs.insert(def.name.clone(), def.clone()); } - for info in infos.iter_mut() { + // The `QueryResultObserver::Invalid` callback exposes a live model evaluator + // (`eval_bool_expr`), so the solver model must stay valid across the callback. + // Disabling the failing assertion's label invalidates the model, so that step is + // deferred: first discover the failing assertion, then notify the observer while + // the model is live, and only then disable the label for subsequent check-sats. + // The disable step runs whether or not an observer is registered. + // + // Discover the failing assertion without disabling the label. + let mut discovered_info_index: Option = None; + for (i, info) in infos.iter().enumerate() { if let Some(def) = model_defs.get(&info.label) { if *def.body == "true" { discovered_error = Some(info.clone()); discovered_assert_id = Some(info.assert_id.clone()); - - // Disable this label in subsequent check-sat calls to get additional errors - info.disabled = true; - let disable_label = mk_not(&ident_var(&info.label)); - context.smt_log.log_assert(&None, &None, &disable_label); - + discovered_info_index = Some(i); break; } } @@ -1956,6 +1982,31 @@ fn smt_get_model( let error = discovered_error.error; let e = context.message_interface.append_labels(&error, &discovered_additional_info); + + // Notify the observer while the solver model is still valid. + // eval_expr calls context.evaluate_bool() which sends (eval ...) to the solver. + // This only works before the label is disabled (which invalidates the model). + // Clone the shared handle so `context` stays free for the eval_bool_expr closure. + let obs = context.query_result_observer.clone(); + if let Some(obs) = &obs { + let assert_id = discovered_assert_id.clone().unwrap(); + obs.lock().unwrap().on_check_valid_result( + &mut crate::query_result_observer::CheckValidResult::Invalid { + model_defs: &model_defs, + eval_bool_expr: &mut |expr| context.evaluate_bool(expr), + assert_id: &assert_id, + error: &e, + }, + ); + } + + // Disable the label for subsequent check-sat calls (this invalidates the model). + if let Some(idx) = discovered_info_index { + infos[idx].disabled = true; + let disable_label = mk_not(&ident_var(&infos[idx].label)); + context.smt_log.log_assert(&None, &None, &disable_label); + } + context.state = ContextState::FoundInvalid(infos, Some(air_model.clone())); ValidityResult::Invalid(Some(air_model), Some(e), discovered_assert_id.unwrap()) } diff --git a/source/air/src/var_to_const.rs b/source/air/src/var_to_const.rs index 7a5a6f18b8..7a85fd91a8 100644 --- a/source/air/src/var_to_const.rs +++ b/source/air/src/var_to_const.rs @@ -119,7 +119,7 @@ fn update_breaks_to_versions( } } -struct LowerStmtState { +struct LowerStmtState<'a> { decls: Vec, break_versions: HashMap>>, version_decls: HashSet, @@ -129,6 +129,7 @@ struct LowerStmtState { /// When kept, each assert reached, with the versions and snapshots in /// force there. goal_scopes: Option, GoalScope)>>, + observer: Option<&'a mut dyn crate::air_observer::AirObserver>, } /// The variable versions and snapshots in force at one assert of a query: @@ -145,7 +146,7 @@ impl GoalScope { /// 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 (_, _, _, _, entry, scopes) = lower_query_with(query, false, true, None); 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)) @@ -168,8 +169,20 @@ impl GoalScope { } } +impl LowerStmtState<'_> { + fn notify_version_created( + &mut self, + versioned: &Ident, + kind: crate::air_observer::VersionOrigin, + ) { + if let Some(obs) = &mut self.observer { + obs.on_wp_version_created(versioned, kind); + } + } +} + fn lower_stmt( - state: &mut LowerStmtState, + state: &mut LowerStmtState<'_>, versions: &mut IndexMap, snapshots: &mut Snapshots, types: &HashMap, @@ -188,6 +201,7 @@ fn lower_stmt( stmt } StmtX::Havoc(x) | StmtX::Assign(x, _) => { + let is_havoc = matches!(&*stmt, StmtX::Havoc(_)); let n = find_version(&versions, x); let typ = types[x].clone(); versions.insert(x.clone(), n + 1); @@ -200,6 +214,12 @@ fn lower_stmt( state.decls.push(decl); state.version_decls.insert(x.clone()); } + let kind = if is_havoc { + crate::air_observer::VersionOrigin::Havoc + } else { + crate::air_observer::VersionOrigin::Assign + }; + state.notify_version_created(&x, kind); match &*stmt { StmtX::Assign(_, e) => { let expr1 = Arc::new(ExprX::Var(x)); @@ -235,6 +255,18 @@ fn lower_stmt( state.break_versions.remove(label).expect("break_versions"); all_versions.insert(0, versions.clone()); update_versions_from_all_branches(&all_versions, versions); + // Notify observer of phantom versions created by break merge reconciliation + for x in versions.keys() { + let merged_version = versions[x]; + let had_explicit = all_versions.iter().any(|v| v[x] == merged_version); + if !had_explicit { + let renamed = Arc::new(rename_var(x, merged_version)); + state.notify_version_created( + &renamed, + crate::air_observer::VersionOrigin::BreakMerge, + ); + } + } let mut break_i: usize = 1; let s = update_breaks_to_versions(label, &all_versions, versions, &mut break_i, &s); assert!(break_i == all_versions.len()); @@ -264,6 +296,18 @@ fn lower_stmt( state.all_snapshots.extend(snapshots_i); } update_versions_from_all_branches(&all_versions, versions); + // Notify observer of phantom versions created by merge reconciliation + for x in versions.keys() { + let merged_version = versions[x]; + let had_explicit = all_versions.iter().any(|v| v[x] == merged_version); + if !had_explicit { + let renamed = Arc::new(rename_var(x, merged_version)); + state.notify_version_created( + &renamed, + crate::air_observer::VersionOrigin::BranchMerge, + ); + } + } for i in 0..ss.len() { stmts[i] = update_branch_to_versions(&all_versions[i], versions, &stmts[i], false); } @@ -275,9 +319,10 @@ fn lower_stmt( pub(crate) fn lower_query( query: &Query, record_versions: bool, + observer: Option<&mut dyn crate::air_observer::AirObserver>, ) -> (Query, Snapshots, Vec, crate::context::VariableVersions) { let (query, snapshots, local_vars, versions, _, _) = - lower_query_with(query, record_versions, false); + lower_query_with(query, record_versions, false, observer); (query, snapshots, local_vars, versions) } @@ -287,6 +332,7 @@ fn lower_query_with( query: &Query, record_versions: bool, record_goal_scopes: bool, + observer: Option<&mut dyn crate::air_observer::AirObserver>, ) -> ( Query, Snapshots, @@ -339,6 +385,7 @@ fn lower_query_with( variable_versions, record_versions, goal_scopes: record_goal_scopes.then(Vec::new), + observer, }; let entry = GoalScope { versions: versions.clone(), snapshots: snapshots.clone() }; let assertion = lower_stmt(&mut state, &mut versions, &mut snapshots, &types, assertion); @@ -370,14 +417,14 @@ mod tests { }) }; let (_, _, _, versions) = - lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), true); + lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), true, None); assert_eq!(versions.get("balance@0"), Some(&("balance@".into(), 0))); assert_eq!(versions.get("balance@1"), Some(&("balance@".into(), 1))); - let (_, _, _, versions) = lower_query(&query(vec![]), true); + let (_, _, _, versions) = lower_query(&query(vec![]), true, None); assert_eq!(versions.len(), 1); assert!(!versions.contains_key("balance@1")); let (_, _, _, versions) = - lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), false); + lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), false, None); assert!(versions.is_empty()); } diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 9cc3c60854..6b83837f35 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -151,6 +151,7 @@ pub struct ArgsX { pub reach: Option, /// Serve retained AIR queries over stdin/stdout after compilation. pub resident: bool, + pub observers: Vec, } impl ArgsX { @@ -209,6 +210,7 @@ impl ArgsX { inst_pressure: Default::default(), reach: Default::default(), resident: false, + observers: Default::default(), } } } @@ -464,6 +466,7 @@ pub fn parse_args_with_imports( const EXTENDED_INST_PRESSURE: &str = "inst-pressure"; const EXTENDED_DIFFICULTY: &str = "difficulty"; const EXTENDED_TLA_EXPORT: &str = "tla-export"; + const EXTENDED_OBSERVERS: &str = "observers"; const EXTENDED_KEYS: &[(&str, &str)] = &[ ( EXTENDED_INST_PRESSURE, @@ -519,6 +522,7 @@ pub fn parse_args_with_imports( EXTENDED_NO_BV_SIMPLIFY, "internal option to disable simplification of bit-vector assertions before sending to the SMT solver", ), + (EXTENDED_OBSERVERS, "Comma-separated list of observers (e.g., test)"), ]; let default_num_threads: usize = std::thread::available_parallelism() @@ -970,6 +974,11 @@ pub fn parse_args_with_imports( }, inst_pressure: extended.contains_key(EXTENDED_INST_PRESSURE), resident: matches.opt_present(OPT_RESIDENT), + observers: extended + .get(EXTENDED_OBSERVERS) + .and_then(|v| v.as_ref()) + .map(|s| s.split(',').map(|s| s.trim().to_string()).collect::>()) + .unwrap_or_default(), }; if args.nl_frontier && !matches!(args.solver, SmtSolver::Cvc5) { diff --git a/source/rust_verify/src/lib.rs b/source/rust_verify/src/lib.rs index c4d58cb467..224fcfec4f 100644 --- a/source/rust_verify/src/lib.rs +++ b/source/rust_verify/src/lib.rs @@ -73,6 +73,7 @@ mod scaffold; #[cfg(feature = "singular")] pub mod singular; mod spans; +pub mod test_observer; pub mod trait_check; mod trait_check_ast; mod trait_check_emit; diff --git a/source/rust_verify/src/test_observer.rs b/source/rust_verify/src/test_observer.rs new file mode 100644 index 0000000000..e1d917c760 --- /dev/null +++ b/source/rust_verify/src/test_observer.rs @@ -0,0 +1,609 @@ +//! Built-in test observer activated by `-V observers=test`. +//! Records callback data and emits JSON for test assertions. + +use std::any::Any; +use vir::ast_util::LowerUniqueVar; + +/// Counts `Breakable` / `Break` statements in a query assertion (present when loops are +/// lowered without isolation). +fn count_break_stmts(stmt: &air::ast::Stmt) -> (usize, usize) { + use air::ast::StmtX; + match &**stmt { + StmtX::Breakable(_, body) => { + let (b, k) = count_break_stmts(body); + (b + 1, k) + } + StmtX::Break(_) => (0, 1), + StmtX::DeadEnd(body) => count_break_stmts(body), + StmtX::Block(stmts) | StmtX::Switch(stmts) => stmts.iter().fold((0, 0), |(b, k), s| { + let (b2, k2) = count_break_stmts(s); + (b + b2, k + k2) + }), + _ => (0, 0), + } +} + +pub struct TestObserver { + pub krate_function_names: Vec, + pub krate_datatype_names: Vec, + pub havocs: Vec, + pub assigns: Vec, + pub branch_merges: usize, + pub break_merges: usize, + pub variable_defs: Vec, + pub for_loop_vars: Vec<(String, String)>, + pub reveal_strings: Vec, + pub quantifier_binders: Vec, + pub assert_id_kinds: Vec, + pub function_lowered_count: usize, + pub query_lowered_count: usize, + pub query_snapshot_counts: Vec, + pub version_correlations: Vec<(String, u32, String)>, + pub correlator: vir::vir_observer::VersionCorrelator, + pub lambda_decls: Vec, + pub choose_decls: Vec, + pub check_valid_invalid_count: usize, + pub check_valid_valid_count: usize, + pub check_valid_timeout: usize, + pub check_valid_invalid_model_size: Vec, + pub eval_expr_results: Vec>, + pub binder_decls: Vec, + /// Count of `StmtX::Breakable` in lowered queries (loop encodings without isolation). + /// Per discharged (Valid) query: how many labeled assertion ids it reported. + pub valid_assert_id_counts: Vec, + /// Per discharged query: number of named axioms in the unsat core, or None when usage + /// reporting is not enabled. + pub valid_used_axiom_counts: Vec>, + pub breakable_count: usize, + /// Count of `StmtX::Break` in lowered queries. + pub break_count: usize, + pub pre_body_binders: Vec, + pub post_body_binders: Vec, + pub body_lowering_started: bool, + /// Ordered trace of every callback in fire order — enables sequencing + /// assertions (L1–L5) that per-callback aggregates cannot express. + pub events: Vec, + /// Count of `on_axiom_decl` (high-frequency; counted, not traced). + pub axiom_decls: usize, +} + +impl TestObserver { + pub fn new() -> Self { + TestObserver { + krate_function_names: vec![], + krate_datatype_names: vec![], + havocs: vec![], + assigns: vec![], + branch_merges: 0, + break_merges: 0, + variable_defs: vec![], + for_loop_vars: vec![], + reveal_strings: vec![], + quantifier_binders: vec![], + assert_id_kinds: vec![], + function_lowered_count: 0, + query_lowered_count: 0, + query_snapshot_counts: vec![], + version_correlations: vec![], + correlator: vir::vir_observer::VersionCorrelator::new(), + lambda_decls: vec![], + choose_decls: vec![], + check_valid_invalid_count: 0, + check_valid_valid_count: 0, + check_valid_timeout: 0, + check_valid_invalid_model_size: vec![], + eval_expr_results: vec![], + binder_decls: vec![], + valid_assert_id_counts: vec![], + valid_used_axiom_counts: vec![], + breakable_count: 0, + break_count: 0, + pre_body_binders: vec![], + post_body_binders: vec![], + body_lowering_started: false, + events: vec![], + axiom_decls: 0, + } + } + + fn json_strings(v: &[String]) -> String { + let items: Vec = v.iter().map(|s| format!("\"{}\"", s)).collect(); + format!("[{}]", items.join(",")) + } + fn json_usizes(v: &[usize]) -> String { + let items: Vec = v.iter().map(|n| n.to_string()).collect(); + format!("[{}]", items.join(",")) + } + fn json_opt_bools(v: &[Option]) -> String { + let items: Vec = v + .iter() + .map(|b| match b { + Some(true) => "true".to_string(), + Some(false) => "false".to_string(), + None => "null".to_string(), + }) + .collect(); + format!("[{}]", items.join(",")) + } + fn json_opt_usizes(v: &[Option]) -> String { + let items: Vec = v + .iter() + .map(|n| match n { + Some(n) => n.to_string(), + None => "null".to_string(), + }) + .collect(); + format!("[{}]", items.join(",")) + } + fn json_version_correlations(v: &[(String, u32, String)]) -> String { + let items: Vec = v + .iter() + .map(|(name, line, kind)| format!("[\"{}\",{},\"{}\"]", name, line, kind)) + .collect(); + format!("[{}]", items.join(",")) + } + fn json_string_pairs(v: &[(String, String)]) -> String { + let items: Vec = v.iter().map(|(a, b)| format!("[\"{}\",\"{}\"]", a, b)).collect(); + format!("[{}]", items.join(",")) + } + + pub fn summary_json(&self) -> String { + format!( + concat!( + "OBSERVER:{{", + "\"krate_function_names\":{},\"krate_datatype_names\":{},", + "\"havocs\":{},\"assigns\":{},", + "\"branch_merges\":{},\"break_merges\":{},", + "\"variable_defs\":{},\"for_loop_vars\":{},", + "\"reveal_strings\":{},", + "\"quantifier_binders\":{},", + "\"assert_id_kinds\":{},", + "\"function_lowered\":{},\"query_lowered\":{},", + "\"query_snapshot_counts\":{},", + "\"version_correlations\":{},", + "\"lambda_decls\":{},\"choose_decls\":{},", + "\"check_valid_invalid\":{},\"check_valid_valid\":{},", + "\"check_valid_timeout\":{},", + "\"check_valid_invalid_model_size\":{},", + "\"eval_expr_results\":{},", + "\"binder_decls\":{},", + "\"pre_body_binders\":{},", + "\"post_body_binders\":{},", + "\"events\":{},", + "\"axiom_decls\":{},", + "\"breakable_count\":{},\"break_count\":{},", + "\"valid_assert_id_counts\":{},", + "\"valid_used_axiom_counts\":{}", + "}}" + ), + Self::json_strings(&self.krate_function_names), + Self::json_strings(&self.krate_datatype_names), + Self::json_strings(&self.havocs), + Self::json_strings(&self.assigns), + self.branch_merges, + self.break_merges, + Self::json_strings(&self.variable_defs), + Self::json_string_pairs(&self.for_loop_vars), + Self::json_strings(&self.reveal_strings), + Self::json_strings(&self.quantifier_binders), + Self::json_strings(&self.assert_id_kinds), + self.function_lowered_count, + self.query_lowered_count, + Self::json_usizes(&self.query_snapshot_counts), + Self::json_version_correlations(&self.version_correlations), + Self::json_strings(&self.lambda_decls), + Self::json_strings(&self.choose_decls), + self.check_valid_invalid_count, + self.check_valid_valid_count, + self.check_valid_timeout, + Self::json_usizes(&self.check_valid_invalid_model_size), + Self::json_opt_bools(&self.eval_expr_results), + Self::json_strings(&self.binder_decls), + Self::json_strings(&self.pre_body_binders), + Self::json_strings(&self.post_body_binders), + Self::json_strings(&self.events), + self.axiom_decls, + self.breakable_count, + self.break_count, + Self::json_usizes(&self.valid_assert_id_counts), + Self::json_opt_usizes(&self.valid_used_axiom_counts), + ) + } +} + +fn fun_name(f: &vir::ast::Function) -> String { + f.x.name.path.segments.last().map(|s| s.to_string()).unwrap_or_default() +} +fn dt_name(d: &vir::ast::Datatype) -> String { + match &d.x.name { + vir::ast::Dt::Path(p) => p.segments.last().map(|s| s.to_string()).unwrap_or_default(), + vir::ast::Dt::Tuple(n) => format!("tuple{}", n), + } +} + +impl air::air_observer::AirObserver for TestObserver { + fn on_query_lowered( + &mut self, + query: &air::ast::Query, + snapshots: &air::ast::Snapshots, + _: &[air::ast::Decl], + ) { + self.query_lowered_count += 1; + self.query_snapshot_counts.push(snapshots.len()); + let (breakables, breaks) = count_break_stmts(&query.assertion); + self.breakable_count += breakables; + self.break_count += breaks; + self.events.push("query_lowered".to_string()); + } + fn on_wp_version_created( + &mut self, + versioned: &air::ast::Ident, + kind: air::air_observer::VersionOrigin, + ) { + self.events.push(format!("wp_version:{:?}", kind)); + if let Some(stm) = self.correlator.resolve(versioned, kind) { + if let Some(line) = vir::vir_observer::line_from_span(&stm.span) { + let kind_str = format!("{:?}", kind); + self.version_correlations.push((versioned.to_string(), line, kind_str)); + } + } + } + fn on_lambda_decl( + &mut self, + name: &air::ast::Ident, + _: &[air::ast::Ident], + _: &air::ast::Expr, + ) { + self.lambda_decls.push(name.to_string()); + self.events.push(format!("lambda_decl:{}", name)); + } + fn on_choose_decl(&mut self, name: &air::ast::Ident, _: &air::ast::Ident) { + self.choose_decls.push(name.to_string()); + self.events.push(format!("choose_decl:{}", name)); + } + fn on_axiom_decl(&mut self, _expr: &air::ast::Expr) { + self.axiom_decls += 1; + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +impl air::query_result_observer::QueryResultObserver for TestObserver { + fn on_check_valid_result(&mut self, result: &mut air::query_result_observer::CheckValidResult) { + match result { + air::query_result_observer::CheckValidResult::Invalid { + model_defs, + eval_bool_expr, + .. + } => { + self.events.push("check_valid:Invalid".to_string()); + self.check_valid_invalid_count += 1; + self.check_valid_invalid_model_size.push(model_defs.len()); + // Pin the evaluator's three-way contract: a true boolean, a false boolean, + // and a non-boolean (unevaluable) expression. + let true_expr = + std::sync::Arc::new(air::ast::ExprX::Const(air::ast::Constant::Bool(true))); + self.eval_expr_results.push(eval_bool_expr(&true_expr)); + let false_expr = + std::sync::Arc::new(air::ast::ExprX::Const(air::ast::Constant::Bool(false))); + self.eval_expr_results.push(eval_bool_expr(&false_expr)); + let non_bool = std::sync::Arc::new(air::ast::ExprX::Const( + air::ast::Constant::Nat(std::sync::Arc::new("42".to_string())), + )); + self.eval_expr_results.push(eval_bool_expr(&non_bool)); + } + air::query_result_observer::CheckValidResult::Valid { assert_ids, usage_info } => { + self.events.push("check_valid:Valid".to_string()); + self.check_valid_valid_count += 1; + // A discharged query names the obligations it checked (ids may be None for + // assertions the lowering left unlabeled). + self.valid_assert_id_counts.push(assert_ids.iter().filter(|a| a.is_some()).count()); + // Usage data is opt-in: the count of used axioms when reporting is on, else None. + self.valid_used_axiom_counts.push(match usage_info { + air::context::UsageInfo::UsedAxioms(names) => Some(names.len()), + air::context::UsageInfo::None => None, + }); + } + air::query_result_observer::CheckValidResult::Timeout { .. } => { + self.events.push("check_valid:Timeout".to_string()); + self.check_valid_timeout += 1; + } + } + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +impl vir::vir_observer::VirObserver for TestObserver { + fn on_krate( + &mut self, + krate: &vir::ast::Krate, + _name_ctxt: &vir::def::NameCtxt, + _current_crate: &vir::ast::CrateId, + ) { + self.krate_function_names = krate.functions.iter().map(fun_name).collect(); + self.krate_datatype_names = krate.datatypes.iter().map(dt_name).collect(); + self.events.push("krate".to_string()); + } + fn on_havoc(&mut self, stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.havocs.push(base.to_string()); + self.events.push(format!("havoc:{}", base)); + self.correlator.record_havoc_or_assign(&base, stm); + } + fn on_assign(&mut self, stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.assigns.push(base.to_string()); + self.events.push(format!("assign:{}", base)); + self.correlator.record_havoc_or_assign(&base, stm); + } + fn on_branch_merge(&mut self, stm: &vir::sst::Stm) { + self.branch_merges += 1; + self.events.push("branch_merge".to_string()); + self.correlator.record_branch_merge(stm); + } + fn on_break_merge(&mut self, stm: &vir::sst::Stm) { + self.break_merges += 1; + self.events.push("break_merge".to_string()); + self.correlator.record_break_merge(stm); + } + fn on_variable_def(&mut self, _stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + self.variable_defs.push(vir::def::suffix_local_unique_id(var).to_string()); + self.events.push(format!("variable_def:{}", vir::def::suffix_local_unique_id(var))); + } + fn on_for_loop(&mut self, _stm: &vir::sst::Stm) { + self.for_loop_vars.push(("for_loop".to_string(), "detected".to_string())); + self.events.push("for_loop".to_string()); + } + fn on_reveal_string(&mut self, lit: &std::sync::Arc) { + self.reveal_strings.push((**lit).clone()); + self.events.push("reveal".to_string()); + } + fn on_quantifier_binder( + &mut self, + binder: &vir::ast::VarBinder, + _exp: &vir::sst::Exp, + ) { + let name = binder.name.lower().to_string(); + self.quantifier_binders.push(name.clone()); + self.events.push(format!("quant_binder:{}", name)); + if self.body_lowering_started { + self.post_body_binders.push(name); + } else { + self.pre_body_binders.push(name); + } + } + fn on_body_lowering_start(&mut self) { + self.body_lowering_started = true; + self.events.push("body_start".to_string()); + } + fn make_assert_id( + &mut self, + kind: &vir::vir_observer::AssertIdKind, + _index: usize, + parent: &Option, + ) -> Option { + self.assert_id_kinds.push(format!("{:?}", kind)); + self.events.push(format!("assert_id:{:?}", kind)); + parent.clone() + } + fn on_quantifier_binder_decl(&mut self, var: &vir::ast::VarIdent) { + self.binder_decls.push(vir::def::suffix_local_unique_id(var).to_string()); + self.events.push(format!("binder_decl:{}", vir::def::suffix_local_unique_id(var))); + } + fn on_function_lowered(&mut self) { + self.function_lowered_count += 1; + self.body_lowering_started = false; + self.events.push("function_lowered".to_string()); + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +// --------------------------------------------------------------------------- +// Dedicated single-trait observers. +// +// Each implements exactly ONE observer trait. They serve double duty: +// (1) focused functional coverage of that trait's callbacks (payloads + +// within-trait order), on inputs designed to elicit them; and +// (2) a compile-time + runtime proof of decoupling — a single-trait `impl` +// compiles and binds without requiring the other traits, and the +// unrelated registry slots stay `None`. +// --------------------------------------------------------------------------- + +/// Implements only `AirObserver`. +pub struct AirOnlyObserver { + pub events: Vec, + pub lambda_decls: Vec, + pub choose_decls: Vec, + pub query_lowered: usize, + pub axiom_decls: usize, +} +impl AirOnlyObserver { + pub fn new() -> Self { + AirOnlyObserver { + events: vec![], + lambda_decls: vec![], + choose_decls: vec![], + query_lowered: 0, + axiom_decls: 0, + } + } + pub fn summary_json(&self) -> String { + format!( + "AIROBS:{{\"events\":{},\"lambda_decls\":{},\"choose_decls\":{},\"query_lowered\":{},\"axiom_decls\":{}}}", + TestObserver::json_strings(&self.events), + TestObserver::json_strings(&self.lambda_decls), + TestObserver::json_strings(&self.choose_decls), + self.query_lowered, + self.axiom_decls, + ) + } +} +impl air::air_observer::AirObserver for AirOnlyObserver { + fn on_query_lowered( + &mut self, + _: &air::ast::Query, + _: &air::ast::Snapshots, + _: &[air::ast::Decl], + ) { + self.query_lowered += 1; + self.events.push("query_lowered".to_string()); + } + fn on_wp_version_created( + &mut self, + _: &air::ast::Ident, + kind: air::air_observer::VersionOrigin, + ) { + self.events.push(format!("wp_version:{:?}", kind)); + } + fn on_lambda_decl( + &mut self, + name: &air::ast::Ident, + _: &[air::ast::Ident], + _: &air::ast::Expr, + ) { + self.lambda_decls.push(name.to_string()); + self.events.push(format!("lambda_decl:{}", name)); + } + fn on_choose_decl(&mut self, name: &air::ast::Ident, _: &air::ast::Ident) { + self.choose_decls.push(name.to_string()); + self.events.push(format!("choose_decl:{}", name)); + } + fn on_axiom_decl(&mut self, _expr: &air::ast::Expr) { + self.axiom_decls += 1; + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +/// Implements only `QueryResultObserver` — receives `Invalid`/`Valid`/`Timeout` +/// and exercises the live `eval_bool_expr` closure on `Invalid`. Proves a +/// results-only consumer couples nothing else. +pub struct QueryResultOnlyObserver { + pub events: Vec, + pub invalid: usize, + pub valid: usize, + pub timeout: usize, + pub eval_expr_results: Vec>, +} +impl QueryResultOnlyObserver { + pub fn new() -> Self { + QueryResultOnlyObserver { + events: vec![], + invalid: 0, + valid: 0, + timeout: 0, + eval_expr_results: vec![], + } + } + pub fn summary_json(&self) -> String { + format!( + "QROBS:{{\"events\":{},\"invalid\":{},\"valid\":{},\"timeout\":{},\"eval_expr_results\":{}}}", + TestObserver::json_strings(&self.events), + self.invalid, + self.valid, + self.timeout, + TestObserver::json_opt_bools(&self.eval_expr_results), + ) + } +} +impl air::query_result_observer::QueryResultObserver for QueryResultOnlyObserver { + fn on_check_valid_result(&mut self, result: &mut air::query_result_observer::CheckValidResult) { + match result { + air::query_result_observer::CheckValidResult::Invalid { eval_bool_expr, .. } => { + self.invalid += 1; + self.events.push("check_valid:Invalid".to_string()); + let true_expr = + std::sync::Arc::new(air::ast::ExprX::Const(air::ast::Constant::Bool(true))); + self.eval_expr_results.push(eval_bool_expr(&true_expr)); + } + air::query_result_observer::CheckValidResult::Valid { .. } => { + self.valid += 1; + self.events.push("check_valid:Valid".to_string()); + } + air::query_result_observer::CheckValidResult::Timeout { .. } => { + self.timeout += 1; + self.events.push("check_valid:Timeout".to_string()); + } + } + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +/// Implements only `VirObserver`. +pub struct VirOnlyObserver { + pub events: Vec, + pub function_names: Vec, + pub havocs: Vec, + pub assigns: Vec, + pub function_lowered: usize, +} +impl VirOnlyObserver { + pub fn new() -> Self { + VirOnlyObserver { + events: vec![], + function_names: vec![], + havocs: vec![], + assigns: vec![], + function_lowered: 0, + } + } + pub fn summary_json(&self) -> String { + format!( + "VIROBS:{{\"events\":{},\"function_names\":{},\"havocs\":{},\"assigns\":{},\"function_lowered\":{}}}", + TestObserver::json_strings(&self.events), + TestObserver::json_strings(&self.function_names), + TestObserver::json_strings(&self.havocs), + TestObserver::json_strings(&self.assigns), + self.function_lowered, + ) + } +} +impl vir::vir_observer::VirObserver for VirOnlyObserver { + fn on_krate(&mut self, krate: &vir::ast::Krate, _: &vir::def::NameCtxt, _: &vir::ast::CrateId) { + self.function_names = krate.functions.iter().map(fun_name).collect(); + self.events.push("krate".to_string()); + } + fn on_havoc(&mut self, _stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.havocs.push(base.to_string()); + self.events.push(format!("havoc:{}", base)); + } + fn on_assign(&mut self, _stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.assigns.push(base.to_string()); + self.events.push(format!("assign:{}", base)); + } + fn on_function_lowered(&mut self) { + self.function_lowered += 1; + self.events.push("function_lowered".to_string()); + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index eddefbd3ba..64d0b4e1e8 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -29,6 +29,66 @@ use rustc_error_messages::MultiSpan; use rustc_index::bit_set::DenseBitSet; use rustc_middle::ty::TyCtxt; use rustc_span::Span; + +/// Build the observer registry for a given observer name. The concrete type is +/// known here, so each `Arc>` is coerced (unsizing) into an +/// independent per-trait handle. A consumer that implements only a subset of the +/// traits populates only those slots. `TestObserver` implements all three. +fn create_observer(name: &str) -> vir::vir_observer::Observers { + use std::sync::{Arc, Mutex}; + match name { + "test" => { + let o = Arc::new(Mutex::new(crate::test_observer::TestObserver::new())); + let vir: vir::vir_observer::VirObserverHandle = o.clone(); + let air: air::air_observer::AirObserverHandle = o.clone(); + let query_result: air::query_result_observer::QueryResultObserverHandle = + o.clone(); + vir::vir_observer::Observers { + vir: Some(vir), + air: Some(air), + query_result: Some(query_result), + } + } + // Dedicated single-trait observers: each populates only its own slot, + // proving a consumer couples nothing it does not implement. + "air-only" => { + let o = Arc::new(Mutex::new(crate::test_observer::AirOnlyObserver::new())); + let air: air::air_observer::AirObserverHandle = o; + vir::vir_observer::Observers { air: Some(air), ..Default::default() } + } + "query-result-only" => { + let o = Arc::new(Mutex::new(crate::test_observer::QueryResultOnlyObserver::new())); + let qr: air::query_result_observer::QueryResultObserverHandle = o; + vir::vir_observer::Observers { query_result: Some(qr), ..Default::default() } + } + "vir-only" => { + let o = Arc::new(Mutex::new(crate::test_observer::VirOnlyObserver::new())); + let vir: vir::vir_observer::VirObserverHandle = o; + vir::vir_observer::Observers { vir: Some(vir), ..Default::default() } + } + _ => vir::vir_observer::Observers::default(), + } +} + +fn create_observer_from_args(names: &[String]) -> vir::vir_observer::Observers { + if names.len() > 1 { + panic!("only one observer may be specified at a time; got: {:?}", names); + } + names.first().map_or_else(Default::default, |n| create_observer(n)) +} + +fn emit_observer_summaries(any: &dyn std::any::Any, reporter: &impl air::messages::Diagnostics) { + if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } else if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } else if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } else if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } +} + use rustc_span::def_id::LOCAL_CRATE; use rustc_span::source_map::SourceMap; use std::collections::{HashMap, HashSet, VecDeque}; @@ -1885,6 +1945,10 @@ impl Verifier { prover_choice, )?; + // Attach the same shared observer object to the spinoff context via its + // per-trait handles (real trait-object views of one object — no bridge). + air_context.set_observers(ctx.air_observer.clone(), ctx.query_result_observer.clone()); + // Write the span of spun-off query air_context.comment(&span.as_string); air_context.blank_line(); @@ -1962,6 +2026,13 @@ impl Verifier { profile_all_file_name.as_ref(), vir::def::ProverChoice::DefaultProver, )?; + + // Attach the same shared observer object to air::Context via its per-trait + // handles. All views point at one object; the Arc keeps it alive on both + // ctx (VIR callbacks during lowering) and air_context (AIR callbacks + + // query results during verification). + air_context.set_observers(ctx.air_observer.clone(), ctx.query_result_observer.clone()); + if self.args.solver_version_check { air_context.set_expected_solver_version(match self.args.solver { air::context::SmtSolver::Z3 => crate::consts::expected_z3_version().to_string(), @@ -2615,6 +2686,16 @@ impl Verifier { let (time_smt_init, time_smt_run) = air_context.get_time(); let rlimit_count = air_context.get_rlimit_count(); + // Emit observer summaries as diagnostic notes. Only one underlying object + // exists; try each handle (a single-trait observer populates only one). + if let Some(obs_cell) = &ctx.observer { + emit_observer_summaries(obs_cell.lock().unwrap().as_any(), reporter); + } else if let Some(obs_cell) = &ctx.air_observer { + emit_observer_summaries(obs_cell.lock().unwrap().as_any(), reporter); + } else if let Some(obs_cell) = &ctx.query_result_observer { + emit_observer_summaries(obs_cell.lock().unwrap().as_any(), reporter); + } + if let Some(journal) = resident { self.resident_buckets.push(crate::resident::RetainedBucket::new( bucket_id.clone(), @@ -2698,6 +2779,7 @@ impl Verifier { fndef_types, resolved_typs.unwrap(), self.args.debugger, + create_observer_from_args(&self.args.observers), )?; if self.args.log_all || self.args.log_args.log_vir_poly { let mut file = diff --git a/source/rust_verify_test/tests/common/mod.rs b/source/rust_verify_test/tests/common/mod.rs index c1210d5cea..dd4d54ee41 100644 --- a/source/rust_verify_test/tests/common/mod.rs +++ b/source/rust_verify_test/tests/common/mod.rs @@ -324,6 +324,9 @@ pub fn run_verus( } else if *option == "-V difficulty" { verus_args.push("-V".to_string()); verus_args.push("difficulty".to_string()); + } else if *option == "-V axiom-usage-info" { + verus_args.push("-V".to_string()); + verus_args.push("axiom-usage-info".to_string()); } else if *option == "-V spinoff-all" { verus_args.push("-V".to_string()); verus_args.push("spinoff-all".to_string()); @@ -344,6 +347,14 @@ pub fn run_verus( verus_args.extend(["-V".to_string(), format!("tla-export={module}")]); } else if let Some(dir) = option.strip_prefix("--log-dir ") { verus_args.extend(["--log-dir".to_string(), dir.to_string()]); + } else if option.starts_with("observers=") || option.starts_with("observer=") { + verus_args.push("-V".to_string()); + if option.starts_with("observer=") && !option.starts_with("observers=") { + // Normalize singular to plural form + verus_args.push(format!("observers={}", &option["observer=".len()..])); + } else { + verus_args.push(option.to_string()); + } } else { panic!("option '{}' not recognized by test harness", option); } diff --git a/source/rust_verify_test/tests/observer.rs b/source/rust_verify_test/tests/observer.rs new file mode 100644 index 0000000000..82224baa16 --- /dev/null +++ b/source/rust_verify_test/tests/observer.rs @@ -0,0 +1,1062 @@ +//! Observer e2e tests with strong oracles. +//! +//! Shared VC-shape seed corpus lives in `vc_shapes` (this branch), so all three layers' +//! suites can drive the same programs. This file adds event-trace oracles over selected seeds. +//! +//! Coverage matrix (+ = positive check, 0 = negative check): +//! +//! ```text +//! | loop | mut | valid | spec | break | for | inv | reveal | bvec | +//! ------------------------------------|------|------|-------|------|-------|------|------|--------|------| +//! on_krate (function names) | + | + | + | + | | | | | | +//! on_krate (datatype names) | + | + | | | | | | | | +//! on_havoc | + | 0 | 0 | 0 | + | + | + | | | +//! on_assign (names) | + | + | 0 | 0 | + | | + | | | +//! on_branch_merge | + | 0 | 0 | 0 | + | 0 | 0 | | | +//! on_break_merge | 0 | 0 | 0 | 0 | + | 0 | 0 | | | +//! on_variable_def (names) | + | | 0 | 0 | | | | | | +//! on_for_loop_var (ghost, user) | 0 | 0 | 0 | 0 | 0 | + | 0 | | | +//! on_reveal_string | | | | | | | | + | | +//! on_quantifier_binder (names) | 0 | + | 0 | + | 0 | 0 | 0 | | | +//! make_assert_id(Ensures) | + | + | + | + | + | | | | | +//! make_assert_id(LoopInvariant) | + | | | | + | | + | | | +//! make_assert_id(DecreasesCheck) | + | | | | + | | + | | | +//! on_function_lowered | + | + | + | + | + | | + | | | +//! on_query_lowered (count) | + | + | + | + | + | | + | | | +//! on_query_lowered (snapshots) | + | | + | | | | | | | +//! on_lambda_decl (names) | 0 | 0 | 0 | + | 0 | 0 | 0 | | | +//! on_choose_decl (names) | 0 | 0 | 0 | + | 0 | 0 | 0 | | | +//! check_valid_result(Invalid) | + | + | 0 | + | + | | + | + | + | +//! check_valid_result(Valid) | + | | + | | | | | | | +//! check_valid_result(Timeout) | | | | | | | | TODO | | +//! invalid model_defs size | + | + | | + | | | + | | | +//! eval_bool_expr during Invalid | + | | | | | | | | | +//! ``` + +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; +mod vc_shapes; + +// ── JSON parsing (mirrors TestObserver data model) ── + +struct D { + krate_function_names: Vec, + krate_datatype_names: Vec, + havocs: Vec, + assigns: Vec, + branch_merges: usize, + break_merges: usize, + variable_defs: Vec, + for_loop_vars: Vec<(String, String)>, + reveal_strings: Vec, + quantifier_binders: Vec, + assert_id_kinds: Vec, + function_lowered: usize, + query_lowered: usize, + query_snapshot_counts: Vec, + version_correlations: Vec<(String, u32, String)>, + lambda_decls: Vec, + choose_decls: Vec, + check_valid_invalid: usize, + check_valid_valid: usize, + check_valid_timeout: usize, + check_valid_invalid_model_size: Vec, + eval_expr_results: Vec>, + binder_decls: Vec, + breakable_count: usize, + break_count: usize, + valid_assert_id_counts: Vec, + valid_used_axiom_counts: Vec>, + pre_body_binders: Vec, + post_body_binders: Vec, + events: Vec, +} + +fn strings(s: &str) -> Vec { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1].split(',').map(|i| i.trim().trim_matches('"').to_string()).collect() +} +fn usizes(s: &str) -> Vec { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1].split(',').filter_map(|i| i.trim().parse().ok()).collect() +} +fn opt_usizes(s: &str) -> Vec> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1].split(',').map(|i| i.trim().parse::().ok()).collect() +} + +fn opt_bools(s: &str) -> Vec> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1] + .split(',') + .map(|i| match i.trim() { + "true" => Some(true), + "false" => Some(false), + _ => None, + }) + .collect() +} +fn nested_strings(s: &str) -> Vec> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + let inner = &s[1..s.len() - 1]; + let mut result = vec![]; + let mut depth = 0; + let mut start = 0; + for (i, c) in inner.char_indices() { + match c { + '[' => { + if depth == 0 { + start = i; + } + depth += 1; + } + ']' => { + depth -= 1; + if depth == 0 { + result.push(strings(&inner[start..=i])); + } + } + _ => {} + } + } + result +} +fn parse_version_correlations(s: &str) -> Vec<(String, u32, String)> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + // Format: [["name",line,"kind"],...] + let mut result = vec![]; + let inner = &s[1..s.len() - 1]; + let mut depth = 0; + let mut start = 0; + for (i, c) in inner.char_indices() { + match c { + '[' => { + if depth == 0 { + start = i; + } + depth += 1; + } + ']' => { + depth -= 1; + if depth == 0 { + let triple = &inner[start + 1..i]; + let parts: Vec<&str> = triple.splitn(3, ',').collect(); + if parts.len() == 3 { + let name = parts[0].trim().trim_matches('"').to_string(); + let line: u32 = parts[1].trim().parse().unwrap_or(0); + let kind = parts[2].trim().trim_matches('"').to_string(); + result.push((name, line, kind)); + } + } + } + _ => {} + } + } + result +} +fn string_pairs(s: &str) -> Vec<(String, String)> { + let nested = nested_strings(s); + nested + .into_iter() + .map(|v| { + assert_eq!(v.len(), 2); + (v[0].clone(), v[1].clone()) + }) + .collect() +} +fn val<'a>(json: &'a str, key: &str) -> &'a str { + let needle = format!("\"{}\":", key); + let start = json.find(&needle).unwrap_or_else(|| panic!("key '{}' not found", key)); + let rest = &json[start + needle.len()..]; + if rest.starts_with("[[") || rest.starts_with("[]") { + // nested array — find matching outer ] + let mut depth = 0; + for (i, c) in rest.char_indices() { + match c { + '[' => depth += 1, + ']' => { + depth -= 1; + if depth == 0 { + return &rest[..=i]; + } + } + _ => {} + } + } + rest + } else if rest.starts_with('[') { + &rest[..rest.find(']').unwrap() + 1] + } else { + let end = rest.find(|c: char| c == ',' || c == '}').unwrap_or(rest.len()); + rest[..end].trim() + } +} + +fn parse_note(note_text: &str) -> D { + let json = note_text + .strip_prefix("OBSERVER:") + .or_else(|| { + // Handle OBSERVER_N: prefix for composite + note_text.find(':').and_then(|i| { + if note_text[..i].starts_with("OBSERVER_") { + Some(¬e_text[i + 1..]) + } else { + None + } + }) + }) + .unwrap_or(note_text); + D { + krate_function_names: strings(val(json, "krate_function_names")), + krate_datatype_names: strings(val(json, "krate_datatype_names")), + havocs: strings(val(json, "havocs")), + assigns: strings(val(json, "assigns")), + branch_merges: val(json, "branch_merges").parse().unwrap(), + break_merges: val(json, "break_merges").parse().unwrap(), + variable_defs: strings(val(json, "variable_defs")), + for_loop_vars: string_pairs(val(json, "for_loop_vars")), + reveal_strings: strings(val(json, "reveal_strings")), + quantifier_binders: strings(val(json, "quantifier_binders")), + assert_id_kinds: strings(val(json, "assert_id_kinds")), + function_lowered: val(json, "function_lowered").parse().unwrap(), + query_lowered: val(json, "query_lowered").parse().unwrap(), + query_snapshot_counts: usizes(val(json, "query_snapshot_counts")), + version_correlations: parse_version_correlations(val(json, "version_correlations")), + lambda_decls: strings(val(json, "lambda_decls")), + choose_decls: strings(val(json, "choose_decls")), + check_valid_invalid: val(json, "check_valid_invalid").parse().unwrap(), + check_valid_valid: val(json, "check_valid_valid").parse().unwrap(), + check_valid_timeout: val(json, "check_valid_timeout").parse().unwrap(), + check_valid_invalid_model_size: usizes(val(json, "check_valid_invalid_model_size")), + eval_expr_results: opt_bools(val(json, "eval_expr_results")), + binder_decls: strings(val(json, "binder_decls")), + breakable_count: val(json, "breakable_count").parse().unwrap(), + break_count: val(json, "break_count").parse().unwrap(), + valid_assert_id_counts: usizes(val(json, "valid_assert_id_counts")), + valid_used_axiom_counts: opt_usizes(val(json, "valid_used_axiom_counts")), + pre_body_binders: strings(val(json, "pre_body_binders")), + post_body_binders: strings(val(json, "post_body_binders")), + events: strings(val(json, "events")), + } +} + +fn parse(err: &TestErr) -> D { + let note = err + .notes + .iter() + .find_map(|n| { + let t = n.rendered.strip_prefix("note: ").unwrap_or(&n.rendered); + t.strip_prefix("OBSERVER:").map(|_| t.to_string()) + }) + .expect("OBSERVER note not found"); + parse_note(¬e) +} + +fn has(v: &[String], s: &str) -> bool { + v.contains(&s.to_string()) +} +fn count(v: &[String], s: &str) -> usize { + v.iter().filter(|x| *x == s).count() +} + +// Find a diagnostic note beginning with `prefix` (e.g. "AIROBS:", "QROBS:", "VIROBS:"). +fn find_note(err: &TestErr, prefix: &str) -> String { + err.notes + .iter() + .find_map(|n| { + let t = n.rendered.strip_prefix("note: ").unwrap_or(&n.rendered); + if t.starts_with(prefix) { Some(t.to_string()) } else { None } + }) + .unwrap_or_else(|| { + panic!( + "{} note not found; notes: {:?}", + prefix, + err.notes.iter().map(|n| n.rendered.clone()).collect::>() + ) + }) +} +// Assert NO note begins with `prefix` (zero-overhead / decoupling checks). +fn no_note(err: &TestErr, prefix: &str) -> bool { + !err.notes.iter().any(|n| { + let t = n.rendered.strip_prefix("note: ").unwrap_or(&n.rendered); + t.starts_with(prefix) + }) +} +// Index of first event exactly equal to `tag`. +fn idx(events: &[String], tag: &str) -> Option { + events.iter().position(|e| e == tag) +} +// Index of first event starting with `prefix` (for tags carrying a payload). +fn idx_pfx(events: &[String], prefix: &str) -> Option { + events.iter().position(|e| e.starts_with(prefix)) +} + +// ── Tests ── + +test_verify_one_file_with_options! { + #[test] + test_observer_loop ["observers=test"] => verus_code! { + fn test_loop(n: u64) + requires n > 0 + ensures false + { + let mut x: u64 = 0; + let mut i: u64 = 0; + while i < n + invariant i <= n, x >= 0, + decreases n - i + { + x = if i % 2 == 0 { x + 1 } else { x + 2 }; + i = i + 1; + } + } + } => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "test_loop"), "got {:?}", d.krate_function_names); + assert!(has(&d.krate_datatype_names, "tuple0"), "got {:?}", d.krate_datatype_names); + assert!(has(&d.assigns, "x@") && has(&d.assigns, "i@"), "got {:?}", d.assigns); + assert_eq!(d.branch_merges, 2); + assert!(has(&d.variable_defs, "x@") && has(&d.variable_defs, "i@"), "got {:?}", d.variable_defs); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "DecreasesCheck"), "got {:?}", d.assert_id_kinds); + assert_eq!(d.function_lowered, 2); + assert!(d.query_lowered >= 2); + assert!(!d.query_snapshot_counts.is_empty()); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_valid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + assert!(d.eval_expr_results.iter().any(|r| *r == Some(true)), + "eval_bool_expr(true) should return Some(true), got {:?}", d.eval_expr_results); + // Version correlations: loop-modified variables have havoc and assign entries + assert!(!d.version_correlations.is_empty(), + "loop should produce version correlations"); + assert!(d.version_correlations.iter().any(|(_, _, k)| k == "Havoc"), + "should have Havoc correlation from loop entry"); + assert!(d.version_correlations.iter().any(|(_, _, k)| k == "Assign"), + "should have Assign correlation from loop body"); + // x should have correlations with distinct lines + let x_corr: Vec<_> = d.version_correlations.iter() + .filter(|(v, _, _)| v.contains("x")).collect(); + assert!(x_corr.len() >= 2, + "x should have >= 2 correlations, got {}", x_corr.len()); + for (v, line, _) in &d.version_correlations { + assert!(*line > 0, "{} has line 0", v); + } + let x_lines: std::collections::HashSet = + x_corr.iter().map(|(_, l, _)| *l).collect(); + assert!(x_lines.len() >= 2, + "x should have >= 2 distinct lines, got {:?}", x_lines); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert_eq!(d.break_merges, 0); + assert!(d.for_loop_vars.is_empty()); + assert!(d.quantifier_binders.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_mut_ref ["observers=test"] => verus_code! { + struct Pair { a: u64, b: u64 } + spec fn is_positive(x: int) -> bool { x >= 0 } + fn test_mut(p: &mut Pair, x: &mut u64) + requires old(p).a < 100, *old(x) < 100, + forall|i: int| #[trigger] is_positive(i) ==> i >= 0, + ensures (*final(p)).a == old(p).a + 1, *final(x) == *old(x) + 1, + { + p.a = p.a + 1; + *x = *x + 2; + } + } => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_datatype_names, "Pair"), "got {:?}", d.krate_datatype_names); + assert!(has(&d.krate_function_names, "test_mut") && has(&d.krate_function_names, "is_positive"), + "got {:?}", d.krate_function_names); + assert!(has(&d.assigns, "p!") && has(&d.assigns, "x!"), "got {:?}", d.assigns); + assert!(has(&d.quantifier_binders, "i$"), "got {:?}", d.quantifier_binders); + assert_eq!(count(&d.assert_id_kinds, "Ensures"), 2, "got {:?}", d.assert_id_kinds); + assert_eq!(d.function_lowered, 2); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + // Negatives + assert!(d.havocs.is_empty()); + assert_eq!(d.branch_merges, 0); + assert_eq!(d.break_merges, 0); + assert!(d.for_loop_vars.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_valid ["observers=test"] => verus_code! { + fn add_one(x: u64) -> (r: u64) + requires x < 100 + ensures r == x + 1 + { x + 1 } + } => Ok(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "add_one"), "got {:?}", d.krate_function_names); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(!d.query_snapshot_counts.is_empty()); + assert!(d.check_valid_valid >= 1); + assert_eq!(d.check_valid_invalid, 0); + // No loops → no version correlations + assert!(d.version_correlations.is_empty(), + "non-mutating function should have no version correlations, got {:?}", + d.version_correlations); + // Negatives + assert!(d.havocs.is_empty()); + assert_eq!(d.branch_merges, 0); + assert_eq!(d.break_merges, 0); + assert!(d.for_loop_vars.is_empty()); + assert!(d.quantifier_binders.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_spec ["observers=test"] => verus_code! { + use vstd::prelude::*; + spec fn has_pos(s: Seq) -> bool { + exists|i: int| 0 <= i < s.len() && s[i] > 0 + } + proof fn test_spec(s: Seq) + requires s.len() > 0, + s.map(|_idx: int, x: int| x + 1).len() > 0, + has_pos(s), + ensures false + {} + } => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "has_pos"), "got {:?}", d.krate_function_names); + assert!(has(&d.krate_function_names, "test_spec"), "got {:?}", d.krate_function_names); + // Lambda from s.map(|...|...) + assert!(!d.lambda_decls.is_empty(), "should have lambda decls, got {:?}", d.lambda_decls); + assert!(d.lambda_decls.iter().any(|n| n.contains("lambda")), "got {:?}", d.lambda_decls); + // Quantifier binder + assert!(!d.quantifier_binders.is_empty(), "got {:?}", d.quantifier_binders); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + // Negatives + assert!(d.havocs.is_empty()); + assert_eq!(d.break_merges, 0); + assert!(d.for_loop_vars.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_break ["observers=test"] => verus_code! { + use vstd::prelude::*; + fn find(v: &Vec, target: u64) -> (found: bool) + ensures !found // wrong + { + let mut found = false; + let mut i: usize = 0; + while i < v.len() + invariant + i <= v.len(), + !found, + decreases v.len() - i + { + if v[i] == target { + found = true; + break; + } + i = i + 1; + } + found + } + } => Err(err) => { + let d = parse(&err); + // Break: loop isolation may prevent break_merge from firing, + // but branch_merges should increase from the if + break structure + assert!(d.branch_merges > 0, "if should trigger branch_merge, got {}", d.branch_merges); + // Assigns + assert!(has(&d.assigns, "found@"), "got {:?}", d.assigns); + assert!(has(&d.assigns, "i@"), "got {:?}", d.assigns); + // Assert ID kinds + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "DecreasesCheck"), "got {:?}", d.assert_id_kinds); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert!(d.for_loop_vars.is_empty()); + // quantifier_binders may be non-empty due to vstd internals + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_for_loop ["observers=test"] => verus_code! { + use vstd::prelude::*; + fn sum_first(v: &Vec, n: usize) -> (s: u64) + requires n <= v.len(), n < 100, + forall|i: int| 0 <= i < v.len() ==> v[i] < 100, + ensures false + { + let mut s: u64 = 0; + for i in iter: 0..n + invariant + s <= 100 * i, + n < 100, + n <= v.len(), + forall|j: int| 0 <= j < v.len() ==> v[j] < 100, + { + s = s + v[i]; + } + s + } + } => Err(err) => { + let d = parse(&err); + assert!(!d.for_loop_vars.is_empty(), "for-loop should be detected"); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert_eq!(d.break_merges, 0); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_loop_invariant ["observers=test"] => verus_code! { + fn bad_loop(n: u64) + requires n > 0 + ensures false + { + let mut i: u64 = 0; + while i < n + invariant i <= n, + decreases n - i + { + i = i + 1; + } + } + } => Err(err) => { + let d = parse(&err); + // Assert ID kinds: LoopInvariant and DecreasesCheck are primary + assert!(count(&d.assert_id_kinds, "LoopInvariant") >= 2, + "should have multiple LoopInvariant, got {:?}", d.assert_id_kinds); + assert!(count(&d.assert_id_kinds, "DecreasesCheck") >= 1, + "got {:?}", d.assert_id_kinds); + assert!(has(&d.assigns, "i@"), "got {:?}", d.assigns); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert!(d.for_loop_vars.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + assert!(d.quantifier_binders.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_bitvector ["observers=test"] => verus_code! { + proof fn test_bv(x: u32) by(bit_vector) + ensures x & 0xff == x + { } + } => Err(err) => { + let d = parse(&err); + assert!(d.query_lowered >= 1, + "bitvector query should reach observer, got {} queries", d.query_lowered); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_reveal_string ["observers=test"] => verus_code! { + use vstd::prelude::*; + use vstd::string::*; + fn test_reveal() + ensures false + { + let _s = "hello"; + proof { reveal_strlit("hello"); } + } + } => Err(err) => { + let d = parse(&err); + assert!(d.reveal_strings.contains(&"hello".to_string()), + "should record 'hello', got {:?}", d.reveal_strings); + assert!(d.check_valid_invalid >= 1); + } +} + +// TODO: test_observer_timeout — requires --rlimit CLI flag which the test harness +// doesn't currently support. Add rlimit support to common/mod.rs, then test with +// rlimit=1 and assert d.check_valid_timeout > 0. + +test_verify_one_file_with_options! { + #[test] + test_body_boundary ["observers=test"] => verus_code! { + use vstd::prelude::*; + + // requires has forall|x|, body has forall|y| + fn test_body_boundary(v: &Vec) + requires forall|x: int| 0 <= x < v.len() ==> v[x] < 100, + { + assert(forall|y: int| 0 <= y < v.len() ==> v[y] < 200) by { + // intentionally wrong bound to force failure + assume(false); + } + assert(false); // force verification failure + } + } => Err(err) => { + let d = parse(&err); + // x is in requires (pre-body), y is in body (post-body) + assert!(d.pre_body_binders.iter().any(|b| b.starts_with("x")), + "requires binder 'x' should be pre-body, got pre={:?}", d.pre_body_binders); + assert!(d.post_body_binders.iter().any(|b| b.starts_with("y")), + "body binder 'y' should be post-body, got post={:?}", d.post_body_binders); + // y should NOT appear in pre-body (it's only in the body assert) + assert!(!d.pre_body_binders.iter().any(|b| b.starts_with("y")), + "body binder 'y' should NOT be in pre-body, got pre={:?}", d.pre_body_binders); + } +} + +test_verify_one_file_with_options! { + + // ── §3.2 Cross-trait lifecycle sequencing (L1–L5) via the ordered trace ── + #[test] + test_lifecycle_sequencing ["observers=test"] => verus_code! { + fn seq_demo(n: u64) -> (r: u64) + requires n < 100, + ensures r == n, + { + let mut i: u64 = 0; + while i < n + invariant i <= n, + decreases n - i, + { i = i + 1; } + i + } + } => Ok(err) => { + let d = parse(&err); + let e = &d.events; + // L1: on_krate fires exactly once, before everything. + assert_eq!(e.first().map(|s| s.as_str()), Some("krate"), + "L1: krate must be first; events={:?}", e); + assert_eq!(count(e, "krate"), 1, "L1: krate exactly once; events={:?}", e); + // L2: on_body_lowering_start precedes on_function_lowered. + let body = idx(e, "body_start").expect("body_start present"); + let flow = idx(e, "function_lowered").expect("function_lowered present"); + assert!(body < flow, "L2: body_start before function_lowered; events={:?}", e); + // L4: some on_query_lowered precedes a check_valid result. + let q = idx(e, "query_lowered").expect("query_lowered present"); + let cv = idx_pfx(e, "check_valid:").expect("check_valid present"); + assert!(q < cv, "L4: query_lowered before check_valid; events={:?}", e); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1 VirObserver-only: functional coverage + decoupling proof ── + #[test] + test_vir_only_observer ["observers=vir-only"] => verus_code! { + fn vo(a: u64) -> (r: u64) + ensures r == a, + { + let x: u64 = a; + x + } + } => Ok(err) => { + // Decoupling: only VIROBS is emitted — no all-three / air / query-result notes. + assert!(no_note(&err, "OBSERVER:"), "vir-only must not emit all-three note"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "QROBS:"), + "vir-only must not emit AIR/QR notes"); + let note = find_note(&err, "VIROBS:"); + let json = note.strip_prefix("VIROBS:").unwrap(); + let events = strings(val(json, "events")); + let fns = strings(val(json, "function_names")); + let flowered: usize = val(json, "function_lowered").parse().unwrap(); + assert!(has(&fns, "vo"), "function_names has vo; got {:?}", fns); + assert!(flowered >= 1, "function_lowered >= 1"); + assert_eq!(events.first().map(|s| s.as_str()), Some("krate"), + "krate first; events={:?}", events); + assert!(idx(&events, "function_lowered").is_some(), "events={:?}", events); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1 AirObserver-only: functional coverage + decoupling proof ── + #[test] + test_air_only_observer ["observers=air-only"] => verus_code! { + proof fn ao(x: u64) + requires x < 10, + ensures x < 20, + { } + } => Ok(err) => { + assert!(no_note(&err, "OBSERVER:"), "air-only must not emit all-three note"); + assert!(no_note(&err, "VIROBS:") && no_note(&err, "QROBS:"), + "air-only must not emit VIR/QR notes"); + let note = find_note(&err, "AIROBS:"); + let json = note.strip_prefix("AIROBS:").unwrap(); + let events = strings(val(json, "events")); + let ql: usize = val(json, "query_lowered").parse().unwrap(); + let ax: usize = val(json, "axiom_decls").parse().unwrap(); + assert!(ql >= 1, "query_lowered >= 1; events={:?}", events); + assert!(ax >= 1, "axiom_decls >= 1"); + assert!(idx(&events, "query_lowered").is_some(), "events={:?}", events); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1 QueryResultObserver-only, Invalid: eval_expr liveness + decoupling ── + #[test] + test_query_result_only_invalid ["observers=query-result-only"] => verus_code! { + proof fn bad() + ensures false, + { } + } => Err(err) => { + assert!(no_note(&err, "OBSERVER:"), "qr-only must not emit all-three note"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "VIROBS:"), + "qr-only must not emit AIR/VIR notes"); + let note = find_note(&err, "QROBS:"); + let json = note.strip_prefix("QROBS:").unwrap(); + let invalid: usize = val(json, "invalid").parse().unwrap(); + let events = strings(val(json, "events")); + let eval = opt_bools(val(json, "eval_expr_results")); + assert!(invalid >= 1, "invalid >= 1"); + assert!(idx(&events, "check_valid:Invalid").is_some(), "events={:?}", events); + assert!(!eval.is_empty(), "eval_expr worked during Invalid; got {:?}", eval); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1/§3.4 QueryResultObserver-only, Valid: no unsat core (capabilities live on AirObserver) ── + // ── §3.1 QueryResultObserver-only, Valid: sees the Valid result + decoupling ── + #[test] + test_query_result_only_valid ["observers=query-result-only"] => verus_code! { + proof fn good(x: u64) + requires x < 10, + ensures x < 20, + { } + } => Ok(err) => { + // Decoupling: only QROBS emitted. + assert!(no_note(&err, "OBSERVER:"), "qr-only must not emit all-three note"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "VIROBS:"), + "qr-only must not emit AIR/VIR notes"); + let note = find_note(&err, "QROBS:"); + let json = note.strip_prefix("QROBS:").unwrap(); + let valid: usize = val(json, "valid").parse().unwrap(); + let events = strings(val(json, "events")); + assert!(valid >= 1, "valid >= 1"); + assert!(events.iter().any(|e| e == "check_valid:Valid"), + "events should contain check_valid:Valid; got {:?}", events); + } +} + +test_verify_one_file_with_options! { + + // ── §3.5 Zero-overhead: no observer flag => no observer notes at all ── + #[test] + test_no_observer_zero_overhead [] => verus_code! { + proof fn noop(x: u64) + requires x < 10, + ensures x < 20, + { } + } => Ok(err) => { + assert!(no_note(&err, "OBSERVER:"), "no all-three note without flag"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "QROBS:") && no_note(&err, "VIROBS:"), + "no per-trait notes without flag"); + } +} + +// ---- event-trace oracles over the shared VC-shape corpus ------------------------ + +test_verify_one_file_with_options! { + // covers (VO axis): nested-loops seed drives transitive havoc + all three assert-id kinds. + #[test] + test_observer_seed_nested_loops ["observers=test"] => vc_shapes::seed_nested_loops() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "test"), "got {:?}", d.krate_function_names); + // Both loop counters are havoced/assigned; outer + inner invariants + decreases fire. + assert!(has(&d.assigns, "i@") && has(&d.assigns, "j@"), "got {:?}", d.assigns); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "DecreasesCheck"), "got {:?}", d.assert_id_kinds); + assert!(d.query_lowered >= 2, "nested loops -> multiple isolated queries"); + } +} + +// ---- Uncovered-callback assertions, result-payload semantics, and neutrality ---- + +test_verify_one_file_with_options! { + // covers (VO axis): on_quantifier_binder_decl — a choose binding declares its binder. + #[test] + test_observer_binder_decl ["observers=test"] => verus_code! { + spec fn p(i: int) -> bool; + proof fn f() { + let w = choose|i: int| p(i); + assert(p(w)); + } + } => Err(err) => { + let d = parse(&err); + assert!(!d.binder_decls.is_empty(), + "choose must declare a quantifier binder; got {:?}", d.binder_decls); + assert!(!d.choose_decls.is_empty(), "got {:?}", d.choose_decls); + } +} + +test_verify_one_file_with_options! { + // covers (VO axis): on_check_valid_result Invalid payload — the live evaluator's + // three-way contract: Some(true) / Some(false) / None per failing query. + #[test] + test_observer_eval_three_way ["observers=test"] => verus_code! { + proof fn f(x: u64) { + assert(x < 5); + } + } => Err(err) => { + let d = parse(&err); + assert!(d.check_valid_invalid >= 1); + // Recorded in triples per Invalid: eval(true), eval(false), eval(non-bool). + assert!(d.eval_expr_results.chunks(3).any(|c| + c == [Some(true), Some(false), None]), + "expected a [Some(true), Some(false), None] triple; got {:?}", d.eval_expr_results); + } +} + +test_verify_one_file_with_options! { + // covers (VO axis over corpus): guarded match — merges and per-arm assigns observed. + #[test] + test_observer_seed_match_guard ["observers=test"] => vc_shapes::seed_match_guard() + => Err(err) => { + let d = parse(&err); + assert!(d.branch_merges >= 1, "a match produces branch merges; got {}", d.branch_merges); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + } +} + +test_verify_one_file_with_options! { + // covers (VO axis over corpus): early return — ensures obligation still identified. + #[test] + test_observer_seed_early_return ["observers=test"] => vc_shapes::seed_early_return() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(d.query_lowered >= 1); + } +} + +/// Behavior-neutrality differential: for every corpus seed, verification outcomes are +/// identical with and without observers registered (same error count, same primary spans). +#[test] +fn test_observer_neutrality_differential() { + let seeds: Vec<(&str, String)> = vec![ + ("match_nested", vc_shapes::seed_match_nested()), + ("match_in_loop_inv", vc_shapes::seed_match_in_loop_inv()), + ("loop_break", vc_shapes::seed_loop_break()), + ("branch_merge", vc_shapes::seed_branch_merge()), + ("param_mutated_before_loop", vc_shapes::seed_param_mutated_before_loop()), + ("nested_loops", vc_shapes::seed_nested_loops()), + ("for_loop", vc_shapes::seed_for_loop()), + ("match_guard", vc_shapes::seed_match_guard()), + ("bare_loop", vc_shapes::seed_bare_loop()), + ("early_return", vc_shapes::seed_early_return()), + ("continue", vc_shapes::seed_continue()), + ("break_labeled", vc_shapes::seed_break_labeled()), + ("loop_break_noniso", vc_shapes::seed_loop_break_noniso()), + ("nested_loops_noniso", vc_shapes::seed_nested_loops_noniso()), + ("break_labeled_noniso", vc_shapes::seed_break_labeled_noniso()), + ("expand_ensures", vc_shapes::seed_expand_ensures()), + ("truncate_cast", vc_shapes::seed_truncate_cast()), + ]; + for (name, code) in seeds { + let plain = verify_one_file(&format!("neutral_{}_plain", name), code.clone(), &[]); + let observed = verify_one_file(&format!("neutral_{}_obs", name), code, &["observers=test"]); + let (p, o) = match (&plain, &observed) { + (Ok(p), Ok(o)) | (Err(p), Err(o)) | (Ok(p), Err(o)) | (Err(p), Ok(o)) => (p, o), + }; + assert_eq!( + plain.is_err(), + observed.is_err(), + "seed {}: overall outcome differs with observers", + name + ); + assert_eq!( + p.errors.len(), + o.errors.len(), + "seed {}: error count differs with observers", + name + ); + // The corpus programs are small; none should hit the solver resource limit, so the + // result channel must report no Timeout for any of them. + let d = parse(o); + assert_eq!(d.check_valid_timeout, 0, "seed {}: unexpected solver timeout", name); + for (a, b) in p.errors.iter().zip(o.errors.iter()) { + assert_eq!( + a.rendered.lines().next(), + b.rendered.lines().next(), + "seed {}: error text differs with observers", + name + ); + } + } +} + +test_verify_one_file_with_options! { + // covers: S-continue — the loop's invariants (and decreases) are asserted at the + // continue site; the too-strong invariant fails there. + #[test] + test_observer_seed_continue ["observers=test"] => vc_shapes::seed_continue() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + // Isolated lowering (the default): loops never appear as Breakable regions. + assert_eq!(d.breakable_count, 0, "got {}", d.breakable_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-break-labeled — `break 'outer` asserts the TARGET loop's invariants at + // the break site; the outer invariant fails there. + #[test] + test_observer_seed_break_labeled ["observers=test"] => vc_shapes::seed_break_labeled() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert_eq!(d.breakable_count, 0, "got {}", d.breakable_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-loop-noniso — without loop isolation the loop lowers into the enclosing + // query as a labeled Breakable region with Break jumps. + #[test] + test_observer_seed_loop_break_noniso ["observers=test"] => vc_shapes::seed_loop_break_noniso() + => Err(err) => { + let d = parse(&err); + assert!(d.breakable_count >= 1, "non-isolated loop must lower as Breakable; got {}", + d.breakable_count); + assert!(d.break_count >= 1, "got {}", d.break_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-break-labeled-noniso — a labeled break without isolation still lowers the + // loops as Breakable regions with Break jumps (two nested loops -> two of each). + #[test] + test_observer_seed_break_labeled_noniso ["observers=test"] => vc_shapes::seed_break_labeled_noniso() + => Err(err) => { + let d = parse(&err); + assert!(d.breakable_count >= 2, "nested non-isolated loops -> Breakable regions; got {}", + d.breakable_count); + assert!(d.break_count >= 1, "labeled break emits a Break; got {}", d.break_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-nested-noniso — nested loops without isolation: nested Breakable regions + // in a single query. + #[test] + test_observer_seed_nested_loops_noniso ["observers=test"] => vc_shapes::seed_nested_loops_noniso() + => Err(err) => { + let d = parse(&err); + assert!(d.breakable_count >= 2, "two nested Breakable regions; got {}", + d.breakable_count); + assert!(d.break_count >= 2, "got {}", d.break_count); + } +} + +test_verify_one_file_with_options! { + // A discharged (unsat) query is observed with the same shape callbacks as a failing one, + // and its result callback names the obligations it checked: two postconditions and one + // loop invariant here, none of which fail. + #[test] + test_observer_valid_reports_obligations ["observers=test"] => verus_code! { + fn test(n: u64) -> (r: u64) + requires n < 100 + ensures r >= n, r < 200 + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + i = i + 1; + } + i + 1 + } + } => Ok(err) => { + let d = parse(&err); + assert!(d.check_valid_valid >= 1, "got {}", d.check_valid_valid); + assert_eq!(d.check_valid_invalid, 0); + // Shape callbacks fire regardless of outcome. + assert!(d.query_lowered >= 1); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + // At least one discharged query reported labeled obligations. + assert!(d.valid_assert_id_counts.iter().any(|&c| c >= 1), + "a Valid result should name its assertion ids; got {:?}", d.valid_assert_id_counts); + // Usage reporting is opt-in: not enabled here, so no core is attached. + assert!(d.valid_used_axiom_counts.iter().all(|c| c.is_none()), + "no usage info without the flag; got {:?}", d.valid_used_axiom_counts); + } +} + +test_verify_one_file_with_options! { + // With usage reporting enabled, a discharged query carries the unsat core: the named + // axioms the solver used. A call to a lemma with a broadcast-style axiom makes the core + // non-empty. + #[test] + test_observer_valid_usage_info ["observers=test", "-V axiom-usage-info"] => verus_code! { + spec fn f(x: int) -> int; + proof fn lemma_f(x: int) + ensures f(x) > 0 + { + admit(); + } + proof fn test(x: int) { + lemma_f(x); + assert(f(x) > 0); + } + } => Ok(err) => { + let d = parse(&err); + assert!(d.check_valid_valid >= 1, "got {}", d.check_valid_valid); + assert!(d.valid_used_axiom_counts.iter().any(|c| c.is_some()), + "usage info should be attached when enabled; got {:?}", d.valid_used_axiom_counts); + } +} diff --git a/source/rust_verify_test/tests/vc_shapes/mod.rs b/source/rust_verify_test/tests/vc_shapes/mod.rs new file mode 100644 index 0000000000..6a92f602b3 --- /dev/null +++ b/source/rust_verify_test/tests/vc_shapes/mod.rs @@ -0,0 +1,381 @@ +//! VC-shape seed corpus, shared by end-to-end suites. +//! +//! Each function returns a small Verus program with a forced verification failure. The +//! `covers:` tags name the shape(s) a seed exercises, using these prefixes: +//! +//! - `S-` statement/control structure (the shapes verification-condition generation composes: +//! branches, matches, loops, breaks, early returns, ...) +//! - `E-` expression grammar (expression forms reachable from source) +//! - `I-` encoding idioms (naming/encoding conventions of the lowering: temporaries, +//! variable versions, old/final values, contract functions, ...) +//! - `X-` interactions (idiom x structure combinations that share per-query state, +//! e.g. temporaries assigned per match arm) +//! +//! Seeds are APPEND-ONLY: once any suite pins an expected-output oracle to a seed, the seed's +//! program text is immutable — behavior changes get a new seed function. This keeps oracles in +//! all consuming suites stable against edits made in any one of them. + +// Not every consumer uses every seed. +#![allow(dead_code)] + +use rust_verify_test_macros::verus_code; + +/// covers: S-match-nested +pub fn seed_match_nested() -> String { + verus_code! { + #[allow(unused)] + enum Outer { A, B } + #[allow(unused)] + enum Inner { X, Y } + + proof fn test(o: Outer, i: Inner, v: int) + requires v > 0 + { + match o { + Outer::A => { + match i { + Inner::X => { + assert(v > 1000); + } + _ => {} + } + } + _ => {} + } + } + } +} + +/// covers: S-match-in-loop, X-switch-in-loop (failing loop invariant, so the match arms are +/// inside the failing query) +pub fn seed_match_in_loop_inv() -> String { + verus_code! { + #[allow(unused)] + enum Op { Add, Nop } + fn test(op: Op, n: u64) + requires n > 0 + { + let mut val: u64 = 0; + let mut i: u64 = 0; + while i < n + invariant i <= n, val == 0 + decreases n - i + { + match op { + Op::Add => { val = val + 1; } + Op::Nop => {} + } + i = i + 1; + } + } + } +} + +/// covers: S-loop-break (bare break inside while) +pub fn seed_loop_break() -> String { + verus_code! { + fn test(n: u64) + requires n > 10 + ensures false + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + if i == 5 { + break; + } + i = i + 1; + } + } + } +} + +/// covers: I-versions-merge, S-if-noelse +pub fn seed_branch_merge() -> String { + verus_code! { + proof fn test(cond: bool, v: int) + requires v < 100 + { + let mut x: int = v; + if cond { + x = x + 10; + } + assert(x > v); + } + } +} + +/// covers: X-old-loop, I-versions-mutation (param mutated before the loop) +pub fn seed_param_mutated_before_loop() -> String { + verus_code! { + fn test(n: u64) + requires n > 10 + ensures false + { + let mut x: u64 = n; + x = x + 1; + let mut i: u64 = 0; + while i < x + invariant i <= x + decreases x - i + { + i = i + 1; + } + } + } +} + +/// covers: S-nested-loops, X-versions-nested-loop (inner invariant fails) +pub fn seed_nested_loops() -> String { + verus_code! { + fn test(n: u64) + requires n > 0 + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + let mut j: u64 = 0; + while j < i + invariant j <= i, j < 5 + decreases i - j + { + j = j + 1; + } + i = i + 1; + } + } + } +} + +/// covers: S-for (ghost-iterator machinery) +pub fn seed_for_loop() -> String { + verus_code! { + use vstd::prelude::*; + fn test(v: &Vec) -> (sum: u64) + ensures sum == 0 + { + let mut sum: u64 = 0; + for x in v.iter() + invariant sum < 1000000u64, + { + sum = sum + 1u64; + } + sum + } + } +} + +/// covers: S-match-guard (arm with if-guard) +pub fn seed_match_guard() -> String { + verus_code! { + #[allow(unused)] + enum Kind { A, B } + proof fn test(k: Kind, v: int) -> (r: int) + ensures r > 0 + { + match k { + Kind::A if v > 10 => 1, + Kind::A => 0, + Kind::B => 2, + } + } + } +} + +/// covers: S-loop (bare loop with break) +/// (break-with-value is unreachable: Verus rejects "complex break expressions") +pub fn seed_bare_loop() -> String { + verus_code! { + fn test() -> (r: u64) + ensures r > 100 + { + let mut i: u64 = 0; + loop + invariant i <= 10, + decreases 10 - i, + { + if i >= 7 { + break; + } + i = i + 1; + } + i + } + } +} + +/// covers: S-return (early return before an unprovable postcondition) +pub fn seed_early_return() -> String { + verus_code! { + proof fn test(c: bool, v: int) -> (r: int) + ensures r > 10 + { + if c { + return v; + } + 20 + } + } +} + +/// covers: S-continue (loop invariants + decreases asserted at the continue site) +pub fn seed_continue() -> String { + verus_code! { + fn test(n: u64) + requires n > 0 + { + let mut i: u64 = 0; + let mut s: u64 = 0; + while i < n + invariant s >= i, i <= n + decreases n - i + { + i = i + 1; + if i % 2 == 0 { + continue; + } + s = s + 2; + } + } + } +} + +/// covers: S-break-labeled (the labeled target loop's invariants asserted at the break site) +pub fn seed_break_labeled() -> String { + verus_code! { + fn test(n: u64) + requires n > 10 + { + let mut i: u64 = 0; + let mut j: u64 = 0; + 'outer: while i < n + invariant i <= n, j <= 5 + decreases n - i + { + j = 0; + while j < 10 + invariant j <= 10 + decreases 10 - j + { + if j == 8 { + break 'outer; + } + j = j + 1; + } + i = i + 1; + } + } + } +} + +/// covers: S-loop-noniso (same program as seed_loop_break, lowered without loop isolation: +/// the query carries the loop as a labeled `Breakable`/`Break` region with inline +/// assume-false exits instead of a separate loop query) +pub fn seed_loop_break_noniso() -> String { + verus_code! { + #[verifier::loop_isolation(false)] + fn test(n: u64) + requires n > 10 + ensures false + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + if i == 5 { + break; + } + i = i + 1; + } + } + } +} + +/// covers: S-nested-noniso (nested loops without isolation: nested Breakable regions in +/// one query) +pub fn seed_nested_loops_noniso() -> String { + verus_code! { + #[verifier::loop_isolation(false)] + fn test(n: u64) + requires n > 0 + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + let mut j: u64 = 0; + while j < i + invariant j <= i, j < 5 + decreases i - j + { + j = j + 1; + } + i = i + 1; + } + } + } +} + +/// covers: I-expand (an ensures whose failing spec function expands into conjuncts under +/// --expand-errors, introducing expand% temporaries in the second lowering) +pub fn seed_expand_ensures() -> String { + verus_code! { + spec fn in_range(x: u64) -> bool { + x > 0 && x < 100 + } + fn test() -> (r: u64) + ensures in_range(r) + { + 0 + } + } +} + +/// covers: I-truncate (a truncating cast: the VC clips the value to the target width) +pub fn seed_truncate_cast() -> String { + verus_code! { + #[verifier::truncate] + fn test(x: u64) -> (r: u8) + ensures r as u64 == x + { + x as u8 + } + } +} + +/// covers: S-break-labeled-noniso (labeled `break 'outer` without loop isolation: the +/// break targets the outer Breakable region by label, exercising the labeled-break +/// encoding in a single query) +pub fn seed_break_labeled_noniso() -> String { + verus_code! { + #[verifier::loop_isolation(false)] + fn test(n: u64) + requires n > 10 + ensures false + { + let mut i: u64 = 0; + 'outer: while i < n + invariant i <= n + decreases n - i + { + let mut j: u64 = 0; + while j < 10 + invariant j <= 10 + decreases 10 - j + { + if j == 8 { + break 'outer; + } + j = j + 1; + } + i = i + 1; + } + } + } +} diff --git a/source/vir/src/context.rs b/source/vir/src/context.rs index 6d28e80b2c..3cbb12bcfd 100644 --- a/source/vir/src/context.rs +++ b/source/vir/src/context.rs @@ -154,10 +154,45 @@ pub struct Ctx { pub(crate) byte_string_hashes: RefCell>>>, // proof debug purposes pub debug: bool, + /// Observer for the verification pipeline. Three layers of indirection: + /// - `Arc`: shared between VIR `Ctx` (for lowering callbacks) and AIR + /// `Context` (for query/result callbacks) which have independent lifetimes. + /// - `Mutex`: callbacks require `&mut` through shared `Arc` references, and + /// an AIR context retained by a resident session must stay `Send`. + /// - `dyn VirObserver`: type-erased observer, shared with the AIR context's + /// own trait handles via the verifier's observer registry (all views point + /// at one object). + pub observer: Option, + /// AIR-level handles to the same shared observer object, carried here so the + /// verifier can attach them to each `air::Context` it builds (see verifier.rs). + pub air_observer: Option, + pub query_result_observer: Option< + air::query_result_observer::QueryResultObserverHandle, + >, pub arch_word_bits: ArchWordBits, } impl Ctx { + /// Call a callback on the observer if one is registered. + pub(crate) fn notify(&self, f: F) { + if let Some(obs) = &self.observer { + f(&mut *obs.lock().unwrap()); + } + } + + /// Ask the observer for an assert ID, or use the default (clone parent). + pub(crate) fn make_assert_id( + &self, + kind: &crate::vir_observer::AssertIdKind, + index: usize, + parent: &Option, + ) -> Option { + self.observer.as_ref().map_or_else( + || parent.clone(), + |obs| obs.lock().unwrap().make_assert_id(kind, index, parent), + ) + } + pub(crate) fn checking_spec_preconditions(&self) -> bool { match self.fun { Some(FunctionCtx { checking_spec_preconditions: true, .. }) => true, @@ -847,6 +882,7 @@ impl Ctx { fndef_types: Vec, resolved_typs: Vec, debug: bool, + observers: crate::vir_observer::Observers, ) -> Result { let name_ctxt = NameCtxt::new(); let mut datatype_is_transparent: HashMap = HashMap::new(); @@ -895,6 +931,19 @@ impl Ctx { opaque_type_map.insert(opaque_type.x.name.clone(), opaque_type.clone()); } + // Register the observer and deliver the krate. The observer receives the + // NameCtxt so it can compute AIR names consistently with lowering — both + // share the same NameCtxt instance, so crate-name interning decisions + // made here are reused during lowering. + let crate::vir_observer::Observers { + vir: observer, + air: air_observer, + query_result: query_result_observer, + } = observers; + if let Some(obs) = &observer { + obs.lock().unwrap().on_krate(&krate, &name_ctxt, &module.x.path.krate); + } + Ok(Ctx { module, datatype_is_transparent, @@ -923,6 +972,9 @@ impl Ctx { string_hashes, byte_string_hashes, debug, + observer, + air_observer, + query_result_observer, arch_word_bits: krate.arch.word_bits, opaque_type_map, }) diff --git a/source/vir/src/lib.rs b/source/vir/src/lib.rs index 21db18dc9c..f0337c1fb5 100644 --- a/source/vir/src/lib.rs +++ b/source/vir/src/lib.rs @@ -81,5 +81,6 @@ mod triggers_auto; mod unicode; pub mod user_defined_type_invariants; pub mod util; +pub mod vir_observer; mod visitor; pub mod well_formed; diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index d8f560f3f0..dea3653505 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -1582,6 +1582,9 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< } BndX::Quant(quant, binders, trigs, _) => { let expr = exp_to_expr(ctx, e, expr_ctxt)?; + for b in binders.iter() { + ctx.notify(|obs| obs.on_quantifier_binder(b, exp)); + } let mut invs: Vec = Vec::new(); for binder in binders.iter() { let typ_inv = typ_invariant( @@ -2130,6 +2133,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi let var = suffix_local_unique_id(&get_loc_var(dest)); ens_args.push(exp_to_expr(ctx, &dest, expr_ctxt)?); if !*is_init { + ctx.notify(|obs| obs.on_havoc(stm, &get_loc_var(dest))); let havoc = StmtX::Havoc(var); stmts.push(Arc::new(havoc)); } @@ -2270,8 +2274,8 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi stmts.append(&mut new_stmts); } } else { - for (span, ens, proof_note) in - state.post_condition_info.ens_exprs.clone().iter() + for (ens_idx, (span, ens, proof_note)) in + state.post_condition_info.ens_exprs.clone().iter().enumerate() { // The base_error should point to the return-statement or // return-expression. Augment with an additional label pointing @@ -2313,7 +2317,12 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi } }; - let ens_stmt = StmtX::Assert(assert_id.clone(), error, None, ens.clone()); + let ens_id = ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::Ensures, + ens_idx, + &assert_id, + ); + let ens_stmt = StmtX::Assert(ens_id, error, None, ens.clone()); stmts.push(Arc::new(ens_stmt)); } } @@ -2402,6 +2411,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi } StmX::Assign { lhs: Dest { dest, is_init: true }, rhs } => { let x = loc_is_var(dest).expect("is_init assign dest must be a variable"); + ctx.notify(|obs| obs.on_variable_def(stm, x)); stm_to_stmts(ctx, state, &assume_var(&stm.span, x, rhs))? } StmX::Assign { lhs: Dest { dest, is_init: false }, rhs } => { @@ -2473,6 +2483,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi false }; + ctx.notify(|obs| obs.on_assign(stm, &base_var)); let a = Arc::new(StmtX::Assign(suffix_local_unique_id(&base_var), value)); stmts.push(a); if fields.len() > 0 { @@ -2530,7 +2541,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi } else { error_with_label(&stm.span, "loop invariant not satisfied", "at this continue") }; - for (span, inv, msg, both) in invs.iter() { + for (inv_idx, (span, inv, msg, both)) in invs.iter().enumerate() { let mut error = base_error.secondary_label(span, "failed this invariant"); if let Some(msg) = msg { error = error.secondary_label(span, &**msg); @@ -2541,7 +2552,16 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi and use 'ensures' for what is true at the break)"; error = error.secondary_label(span, msg); } - stmts.push(Arc::new(StmtX::Assert(None, error, None, inv.clone()))); + stmts.push(Arc::new(StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::LoopInvariant, + inv_idx, + &None, + ), + error, + None, + inv.clone(), + ))); } let decrease = &loop_info.decrease; if !is_break && decrease.len() > 0 { @@ -2564,7 +2584,16 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi )?; let expr = exp_to_expr(ctx, &dec_exp, expr_ctxt)?; let error = error(&stm.span, crate::def::DEC_FAIL_LOOP_CONTINUE); - let dec_stmt = StmtX::Assert(None, error, None, expr); + let dec_stmt = StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::DecreasesCheck, + 0, + &None, + ), + error, + None, + expr, + ); stmts.push(Arc::new(dec_stmt)); } } @@ -2610,6 +2639,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi let lblock = Arc::new(StmtX::Block(Arc::new(lhss))); let rblock = Arc::new(StmtX::Block(Arc::new(rhss))); let mut stmts = vec![Arc::new(StmtX::Switch(Arc::new(vec![lblock, rblock])))]; + ctx.notify(|obs| obs.on_branch_merge(stm)); if ctx.debug { // Add a snapshot for the state after we join the lhs and rhs back together let sid = state.update_current_sid(SUFFIX_SNAP_JOIN); @@ -2674,6 +2704,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi stmts } StmX::RevealString(lit) => { + ctx.notify(|obs| obs.on_reveal_string(lit)); let exprs = Arc::new({ vec![string_len_to_air(ctx, lit.clone()), string_indices_to_air(ctx, lit.clone())] }); @@ -2745,6 +2776,9 @@ fn loop_to_stmts( }; let loop_isolation = *loop_isolation; + if *is_for_loop { + ctx.notify(|obs| obs.on_for_loop(stm)); + } let (cond_stm, pos_assume, neg_assume) = if let Some((cond_stm, cond_exp)) = cond { let pos_cond = exp_to_expr(ctx, &cond_exp, expr_ctxt)?; let neg_cond = Arc::new(ExprX::Unary(air::ast::UnaryOp::Not, pos_cond.clone())); @@ -2854,6 +2888,9 @@ fn loop_to_stmts( let mut air_body: Vec = state.static_prelude.clone(); if !loop_isolation { air_body.push(Arc::new(StmtX::Snapshot(snapshot_ident(SNAPSHOT_LOOP)))); + for (var, _) in modified_vars.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } modified_vars.emit_havocs(ctx, SNAPSHOT_LOOP, &mut air_body); } @@ -2884,6 +2921,9 @@ fn loop_to_stmts( // we need to havoc it, in order to create a difference between // the "current" value and the "pre-state" value. let pre_modified_params_incl = pre_modified_params_incl.as_ref().unwrap(); + for (var, _) in pre_modified_params_incl.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } pre_modified_params_incl.emit_havocs(ctx, SNAPSHOT_PRE, &mut air_body); } else { // Similar, but this time accounting for isolation boundary @@ -2891,6 +2931,9 @@ fn loop_to_stmts( // Havoc vars between beginning of the function and the start of // the isolation_boundary let pre_modified_params_excl = pre_modified_params_excl.as_ref().unwrap(); + for (var, _) in pre_modified_params_excl.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } pre_modified_params_excl.emit_havocs(ctx, SNAPSHOT_PRE, &mut air_body); // Execute the code between the isolation boundary and the actual loop start @@ -2898,6 +2941,9 @@ fn loop_to_stmts( // Havoc all vars that might be modified during the loop air_body.push(Arc::new(StmtX::Snapshot(snapshot_ident(SNAPSHOT_BOUNDARY)))); + for (var, _) in modified_vars.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } modified_vars.emit_havocs(ctx, SNAPSHOT_BOUNDARY, &mut air_body); } } @@ -2950,12 +2996,21 @@ fn loop_to_stmts( } if !ctx.checking_spec_preconditions() { - for (span, inv, msg, _) in invs_entry.iter() { + for (inv_idx, (span, inv, msg, _)) in invs_entry.iter().enumerate() { let mut error = error(span, crate::def::INV_FAIL_LOOP_END); if let Some(msg) = msg { error = error.secondary_label(span, &**msg); } - let inv_stmt = StmtX::Assert(None, error, None, inv.clone()); + let inv_stmt = StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::LoopInvariant, + inv_idx, + &None, + ), + error, + None, + inv.clone(), + ); air_body.push(Arc::new(inv_stmt)); } if decrease.len() > 0 { @@ -2968,7 +3023,12 @@ fn loop_to_stmts( )?; let expr = exp_to_expr(ctx, &dec_exp, expr_ctxt)?; let error = error(&stm.span, crate::def::DEC_FAIL_LOOP_END); - let dec_stmt = StmtX::Assert(None, error, None, expr); + let dec_stmt = StmtX::Assert( + ctx.make_assert_id(&crate::vir_observer::AssertIdKind::DecreasesCheck, 0, &None), + error, + None, + expr, + ); air_body.push(Arc::new(dec_stmt)); } } @@ -3005,12 +3065,21 @@ fn loop_to_stmts( // At original site of while loop, assert invariant, havoc, assume invariant + neg_cond let mut stmts: Vec = Vec::new(); if !ctx.checking_spec_preconditions() { - for (span, inv, msg, _) in invs_entry.iter() { + for (inv_idx, (span, inv, msg, _)) in invs_entry.iter().enumerate() { let mut error = error(span, crate::def::INV_FAIL_LOOP_FRONT); if let Some(msg) = msg { error = error.secondary_label(span, &**msg); } - let inv_stmt = StmtX::Assert(None, error, None, inv.clone()); + let inv_stmt = StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::LoopInvariant, + inv_idx, + &None, + ), + error, + None, + inv.clone(), + ); stmts.push(Arc::new(inv_stmt)); } } @@ -3021,6 +3090,9 @@ fn loop_to_stmts( } if loop_isolation { stmts.push(Arc::new(StmtX::Snapshot(snapshot_ident(SNAPSHOT_LOOP)))); + for (var, _) in modified_vars.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } modified_vars.emit_havocs(ctx, SNAPSHOT_LOOP, &mut stmts); for (_, inv, _, _) in invs_exit.iter() { let inv_stmt = StmtX::Assume(inv.clone()); @@ -3263,6 +3335,10 @@ pub(crate) fn body_stm_to_air( unwind, } = func_check_sst; + // Notify observer that body lowering is starting. + // Binders recorded before this point (requires/ensures) should be discarded. + ctx.notify(|obs| obs.on_body_lowering_start()); + if is_bit_vector_mode { if is_integer_ring { panic!("Error: integer_ring and bit_vector should not be used together"); @@ -3459,6 +3535,17 @@ pub(crate) fn body_stm_to_air( is_integer_ring || is_nonlinear, )); } + // Notify observer of binder-originated local declarations (including Skolemized + // copies): quantifier binders and choose binders alike. + for decl in local_decls.iter() { + if matches!( + decl.kind, + crate::sst::LocalDeclKind::QuantBinder | crate::sst::LocalDeclKind::ChooseBinder + ) { + ctx.notify(|obs| obs.on_quantifier_binder_decl(&decl.ident)); + } + } + ctx.notify(|obs| obs.on_function_lowered()); Ok((state.commands, state.snap_map)) } diff --git a/source/vir/src/vir_observer.rs b/source/vir/src/vir_observer.rs new file mode 100644 index 0000000000..7fa2cec2da --- /dev/null +++ b/source/vir/src/vir_observer.rs @@ -0,0 +1,179 @@ +//! VIR-level verification observer. +//! +//! Defines `VirObserver` — callbacks fired during VIR→AIR lowering (havoc, +//! assign, branch/break merges, loops, quantifier binders, reveals, and +//! function/krate lifecycle). +//! +//! This trait is independent: it does **not** require `AirObserver` or +//! `QueryResultObserver`. A consumer implements only the traits it needs; the +//! verifier wires each implemented trait to its own callbacks (see the observer +//! handle registry in `rust_verify/src/verifier.rs`). + +use crate::ast::{Krate, Typ, VarIdent}; +use crate::sst::{Exp, Stm}; +use air::ast::AssertId; +use std::any::Any; + +// Re-export for convenience (used by `VersionCorrelator::resolve`). +pub use air::air_observer::VersionOrigin; + +/// What kind of assertion is being assigned an ID. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum AssertIdKind { + Ensures, + LoopInvariant, + DecreasesCheck, +} + +/// Observer for the VIR-level verification pipeline. +/// +/// Callbacks fire during VIR→AIR lowering. All methods have default no-op +/// implementations except `as_any`/`as_any_mut` (trivially: `self`). +pub trait VirObserver: Any + Send { + /// Fired once per module in `Ctx::new`. The `NameCtxt` is the same instance + /// used by lowering, so AIR names computed by the observer are consistent + /// with the names lowering will produce. `current_crate` identifies the + /// crate under verification, so observers can strip its prefix from + /// friendly names (e.g. render `double(x)` not `test_crate::double(x)`). + fn on_krate( + &mut self, + _krate: &Krate, + _name_ctxt: &crate::def::NameCtxt, + _current_crate: &crate::ast::CrateId, + ) { + } + fn on_havoc(&mut self, _stm: &Stm, _var: &VarIdent) {} + fn on_assign(&mut self, _stm: &Stm, _var: &VarIdent) {} + fn on_variable_def(&mut self, _stm: &Stm, _var: &VarIdent) {} + fn on_branch_merge(&mut self, _stm: &Stm) {} + fn on_break_merge(&mut self, _stm: &Stm) {} + fn on_for_loop(&mut self, _stm: &Stm) {} + fn on_quantifier_binder(&mut self, _binder: &crate::ast::VarBinder, _exp: &Exp) {} + fn on_reveal_string(&mut self, _lit: &std::sync::Arc) {} + fn make_assert_id( + &mut self, + _kind: &AssertIdKind, + _index: usize, + parent: &Option, + ) -> Option { + parent.clone() + } + /// A quantifier binder local declaration was processed. + /// Fires for each QuantBinder in local_decls after body lowering, + /// including Skolemized copies (e.g., i$0, i$1). The observer can + /// correlate with the original binder's line via prefix matching + /// on suffix_local_unique_id(var). + /// Fires for choose binders as well as quantifier binders. + fn on_quantifier_binder_decl(&mut self, _var: &VarIdent) {} + /// Called at the start of function body lowering (body_stm_to_air). + /// Binders recorded after this point are body-level binders. + /// Observers should clear any pre-body binder accumulation here. + fn on_body_lowering_start(&mut self) {} + fn on_function_lowered(&mut self) {} + + fn as_any(&self) -> &dyn Any; + fn as_any_mut(&mut self) -> &mut dyn Any; +} + +/// A shared handle to a `VirObserver`; `Arc>` like the AIR handles. +pub type VirObserverHandle = std::sync::Arc>; + +/// Registry of per-trait observer handles: independent trait-object views of +/// (up to) one shared observer object. Each field is `Some` only if the observer +/// implements that trait, so a consumer couples nothing it does not use. All +/// populated fields point at the same underlying `Mutex` (via `Arc` unsizing +/// coercion at the factory), so callbacks mutate one shared object. +#[derive(Clone, Default)] +pub struct Observers { + pub vir: Option, + pub air: Option, + pub query_result: Option< + air::query_result_observer::QueryResultObserverHandle, + >, +} + +use std::collections::{HashMap, VecDeque}; +use std::sync::Arc; + +/// Extract line number from a VIR span's string representation ("file:line:col:..."). +pub fn line_from_span(span: &crate::messages::Span) -> Option { + span.as_string.split(':').nth(1)?.trim().parse().ok() +} + +/// Strip the version suffix from a versioned WP constant name. +/// `"x@2"` → `"x@"`, `"foo!@3"` → `"foo!@"` +fn strip_version_suffix(name: &str) -> &str { + if let Some(pos) = name.rfind('@') { &name[..=pos] } else { name } +} + +/// Helper for observers that need to correlate VIR-level +/// `on_havoc`/`on_assign` callbacks with AIR-level WP versioned +/// constants created during `lower_query`. +/// +/// # Ordering invariant +/// +/// For each variable `x`, the Nth `record_havoc_or_assign` call +/// corresponds to the Nth `resolve` call with a `Havoc` or `Assign` +/// origin. This ordering is guaranteed because VIR emits +/// Havoc/Assign statements in the same order that `lower_query` +/// processes them. No AIR pass reorders these statements. +/// +/// Enforced via `debug_assert!` in `resolve`. +pub struct VersionCorrelator { + /// Per-base-variable queue of VIR statements (Havoc/Assign). + queues: HashMap, VecDeque>, + /// Most recent branch merge stm. + last_branch_merge: Option, + /// Most recent break merge stm. + last_break_merge: Option, +} + +impl VersionCorrelator { + pub fn new() -> Self { + Self { queues: HashMap::new(), last_branch_merge: None, last_break_merge: None } + } + + /// Record a VIR-level Havoc or Assign for a variable. + /// `base` is the AIR base name (e.g., `"x@"` from `suffix_local_unique_id`). + pub fn record_havoc_or_assign(&mut self, base: &air::ast::Ident, stm: &Stm) { + self.queues.entry(base.clone()).or_default().push_back(stm.clone()); + } + + /// Record a branch merge point (from `on_branch_merge`). + pub fn record_branch_merge(&mut self, stm: &Stm) { + self.last_branch_merge = Some(stm.clone()); + } + + /// Record a break merge point (from `on_break_merge`). + pub fn record_break_merge(&mut self, stm: &Stm) { + self.last_break_merge = Some(stm.clone()); + } + + /// Resolve an AIR versioned constant to its VIR origin. + /// Returns the VIR `Stm` that caused this version to exist. + pub fn resolve(&mut self, versioned: &air::ast::Ident, kind: VersionOrigin) -> Option { + match kind { + VersionOrigin::Havoc | VersionOrigin::Assign => { + let base = strip_version_suffix(versioned); + let base_key = Arc::new(base.to_string()); + let queue = self.queues.get_mut(&base_key)?; + debug_assert!( + !queue.is_empty(), + "VIR/AIR ordering invariant violated for {}: \ + no VIR record available (queue empty)", + versioned + ); + queue.pop_front() + } + VersionOrigin::BranchMerge => self.last_branch_merge.clone(), + VersionOrigin::BreakMerge => self.last_break_merge.clone(), + } + } + + /// Reset between functions. + pub fn reset(&mut self) { + self.queues.clear(); + self.last_branch_merge = None; + self.last_break_merge = None; + } +} From fbd3e49c83e03dbf441f4cee45a5db4b4f5ab5fe Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sat, 26 Sep 2026 21:08:23 -0400 Subject: [PATCH 2/7] Evaluate observer expressions with get-value under cvc5 `QueryResultObserver::Invalid` hands observers `eval_bool_expr`, which sends z3's `(eval ...)` extension. cvc5 has no `eval`: it answers with an error the reader does not expect, and the run dies with "Got too many empty lines" / "Z3 reader thread failure". The PR's own `test` observer does this on any failing query here, since the fork runs cvc5 outside internal test mode; upstream's tests pass because they run z3. Under cvc5 `evaluate_bool` now asks `(get-value (e))` and reads the `((e true))` / `((e false))` answer; z3 keeps `eval`. Co-Authored-By: Claude Opus 5.5 (1M context) --- source/air/src/context.rs | 23 +++++++++++++++++++---- source/air/src/emitter.rs | 8 ++++++++ 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/source/air/src/context.rs b/source/air/src/context.rs index 7d47f6c0e1..a1bbde530c 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -1672,10 +1672,25 @@ impl Context { let printer = crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone()); let node = printer.expr_to_node(expr); - match self.eval_expr(node).as_str() { - "true" => Some(true), - "false" => Some(false), - _ => None, + match self.solver { + SmtSolver::Z3 => match self.eval_expr(node).as_str() { + "true" => Some(true), + "false" => Some(false), + _ => None, + }, + // cvc5 has no `eval`: it takes the command for an unknown one + // and the reader loses its place in the solver's output. + // `get-value` answers `((expr value))` on one line. + SmtSolver::Cvc5 => { + self.smt_log.log_get_value(node); + let smt_data = self.smt_log.take_pipe_data(); + let smt_output = self.get_smt_process().send_commands(smt_data); + match smt_output.as_slice() { + [line] if line.ends_with(" true))") => Some(true), + [line] if line.ends_with(" false))") => Some(false), + _ => None, + } + } } } diff --git a/source/air/src/emitter.rs b/source/air/src/emitter.rs index 7156b399d5..9c5bf3f170 100644 --- a/source/air/src/emitter.rs +++ b/source/air/src/emitter.rs @@ -273,4 +273,12 @@ impl Emitter { self.log_node(&nodes!(eval { expr })); } } + + /// `(get-value (expr))`: the standard spelling of `eval`, which cvc5 + /// answers and z3's `eval` extension does not require. + pub fn log_get_value(&mut self, expr: Node) { + if !self.is_none() { + self.log_node(&nodes!(get-value { Node::List(vec![expr]) })); + } + } } From 21cc55fa99aa4dd3471199a4fce4f28acbfa4521 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sat, 26 Sep 2026 21:08:24 -0400 Subject: [PATCH 3/7] Record variable versions through the observer's version hook `lower_stmt` had two paths for a new variable version: the fork's `record_versions` bookkeeping (read back by provenance, e-graph readings and speculation) and the PR's `notify_version_created`, which announces it to an `AirObserver`. They now share one: `notify_version_created` records the version when asked and then notifies the observer, for havoc, assign and merge versions alike. The declared version 0 is still recorded where it is declared, which no statement announces. A merge's version is always the highest a branch reached, so it was already in the map; recording it again changes nothing. Co-Authored-By: Claude Opus 5.5 (1M context) --- source/air/src/var_to_const.rs | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/source/air/src/var_to_const.rs b/source/air/src/var_to_const.rs index 7a85fd91a8..bcc3dbed38 100644 --- a/source/air/src/var_to_const.rs +++ b/source/air/src/var_to_const.rs @@ -170,11 +170,20 @@ impl GoalScope { } impl LowerStmtState<'_> { + /// Version `n` of `x` came into being as `versioned`: recorded for the + /// context's own readers when asked (`record_versions`), and announced to + /// the observer. The declared version 0 of each variable is recorded + /// where it is declared, before any statement. fn notify_version_created( &mut self, + x: &Ident, + n: u32, versioned: &Ident, kind: crate::air_observer::VersionOrigin, ) { + if self.record_versions { + self.variable_versions.insert(versioned.to_string(), (x.to_string(), n)); + } if let Some(obs) = &mut self.observer { obs.on_wp_version_created(versioned, kind); } @@ -205,9 +214,7 @@ fn lower_stmt( let n = find_version(&versions, x); let typ = types[x].clone(); versions.insert(x.clone(), n + 1); - if state.record_versions { - state.variable_versions.insert(rename_var(x, n + 1), (x.to_string(), n + 1)); - } + let base = x; let x = Arc::new(rename_var(x, n + 1)); if !state.version_decls.contains(&x) { let decl = Arc::new(DeclX::Const(x.clone(), typ)); @@ -219,7 +226,7 @@ fn lower_stmt( } else { crate::air_observer::VersionOrigin::Assign }; - state.notify_version_created(&x, kind); + state.notify_version_created(base, n + 1, &x, kind); match &*stmt { StmtX::Assign(_, e) => { let expr1 = Arc::new(ExprX::Var(x)); @@ -262,6 +269,8 @@ fn lower_stmt( if !had_explicit { let renamed = Arc::new(rename_var(x, merged_version)); state.notify_version_created( + x, + merged_version, &renamed, crate::air_observer::VersionOrigin::BreakMerge, ); @@ -303,6 +312,8 @@ fn lower_stmt( if !had_explicit { let renamed = Arc::new(rename_var(x, merged_version)); state.notify_version_created( + x, + merged_version, &renamed, crate::air_observer::VersionOrigin::BranchMerge, ); From 0e4d7c43c95f290907d2fee0c7e2f6f5e76bff99 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sat, 26 Sep 2026 21:30:12 -0400 Subject: [PATCH 4/7] Add -V observers=coverage and proof-state Two observers built on the observation interface, served by one object (rust_verify/src/observers.rs), so they may be named together. coverage: per query, every obligation Verus asserted (an assert, a postcondition, a loop invariant, a call's precondition, an overflow check) with its message, span and status: proved, failed, unknown (the solver gave up on the query) or unchecked (the query stopped before deciding it). With -V axiom-usage-info a proved query also lists its unsat-core axioms. Obligation-level coverage, beside verus-reach's function-level reachability. proof-state: at each failing obligation, while the counterexample is live, the failing assertion's conjuncts with their value in it (false first) and the counterexample value of each constant it reads, rendered as source with the names the encoders recorded. The observer sees queries but not functions, so the verifier drains it after each query, files the records under the function like the other per-query solver reports, and renders them at the end of the crate. They appear in func-details as `obligations` and `failing_asserts`, and so in --output-json and --report-json. Assertion ids are not unique (loop invariants have none; a function's postconditions share one), so a failure is placed by its error's span. A failure that reaches the verifier without the Invalid callback (no model) is still recorded from the ids the verifier saw fail, and when the --multiple-errors budget runs out the obligations after the last failure are unchecked rather than proved. Also formats the observer handle types the previous commits introduced. Co-Authored-By: Claude Opus 5.5 (1M context) --- source/air/src/context.rs | 19 +- source/rust_verify/src/lib.rs | 1 + source/rust_verify/src/observers.rs | 628 ++++++++++++++++++ source/rust_verify/src/verifier.rs | 67 +- .../tests/obligation_observer.rs | 166 +++++ source/vir/src/context.rs | 4 +- source/vir/src/vir_observer.rs | 4 +- 7 files changed, 873 insertions(+), 16 deletions(-) create mode 100644 source/rust_verify/src/observers.rs create mode 100644 source/rust_verify_test/tests/obligation_observer.rs diff --git a/source/air/src/context.rs b/source/air/src/context.rs index a1bbde530c..1d256baf14 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -541,11 +541,9 @@ pub struct Context { name_counters: Vec, pub(crate) typing: Typing, pub(crate) debug: bool, - pub(crate) air_observer: - Option, - pub(crate) query_result_observer: Option< - crate::query_result_observer::QueryResultObserverHandle, - >, + pub(crate) air_observer: Option, + pub(crate) query_result_observer: + Option, pub(crate) ignore_unexpected_smt: bool, pub(crate) rlimit: u32, pub(crate) air_initial_log: Emitter, @@ -818,14 +816,19 @@ impl Context { pub fn set_observers( &mut self, air_observer: Option, - query_result_observer: Option< - crate::query_result_observer::QueryResultObserverHandle, - >, + query_result_observer: Option, ) { self.air_observer = air_observer; self.query_result_observer = query_result_observer; } + /// The query-result observer `set_observers` registered, if any. + pub fn query_result_observer( + &self, + ) -> Option<&crate::query_result_observer::QueryResultObserverHandle> { + self.query_result_observer.as_ref() + } + pub fn set_air_initial_log(&mut self, writer: Box) { self.air_initial_log.set_log(Some(writer)); } diff --git a/source/rust_verify/src/lib.rs b/source/rust_verify/src/lib.rs index 224fcfec4f..b1dd58458d 100644 --- a/source/rust_verify/src/lib.rs +++ b/source/rust_verify/src/lib.rs @@ -52,6 +52,7 @@ pub mod file_loader; mod fn_call_to_vir; mod hir_hide_reveal_rewrite; mod import_export; +pub mod observers; pub mod profiler; mod provenance; mod reach; diff --git a/source/rust_verify/src/observers.rs b/source/rust_verify/src/observers.rs new file mode 100644 index 0000000000..fb6fc73bbc --- /dev/null +++ b/source/rust_verify/src/observers.rs @@ -0,0 +1,628 @@ +//! Observers the verifier ships, as opposed to the test observers. +//! +//! One object, [`ObligationObserver`], serves two `-V observers=` names: +//! +//! - `coverage`: for every query, each obligation it asserted (an `assert`, +//! a postcondition, a loop invariant, a precondition of a call...) and what +//! became of it: `proved`, `failed`, `unknown` (the solver gave up on the +//! query) or `unchecked` (the query stopped before reaching it). With +//! `-V axiom-usage-info` a proved query also names the axioms in its unsat +//! core. This is the obligation-level counterpart of `verus-reach`, which +//! says which functions are used; this says which of a function's +//! obligations were actually discharged. +//! - `proof-state`: at each failing obligation, while the solver's +//! counterexample is still live, which conjuncts of the failing assertion +//! are false in it and what the counterexample gives each variable the +//! assertion reads. +//! +//! Both need the query's assertions, which `AirObserver::on_query_lowered` +//! hands over after variables became versioned constants, and the answer, +//! which `QueryResultObserver` hands over. Neither knows which function a +//! query belongs to; the verifier does, so it drains the observer after each +//! query ([`ObligationObserver::take_query`]) and files the records under the +//! function, the way it files the other per-query solver reports. Terms stay +//! AIR text until the end of the crate, when [`resolve`] renders them as +//! source with the names the encoders recorded. + +use air::ast::{AssertId, Expr, ExprX, MultiOp, Query, Stmt, StmtX}; +use air::query_result_observer::CheckValidResult; +use serde::Serialize; +use std::any::Any; +use std::collections::BTreeSet; +use std::sync::Arc; + +/// The observer names this module serves. +pub const COVERAGE: &str = "coverage"; +pub const PROOF_STATE: &str = "proof-state"; + +/// A failing assertion's conjuncts are listed up to this many; the rest are +/// counted in `conjuncts_omitted`. +const MAX_CONJUNCTS: usize = 32; +/// Likewise the variables whose counterexample values are reported. +const MAX_VALUES: usize = 64; + +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] +#[serde(rename_all = "snake_case")] +pub enum Status { + Proved, + Failed, + /// The solver gave up (resource limit or cancellation) before deciding it. + Unknown, + /// The query stopped before the solver decided it: an earlier failure + /// ended the query (`--multiple-errors 0`), or the error budget ran out. + Unchecked, +} + +/// One assertion of a lowered query. +struct Assertion { + id: Option, + message: String, + span: Option, + /// The asserted formula, over versioned constants. + expr: Expr, + status: Option, +} + +/// The query being checked: its assertions, and the answers so far. +struct Pending { + assertions: Vec, + used_axioms: Option>, + failing: Vec, +} + +/// One obligation, before its terms are rendered as source. +#[derive(Clone, Debug, Serialize)] +pub struct Obligation { + #[serde(skip_serializing_if = "Option::is_none")] + pub assert_id: Option, + /// What Verus reports when it fails: "postcondition not satisfied", ... + pub message: String, + #[serde(skip_serializing_if = "Option::is_none")] + pub span: Option, + pub status: Status, +} + +/// A conjunct of a failing assertion, and its value in the counterexample: +/// null when the solver could not evaluate it (a quantifier, say). +#[derive(Clone, Debug, Serialize)] +pub struct Conjunct { + pub term: String, + pub value: Option, +} + +/// A variable the failing assertion reads, and its counterexample value. +#[derive(Clone, Debug, Serialize)] +pub struct Value { + /// The versioned AIR constant (`x@2`): which assignment of `x` it is. + pub symbol: String, + /// The variable as the source names it, when the encoders recorded it. + #[serde(skip_serializing_if = "Option::is_none")] + pub name: Option, + pub value: String, +} + +#[derive(Clone, Debug)] +pub struct RawFailingAssert { + assert_id: Option, + message: String, + span: Option, + conjuncts: Vec<(String, Option)>, + conjuncts_omitted: usize, + values: Vec<(String, String)>, + values_omitted: usize, +} + +/// What the observer saw of one query, before rendering. +pub struct RawQuery { + obligations: Vec, + used_axioms: Option>, + failing: Vec, +} + +/// Coverage of one query, as `func-details` publishes it under `obligations`. +#[derive(Clone, Debug, Serialize)] +pub struct QueryObligations { + pub desc: String, + pub span: String, + /// `body`, `recommends`, `expanded`, ... as the other per-query records. + pub kind: &'static str, + pub obligations: Vec, + /// Under `-V axiom-usage-info`, when the query was proved: the axioms in + /// its unsat core, rendered as source where the encoders named them. + #[serde(skip_serializing_if = "Option::is_none")] + pub used_axioms: Option>, +} + +/// The counterexample at one failing obligation, as `func-details` publishes +/// it under `failing_asserts`. +#[derive(Clone, Debug, Serialize)] +pub struct FailingAssert { + pub desc: String, + pub kind: &'static str, + #[serde(skip_serializing_if = "Option::is_none")] + pub assert_id: Option, + pub message: String, + #[serde(skip_serializing_if = "Option::is_none")] + pub span: Option, + /// False conjuncts first, then undecided, then true ones. + pub conjuncts: Vec, + #[serde(skip_serializing_if = "is_zero")] + pub conjuncts_omitted: usize, + pub values: Vec, + #[serde(skip_serializing_if = "is_zero")] + pub values_omitted: usize, +} + +fn is_zero(n: &usize) -> bool { + *n == 0 +} + +/// A query's records, filed under its function until the end of the crate. +pub struct FiledQuery { + pub desc: String, + pub span: String, + pub kind: &'static str, + pub raw: RawQuery, +} + +pub struct ObligationObserver { + coverage: bool, + proof_state: bool, + pending: Option, +} + +impl ObligationObserver { + /// `None` unless `names` asks for this observer and nothing else. + pub fn from_names(names: &[String]) -> Option { + let coverage = names.iter().any(|n| n == COVERAGE); + let proof_state = names.iter().any(|n| n == PROOF_STATE); + let others = names.iter().any(|n| n != COVERAGE && n != PROOF_STATE); + ((coverage || proof_state) && !others).then(|| ObligationObserver { + coverage, + proof_state, + pending: None, + }) + } + + /// Close the query just checked and hand over what was seen of it. + /// + /// `failed` are the ids the verifier saw fail, which covers answers that + /// reach it without the `Invalid` callback (no model, bit-vector checks). + /// `truncated` says the verifier stopped checking obligations after the + /// last failure (the `--multiple-errors` budget ran out), so a later + /// `Valid` does not speak for them. + pub fn take_query( + &mut self, + failed: &[AssertId], + timed_out: bool, + truncated: bool, + ) -> Option { + let mut pending = self.pending.take()?; + for a in pending.assertions.iter_mut() { + if a.status.is_none() && a.id.as_ref().is_some_and(|id| failed.contains(id)) { + a.status = Some(Status::Failed); + } + } + if truncated { + if let Some(last) = + pending.assertions.iter().rposition(|a| a.status == Some(Status::Failed)) + { + for a in pending.assertions[last + 1..].iter_mut() { + if a.status == Some(Status::Proved) { + a.status = Some(Status::Unchecked); + } + } + } + } + let rest = if timed_out { Status::Unknown } else { Status::Unchecked }; + let obligations = if self.coverage { + pending + .assertions + .into_iter() + .map(|a| Obligation { + assert_id: a.id.as_ref().map(air::def::assert_id_to_symbol), + message: a.message, + span: a.span, + status: a.status.unwrap_or(rest), + }) + .collect() + } else { + Vec::new() + }; + Some(RawQuery { obligations, used_axioms: pending.used_axioms, failing: pending.failing }) + } +} + +/// The message and primary span of an assertion's error. +fn describe(message: &air::messages::ArcDynMessage) -> (String, Option) { + match message.downcast_ref::() { + Some(m) => (m.note.clone(), m.spans.first().map(|s| s.as_string.clone())), + None => (String::new(), None), + } +} + +fn collect_assertions(stmt: &Stmt, out: &mut Vec) { + match &**stmt { + StmtX::Assert(id, message, _, expr) => { + let (message, span) = describe(message); + out.push(Assertion { id: id.clone(), message, span, expr: expr.clone(), status: None }); + } + StmtX::DeadEnd(s) | StmtX::Breakable(_, s) => collect_assertions(s, out), + StmtX::Block(ss) | StmtX::Switch(ss) => { + for s in ss.iter() { + collect_assertions(s, out); + } + } + StmtX::Assume(_) + | StmtX::Havoc(_) + | StmtX::Assign(..) + | StmtX::Snapshot(_) + | StmtX::Break(_) => {} + } +} + +/// The formula's top-level conjuncts, flattening nested conjunctions. +fn conjuncts(expr: &Expr, out: &mut Vec) { + match &**expr { + ExprX::Multi(MultiOp::And, es) => { + for e in es.iter() { + conjuncts(e, out); + } + } + _ => out.push(expr.clone()), + } +} + +/// The constants the formula reads, outside binders' own variables. +fn free_constants(expr: &Expr, bound: &mut Vec, out: &mut BTreeSet) { + match &**expr { + ExprX::Const(_) => {} + ExprX::Var(x) => { + if !bound.iter().any(|b| b == &**x) { + out.insert(x.to_string()); + } + } + ExprX::Old(_, x) => { + out.insert(x.to_string()); + } + ExprX::Apply(_, es) | ExprX::Multi(_, es) | ExprX::Array(es) => { + for e in es.iter() { + free_constants(e, bound, out); + } + } + ExprX::ApplyFun(_, f, es) => { + free_constants(f, bound, out); + for e in es.iter() { + free_constants(e, bound, out); + } + } + ExprX::Unary(_, e) | ExprX::LabeledAxiom(_, _, e) | ExprX::LabeledAssertion(_, _, _, e) => { + free_constants(e, bound, out) + } + ExprX::Binary(_, a, b) => { + free_constants(a, bound, out); + free_constants(b, bound, out); + } + ExprX::IfElse(a, b, c) => { + free_constants(a, bound, out); + free_constants(b, bound, out); + free_constants(c, bound, out); + } + ExprX::Bind(bind, e) => { + let names: Vec = match &**bind { + air::ast::BindX::Let(bs) => { + for b in bs.iter() { + free_constants(&b.a, bound, out); + } + bs.iter().map(|b| b.name.to_string()).collect() + } + air::ast::BindX::Quant(_, bs, _, _) | air::ast::BindX::Lambda(bs, _, _) => { + bs.iter().map(|b| b.name.to_string()).collect() + } + air::ast::BindX::Choose(bs, _, _, cond) => { + let names: Vec = bs.iter().map(|b| b.name.to_string()).collect(); + let depth = bound.len(); + bound.extend(names.iter().cloned()); + free_constants(cond, bound, out); + bound.truncate(depth); + names + } + }; + let depth = bound.len(); + bound.extend(names); + free_constants(e, bound, out); + bound.truncate(depth); + } + } +} + +fn term_text(expr: &Expr) -> String { + let printer = air::printer::Printer::new( + Arc::new(air::messages::AirMessageInterface {}), + true, + air::context::SmtSolver::Cvc5, + ); + air::printer::NodeWriter::new() + .node_to_string_indent(&String::new(), &printer.expr_to_node(expr)) +} + +impl air::air_observer::AirObserver for ObligationObserver { + fn on_query_lowered( + &mut self, + query: &Query, + _snapshots: &air::ast::Snapshots, + _local_vars: &[air::ast::Decl], + ) { + let mut assertions = Vec::new(); + collect_assertions(&query.assertion, &mut assertions); + self.pending = Some(Pending { assertions, used_axioms: None, failing: Vec::new() }); + } + + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +impl air::query_result_observer::QueryResultObserver for ObligationObserver { + fn on_check_valid_result(&mut self, result: &mut CheckValidResult) { + let proof_state = self.proof_state; + let Some(pending) = &mut self.pending else { return }; + match result { + CheckValidResult::Valid { usage_info, .. } => { + for a in pending.assertions.iter_mut() { + if a.status.is_none() { + a.status = Some(Status::Proved); + } + } + if let air::context::UsageInfo::UsedAxioms(axioms) = usage_info { + pending.used_axioms = Some(axioms.iter().map(|a| a.to_string()).collect()); + } + } + CheckValidResult::Timeout { .. } => { + for a in pending.assertions.iter_mut() { + if a.status.is_none() { + a.status = Some(Status::Unknown); + } + } + } + CheckValidResult::Invalid { model_defs, eval_bool_expr, assert_id, error } => { + // The undecided assertion the solver's label named. Ids are + // not unique (loop invariants have none, a function's + // postconditions share one), so the error's primary span + // decides between assertions with the same id. + let (_, error_span) = describe(error); + let undecided = |a: &Assertion| a.status.is_none() && &a.id == *assert_id; + let Some(index) = pending + .assertions + .iter() + .position(|a| undecided(a) && error_span.is_some() && a.span == error_span) + .or_else(|| pending.assertions.iter().position(undecided)) + else { + return; + }; + let a = &mut pending.assertions[index]; + a.status = Some(Status::Failed); + if !proof_state { + return; + } + let mut parts = Vec::new(); + conjuncts(&a.expr, &mut parts); + let mut evaluated: Vec<(String, Option)> = + parts.iter().map(|c| (term_text(c), eval_bool_expr(c))).collect(); + // false first: those are why the assertion failed + evaluated.sort_by_key(|(_, v)| match v { + Some(false) => 0, + None => 1, + Some(true) => 2, + }); + let conjuncts_omitted = evaluated.len().saturating_sub(MAX_CONJUNCTS); + evaluated.truncate(MAX_CONJUNCTS); + let mut symbols = BTreeSet::new(); + free_constants(&a.expr, &mut Vec::new(), &mut symbols); + let mut values: Vec<(String, String)> = symbols + .into_iter() + .filter_map(|s| { + let def = model_defs.get(&Arc::new(s.clone()))?; + def.params.is_empty().then(|| (s, def.body.to_string())) + }) + .collect(); + let values_omitted = values.len().saturating_sub(MAX_VALUES); + values.truncate(MAX_VALUES); + pending.failing.push(RawFailingAssert { + assert_id: a.id.as_ref().map(air::def::assert_id_to_symbol), + message: a.message.clone(), + span: a.span.clone(), + conjuncts: evaluated, + conjuncts_omitted, + values, + values_omitted, + }); + } + } + } + + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +/// The source spelling of a versioned constant's variable: `x@2` reads as +/// `x`, when the encoders recorded `x@`. +fn variable_name(names: &vir::air_names::SourceNames, symbol: &str) -> Option { + let base = match symbol.rfind('@') { + Some(at) => &symbol[..=at], + None => symbol, + }; + let rendered = vir::air_names::render_term(names, base); + (rendered != base).then_some(rendered) +} + +/// A term with each versioned constant (`i@1`) read as its variable (`i@`), +/// which the encoders recorded: the source has no versions. +fn render_unversioned(names: &vir::air_names::SourceNames, term: &str) -> String { + let mut out = String::with_capacity(term.len()); + let mut chars = term.chars().peekable(); + while let Some(c) = chars.next() { + out.push(c); + if c == '@' { + while chars.peek().is_some_and(|d| d.is_ascii_digit()) { + chars.next(); + } + } + } + vir::air_names::render_term(names, &out) +} + +/// Render one function's filed queries as source. +pub fn resolve( + names: &vir::air_names::SourceNames, + queries: Vec, +) -> (Vec, Vec) { + let mut obligations = Vec::new(); + let mut failing = Vec::new(); + for q in queries { + let FiledQuery { desc, span, kind, raw } = q; + if !raw.obligations.is_empty() { + obligations.push(QueryObligations { + desc: desc.clone(), + span, + kind, + obligations: raw.obligations, + used_axioms: raw.used_axioms.map(|axioms| { + axioms.iter().map(|a| vir::air_names::render_term(names, a)).collect() + }), + }); + } + for f in raw.failing { + failing.push(FailingAssert { + desc: desc.clone(), + kind, + assert_id: f.assert_id, + message: f.message, + span: f.span, + conjuncts: f + .conjuncts + .into_iter() + .map(|(term, value)| Conjunct { term: render_unversioned(names, &term), value }) + .collect(), + conjuncts_omitted: f.conjuncts_omitted, + values: f + .values + .into_iter() + .map(|(symbol, value)| Value { + name: variable_name(names, &symbol), + value: vir::air_names::render_term(names, &value), + symbol, + }) + .collect(), + values_omitted: f.values_omitted, + }); + } + } + (obligations, failing) +} + +#[cfg(test)] +mod tests { + use super::*; + use air::ast::{BinaryOp, Constant, TypX}; + + fn var(x: &str) -> Expr { + Arc::new(ExprX::Var(Arc::new(x.to_string()))) + } + + #[test] + fn names_select_the_observer_alone() { + let names = |ns: &[&str]| ns.iter().map(|n| n.to_string()).collect::>(); + assert!(ObligationObserver::from_names(&names(&["coverage"])).is_some()); + let both = ObligationObserver::from_names(&names(&["coverage", "proof-state"])).unwrap(); + assert!(both.coverage && both.proof_state); + assert!(ObligationObserver::from_names(&names(&["coverage", "test"])).is_none()); + assert!(ObligationObserver::from_names(&names(&["test"])).is_none()); + } + + #[test] + fn versions_are_dropped_before_rendering() { + let names = vir::air_names::SourceNames::new(); + assert_eq!(render_unversioned(&names, "(<= i@12 n@)"), "(i@ <= n@)"); + } + + #[test] + fn conjuncts_flatten_nested_ands() { + let and = |es: Vec| Arc::new(ExprX::Multi(MultiOp::And, Arc::new(es))); + let e = and(vec![var("a"), and(vec![var("b"), var("c")])]); + let mut out = Vec::new(); + conjuncts(&e, &mut out); + assert_eq!(out.len(), 3); + } + + #[test] + fn free_constants_skip_bound_variables() { + let binder = + Arc::new(air::ast::BinderX { name: Arc::new("i".to_string()), a: Arc::new(TypX::Int) }); + let body = Arc::new(ExprX::Binary(BinaryOp::Le, var("i"), var("n@1"))); + let bind = Arc::new(air::ast::BindX::Quant( + air::ast::Quant::Forall, + Arc::new(vec![binder]), + Arc::new(vec![]), + None, + )); + let e = Arc::new(ExprX::Multi( + MultiOp::And, + Arc::new(vec![ + Arc::new(ExprX::Bind(bind, body)), + var("x@0"), + Arc::new(ExprX::Const(Constant::Bool(true))), + ]), + )); + let mut out = BTreeSet::new(); + free_constants(&e, &mut Vec::new(), &mut out); + assert_eq!(out.into_iter().collect::>(), vec!["n@1", "x@0"]); + } + + #[test] + fn take_query_fills_statuses() { + let mut o = ObligationObserver { coverage: true, proof_state: false, pending: None }; + let id = |n: u64| Some(Arc::new(vec![n])); + let assertion = |n: u64, status| Assertion { + id: id(n), + message: String::new(), + span: None, + expr: var("x"), + status, + }; + let pending = |o: &mut ObligationObserver| { + o.pending = Some(Pending { + assertions: vec![ + assertion(0, Some(Status::Proved)), + assertion(1, Some(Status::Failed)), + assertion(2, Some(Status::Proved)), + assertion(3, None), + ], + used_axioms: None, + failing: Vec::new(), + }) + }; + pending(&mut o); + let statuses = |q: RawQuery| q.obligations.iter().map(|o| o.status).collect::>(); + use Status::*; + // the error budget ran out after #1: a later Valid does not speak for #2 + let q = o.take_query(&[], false, true).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Unchecked, Unchecked]); + // #3 failed without an Invalid callback (no model) + pending(&mut o); + let q = o.take_query(&[Arc::new(vec![3])], false, false).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Proved, Failed]); + // the solver gave up + pending(&mut o); + let q = o.take_query(&[], true, false).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Proved, Unknown]); + assert!(o.take_query(&[], false, false).is_none()); + } +} diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index 64d0b4e1e8..07e12ae755 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -41,8 +41,7 @@ fn create_observer(name: &str) -> vir::vir_observer::Observers { let o = Arc::new(Mutex::new(crate::test_observer::TestObserver::new())); let vir: vir::vir_observer::VirObserverHandle = o.clone(); let air: air::air_observer::AirObserverHandle = o.clone(); - let query_result: air::query_result_observer::QueryResultObserverHandle = - o.clone(); + let query_result: air::query_result_observer::QueryResultObserverHandle = o.clone(); vir::vir_observer::Observers { vir: Some(vir), air: Some(air), @@ -71,6 +70,17 @@ fn create_observer(name: &str) -> vir::vir_observer::Observers { } fn create_observer_from_args(names: &[String]) -> vir::vir_observer::Observers { + // `coverage` and `proof-state` are one object, so they may be named together. + if let Some(o) = crate::observers::ObligationObserver::from_names(names) { + let o = Arc::new(std::sync::Mutex::new(o)); + let air: air::air_observer::AirObserverHandle = o.clone(); + let query_result: air::query_result_observer::QueryResultObserverHandle = o; + return vir::vir_observer::Observers { + air: Some(air), + query_result: Some(query_result), + ..Default::default() + }; + } if names.len() > 1 { panic!("only one observer may be specified at a time; got: {:?}", names); } @@ -493,6 +503,9 @@ pub struct Verifier { /// Under `-V inst-pressure`: what cvc5 reported for each query of each /// function, by qid, in check order func_inst_pressure: HashMap>, + /// Under `-V observers=coverage` / `proof-state`: each query's + /// obligations and failing-assert counterexamples, not yet rendered. + func_observations: HashMap>, /// Errors to report after verification has run deferred_errors: Vec, /// Every diagnostic raised while verifying a function's obligations, @@ -564,6 +577,12 @@ pub struct FuncDetails { /// filled under `-V inst-pressure` #[serde(skip_serializing_if = "Vec::is_empty")] pub inst_pressure: Vec, + /// filled under `-V observers=coverage` + #[serde(skip_serializing_if = "Vec::is_empty")] + pub obligations: Vec, + /// filled under `-V observers=proof-state` + #[serde(skip_serializing_if = "Vec::is_empty")] + pub failing_asserts: Vec, } impl Default for FuncDetails { @@ -577,6 +596,8 @@ impl Default for FuncDetails { nl_frontier: Default::default(), matching_loops: Default::default(), inst_pressure: Default::default(), + obligations: Default::default(), + failing_asserts: Default::default(), } } } @@ -591,6 +612,8 @@ impl FuncDetails { self.nl_frontier.extend(other.nl_frontier); self.matching_loops.extend(other.matching_loops); self.inst_pressure.extend(other.inst_pressure); + self.obligations.extend(other.obligations); + self.failing_asserts.extend(other.failing_asserts); } pub fn to_json(&self) -> serde_json::Value { @@ -768,6 +791,7 @@ impl Verifier { func_nl_frontier: HashMap::new(), func_matching_loops: HashMap::new(), func_inst_pressure: HashMap::new(), + func_observations: HashMap::new(), deferred_errors: Vec::new(), raised_diagnostics: Vec::new(), reported_diagnostics: Vec::new(), @@ -830,6 +854,7 @@ impl Verifier { func_nl_frontier: HashMap::new(), func_matching_loops: HashMap::new(), func_inst_pressure: HashMap::new(), + func_observations: HashMap::new(), deferred_errors: Vec::new(), raised_diagnostics: Vec::new(), reported_diagnostics: Vec::new(), @@ -889,6 +914,9 @@ impl Verifier { for (fun, queries) in other.func_inst_pressure { self.func_inst_pressure.entry(fun).or_default().extend(queries); } + for (fun, queries) in other.func_observations { + self.func_observations.entry(fun).or_default().extend(queries); + } self.deferred_errors.extend(other.deferred_errors); } @@ -1203,6 +1231,8 @@ impl Verifier { let mut invalidity = false; let mut timed_out = false; let mut used_axioms = None; + // the ids this query failed at, for an observer that missed the answer + let mut failed_here: Vec = Vec::new(); // 0 for the query's first check, then one per multi-error round let mut round = 0usize; loop { @@ -1336,6 +1366,7 @@ impl Verifier { | ValidityResult::Invalid(_, error @ None, assert_id_opt) => { // no model, but the obligation may still be known // Borrowed, not moved: the report reads the same id below. + failed_here.extend(assert_id_opt.iter().cloned()); if let Some(assert_id) = &assert_id_opt { if prover_choice == vir::def::ProverChoice::DefaultProver { default_prover_failed_assert_ids.push(assert_id.clone()); @@ -1366,6 +1397,7 @@ impl Verifier { } ValidityResult::Invalid(Some(air_model), Some(error), assert_id_opt) => { // Borrowed, not moved: the report reads the same id below. + failed_here.extend(assert_id_opt.iter().cloned()); if let Some(assert_id) = &assert_id_opt { if prover_choice == vir::def::ProverChoice::DefaultProver { default_prover_failed_assert_ids.push(assert_id.clone()); @@ -1466,6 +1498,23 @@ impl Verifier { } if is_check_valid && !is_singular { + if let Some(obs) = air_context.query_result_observer() { + let mut obs = obs.lock().unwrap(); + if let Some(o) = + obs.as_any_mut().downcast_mut::() + { + if let Some(raw) = o.take_query(&failed_here, timed_out, only_check_earlier) { + self.func_observations.entry(context.fun.clone()).or_default().push( + crate::observers::FiledQuery { + desc: context.desc.clone(), + span: context.span.as_string.clone(), + kind: query_op.kind(), + raw, + }, + ); + } + } + } air_context.finish_query(); } @@ -1696,6 +1745,17 @@ impl Verifier { } } + /// Render each query's observed obligations and counterexamples as + /// source, per function. + fn resolve_observations(&mut self, names: &vir::air_names::SourceNames) { + for (fun, queries) in std::mem::take(&mut self.func_observations) { + let (obligations, failing) = crate::observers::resolve(names, queries); + let details = self.func_details.entry(fun).or_default(); + details.obligations.extend(obligations); + details.failing_asserts.extend(failing); + } + } + /// Join each query's instantiation pressure to source, per function. fn resolve_inst_pressure(&mut self, symbols: &crate::provenance::Symbols) { for (fun, queries) in std::mem::take(&mut self.func_inst_pressure) { @@ -3365,6 +3425,9 @@ impl Verifier { self.resolve_unknown_reasons(&global_ctx); // Join the diagnostics raised while verifying to their source spans. self.resolve_raised_diagnostics(&reporter); + if !self.func_observations.is_empty() { + self.resolve_observations(&global_ctx.air_source_names.borrow().clone()); + } // Join what cvc5 reported (matching loops, instantiation pressure, // difficulty, provenance, nonlinear frontiers) back to source, per // function. The joins read the same symbols. diff --git a/source/rust_verify_test/tests/obligation_observer.rs b/source/rust_verify_test/tests/obligation_observer.rs new file mode 100644 index 0000000000..db19f8044c --- /dev/null +++ b/source/rust_verify_test/tests/obligation_observer.rs @@ -0,0 +1,166 @@ +//! `-V observers=coverage` and `-V observers=proof-state`, read back from +//! `--report-json`. These run cvc5 (no internal test mode), which is what +//! `proof-state`'s live model evaluation has to work against. + +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; + +use tempfile::TempDir; + +/// Verify `code` with the given observers and return the per-function +/// details of the report. +fn functions_for(code: &str, extra: &[&str]) -> serde_json::Value { + let tempdir = TempDir::new().expect("temp dir"); + let entry_file = tempdir.path().join("test.rs"); + let source = format!("{}\n{}\n{}\n", FEATURE_PRELUDE, USE_PRELUDE, code); + std::fs::write(&entry_file, source).expect("write source file"); + let report_path = tempdir.path().join("report.json"); + let mut args = vec!["--crate-type=lib", "--report-json", report_path.to_str().unwrap()]; + args.extend_from_slice(extra); + args.push(entry_file.to_str().unwrap()); + let output = run_verus_raw(&args, tempdir.path()); + let text = std::fs::read_to_string(&report_path).unwrap_or_else(|err| { + panic!( + "no report at {}: {err}\nstderr:\n{}", + report_path.display(), + String::from_utf8_lossy(&output.stderr) + ) + }); + let report: serde_json::Value = serde_json::from_str(&text).expect("valid json"); + report["functions"].clone() +} + +/// Each obligation of `f`'s queries as (message, status), in query order. +fn statuses(functions: &serde_json::Value, f: &str) -> Vec<(String, String)> { + functions[f]["obligations"] + .as_array() + .unwrap_or_else(|| panic!("no obligations for {}: {:#}", f, functions)) + .iter() + .flat_map(|q| q["obligations"].as_array().unwrap().iter()) + .map(|o| { + (o["message"].as_str().unwrap().to_string(), o["status"].as_str().unwrap().to_string()) + }) + .collect() +} + +const CODE: &str = r#" +verus!{ +fn bump(x: u32, y: u32) -> (r: u32) + requires x < 100, y < 100, + ensures r == x + y + 1, +{ + x + y +} + +fn fine(a: u32) -> (r: u32) + requires a < 10, + ensures r < 20, +{ + let b = a + 1; + assert(b <= 10); + b + 1 +} + +fn loops(n: u32) + requires n < 50, +{ + let mut i = 0; + while i < n + invariant i <= n, i < 40, + decreases n - i, + { + i = i + 1; + } +} + +fn two_bad(a: u32) { + assert(a < 5); + assert(a > 7); +} +} +"#; + +#[test] +fn coverage_says_what_became_of_each_obligation() { + let functions = functions_for(CODE, &["-V", "observers=coverage"]); + let s = |m: &str, st: &str| (m.to_string(), st.to_string()); + assert_eq!( + statuses(&functions, "test::fine"), + vec![ + s("possible arithmetic underflow/overflow", "proved"), + s("assertion failed", "proved"), + s("possible arithmetic underflow/overflow", "proved"), + s("postcondition not satisfied", "proved"), + ] + ); + assert!( + statuses(&functions, "test::bump").contains(&s("postcondition not satisfied", "failed")) + ); + // coverage alone does not collect counterexamples + assert!(functions["test::bump"].get("failing_asserts").is_none()); +} + +/// Loop invariants carry no assertion id: the failure is placed by its span, +/// not on the first id-less invariant. +#[test] +fn an_id_less_failure_lands_on_the_invariant_that_failed() { + let functions = functions_for(CODE, &["-V", "observers=coverage"]); + let loop_query = functions["test::loops"]["obligations"] + .as_array() + .unwrap() + .iter() + .find(|q| q["desc"] == "while loop") + .expect("the loop's query") + .clone(); + let ends: Vec<(String, String)> = loop_query["obligations"] + .as_array() + .unwrap() + .iter() + .filter(|o| o["message"] == "invariant not satisfied at end of loop body") + .map(|o| { + (o["span"].as_str().unwrap().to_string(), o["status"].as_str().unwrap().to_string()) + }) + .collect(); + assert_eq!(ends.len(), 2, "{ends:?}"); + assert_eq!(ends[0].1, "proved", "i <= n holds: {ends:?}"); + assert_eq!(ends[1].1, "failed", "i < 40 fails: {ends:?}"); +} + +/// With `--multiple-errors 0` the query ends at the first failure, so the +/// later assertion is unchecked, not proved. +#[test] +fn a_query_that_stops_early_leaves_obligations_unchecked() { + let functions = functions_for(CODE, &["-V", "observers=coverage", "--multiple-errors", "0"]); + let s = |m: &str, st: &str| (m.to_string(), st.to_string()); + assert_eq!( + statuses(&functions, "test::two_bad"), + vec![s("assertion failed", "failed"), s("assertion failed", "unchecked")] + ); +} + +/// The counterexample is read while it is live: the false conjunct, in +/// source spelling, and the value the loop counter has there. +#[test] +fn proof_state_reports_the_false_conjunct_and_its_values() { + let functions = functions_for(CODE, &["-V", "observers=proof-state"]); + let failing = functions["test::loops"]["failing_asserts"].as_array().expect("failing_asserts"); + assert_eq!(failing.len(), 1, "{failing:#?}"); + let f = &failing[0]; + assert_eq!(f["message"], "invariant not satisfied at end of loop body"); + assert_eq!(f["conjuncts"][0], serde_json::json!({ "term": "(i < 40)", "value": false })); + let i = f["values"] + .as_array() + .unwrap() + .iter() + .find(|v| v["name"] == "i") + .unwrap_or_else(|| panic!("no value for i: {:#}", f)); + assert_eq!(i["value"], "40"); + // proof-state alone does not collect coverage + assert!(functions["test::loops"].get("obligations").is_none()); + + let bump = &functions["test::bump"]["failing_asserts"][0]; + assert_eq!(bump["conjuncts"][0]["term"], "(r == ((x + y) + 1))"); + assert_eq!(bump["conjuncts"][0]["value"], false); +} diff --git a/source/vir/src/context.rs b/source/vir/src/context.rs index 3cbb12bcfd..e8c3db1cad 100644 --- a/source/vir/src/context.rs +++ b/source/vir/src/context.rs @@ -166,9 +166,7 @@ pub struct Ctx { /// AIR-level handles to the same shared observer object, carried here so the /// verifier can attach them to each `air::Context` it builds (see verifier.rs). pub air_observer: Option, - pub query_result_observer: Option< - air::query_result_observer::QueryResultObserverHandle, - >, + pub query_result_observer: Option, pub arch_word_bits: ArchWordBits, } diff --git a/source/vir/src/vir_observer.rs b/source/vir/src/vir_observer.rs index 7fa2cec2da..505eb8db4d 100644 --- a/source/vir/src/vir_observer.rs +++ b/source/vir/src/vir_observer.rs @@ -87,9 +87,7 @@ pub type VirObserverHandle = std::sync::Arc>; pub struct Observers { pub vir: Option, pub air: Option, - pub query_result: Option< - air::query_result_observer::QueryResultObserverHandle, - >, + pub query_result: Option, } use std::collections::{HashMap, VecDeque}; From 0d136406324495c14f0c6db36a7a68ac668ea3e4 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sun, 27 Sep 2026 21:17:10 +0000 Subject: [PATCH 5/7] Observers: split temporaries and preconditions, place id-less failures, reject unknown names Review fixes for -V observers=coverage / proof-state and the interface: - proof-state reads an asserted Verus temporary (`assert(a && b)` asserts `tmp%1`, defined by `assume (= tmp%1 e)`) as its definition, and a failing call's precondition `req%f(args)` as f's requires at those arguments, from the `req%` axioms `on_axiom_decl` sees; the axiom location labels are looked through. A temporary or precondition whose definition is not available is kept whole and marked `unexpanded`. Values are taken from what the split conjuncts read, without the encoding's own constants (Type, Dcr, Fuel sorts: `INT`, `$`, `TYPE%..`). - A failure without a model is placed by its id only when that id names exactly one undecided assertion (postconditions share ids). Such failures are passed as Option, so a bit-vector assert, which has no id, is `failed` rather than `unchecked`. Failures seen through the Invalid callback are no longer passed a second time. - get-unsat-core: cvc5 prints the core one name per line; the reply is parsed across lines (and |quoted| names), so -V axiom-usage-info no longer aborts under cvc5 and coverage lists used_axioms. - -V observers= names are checked in parse_args: unknown or empty names, and a test observer combined with another, are errors. - VersionOrigin::{BranchMerge, BreakMerge}, VirObserver::on_break_merge and the correlator's merge records are removed: a merge takes the highest version a branch reached, which that branch already created, so they never fired. - eval_expr keeps its single-line contract; the multi-line fallback is local to evaluate_bool. Co-Authored-By: Claude Opus 5.5 --- source/air/src/air_observer.rs | 12 +- source/air/src/context.rs | 29 +- source/air/src/lib.rs | 2 +- source/air/src/smt_verify.rs | 62 ++- source/air/src/var_to_const.rs | 82 ++-- source/air/src/visitor.rs | 3 +- source/rust_verify/src/config.rs | 11 +- source/rust_verify/src/observers.rs | 357 ++++++++++++++++-- source/rust_verify/src/test_observer.rs | 13 +- source/rust_verify/src/verifier.rs | 19 +- .../tests/obligation_observer.rs | 154 ++++++++ source/rust_verify_test/tests/observer.rs | 15 +- source/vir/src/def.rs | 4 +- source/vir/src/vir_observer.rs | 49 +-- 14 files changed, 653 insertions(+), 159 deletions(-) diff --git a/source/air/src/air_observer.rs b/source/air/src/air_observer.rs index 4685ce34ca..59857e3efc 100644 --- a/source/air/src/air_observer.rs +++ b/source/air/src/air_observer.rs @@ -19,10 +19,6 @@ pub enum VersionOrigin { Havoc, /// From a `StmtX::Assign` — constrained new version (= rhs). Assign, - /// Phantom version from Switch branch reconciliation. - BranchMerge, - /// Phantom version from Breakable break reconciliation. - BreakMerge, } /// Observer for the AIR-level verification pipeline. @@ -35,10 +31,10 @@ pub trait AirObserver: Any + Send { /// Called from `lower_query` at the moment a new WP version is created. /// - /// For `Havoc`/`Assign` origins, the Nth call for base variable `x` - /// corresponds to the Nth VIR-level `on_havoc` or `on_assign` callback - /// for `x`. For merge origins, the call corresponds to the most recent - /// `on_branch_merge` or `on_break_merge` callback. + /// The Nth call for base variable `x` corresponds to the Nth VIR-level + /// `on_havoc` or `on_assign` callback for `x`. Branch and break merges + /// create no versions: a merge takes the highest version a branch reached, + /// which that branch already created. /// /// See `VersionCorrelator` in `vir/src/vir_observer.rs` for a shared helper /// that correlates these callbacks with VIR-level data. diff --git a/source/air/src/context.rs b/source/air/src/context.rs index 1d256baf14..a9b3c59cfa 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -1658,14 +1658,10 @@ impl Context { self.smt_log.log_eval(expr); let smt_data = self.smt_log.take_pipe_data(); let smt_output = self.get_smt_process().send_commands(smt_data); - if smt_output.len() == 1 { - smt_output[0].clone() - } else { - // The solver prints multi-line output for compound model values (quantified - // formulas, algebraic data type constructors). These are never simple booleans, - // so return a value that callers will treat as unknown. - "unknown".to_string() + if smt_output.len() != 1 { + panic!("unexpected output from SMT eval {:?}", smt_output); } + smt_output[0].clone() } /// Evaluate an AIR expression against the current solver model as a boolean. @@ -1675,20 +1671,25 @@ impl Context { let printer = crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone()); let node = printer.expr_to_node(expr); + // A compound value (a quantified formula, a datatype constructor) + // may span several lines; it is never a boolean, so it reads as None. match self.solver { - SmtSolver::Z3 => match self.eval_expr(node).as_str() { - "true" => Some(true), - "false" => Some(false), - _ => None, - }, + SmtSolver::Z3 => { + self.smt_log.log_eval(node); + let smt_data = self.smt_log.take_pipe_data(); + match self.get_smt_process().send_commands(smt_data).as_slice() { + [line] if line == "true" => Some(true), + [line] if line == "false" => Some(false), + _ => None, + } + } // cvc5 has no `eval`: it takes the command for an unknown one // and the reader loses its place in the solver's output. // `get-value` answers `((expr value))` on one line. SmtSolver::Cvc5 => { self.smt_log.log_get_value(node); let smt_data = self.smt_log.take_pipe_data(); - let smt_output = self.get_smt_process().send_commands(smt_data); - match smt_output.as_slice() { + match self.get_smt_process().send_commands(smt_data).as_slice() { [line] if line.ends_with(" true))") => Some(true), [line] if line.ends_with(" false))") => Some(false), _ => None, diff --git a/source/air/src/lib.rs b/source/air/src/lib.rs index 7c2e5b8e3e..a57e595ff3 100644 --- a/source/air/src/lib.rs +++ b/source/air/src/lib.rs @@ -32,7 +32,7 @@ mod typecheck; mod util; mod var_to_const; pub use var_to_const::GoalScope; -mod visitor; +pub mod visitor; #[cfg(feature = "singular")] pub mod singular_manager; diff --git a/source/air/src/smt_verify.rs b/source/air/src/smt_verify.rs index f1b21efef2..2549e25fb6 100644 --- a/source/air/src/smt_verify.rs +++ b/source/air/src/smt_verify.rs @@ -666,20 +666,7 @@ pub(crate) fn smt_check_assertion<'ctx>( let smt_data = context.smt_log.take_pipe_data(); let smt_output = context.get_smt_process().send_commands(smt_data); - let mut smt_output = smt_output.into_iter(); - let unsat_core_str = - smt_output.next().expect("expected one line in the unsat core output"); - assert!(smt_output.next().is_none()); - - let fun_names: Vec = unsat_core_str - .strip_prefix('(') - .expect("invalid unsat core") - .strip_suffix(')') - .expect("invalid unsat core") - .split_terminator(' ') - .map(|x| Arc::new(x.to_owned())) - .collect(); - crate::context::UsageInfo::UsedAxioms(fun_names) + crate::context::UsageInfo::UsedAxioms(parse_unsat_core(&smt_output)) } else { crate::context::UsageInfo::None }; @@ -2111,6 +2098,53 @@ pub(crate) fn smt_check_query<'ctx>( result } +/// The names in a `(get-unsat-core)` reply. z3 prints the core on one line; +/// cvc5 puts one name per line. Names may be `|quoted|`. +pub(crate) fn parse_unsat_core(lines: &[String]) -> Vec { + let text = lines.join(" "); + let body = text + .trim() + .strip_prefix('(') + .and_then(|t| t.strip_suffix(')')) + .unwrap_or_else(|| panic!("invalid unsat core: {:?}", lines)); + let mut names = Vec::new(); + let mut rest = body.trim_start(); + while !rest.is_empty() { + let (name, tail) = match rest.strip_prefix('|') { + Some(quoted) => { + let end = + quoted.find('|').unwrap_or_else(|| panic!("invalid unsat core: {:?}", lines)); + ("ed[..end], "ed[end + 1..]) + } + None => { + let end = rest.find(char::is_whitespace).unwrap_or(rest.len()); + (&rest[..end], &rest[end..]) + } + }; + names.push(Arc::new(name.to_owned())); + rest = tail.trim_start(); + } + names +} + +#[cfg(test)] +mod unsat_core_tests { + use super::parse_unsat_core; + + fn names(lines: &[&str]) -> Vec { + let lines: Vec = lines.iter().map(|l| l.to_string()).collect(); + parse_unsat_core(&lines).iter().map(|n| n.to_string()).collect() + } + + #[test] + fn unsat_core_parses_one_line_and_one_name_per_line() { + assert_eq!(names(&["(a b)"]), ["a", "b"]); + assert_eq!(names(&["()"]), Vec::::new()); + assert_eq!(names(&["(", "a", "|b c|", ")"]), ["a", "b c"]); + assert_eq!(names(&["(a", "b)"]), ["a", "b"]); + } +} + #[cfg(test)] mod strategy_rung_tests { use super::parse_strategy_rung; diff --git a/source/air/src/var_to_const.rs b/source/air/src/var_to_const.rs index bcc3dbed38..f244c635bc 100644 --- a/source/air/src/var_to_const.rs +++ b/source/air/src/var_to_const.rs @@ -262,20 +262,6 @@ fn lower_stmt( state.break_versions.remove(label).expect("break_versions"); all_versions.insert(0, versions.clone()); update_versions_from_all_branches(&all_versions, versions); - // Notify observer of phantom versions created by break merge reconciliation - for x in versions.keys() { - let merged_version = versions[x]; - let had_explicit = all_versions.iter().any(|v| v[x] == merged_version); - if !had_explicit { - let renamed = Arc::new(rename_var(x, merged_version)); - state.notify_version_created( - x, - merged_version, - &renamed, - crate::air_observer::VersionOrigin::BreakMerge, - ); - } - } let mut break_i: usize = 1; let s = update_breaks_to_versions(label, &all_versions, versions, &mut break_i, &s); assert!(break_i == all_versions.len()); @@ -305,20 +291,6 @@ fn lower_stmt( state.all_snapshots.extend(snapshots_i); } update_versions_from_all_branches(&all_versions, versions); - // Notify observer of phantom versions created by merge reconciliation - for x in versions.keys() { - let merged_version = versions[x]; - let had_explicit = all_versions.iter().any(|v| v[x] == merged_version); - if !had_explicit { - let renamed = Arc::new(rename_var(x, merged_version)); - state.notify_version_created( - x, - merged_version, - &renamed, - crate::air_observer::VersionOrigin::BranchMerge, - ); - } - } for i in 0..ss.len() { stmts[i] = update_branch_to_versions(&all_versions[i], versions, &stmts[i], false); } @@ -477,4 +449,58 @@ mod tests { 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())); } + + /// A merge takes the highest version a branch reached, so every version + /// the lowered query declares was announced where a branch created it. + #[test] + fn merges_announce_no_versions_of_their_own() { + struct Announced(Vec<(String, crate::air_observer::VersionOrigin)>); + impl crate::air_observer::AirObserver for Announced { + fn on_wp_version_created( + &mut self, + versioned: &Ident, + kind: crate::air_observer::VersionOrigin, + ) { + self.0.push((versioned.to_string(), kind)); + } + fn as_any(&self) -> &dyn std::any::Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn std::any::Any { + self + } + } + let x = Arc::new("x@".to_string()); + let havoc = || Arc::new(StmtX::Havoc(x.clone())); + let block = |ss: Vec| Arc::new(StmtX::Block(Arc::new(ss))); + let label = Arc::new("l".to_string()); + // a switch whose branches reach x@1 and x@2, then a breakable whose + // break leaves at x@3 and whose fallthrough reaches x@4 + let query = Arc::new(QueryX { + local: Arc::new(vec![Arc::new(DeclX::Var(x.clone(), Arc::new(crate::ast::TypX::Int)))]), + assertion: block(vec![ + Arc::new(StmtX::Switch(Arc::new(vec![ + block(vec![havoc()]), + block(vec![havoc(), havoc()]), + ]))), + Arc::new(StmtX::Breakable( + label.clone(), + block(vec![havoc(), Arc::new(StmtX::Break(label.clone())), havoc()]), + )), + ]), + }); + let mut announced = Announced(Vec::new()); + let (_, _, decls, _) = lower_query(&query, false, Some(&mut announced)); + let declared: Vec = decls + .iter() + .filter_map(|d| match &**d { + DeclX::Const(c, _) if **c != "x@0" => Some(c.to_string()), + _ => None, + }) + .collect(); + let names: Vec = announced.0.iter().map(|(n, _)| n.clone()).collect(); + assert_eq!(names, ["x@1", "x@1", "x@2", "x@3", "x@4"]); + assert!(declared.iter().all(|d| names.contains(d)), "{:?} vs {:?}", declared, names); + assert!(announced.0.iter().all(|(_, k)| *k == crate::air_observer::VersionOrigin::Havoc)); + } } diff --git a/source/air/src/visitor.rs b/source/air/src/visitor.rs index cba86c0043..f99f016694 100644 --- a/source/air/src/visitor.rs +++ b/source/air/src/visitor.rs @@ -1,7 +1,8 @@ use crate::ast::{BindX, Binder, BinderX, Expr, ExprX, Stmt, StmtX, Trigger}; use std::sync::Arc; -pub(crate) fn map_expr_visitor Expr>(expr: &Expr, f: &mut F) -> Expr { +/// Rebuild `expr` bottom-up, applying `f` to each node after its children. +pub fn map_expr_visitor Expr>(expr: &Expr, f: &mut F) -> Expr { match &**expr { ExprX::Const(_) => f(expr), ExprX::Var(_) => f(expr), diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 6b83837f35..66d4c5c61a 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -522,7 +522,10 @@ pub fn parse_args_with_imports( EXTENDED_NO_BV_SIMPLIFY, "internal option to disable simplification of bit-vector assertions before sending to the SMT solver", ), - (EXTENDED_OBSERVERS, "Comma-separated list of observers (e.g., test)"), + ( + EXTENDED_OBSERVERS, + "Comma-separated observers: coverage and/or proof-state (reported in func-details under --output-json/--report-json)", + ), ]; let default_num_threads: usize = std::thread::available_parallelism() @@ -981,6 +984,12 @@ pub fn parse_args_with_imports( .unwrap_or_default(), }; + if extended.contains_key(EXTENDED_OBSERVERS) { + if let Err(msg) = crate::observers::check_names(&args.observers) { + error(format!("-V {EXTENDED_OBSERVERS}: {msg}")); + } + } + if args.nl_frontier && !matches!(args.solver, SmtSolver::Cvc5) { error( "-V nl-frontier requires cvc5 (it is unavailable for vstd and internal test mode)" diff --git a/source/rust_verify/src/observers.rs b/source/rust_verify/src/observers.rs index fb6fc73bbc..723a3bbc73 100644 --- a/source/rust_verify/src/observers.rs +++ b/source/rust_verify/src/observers.rs @@ -24,22 +24,45 @@ //! AIR text until the end of the crate, when [`resolve`] renders them as //! source with the names the encoders recorded. -use air::ast::{AssertId, Expr, ExprX, MultiOp, Query, Stmt, StmtX}; +use air::ast::{AssertId, BinaryOp, BindX, Expr, ExprX, Ident, MultiOp, Query, Stmt, StmtX}; use air::query_result_observer::CheckValidResult; use serde::Serialize; use std::any::Any; -use std::collections::BTreeSet; +use std::collections::{BTreeSet, HashMap}; use std::sync::Arc; /// The observer names this module serves. pub const COVERAGE: &str = "coverage"; pub const PROOF_STATE: &str = "proof-state"; +/// The observers the test suites register, one at a time. +pub const TEST_OBSERVERS: &[&str] = &["test", "air-only", "query-result-only", "vir-only"]; + +/// Whether `-V observers=` names a valid set: `coverage` and `proof-state` +/// in any combination, or a single test observer. +pub fn check_names(names: &[String]) -> Result<(), String> { + let known = |n: &str| n == COVERAGE || n == PROOF_STATE || TEST_OBSERVERS.contains(&n); + if names.is_empty() { + return Err(format!("expected a list of observers ({COVERAGE}, {PROOF_STATE})")); + } + if let Some(bad) = names.iter().find(|n| !known(n)) { + return Err(format!("unknown observer `{bad}`; expected {COVERAGE} and/or {PROOF_STATE}")); + } + let tests = names.iter().filter(|n| TEST_OBSERVERS.contains(&n.as_str())).count(); + if tests > 0 && names.len() > 1 { + return Err(format!("a test observer cannot be combined with others: {}", names.join(","))); + } + Ok(()) +} + /// A failing assertion's conjuncts are listed up to this many; the rest are /// counted in `conjuncts_omitted`. const MAX_CONJUNCTS: usize = 32; /// Likewise the variables whose counterexample values are reported. const MAX_VALUES: usize = 64; +/// How deeply temporaries and preconditions are expanded into their +/// definitions. +const MAX_TEMP_DEPTH: usize = 8; #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] #[serde(rename_all = "snake_case")] @@ -66,6 +89,10 @@ struct Assertion { /// The query being checked: its assertions, and the answers so far. struct Pending { assertions: Vec, + /// Each Verus temporary (`tmp%1`) the query defines exactly once, by + /// `assume (= tmp%1 e)`, with its definition. `assert(a && b)` asserts + /// such a temporary, so its conjuncts are those of the definition. + temps: HashMap, used_axioms: Option>, failing: Vec, } @@ -88,6 +115,10 @@ pub struct Obligation { pub struct Conjunct { pub term: String, pub value: Option, + /// A temporary or a callee's precondition (`req%f(args)`) whose + /// definition was not available, so it could not be split further. + #[serde(skip_serializing_if = "std::ops::Not::not")] + pub unexpanded: bool, } /// A variable the failing assertion reads, and its counterexample value. @@ -106,7 +137,8 @@ pub struct RawFailingAssert { assert_id: Option, message: String, span: Option, - conjuncts: Vec<(String, Option)>, + /// (term, value, unexpanded) + conjuncts: Vec<(String, Option, bool)>, conjuncts_omitted: usize, values: Vec<(String, String)>, values_omitted: usize, @@ -169,6 +201,11 @@ pub struct ObligationObserver { coverage: bool, proof_state: bool, pending: Option, + /// Under proof-state: each precondition function the context declared + /// (`req%f`), with its parameters and definition, from the axiom + /// `forall params. req%f(params) == body`. A failing call's + /// precondition splits into the conjuncts of its body. + requires: HashMap, Expr)>, } impl ObligationObserver { @@ -181,25 +218,33 @@ impl ObligationObserver { coverage, proof_state, pending: None, + requires: HashMap::new(), }) } /// Close the query just checked and hand over what was seen of it. /// - /// `failed` are the ids the verifier saw fail, which covers answers that - /// reach it without the `Invalid` callback (no model, bit-vector checks). + /// `failed` are the ids of the failures that reached the verifier + /// without the `Invalid` callback (no model: bit-vector and nonlinear + /// checks, which carry no id at all). Such an answer has no error span, + /// and ids are not unique (a function's postconditions share one; loop + /// invariants and bit-vector asserts have none), so a failure is placed + /// only when its id names exactly one undecided assertion; otherwise + /// which one failed is unknown, and they stay undecided. /// `truncated` says the verifier stopped checking obligations after the /// last failure (the `--multiple-errors` budget ran out), so a later /// `Valid` does not speak for them. pub fn take_query( &mut self, - failed: &[AssertId], + failed: &[Option], timed_out: bool, truncated: bool, ) -> Option { let mut pending = self.pending.take()?; - for a in pending.assertions.iter_mut() { - if a.status.is_none() && a.id.as_ref().is_some_and(|id| failed.contains(id)) { + for id in failed { + let mut undecided = + pending.assertions.iter_mut().filter(|a| a.status.is_none() && &a.id == id); + if let (Some(a), None) = (undecided.next(), undecided.next()) { a.status = Some(Status::Failed); } } @@ -261,15 +306,133 @@ fn collect_assertions(stmt: &Stmt, out: &mut Vec) { } } -/// The formula's top-level conjuncts, flattening nested conjunctions. -fn conjuncts(expr: &Expr, out: &mut Vec) { +/// The temporaries `stmt` defines exactly once, with their definitions. +fn temp_definitions(stmt: &Stmt) -> HashMap { + fn walk(stmt: &Stmt, defs: &mut HashMap>) { + match &**stmt { + StmtX::Assume(e) => { + if let ExprX::Binary(air::ast::BinaryOp::Eq, lhs, rhs) = &**e { + if let ExprX::Var(x) = &**lhs { + if x.starts_with(vir::def::PREFIX_TEMP_VAR) { + defs.entry(x.to_string()).or_default().push(rhs.clone()); + } + } + } + } + StmtX::DeadEnd(s) | StmtX::Breakable(_, s) => walk(s, defs), + StmtX::Block(ss) | StmtX::Switch(ss) => { + for s in ss.iter() { + walk(s, defs); + } + } + StmtX::Assert(..) + | StmtX::Havoc(_) + | StmtX::Assign(..) + | StmtX::Snapshot(_) + | StmtX::Break(_) => {} + } + } + let mut defs = HashMap::new(); + walk(stmt, &mut defs); + defs.into_iter() + .filter_map(|(x, mut es)| (es.len() == 1).then(|| (x, es.pop().unwrap()))) + .collect() +} + +/// A precondition function's definition, if `axiom` is the one Verus +/// declares for it: `forall params. req%f(params) == body` (or, with no +/// parameters, `req%f == body`). +fn requires_definition(axiom: &Expr) -> Option<(String, Vec, Expr)> { + let (params, eq): (Vec, &Expr) = match &**axiom { + ExprX::Bind(bind, body) => match &**bind { + BindX::Quant(air::ast::Quant::Forall, bs, _, _) => { + (bs.iter().map(|b| b.name.clone()).collect(), body) + } + _ => return None, + }, + _ => (Vec::new(), axiom), + }; + let ExprX::Binary(BinaryOp::Eq, lhs, body) = &**eq else { return None }; + let (f, args) = match &**lhs { + ExprX::Apply(f, args) => (f, args.iter().collect::>()), + ExprX::Var(f) => (f, Vec::new()), + _ => return None, + }; + let is_param = |(a, p): (&&Expr, &Ident)| matches!(&***a, ExprX::Var(x) if x == p); + (f.starts_with(vir::def::PREFIX_REQUIRES) + && args.len() == params.len() + && args.iter().zip(params.iter()).all(is_param)) + .then(|| (f.to_string(), params, body.clone())) +} + +/// `body` with each parameter replaced by its argument; `None` when a +/// binder inside `body` shadows a parameter. +fn instantiate(params: &[Ident], args: &[Expr], body: &Expr) -> Option { + let mut shadowed = false; + air::visitor::map_expr_visitor(body, &mut |e| { + if let ExprX::Bind(bind, _) = &**e { + let names: Vec<&Ident> = match &**bind { + BindX::Let(bs) => bs.iter().map(|b| &b.name).collect(), + BindX::Quant(_, bs, _, _) + | BindX::Lambda(bs, _, _) + | BindX::Choose(bs, _, _, _) => bs.iter().map(|b| &b.name).collect(), + }; + shadowed |= names.iter().any(|n| params.contains(n)); + } + e.clone() + }); + if shadowed { + return None; + } + Some(air::visitor::map_expr_visitor(body, &mut |e| match &**e { + ExprX::Var(x) => match params.iter().position(|p| p == x) { + Some(i) => args[i].clone(), + None => e.clone(), + }, + _ => e.clone(), + })) +} + +/// What a failing assertion's conjuncts may be read through. +struct Definitions<'a> { + temps: &'a HashMap, + requires: &'a HashMap, Expr)>, +} + +/// The formula's top-level conjuncts, flattening nested conjunctions, +/// reading a temporary as its definition and a callee's precondition as +/// its body at the call's arguments. Each comes with whether it is a +/// temporary or precondition that could not be read that way. +fn conjuncts(expr: &Expr, defs: &Definitions, depth: usize, out: &mut Vec<(Expr, bool)>) { + let deeper = depth < MAX_TEMP_DEPTH; match &**expr { ExprX::Multi(MultiOp::And, es) => { for e in es.iter() { - conjuncts(e, out); + conjuncts(e, defs, depth, out); + } + } + // a precondition's `axiom_location`, once labelled: + // `%%global_location_label%%N => e` + ExprX::Binary(BinaryOp::Implies, label, e) if matches!(&**label, ExprX::Var(l) if l.starts_with(air::def::GLOBAL_PREFIX_LABEL)) => { + conjuncts(e, defs, depth, out) + } + ExprX::LabeledAxiom(_, _, e) => conjuncts(e, defs, depth, out), + ExprX::Var(x) if deeper && defs.temps.contains_key(&**x) => { + conjuncts(&defs.temps[&**x], defs, depth + 1, out) + } + ExprX::Var(x) if x.starts_with(vir::def::PREFIX_TEMP_VAR) => out.push((expr.clone(), true)), + ExprX::Apply(f, args) if f.starts_with(vir::def::PREFIX_REQUIRES) => { + let body = defs + .requires + .get(&**f) + .filter(|_| deeper) + .and_then(|(params, body)| instantiate(params, args, body)); + match body { + Some(body) => conjuncts(&body, defs, depth + 1, out), + None => out.push((expr.clone(), true)), } } - _ => out.push(expr.clone()), + _ => out.push((expr.clone(), false)), } } @@ -336,6 +499,15 @@ fn free_constants(expr: &Expr, bound: &mut Vec, out: &mut BTreeSet bool { + use vir::def::{DECORATION, FUEL_ID, FUEL_TYPE, TYPE}; + matches!(&**typ, air::ast::TypX::Named(n) + if [TYPE, DECORATION, FUEL_TYPE, FUEL_ID].contains(&n.as_str())) +} + fn term_text(expr: &Expr) -> String { let printer = air::printer::Printer::new( Arc::new(air::messages::AirMessageInterface {}), @@ -347,6 +519,14 @@ fn term_text(expr: &Expr) -> String { } impl air::air_observer::AirObserver for ObligationObserver { + fn on_axiom_decl(&mut self, expr: &Expr) { + if self.proof_state { + if let Some((f, params, body)) = requires_definition(expr) { + self.requires.insert(f, (params, body)); + } + } + } + fn on_query_lowered( &mut self, query: &Query, @@ -355,7 +535,9 @@ impl air::air_observer::AirObserver for ObligationObserver { ) { let mut assertions = Vec::new(); collect_assertions(&query.assertion, &mut assertions); - self.pending = Some(Pending { assertions, used_axioms: None, failing: Vec::new() }); + let temps = + if self.proof_state { temp_definitions(&query.assertion) } else { HashMap::new() }; + self.pending = Some(Pending { assertions, temps, used_axioms: None, failing: Vec::new() }); } fn as_any(&self) -> &dyn Any { @@ -409,24 +591,32 @@ impl air::query_result_observer::QueryResultObserver for ObligationObserver { return; } let mut parts = Vec::new(); - conjuncts(&a.expr, &mut parts); - let mut evaluated: Vec<(String, Option)> = - parts.iter().map(|c| (term_text(c), eval_bool_expr(c))).collect(); + let defs = Definitions { temps: &pending.temps, requires: &self.requires }; + conjuncts(&a.expr, &defs, 0, &mut parts); + let mut evaluated: Vec<(String, Option, bool)> = parts + .iter() + .map(|(c, unexpanded)| (term_text(c), eval_bool_expr(c), *unexpanded)) + .collect(); // false first: those are why the assertion failed - evaluated.sort_by_key(|(_, v)| match v { + evaluated.sort_by_key(|(_, v, _)| match v { Some(false) => 0, None => 1, Some(true) => 2, }); let conjuncts_omitted = evaluated.len().saturating_sub(MAX_CONJUNCTS); evaluated.truncate(MAX_CONJUNCTS); + // what the conjuncts read, so an expanded temporary shows + // the variables of its definition let mut symbols = BTreeSet::new(); - free_constants(&a.expr, &mut Vec::new(), &mut symbols); + for (part, _) in parts.iter() { + free_constants(part, &mut Vec::new(), &mut symbols); + } let mut values: Vec<(String, String)> = symbols .into_iter() .filter_map(|s| { let def = model_defs.get(&Arc::new(s.clone()))?; - def.params.is_empty().then(|| (s, def.body.to_string())) + (def.params.is_empty() && !is_encoding_sort(&def.ret)) + .then(|| (s, def.body.to_string())) }) .collect(); let values_omitted = values.len().saturating_sub(MAX_VALUES); @@ -509,7 +699,11 @@ pub fn resolve( conjuncts: f .conjuncts .into_iter() - .map(|(term, value)| Conjunct { term: render_unversioned(names, &term), value }) + .map(|(term, value, unexpanded)| Conjunct { + term: render_unversioned(names, &term), + value, + unexpanded, + }) .collect(), conjuncts_omitted: f.conjuncts_omitted, values: f @@ -547,6 +741,20 @@ mod tests { assert!(ObligationObserver::from_names(&names(&["test"])).is_none()); } + #[test] + fn observer_names_are_checked() { + let names = |ns: &[&str]| ns.iter().map(|n| n.to_string()).collect::>(); + assert!(check_names(&names(&["coverage", "proof-state"])).is_ok()); + assert!(check_names(&names(&["test"])).is_ok()); + assert!( + check_names(&names(&["covrage"])).unwrap_err().contains("unknown observer `covrage`") + ); + assert!(check_names(&names(&["coverage", ""])).is_err()); + assert!(check_names(&names(&["test", "coverage"])).is_err()); + assert!(check_names(&names(&["test", "vir-only"])).is_err()); + assert!(check_names(&[]).is_err()); + } + #[test] fn versions_are_dropped_before_rendering() { let names = vir::air_names::SourceNames::new(); @@ -557,11 +765,89 @@ mod tests { fn conjuncts_flatten_nested_ands() { let and = |es: Vec| Arc::new(ExprX::Multi(MultiOp::And, Arc::new(es))); let e = and(vec![var("a"), and(vec![var("b"), var("c")])]); + let (temps, requires) = (HashMap::new(), HashMap::new()); let mut out = Vec::new(); - conjuncts(&e, &mut out); + conjuncts(&e, &Definitions { temps: &temps, requires: &requires }, 0, &mut out); assert_eq!(out.len(), 3); } + /// `assert(a && b)` asserts a temporary; its conjuncts are its + /// definition's. A temporary defined on two branches is left alone. + #[test] + fn temporaries_read_as_their_definitions() { + let and = |es: Vec| Arc::new(ExprX::Multi(MultiOp::And, Arc::new(es))); + let def = |x: &str, e: Expr| { + Arc::new(StmtX::Assume(Arc::new(ExprX::Binary(BinaryOp::Eq, var(x), e)))) + }; + let block = |ss: Vec| Arc::new(StmtX::Block(Arc::new(ss))); + let body = block(vec![ + def("tmp%1", and(vec![var("a@0"), var("tmp%2")])), + def("tmp%2", and(vec![var("b@1"), var("c!")])), + Arc::new(StmtX::Switch(Arc::new(vec![def("tmp%3", var("d")), def("tmp%3", var("e"))]))), + ]); + let temps = temp_definitions(&body); + assert!(temps.contains_key("tmp%1") && !temps.contains_key("tmp%3")); + let requires = HashMap::new(); + let defs = Definitions { temps: &temps, requires: &requires }; + let split = |e: Expr| { + let mut out = Vec::new(); + conjuncts(&e, &defs, 0, &mut out); + out.iter().map(|(c, unexpanded)| (term_text(c), *unexpanded)).collect::>() + }; + let s = |t: &str, u: bool| (t.to_string(), u); + assert_eq!(split(var("tmp%1")), [s("a@0", false), s("b@1", false), s("c!", false)]); + assert_eq!(split(var("tmp%3")), [s("tmp%3", true)]); + } + + /// A failing call's precondition `req%f(args)` splits into the + /// conjuncts of `f`'s requires at those arguments, read through the + /// labels Verus puts on each requires clause. + #[test] + fn preconditions_read_as_their_definitions() { + let int = Arc::new(TypX::Int); + let binder = + |x: &str| Arc::new(air::ast::BinderX { name: Arc::new(x.to_string()), a: int.clone() }); + let app = + |f: &str, es: Vec| Arc::new(ExprX::Apply(Arc::new(f.to_string()), Arc::new(es))); + let bin = |op, a, b| Arc::new(ExprX::Binary(op, a, b)); + let labelled = |n: &str, e| { + bin(BinaryOp::Implies, var(&format!("{}{}", air::def::GLOBAL_PREFIX_LABEL, n)), e) + }; + let body = Arc::new(ExprX::Multi( + MultiOp::And, + Arc::new(vec![ + labelled("0", bin(BinaryOp::Gt, var("y!"), var("five"))), + labelled("1", bin(BinaryOp::Lt, var("y!"), var("z!"))), + ]), + )); + let axiom = Arc::new(ExprX::Bind( + Arc::new(BindX::Quant( + air::ast::Quant::Forall, + Arc::new(vec![binder("y!"), binder("z!")]), + Arc::new(vec![]), + None, + )), + bin(BinaryOp::Eq, app("req%m!g.", vec![var("y!"), var("z!")]), body), + )); + let mut o = ObligationObserver::from_names(&["proof-state".to_string()]).unwrap(); + air::air_observer::AirObserver::on_axiom_decl(&mut o, &axiom); + assert!(o.requires.contains_key("req%m!g.")); + let temps = HashMap::new(); + let defs = Definitions { temps: &temps, requires: &o.requires }; + let mut out = Vec::new(); + conjuncts(&app("req%m!g.", vec![var("a@1"), var("seven")]), &defs, 0, &mut out); + let terms: Vec<(String, bool)> = out.iter().map(|(c, u)| (term_text(c), *u)).collect(); + assert_eq!( + terms, + [("(> a@1 five)".to_string(), false), ("(< a@1 seven)".to_string(), false)] + ); + // a callee whose requires the context never declared stays whole + let mut out = Vec::new(); + conjuncts(&app("req%m!h.", vec![var("a@1")]), &defs, 0, &mut out); + assert_eq!(out.len(), 1); + assert!(out[0].1); + } + #[test] fn free_constants_skip_bound_variables() { let binder = @@ -588,7 +874,12 @@ mod tests { #[test] fn take_query_fills_statuses() { - let mut o = ObligationObserver { coverage: true, proof_state: false, pending: None }; + let mut o = ObligationObserver { + coverage: true, + proof_state: false, + pending: None, + requires: HashMap::new(), + }; let id = |n: u64| Some(Arc::new(vec![n])); let assertion = |n: u64, status| Assertion { id: id(n), @@ -599,6 +890,7 @@ mod tests { }; let pending = |o: &mut ObligationObserver| { o.pending = Some(Pending { + temps: HashMap::new(), assertions: vec![ assertion(0, Some(Status::Proved)), assertion(1, Some(Status::Failed)), @@ -617,12 +909,31 @@ mod tests { assert_eq!(statuses(q), vec![Proved, Failed, Unchecked, Unchecked]); // #3 failed without an Invalid callback (no model) pending(&mut o); - let q = o.take_query(&[Arc::new(vec![3])], false, false).unwrap(); + let q = o.take_query(&[id(3)], false, false).unwrap(); assert_eq!(statuses(q), vec![Proved, Failed, Proved, Failed]); // the solver gave up pending(&mut o); let q = o.take_query(&[], true, false).unwrap(); assert_eq!(statuses(q), vec![Proved, Failed, Proved, Unknown]); + // two undecided postconditions share the id that failed without a + // model: which one failed is not known + o.pending = Some(Pending { + temps: HashMap::new(), + assertions: vec![assertion(5, None), assertion(5, None), assertion(6, None)], + used_axioms: None, + failing: Vec::new(), + }); + let q = o.take_query(&[id(5), id(6)], false, false).unwrap(); + assert_eq!(statuses(q), vec![Unchecked, Unchecked, Failed]); + // a bit-vector assert has no id, and fails without a model + o.pending = Some(Pending { + temps: HashMap::new(), + assertions: vec![Assertion { id: None, ..assertion(0, None) }], + used_axioms: None, + failing: Vec::new(), + }); + let q = o.take_query(&[None], false, false).unwrap(); + assert_eq!(statuses(q), vec![Failed]); assert!(o.take_query(&[], false, false).is_none()); } } diff --git a/source/rust_verify/src/test_observer.rs b/source/rust_verify/src/test_observer.rs index e1d917c760..91db283466 100644 --- a/source/rust_verify/src/test_observer.rs +++ b/source/rust_verify/src/test_observer.rs @@ -29,7 +29,6 @@ pub struct TestObserver { pub havocs: Vec, pub assigns: Vec, pub branch_merges: usize, - pub break_merges: usize, pub variable_defs: Vec, pub for_loop_vars: Vec<(String, String)>, pub reveal_strings: Vec, @@ -75,7 +74,6 @@ impl TestObserver { havocs: vec![], assigns: vec![], branch_merges: 0, - break_merges: 0, variable_defs: vec![], for_loop_vars: vec![], reveal_strings: vec![], @@ -153,7 +151,7 @@ impl TestObserver { "OBSERVER:{{", "\"krate_function_names\":{},\"krate_datatype_names\":{},", "\"havocs\":{},\"assigns\":{},", - "\"branch_merges\":{},\"break_merges\":{},", + "\"branch_merges\":{},", "\"variable_defs\":{},\"for_loop_vars\":{},", "\"reveal_strings\":{},", "\"quantifier_binders\":{},", @@ -181,7 +179,6 @@ impl TestObserver { Self::json_strings(&self.havocs), Self::json_strings(&self.assigns), self.branch_merges, - self.break_merges, Self::json_strings(&self.variable_defs), Self::json_string_pairs(&self.for_loop_vars), Self::json_strings(&self.reveal_strings), @@ -345,15 +342,9 @@ impl vir::vir_observer::VirObserver for TestObserver { self.events.push(format!("assign:{}", base)); self.correlator.record_havoc_or_assign(&base, stm); } - fn on_branch_merge(&mut self, stm: &vir::sst::Stm) { + fn on_branch_merge(&mut self, _stm: &vir::sst::Stm) { self.branch_merges += 1; self.events.push("branch_merge".to_string()); - self.correlator.record_branch_merge(stm); - } - fn on_break_merge(&mut self, stm: &vir::sst::Stm) { - self.break_merges += 1; - self.events.push("break_merge".to_string()); - self.correlator.record_break_merge(stm); } fn on_variable_def(&mut self, _stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { self.variable_defs.push(vir::def::suffix_local_unique_id(var).to_string()); diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index 07e12ae755..fe279958f8 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -65,7 +65,8 @@ fn create_observer(name: &str) -> vir::vir_observer::Observers { let vir: vir::vir_observer::VirObserverHandle = o; vir::vir_observer::Observers { vir: Some(vir), ..Default::default() } } - _ => vir::vir_observer::Observers::default(), + // parse_args rejected any other name + _ => unreachable!("unknown observer {name}"), } } @@ -81,9 +82,7 @@ fn create_observer_from_args(names: &[String]) -> vir::vir_observer::Observers { ..Default::default() }; } - if names.len() > 1 { - panic!("only one observer may be specified at a time; got: {:?}", names); - } + // parse_args allows a test observer only alone names.first().map_or_else(Default::default, |n| create_observer(n)) } @@ -1231,8 +1230,9 @@ impl Verifier { let mut invalidity = false; let mut timed_out = false; let mut used_axioms = None; - // the ids this query failed at, for an observer that missed the answer - let mut failed_here: Vec = Vec::new(); + // the ids of this query's failures without a model, which an + // observer's Invalid callback did not see + let mut failed_here: Vec> = Vec::new(); // 0 for the query's first check, then one per multi-error round let mut round = 0usize; loop { @@ -1365,8 +1365,11 @@ impl Verifier { ValidityResult::Invalid(None, error, assert_id_opt) | ValidityResult::Invalid(_, error @ None, assert_id_opt) => { // no model, but the obligation may still be known + // No model, so no observer callback: the observer + // places this failure from its id (none for a + // bit-vector assert) when the query is drained. + failed_here.push(assert_id_opt.clone()); // Borrowed, not moved: the report reads the same id below. - failed_here.extend(assert_id_opt.iter().cloned()); if let Some(assert_id) = &assert_id_opt { if prover_choice == vir::def::ProverChoice::DefaultProver { default_prover_failed_assert_ids.push(assert_id.clone()); @@ -1396,8 +1399,8 @@ impl Verifier { break; } ValidityResult::Invalid(Some(air_model), Some(error), assert_id_opt) => { + // The observer saw this one through its Invalid callback. // Borrowed, not moved: the report reads the same id below. - failed_here.extend(assert_id_opt.iter().cloned()); if let Some(assert_id) = &assert_id_opt { if prover_choice == vir::def::ProverChoice::DefaultProver { default_prover_failed_assert_ids.push(assert_id.clone()); diff --git a/source/rust_verify_test/tests/obligation_observer.rs b/source/rust_verify_test/tests/obligation_observer.rs index db19f8044c..f601b01694 100644 --- a/source/rust_verify_test/tests/obligation_observer.rs +++ b/source/rust_verify_test/tests/obligation_observer.rs @@ -164,3 +164,157 @@ fn proof_state_reports_the_false_conjunct_and_its_values() { assert_eq!(bump["conjuncts"][0]["term"], "(r == ((x + y) + 1))"); assert_eq!(bump["conjuncts"][0]["value"], false); } + +const MORE: &str = r#" +use vstd::prelude::*; +verus!{ +fn conj(a: u32, b: u32) + requires a > 2, +{ + assert(a > 3 && b < 2); +} + +fn bits(x: u32) { + assert(x & 1 == 0) by (bit_vector); +} + +fn callee(y: u32, z: u32) + requires y > 5 && y < z, z < 100, +{ +} + +fn caller(y: u32) { + callee(y, 7); +} + +fn all_big(v: &Vec) -> (r: u64) + requires v.len() > 0, + ensures forall|i: int| 0 <= i < v.len() ==> v[i] <= r, +{ + v[0] +} + +fn fine(a: u32) -> (r: u32) + requires a < 10, + ensures r == a, +{ + a +} +} +"#; + +/// The failing assertion of `f`, as (term, value) per conjunct, and the +/// symbols it reports values for. +fn failing( + functions: &serde_json::Value, + f: &str, +) -> (Vec<(String, serde_json::Value)>, Vec) { + let failing = functions[f]["failing_asserts"] + .as_array() + .unwrap_or_else(|| panic!("no failing_asserts for {}: {:#}", f, functions[f])); + assert_eq!(failing.len(), 1, "{failing:#?}"); + let conjuncts = failing[0]["conjuncts"] + .as_array() + .unwrap() + .iter() + .map(|c| (c["term"].as_str().unwrap().to_string(), c["value"].clone())) + .collect(); + let symbols = failing[0]["values"] + .as_array() + .unwrap() + .iter() + .map(|v| v["symbol"].as_str().unwrap().to_string()) + .collect(); + (conjuncts, symbols) +} + +/// `assert(a && b)` asserts a Verus temporary; proof-state splits it into +/// the conjuncts of its definition and reports the variables they read. +#[test] +fn proof_state_splits_an_asserted_conjunction() { + let functions = functions_for(MORE, &["-V", "observers=proof-state"]); + let (conjuncts, symbols) = failing(&functions, "test::conj"); + assert_eq!( + conjuncts, + vec![ + ("(a > 3)".to_string(), serde_json::json!(false)), + ("(b < 2)".to_string(), serde_json::json!(true)), + ] + ); + assert_eq!(symbols, vec!["a!", "b!"]); +} + +/// A failing call's precondition splits into the callee's requires +/// clauses at the call's arguments. +#[test] +fn proof_state_splits_a_callee_precondition() { + let functions = functions_for(MORE, &["-V", "observers=proof-state"]); + let (conjuncts, symbols) = failing(&functions, "test::caller"); + let terms: Vec<&str> = conjuncts.iter().map(|(t, _)| t.as_str()).collect(); + assert_eq!(terms, vec!["(y > 5)", "(y < 7)", "(7 < 100)"]); + assert_eq!(conjuncts[0].1, serde_json::json!(false)); + assert_eq!(symbols, vec!["y!"]); +} + +/// Values are the program's: the encoding's type ids and decorations +/// (`INT`, `$`, `TYPE%...`) are left out. +#[test] +fn proof_state_values_leave_out_encoding_constants() { + let functions = functions_for(MORE, &["-V", "observers=proof-state"]); + let (_, symbols) = failing(&functions, "test::all_big"); + assert_eq!(symbols, vec!["r!", "v!"]); +} + +/// A bit-vector assert fails without a model and without an assertion id; +/// coverage still says it failed. +#[test] +fn coverage_marks_a_failing_bit_vector_assert_failed() { + let functions = functions_for(MORE, &["-V", "observers=coverage"]); + let s = |m: &str, st: &str| (m.to_string(), st.to_string()); + assert!( + statuses(&functions, "test::bits") + .contains(&s("bitvector assertion not satisfied", "failed")), + "{:#}", + functions["test::bits"] + ); +} + +/// Under `-V axiom-usage-info` a proved query lists its unsat core; cvc5 +/// prints the core over several lines. +#[test] +fn coverage_lists_used_axioms_under_cvc5() { + let functions = functions_for(MORE, &["-V", "observers=coverage", "-V", "axiom-usage-info"]); + let queries = functions["test::fine"]["obligations"].as_array().expect("obligations"); + let body = queries.iter().find(|q| q["kind"] == "body").expect("the body query"); + assert!(body["used_axioms"].is_array(), "{:#}", body); + let with_axioms = functions + .as_object() + .unwrap() + .values() + .flat_map(|f| f["obligations"].as_array().into_iter().flatten()) + .filter(|q| q["used_axioms"].as_array().is_some_and(|a| !a.is_empty())) + .count(); + assert!(with_axioms > 0, "no proved query named an axiom: {:#}", functions); +} + +/// An observer name Verus does not know is an error, not a run without it. +#[test] +fn unknown_observer_names_are_rejected() { + for (names, expected) in [ + ("covrage", "unknown observer `covrage`"), + ("coverage,", "unknown observer ``"), + ("test,coverage", "cannot be combined"), + ] { + let tempdir = TempDir::new().expect("temp dir"); + let entry_file = tempdir.path().join("test.rs"); + std::fs::write(&entry_file, format!("{}\n{}\n", FEATURE_PRELUDE, USE_PRELUDE)).unwrap(); + let observers = format!("observers={names}"); + let output = run_verus_raw( + &["--crate-type=lib", "-V", &observers, entry_file.to_str().unwrap()], + tempdir.path(), + ); + let stderr = String::from_utf8_lossy(&output.stderr); + assert!(!output.status.success(), "{}: {}", names, stderr); + assert!(stderr.contains(expected), "{}: {}", names, stderr); + } +} diff --git a/source/rust_verify_test/tests/observer.rs b/source/rust_verify_test/tests/observer.rs index 82224baa16..929b880c44 100644 --- a/source/rust_verify_test/tests/observer.rs +++ b/source/rust_verify_test/tests/observer.rs @@ -13,7 +13,6 @@ //! on_havoc | + | 0 | 0 | 0 | + | + | + | | | //! on_assign (names) | + | + | 0 | 0 | + | | + | | | //! on_branch_merge | + | 0 | 0 | 0 | + | 0 | 0 | | | -//! on_break_merge | 0 | 0 | 0 | 0 | + | 0 | 0 | | | //! on_variable_def (names) | + | | 0 | 0 | | | | | | //! on_for_loop_var (ghost, user) | 0 | 0 | 0 | 0 | 0 | + | 0 | | | //! on_reveal_string | | | | | | | | + | | @@ -47,7 +46,6 @@ struct D { havocs: Vec, assigns: Vec, branch_merges: usize, - break_merges: usize, variable_defs: Vec, for_loop_vars: Vec<(String, String)>, reveal_strings: Vec, @@ -207,7 +205,7 @@ fn val<'a>(json: &'a str, key: &str) -> &'a str { } else if rest.starts_with('[') { &rest[..rest.find(']').unwrap() + 1] } else { - let end = rest.find(|c: char| c == ',' || c == '}').unwrap_or(rest.len()); + let end = rest.find([',', '}']).unwrap_or(rest.len()); rest[..end].trim() } } @@ -232,7 +230,6 @@ fn parse_note(note_text: &str) -> D { havocs: strings(val(json, "havocs")), assigns: strings(val(json, "assigns")), branch_merges: val(json, "branch_merges").parse().unwrap(), - break_merges: val(json, "break_merges").parse().unwrap(), variable_defs: strings(val(json, "variable_defs")), for_loop_vars: string_pairs(val(json, "for_loop_vars")), reveal_strings: strings(val(json, "reveal_strings")), @@ -346,7 +343,7 @@ test_verify_one_file_with_options! { assert!(d.check_valid_invalid >= 1); assert!(d.check_valid_valid >= 1); assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); - assert!(d.eval_expr_results.iter().any(|r| *r == Some(true)), + assert!(d.eval_expr_results.contains(&Some(true)), "eval_bool_expr(true) should return Some(true), got {:?}", d.eval_expr_results); // Version correlations: loop-modified variables have havoc and assign entries assert!(!d.version_correlations.is_empty(), @@ -369,7 +366,6 @@ test_verify_one_file_with_options! { "x should have >= 2 distinct lines, got {:?}", x_lines); // Negatives assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); - assert_eq!(d.break_merges, 0); assert!(d.for_loop_vars.is_empty()); assert!(d.quantifier_binders.is_empty()); assert!(d.lambda_decls.is_empty()); @@ -405,7 +401,6 @@ test_verify_one_file_with_options! { // Negatives assert!(d.havocs.is_empty()); assert_eq!(d.branch_merges, 0); - assert_eq!(d.break_merges, 0); assert!(d.for_loop_vars.is_empty()); assert!(d.lambda_decls.is_empty()); assert!(d.choose_decls.is_empty()); @@ -435,7 +430,6 @@ test_verify_one_file_with_options! { // Negatives assert!(d.havocs.is_empty()); assert_eq!(d.branch_merges, 0); - assert_eq!(d.break_merges, 0); assert!(d.for_loop_vars.is_empty()); assert!(d.quantifier_binders.is_empty()); assert!(d.lambda_decls.is_empty()); @@ -472,7 +466,6 @@ test_verify_one_file_with_options! { assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); // Negatives assert!(d.havocs.is_empty()); - assert_eq!(d.break_merges, 0); assert!(d.for_loop_vars.is_empty()); } } @@ -502,8 +495,7 @@ test_verify_one_file_with_options! { } } => Err(err) => { let d = parse(&err); - // Break: loop isolation may prevent break_merge from firing, - // but branch_merges should increase from the if + break structure + // The if + break structure produces branch merges assert!(d.branch_merges > 0, "if should trigger branch_merge, got {}", d.branch_merges); // Assigns assert!(has(&d.assigns, "found@"), "got {:?}", d.assigns); @@ -549,7 +541,6 @@ test_verify_one_file_with_options! { assert!(!d.for_loop_vars.is_empty(), "for-loop should be detected"); // Negatives assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); - assert_eq!(d.break_merges, 0); assert!(d.choose_decls.is_empty()); } } diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs index 2fd44b0843..f79346affc 100644 --- a/source/vir/src/def.rs +++ b/source/vir/src/def.rs @@ -47,14 +47,14 @@ const SUFFIX_PATH: &str = "."; const PREFIX_ESCAPE: &str = "$~"; const PREFIX_FUEL_ID: &str = "fuel%"; const PREFIX_FUEL_NAT: &str = "fuel_nat%"; -const PREFIX_REQUIRES: &str = "req%"; +pub const PREFIX_REQUIRES: &str = "req%"; const PREFIX_ENSURES: &str = "ens%"; const PREFIX_ENSURES_ASYNC_RET: &str = "VERUS_ASYNC_FUNC_RETURN_VALUE_"; const PREFIX_OPEN_INV: &str = "openinv%"; const PREFIX_NO_UNWIND_WHEN: &str = "no_unwind_when%"; const PREFIX_RECURSIVE: &str = "rec%"; const PREFIX_SIMPLIFY_TEMP_VAR: &str = "tmp%%"; -const PREFIX_TEMP_VAR: &str = "tmp%"; +pub const PREFIX_TEMP_VAR: &str = "tmp%"; pub const PREFIX_EXPAND_ERRORS_TEMP_VAR: &str = "expand%"; const PREFIX_PRE_VAR: &str = "pre%"; /// Datatype box/unbox: `(Poly%D. x)` and `(%Poly%D. p)`. Public because a diff --git a/source/vir/src/vir_observer.rs b/source/vir/src/vir_observer.rs index 505eb8db4d..8db3c1dfd4 100644 --- a/source/vir/src/vir_observer.rs +++ b/source/vir/src/vir_observer.rs @@ -1,7 +1,7 @@ //! VIR-level verification observer. //! //! Defines `VirObserver` — callbacks fired during VIR→AIR lowering (havoc, -//! assign, branch/break merges, loops, quantifier binders, reveals, and +//! assign, branch merges, loops, quantifier binders, reveals, and //! function/krate lifecycle). //! //! This trait is independent: it does **not** require `AirObserver` or @@ -46,7 +46,6 @@ pub trait VirObserver: Any + Send { fn on_assign(&mut self, _stm: &Stm, _var: &VarIdent) {} fn on_variable_def(&mut self, _stm: &Stm, _var: &VarIdent) {} fn on_branch_merge(&mut self, _stm: &Stm) {} - fn on_break_merge(&mut self, _stm: &Stm) {} fn on_for_loop(&mut self, _stm: &Stm) {} fn on_quantifier_binder(&mut self, _binder: &crate::ast::VarBinder, _exp: &Exp) {} fn on_reveal_string(&mut self, _lit: &std::sync::Arc) {} @@ -120,15 +119,11 @@ fn strip_version_suffix(name: &str) -> &str { pub struct VersionCorrelator { /// Per-base-variable queue of VIR statements (Havoc/Assign). queues: HashMap, VecDeque>, - /// Most recent branch merge stm. - last_branch_merge: Option, - /// Most recent break merge stm. - last_break_merge: Option, } impl VersionCorrelator { pub fn new() -> Self { - Self { queues: HashMap::new(), last_branch_merge: None, last_break_merge: None } + Self { queues: HashMap::new() } } /// Record a VIR-level Havoc or Assign for a variable. @@ -137,41 +132,23 @@ impl VersionCorrelator { self.queues.entry(base.clone()).or_default().push_back(stm.clone()); } - /// Record a branch merge point (from `on_branch_merge`). - pub fn record_branch_merge(&mut self, stm: &Stm) { - self.last_branch_merge = Some(stm.clone()); - } - - /// Record a break merge point (from `on_break_merge`). - pub fn record_break_merge(&mut self, stm: &Stm) { - self.last_break_merge = Some(stm.clone()); - } - /// Resolve an AIR versioned constant to its VIR origin. /// Returns the VIR `Stm` that caused this version to exist. - pub fn resolve(&mut self, versioned: &air::ast::Ident, kind: VersionOrigin) -> Option { - match kind { - VersionOrigin::Havoc | VersionOrigin::Assign => { - let base = strip_version_suffix(versioned); - let base_key = Arc::new(base.to_string()); - let queue = self.queues.get_mut(&base_key)?; - debug_assert!( - !queue.is_empty(), - "VIR/AIR ordering invariant violated for {}: \ - no VIR record available (queue empty)", - versioned - ); - queue.pop_front() - } - VersionOrigin::BranchMerge => self.last_branch_merge.clone(), - VersionOrigin::BreakMerge => self.last_break_merge.clone(), - } + pub fn resolve(&mut self, versioned: &air::ast::Ident, _kind: VersionOrigin) -> Option { + let base = strip_version_suffix(versioned); + let base_key = Arc::new(base.to_string()); + let queue = self.queues.get_mut(&base_key)?; + debug_assert!( + !queue.is_empty(), + "VIR/AIR ordering invariant violated for {}: \ + no VIR record available (queue empty)", + versioned + ); + queue.pop_front() } /// Reset between functions. pub fn reset(&mut self) { self.queues.clear(); - self.last_branch_merge = None; - self.last_break_merge = None; } } From f4cd7ac3b83d4af80b18e52b4d4a1d414a1ac389 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sun, 27 Sep 2026 21:27:15 +0000 Subject: [PATCH 6/7] Observers: cut truncated queries at the first failure, cap evaluations, detach from resident contexts - When the --multiple-errors budget runs out, AIR's only_check_earlier disables every label after the first failed one, so the final Valid speaks only for the assertions before it. take_query cut at the last failure, and so reported obligations between two failures as proved though no round proved them. It now cuts at the first failure. - proof-state evaluates at most MAX_EVALUATIONS (4 * MAX_CONJUNCTS) conjuncts in the counterexample, one solver round trip each; the rest are counted in conjuncts_omitted. - A context handed to a resident session no longer carries the observers: its queries would run the callbacks and evaluations with nothing to drain them. Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/observers.rs | 81 +++++++++++++++++-- source/rust_verify/src/resident.rs | 19 ++++- .../tests/obligation_observer.rs | 21 +++++ 3 files changed, 115 insertions(+), 6 deletions(-) diff --git a/source/rust_verify/src/observers.rs b/source/rust_verify/src/observers.rs index 723a3bbc73..c3a0c9a1e8 100644 --- a/source/rust_verify/src/observers.rs +++ b/source/rust_verify/src/observers.rs @@ -58,6 +58,10 @@ pub fn check_names(names: &[String]) -> Result<(), String> { /// A failing assertion's conjuncts are listed up to this many; the rest are /// counted in `conjuncts_omitted`. const MAX_CONJUNCTS: usize = 32; +/// At most this many conjuncts are evaluated in the counterexample (one +/// solver round trip each), so that false ones beyond the first +/// `MAX_CONJUNCTS` can still be listed first; the rest are omitted. +const MAX_EVALUATIONS: usize = 4 * MAX_CONJUNCTS; /// Likewise the variables whose counterexample values are reported. const MAX_VALUES: usize = 64; /// How deeply temporaries and preconditions are expanded into their @@ -232,7 +236,7 @@ impl ObligationObserver { /// only when its id names exactly one undecided assertion; otherwise /// which one failed is unknown, and they stay undecided. /// `truncated` says the verifier stopped checking obligations after the - /// last failure (the `--multiple-errors` budget ran out), so a later + /// first failure (the `--multiple-errors` budget ran out), so a later /// `Valid` does not speak for them. pub fn take_query( &mut self, @@ -249,10 +253,13 @@ impl ObligationObserver { } } if truncated { - if let Some(last) = - pending.assertions.iter().rposition(|a| a.status == Some(Status::Failed)) + // AIR's `only_check_earlier` disables every label after the + // first failed one (in label order), so a later `Valid` speaks + // only for the assertions before it. + if let Some(first) = + pending.assertions.iter().position(|a| a.status == Some(Status::Failed)) { - for a in pending.assertions[last + 1..].iter_mut() { + for a in pending.assertions[first + 1..].iter_mut() { if a.status == Some(Status::Proved) { a.status = Some(Status::Unchecked); } @@ -593,8 +600,11 @@ impl air::query_result_observer::QueryResultObserver for ObligationObserver { let mut parts = Vec::new(); let defs = Definitions { temps: &pending.temps, requires: &self.requires }; conjuncts(&a.expr, &defs, 0, &mut parts); + // each evaluation is a solver round trip; past the cap the + // conjuncts are counted as omitted, not evaluated let mut evaluated: Vec<(String, Option, bool)> = parts .iter() + .take(MAX_EVALUATIONS) .map(|(c, unexpanded)| (term_text(c), eval_bool_expr(c), *unexpanded)) .collect(); // false first: those are why the assertion failed @@ -603,7 +613,7 @@ impl air::query_result_observer::QueryResultObserver for ObligationObserver { None => 1, Some(true) => 2, }); - let conjuncts_omitted = evaluated.len().saturating_sub(MAX_CONJUNCTS); + let conjuncts_omitted = parts.len().saturating_sub(MAX_CONJUNCTS); evaluated.truncate(MAX_CONJUNCTS); // what the conjuncts read, so an expanded temporary shows // the variables of its definition @@ -848,6 +858,51 @@ mod tests { assert!(out[0].1); } + /// A failing assertion with many conjuncts costs at most + /// `MAX_EVALUATIONS` solver round trips; the rest are counted omitted. + #[test] + fn evaluations_are_capped() { + use air::messages::MessageInterface; + let n = MAX_EVALUATIONS + 10; + let expr = Arc::new(ExprX::Multi( + MultiOp::And, + Arc::new((0..n).map(|i| var(&format!("c{i}"))).collect()), + )); + let mut o = ObligationObserver::from_names(&["proof-state".to_string()]).unwrap(); + o.pending = Some(Pending { + assertions: vec![Assertion { + id: None, + message: String::new(), + span: None, + expr, + status: None, + }], + temps: HashMap::new(), + used_axioms: None, + failing: Vec::new(), + }); + let mut calls = 0; + let mut eval = |_: &Expr| { + calls += 1; + Some(false) + }; + let error = air::messages::AirMessageInterface {} + .bare(air::messages::MessageLevel::Error, "assertion failed"); + air::query_result_observer::QueryResultObserver::on_check_valid_result( + &mut o, + &mut CheckValidResult::Invalid { + model_defs: &HashMap::new(), + eval_bool_expr: &mut eval, + assert_id: &None, + error: &error, + }, + ); + assert_eq!(calls, MAX_EVALUATIONS); + let f = &o.pending.as_ref().unwrap().failing[0]; + assert_eq!(f.conjuncts.len(), MAX_CONJUNCTS); + assert_eq!(f.conjuncts_omitted, n - MAX_CONJUNCTS); + } + #[test] fn free_constants_skip_bound_variables() { let binder = @@ -907,6 +962,22 @@ mod tests { // the error budget ran out after #1: a later Valid does not speak for #2 let q = o.take_query(&[], false, true).unwrap(); assert_eq!(statuses(q), vec![Proved, Failed, Unchecked, Unchecked]); + // two failures before the budget ran out: the last round disabled + // everything after the first, #1, so #2 was never proved either + o.pending = Some(Pending { + temps: HashMap::new(), + assertions: vec![ + assertion(0, Some(Status::Proved)), + assertion(1, Some(Status::Failed)), + assertion(2, Some(Status::Proved)), + assertion(3, Some(Status::Failed)), + assertion(4, Some(Status::Proved)), + ], + used_axioms: None, + failing: Vec::new(), + }); + let q = o.take_query(&[], false, true).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Unchecked, Failed, Unchecked]); // #3 failed without an Invalid callback (no model) pending(&mut o); let q = o.take_query(&[id(3)], false, false).unwrap(); diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index 16a0b5379f..111f6b0032 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -532,7 +532,10 @@ pub(crate) struct SolverState { } impl SolverState { - pub(crate) fn new(air: Context, journal: QueryJournal) -> Self { + pub(crate) fn new(mut air: Context, journal: QueryJournal) -> Self { + // `-V observers=` records are drained per query by the verifier's + // own query loop; a session's queries would feed them to no one. + air.set_observers(None, None); Self { air, journal } } } @@ -6512,6 +6515,20 @@ mod tests { assert_eq!(names, COMMANDS.iter().copied().collect::>(), "{error}"); } + /// A context a session keeps runs its queries with no `-V observers=` + /// attached: nothing would drain what they record. + #[test] + fn retained_contexts_carry_no_observers() { + let observer = Arc::new(std::sync::Mutex::new( + crate::observers::ObligationObserver::from_names(&["proof-state".to_string()]).unwrap(), + )); + let mut air = Context::new(Arc::new(VirMessageInterface {}), SmtSolver::Cvc5); + air.set_observers(Some(observer.clone()), Some(observer)); + assert!(air.query_result_observer().is_some()); + let state = SolverState::new(air, QueryJournal::new()); + assert!(state.air.query_result_observer().is_none()); + } + #[test] fn kept_graphs_drop_the_least_recently_used_past_the_budget() { let graph = |n: usize| { diff --git a/source/rust_verify_test/tests/obligation_observer.rs b/source/rust_verify_test/tests/obligation_observer.rs index f601b01694..bc59494f17 100644 --- a/source/rust_verify_test/tests/obligation_observer.rs +++ b/source/rust_verify_test/tests/obligation_observer.rs @@ -140,6 +140,27 @@ fn a_query_that_stops_early_leaves_obligations_unchecked() { ); } +/// When the `--multiple-errors` budget runs out, the last round disables every +/// assertion after the first failure. Whichever failure the solver finds first, +/// `b + 0 == b` between the two is never proved, so it is unchecked. +#[test] +fn a_truncated_query_leaves_obligations_after_the_first_failure_unchecked() { + let code = r#" +verus!{ +fn tricky(a: u32, b: u32) { + assert(b == b); + assert(a != 123456); + assert(b + 0 == b); + assert(a != 0); +} +} +"#; + let functions = functions_for(code, &["-V", "observers=coverage", "--multiple-errors", "2"]); + let st: Vec = + statuses(&functions, "test::tricky").into_iter().map(|(_, status)| status).collect(); + assert_eq!(st, ["proved", "failed", "unchecked", "failed"]); +} + /// The counterexample is read while it is live: the false conjunct, in /// source spelling, and the value the loop counter has there. #[test] From bbf0e57ccaab1d776f885bb365dc3fe35969a0b6 Mon Sep 17 00:00:00 2001 From: Kiran Gopinathan Date: Sun, 27 Sep 2026 21:33:46 +0000 Subject: [PATCH 7/7] Observers: render quantifiers without SMT attributes, place unmatched failures only when unambiguous, document conditional proved Co-Authored-By: Claude Opus 5.5 --- source/rust_verify/src/observers.rs | 108 +++++++++++++++++++++++++++- 1 file changed, 106 insertions(+), 2 deletions(-) diff --git a/source/rust_verify/src/observers.rs b/source/rust_verify/src/observers.rs index c3a0c9a1e8..b010775ba3 100644 --- a/source/rust_verify/src/observers.rs +++ b/source/rust_verify/src/observers.rs @@ -5,7 +5,10 @@ //! - `coverage`: for every query, each obligation it asserted (an `assert`, //! a postcondition, a loop invariant, a precondition of a call...) and what //! became of it: `proved`, `failed`, `unknown` (the solver gave up on the -//! query) or `unchecked` (the query stopped before reaching it). With +//! query) or `unchecked` (the query stopped before reaching it). As in +//! Verus's own checking, an obligation after a failed one is proved +//! assuming the failed one held: after a failing `assert(x > 5 && x < 3)`, +//! `assert(x == 2)` is `proved`. With //! `-V axiom-usage-info` a proved query also names the axioms in its unsat //! core. This is the obligation-level counterpart of `verus-reach`, which //! says which functions are used; this says which of a function's @@ -71,6 +74,8 @@ const MAX_TEMP_DEPTH: usize = 8; #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] #[serde(rename_all = "snake_case")] pub enum Status { + /// Proved assuming every earlier obligation of the query held, failed + /// ones included. Proved, Failed, /// The solver gave up (resource limit or cancellation) before deciding it. @@ -515,7 +520,32 @@ fn is_encoding_sort(typ: &air::ast::Typ) -> bool { if [TYPE, DECORATION, FUEL_TYPE, FUEL_ID].contains(&n.as_str())) } +/// `expr` without its binders' triggers and qids: the printer spells them +/// as SMT's `(! body :pattern ...)`, which reads as a negation once +/// rendered as source. +fn strip_attributes(expr: &Expr) -> Expr { + air::visitor::map_expr_visitor(expr, &mut |e| match &**e { + ExprX::Bind(bind, body) => { + let bare = match &**bind { + BindX::Quant(q, bs, trigs, qid) if !trigs.is_empty() || qid.is_some() => { + BindX::Quant(*q, bs.clone(), Arc::new(vec![]), None) + } + BindX::Lambda(bs, trigs, qid) if !trigs.is_empty() || qid.is_some() => { + BindX::Lambda(bs.clone(), Arc::new(vec![]), None) + } + BindX::Choose(bs, trigs, qid, cond) if !trigs.is_empty() || qid.is_some() => { + BindX::Choose(bs.clone(), Arc::new(vec![]), None, cond.clone()) + } + _ => return e.clone(), + }; + Arc::new(ExprX::Bind(Arc::new(bare), body.clone())) + } + _ => e.clone(), + }) +} + fn term_text(expr: &Expr) -> String { + let expr = &strip_attributes(expr); let printer = air::printer::Printer::new( Arc::new(air::messages::AirMessageInterface {}), true, @@ -583,12 +613,23 @@ impl air::query_result_observer::QueryResultObserver for ObligationObserver { // postconditions share one), so the error's primary span // decides between assertions with the same id. let (_, error_span) = describe(error); + // Without a span match, the failure is placed only when its + // id picks out exactly one undecided assertion, as in + // `take_query`. let undecided = |a: &Assertion| a.status.is_none() && &a.id == *assert_id; + let sole_undecided = || { + let mut candidates = + pending.assertions.iter().enumerate().filter(|(_, a)| undecided(a)); + match (candidates.next(), candidates.next()) { + (Some((i, _)), None) => Some(i), + _ => None, + } + }; let Some(index) = pending .assertions .iter() .position(|a| undecided(a) && error_span.is_some() && a.span == error_span) - .or_else(|| pending.assertions.iter().position(undecided)) + .or_else(sole_undecided) else { return; }; @@ -903,6 +944,69 @@ mod tests { assert_eq!(f.conjuncts_omitted, n - MAX_CONJUNCTS); } + /// A quantifier's triggers and qid are left out of its source text: + /// SMT's `(! body :pattern ...)` would render as a negation. + #[test] + fn quantifier_attributes_are_not_rendered() { + let binder = + Arc::new(air::ast::BinderX { name: Arc::new("i".to_string()), a: Arc::new(TypX::Int) }); + let body = Arc::new(ExprX::Binary(BinaryOp::Le, var("i"), var("n@1"))); + let bind = Arc::new(BindX::Quant( + air::ast::Quant::Forall, + Arc::new(vec![binder]), + Arc::new(vec![Arc::new(vec![var("i")])]), + Some(Arc::new("user_q_1".to_string())), + )); + let text = term_text(&Arc::new(ExprX::Bind(bind, body))); + assert!(!text.contains('!') && !text.contains(":pattern"), "{text}"); + assert!(!text.contains(":qid"), "{text}"); + let names = vir::air_names::SourceNames::new(); + assert!(!render_unversioned(&names, &text).contains('!')); + } + + /// A failure whose span matches no assertion is placed only when its + /// id picks out exactly one undecided assertion. + #[test] + fn an_unmatched_failure_is_placed_only_when_unambiguous() { + use air::messages::MessageInterface; + let invariant = || Assertion { + id: None, + message: String::new(), + span: Some("elsewhere".to_string()), + expr: var("x"), + status: None, + }; + let mut o = ObligationObserver::from_names(&["coverage".to_string()]).unwrap(); + let fail = |o: &mut ObligationObserver| { + let error = air::messages::AirMessageInterface {} + .bare(air::messages::MessageLevel::Error, "invariant not satisfied"); + air::query_result_observer::QueryResultObserver::on_check_valid_result( + o, + &mut CheckValidResult::Invalid { + model_defs: &HashMap::new(), + eval_bool_expr: &mut |_: &Expr| None, + assert_id: &None, + error: &error, + }, + ); + }; + let pending = |assertions| Pending { + assertions, + temps: HashMap::new(), + used_axioms: None, + failing: Vec::new(), + }; + o.pending = Some(pending(vec![invariant(), invariant()])); + fail(&mut o); + let statuses = |o: &ObligationObserver| { + o.pending.as_ref().unwrap().assertions.iter().map(|a| a.status).collect::>() + }; + assert_eq!(statuses(&o), vec![None, None]); + o.pending = Some(pending(vec![invariant()])); + fail(&mut o); + assert_eq!(statuses(&o), vec![Some(Status::Failed)]); + } + #[test] fn free_constants_skip_bound_variables() { let binder =