An object is one allocation a capabilitycapability 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. 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, regionBase, End, Kind, Life: its bounds [Base, End), its kind (stack, heap or global data) and whether it is live or freed.

• interp.pl keeps the regions in memBytes, Regions, Next, Aux; Memory.v has region with kind and life, listed in mem's m_regions. Next is not part of the model's memory: the runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c. keeps it.

• Only an ending changes a region: End becomes Base and Life becomes freed. Free does this to a live heap object (lifetime_step); the end of an invocation does it to its locals (region_step). Bytes and stored capabilities stay where they were.

• An object is what object_region (interp:object_region/3interp.plobject_region+Base, +Rs, -Regioncapabilities refer to registered identities. An injected unknown base is outside the interpreter domain, not authority for the live object that happens to contain its address.) finds for a base: the first region with that base. A later region of the same 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. is no object, and the proofs (fresh, persists, objects_fit) speak of objects only this way.

The subtlety: a live zero-sized object also has End = Base, so empty bounds do not mean freed. Only the converse holds, freed implies empty (freed_empty), and freed_bounds asks it of every 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. memory.

Defined in Memory.v and interp.pl's Memory section.