A direct call about to run: its blockblock nanofilA block is a labelled straight line of a function: phis, then instructions, then one jump (goto, branch, ret, rets, ret, unreachable). The first block is the entry and has no phis; its label is the name edges use. label, the call's result (where the returned words go), the called global's name, the argument syntax, and the instructions and jump that follow it in the block.

In the global environment ge, the configuration c is at the external call site: its frameframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point. is not doomeddoomed frame nanofilA frame is doomed after a check_ahead whose early bytes failed: the check yields its pointer anyway and the frame records the failure, because the validator promised that the frame will reach an access that fails on those bytes before anything observable happens., its next instruction is a direct call of site's global name, and that name is neither a function of the module (defined or 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 and variadics. A function that uses anything else decodes to IOutside., find_fn), nor global data, nor free. This preserves core dispatch precedence: free remains the runtime's operation. In particular a doomed call cannot use this rule to escape Ahead.

The 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. a call's returned words xs make under the declared return type ty: RetVoid for void, Ret for a scalar, Rets for any tuple; none when void or scalar gets the wrong number of words. The declared shape, not list length, selects the return channel.

Words of the declared return_shape always make an outcome.

The caller's environment e with the words xs a call of the contract spec returned bound as the site's result reads them (returned_env, as call_outcome_result/5); none if the declared return channel and the site's result do not fit.

The configurationframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point. after an external call returns: the same function, locals, callers 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)., with environment e and memory m, at the instruction after the call.

How a call site fails its contract: no contract is registered for the name, an argument does not evaluate, the ABI or the precondition does not hold, or the returned words do not fit the call's result. These are specification failures, not Fil-C trapstrap Fil-CA trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trap(Reason), terminal and uncatchable. Because nothing follows it, a check is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour..

Why the labelled machine stopped: a core 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., a stuck core step with its diagnostic, a process exit with its status from an external call, or a contract violation at the call of symbol.

At an external_site, the core Semantics.step is stuck on the instruction, so no core continuation or allocation can compete with contract dispatch. Runtime safepoints (pollpoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1).) remain.

The labelled machine over any 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. R, with the call relations (E), the evidence invariant (P) and the single definitionsingle 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. invariant (S) instantiated at R.