The two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every 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)., every 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). and the 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). it uses, so 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. can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2ir.plmodule_stage+M, -StagedetStage is checked when M uses any word of the checked stage (a check, renew, span test, raw access, flight or a poll edge), else unchecked. Like the mode, the stage is read off the vocabulary, never stated.).

Pizlonationpizlonate 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). turns unchecked IR into checked. The Rocq model covers checked filc-mode IR only: module_checked reads the stage, and stage_func is the checked part of the validator, the evidence passevidence pass nanofilThe evidence pass is the validator's forward walk over a checked function: it tracks live facts and accepts each raw access only where its own check, a live fact or a reuse rule covers it. It visits the blocks once, in order; a block's entry facts are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited. and its companions.