A touch uses a vector check's 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). without accessing anything: touchtmpQ follows the 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). that an accessaccess nanofilA vector's full-width access check: access(K, Addr, Size, Align) traps as a K (read or write) access of Size bytes at Addr with alignment Align would, and moves no data. It comes before the vector's 8-byte chunks, so the vector traps as one access (vector-access.md). pizlonates to, so the check has its covering use (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.). It is ir:evidence_preserving/1ir.plevidence_preserving+InstsemidetInst reaches no safepoint and cannot free an object or change its bounds or rights: pure arithmetic, comparison and conversion, pure pointer construction, a heap check, a scalar raw access (object headers lie outside every object's bounds) and a raw pointer load (aux and box reads, no helper). Calls, alloc, getters, setjmp, va_arg, pointer stores and the res… and in the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside.: the model steps it as interp.pl does, doing nothing (Semantics.v's inst_step, Touch).