A frame is doomed after a check_aheadcheck_ahead nanofilcheck_ahead(Lo, Hi, Rights, Align, AHi) is a check of [Lo, Hi) whose own access needs only [Lo, AHi): the bytes [AHi, Hi) are checked early for later accesses through the same base, as filcc's check scheduler does. It may trap earlier than the reference program, but only on runs that would trap later anyway. 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.

• interp.pl: interp:doomed_result/5interp.pldoomed_result+Inst, +Ctx, +Env₀, +Result₀, -Resulta check_ahead whose early bytes fail (docs/schedule.md) yields its pointer and dooms the run: from then on it must reach, through ahead_transparent/1 instructions only, an access whose reference check fails, which shows here as a renew's failed span or a raw access's unchecked bounds (a read of the widened proof itself). That is the program's trap, made earl…. The doomed run ends trapearlyWhy at the failing access, or uncheckedaheadWhy if it first reaches a poll edge, a return or an instruction that is not ahead-transparentahead-transparent nanofilAn instruction is ahead-transparent when it may stand between a check_ahead and the access whose need it checks early: it reaches no safepoint, calls nothing, cannot free, and is not a division, whose fault would end the program other than by a Fil-C trap.. A renew of another object or a wrong limit stays uncheckedalias or uncheckedlimit.

• Rocq: the fr_doomed field of frame, doomed_result, edge_step, jump_step. Doomed.v proves a doomed frame never steps to unchecked (run_doomed_checked) with the invariant dinv / doomed_ok: the 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. holds weakly (scope_weak: a doomed proof holds its pointer, not a passed check), memory keeps the doom (doom_mem), and the validator's needneed nanofilA need is the validator's backward fact for check_ahead: need(B) = H at a point says every path from it reaches a raw heap access through a pointer of which B is an exact base, whose bytes reach B + H, and reaches it first: before any instruction that is not ahead-transparent, any poll edge, edge back or end, and before B is redefined. at the point covers it (need_at).

The subtlety: a doomed frame claims nothing for 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. or 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.; both exclude it, and Doomed.v treats it apart. A doomed frame never calls or returns, so every waiting callerparked nanofilA waiting caller is a frame 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. is undoomed.

See rocq.md, The doomed frame and schedule.md, Interpreter rule.