The 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 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. axiom address_space says it of every memory the runtime is 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. in; the runtime may also refuse an allocation it cannot hold, and the run traps out_of_memory.

• Runtime.v: objects_fit, address_space; Machine.v's mreachable_objects_fit gives it in every state of a run that starts ready. interp.pl: interp:address_space/2interp.pladdress_space+Mode, +NextNext is within the address space. Fil-C's objects lie below 2^48, libpas's address space (PAS_ADDRESS_BITS), so an address never wraps inside one, and two addresses of one object are less than 2^63 apart (the Rocq model's objects_fit). Plain mode sets no limit., where Next stops at 2^48.

• What it buys: a covered accesscovered access nanofilA raw access is covered by a check when it lies inside the checked bytes, at an alignment the check's implies, with rights the check allows. Its own access check, which the raw access makes again without trapping, then passes too. cannot wrap (needs only 2^64); two addresses of one object are less than 2^63 apart, so a hullrenew_hull nanofilThe hull of several passed checks of one object is the interval from the least lower end to the greatest upper end of their spans; since an object is one interval, every byte of the hull is in it. renew_hull(Lo, Hi, Rights, Align) of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi. of spans does not straddle the wrap; an address that wrapped below 0, read signed, fails a lower half_checkhalf_check nanofilhalf_check(Bound, Lo, Hi, Rights, Align) of [Q1, P] is exactly a check of [Lo, Hi) at P that natively tests only one bound, upper or lower; the other end is known from Q1's earlier check of the same object, P being at a known distance from Q1's pointer..

The subtlety: Coverage.v needed only 2^64; the hull needed more, and mbrock chose native's 2^48 over a validator change. Whether a valid module's initial data fits is not proved, hence the ready-start hypothesis.

See runtime-axioms.md, The address space and rocq.md, Objects end below 2^48.