Iris's propositions hold or fail at each step index, a budget of program steps still to run, and ▷P ("later P") holds at n + 1 when P holds at n. Stored propositions, in invariants or ghost state, come back only under a ▷, and each program step lets a proof remove one. Löb induction, ▷P → P ⊢ P, proves P while assuming it one step later; loops, recursion and the weakest preconditionweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it. itself are proved or defined that way.

• In nanofil's Iris spike, a safepointpoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1). is a step from a configuration to itself, so the lifting lemma wpc_lift closes it by Löb induction once, and no program proof mentions safepoints. 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). cannot do this, because a safepoint spends none; for blocks, the machine's fuel (OutOfFuel) gives an induction without step-indexing.

• Later credits (Iris 4.0) make the right to remove a ▷ an ownable resource; the spike does not need them.

See How Iris works, The later modality.