The machine of a runtime R, Machine R, is what one thread's program sees run under R: Semantics.v's stepsstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck., plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs.

mstep_refines ties it to the bare semantics: from a readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states. state each machine step is a step_rel step or a safepoint action, so what is proved of those holds of every run of every runtime.

interp.pl has no counterpart: it is one runtime, built in. ExternalMachine.v extends the machine with labelled external callsexternal 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. without changing it.

The subtlety: the runtime acts before the instruction, so the instruction runs on what the runtime left, as native code runs after its pollcheck.

Defined in Machine.v; see rocq.md, Campaign 3: the machine of a runtime.