The evidence invariant says that along every run, at the running frame's point, the 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. 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: each fact's check passes in the current memory, and its 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. dominating the point. It is how the pass's static bookkeeping becomes a fact about runs.

• One step at a time (Evidence.v): fact_holds is a fact's meaning; checked_inst_holds keeps the facts across every case of ir:checked_inst_rest/7ir.plchecked_inst_rest/7not documented, entry_holds across an unpolled edge into the meet of exit 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..

• The pass read back (Walk.v): pass_fold, walks, and relies, the instructions before which it keeps facts.

• Stated (Invariant.v): at_pos, point_ok, frame_ok, live_dom, and inv: the running frame is point_ok unless doomeddoomed frame nanofilA frame is doomed after a check_ahead whose early bytes failed: the check yields its pointer anyway and the frame records the failure, because the validator promised that the frame will reach an access that fails on those bytes before anything observable happens., every waiting caller parkedparked nanofilA waiting caller is a frame suspended at a call until its callee returns; the configuration keeps them in c_callers, each with how it will read the result (pending). interp.pl has none: its callers wait on Prolog's own stack..

• Over runs (Persistence.v): mstep_inv; run_access_not_unchecked, over every runtime; the safepoint case uses 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., a lemma for every runtime (spares_any).

The subtlety: a back edge without a poll carries no facts (the pass had not reached its source), so nothing needs justifying there; a doomed frame claims nothing.

See rocq.md, The evidence invariant over runs.