The validator decides whether a module is well formed and, in checked IRchecked IR nanofilThe 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 check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2)., 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 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)..

• Prolog: ir:valid_module/1ir.plvalid_module+MsemidetM is a well-formed module. When it is not, throws nanofil_error(Message) describing the first problem found, so callers get a diagnostic rather than a silent failure. A few terms outside the grammar (an item, instruction or jump of no known shape) make it fail instead., which throws at the first problem; the checked part is ir:stage_func/6ir.plstage_func+Stage, +Symbols, +Fn, +Mode, +Params, +BlocksdetFn's blocks are well formed for the module's Stage. A checked function accesses memory only by raw accesses, each covered by a check whose evidence still holds, and polls on every cycle. (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., ir:limit_reads/2ir.pllimit_reads+Fn, +BlocksdetA limit's value is an encoding only check_limit reads (docs/bounds.md): no phi, jump or other instruction reads a name a limit defines, and a check_limit reads one only as its second argument. Throws otherwise., ir:polls_every_cycle/1ir.plpolls_every_cycle+BlockssemidetEvery cycle of the control-flow graph of Blocks, unreachable blocks included, has a poll edge: without them the graph is acyclic. A call does not count, since the callee need not poll. Depth-first search, with each label gray while on the path and done after.).

• Rocq: valid in Validate.v, with valid_func, valid_data and valid_alias. It returns false where ir.pl throws, so it follows ir.pl's clause groups, not its order of evaluation. valid_no_unchecked is the theorem, soundness of checkingsoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps..

The subtlety: the theorem is about Validate.v's transcription, not ir.pl. What ties the two is the mutantmutant nanofilA mutant is a checked module with one item changed, inserted or deleted: a check deleted or moved, its bounds, rights or alignment changed, a raw access's offset moved by one, a free inserted between evidence and its use, a reuse form given another proof, a poll edge removed, or a data object's or alias's linkage, target or name changed. Prolog's and Rocq's validators judge each, and must agree. gate, comparing verdicts on every mutant of the corpus, not a proof. Three places where ir.pl's answer depends on Prolog's evaluation (the offset intervaloffset interval nanofilAn offset interval bounds the values an integer name can hold, derived through its single definitions, so that a flight's offset from its base is known to lie in [Lo, Hi]. At class w it bounds the signed word itself; at l it bounds some integer congruent to the value modulo 2^64, which is all address arithmetic needs. memo, a cut in ir:pointer_distance/4ir.plpointer_distance+Once, +P, +P₁, -DsemidetP's address is P1's plus D modulo 2^64, with P1's capability, at any point both dominate: both reach one single-definition base B through guard_chain/3 at exact offsets K and K1, and D = K - K1 (the argument of same_pointer/3, which is the case D = 0 modulo 2^64)., ir:op_interval/9ir.plop_interval/9not documented's commits) are copied deliberately.

See rocq.md, The validator and its gate and rocq.md, No run is unchecked.