Campaign 3's scheduled checkscheck_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.: what the validator's backward pass for check_ahead computes, point by point (formal.md, Campaign 3; rocq.md, Facts ahead; schedule.md). It is the first step toward the doomed framedoomed 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. of Doomed.v.

ahead_justified/3 walks a function's blocks once, from the last, and each block's instructions from its jump. At each point it keeps needsneed 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.: a single-definitionsingle 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. base N with an offset H, meaning that every path from the point reaches, through 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. instructions only and before any poll edgepoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1)., edge back or end, a raw access through N whose bytes reach N + H. A check_ahead is accepted where its access is followed by a need that covers the bytes it checks early. This file states those needs as functions of the point, so that a frame can carry them forward, and proves that the pass's one sweep computes them.

Decisions