Evidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is 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). immediately before the access, an earlier heap check whose live factlive 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. still holds, or a 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. form's trust: for 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). a dominating check, for 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). a guardguard nanofilRange guards, --checks=guard: a span test before a loop proves its accesses' bounds once, and the loop's checks become renew_if, which tests only the flags and alignment when the guard passed and runs the full check out of line otherwise (check_reuse:guard_checks/2, m7.md, Range guards (round 5)).'s 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..

• The validator's fact for it is liveQ, P, Lo, Hi, Rights, Align (ir:checked_insts/5ir.plchecked_insts+Insts, +Fn, +Mode, +Live, -LiveOutdetEach check in Insts is followed by an access it covers, its first use, so no safepoint can come between them; no other instruction accesses memory unchecked. Live are the heap proofs live(Q, P, Lo, Hi, Rights, Align) whose evidence still holds (docs/m7.md): a later scalar raw access may read one that covers it. An instruction that is not evidence_preservin…); Rocq's is fact, with its meaning fact_holds.

• 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. tracks it, and the evidence invariantevidence invariant nanofilThe evidence invariant says that along every run, at the running frame's point, the live facts the evidence pass computed for that point hold: each fact's check passes in the current memory, and its pointer has a single definition dominating the point. It is how the pass's static bookkeeping becomes a fact about runs. proves it true along runs.

campaign.md separates requirement, evidence and implementation: an optimizer may choose cheaper evidence, never weaker.