The checked module, decoded from the fixture prefix_term (prefix_decodes).

The fixture decodes to prefix_module.

The function prefix, the module's first item.

The module's globals: the array xs, laid out as in Sum.v, and the function prefix.

The module's initial memory.

Laying out the module succeeds, with prefix_globals and prefix_mem.

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

prefix 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.

The name of prefix's parameter.

Any arguments whose first word is the integer n start prefix at its entry block with n as its parameter.

The environment e with the parameter's word replaced by the integer n: a state of a computed run, for the input n.

The run of prefix on the input k, computed by the model on the initial memory.

The runs on the inputs 0 to 5: every way the comparisons with n can go, since the loop stops at the first false one or after four.

Where the run r leaves the loop because the index is not below the input: the first point at the loop's branch with the comparison false; the run's length if there is none.

Index i of run k stands for a state: run 5 stands for every run up to where it leaves, so a run k below 5 is used only from there.

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

Each long the step read from the array, known by Hb that the memory has the initial bytes: the long at its address.

The next state is index S i of run k.

One state of run k: take its point and environment from Hn, take its step by its rule (take_step) with the longs it loads, and find it among the outcomes prefix_progress allows, trying run k first for the next state, then each run.

The states of run k below 5, which start where it leaves run 5 (canonical): five of them, to its return.

From index i of run k, for the 32-bit input n, in any memory that is mem_ok and with any fuel, prefix steps to index S i of some run with the same memory, ends for lack of fuel, or returns.

prefix 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.