Merge the verification observer (verus#2965), and add coverage and proof-state observers

source/air/src/air_observer.rs

@@ -0,0 +1,59 @@
+//! 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,
+}
+
+/// 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.
+    ///
+    /// 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.
+    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<Mutex<..>>` rather than
+/// `Rc<RefCell<..>>` 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<std::sync::Mutex<dyn AirObserver>>;

source/air/src/ast.rs

@@ -9,8 +9,8 @@ pub type TypeError = String;
 
 pub type Ident = Arc<String>;
 
-pub(crate) type Snapshot = IndexMap<Ident, u32>;
-pub(crate) type Snapshots = HashMap<Ident, Snapshot>;
+pub type Snapshot = IndexMap<Ident, u32>;
+pub type Snapshots = HashMap<Ident, Snapshot>;
 
 pub type Typ = Arc<TypX>;
 pub type Typs = Arc<Vec<Typ>>;

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<Fact>), 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();

source/air/src/block_to_assert.rs

@@ -77,7 +77,12 @@ fn stmt_to_expr(label_n: &mut u64, locals: &mut Vec<Decl>, 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 {

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<Ident> = binders.iter().map(|b| b.name.clone()).collect();
+                obs.lock().unwrap().on_lambda_decl(&closure_fun, &params, &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()));

source/air/src/context.rs

@@ -541,6 +541,9 @@ pub struct Context {
     name_counters: Vec<NameCounters>,
     pub(crate) typing: Typing,
     pub(crate) debug: bool,
+    pub(crate) air_observer: Option<crate::air_observer::AirObserverHandle>,
+    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 +690,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 +811,24 @@ 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<crate::air_observer::AirObserverHandle>,
+        query_result_observer: Option<crate::query_result_observer::QueryResultObserverHandle>,
+    ) {
+        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<dyn std::io::Write + Send>) {
         self.air_initial_log.set_log(Some(writer));
     }
@@ -1555,11 +1578,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);
@@ -1630,6 +1664,40 @@ impl Context {
         smt_output[0].clone()
     }
 
+    /// 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<bool> {
+        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 => {
+                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();
+                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,
+                }
+            }
+        }
+    }
+
     pub fn command(
         &mut self,
         message_interface: &dyn crate::messages::MessageInterface,

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]) }));
+        }
+    }
 }

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;
@@ -29,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;

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<Ident, ModelDef>,
+        /// 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<bool>,
+        assert_id: &'a Option<crate::ast::AssertId>,
+        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<crate::ast::AssertId>],
+        /// 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<crate::ast::AssertId>,
+    },
+}
+
+/// 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<Mutex<..>>` for the reason
+/// given at `AirObserverHandle`.
+pub type QueryResultObserverHandle = std::sync::Arc<std::sync::Mutex<dyn QueryResultObserver>>;