Resident: query fingerprints, retain-only sessions and a pin request

[kiranandcode]

What a caller needs to keep a resident session across a source edit without reopening it (verus-tools-mcp refresh_session, BasisResearch/verus-tools-mcp#49):

• Fingerprints. Every catalogue query carries fingerprint: {prefix, body}: FNV-1a over its AIR as the printer writes it, the declaration prefix asserted below the query (the prelude, the bucket's base context plus the journal scopes up to the query's own, hashed incrementally per solver) and the query body apart; the body hash also covers the query's rlimit, which is set outside the AIR. The prelude is hashed because it is not fixed text: it reads the crate's word size, which a global size_of usize line sets, possibly in another module whose size_of lemma the bucket prunes, so a query's AIR and bucket context can stay the same while its verdict changes. A by(bit_vector) query's solver gets neither the prelude nor the bucket context, so its prefix covers neither, and declarations added to its bucket leave it alone. The printer writes assertion labels as their notes and never a span, so a query that only moved to other lines fingerprints the same; generated local names carry per-function counters, not line numbers. A user quantifier's :qid/:skolemid is hashed without the counter it ends in (forget_quantifier_counters): that counter is the bucket's Ctx's, not the function's, so without this every quantifier lowered after an extra recommends follow-up (which a retain-only session lowers and a checked one skips), after a quantifier added to an earlier function, or after an earlier check flipping between pass and fail, fingerprinted differently on queries the edit left alone. Two queries with equal fingerprints are therefore the same up to their quantifiers' names, so what a caller carries over by fingerprint must not name a quantifier by :qid (a pin does not). A quantifier's :pattern groups are hashed sorted and once each (sort_patterns): automatic trigger selection lists them in an order that varies between compilations and sometimes lists one twice (page-table's protect_aux fingerprinted differently on runs of unchanged source before this). Together with the existing identity (function, kind, description, repeat), this is what a caller compares across compilations.
• Retain-only sessions. Under VERUS_RESIDENT_RETAIN_ONLY the invocation retains every selected query and checks none of them (run_commands_queries returns early), reported as ready.retain_only. This is the front-end pass a caller opens on the edited source, after which it checks only the queries whose fingerprints changed. With no answers to decide which recommends follow-ups to retain, it retains every one a check could have added (retain_unchecked_recommends): the follow-up of every body or termination op that has something to check, and for check_recommends functions the checked kind too, for the functions the --verify-* filter selects (for the rest nothing is retained, so nothing is generated). Its catalogue is then a superset of any checked session's on the same source, with the same fingerprints, so a follow-up retained because a check failed before the edit is still there to compare. A caller should check a follow-up only when its function's body fails, as the batch run does. --expand-errors queries are the one exception: they focus on the assertion a failed check named, so a retain-only session has none.
• pin request ({bucket, query, rung, alongside, rlimit} → pinned): gives a query the rung its checks try first, as a ladder request does, so a caller can carry a pin over to the new worker. Refused, as a ladder refuses or skips, on a cvc5 without :quant-strategy (whose pinned check would end the session), for a rung the solver has no module for, and for a budget below one cvc5 resource unit (which would reach cvc5 as no limit).

Why not a refresh request served in-process: that was implemented first (a second driver::run from the serving process with the invocation's own arguments). It cannot work on this toolchain: rustc_mir_build's VERUS_AWARE_DEF_IDS / VERUS_ERASURE_CTXT (source/rustc_mir_build_additional_files/verus.rs, compiled into the patched rustc) are set once per process and panic on a second set (VERUS_AWARE_DEF_IDS has already been set). So the second front-end pass runs in a new worker process, and the diff lives in the caller; Verus provides what the diff needs.

Tests: resident::tests::fingerprints_ignore_spans_and_tell_the_prefix_from_the_body (same AIR at other spans → same fingerprint; a declaration added below the query → prefix differs, body does not; the query edited → body differs, prefix does not; triggers reordered or repeated → same body, one dropped → different; a user :qid/:skolemid with another counter → same body, another function's → different); plus the same query at another rlimit → body differs; a journal on another prelude → prefix differs, body does not; commands_names_every_request and resident_ready_lists_the_requests_it_serves cover pin. Integration tests: resident_fingerprints_cover_the_word_size_in_the_prelude (a global size_of usize == 8 in another module flips a query from invalid to valid; before the prelude was hashed its fingerprint was identical, prefix and body), resident_bit_vector_fingerprints_ignore_the_bucket_context (a spec fn and a struct added to the bucket change a default query's prefix but not a bit-vector query's; before, the bit-vector prefix changed too), resident_pin_is_refused_where_checks_could_not_follow_it (unavailable rungs, out-of-range and sub-unit budgets refused, the session still checks, a valid pin is followed), resident_retain_only_session_pins_and_ladders_before_any_check (a pin and a ladder on solvers that have checked nothing see all five rungs), resident_retain_only_session_pins_and_ladders_bit_vector_queries (the same for by(bit_vector) queries, whose solvers get no prelude, context or scope, so probe_strategy_rung pushes and pops an empty scope before asking; fails without that), resident_retain_only_session_retains_what_any_checked_session_could (every query of a checked session is in the retain-only catalogue with the same fingerprint; the extras are exactly the follow-ups of checks that passed; the source has quantifiers in those functions and in a function lowered after them, so the retain-only session numbers that function's quantifier differently, and the test fails without forget_quantifier_counters). On this Mac: cargo test -p rust_verify --lib resident 33 passed, vargo test --release -p rust_verify_test --test resident 58 passed (both new tests fail on the commit before the prelude/bit-vector fix); on the code before the review fixes, the pin and catalogue tests fail and the ready-list test failed; with only the forget_quantifier_counters call removed, the fingerprint unit test and the catalogue test fail (the catalogue test on later's body fingerprint). rustfmt --check and cargo clippy -p air -p rust_verify --all-targets -- -D warnings clean.

Measured before the retain-only session retained follow-ups for passing checks and before quantifier names were hashed without their counter, so its catalogue and front-end time are now somewhat larger (through the resident protocol directly, this Mac, -V cvc5 --rlimit 10, verified-nrkernel page-table, one-line edit in the body of lemma_new_entry_mb0_bits_are_zero):

• --verify-module impl_u::l2_impl (7 buckets, 134 queries): a full open (front-end + every check) 131.7 s wall; a retain-only run on the edited source 4.5–6.0 s, classified 133 unchanged / 1 changed (body); the changed query then checked in 4.9–8.7 s. Three retain-only runs of unchanged source agree on all 134.
• --verify-only-module impl_u::l2_impl --verify-function lemma_new_entry_mb0_bits_are_zero (16 queries): 11.5 s vs 4.7 s, 15 unchanged / 1 changed.
• Small 4-query fixture: 0.6 s vs 0.2 s, 3 unchanged / 1 changed.

🤖 Generated with Claude Code

[kiranandcode]

Review follow-up (pushed as dd3227a + c11737d):

Fixed: a pin or ladder on a by(bit_vector) query in a retain-only session saw no rungs. A bit-vector solver gets no prelude, no bucket context and no journal scope, so before its first check it has been sent neither an assertion nor a push, and cvc5 reports :strategy-rung's available empty. Reproduced on eef685a: in a retain-only session, pin on such a query was refused with "the solver has no module for this rung", and ladder marked all five rungs unavailable with available: []. The same requests in a checked session work, since the startup check already initialized the solver. probe_strategy_rung now pushes and pops an empty scope before the get-info. New test resident_retain_only_session_pins_and_ladders_bit_vector_queries fails on eef685a and passes with the fix. Resident suite 58/58, air 216/216, rust_verify --lib resident 33/33, clippy -D warnings and rustfmt clean.

Not a bug: the fingerprint leaves out the prover. Adding #[verifier::nonlinear] to a function gives the same fingerprint (prefix and body) and the same verdict, retain-only or checked. The only solver-side difference between Nonlinear and the default prover is Z3's smt.arith.solver=6, and user crates always run cvc5 here (config.rs: Z3 only for vstd and internal test mode), where apply_per_query_smt_options sets nothing for Nonlinear. Left unchanged. If cvc5 ever gets nonlinear-specific options, query.prover should go into the body hash.

🤖 Generated with Claude Code