A live fact liveQ, P, Lo, Hi, Rights, Align is the validator's record that the 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). 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.

• ir.pl: each check-like op adds one in ir:checked_inst_rest/7ir.plchecked_inst_rest/7not documented; ir:evidence_after/3ir.plevidence_after+Inst, +Live₀, -LiveLive are the proofs of Live0 whose evidence still holds after Inst (checked_insts/5). keeps them across an 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 ir:evidence_kill/3ir.plevidence_kill/3not documented drops those naming a redefined name; any other instruction ends them all. Validate.v: fact, evidence_after, kill.

• Its meaning is fact_holds (Evidence.v): Q holds a pointer word, P evaluates to the same word, and the access check of that pointer passes in the current memory. A check reads only regions, so a step that changes no region keeps it.

• 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 facts hold along runs; its live_dom adds that each fact's pointer has a single definition dominating the point, which hullrenew_hull nanofilThe hull of several passed checks of one object is the interval from the least lower end to the greatest upper end of their spans; since an object is one interval, every byte of the hull is in it. renew_hull(Lo, Hi, Rights, Align) of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi. coverage needs.

The subtlety: 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. that dooms its frame leaves a fact that does not hold; the evidence invariant therefore excludes 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. frames.

See rocq.md, The evidence invariant, instruction by instruction.