A proof is a temporarytemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR. of class a or f, the result of a 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).: it holds the checked pointer itself and certifies that the check passed. 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). names the proof it relies on, so evidence is structural (ir:proof_use/6ir.plproof_use+Access, +Q, +Lo, +Hi, +Rights, +AlignsemidetAccess, right after the heap check, renew or renew_if that defines Q over [Lo, Hi) with Rights and Align, uses its proof: a heap raw access it covers, or a touch of Q, which accesses nothing (docs/vector-access.md).).

• Rocq: the classes A and F (proof_class); a proof's wordword nanofilA word is the value a temporary holds at run time: an integer, a pointer (an address with its capability), or a limit's opaque snapshot. The temporary's class says how it is read. is the pointer, a WPtr.

• A heap proof is usable only 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, or through 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's rule.