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 two: 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 over a 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. and 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. (formal.md, Campaign 3; rocq.md, Renew and the half check).

All three reuse 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). that passed earlier. A renew of a pointer P trusts Q1, the 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). of 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. check of a pointer P1 (a renew sourcerenew 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., renew_source_op/6), whose span covers P's at the distance pointer_distance/4 finds. A half check of P trusts the same kind of source for the bound it does not test (half_known/6). A renew over a hull trusts two sources, QL and QH, whose spans bound P's from below and above (hull_renewable/8). The interpreter makes the run 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). where that trust was false: Q1 of another capability (unchecked(alias)), a renew whose access test fails but not because the object was freed (unchecked(span)), or a half check whose one-sided native test disagrees with the whole check (unchecked(half)). This file proves none of them happens where the pass accepted the instruction.

The argument is the same for all three. Q1 is an operand of the instruction, so its single definition dominatesdominance 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. it and replaysreplay nanofilA single definition replays at a point when its name holds what its own instruction's step made, in some earlier frame that agrees with the current one on the instruction's single-definition operands, and the current memory persists from the memory that step left, which lay in the address space. (Single.v): Q1 holds the pointer P1 held when its check passed, and memory persistsidentity nanofilAn object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object. from then, so the object is as it was or freed. P is a known distance from P1, so it has P1'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. (Chain.v). What is left is arithmetic over cap_access_res/7.

Decisions