span_testLo, 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 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)). that --checks=guard puts before a loop.

• A 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). of P reads its result G. 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. accepts it when G is a single-definition span test of a single-definition P0 and 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. puts P's span inside the tested one. Where G is 0 the renew_if runs the full check out of line.

• interp.pl evaluates it in interp:kind_res/8interp.plkind_res+Kind, +Op, +K, +Mode, +Args, +S₀, -Res, -Sas op_res/7, for Op of Kind. Loads and allocs use the memory; the rest is arithmetic.; Validate.v transcribes guard_covers. Guard.v proves the trust sound: span_test_ok, guard_inside, renew_inside, and along runs run_guard_checked.

The subtlety: the span test reduces its two addresses modulo 2^64 separately, so their difference is the span's width only because the width is below 2^64, which ir:valid_op/1ir.plvalid_op+OpsemidetOp is an instruction of the IR: one of op_kind/2's, with operands from the sets below where it has them. ensures by bounding Lo and Hi as signed 64-bit offsets.

See rocq.md, Guards and limits and m7.md, round 5.