A waiting caller is a frameframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point. suspended at a call until its callee returns; the configuration keeps them in c_callers, each with how it will read the result (pending). interp.pl has none: its callers wait on Prolog's own stack.

Each run-level invariant says what holds of a waiting caller:

• parked (Invariant.v, the evidence invariantevidence invariant nanofilThe evidence invariant says that along every run, at the running frame's point, the live facts the evidence pass computed for that point hold: each fact's check passes in the current memory, and its pointer has a single definition dominating the point. It is how the pass's static bookkeeping becomes a fact about runs.): it runs a function of the module, its locals lie above 0, it is not doomeddoomed frame nanofilA frame is doomed after a check_ahead whose early bytes failed: the check yields its pointer anyway and the frame records the failure, because the validator promised that the frame will reach an access that fails on those bytes before anything observable happens., and it waits just after its call with no fact, since a call ends every live factlive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own.; the pass walks the rest of its block from nothing (walks).

• waiting (Single.v, the single-definition invariantsingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point.): it is not doomed, waits just after the call that made its callee (waits), and holds its scopescope nanofilA frame's scope is the set of single definitions whose site dominates its point: the names the reuse rules may read relations off there. The single-definition invariant says every one of them replays..

Why no waiting caller is doomed: a doomed frame never calls, so it never becomes one. call_parked and parked_resume carry a frame into and out of waiting.

See rocq.md, The evidence invariant over runs.