Add resident speculate: test an instantiation hypothesis on a retained query

[kiranandcode]

Implements the Verus side of plans/speculative_probe.md. It uses BasisResearch/cvc5#14, (speculate ...) and (get-info :speculation). cvc5#14 is merged, and the cvc5 pin here is basis-e68dc63e37, cvc5 main at that merge.

What a speculate request does

{"command":"speculate","session":"...","bucket":0,"query":3,
 "hypothesis":{"instantiation":{"qid":"user_crate__f_3","subst":{"i":"a"}}}}

hypothesis is one of the following. Without one, the reply lists the quantifiers written in source that the query's scope asserts (qid, variables with source and SMT names and sorts, triggers), the first 40; notes says when the scope asserts more.

• instantiation {qid, subst}: instantiate once at the given terms.
• trigger_pattern {qid, pattern}: add one more trigger; pattern is one term or a list.
• block_cycle {qid, fingerprint}: refuse the instantiations that fit a shape.

A term is a Verus expression (s.len() - 1, f(y)) or an SMT term in the solver's spelling ((I y@1), (Add a! 1)). It is read at the goal the query fails at, so a mutable local means its value there.

The worker checks the query as usual (before), then with the hypothesis sent in the query's own scope (after). If after is valid, it checks again without the hypothesis (recheck). Queries near the resource limit flip between two checks of their own; the egraph work saw this. So a close counts only if the recheck still fails.

The reply carries:

• closed;
• introduced_loop and new_loops: a quantifier whose deepest instantiating term got deeper in at least loop_threshold rounds after the hypothesis, where it did not without it;
• new_provenance.closing_instantiations: the instances it made, tagged LLM_DIRECTED;
• the refused count and examples for a block;
• verus_snippet after a close: an assert of the instance for an instantiation, or #![trigger ...] for a trigger, which also gets fallback_snippet, an assert of one instance it made;
• readings: how names in Verus terms were read, where more than one reading was possible.

A hypothesis that cannot be applied comes back with a status and a reason (no_quantifier, mismatch, could_not_lower, unusable, rejected). The session goes on serving.

Design

• air::speculate. It holds the request, the reply parser, and a finder that locates a quantifier by qid in the retained AIR (prefix declarations and the query) in the solver's spelling. It also substitutes binders for rendering.
• What reaches cvc5 unquoted. The (speculate ...) command's outer syntax is fixed by the worker: the qid and variable names come from the AIR quantifier the worker found (so a qid the caller made up is answered no_quantifier and never sent), and every caller-written term, pattern and fingerprint goes as a string literal that cvc5 parses on its own and can refuse without ending the session.
• When the command is sent. Context::set_speculation sends (speculate ...) just before the early flush (get-info :version), after the query's assertions, with an echoed marker in front of it. A term cvc5 cannot read therefore comes back as an (error ...) line after the marker; an error before it is the query's own and stays unexpected output. The check then returns Canceled without a check-sat, and the reply carries the error. (get-info :speculation) is read in the same batch as the check-sat. supports_speculation asks (get-info :speculation) once, because a cvc5 without the command would end at it.
• Lowering. The plan asked to lower Verus surface terms through sst_to_air. There is no VIR at resident time, so the worker reads the text itself. It checks the request's variable names first, then runs before, and reads the terms at the goal before failed at (the query's last goal when it names none).
  • A Verus term goes through the scaffold lowerer from Resident scaffold requests: try one intermediate assertion at one goal #37 (scaffold::lower_term). It reads calls, method calls, fields, indexing, @, old, casts and the operators, and boxes as the encoders do. air::GoalScope then reads the result as the lowered query does at the goal, so a mutable local is its SSA version there.
  • An SMT term is one the scope or the solver declares, one no Rust name could be ($, a!), or an application headed by an SMT operator or a declared function. It is resolved symbol by symbol. A variable's AIR name reads as its version at the goal, every version is declared, and the prelude's functions come from the AIR context.
  • An instantiation's terms stand outside the quantifier, so they never see its variables: a parameter it shadows is the parameter. A trigger's terms are over its variables, which shadow locals of the same name.
  • A fingerprint keeps the small surface syntax, since its holes are no Verus.
  • A name that could mean several declarations is refused.
