As data_base/1: the address where the module's items start.

As data_cap/3: the 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. of data with the linkage lk at base, writable or read-only; a weak declaration or an unknown linkage has none.

As filc_layout/3: the item it placed after those before it, updating the next address, the globals and the objects. A data object goes at the next address aligned to 16 or its stricter alignment, its size rounded up to 8, with a 16-byte gap after it; a function at the next 16-aligned address, 16 bytes, with the capability fn(Name). A weak declaration (extern(weak)) takes no space and stays undefined; an alias waits for alias_global.

As alias_global/3: an alias's address is its target's, the same pointer.

As filc_item_contents/4: one item of a data object written at the next address, and the address after it. A pointer item writes its symbol's address plus the offset, and the symbol's 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.; a symbol the module does not define is an external one.

As filc_contents/4: a data object's items written in order from its address; other items write nothing.

The memory with no objects, every byte zero and no stored capability.

As initial_memory/4 in filc mode: the module md's globals, each name with its pointer, and the memory with every item placed in order from data_base (layout), aliases bound (alias_global), and each data object's contents written (contents).

What a run ends with: an outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares., or halted where the interpreter throws or fails, with the step that was stuck.

Running under 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. R: R's alloc chooses each allocation's base, and R's free is the genv's.