The runtime's own state, which the program never reads: the interpreter's Next.

The runtime's state when a run starts.

The runtime in state s 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. to allocate in the memory m: its bookkeeping agrees with m, so a new object will be fresh there. For the interpreter, every object lies below Next and nothing above it has been written.

The base of a new object for the request q, and the state after it; None when the runtime cannot hold the object, which ends the run with trap(out_of_memory).

The allocator gives each new object an address no other object uses. Where the runtime in state s is ready in memory m, a request q with a positive alignment and an extent of at least 0 that alloc grants gets a fresh base: a new 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., aligned, overlapping no object, ending at or below 2^64, reading as zero with no stored capability; and the runtime is ready in the memory with the new object. The model needs it so that a new object cannot alias an old one, and so the step relation's choice of any fresh base covers every runtime.

Natively a freed object's address can be a new object's once nothing names the old one; the model never reuses an identity, because a capability never dies in it. The two agree on whether each access through a capability the program still holds traps, not on its address bits after a collection. Native test: axiom − fresh.c.

Every object lies in native Fil-C's address space: where the runtime in state s is ready in memory m, every object of m lies between 0 and 2^48 (objects_fit). The model needs it so that no address inside an object wraps and a wrapped address 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.; an allocation the runtime cannot hold is refused, a trap. Native test: axiom − address.c.

No freed object of a memory m the runtime is ready in has bounds (freed_empty). Every free and the end of every invocation empty them (lifetime_step, region_step), so it constrains only the memory a run starts in. It is about the runtime's own bookkeeping, not Fil-C, so it has no native test.

The program's own changes keep the runtime ready: if it is ready in m, and m' is m after the program wrote inside objects and ended some (kept), it is ready in m'. With fresh_allocation and safepoint_ready this makes ready hold in every state of a run (Machine.v). No native test: it is about the runtime's own bookkeeping.

Free of a pointer word: its result, and the memory after it. This is what a call of libc's free runs, the genv's ge_free.

Free changes an object's bounds only by emptying a live heap object's, for every alias at once, and makes no new identity (lifetime_step). The model needs it so that a capability the program holds keeps its meaning across a free except for the freed object, whose every access then traps. Native test: axiom − lifetime.c.

Free changes no byte and no stored capability: a freed object's memory is retained while anything can name it. Machine.v uses it to show a free keeps the program's other memory; natively it is also what lets an access whose check passed before another thread's free read the same bytes. Native test: axiom − retention.c.

Free reclaims nothing: every 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. before it is one after it, the freed object's too. Only the collector reclaims, at a safepoint (rooting), and natively only of objects nothing can name, whose regions the model keeps. With fresh_allocation this keeps a later allocation from taking a freed object's base. Native test: axiom − identity.c.

Free frees or trapstrap Fil-CA trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trap(Reason), terminal and uncatchable. Because nothing follows it, a check is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour.; it never goes on having done something else, so it never answers uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2)., which the model keeps for a broken pass. Native test: axiom − free.c.

Free succeeds where a program frees what it owns: on the null pointer it does nothing, and on the base pointer of a live heap object it frees that object as frees_heap says. free_lifetime, retention and free_keeps_ids bound what any free may change; this says that such a free returns, so that a program logic can prove a call of free goes on (Logic.v's wp_free). The pointer carries the object's Obj capability, not a read-only one. The model's heap objects are what the IR's alloc makes (malloc-like calls, and the address-taken locals, VLAs and allocas nanofil leaves on the heap), what the malloc and strdup contracts make, and the startup argv and environ objects; natively each is an ordinary collected object, which free returns on. Free of a global, an mmap'd object, an interior pointer or a freed object traps. Native test: axiom − free − succeeds.c.

The runtime may act at the instruction i: the collector's handshake, a pollcheck callback, or a signal handler the program installed. Another thread's effects are outside the model (the header's One thread's view).

The runtime acts only at instructions that are not evidence_preserving/1: calls, polls, alloc and the rest. The model needs it because the validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. keeps evidenceevidence nanofilEvidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is a check immediately before the access, an earlier heap check whose live fact still holds, or a reuse form's trust: for renew a dominating check, for renew_if a guard's span test. across every other instruction, which would be unsound if the runtime could free or rewrite memory there. Native test: axiom − safepoint.c.

What the program may find changed when it reaches 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). with the runtime in state s and memory m: the runtime's state s' and memory m' after the collector acted.

At a safepoint no regionregion Fil-CAn object is one allocation a capability can name, its bytes what upstream calls the payload: a heap object, a named local, a data item or a variadic argument snapshot. A region is the model's record of it, region(Base, End, Kind, Life): its bounds [Base, End), its kind (stack, heap or global data) and whether it is live or freed. changes: the collector frees no object, live or freed, and no identity appears. Natively the collector reclaims objects nothing can name; the model keeps their regions, as fresh_allocation explains. Only the program frees, by free or by code it brought in (a signal handler, a thread), and that is not the runtime's action. The model needs it so that an object live before a poll is live after it with the same bounds. Native test: axiom − collector − live.c.

At a safepoint, as at a free, an object's bounds change only by a live heap object's being freed, and no identity appears (lifetime_step); at a safepoint none changes at all (collector_live).

At a safepoint no byte moves or changes: the collector writes no object's contents and no address word. The model needs it so that the bytes a check passed stay readable, unchanged, until the program next looks at the header. Native test: axiom − nonmoving.c.

At a safepoint each stored 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. (in the auxaux Fil-CAn object's aux allocation, as large as its payload: where Fil-C keeps the lowers of the pointers stored in the object, slot for slot, while their intvals sit in the object's bytes. The aux word in the object header points at it; it is null for an object no pointer was ever stored into, which the collector then scans as a leaf. A pointer store must *ensure* it exists, which may call the runtime; a pointer load reads it.) stays, or, if its object was freed, becomes one that traps as a freed object does: the collector's free singleton. The model needs it so that a pointer loaded back after a collection behaves as the one stored, reading or trapping alike. Native test: axiom − aux.c.

At a safepoint the collector reclaims no 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. the program can name: every object of m is still one of m'. The model needs it because a capability never dies in the model, so the object it names must stay. It follows from collector_live. Native test: axiom − rooting.c.

The runtime's actions at a safepoint keep it 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.. With fresh_allocation and ready_kept this makes ready hold in every state of a run (Machine.v). No native test: it is about the runtime's own bookkeeping.