Campaign 3's theorem, valid_no_unchecked: if 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. accepts a module, no runrun nanofilA run is the execution of one function of a module from its initial memory, step after step, to an outcome or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too. of it that starts readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states. ever steps to uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2). (formal.md, Campaign 3; rocq.md, No run is unchecked).

The interpreterinterpreter nanofilThe interpreter is interp.pl, nanofil's executable meaning of the IR: a relation from a module, a function, arguments and fuel to an outcome, with CLP(Z) integers so that it runs in every direction. The Rocq model transcribes it, and the outcome gate checks that the two agree on every run line of the corpus.'s unchecked(Reason) is the outcome a validated module must never reach: it marks 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). or a reuse formreuse 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. the validator accepted but whose justification was false at run time. So the theorem says the validator's checks are sound: every access it lets go unchecked is in fact in bounds, or traps as a checked access would. It rests on the runtime axiomsruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c. of Runtime.v and on the run starting ready; the runtime's safepointspoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1). spare the pass's facts for every runtime (Invariant.v's spares_any), and the interpreter's instance is interp_valid_no_unchecked. The validator here is Validate.v's transcription, which the gates compare with ir:valid_module/1; external calls other than free are stuck in the model, so the theorem says nothing about a run past one. The proof is assembled from the run theorems, one per place an unchecked can come from:

Decisions