Extractionextraction 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. of the model to OCaml: the decoder (decode_module), 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 instance of the semantics, and judge, which the driver (extraction/main.ml) applies to every line nanofiloutcomes prints, and judge_valid, which it applies to rocq/mutants.pl's 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. verdicts (Transport.v). Integers become zarith's, strings OCaml's, and nat OCaml's int: the model's nats count list elements and rounds, and a unary one as large as the fuelfuel nanofilThe interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5). of a big function (before Cfg.v, the square of its block count, a million for Lua's luaV_execute) overflowed the stack.