A step moves a 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. on by one thing: entering a block (its phis, one unit of 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).), one instruction, or one jump. step answers Next with the next configuration, Done with 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., Fresh for an allocation that waits for a base, or Stuck.

• Semantics.v: step for the configuration, reading the global environmentglobal environment nanofilThe global environment is what every step of a run reads but never changes: the module, each global's pointer, and the free that a call of libc's free runs., inst_step for one instruction, step_rel the relation (any freshfresh base nanofilA fresh base is an address where a new object may be placed: positive, aligned, no object's identity (live or freed), overlapping no object's bounds, ending at or below 2^64, and reading as zero with no stored capability, as Fil-C's allocations do. base for an allocation), reachable its closure.

• It transcribes interp.pl's big-step 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.: interp:block_outcome/7interp.plblock_outcome+Ctx, +Label, +Pred, +Env₀, +S₀, -Out, -SnondetOut and S are the outcome and final state of running the block Label, entered from Pred (from(L) or entry), and everything after it. Each block costs one unit of fuel., interp:insts_result/5interp.plinsts_result+Insts, +Ctx, +Env₀, +S₀, -ResultnondetResult is cont(Env, S) when every instruction ran, or stop(Outcome, S) when one ended the run., interp:inst_result/5interp.plinst_result+Inst, +Ctx, +Env₀, +S₀, -ResultnondetResult is cont(Env, S) after Inst, or stop(Outcome, S) when it ends the run., interp:edge_outcome/7interp.pledge_outcome/7not documented. Small-step was formal.md's decision, so that invariants can be stated between any two steps.

• Stuck is where the interpreter throws or fails: an external callexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings. other than free, an access through an external capability, a temporary read before it is assigned, code 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.. step_rel has no step there.

The machinemachine nanofilThe machine of a runtime R, Machine R, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs. adds the runtime's steps, allocation and safepoint, on top of these.

Defined in Semantics.v.