A meta fact, meta b n k, says that the object of 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. 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 checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4).'s bounds by arithmetic alone; whether the object is still there is 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's part.

• It is ghost state: after a free the regionregion Fil-CAn object is one allocation a capability can name, its bytes what upstream calls the payload: a heap object, a named local, a data item or a variadic argument snapshot. A region is the model's record of it, region(Base, End, Kind, Life): its bounds [Base, End), its kind (stack, heap or global data) and whether it is live or freed.'s bounds are empty, but the meta fact still says what the object was. Runtime.v makes it stable: an identity is never reused (fresh_allocation), free keeps every identity (free_keeps_ids), and nothing else changes a region's bounds (free_lifetime, safepoint_lifetime).

• In Iris it would be a persistentpersistent proposition IrisA 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 ⌜φ⌝, invariants, a cell that never changes again (ℓ ↦□ v) and specifications of functions are persistent; ℓ ↦ v is not. ghost_map element, b ↪□ (n, k), which anyone may copy.

• Buffer.v's holds_buffer contains it for the buffer, written as the region's equation: meta b 32 Heap and live b in one fact.

See logic.md, The proposal in one paragraph.