The interpreter is interp.pl, nanofil's executable meaning of the IR: a relation from a module, a function, arguments and 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). to an 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., 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.

• Entry points: 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., or interp:module_prepared/2interp.plmodule_prepared+M, -PrepareddetPrepared is M ready to run: its mode, the address of each global, its initial memory, and its functions and their blocks indexed by name and label. The initial memory holds integers only, so runs can share it. once and interp:run_prepared/5interp.plrun_prepared+Prepared, +Fn, ?Args, +Fuel, ?OutcomenondetOutcome is the result of calling Fn of the prepared module on Args within Fuel blocks. Args is constrained to the ranges of Fn's parameter classes. Where a branch or a division depends on an unknown value (an argument, or a byte nobody wrote), there is one solution per case, each constraining that value; comparisons are reified instead. When every such value… many times. The tests also compare it with the native code nanofil and clang emit (difftest, progtest).

• Rocq: Semantics.v transcribes its steps, small-step where interp.pl is big-step; Run.v's Driver InterpRuntime (Driver, InterpRuntime) runs them with the interpreter's allocator and free. "The interpreter's runtime" means InterpRuntime, which proves every 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. axiom.

The subtlety: it is the deterministic explicit-free subset, not a GC simulator: no reclamation, no concurrent or signal-handler frees, no free singleton. It has been both more permissive than native (an object past 2^64, now refused) and stricter (a freed snapshot's renew, now a trap); each was fixed toward native.

See guide.md, 13. Running it and interp.pl's header.