Ghost state exists only in the proof. ownγ a owns the piece a of the ghost location γ, where a belongs to a cameracamera IrisA camera is the kind of resource Iris's propositions are about: a set with a composition ⋅ of two pieces, a validity ✓ saying which compositions are possible, and a step-indexed equality. Owning two pieces is owning their composition. A frame-preserving update a ~~> a' changes a piece to another that stays valid with anything another party could own. Choosing a camera is choosing what can be owned and how it may change.; it is allocated and changed by updatesupdate modality IrisAn update modality says a proposition holds after a change the proof makes on its own, with no program step. The basic update |==> P changes ghost state by frame-preserving updates and allocates new ghost locations. The fancy update |={E1,E2}=> P may also open and close invariants, from the mask E1 of closed invariants to E2; P ={E}=∗ Q is P -∗ |={E}=> Q., 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 interpretationstate interpretation IrisThe state interpretation is the proposition a language instance ties to the machine's real state. The WP 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 ghost heap, which equals the real heap. ties to the real heap.

• nanofil's ghost heap maps pieces, keyed by identityidentity nanofilAn object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object., to an object's region, a byte or an auxaux Fil-CAn object's aux allocation, as large as its payload: where Fil-C keeps the lowers of the pointers stored in the object, slot for slot, while their intvals sit in the object's bytes. The aux word in the object header points at it; it is null for an object no pointer was ever stored into, which the collector then scans as a leaf. A pointer store must *ensure* it exists, which may call the runtime; a pointer load reads it. capability, and the spike's state interpretation, heap_interp, says it agrees with the memory. The planned livelive nanofilA live token, live b, is permission to rely on the object of identity b not being freed. It is the temporal half of a check: the bounds come from b's meta fact, and the free flag passes as long as the token is held. Free consumes it, so whoever frees an object must own it, and an object no one else owns cannot be freed behind the owner's back. For a heap object it is exclusive, or split into fractions for readers; for global data, which is never freed, it is persistent. token is a ghost piece that free consumes; Buffer.v's holds_buffer states the same facts about the real memory, as one non-separating fact.

See How Iris works, Ghost state.