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

[kiranandcode]

Summary

Brings upstream's verification-observer interface (verus-lang#2965, still open upstream) into the fork, and builds two observers on it.

1. The observer interface (cherry-pick of 9bccfb4, author kept). VirObserver, AirObserver and QueryResultObserver are callbacks fired during VIR→AIR lowering, AIR lowering and after each query. A consumer selects one with -V observers=<name>. The conflicts with the fork are in var_to_const, smt_verify, context.rs, config.rs, verifier.rs and the test harness. Both sides were kept in each; the commit message lists how. Two changes to the PR's API:

• The handles are Arc<Mutex<dyn Trait>> and the traits require Send, instead of Rc<RefCell<..>>. Resident sessions keep air::Context in a Mutex served from other threads, so an Rc in Context does not compile here.
• VersionOrigin::{BranchMerge, BreakMerge} and VirObserver::on_break_merge are removed. They never fired. A merge takes the highest version a branch reached, and that branch already created it, so a merge makes no new version. on_break_merge had no caller.

2. A fix to the PR for cvc5. The Invalid callback's eval_bool_expr sends z3's (eval ...). cvc5 does not accept that, and the run dies with "Z3 reader thread failure". Under cvc5 it now asks (get-value (e)). eval_expr itself is unchanged; only the evaluator treats a multi-line answer as "not a boolean". Upstream's tests run z3 in internal test mode, so they never hit this. The PR's own test observer crashes on any failing query in the fork without this fix.

3. One version hook. The fork's own version recording in var_to_const (read by provenance, e-graph readings and speculation) now goes through the PR's notify_version_created, rather than a second path beside it. Behaviour is unchanged. Other fork lowering hooks were not ported: the goal scopes, and source names recorded at encode time. They feed the fork's own solver-side tools, and routing them through an external observer would add a layer without removing any fork code.

4. -V observers=coverage and -V observers=proof-state. One object, rust_verify/src/observers.rs, serves both names; they can be given together. Any other name, except the test suites' own observers used alone, is an argument error. The verifier takes each query's records out after the query and files them under the function, as it does for the other per-query solver reports. They are published in func-details, and so in --output-json and --report-json:

• obligations (coverage): per query, every obligation Verus asserted, with its message, span and one of four statuses:

  • proved
  • failed
  • unknown: the solver gave up on the query
  • unchecked: the query stopped first, e.g. --multiple-errors 0 or the error budget ran out

  With -V axiom-usage-info, a proved query also lists its unsat-core axioms. This needed a fix to the fork: cvc5 prints the unsat core one name per line, and the one-line parser aborted the run under -V axiom-usage-info with or without an observer. This is coverage at the obligation level, the counterpart to verus-reach (Static reachability of verified code (verus --reach, tools/verus-reach) #12/verus-reach: static reachability coverage of verified code (HTML report, explicit roots, --connected, thresholds) #39), which covers which functions are used.

• failing_asserts (proof-state): at each failing obligation, while cvc5's counterexample is live:

  • which conjuncts of the failing assertion are false, in source spelling
  • the counterexample's value for each variable those conjuncts read (the encoding's type ids and decorations are left out)

  For example, (i < 40) is false with i = 40. The split looks through two things:

  • assert(a && b) asserts a Verus temporary (tmp%1), which is read as its definition.
  • A failing call's precondition req%f(args) is read as f's requires at the call's arguments, taken from the req% axiom.

  A temporary or precondition whose definition is not available stays whole and is marked unexpanded.

Loop invariants and bit-vector asserts have no assert id, and a function's postconditions share one. So a failure is placed by its error's span, not on the first assertion with a matching id. A failure without a model has no span; the verifier passes its id, which may be none (a bit-vector assert). It is placed only when that id picks out exactly one undecided assertion.

Companion MCP PR: BasisResearch/verus-tools-mcp#60 (obligation_coverage, failing_assert_state).

Test plan

• vargo build --release
• vargo test --release -p rust_verify_test --test observer: the PR's 29 tests
• CI: full rust_verify_test suite
• vargo test --release -p rust_verify_test --test obligation_observer: 10 new tests, run under cvc5
  • statuses, an id-less invariant failure, --multiple-errors 0, false conjunct and values
  • assert(a && b) split, callee precondition split, no encoding constants among values
  • a failing bit-vector assert is failed
  • used_axioms under cvc5
  • unknown observer names rejected
• cargo test --release -p rust_verify --lib observers (8), cargo test --release -p air --lib (218, including the multi-line unsat core parser and "merges announce no versions")
• report_json (11), difficulty (3), resident (64) suites
• cargo fmt -- --check, cargo clippy --all-targets -- -D warnings in source/ (as CI runs it)

🤖 Generated with Claude Code