An instruction is ahead-transparent when it may stand between 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. and the access whose 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. 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.

• ir:ahead_transparent/1ir.plahead_transparent+InstsemidetInst may come between a check_ahead and the access whose need it checks early (docs/schedule.md): it is evidence_preserving/1, so it reaches no safepoint, calls nothing and cannot free, and it is not a division, whose fault would end the program otherwise than a Fil-C trap. Calls, allocation, getters, pointer stores, atomics, setjmp and va_arg are not, nor a… is ir:evidence_preserving/1ir.plevidence_preserving+InstsemidetInst reaches no safepoint and cannot free an object or change its bounds or rights: pure arithmetic, comparison and conversion, pure pointer construction, a heap check, a scalar raw access (object headers lie outside every object's bounds) and a raw pointer load (aux and box reads, no helper). Calls, alloc, getters, setjmp, va_arg, pointer stores and the res… less div, udiv, rem and urem; Syntax.v's ahead_transparent is the same table. Not transparent: calls, allocation, getters, pointer stores, atomics, setjmp, va_arg. Poll edges, edges back and returns also end the scheduled region.

• A 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. frame that reaches a non-transparent instruction is uncheckedaheadWhy, in interp:insts_result/5interp.plinsts_result+Insts, +Ctx, +Env₀, +S₀, -ResultnondetResult is cont(Env, S) when every instruction ran, or stop(Outcome, S) when one ended the run. and in step.

Why it is enough: what an early trap skips are scalar stores, loads and arithmetic, which nobody in the process observes once it has trapped (schedule.md, nanofil's contract).

The subtlety: the check's own access counts too, so a check whose access is a pointer store or an atomic is never widened, where filcc would widen it.