Transport is the crossing between Prolog terms and the model: decoding a checked module that nanofil printed into Syntax.v's syntax, and encoding the model's outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares. back as the term interp:run/5interp.plrun+M, +Fn, ?Args, +Fuel, ?OutcomenondetOutcome is the result of calling the function Fn of module M on Args and executing at most Fuel blocks. With unknown Args each solution constrains them to the inputs that take one path; see run_prepared/5. would give, so that the two can be compared with ==.

• main:outcomes/3main.ploutcomes+Opt, +Checks, +FiledetPrints, as Prolog terms, the checked module of the Fil-C IR File (after the middle end when Opt is o1, and the check passes Checks) and then, for each run line, outcome(Fn, Args, Fuel, Outcome), the interpreter's outcome on that module, or error(Fn, Args, Fuel, E) when the run throws E or finds no outcome. An independent model of the checked IR (rocq/, docs/… (nanofil outcomes FILE) prints the module and each run line. Transport.v decodes with decode_module and its helpers (dinst, dfunc, ...) and encodes with eoutcome, ereason, eword and ecap.

• Both sides are Term.v's term: an integer, an atom, a compound or a proper list, as ground Prolog terms are.

• Decoding is partial on purpose: a function outside the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside. becomes IOutside, a data item the interpreter does not lay out ItemOther, an unknown linkage LOther, each keeping its term.

judge and judge_valid are built on it; see 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..

Defined in Transport.v.