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

source/air/src/bisect.rs

@@ -218,6 +218,12 @@ impl Answer {
         }
     }
 
+    /// The solver cancelled the check at a wall-clock cap
+    /// (`Prober::set_probe_timeout`), so the probe says nothing.
+    pub fn timed_out(&self) -> bool {
+        matches!(self, Answer::Unknown(reason) if reason == "timeout")
+    }
+
     /// The classes a `Changed` search tells apart: the result, and for
     /// `unknown` whether the solver ran out of budget or gave up.
     pub fn class(&self) -> &'static str {
@@ -309,6 +315,8 @@ pub struct Prober<'c> {
     context: &'c mut Context,
     units: Vec<Unit>,
     checks: usize,
+    /// Wall-clock cap per probe, in milliseconds (see `set_probe_timeout`).
+    probe_timeout_ms: Option<u64>,
     /// The switch that turns every goal into `false` (ablation only).
     vacuity: Option<Ident>,
     /// The scope was opened with `Context::push`, so the AIR logs saw it too.
@@ -355,7 +363,14 @@ impl Context {
         match assert_switchable(self, &query, facts, None) {
             Ok(mut units) => {
                 units.sort_by_key(|u| u.sort_key());
-                Ok(Prober { context: self, units, checks: 0, vacuity: None, air_scope: false })
+                Ok(Prober {
+                    context: self,
+                    units,
+                    checks: 0,
+                    probe_timeout_ms: None,
+                    vacuity: None,
+                    air_scope: false,
+                })
             }
             Err(err) => {
                 self.pop_name_scope();
@@ -394,6 +409,7 @@ impl Context {
                     context: self,
                     units,
                     checks: 0,
+                    probe_timeout_ms: None,
                     vacuity: Some(vacuity),
                     air_scope: true,
                 })
@@ -537,6 +553,13 @@ impl<'c> Prober<'c> {
     }
 
     /// Ask the solver about the query with `disabled[i]` switching off
+    /// Cancel any probe that runs longer than `ms` milliseconds of wall-clock
+    /// time: it answers `unknown` with reason `timeout` (`Answer::timed_out`),
+    /// which the searches take as not valid. `None` lifts the cap.
+    pub fn set_probe_timeout(&mut self, ms: Option<u64>) {
+        self.probe_timeout_ms = ms;
+    }
+
     /// `units()[i]`, under the query's resource budget. An `Err` carries
     /// solver output this could not read.
     pub fn probe(&mut self, disabled: &[bool]) -> Result<Answer, String> {
@@ -585,6 +608,7 @@ impl<'c> Prober<'c> {
             let var = ident_var(switch);
             literals.push(if vacuous { var } else { mk_not(&var) });
         }
+        let probe_timeout_ms = self.probe_timeout_ms;
         let context = &mut *self.context;
         let detailed = detailed && matches!(context.solver, SmtSolver::Cvc5);
         match context.solver {
@@ -597,6 +621,9 @@ impl<'c> Prober<'c> {
                 context.smt_log.log_set_option("reproducible-resource-limit", &budget.to_string());
             }
         }
+        if probe_timeout_ms.is_some() {
+            context.set_check_timeout(probe_timeout_ms);
+        }
         context.smt_log.log_check_sat_assuming(&literals);
         if detailed {
             // in the same batch, right after the answer it describes
@@ -614,6 +641,9 @@ impl<'c> Prober<'c> {
             }
             SmtSolver::Cvc5 => context.smt_log.log_set_option("reproducible-resource-limit", "0"),
         }
+        if probe_timeout_ms.is_some() {
+            context.set_check_timeout(None);
+        }
         let mut answer = None;
         let mut detail = ProbeDetail::default();
         for line in output {

source/air/src/context.rs

@@ -1113,6 +1113,20 @@ impl Context {
         crate::smt_verify::cvc5_query_budget(self)
     }
 
+    /// Bound each following `check-sat`'s wall-clock time to `ms`
+    /// milliseconds (cvc5's `tlimit-per`, z3's `timeout`): a check that
+    /// reaches it is cancelled by the solver and answers `unknown` with
+    /// reason `timeout`. `None` lifts the bound. The option goes to the
+    /// solver with the next commands sent, and stays until set again.
+    pub fn set_check_timeout(&mut self, ms: Option<u64>) {
+        let ms = ms.unwrap_or(0).to_string();
+        let option = match self.solver {
+            SmtSolver::Z3 => "timeout",
+            SmtSolver::Cvc5 => "tlimit-per",
+        };
+        self.smt_log.log_set_option(option, &ms);
+    }
+
     /// Ask the solver for the instantiation graph of its last `check-sat` and
     /// return its reply lines (cvc5 with `set_inst_graph` only). Read-only:
     /// call it after a query's answer and before anything that checks again.

source/rust_verify/src/resident.rs

@@ -235,6 +235,17 @@ enum Request {
         /// candidates. Lets a caller search past a witness the absence
         /// check disowned.
         exclude: Option<Vec<usize>>,
+        /// Resource limit for each probe, in `#[verifier::rlimit]` units,
+        /// above 0 and at most `MAX_RUNG_RLIMIT`. Default: the query's own.
+        /// A diagnostic budget for the probes alone: the absence check, an
+        /// ordinary check of the witness, keeps the query's own limit, as
+        /// does every other request.
+        rlimit: Option<f32>,
+        /// Wall-clock cap per probe, in milliseconds. A probe that reaches
+        /// it is cancelled by the solver (it answers `unknown`, reason
+        /// `timeout`, and the search takes it as not valid), is listed in
+        /// `skipped_probes`, and the reply is marked `partial`.
+        probe_timeout_ms: Option<u64>,
     },
     Egraph {
         session: String,
@@ -1374,13 +1385,24 @@ struct AblateReport {
     probes: Vec<BisectProbe>,
     elapsed_ms: u128,
     restore_ms: u128,
+    /// Some probe was cancelled at the request's `probe_timeout_ms`, so the
+    /// witness is what the other probes established: possibly not minimal,
+    /// and confirmed only as far as `skipped_probes` allows.
+    partial: bool,
+    /// The probes cancelled at the wall-clock cap, by what they asked.
+    #[serde(skip_serializing_if = "Vec::is_empty")]
+    skipped_probes: Vec<String>,
 }
 
 struct AblateRequest {
     mode: AblateMode,
     budget: usize,
     hypotheses: bool,
     exclude: Vec<usize>,
+    /// The probes' own resource limit; `None` keeps the query's.
+    rlimit: Option<f32>,
+    /// Wall-clock cap per probe.
+    probe_timeout_ms: Option<u64>,
 }
 
 /// A goal the vacuity probes name.
@@ -1421,6 +1443,8 @@ fn scan_vacuity(
     goals: &[usize],
     removed: &[usize],
     checks: &mut usize,
+    skipped: &mut Vec<String>,
+    label: &str,
 ) -> Result<VacuityScan, String> {
     use air::bisect::Answer;
     let count = prober.units().len();
@@ -1434,6 +1458,9 @@ fn scan_vacuity(
     if goals.is_empty() {
         let answer = prober.probe_vacuity(&mask(removed))?;
         *checks += 1;
+        if answer.timed_out() {
+            skipped.push(format!("{label} vacuity probe"));
+        }
         return Ok(VacuityScan { answer, goal: None, unchecked: 0 });
     }
     let mut unknown = None;
@@ -1448,6 +1475,9 @@ fn scan_vacuity(
         off.extend(goals.iter().copied().filter(|&g| g != goal));
         let answer = prober.probe_vacuity(&mask(&off))?;
         *checks += 1;
+        if answer.timed_out() {
+            skipped.push(format!("{label} vacuity probe of goal {goal}"));
+        }
         if answer == Answer::Valid {
             return Ok(VacuityScan { answer, goal: Some(goal), unchecked: 0 });
         }
@@ -1476,14 +1506,21 @@ fn ablate(
     query: &RetainedQuery,
     symbols: Option<&crate::provenance::Symbols>,
     request: AblateRequest,
+    set_rlimit: &impl Fn(&mut Context, f32),
 ) -> io::Result<AblateReport> {
     use air::bisect::{Answer, Mode, ProbeDetail, Status, Target, UnitKind};
     let group_of = |axiom: &air::ast::Axiom| -> Option<String> {
         symbols.and_then(|symbols| symbols.axiom_group(axiom)).map(str::to_owned)
     };
+    // The probes' budget: their own rlimit when the request gives one, and
+    // a wall-clock cap each. The absence check below runs at the query's.
+    set_rlimit(air, request.rlimit.unwrap_or(query.rlimit));
     let mut prober = air
         .ablate_query(prefix, &mut |axiom| group_of(axiom), &query.query)
         .map_err(|error| io::Error::other(error.to_string()))?;
+    prober.set_probe_timeout(request.probe_timeout_ms);
+    // Probes the solver cancelled at the cap, by what they asked.
+    let mut skipped: Vec<String> = Vec::new();
     let units = prober.units().to_vec();
     let count = units.len();
     let no_candidate = |&&i: &&usize| {
@@ -1514,6 +1551,9 @@ fn ablate(
     };
     let mut details: HashMap<Vec<usize>, ProbeDetail> = HashMap::new();
     let (before, detail) = prober.probe_detailed(&mask(&[])).map_err(io::Error::other)?;
+    if before.timed_out() {
+        skipped.push("probe with nothing removed".to_owned());
+    }
     details.insert(Vec::new(), detail);
     let mode = match request.mode {
         AblateMode::Auto if before == Answer::Valid => AblateMode::LoadBearing,
@@ -1561,7 +1601,11 @@ fn ablate(
         Some(before),
         &mut |disabled| -> Result<Answer, String> {
             let (answer, detail) = prober.probe_detailed(disabled)?;
-            details.insert(switched_off(disabled), detail);
+            let removed = switched_off(disabled);
+            if answer.timed_out() {
+                skipped.push(format!("search probe with {removed:?} removed"));
+            }
+            details.insert(removed, detail);
             Ok(answer)
         },
     )
@@ -1578,13 +1622,15 @@ fn ablate(
     let goals: Vec<usize> = (0..count).filter(|&i| units[i].kind == UnitKind::Goal).rev().collect();
     let mut extra_checks = 0;
     let vacuity_before =
-        scan_vacuity(&mut prober, &goals, &[], &mut extra_checks).map_err(io::Error::other)?;
+        scan_vacuity(&mut prober, &goals, &[], &mut extra_checks, &mut skipped, "before")
+            .map_err(io::Error::other)?;
     let mut vacuity_witness = None;
     let mut participated = Vec::new();
     let mut participation_unchecked = 0;
     if let Some(removed) = &witness_removed {
-        let scan = scan_vacuity(&mut prober, &goals, removed, &mut extra_checks)
-            .map_err(io::Error::other)?;
+        let scan =
+            scan_vacuity(&mut prober, &goals, removed, &mut extra_checks, &mut skipped, "witness")
+                .map_err(io::Error::other)?;
         // A removal leaves its members out of the contradiction by
         // definition; only kept members can take part in it. Each is tried
         // at the goal the scan found contradictory.
@@ -1601,6 +1647,9 @@ fn ablate(
                 without.push(member);
                 let answer = prober.probe_vacuity(&mask(&without)).map_err(io::Error::other)?;
                 extra_checks += 1;
+                if answer.timed_out() {
+                    skipped.push(format!("participation probe of unit {member}"));
+                }
                 if answer != Answer::Valid {
                     participated.push(member);
                 }
@@ -1622,18 +1671,35 @@ fn ablate(
         Some(removed) => {
             let answer = prober.probe_vacuity(&mask(&removed)).map_err(io::Error::other)?;
             extra_checks += 1;
+            if answer.timed_out() {
+                skipped.push("every-goal vacuity probe".to_owned());
+            }
             Some(answer)
         }
         None => None,
     };
     drop(prober);
 
+    // The absence check is an ordinary check of the witness: the query's
+    // own rlimit, which every later request expects to find, under the
+    // same wall-clock cap.
+    set_rlimit(air, query.rlimit);
     let absence_check = match &witness_removed {
         Some(removed) => {
             let probed_valid = outcome.after == Some(Answer::Valid);
-            let check =
-                absence_check(air, prefix, query, &group_of, &units, removed, probed_valid)?;
+            air.set_check_timeout(request.probe_timeout_ms);
+            let checked =
+                absence_check(air, prefix, query, &group_of, &units, removed, probed_valid);
+            if request.probe_timeout_ms.is_some() {
+                air.set_check_timeout(None);
+            }
+            let check = checked?;
             extra_checks += 1;
+            if check.result == QueryResult::ResourceLimit
+                && request.probe_timeout_ms.is_some_and(|ms| check.elapsed_ms >= ms as u128)
+            {
+                skipped.push("absence check".to_owned());
+            }
             Some(check)
         }
         None => None,
@@ -1789,6 +1855,8 @@ fn ablate(
             .collect(),
         elapsed_ms: 0,
         restore_ms: 0,
+        partial: !skipped.is_empty(),
+        skipped_probes: skipped,
     })
 }
 
@@ -5153,6 +5221,8 @@ impl Server {
                     budget_checks,
                     hypotheses,
                     exclude,
+                    rlimit,
+                    probe_timeout_ms,
                     ..
                 } => {
                     let Some(bucket) = self.buckets.get(bucket_id.0) else {
@@ -5171,6 +5241,20 @@ impl Server {
                         )?;
                         continue;
                     }
+                    if rlimit.is_some_and(|r| !(r.is_finite() && r > 0.0 && r <= MAX_RUNG_RLIMIT)) {
+                        send(
+                            &mut output,
+                            &Response::Error { message: "rlimit must be above 0 and at most 1000" },
+                        )?;
+                        continue;
+                    }
+                    if probe_timeout_ms == Some(0) {
+                        send(
+                            &mut output,
+                            &Response::Error { message: "probe_timeout_ms must be positive" },
+                        )?;
+                        continue;
+                    }
                     let mut state = match bucket.state.lock() {
                         Ok(state) => state,
                         Err(_) => {
@@ -5192,16 +5276,39 @@ impl Server {
                     let restore_ms = restore_start.elapsed().as_millis();
                     let query = &journal.queries[local];
                     let prefix = journal.prefix_decls(query.prefix);
-                    set_rlimit(air, query.rlimit);
+                    // A probe budget too small for one cvc5 unit converts to
+                    // 0, which cvc5 takes as no limit, as the ladder refuses.
+                    if let Some(probe_rlimit) = rlimit {
+                        set_rlimit(air, probe_rlimit);
+                        let empty = air.cvc5_query_budget() == 0;
+                        set_rlimit(air, query.rlimit);
+                        if empty {
+                            send(
+                                &mut output,
+                                &Response::Error {
+                                    message: "rlimit is below one cvc5 resource unit",
+                                },
+                            )?;
+                            continue;
+                        }
+                    }
                     let request = AblateRequest {
                         mode,
                         budget,
                         hypotheses: hypotheses.unwrap_or(true),
                         exclude: exclude.unwrap_or_default(),
+                        rlimit,
+                        probe_timeout_ms,
                     };
                     let start = Instant::now();
-                    let report = match ablate(air, &prefix, query, bucket.symbols.as_ref(), request)
-                    {
+                    let report = match ablate(
+                        air,
+                        &prefix,
+                        query,
+                        bucket.symbols.as_ref(),
+                        request,
+                        &set_rlimit,
+                    ) {
                         Ok(mut report) => {
                             report.elapsed_ms = start.elapsed().as_millis();
                             report.restore_ms = restore_ms;