The 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 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.. The validator finds it when both pointers reach one 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. on their guard chainsguard 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.: 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… is the case D = 0 modulo 2^64. Validate.v transcribes pointer_distance, including ir.pl's cut: both take the first base of P's chain that P1's chain shares.

• Readers: 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)., half_checkhalf_check nanofilhalf_check(Bound, Lo, Hi, Rights, Align) of [Q1, P] is exactly a check of [Lo, Hi) at P that natively tests only one bound, upper or lower; the other end is known from Q1's earlier check of the same object, P being at a known distance from Q1's pointer. (ir:half_known/6ir.plhalf_known+Bound, +Lo, +Hi, +D₀, +Lo₁, +Hi₁semidetA check of [Lo, Hi) at P, where P is P1 + D0 modulo 2^64 with P1's capability, may test only Bound when a passed check of [Lo1, Hi1) at P1 proves the other end (docs/half.md). D is D0 taken signed modulo 2^64. upper: P+Lo is E = D + Lo - Lo1 >= 0 bytes above P1+Lo1, which was at or above lower, and with E =< 2^62 that sum cannot wrap, as P1+Lo1 is a user add…), renew_hullrenew_hull nanofilThe hull of several passed checks of one object is the interval from the least lower end to the greatest upper end of their spans; since an object is one interval, every byte of the hull is in it. renew_hull(Lo, Hi, Rights, Align) of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi. (ir:hull_renewable/8ir.plhull_renewable/8not documented) and hull coverage (ir:hull_covered/7ir.plhull_covered/7not documented).

• Chain.v's pointer_distance_sound makes it true at run time where the names dominate the point; Renew.v's distance_pointer shows P then reads as a pointer, which excludes uncheckedalias.

The subtlety: D is a difference modulo 2^64, so a reader that needs a true signed distance asks it 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. too.

See schedule.md, Checked-IR evidence and rocq.md, Reading single definitions.