• Eliminated variables. cvc5 eliminates a variable that an equality in the formula's body fixes (x == y ==> ...), and the formula it holds then binds only the rest. It answers an instantiation naming the eliminated one with mismatch. The worker sends the instance again without each such variable, lists them in eliminated, and offers as the snippet the instance cvc5 made (its :bodies), since the requested term need not be the one the equality fixes. A trigger's fallback is built only when its terms line up with the quantifier's variables.
• no_quantifier from cvc5. cvc5 registers alpha-equivalent formulas once, under the first qid, so a hypothesis on the second qid finds nothing there even though the scope asserts it. notes says so.
• Journal base. The journal keeps the bucket's setup batches (fuel, traits, datatypes, function declarations), which the solver holds below its scopes. They are only read, never replayed. Add the resident twin request: a query and one edit of it, compared #34's twin added the same base and record_base; this PR now uses those.
• Snippets. Snippets are built from the AIR quantifier, not from cvc5's rewritten instance. For an instantiation, the snippet is the body at the terms with its has_type guards dropped. Where that does not read as source, it is an assert that mentions the trigger's instance instead. QueryNames::pasteable, factored out of the egraph verus_assert, applies the same rules: every symbol must read as source, no variable may appear at two versions, and none at another version than the one where the snippet goes. The egraph's verus_assert gets the last rule too.
• Not in this PR. Which of a trigger's instances a proof used needs full proofs; the reply lists all of them.

Testing

Run on arm64 macOS against the pinned cvc5 (basis-e68dc63e37), with the solver version check on. The two speculate tests run with the rest of the resident suite.

• resident_speculate_probes_and_leaves_the_session_unchanged covers:
  • Instantiation: closes with assert(((crate::g(a) > 0) && (crate::f(a) > 0))); (recheck still invalid). A fresh worker with that assert pasted verifies.
  • Trigger: f(i) closes with #![trigger crate::f(i)]; pasted into the quantifier, it verifies.
  • Block: for the loop h(x) > h(s(x)), before is resource_limit with the quantifier rising past the threshold. With block_cycle h(s(s(_))), after has no loop and instances were refused.
  • Introduced loop: a quantifier triggered on g never fires. Given the trigger h(x), it climbs, and introduced_loop is true.
  • Refusals: no_quantifier with candidates, mismatch, could_not_lower, and an out-of-range loop_threshold. A last check answers exactly as the first did, one solver process served everything, and pushes and pops balance.
• resident_speculate_reads_terms_at_the_goal covers:
  • Shadowing: in proof fn shadowed(i: int) requires forall|i: int| ..., {"i": "i"} is the parameter and closes the goal.
  • Mutable local: after let mut y = a; y = y + 1;, {"i": "y"} closes, and its snippet, pasted before the goal, verifies in a fresh worker.
  • SMT spelling: (Add a! 1) is boxed and closes the same goal.
  • Stale versions: the trigger f(i) matches cvc5's term over y's first version, so an assert of it is offered only when it names no stale version, and one offered verifies pasted.
  • Method calls: {"i": "s.len() - 1"} closes assert(s[s.len() - 1] > 0).
  • A generic quantifier with an equality guard (forall|x: A, y: A| x == y ==> p(x)) closes at {x: a, y: a}. cvc5 keeps both of its variables, since the equality is between boxed values under type guards. The retry for an eliminated variable is therefore covered by the unit test an_eliminated_variable_is_read_from_the_refusal, and the elimination itself by cvc5#14's speculate-varelim regression; no Verus fixture reaches it yet.
• resident suite against the pinned cvc5: 52 passed, none ignored, the two speculate tests included.
• air unit tests: 216 passed, including request printing, the reply parser, binder substitution, and goal scopes. The rust_verify lib tests: 48 passed, including sort-directed boxing, ground terms and versions at the goal, SMT-or-Verus reading, stale-version snippets, and type-guard dropping. fmt and clippy are clean.

toyDB acceptance: not met

These runs predate the review fixes: they were measured at d2dcec3 with cvc5#14 at 4cf5707, through the MCP server (speculative_probe) against toyDB d79db20. Every term was given in the solver's spelling, which reads the same after the fixes.

Targeted hints. Five toyDB functions each had one hint removed. Each hint is an instance of the function's own quantified requires, and each was probed with that instance:

