A persistent proposition is knowledge rather than ownership: it owns nothing exclusive, so it can be copied, □P giving □P ∗ □P, and kept after it is used. Pure facts ⌜φ⌝, 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., a cell that never changes again (ℓ ↦□ v) and specifications of functions are persistent; ℓ ↦ v is not.
nanofil's 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 persistent: nothing after an allocation changes what was allocated, and Runtime.v never reuses an identity (fresh_allocation, free_keeps_ids), so the fact that b was allocated with n bytes stays true after b is freed. The 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 the part that is not.
See How Iris works, Propositions are resources.