Campaign 3's reuse formsreuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead., part three: renew_ifrenew_if nanofilA renew whose bounds come from a guard: renew_if(Lo, Hi, Rights, Align) of [P, G] is exactly a check of P, but where the span test G passed it natively tests only the flags and alignment, and where G failed it runs the full check out of line. The validator accepts it through ir:guard_covers/5, following P's guard chain (ir:guard_chain/3). and check_limit (formal.md, Campaign 3; rocq.md, Guards and limits).

Both take their evidence from a single definitionsingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. that tested the pointer earlier, not from a checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4).. A renew_if of a pointer P with guard G trusts G, a span testspan_test nanofilspan_test(Lo, Hi) of a pointer P0 is 1 when P0's object contains [P0+Lo, P0+Hi), addresses taken modulo 2^64 and compared unsigned, and 0 otherwise, including for a null, function, external or freed capability. It never traps and reaches no safepoint: it is the guard that --checks=guard puts before a loop. of a pointer N0 (guard_covers/5): where G is nonzero, the span from N0+GLo up to N0+GHi lay inside its object, and P's span lies inside that one at the offset P's 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. gives (guard_chain/3). The interpreter renews then, and a failed access test that is not on a freed object is unchecked(span) (renew_res/4). A check_limit of P with U trusts U, a 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. of N0 whose size is the check's span (limit_covers/5), and P has N0's lower (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., lower_chain/3). The interpreter checks then, and a limit of another capability or another size is unchecked(limit). This file proves neither uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2). outcome happens where the pass accepted the instruction.

Decisions