Reuse is using earlier evidenceevidence nanofilEvidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is a check immediately before the access, an earlier heap check whose live fact still holds, or a reuse form's trust: for renew a dominating check, for renew_if a guard's span test. instead of a new 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).. --checks=reuse deletes a check whose access an earlier livelive 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. proofproof nanofilA proof is a temporary of class a or f, the result of a check: it holds the checked pointer itself and certifies that the check passed. A raw access names the proof it relies on, so evidence is structural (ir:proof_use/6). 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/2check_reuse.plreuse_checks+M₀, -MdetM is the checked module M0 with each heap check that an available proof covers deleted, and its access reading that proof. Context sites follow the instructions; alias(Q, tmp(Q1), none, Os) records that the access of the deleted proof Q reads Q1., m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: 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)., renew_hullrenew_hull nanofilThe 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_hull(Lo, Hi, Rights, Align) of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi., half_checkhalf_check nanofilhalf_check(Bound, 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 distance from Q1's pointer., 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)., 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. and check_aheadcheck_ahead nanofilcheck_ahead(Lo, Hi, Rights, Align, AHi) is a check of [Lo, Hi) whose own access needs only [Lo, AHi): the bytes [AHi, Hi) are checked early for later accesses through the same base, as filcc's check scheduler does. It may trap earlier than the reference program, but only on runs that would trap later anyway..

• Rocq: reuse of a live fact is Validate.v's reusing_access and Evidence.v's live_access_not_unchecked; Renew.v's reuse_form names the renew, hull and half check. Each form has its own run theorem, assembled in soundnesssoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps..

• The forms read relations between single definitionssingle 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., which is why they rest on dominancedominance nanofilBlock A dominates block B when every path from the entry to B passes through A. The validator decides it with the dominator tree's preorder intervals: each label gets the numbers of its subtree, and A dominates B when B's number lies in A's interval..