An object's aux allocation, as large as its payload: where Fil-C keeps the lowerslower Fil-CThe lower is how Fil-C represents a capability natively: the address of the first byte of the object a pointer may access, kept beside the pointer's intval in a flight pointer. The object header sits just below it: the upper bound at lower−16 and the aux word at lower−8, whose low 48 bits point at the aux allocation and whose top 16 bits hold the object's flags (free, read-only, global, ...). A null lower accesses nothing, and free sets upper to lower, so every access through any lower of a freed object fails. filc_abi:lower_function/5 keeps each live one in a root. 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.

• An entry with its low bit set points at an atomic box, a 16-byte object holding a whole flight pointerflight pointer Fil-CA flight pointer is a pointer held in a variable or register rather than in memory. It has two words: its intval, the address the C program sees, prints and computes with, which nothing trusts; and its lower, the capability, which only an allocation creates and the program can neither see nor forge. Stored to memory it becomes a pointer at rest: the intval goes in the object's bytes and the lower in the object's aux allocation, where no capability reaches. That invisibility gives InvisiCaps their name, and it keeps sizeof(void*) at 8. for a pointer accessed atomically; its lower is at box+8 (ir:pointer_memory_effects/2ir.plpointer_memory_effects?Access, ?EffectsnondetEffects is the closed, ordered protocol of a pointer access of kind Access: load, store, local_load, local_store, atomic_load, atomic_store or cas. For an ordinary heap load, aux_read reads the encoded lower (or none) and lower_resolve unboxes it without taking the box's address. A store ensures aux (may exit), barriers the value's lower (may call, cannot ex…, filc_amd64:pointer_load_effects//4filc_amd64.plThe effect list determines execution; only its caller publishes the result. No-aux jumps to lower_resolve's null arm. Resolving a box reads only its lower: address_read always reads the primary payload.). A named local's stack aux has neither header nor box.

• Rocq: m_aux, 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. stored at each 8-aligned slot, written by store_aux and read by aux_at; 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 aux_round_trip says what a safepoint may do to it.

The subtlety: ensuring aux is a safepoint natively, where a signal handler the program installed may run and free the checked object. That is why a pointer store's facts once needed sparesspares nanofilspares says that at a safepoint just before an instruction the evidence pass keeps facts across, the runtime changes no region. Every runtime meets it, so the generic soundness theorem, once stated under it, no longer takes it as a hypothesis. as a real hypothesis. The model has no handler, so every runtime now meets it and the theorems no longer take it; a verified handler must not free an object whose check is in flight.