uncheckedWhy is the outcome of 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). its capability does not allow, or of a reusereuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead. 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 traptrap Fil-CA trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trap(Reason), terminal and uncatchable. Because nothing follows it, a check is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour., so it refines nothing (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.).

• Why is an access check's reason, or alias, span, half, limit or aheadWhy for the reuse forms.

• Rocq: the outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares. Unchecked and the partial result RUnchecked, made by raw_res. Soundness of checkingsoundness 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. says a valid module's run never reaches it (valid_no_unchecked).