An exact base of a pointer P is a single-definitionsingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. name B on 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. whose offset interval is one point, B−iK, K: P's address is B's plus exactly K, modulo 2^64, with B's capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees..

• ir.pl has no predicate for 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… and ir:raise_need/6ir.plraise_need/6not documented each select chain elements with iK, K whose name is in Once. Validate.v names it exact_base.

• Readers: 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. (two pointers with a common exact base), and the 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. analysis, which raises the need of each exact base of an accessed pointer.

The subtlety: a base reached through a variable offset is on the chain with a wider interval and serves 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).'s guard, but not these readers; and K is exact only modulo 2^64, so readers comparing positions also ask K to be a near offsetnear 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..

See schedule.md, Validator rule.