A lower chain from P to B says P carries 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.: P is B, or a single-definition flightflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it. whose lower donor has B's lower, whatever its address.

• ir:lower_chain/3ir.pllower_chain+Once, +P, +BsemidetP has B's lower: P is B, or a single-definition flight whose lower donor has B's lower, whatever its address. At any point that P's definitions dominate, P's lower is B's current one, by round 4's dominance argument (docs/m7.md), since every name on the way has one definition. Once maps each single-definition name to its definition., at most 64 steps; ir:limit_covers/5ir.pllimit_covers+Once, +P, +U, +Lo, +HiU is a single-definition limit(Size) of a single-definition P0 whose lower P has (lower_chain/3), for exactly P's accesses [0, Size) (docs/bounds.md, hoisted checks). uses it to accept a check_limitlimit nanofillimit(Size) of a pointer P0 is an opaque class-l snapshot of P0's capability and its object's bounds; check_limit(0, Size, Rights, Align) of [P, U] is exactly a check of P, whose bounds are tested natively against the snapshot U rather than the object's header (plus the free flag, and read-only for a write). A hoisted limit makes a loop's bounds test cheap.. Validate.v transcribes lower_chain.

• Guard.v's lower_chain_sound: each step is a flight whose capability is its lower donor's, so at any point the chain's definitions dominate, P has B's current capability.

It differs from a 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., which follows only add, sub and copy flights whose lower donor is their address operand, and tracks the offset as well. A lower chain ignores addresses entirely, which is all a limit needs: the snapshot fixes the bounds, so only the identity must match.

See rocq.md, Guards and limits.