Campaign 3's coverage lemma (docs/formal.md, Campaign 3; docs/rocq.md, The coverage lemma): a raw accessraw access nanofilA raw access is a checked-stage memory access that does no checking of its own and names the proof that covers it: raw_load, raw_store, raw_load_pointer, raw_store_pointer, raw_cas and raw_call (ir:covered_access/6). that a passed 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). covers, as ir.pl's covered_access/6 says, does not give uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2)..

A check let(Q, a, check(Lo, Hi, Rights, Align), [P]) is the accessaccess nanofilA vector's full-width access check: access(K, Addr, Size, Align) traps as a K (read or write) access of Size bytes at Addr with alignment Align would, and moves no data. It comes before the vector's 8-byte chunks, so the vector traps as one access (vector-access.md). check of the bytes from P+Lo up to P+Hi with Rights and Align, and when it passes it yields P itself. A raw access that uses Q afterwards reads or writes Size bytes at Q+Off with no check of its own: the model makes its access check again, and where that would trap the run is unchecked (raw_res/2). covered_access/6 asks that the access lie inside the checked bytes, at an alignment the check's implies, with rights the check's allow. This file proves that this is enough: the access's own check then passes (covered_access_not_unchecked). It is arithmetic over cap_access_res/7.

An address is a sum modulo 2^64 (raw_address/3), while the model's bounds are unbounded integers, so the lemma also needs every object to end inside the address space (objects_fit). The runtime's address_space axiom gives that in every state of a run that starts readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states. (Machine.v's mreachable_objects_fit; docs/rocq.md, An object past 2^64). That the check passes in the memory the access runs in, not only when it ran, is the 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's to show (Evidence.v, Persistence.v).