A 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 lowerlower 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., 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., 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 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. allocation, where no capability reaches. That invisibility gives InvisiCaps their name, and it keeps sizeof(void*) at 8.
Every access pairs an untrusted intval with a trusted lower; the check asks whether the intval's bytes lie inside the lower's object.
Converting an integer to a pointer gives a null lower, unless launderinglaunder Fil-CLaundering gives an integer converted back to a pointer the capability of the pointer it came from, as Fil-C does when its analysis can follow the integer: through arithmetic, promotable local variables and phis, never through memory or a call, and only from one pointer (launder:launder_func/4, m4.md, *Pointer-as-int laundering*). Otherwise the pointer gets no capability and dereferencing it traps. traces the integer to the one pointer it came from. Storing an integer over a pointer at rest changes its intval and keeps its lower, so a load then yields a pointer that may trap but is never forged.
In nanofil a word of classclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). p is a flight pointer: ptrAddr, Cap in interp.pl, ptr in Values.v, whose Cap abstracts the lower to an 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 flightflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it. instruction builds one from an intval and a lower that come from different names (pizlonate:flight_inst/2pizlonate.plflight_inst+Inst0, -InstsemidetInst is the flight of the pure pointer operation Inst0: add or sub of an offset, a copy of a temporary or constant, or itop, which has no lower. The address calculation and lower are chosen independently; no new temporary or safepoint separates them. A symbol copy still calls its getter; it is not a pure projection, and stays.).
Fil-C's source calls the intval ptr: a filc_ptr is the pair ptr, lower.