A 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.
Common ones: Excl (exclusive), fractions (shares in (0, 1]), Agree (a value that never changes), and the authoritative camera (● the whole, ◯ fragments of it), on which Iris's heap, gen_heap, is built.
The step-indexed equality is what lets ghost state hold propositions (higher-order ghost state), the basis of 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..
nanofil's ghost heap in the spike is a gen_heap from 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 values; a planned metameta nanofilA meta fact, meta b n k, says that the object of identity b was allocated with extent n bytes and kind k (heap, global data, stack). It is the persistent half of owning an object in the planned program logic: once true it stays true, so it can be copied and shared freely, because nothing after an allocation changes what was allocated. With the pointer's offset from b it decides a check's bounds by arithmetic alone; whether the object is still there is the live token's part. fact is a persistent ghost_map element, stable because Runtime.v never reuses an identity (fresh_allocation, free_keeps_ids).