The 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_hullLo, Hi, Rights, Align of [QL, QH, P] is a 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). whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi.

• Two uses: ir:hull_renewable/8ir.plhull_renewable/8not documented accepts a renew_hull from two renew sourcesrenew 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.; ir:hull_covered/7ir.plhull_covered/7not documented accepts a raw access between the spans of the live factslive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own. of P's object, related by 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.. Validate.v: hull_renewable, hull_covered.

• Proofs: Chain.v's cap_access_hull and hull_access_not_unchecked for accesses; Renew.v's hull_address and hull_renew_access for renews.

• A write needs some span with write rights.

The subtlety: the spans are joined modulo 2^64, and two spans of one object are on the same side of the wrap only if the object is smaller than about 2^63. That is why the 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. (objects_fit) bounds objects by 2^48 rather than 2^64.

See rocq.md, Objects end below 2^48 and forward.md.