An 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 stateghost 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. by frame-preserving updates and allocates new ghost locations. The fancy update E1|⇛E2 P may also open and close invariantsIris invariant IrisAn Iris invariant inv N P says that P holds, of resources no one owns, between every two steps of the program. It is persistent, so every thread may know it; a thread opens it for one atomic step, takes P out under a later, and puts P back before the step ends. Masks record which invariants are open, so none opens twice at once. Since Iris 3 it is defined in the logic from ghost state and fancy updates., from the mask E1 of closed invariants to E2; P ⇛E Q is P −∗ |⇛E Q.

• In nanofil's Iris spike, an allocation's step gives the new object's pieces by a basic update (gen_heap's allocation) after the runtime picks a freshfresh base nanofilA fresh base is an address where a new object may be placed: positive, aligned, no object's identity (live or freed), overlapping no object's bounds, ending at or below 2^64, and reading as zero with no stored capability, as Fil-C's allocations do. base (fresh_allocation), and a store changes the stored pieces' values by another.

See How Iris works, Update modalities.