Ablation probes take their own rlimit and a wall-clock cap per probe

[kiranandcode]

Worker side of BasisResearch/verus-tools-mcp#48 (ablate_to_witness's probe budget). Both request fields are optional and the reply change is additive.

Request (Request::Ablate, source/rust_verify/src/resident.rs)

• rlimit (f32, #[verifier::rlimit] units, 0 < r ≤ 1000): the resource limit each probe runs at. Refused as an error (session kept) when out of range or when it converts to no cvc5 unit, like a ladder rung. It applies to the probes only — the search, vacuity, every-goal and participation probes. The absence check (an ordinary check of the witness) runs at the query's own rlimit, which ablate restores before it, so every later request finds the session's limit unchanged.
• probe_timeout_ms (u64 > 0): a wall-clock cap per probe. Prober::run now brackets each check-sat-assuming with cvc5's tlimit-per (z3's timeout) and lifts it afterwards; the absence check runs under the same cap. A probe the solver cancels answers unknown with reason timeout (Answer::timed_out), which the search already treats as not valid.

Reply (AblateReport)

• partial: bool — some probe was cancelled at the cap.
• skipped_probes: [String] (omitted when empty) — each cancelled probe by what it asked: probe with nothing removed, search probe with [3, 7] removed, before vacuity probe of goal 5, participation probe of unit 2, every-goal vacuity probe, absence check.

air

• Context::set_check_timeout(Option<u64>) emits the solver's per-check time option.
• Prober::set_probe_timeout(Option<u64>); Answer::timed_out().

Tests

• New resident_ablation_probes_take_their_own_budget (rust_verify_test/tests/resident.rs): both fields accepted with a generous cap (partial: false, no skipped_probes); bad budgets refused without ending the session (rlimit 0 / 5000 / 1e-9, probe_timeout_ms 0); a 1 ms cap yields partial exactly when skipped_probes is non-empty and the reply then names a timeout; the session still answers valid afterwards; the SMT logs show exactly two budgets, the session's and twice it for the rlimit-4 probes; every tlimit-per set is matched by a reset; pushes balance pops.
• Ran: cargo test --release -p rust_verify --lib resident::tests (17 passed) and cargo test --release -p rust_verify_test --test resident ablat (4 passed) after vargo --no-solver-version-check build --release (vstd 2045 verified); cargo fmt --check clean on the touched crates. The full vstd/test suite was not run.

🤖 Generated with Claude Code