The checked module, decoded from the fixture sum_term (sum_decodes).

The fixture decodes to sum_module: the proof is about what nanofil makes of sum.c.

The function sum, the module's first item.

The module's globals, each name with its pointer: the array xs and the function sum.

The module's initial memory, as initial_memory/4 lays it out.

Laying out the module succeeds, with sum_globals and sum_mem.

The genv of the module with any free; the program calls none.

sum is a function of the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals and variadics. A function that uses anything else decodes to IOutside. in the module.

Any argument list starts sum at its entry block with no temporaries.

The points and environments of the run in the genv ge from the configuration c, one per step, for at most n steps, until a step is not Next.

The one path of sum, computed by running the model on the initial memory: 59 points, ending at the return of 10. The proof does not trust it; sum_progress checks every step.

The array xs: 32 bytes of read-only global data.

The memory m agrees with the initial memory m0 on everything a program that only reads the array reads: the bytes, and the array'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..

The initial memory agrees with itself.

A load reads only bytes: two memories with the same bytes load the same value.

The four longs of the array in the initial memory, 1 to 4.

Compute the step in the goal for a memory known only by Hb and Hr and the fuel: at a block's entry, which tests the fuel, split on whether fuel is left, and rewrite that test first, before the arithmetic it guards is unfolded; then reduce the step without unfolding the memory's regions, loads or the initial memory, and rewrite what the reduction is stuck on (the array's region, its loads), again until nothing changes.

One point of the path: take its point and environment from Hn, compute the step, and find it among the three outcomes sum_progress allows.

From the n-th point of the path, in any memory m that is mem_ok and with any fuel, sum steps to the next point with the same memory, ends for lack of fuel, or returns 10.

sum never panics under 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. R.