Campaign 3's run-level 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. invariant, stated (docs/rocq.md, The evidence invariant over runs): what holds at each point of a frameframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point. of Machine R (Machine.v), and the lemmas each kind of step needs. Persistence.v proves that every step keeps it.

The invariant (inv) says that the running frame, unless a 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. doomed it, is at a point where the facts the evidence passevidence pass nanofilThe evidence pass is the validator's forward walk over a checked function: it tracks live facts and accepts each raw access only where its own check, a live fact or a reuse rule covers it. It visits the blocks once, in order; a block's entry facts are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited. computed for that point hold (point_ok), and that every waiting caller has no fact (parked). It also says that each live fact's pointer has 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. 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. 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 (live_dom), so that 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 may read that pointer's definition.