The evidence pass is the validator's forward walk over a checked function: it tracks live factslive 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. 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 factsexit facts nanofilA block's exit facts are what a validator pass knows at its jump; its entry facts are what it knows before its phis. Two passes keep them, over the same edge rule: entry facts are the meet over incoming edges, nothing comes over a poll edge, and an edge from a block the pass has not yet reached carries nothing. are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited.

• ir.pl: ir:stage_func/6ir.plstage_func+Stage, +Symbols, +Fn, +Mode, +Params, +BlocksdetFn's blocks are well formed for the module's Stage. A checked function accesses memory only by raw accesses, each covered by a check whose evidence still holds, and polls on every cycle. drives it, with 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…, ir:checked_inst_rest/7ir.plchecked_inst_rest/7not documented and ir:evidence_after/3ir.plevidence_after+Inst, +Live₀, -LiveLive are the proofs of Live0 whose evidence still holds after Inst (checked_insts/5).. Validate.v: evidence_pass, checked_inst_rest, evidence_meet.

• It keeps facts across every ir:evidence_preserving/1ir.plevidence_preserving+InstsemidetInst reaches no safepoint and cannot free an object or change its bounds or rights: pure arithmetic, comparison and conversion, pure pointer construction, a heap check, a scalar raw access (object headers lie outside every object's bounds) and a raw pointer load (aux and box reads, no helper). Calls, alloc, getters, setjmp, va_arg, pointer stores and the res… instruction and drops all of them at any other, but for three: a pointer store taken with its check, a check_local, and a repeated getterrepeated getter nanofilA repeated getter is a call of a getter that another call of the same getter dominates in the same activation: a single-definition let(tmp(D), p, copy, [global(G)]), G defined in this module with local linkage. The first call has returned, so the repeat takes the fast path: no safepoint, no free, no store. The evidence pass lets live facts survive it..

That what it computes holds at run time is 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., proved in Evidence.v, Walk.v, Invariant.v and Persistence.v; the three exceptions above are covered by sparesspares nanofilspares says that at a safepoint just before an instruction the evidence pass keeps facts across, the runtime changes no region. Every runtime meets it, so the generic soundness theorem, once stated under it, no longer takes it as a hypothesis., which every runtime meets (spares_any), so the generic theorem no longer takes it as a hypothesis.

See m7.md, Across edges (round 2) and rocq.md, The evidence invariant over runs.