A vector's full-width access check: accessK, 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).

Pizlonatedpizlonate nanofilTo pizlonate is to make Fil-C's checks explicit: turn unchecked IR into checked IR, each access becoming a check and a raw access that names its proof, and each pointer operation a flight (after FilPizlonator, Fil-C's LLVM pass; pizlonate:pizlonate_module/2)., it becomes 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). and a touchtouch nanofilA touch uses a vector check's proof without accessing anything: touch(tmp(Q)) follows the check that an access pizlonates to, so the check has its covering use (pizlonate:checked_access/4). It is ir:evidence_preserving/1 and in the core subset: the model steps it as interp.pl does, doing nothing (Semantics.v's inst_step, Touch). of the 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). (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.). Vectors are outside 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 Rocq model has no counterpart, and a function that uses one decodes to IOutside.