S2: retain specialised queries and match batch error reporting - #15
Merged
Merged
Conversation
A recheck reported at most one error per query while the original invocation reports up to --multiple-errors of them, so a function with two failing assertions came back with one. Reading a session as a re-verify oracle therefore saw fewer errors than the run it was meant to reproduce, with nothing to indicate the difference. The Check handler now loops on check_valid_again exactly as check_result_validity does, carries the same "not all errors may have been reported" note, and keeps the verdict and assert_id of the first failure. --multiple-errors joins the session settings so a recheck looks exactly as far as the run did. Preparation that fails after the compiler driver returns published nothing at all: resident_prepared stays false, the summary line is suppressed under --resident, so the caller saw an empty stdout, or a socket that never accepted, and could not tell either from a crash. It now sends one error frame over whichever transport the caller is waiting on. The reason itself is already on stderr. Framing failures closed the session silently, which is what `fatal` was written to avoid: an oversized line, invalid UTF-8, a poisoned bucket and a failed shutdown now each send a frame before closing. The three session settings were assembled by builders whose defaults were never the right value, and this change needed a fourth. They are one SessionInfo passed to Server::new instead, since every field has to come from the invocation. Validation: resident subprocess tests 16 passed, three of them new and one rewritten to assert the frame that preparation failure now sends; resident unit tests 3 passed; AIR 149; basic 61 and one ignored; recommends 15 and two ignored; expand_errors 5. Formatting and `cargo clippy -- -D warnings` as CI runs it are clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011mxEg8kXgBFiUGBXVG8HNG
`check_result_validity` splits `Invalid` in two: a failure the solver returned no model for breaks out, and only a failure with both a model and a message goes round again. The Check handler collapsed both into one arm and called `check_valid_again` on either, which panics rather than reporting when the context holds no model, taking every retained solver with it. The arms now match the batch run's. A `Canceled` on a later round was dropped: the verdict is already `invalid` by then, so `get_or_insert` did nothing and the reply gave no sign the rlimit had cut the error list short. It now carries the same "Resource limit (rlimit) exceeded" diagnostic the batch run reports on every round, minus the `--profile` hint, which is a rerun the caller of a session does not make. The note about a truncated search stays guarded on the query having failed, which the batch run does not do; at `--multiple-errors 0` its counter starts spent and it says the search was cut short even for a query that passed. The comment now says the departure is deliberate. `--multiple-errors` had one test, at the default of 2, so hardcoding the new session field would have passed. The test now runs 0, 2 and 3 and pins the error count and the note against each. Also: `fatal`'s doc comment had been left attached to `report_unavailable`, describing a function it is not about, and `note` sat in a second `impl QueryDiagnostics` block beside the first. `bare` replaces it in the first block and carries the level, since the rlimit diagnostic needs the query's own. Validation: resident subprocess tests 16 passed, resident unit tests 3, basic 61 and one ignored, recommends 5, expand_errors 15 and two ignored. Formatting and `cargo clippy -- -D warnings` clean for rust_verify and the resident test target. Built with vargo against the pinned cvc5 1.3.5.dev+main@4a42bee. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YCzizB3HPQ9cCESBM4AwSY
kiranandcode
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Retained sessions now recheck nonlinear and bit-vector obligations in their original solver processes. The catalogue identifies each query's prover. Bit-vector solvers remain prelude-free and use incremental query scopes; nonlinear solvers retain their existing tuning. Both routes support provenance and
spinoff-all. Singular remains unsupported.Rechecks also follow the original invocation's
--multiple-errorssearch, including resource-limit and incomplete-search diagnostics. The response keeps the first verdict, assertion ID and provenance together. Later rounds add diagnostics without replacing round-zero provenance. Queries without a model stop where batch verification stops.Preparation failures send an error frame over stdio or the Unix socket. Framing failures and explicit shutdown errors report why the session ended. Required invocation settings are passed together as
SessionInfo.Validation: 19 native resident subprocess tests and three journal tests pass; formatting and clippy are clean. Coverage includes ordinary/retained verification-summary parity, serial/parallel preparation, provenance with and without spinoff, repeated checks across specialised solvers, unchanged solver launch logs, balanced scopes, close/EOF cleanup, and a regression that marks real solver rounds to detect provenance replacement. The actual MCP integration performs open, six specialised checks and graceful close with provenance/spinoff enabled.
Targets
mainafter merged #14. Custom SMT options remain separate in #16. Companion client changes are in verus-tools-mcp #16, including correct handling of preparation error frames.