pub fn observe_resource_stops<R>(
f: impl FnOnce() -> R,
) -> (R, Option<Unreduced>)Expand description
Whether a verdict depended on kernel work that stopped for want of a resource: a conversion
that says “not equal” decided nothing when one of its reductions ran out of budget.
Run f and report the first resource stop of any kernel work it did — a reduction that spent
its step budget, or a term too deep to descend — on this thread or on any sized-stack thread
the kernel started for it.
This is what makes “not equal” an answer. A conversion that returns false after one of its
reductions stopped short has compared a partial term, and a partial term can differ from a
normal form it never reached: that false is an UNDECIDED comparison, never evidence that the
two sides differ. Only the conversion that ran knows whether it depended on such a stop, so
the record is taken from inside it — never reconstructed afterwards by normalizing the whole
sides again, which costs more than the conversion it audits and cannot even see what the
conversion actually compared (refute-cheap-first refutes (false, count 200) against
(true, count 201) at the booleans without ever evaluating count).
Observations nest: the record of the enclosing observation is restored afterwards, and learns of a stop inside this one too.