Nanofil's machinemachine nanofilThe machine of a runtime R, MachineR, 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., with the 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. of a contract registry, as an Iris language whose evaluation context is the stack of callers, and Iris adequacyadequacy nanofilAdequacy is the one theorem that ties a program logic to the machine: if a program's proof in the logic can be derived, then no state any of its runs reaches fails. It is proved once; after it, proving a program never panics is deriving its proof, with no reasoning about runs. as a proof of never_panics and of the labelled machine's safety.

The first logic spike's IrisLang.v made the whole configuration one expression, so a call was just another step and a function could have no specification of its own. Here the callers are Iris's evaluation context, so a call is wp_bind and a function's specification is an ordinary Hoare triple that hands resources back to its caller:

• an expression is a running 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. (ERun), 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. an invocation returned (EEnd, the value), an expression running as the callee of a suspended caller frame (EWait), or the bad return of an external call (EBad); the one context item KWait is that caller;
• the Iris state is the memory, the 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.'s state, the 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). and the world of libc state the contracts speak of: the machine has one fuel counter for the whole stack, so it belongs to the state, not to a frame;
• a head step of ERunfr is the stepstep 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. of fr with no caller. step_callers shows that the callers are passive: they change only what a return does, which becomes hs_return (the value) and then hs_resume (the caller reads it);
• an ending that is neither a failure nor a return (running out of fuel, a refusal trap) and an allocation the runtime refuses are stalls: ERunfr steps to itself. The machine has stopped without failing, and to Iris that is a run that never ends, which is safe. A failing frame has no head step at all, not even a safepoint.

The language is over a world type and a contract registry, the labelled machine's (ExternalMachine.v). A call at an external_site is stuck to the core step; here it is:

• admissible (a contract, arguments that evaluate, its ABI and its precondition): it may return (hs_call_return, the frame resumed with the call's memory, runtime state and world), and it may also stall (hs_call_wait). The stall stands for everything the call does that is not a return: it may block, it may exit the process or end for lack of resources (the labelled machine stops there without failing), and the labelled machine makes no step where an admissible call has no completed invocation. None of these is a failure, and to Iris each is a run that never ends, so a stall is safe; and it makes an admissible call always reducible, whether or not the contract allows any return;
• returning words the call site cannot take (hs_call_bad): the expression becomes EBad, which is no value and has no step, so adequacy rules it out;
• rejected: no head step, so adequacy rules it out too.

With the empty registry (no_contracts) no call is admissible and the language is the core machine's.

run_reducible, admissible_reducible and head_step_run_inv say a frame that does not fail, or whose external call is admissible, is always head-reducible, and how. wp_never_panics proves Panics.v's never_panics from a NotStuck weakest precondition of the entry's ERun in the language with no contracts, for every fuel; adequate_labelled and wp_labelled_safe prove that no labelled runrun nanofilA run is the execution of one function of a module from its initial memory, step after step, to an outcome or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too. stops with a failure_ending, and that a returned value satisfies the postcondition.