Resident sessions never export instantiation certificates, so replay does not survive a reopen

[kiranandcode]

Symptom

A resident session with instantiation_replay replays certificates within the session, but never across sessions. Reopening the same target and checking the same query reports certificate: null where it should report source: "imported".

verus-tools-mcp's real_certificates_close_rechecks_and_survive_reopen fails on this:

  left: Null
 right: "imported"

Cause: nothing is ever exported

The certificate directory stays empty for the whole run. write_certificate (source/rust_verify/src/resident.rs) writes <dir>/<key>.smt2 only when air.export_instantiations(key) returns a certificate, and that appears to return None: there is no .smt2 and no leftover .partial file. The import side (read_certificate / set_import_instantiations) is therefore never exercised.

Saving works: the in-session path uses the solver's own saved instantiations, and a second check of the same query in the same session reports {"source":"session","closed":true}.

Reproduction

With a released Verus (the server downloads its pinned solvers):

1. open_session on a standalone file with instantiation_replay: true.
2. check_session the passing query twice: the first reports no certificate, the second source: "session", closed: true.
3. close_session, then open_session the same file again.
4. check_session the same query: certificate is null; expected source: "imported".

Throughout, the directory named by VERUS_RESIDENT_INST_DIR (the MCP server's per-target certificate directory) holds no files.

Affected builds

• basis-1a780498c0 (pins cvc5 basis-c893833109)
• basis-7f56f7cb1c (the release before it)

Both fail identically, so this predates #20 and the cvc5 bump to basis-c893833109. I have not bisected further to find where it broke, or whether cross-session import ever worked against a released build rather than a worktree build.

Why it may have gone unnoticed

The MCP-side test asserting imported is a real-toolchain test: it skips when no Verus is configured, so CI never runs it.

It is worth checking whether export_instantiations depends on a cvc5 command the currently pinned cvc5 no longer provides (the contract documented on the MCP side names save-instantiations, pinned from basis-77ab13ff5b).