limitSize of a pointer P0 is an opaque class-l snapshot of P0's capability and its object's bounds; check_limit0, 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.

• Validator: 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). asks that U be a single-definition limit of a single-definition P0 and that P reach P0 by a lower chainlower chain nanofilA lower chain from P to B says P carries B's capability: P is B, or a single-definition flight whose lower donor has B's lower, whatever its address.; ir:limit_reads/2ir.pllimit_reads+Fn, +BlocksdetA limit's value is an encoding only check_limit reads (docs/bounds.md): no phi, jump or other instruction reads a name a limit defines, and a check_limit reads one only as its second argument. Throws otherwise. lets nothing but a check_limit read a limit. Validate.v: limit_covers, limit_reads.

• Values: interp.pl's limitCap, Size is WLimit in Values.v. A check_limit whose limit is of another capability is uncheckedlimit (WhyLimit).

• Guard.v: lower_chain_sound gives P the limit's capability, so the instruction checks (run_guard_checked).

Why the snapshot is sound: an object's bounds change only when it is freed, which sets the free flag the check also tests.

See bounds.md and rocq.md, Guards and limits.