The eight-byte cell at address a of memory m holds pointer p: its bytes read as p's address and its 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. entry is p's capability. A slot carries address bits AND the corresponding capability. Bounding the address below 2^64 prevents an integer outside the word range from standing for the same stored bytes.

The same address/aux store used by store_res constructs an actual decoded slot. No access or capability authority is inferred here; local_store_pointer supplies the separate footprint obligation.

A byte store of size bytes at address a keeps a pointer_slot at b that it does not overlap.

A pointer store at address a keeps a pointer_slot at b eight or more bytes away.

From address a on, memory m holds one pointer_slot per text, each pointing at a c_string with that text, then a null slot.

Pointer table points at a null-terminated array of C strings with the given texts, as argv and envp are. Check the entire pointer array, including its sentinel, with the array's capability and pointer alignment. A raw address whose 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. metadata was lost does not satisfy the string slots.

Memory m is the launcher's entry image for main's arguments argc, argv and envp, with argument strings args and environment strings environment: argc is a positive int counting args, and argv and envp are string_vectors of them.

A libc-exposed pointer cell has its own writable object authority and decoded value. Authority to its pointee is not authority to change the cell, nor does this predicate establish FILE validity.

Distinct symbolic roles, not an assertion that their storage is disjoint. The program-name aliases may name the same native cells.

Symbol resolution reaches the cells themselves, not the FILE or character buffer stored in them. Module linking supplies this map.

Concrete exposed cells at a successful entry. Program names have independently readable NUL-terminated contents; they are not silently identified with the launcher's copied argv0. Program code may subsequently replace their pointer values. Stream object validity, libc/TLS state and separation remain separate premises.

The ordinary non-atomic pointer-load protocol recovers exactly the stored address AND capability, not an external/null surrogate.