A 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. is ready in a memory when its own state and that memory agree well enough that its next allocation is freshfresh base nanofilA fresh base is an address where a new object may be placed: positive, aligned, no object's identity (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.. Readiness is the runtime's invariant: the axioms about allocation and 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. are stated only for ready states.

• ready is a parameter of Runtime; ready_state in Machine.v pairs it with the machine's memory. InterpRuntime's says every object lies between 0 and Next, empty if freed, Next is at most 2^48, and nothing at or above Next has been written.

• Every step keeps it (mreachable_ready), from ready_kept, safepoint_ready and fresh_allocation. Where it holds, address_space gives objects_fit and freed_bounds gives freed_empty.

The subtlety: "the run starts ready" is a hypothesis of soundnesssoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps. (valid_no_unchecked), not a lemma. A valid module's data has no size limit, and interp:initial_memory/4interp.plinitial_memory/4not documented lays it out from 65536 whatever its size, so the initial memory need not be ready. The planned fix starts the heap above the module's data.

See runtime-axioms.md, Readiness and rocq.md, An object past 2^64.