Range guards, --checks=guard: a span testspan_test nanofilspan_test(Lo, Hi) of a pointer P0 is 1 when P0's object contains [P0+Lo, P0+Hi), addresses taken modulo 2^64 and compared unsigned, and 0 otherwise, including for a null, function, external or freed capability. It never traps and reaches no safepoint: it is the guard that --checks=guard puts before a loop. before a loop proves its accesses' bounds once, and the loop's checks become renew_ifrenew_if nanofilA renew whose bounds come from a guard: renew_if(Lo, Hi, Rights, Align) of [P, G] is exactly a check of P, but where the span test G passed it natively tests only the flags and alignment, and where G failed it runs the full check out of line. The validator accepts it through ir:guard_covers/5, following P's guard chain (ir:guard_chain/3)., which tests only the flags and alignment when the guard passed and runs the full check out of line otherwise (check_reuse:guard_checks/2check_reuse.plguard_checks+M₀, -MdetRange guards (docs/m7.md, round 5, slice A). M is the checked module M0 with each heap check in a natural loop, followed by a renewable access, whose pointer is a base defined outside its innermost loop plus an offset with a constant interval (ir.pl's guard_chain/3), replaced by renew_if of that pointer and a guard: one span_test per loop and base, appended …, m7.md, Range guards (round 5)).

The validator accepts each renew_if through ir:guard_covers/5ir.plguard_covers+Once, +P, +G, +Lo, +HiG is a single-definition span test of a single-definition P0 whose span contains P's [Lo, Hi) for every offset P can have from P0.; Rocq transcribes guard_covers, and Guard.v proves that no run of a valid module makes one unchecked (run_guard_checked).