Extraction 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.

• Extract.v and rocq/extraction/main.ml, a reader of Prolog terms; judge and judge_valid are in Transport.v. rocq/agree.sh pipes nanofil outcomes through judge; rocq/valid.sh pipes 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 through judge_valid.

• The model runs as Driver InterpRuntime (Driver, InterpRuntime), so Print Assumptions of judge is closed: no axiom of the runtimeruntime 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. module type is left open.

• A disagreement is presumed the model's fault; none has been found.

The subtlety: nat extracts to OCaml's int and integers to zarith's. A unary nat as large as a big function's fuel overflowed the stack, and a positive-keyed map walked keys bit by bit, so the model's types were chosen for the extracted code.

See rocq.md, The full outcome gate and Extract.v.