A renewrenew nanofilA renew reuses an earlier check's bounds: renew(Lo, Hi, Rights, Align) of [Q1, P] trusts the dominating check that made Q1 for P's bounds and tests again only what a free changes, that the object is not freed (and, for a write, not read-only). It is the -O default (check_reuse:renew_checks/2, m7.md, round 4). whose bounds come from a guardguard nanofilRange guards, --checks=guard: a span test before a loop proves its accesses' bounds once, and the loop's checks become renew_if, which tests only the flags and alignment when the guard passed and runs the full check out of line otherwise (check_reuse:guard_checks/2, m7.md, Range guards (round 5)).: renew_ifLo, Hi, Rights, Align of [P, G] is exactly a check of P, but where the 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. 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/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., following P's 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. (ir:guard_chain/3ir.plguard_chain+Once, +P, -ChaindetRange guards (docs/m7.md, round 5, slice A). Chain is P-i(0, 0) followed by B-i(Lo, Hi) for each base B of P: P has B's capability and an address congruent modulo 2^64 to B's plus some X with Lo =< X =< Hi, through single-definition flights add, sub and copy whose lower donor is their address operand. Once maps each single-definition name to its definition (…).

Rocq: the op RenewIf; Guard.v's renew_if_not_unchecked and, along runs, run_guard_checked.