A fresh base is an address where a new object may be placed: positive, aligned, no object's 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. (live or freed), overlapping no object's bounds, ending at or below 2^64, and reading as zero with no stored capability, as Fil-C's allocations do.

• fresh in Memory.v, for an allocation request alloc_req. Semantics.v's step answers Fresh at an allocation, and step_rel takes any fresh base, so the semantics never depends on where objects go.

• Every 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.'s alloc must choose one (fresh_allocation); the address spaceaddress space nanofilThe address space is where objects may lie: every object within [0, 2^48], native Fil-C's bound (libpas's PAS_ADDRESS_BITS). objects_fit says this of a memory, and the runtime axiom address_space says it of every memory the runtime is ready in; the runtime may also refuse an allocation it cannot hold, and the run traps out_of_memory. (address_space) then bounds the end by 2^48.

• interp.pl's allocator, interp:alloc_base/6interp.plalloc_base+Mode, +Mem₀, +Align, +Size, -Base, -MemsemidetBase is a new region of Size bytes in Mem. Allocations are aligned (Fil-C's to at least 16, as filc_allocate_with_alignment aligns them), with Fil-C bounds rounded to 16 as prepare_allocate_object does (zero stays zero). A 16-byte gap separates distinct, never-reused identities. Fails when Next would pass the end of the address space (address_space/2): the r…, takes the next aligned address from 2^32 (interp:stack_base/1interp.plstack_base/1not documented) and only adds. That is one fresh choice; nothing may rely on it.

The subtlety: fresh is stated over objects as object_region finds them, not over every region in the list, so 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. and fresh follow from each other without a lemma about the list's shape.

See rocq.md, Campaign 3: the machine of a runtime.