A need is the validator's backward fact for 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.: 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 baseexact base nanofilAn exact base of a pointer P is a single-definition name B on P's guard chain whose offset interval is one point, B-i(K, K): P's address is B's plus exactly K, modulo 2^64, with B's capability., whose bytes reach B + H, and reaches it first: before any 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., any poll edge, edge back or end, and before B is redefined.

• ir.pl computes needs in one backward sweep over the blocks, last first: ir:ahead_justified/3ir.plahead_justified/3not documented with ir:ahead_block/6ir.plahead_block/6not documented, ir:ahead_edge/5ir.plahead_edge/5not documented, ir:raise_need/6ir.plraise_need/6not documented and ir:ahead_meet/2ir.plahead_meet+Facts, -Meetthe bases in every one of Facts, each with its least need; none for no facts.. A block's exit needsexit facts nanofilA block's exit facts are what a validator pass knows at its jump; its entry facts are what it knows before its phis. Two passes keep them, over the same edge rule: entry facts are the meet over incoming edges, nothing comes over a poll edge, and an edge from a block the pass has not yet reached carries nothing. are the meet over its edges, keeping the least H; a plain edge to a later block carries that block's entry needs, any other edge none.

• Ahead.v states them as functions of the point, block_exit and facts_from, and proves the sweep computes them (ahead_entry, ahead_accepted). Doomed.v carries them forward along a doomed run (need_at); the access that meets one fails (need_access_fails).

The subtlety: offsets along a guard chainguard chain nanofilA pointer's guard chain lists its bases with the offset of its address from each: P itself at i(0, 0), then each base B reached through single-definition add, sub and copy flights whose lower donor is their address operand, with an interval for P's address minus B's, modulo 2^64. P has the capability of every base on its chain. are exact only modulo 2^64, so a need counts only near offsetsnear offset nanofilA near offset is one within 2^62 of 0. The validator's offsets between pointers (guard chains, pointer distances) are exact only modulo 2^64, because address arithmetic wraps; for a near offset the integer is the true signed distance, so the validator counts only near ones where it compares positions..

See schedule.md, Validator rule and rocq.md, Facts ahead.