check_aheadLo, 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.

• Made by schedule:schedule_checks/2schedule.plschedule_checks+M₀, -MdetM is the checked module M0 with each heap check widened to a check_ahead over the bytes that every path ahead needs from its base, then each check that a dominating check or check_ahead covers at a distance renewed. Functions with a setjmp are unchanged. under --checks=schedule (opt-in); emitted as a plain check of the whole range.

• Accepted by ir:ahead_justified/3ir.plahead_justified/3not documented where, right after its access, the 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. of P's 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. B (P = B + K) is at least K + Hi, the access is 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., K and K + Lo are 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., and the function has no setjmp. Rocq: ahead_justified in Validate.v, read back by Ahead.v's ahead_accepted.

• interp.pl tests [Lo, AHi) first and traps as a check would; if only the rest fails, the frame is 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..

The subtlety: the bound on K + Lo came from a counterexample in which the check's start wrapped onto the need's end modulo 2^64 (rocq.md, A need past 2^64).

See schedule.md.