function	removed hint	check without it	directed instance
keycode::lemma_lex_lt_at	assert(a[0] == b[0]);	valid	j := 0, applied, valid
keycode::lemma_allff	assert(p[0] == 255);	valid	j := 0, applied, valid
keycode::lemma_prefix_end_fwd	assert(e[j] == p[j]);	valid	(listing only)
verified_lexer::lemma_scan_digits_end_run	assert(is_digit(input[pos]));	valid	i := pos, applied, valid
verified_lexer::lemma_scan_ident_end_run	assert(is_ident_cont(input[pos]));	valid	i := pos, applied, valid

Sweep. Every single-line assert in eight keycode and lexer proof functions was removed one at a time, 53 variants in all. Only one broke its proof. lemma_allff without assert(k.subrange(0, p.len() as int) =~= p); fails its postcondition. Probing it with vstd's lemma_seq_ext_equal at A&. := $, A& := (UINT 8), s1 := k.subrange(0, p.len()), s2 := p applied the instance, but the query stayed invalid. The type binders and boxed terms were given in the solver's spelling. The removed assert is a proof subgoal: Verus proves the pointwise equality behind =~= itself. A single axiom instance cannot stand in for that.

So toyDB's hints of this kind are redundant under cvc5, and the one necessary one is not an instantiation. The plan's criterion (at least three toyDB unknowns flipped by a pasted snippet) is not met, and this PR does not claim it. What these runs do show:

• the listing works on real toyDB queries (each hit the 40-candidate cap);
• directed instances are lowered, boxed and applied there, vstd axioms with type binders included;
• the session is unchanged afterwards (every recheck matched).

The flips themselves are shown on the fixtures in the resident tests.

Review changes

First round:

• serve_speculate: the candidate listing is capped at MAX_CANDIDATES (40) but said nothing about it, so a scope with more looked fully listed; notes now says "the first 40 of the N quantifiers" when it is cut. The toyDB numbers above are restated accordingly.
• Re-tested against cvc5#14 at its review commit, which filters and blocks a speculative trigger's matches like any trigger's; the fixture expectations hold unchanged.
• Left alone after review: the fork isolation (one (speculate ...) per query scope, popped by finish_query, with cvc5 holding all of it in that user context); and the Canceled path for a refused command, which pops like any canceled check.

Second round (see the review comment):

