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. with its single definitionssingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. found through a name mapname map nanofilA name map is a finite map keyed by IR names, the model's counterpart of SWI-Prolog's library(assoc), which ir.pl and cfg.pl use for every table indexed by a label or a temporary: the single-definition map, the evidence indexes, dominator intervals., and the proof that it answers as Validate.v's valid does.

single_definitions asks, for each definition of a function, how many definitions share its name, and answers by walking the list of all of them: time that grows with the square of their number. Three functions of SQLite have 6,000 to 14,800 definitions, and that walk was 7 of the 18 seconds valid took on its module. single_definitions_fast counts every name once, in a name map, and then keeps the definitions whose name counts one.

valid stays the specification: the proofs of the reuse forms read single_definitions, and nothing in them changes. valid_fast is what an extractedextraction nanofilExtraction compiles the Rocq model to OCaml so that it can be run beside the Prolog on the same inputs. judge is the extracted function that reads one run line nanofil printed, runs it in the model, and answers agree, disagree, outside or stuck_both. program runs, and valid_fast_eq says the two are one function. The definitions from stage_sources_fast down to valid_fast repeat Validate.v's with the one name replaced; each equality is proved by unfolding both sides, so a change to one side that the other lacks stops the build here.