A getter is the function that returns a global's or function's address with its 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., initializing it on first use. Upstream every symbol is renamed pizlonated_ plus its name, and that symbol is its getter, returning a 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.; the program checks the result like any pointer. In IR a getter call is lettmpD, p, copy, globalG; calling one is 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). (filc_amd64:object_getter//2filc_amd64.plThe getter of a function object FO: its flight pointer, whose lower is its address, in %rax:%rdx.), so it ends every live factlive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own., except a repeated getterrepeated getter nanofilA repeated getter is a call of a getter that another call of the same getter dominates in the same activation: a single-definition let(tmp(D), p, copy, [global(G)]), G defined in this module with local linkage. The first call has returned, so the repeat takes the fast path: no safepoint, no free, no store. The evidence pass lets live facts survive it..

The model has no getter call: a Global operand reads the symbol's pointer from the global environmentglobal environment nanofilThe global environment is what every step of a run reads but never changes: the module, each global's pointer, and the free that a call of libc's free runs.'s ge_globals, or an external capability for a symbol the module does not define.