Campaign 3's single-definition invariantsingle 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. over runs (docs/formal.md, Campaign 3; docs/rocq.md, The single-definition invariant).

The reusereuse 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. forms' rules read relations between the values of names that have one definition each: a 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. and its base, a 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). and the pointer it checked, 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. or 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. and the pointer it read. Such a relation holds at a point of a run only where the name's 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. the point, and only while the definition's operands hold the values it read. This file states that for every frame of every run (sinv), and proves that every machine step keeps it (mreachable_sinv).

At a frame's point, each single definition whose sitesite nanofilA site is where a temporary is defined: param for a parameter, or at(L, I) for index I of block L, with phis at index -1. A site dominates a position when it comes before it on every path from the entry: the same block at an earlier index, or a block that strictly dominates it. dominates the point 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. (replays): the name holds what its instruction made in some earlier frame and memory, that frame agrees with the current environment on the instruction's single-definition operands, and the current 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 the memory the instruction left (Identity.v), which lay in the address space. A check that passed then passes again or traps; a flight's capability is its lower donor's.

Decisions