The runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGCFUGC Fil-CFUGC, Fil's Unbelievable Garbage Collector, is what reclaims memory in Fil-C. It marks and sweeps on its own threads, in parallel, while the program runs, and never moves an object. It never stops the world: it asks each thread for work, such as scanning its stack, by a soft handshake, which the thread answers at its next pollcheck. While it marks, a store barrier marks the target of every pointer stored to the heap. It finds pointers exactly: on stacks through the roots the compiler keeps, and in objects only in their aux allocation.: where a new object goes, what free does, and what the collector may change while the program waits at 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).. 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.

• Ten axioms: fresh_allocation, address_space, non_moving, free_lifetime, collector_live, safepoints, retention, free_keeps_ids, free_checked, aux_round_trip. safepoint_lifetime and rooting were axioms too; they are now lemmas from collector_live. Three more readinessready 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. obligationsobligation nanofilAn obligation is something a proof leaves to be shown or trusted elsewhere, named rather than assumed away. A realization obligation is the trusted claim that native code realizes a logical model: that pinned libc's FILE, buffering and dispatch behave as Stdio.v's protocol and Libio.v's memory view say., freed_bounds, ready_kept and safepoint_ready, are about the runtime's own bookkeeping and have no native test.

• InterpRuntime is interp.pl's runtime: 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… for allocation, interp:free_res/4interp.plfree_res+P, +Mem₀, -Res, -Memthe pinned runtime's free_with_checks, object_for_deallocate and free_impl, for objects this interpreter owns. ext(_) has a placeholder address, not a known zero; it stays unsupported. Public run/5 also accepts integer p arguments: these have no capability. for free, nothing at a safepoint. It proves every axiom, so the module type is consistent and judge is closed.

• The machinemachine nanofilThe machine of a runtime R, Machine R, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs. runs over any runtime, so every theorem holds of all of them.

The subtlety: the model has one thread and no collector, and its safepoint action changes no region (collector_live): Fil-C's runtime never frees an object by itself. A signal handler or another thread that frees is the program's code; in the model installing a handler or starting a thread is a call to an external with no contract, which ends the run. Natively, retentionretention nanofilRetention is the runtime axiom that free changes no byte and no stored capability: a freed object's memory stays as it was while anything can name it. Only its header changes, so every access through a capability to it traps, but bytes read through a check that passed before the free are the same bytes. and non_moving make another thread's free between a check and its access read retained bytes or trap.

Defined in Runtime.v; the axioms with their tests and sources are runtime-axioms.md.