A pointer's guard chain lists its bases with the offset of its address from each: P itself at i0, 0, then each base B reached through single-definition add, sub and copy flightsflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it. 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 (… (at most 64 steps), offsets from ir:offset_interval/8ir.ploffset_interval+Once, +V, +K, +Depth, -Lo, -Hi, +Memo₀, -Memoas above, with each name's interval (or none) memoised, so an offset whose terms share names (x = x + x, repeated) is walked once per name.. Readers: 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. (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).), pointer distancepointer distance nanofilThe pointer distance from P1 to P is a constant D such that P's address is P1's plus D modulo 2^64, and P has P1's capability. The validator finds it when both pointers reach one exact base on their guard chains: D is the difference of their offsets from it. (ir:pointer_distance/4ir.plpointer_distance+Once, +P, +P₁, -DsemidetP's address is P1's plus D modulo 2^64, with P1's capability, at any point both dominate: both reach one single-definition base B through guard_chain/3 at exact offsets K and K1, and D = K - K1 (the argument of same_pointer/3, which is the case D = 0 modulo 2^64)., ir:same_pointer/3ir.plsame_pointer+Once, +P, +P₁semidetAt any point both P and P1 dominate, they hold the same address and capability: both reach one single-definition base B through guard_chain/3 at point offsets equal modulo 2^64 (P == P1 included). After B's last execution before that point, each definition on either chain ran again, since each dominates it and B dominates each, so both were computed from B's…) through an 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. iK, K, ir:raise_need/6ir.plraise_need/6not documented (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.). Validate.v: guard_chain, pointer_distance.

• Chain.v: guard_chain_sound (each stable element holds of the pointer) and pointer_distance_sound (two pointers D apart share a capability, their addresses D apart modulo 2^64).

The subtlety: offsets are exact only modulo 2^64, so readers that need a true signed distance accept only 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.. A practical one: Chain.v rewrites guard_chain by equations and never unfolds it in a hypothesis, or Qed takes minutes.

See rocq.md, Reading single definitions.