An access check: checkLo, Hi, Rights, Align of a pointer P traps unless P's capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees. permits 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. on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a 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). 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/2ir.plop_kind?Op, ?KindnondetKind is the category of Op that its consumers dispatch on, so that each can case-split on Kind in clause heads. Deterministic in mode (+, -): one fact per op, indexed on the first argument., pizlonate:checked_access/4pizlonate.plchecked_access+Access, ?Q, -Insts, ?Insts₁semidetInsts less Insts1 are Access's check, defining tmp(Q), and its raw access: the table in this module's header, one clause per row. Fails for an instruction that is not an access.).

• Rocq: the ops Check, CheckLocal and CheckFunction in Syntax.v; the test itself is cap_access_res (interp:cap_access_res/7interp.plcap_access_res/7not documented).

• A check is followed at once by the access it covers (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.); later accesses may reuse it while its live factlive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof 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. holds, and the 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. forms trust it longer.

Upstream FilPizlonator schedules bounds checks and removes redundant ones; nanofil's 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. forms and 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. are its versions, each accepted only by the validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked..

Because 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. is terminal, a check is a pure assertion: one proved never to fail can be deleted.