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). is covered by a check when it lies inside the checked bytes, at an alignment the check's implies, with rightsrights Fil-CRights are what an access asks of a capability: read or write, where write allows reading too. Every check, renew and raw access names the rights it needs. the check allows. Its own access check, which the raw access makes again without trapping, then passes too.

• ir:covered_access/6ir.plcovered_access+Access, +Q, +Lo, +Hi, +Rights, +AlignsemidetAccess is a raw access at tmp(Q) within [Q+Lo, Q+Hi), as aligned as it must be, and Rights allow it (write allows reading too)., from ir:raw_access/5ir.plraw_access?Inst, ?Q, ?X, ?Off, ?RightsInst is a raw load of type X or store of width X at tmp(Q)+Off, needing Rights., ir:access_size_align/3ir.placcess_size_align?X, ?Size, ?AlignnondetA load of type X or a store of width X accesses Size bytes, and Fil-C requires its address to be Align-aligned: 8 for a pointer, whose capability lives in the aux word of its 8-byte slot, else 1. and ir:rights_allow/2ir.plrights_allow/2not documented; Validate.v's covered_access.

• Coverage.v's coverage lemma: cap_access_covered (a passed check passes for every covered part), covered_access_checked, access_ok_not_unchecked, and covered_access_not_unchecked: a covered raw access gives no 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)..

The subtlety: addresses wrap modulo 2^64 (raw_address, interp:raw_address/3interp.plraw_address+A, +Off, -BB is the address A plus the constant Off.) while bounds are unbounded integers, so the lemma needs the address spaceaddress space nanofilThe address space is where objects may lie: every object within [0, 2^48], native Fil-C's bound (libpas's PAS_ADDRESS_BITS). objects_fit says this of a memory, and the runtime axiom address_space says it of every memory the runtime is ready in; the runtime may also refuse an allocation it cannot hold, and the run traps out_of_memory. (objects_fit): an object ending past 2^64 would let a covered access wrap to address 0. The lemma also assumes the check passes in the memory the access runs in; that it still does 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.'s job.

"Coverage" also means, in Campaign 4, native coverage of a contract: that real calls stay within it. That is unrelated.

See rocq.md, The coverage lemma.