A near offset is one within 2^62 of 0. The validator's offsets between pointers (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., pointer distancespointer 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.) 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.

• ir:near_offset/1ir.plnear_offset+Kguard_chain/3's offsets are exact only modulo 2^64 (class l wraps), so a need is counted only for offsets well inside the signed range, where the integer is the true distance: an access at B + 2^64 - 8 is at B - 8, and must not count as reaching past B.; Validate.v's near_offset.

• Readers: 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 (ir:raise_need/6ir.plraise_need/6not documented, and a check_aheadcheck_ahead nanofilcheck_ahead(Lo, Hi, Rights, Align, AHi) is a check of [Lo, Hi) whose own access needs only [Lo, AHi): the bytes [AHi, Hi) are checked early for later accesses through the same base, as filcc's check scheduler does. It may trap earlier than the reference program, but only on runs that would trap later anyway.'s K and K + Lo in ir:ahead_insts/8ir.plahead_insts+RevInsts, +Once, +Ptrs, +After, +AfterNext, -Before, +Js₀, -JsAfter are the facts after the first of RevInsts (the block's last instruction), AfterNext those after the instruction that follows it. and the pass's schedule:widened/5schedule.plwidened/5not documented), 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…), hull coverage (ir:hull_covered/7ir.plhull_covered/7not documented). ir:hull_renewable/8ir.plhull_renewable/8not documented writes the same bound inline.

Why it suffices: with every object below 2^48 (address spaceaddress space nanofilThe address space is where objects may lie: every object within [0, 2^48], native Fil-C's bound (libpas's PAS_ADDRESS_BITS). objects_fit says this of a memory, and the runtime axiom address_space says it of every memory the runtime is ready in; the runtime may also refuse an allocation it cannot hold, and the run traps out_of_memory.), two addresses that are near offsets apart, or a near offset from a point inside an object, cannot wrap past each other, so "at or past" between them means what it says.

The subtlety: bounding only the need was not enough; the check's own start K + Lo must be near too, or it can wrap onto the need's end (rocq.md, A need past 2^64).