A raw access is a checked-stage memory access that does no checking of its own and names 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). that covers it: raw_load, raw_store, raw_load_pointer, raw_store_pointer, raw_cas and raw_call (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).).

• Rocq: the ops RawLoad and RawLoadPointer, the instructions RawStore, RawStorePointer and RawCall; raw_access transcribes 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..

• At run time it makes its access check again without trapping: where that check would fail the run is 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). (interp:raw_res/2interp.plraw_res+Res₀, -ResdetA raw access is the access its check covers, made again without trapping: what would have trapped is unchecked., raw_res). Coveragecovered access nanofilA raw access is covered by a check when it lies inside the checked bytes, at an alignment the check's implies, with rights the check allows. Its own access check, which the raw access makes again without trapping, then passes too. and soundnesssoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps. show a valid module never gets there.