A 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 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). left. A frame is one invocation: its function, its temporariestemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR., its named locals, whether it is 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., and its point.

• Semantics.v: config with c_frame, c_callers, c_mem, c_fuel; frame with fr_fn, fr_env, fr_locals, fr_doomed, fr_at.

• A frame's point is Snapshot (a variadic callee about to snapshot its arguments, an allocation), Enter (about to run block l, entered from a predecessor or none), or Exec (inside block l with instructions left, then a jump).

• interp.pl has no such term: it is big-step, so the frame is its ctx... term and Env, the callers are Prolog's own stack, and memory and fuel are sMem, Fuel. The model makes them explicit so that Campaign 3's invariants can be stated between any two 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..

The subtlety: the proofs speak of every frame, not only the running one. The single-definition invariantsingle 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. holds in each waiting callerparked nanofilA waiting caller is a frame suspended at a call until its callee returns; the configuration keeps them in c_callers, each with how it will read the result (pending). interp.pl has none: its callers wait on Prolog's own stack. too, and a waiting caller is never doomed.

Defined in Semantics.v; see rocq.md, Decisions.