spares says that at a safepoint just before an instruction 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. keeps facts across, 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. changes no regionregion Fil-CAn object is one allocation a capability can name, its bytes what upstream calls the payload: a heap object, a named local, a data item or a variadic argument snapshot. A region is the model's record of it, region(Base, End, Kind, Life): its bounds [Base, End), its kind (stack, heap or global data) and whether it is live or freed.. Every runtime meets it, so the generic soundnesssoundness of checking nanofilSoundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps. theorem, once stated under it, no longer takes it as a hypothesis.

• Invariant.v's spares, over Walk.v's relies. The module type lets the runtime act before any instruction that 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…, yet the pass keeps facts across three such: a pointer store taken with its check, a check_local, and 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..

• Invariant.v's spares_any proves it of every runtime, from the axiom collector_live: no region changes at a safepoint. Persistence.v's safepoint_inv uses it directly, so valid_no_unchecked and the run theorems take no such hypothesis (dropped 2026-11-09), and the interpreter's theorems are plain instances of them.

Why it was a hypothesis: until 2026-11 the runtime's safepoint stood for the thread's signal handlers too, and natively a pointer store 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. must be allocated exits to the runtime, which may run a handler that frees the checked object. The store then lands in retained memory, safe by retentionretention nanofilRetention is the runtime axiom that free changes no byte and no stored capability: a freed object's memory stays as it was while anything can name it. Only its header changes, so every access through a capability to it traps, but bytes read through a check that passed before the free are the same bytes. but unchecked in the model. mbrock decided (November 2026) to keep it a hypothesis, then (2026-11-09) that a handler is the program's code, not the runtime's: in the model installing one is a call to an external with no contract, which ends the run. What remains is a constraint on verifying handlers: a verified handler must not free an object whose check is in flight, or the theorems weaken to "checked, or freed since its check".

See rocq.md, The evidence invariant over runs.