The program both logic spikes prove, shared by them: spikes/listsum.c, which builds a linked list of n nodes on the collected heap (__builtin_alloca, which Fil-C places there), then calls sum, which walks it and adds each node's value. Its checked module is listsum_term (ListSumCode.v, checked current by spikes/code.sh).

sum is gc.ir's list walk in checked form: per node a checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4). of the value's 8 bytes, a lower half checkhalf_check nanofilhalf_check(Bound, Lo, Hi, Rights, Align) of [Q1, P] is exactly a check of [Lo, Hi) at P that natively tests only one bound, upper or lower; the other end is known from Q1's earlier check of the same object, P being at a known distance from Q1's pointer. for the next pointer, a raw pointer load through the 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., and a pollpoll 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). on the back edge. listsum adds an allocation per iteration, a pointer store and a direct call. This file holds only what both spikes need: the module, its globals, its two functions and their call frames (docs/logic.md).