A program with a heap object, proved never to panic: rocq/programs/buffer.c, which allocates a buffer of four longs (__builtin_alloca, which Fil-C places in the collected heap), fills it, then sums p[i % 4] for i from 0 while i < n, for every int n (BufferCode.v, checked current by rocq/programs.sh). BufferLogic.v proves the same theorem through the Iris program logic.

The proof is Cycle.v's: an assertion at each of the function's 32 points (buffer_assert), and one stepstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck. from any configuration where it holds is safe and reaches a point where its assertion holds (buffer_safe). What is new is the object. The run chooses its base, so the assertions speak of any base b that the allocation could return (fresh): from the allocation on, the temporary v4 holds a pointer to b with b's own 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., and b's 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. is a live heap object of 32 bytes. The access checks then pass because each address is b plus 0 to 24.

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). leaves the object as it is: the collector changes no region (Runtime.v's collector_live), and Fil-C's runtime frees nothing by itself. Only code a program brings in, a signal handler it installs or a thread it starts, could free the buffer under it, and buffer calls no external at all. So the theorem holds for every runtime with no premise.

Decisions