half_checkBound, 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 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. from Q1's pointer.

• Validator: 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…, its offsets nearnear 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.; Q1 is a renew sourcerenew source nanofilA renew source is an earlier proof that a reuse form trusts for bounds: a single-definition proof Q1 of a single-definition pointer P1, made by a check, check_ahead, renew_if, check_limit or half_check, recorded with its range and alignment.. interp.pl: interp:half_bound/6interp.plhalf_bound/6not documented is the native test and interp:half_res/4interp.plhalf_res/4not documented the result; where the native test disagrees with the whole check the run is uncheckedhalf.

• Rocq: half_known, half_bound, half_res transcribe them; Renew.v proves half_bound_agrees and half_access, and along runs run_reuse_checked.

The subtlety: a lower half check reads its address signed and fails on any freed object, where the whole check fails only outside the bounds. The two agree only because objects start at or above 0 (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.) and a freed object's bounds are empty (freed_bounds); both were added to the runtime's statements for this proof.

See half.md and rocq.md, Renew and the half check.