An allocation: letD, p, allocAlign, Size makes a fresh, zeroed heap object of Size bytes and yields a pointer to it with its 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.. The frontend gives every C local one; promote and local_storage remove most of them under -O (promote:promote_module/2promote.plpromote_module+M₀, -MdetM is the module M0 with the promotable allocs of each function promoted., local_storage.pl).

• Rocq: the op Alloc, whose request heap_req 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.'s alloc places at a 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. base. A size over 2^48 - 1 traps too_big before anything is allocated (interp:alloc_res/6interp.plalloc_res+Mode, +Mem₀, +Align, +Size, -Res, -Memthe heap allocation alloc(Align) of Size bytes. Fil-C refuses an object of more than max_allocation_size/1 bytes before it allocates anything (filc_prepare_allocate_object/1: "attempt to allocate object that is too big"), and one its address space cannot hold ("out of memory"); both are safety errors., max_allocation_size); where the runtime cannot hold the object, the run traps out_of_memory.

• Upstream every alloca becomes a FUGC allocation too, and FilPizlonator's escape analysis puts those that do not escape back on the stack; promote and local_storage are nanofil's counterpart.

• An allocation is a safepointpoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1)., so it ends every live factlive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own..