An object's identity is its base, the number its capabilitiescapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees. 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.

• Identity.v: ids (every object is still an object) and persists (as it was, or freed). persists_access: a check that passed in m passes again in a memory that persists from m, or traps out of bounds. That is what lets a reusereuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead. form trust an earlier check.

• mreachable_persists: every runrun nanofilA run is the execution of one function of a module from its initial memory, step after step, to an outcome or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too. that starts readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states. persists, from the runtime axioms free_keeps_ids (free reclaims nothing) and fresh allocation, and rooting (a safepoint reclaims nothing the program can name, a lemma from collector_live).

• interp.pl gets it by construction: Next never reuses an address, and free keeps the region.

The subtlety: natively a freed object's address may be a new object's after a collection. Model and native agree on whether each access through a capability the program holds traps, not on its address bits.

See rocq.md, Identities persist and runtime-axioms.md, How the model uses them.