The state interpretation is the proposition a language instance ties to the machine's real state. The WPweakest 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. receives it before every step and must give it back for the new state, so it is an invariant of every run; a proof never sees the state itself, only what owning fragments and the interpretation together imply. For heap_lang it is the authoritative ghostghost state IrisGhost state exists only in the proof. own γ a owns the piece a of the ghost location γ, where a belongs to a camera; it is allocated and changed by updates, never by the program. It records what the program's memory does not: shares, histories, a protocol's phase, or a whole map that the state interpretation ties to the real heap. heap, which equals the real heap.

• nanofil's Iris spike, heap_interp, interprets a memory and a runtime state as a ghost heap of pieces that agrees with the memory, live objects that do not overlap, and 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. runtime. 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). keeps it with the same ghost heap, from Runtime.v's collector_live, non_moving and aux_round_trip.

See How Iris works, nanofil's machine in Iris.