A repeated getter is a call of a gettergetter Fil-CA getter is the function that returns a global's or function's address with its capability, initializing it on first use. Upstream every symbol is renamed pizlonated_ plus its name, and that symbol is its getter, returning a flight pointer; the program checks the result like any pointer. In IR a getter call is let(tmp(D), p, copy, [global(G)]); calling one is a safepoint (filc_amd64:object_getter//2), so it ends every live fact, except a repeated getter. that another call of the same getter dominates in the same activation: a single-definition lettmpD, p, copy, globalG, 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 passevidence pass nanofilThe evidence pass is the validator's forward walk over a checked function: it tracks live facts and accepts each raw access only where its own check, a live fact or a reuse rule covers it. It visits the blocks once, in order; a block's entry facts are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited. lets live factslive 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. survive it.

• ir:repeated_getters/4ir.plrepeated_getters/4not documented, with ir:local_global/2ir.pllocal_global+Symbols, +GG is a function or data item this module defines with local linkage (not exported, weak or extern): its getter is a local symbol only this module calls.; empty in a function with setjmp. Validate.v's repeated_getters; Walk.v's repeated_getter marks it among the instructions the pass relies on.

• Local linkage matters: only then is the getter the one nanofil emits and nobody can interpose it.

The subtlety: the module type still lets 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. act before a getter, since it is not ir:evidence_preserving/1ir.plevidence_preserving+InstsemidetInst reaches no safepoint and cannot free an object or change its bounds or rights: pure arithmetic, comparison and conversion, pure pointer construction, a heap check, a scalar raw access (object headers lie outside every object's bounds) and a raw pointer load (aux and box reads, no helper). Calls, alloc, getters, setjmp, va_arg, pointer stores and the res…, so the proofs cover it through 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., which every runtime meets because its safepoint changes no region (collector_live); natively the fast path reaches no safepoint at all.

See forward.md, Getters.