The 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/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.).

The Rocq model counts the same way (c_fuel, the outcome OutOfFuel), so both run out at the same point. The theorems quantify over every state a 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. reaches, so fuel plays no part in them. Not to be confused with the extracted driver's gas or with the fuel of Cfg.v's graph walks.