• An instantiation's terms resolved names through the quantifier's own variables, so a parameter it shadows lowered to the bound variable and came back could_not_lower. They are now read outside the quantifier.
• A mutable local lowered to its unversioned AIR Var, which cvc5 does not declare. Terms are now read at the goal the query fails at, where the local is one SSA version.
• A snippet could name a variable at a stale version: a trigger's fallback asserted g((y + 1)) over y's first version, which pasted before the goal reads as a + 2. pasteable now requires the version where the snippet goes, for the egraph's verus_assert too.
• The lowering knew only four of the prelude's boxes, seeded by hand, so (Add a! 1) was never boxed. It now asks the AIR context.
• An (error line anywhere in the early flush counted as the hypothesis's refusal; an echoed marker now separates the query's output from the command's.
• rejected's documentation names all three reasons cvc5 gives.
• Verus terms go through the scaffold lowerer, so method calls, indexing, casts and @ are read.
• A directed instance over a constant cvc5 had substituted away (y@1 = Add(y@0, 1)) was applied but never connected. That was cvc5's, and cvc5#14 fixes it at 47d666d.

Third round (after cvc5#14 moved to da4b2b0073):

• cvc5 now keeps a formula's :qid through variable elimination, and answers an instantiation naming the eliminated variable with mismatch. The worker retries without it, as above, so such a formula can be instantiated at all; da4b2b0073 is now the minimum.
• rejected has a fourth reason, "the instance simplifies to true", and the docs in resident.rs and air::speculate list it.
• pending now means that no round reached e-matching (for instance because conflict-based instantiation closed every check first), in both docs.
• A no_quantifier answer for a formula the scope asserts explains alpha-equivalence in notes.
• cvc5#14 merged. The pin moves to basis-e68dc63e37, cvc5 main at that merge, and the two speculate tests are no longer ignored. The one cvc5 change after da4b2b0073 reads an integer term given for a real variable as a real, which Verus's encoding never sends.

Overlap

main at da8fa53 (#33's ablate, #34's twin, #35's ladder, #41's scaffold placement, and the cvc5 pin at the pending-lemmas release) is merged in. Its conflicts were side-by-side additions in context.rs, lib.rs, smt_verify.rs, resident.rs and the resident tests, kept both; the journal's base and verifier.rs follow main's. COMMANDS is list, check, bisect, ablate, egraph, scaffold, close, inst_graph, ladder, twin, speculate. The cvc5 pin is basis-e68dc63e37, cvc5 main at #14's merge, which also carries #11's :branch-profile.

🤖 Generated with Claude Code

[kiranandcode]

BasisResearch/cvc5#14 changed after a review, and this branch is now merged with main. Notes on what that means here.

cvc5#14 changes that reach this PR

cvc5#14 is at ce29c5f858 (fixes in f7ccd693eb, then main merged in). Three were bugs; the rest are report details.

• A directed term now goes through cvc5's top-level substitutions before it is rewritten. Before, a term preprocessing had eliminated (a variable fixed by an equality such as (= a b), or a define-fun application) produced an instance about an unconstrained symbol: applied, and no effect. AIR asserts many equalities of that shape, so this is the case the resident lowering hits. The visible change here is that new_provenance.closing_instantiations (built from cvc5's :instances) shows the term after substitution, b where the caller wrote a. verus_snippet is built from the caller's subst, so it is unchanged.
• A check in which a block refused an instance answers unknown (new IncompleteId::QUANTIFIERS_SPECULATIVE_BLOCK), not sat: --finite-model-find answered sat on an unsat query. result_name maps both to invalid, so nothing here changes.
• Rounds whose lemmas come from a hypothesis count toward --inst-max-rounds. A speculative trigger that fed itself ignored the limit and ran until a resource limit. Verus passes --inst-max-rounds only under matching-loop mode, so this matters only for a probe run in that mode.
• Report details, none of which this PR's parser depends on: a leaf constant such as (- 1) or (/ 1 2) matches a fingerprint spelled the way the printer spells it; :quantifiers counts distinct formulas and :bodies/:materialized list each once after a nested pop; (get-info :speculation) before any check says :loop-threshold 5, not 0 (supports_speculation only checks the prefix).

Merge with main

Merged origin/main (#37 resident scaffold, the cvc5 pin moves to basis-b905873c8d) into kg/speculative-probe. The conflicts were in smt_verify.rs, resident.rs and tests/resident.rs. Nearly all were both sides adding next to each other (the speculation and check-effort get-infos and their reply handling, the speculate and scaffold requests, their fixtures and tests), and kept both. The two that edited one line are COMMANDS and the list resident_ready_lists_the_requests_it_serves checks: both are now list, check, bisect, egraph, scaffold, close, inst_graph, speculate.

Tests

On macOS arm64, from a clean build of the merge (60cfcc6ce):

• against the pinned basis-b905873c8d release: the resident suite 38 passed (1 ignored: the speculate test), air 201 passed, rust_verify lib 36 passed; cargo fmt --check and clippy --all-targets -D warnings clean.
• against a build of cvc5#14 at ce29c5f858 (RESIDENT_NO_SOLVER_VERSION_CHECK=1, vargo --no-solver-version-check): resident_speculate_probes_and_leaves_the_session_unchanged passes with its expectations unchanged. The fixtures use no eliminated variables, no blocks under model finding, and no --inst-max-rounds, so the fixes do not reach them.

Still open

The pin: main now pins basis-b905873c8d, which does not have (speculate ...). Once cvc5#14 merges and a release is cut, the pin moves and resident_speculate_probes_and_leaves_the_session_unchanged can be un-ignored.

🤖 Generated with Claude Code

[kiranandcode]

cvc5#14 changed again (head 2ea6c04194, after a review and merges of main #11 and #15). What this PR sees:

• When hypotheses apply. They used to run in a round of their own, before any strategy, and that round returned as soon as they sent a lemma. A speculative trigger that fed itself then kept every other formula from being instantiated: a query the :materialized formula proves unsat at once ran until killed, or was unknown under --inst-max-rounds. Hypotheses now apply at the start of the effort e-matching runs at, and their lemmas go out with that round's strategy lemmas. The probe check can therefore close in fewer rounds than before, and a trigger probe's verdict now matches what the #![trigger ...] snippet would give.
• pending means something narrower. Conflict-based instantiation runs before e-matching, so it can close a check before any hypothesis is applied. The report then says pending, where it used to say no-quantifier. no-quantifier now only appears for a hypothesis that was applied and found no formula with the qid. The doc on HypothesisReport::status in source/air/src/speculate.rs (pending (no instantiation round ran)) should read "no round reached e-matching".
• API checks. Solver::speculateInstantiation rejects terms with free variables, and speculateTrigger requires bound variables and a pattern whose free variables are among them. The resident worker sends (speculate ...) text, which the SMT-LIB parser already keeps closed, so nothing here should change.

I have not rerun this PR's speculate test against 2ea6c04194; it needs the pin moved first.

[kiranandcode]

Review

Reviewed at 60cfcc6 against cvc5#14 at 47d666d, built and run on a separate machine (arm64 macOS).

What holds. fmt and clippy are clean. air 201, rust_verify lib 36, and the resident suite (38 passed, 3 ignored) pass against the pinned cvc5, and resident_speculate_probes_and_leaves_the_session_unchanged passes against cvc5#14. The merge of main kept both sides of every conflict.

Bugs. Each one was reproduced with a fixture test.

1. Instantiation terms resolve names through the quantifier's own variables. In proof fn shadow(i: int) requires forall|i: int| #![trigger g(i)] g(i) > 0 && f(i) > 0, {"instantiation": {"subst": {"i": "i"}}} lowers the term to the bound i$, and the probe answers could_not_lower. Spelled i! by hand, the same instance closes the goal. An instantiation's terms are ground, in the query's scope, so they should never see the binders.
2. Mutable locals cannot be named. After let mut y = a; y = y + 1;, {"i": "y"} lowers to (I y@), the unversioned AIR Var, which cvc5 refuses as undeclared. (I y@1) works. A local should read as the SSA version in force at the goal.
3. Snippets can mention a stale version. In that query, the trigger probe f(i) closes, and its fallback_snippet is assert(((crate::g((y + 1)) > 0) && (crate::f((y + 1)) > 0)));, with y at version 0. Pasted before the goal, where y is version 1, it asserts a fact about a + 2. QueryNames::pasteable rejects a variable at two versions but not one at an old version. The egraph verus_assert shares the helper, so it has the same latent issue.
4. The lowering knows only the prelude's integer and boolean boxes. (Add a! 1) is never boxed and comes back mismatch, because Declarations seeds I/B/%I/%B by hand and nothing else from the prelude.

Fixed on cvc5#14 at 47d666d: a directed instance over a constant cvc5 had substituted away never connected. At 4cf5707, (I y@1), the goal's exact term, was applied but the query stayed invalid, while the trigger f(i) and a pasted assert(g(y) > 0) both closed it. The description should name 47d666d as the minimum cvc5#14 commit.

Nits.

• An (error line anywhere in the early flush counts as the hypothesis's refusal, including one caused by the query's own assertions.
• SpeculationOutcome.status documents rejected as "the instantiation was made already". cvc5 gives three reasons: a duplicate instantiation, a lemma already sent, or the instantiation level limit.
• The surface parser reads no method calls, indexing, as or @, so s[i] and s.len() must be given in SMT spelling. The scaffold lowerer merged in Resident scaffold requests: try one intermediate assertion at one goal #37 reads all of these.

I am pushing fixes for all of the above to this branch, with regression tests, and will follow up with the results.

[kiranandcode]

Fixes pushed

Two commits on top of 60cfcc6:

• a9191e3 merges main at 27cd2c5 (Add the resident twin request: a query and one edit of it, compared #34's twin, Resident ladder requests: which quantifier instantiation strategy discharges a query #35's ladder, the cvc5 pin at basis-79e8830406). The conflicts were side-by-side additions in context.rs, lib.rs, smt_verify.rs, resident.rs and the resident tests, and both sides were kept. Add the resident twin request: a query and one edit of it, compared #34 added the same journal base this PR had, so the journal and verifier.rs now follow main's record_base.
• a493da7 fixes every item in the review above.

The fixes.

1. Shadowed parameters. An instantiation's terms are read outside the quantifier, so they no longer see its variables. {"i": "i"} in shadowed(i) now means the parameter and closes the goal.
2. Mutable locals. The request's names are checked first. Then before runs, and the terms are read at the goal it failed at (the last goal when it names none). Verus terms go through Resident scaffold requests: try one intermediate assertion at one goal #37's scaffold lowerer (scaffold::lower_term, with the quantifier's variables as bound for a trigger), then through air::GoalScope, which reads them as the lowered query does at that assert. y becomes y@1. SMT-spelled terms map a variable's AIR name to the same version.
3. Stale snippets. QueryNames::pasteable now also rejects a variable at a version other than the one live at the goal. This applies to speculate and to the egraph's verus_assert.
4. Prelude functions. The SMT-spelled path asks Context::declared about names the journal lacks, instead of seeding four boxes by hand. (Add a! 1) is boxed and closes.

The nits. An echoed marker now precedes (speculate ...), so an (error counts as the hypothesis's only after it. The rejected doc names all three reasons. Method calls, indexing, casts, @ and old are read through the scaffold lowerer. A new readings field says how an ambiguous name was read.

Tests (arm64 macOS; cvc5#14 at 47d666d for the ignored ones):

• resident_speculate_reads_terms_at_the_goal is new. It covers the shadowed parameter, the mutable local (its snippet pasted into a fresh worker verifies), (Add a! 1), the trigger's fallback (offered only when it names no stale version, and verified when it is), and s.len() - 1. It passes together with resident_speculate_probes_and_leaves_the_session_unchanged.
• The resident suite against the pinned cvc5 gives 47 passed (the 2 speculate tests are ignored).
• The air unit tests give 214 passed, including goal_scopes_read_variables_where_the_goal_is. The rust_verify lib tests give 46 passed, including lowering_reads_ground_terms_at_the_goal and pasted_asserts_name_variables_at_their_version_where_pasted.
• fmt and clippy (--all-targets -D warnings) are clean.

The toyDB acceptance runs in the description predate these fixes. Their terms were all in the solver's spelling, which reads the same now, but they were not rerun. The description is updated. The cvc5 pin still has to move to a release with #14 at 47d666d or later before the speculate tests can be un-ignored.

[kiranandcode]

cvc5#14 changed again, after a third review: head da4b2b0073. What this PR sees:

• A formula keeps its :qid when cvc5 eliminates one of its variables. cvc5's rewriter used to drop the whole pattern list, :qid included, once variable elimination removed a variable (forall x y. x = y + 1 => ... becomes forall y. ...). Every hypothesis about such a formula then came back no-quantifier from cvc5, even though find_quantifier had found it in the retained AIR. The :qid now stays; the patterns still go.
• Naming the eliminated variable is now a mismatch. The resident sends a term for each variable the user names, read against the AIR binders. cvc5's formula no longer binds the eliminated one, so a request that names it is reported as mismatch with the reason "the formula binds no variable named x" (speculate-varelim shows it). Naming only the remaining variables works. Two options, not decided here: the resident could drop names that cvc5 reports as unbound and retry, or cvc5 could accept a term for an eliminated variable. How often AIR produces such a binder (an equality guard on a quantified variable) is not measured.
• Alpha-equivalent formulas are registered once, whatever their :qid (--quant-alpha-equiv, base cvc5 behaviour). If two asserted quantifiers have the same body and different qids, a hypothesis on the second qid gets no-quantifier from cvc5 even though find_quantifier finds it in AIR. This is now documented on speculateInstantiation.
• A new rejected reason: "the instance simplifies to true". It used to be reported as "the instance is a lemma already sent". The reason is passed through as text, so nothing breaks, but the status doc in resident.rs (around line 1914) lists three reasons and needs this one too.
• Smaller changes, none of which should reach this PR: a variable named twice in :instantiate or :trigger is now an error, which a JSON object of terms can't produce; speculate in a logic without quantifiers is a recoverable error instead of ending the session; and a :block fingerprint can be headed by an indexed operator such as (_ extract 3 0).

Still stale from the last round: the pending doc reads "no instantiation round ran" in both source/air/src/speculate.rs (HypothesisReport::status) and resident.rs. Since cvc5 47d666d it means that no round reached e-matching, for instance because conflict-based instantiation closed every check first.

Not done: resident_speculate_probes_and_leaves_the_session_unchanged has not been rerun against da4b2b0073. The cvc5 pin here is main's (basis-79e8830406), so the test stays ignored until cvc5#14 merges and a basis- release is built from it. cvc5-side testing for this round is in the cvc5#14 description: regress0 2730/2730, regress1 quantifiers/nl/proofs 363/363, and every verdict unchanged over 710 quantifier and nl files.

[kiranandcode]

Addressed in f553280 and 2ba14e6, with main merged in twice (8551697 for #41, eff2440 for #33), and tested against cvc5#14 at da4b2b0073.

• Eliminated variables. I took the resident-side option. An instantiation must name every AIR variable, so without a retry a formula cvc5 had rewritten this way could not be instantiated at all. When cvc5 answers mismatch with "the formula binds no variable named x" for a variable the request named, the worker sends the instance again without it, once per such variable. It lists them in a new eliminated field and says so in notes. The requested term for an eliminated variable need not be the one its equality fixes, so the snippet is the instance cvc5 made (from :bodies, type guards dropped), offered only when it pastes. A trigger's fallback_snippet is now built only when cvc5's instance terms line up with the quantifier's variables; after an elimination they don't.
• Alpha-equivalent formulas. When cvc5 answers no-quantifier for a formula the scope asserts, notes now says that cvc5 registers alpha-equivalent formulas once, under the first qid, and drops a formula that rewrites away.
• The fourth rejected reason ("the instance simplifies to true") is in the status docs in resident.rs and air::speculate.
• pending reads, in both places, that no instantiation round reached e-matching, for instance because conflict-based instantiation closed every check first.
• main moved twice more, and both are merged in. Scaffold: place a postcondition checked at an early return before it #41 merged cleanly. Add resident ablate: delta-debug a query's axioms and hypotheses to a witness #33 (ablate) conflicted only in side-by-side additions: the module docs, COMMANDS (now list, check, bisect, ablate, egraph, scaffold, close, inst_graph, ladder, twin, speculate) and the expected list in resident_ready_lists_the_requests_it_serves. Both sides were kept. Add resident ablate: delta-debug a query's axioms and hypotheses to a witness #33 also moved a spinoff's context into its journal's scopes. Speculate reads the journal's base and the prefix contexts, so it still sees every declaration.

Tests (arm64 macOS, on the merged tree):

• resident_speculate_probes_and_leaves_the_session_unchanged and resident_speculate_reads_terms_at_the_goal both pass against cvc5#14 built at da4b2b0073. The second gained a generic quantifier with an equality guard (forall|x: A, y: A| x == y ==> p(x)), which closes at {x: a, y: a}. cvc5 keeps both of its variables there, since the equality is between boxed values under type guards. So no Verus fixture reaches the elimination yet, and the retry's reading of the refusal is covered by the unit test an_eliminated_variable_is_read_from_the_refusal.
• The resident suite against the pinned cvc5 gives 50 passed, with the 2 speculate tests ignored. The air unit tests give 216 passed, and the rust_verify lib tests 48. fmt and clippy (--all-targets -D warnings) are clean.
• The cvc5 pin is still main's basis-79e8830406, so the speculate tests stay ignored until cvc5#14 merges and a release is cut from it; the description now names da4b2b0073 as the minimum.

[kiranandcode]

cvc5#14 is merged, so this PR now pins its release and runs its own tests.

• 8a07d65 pins cvc5 to basis-e68dc63e37, cvc5 main at S2: serve retained cvc5 buckets after compilation #14's merge. It also carries Show provenance terms as source, by recording names at encode time #11's :branch-profile. The only cvc5 change after da4b2b0073 reads an integer term given for a real variable as a real, and Verus's encoding never sends one. resident_speculate_probes_and_leaves_the_session_unchanged and resident_speculate_reads_terms_at_the_goal are no longer ignored.
• Conflicts: none. main is still at da8fa53, which this branch already merges.

Tests (arm64 macOS, pinned cvc5 fetched by get-cvc5.sh, solver version check on):

• The resident suite gives 52 passed and none ignored, both speculate tests included.
• The air unit tests give 216 passed, and the rust_verify lib tests 48.
• fmt and clippy (--all-targets -D warnings) are clean.

Ready to merge once CI passes on this head. Nothing is waiting on cvc5 any more. The toyDB acceptance numbers in the description predate the review fixes and were not rerun; the plan's toyDB criterion was not met, as the description says.