A traptrap Fil-CA trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trap(Reason), terminal and uncatchable. Because nothing follows it, a check is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour. reason that is a refusal, not a panic: the runtime would not hold an allocation (out_of_memory), or the request is over 2^48 - 1 bytes (too_big), which C's malloc would answer with null. These are mbrock's decisions in formal.md's panic table, and ExternalCalls.v's resource_reason for a call (refusal_resource).

The outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares. o is a failure: a trap that is not a refusal (every capability check, Early traps of a check_aheadcheck_ahead nanofilcheck_ahead(Lo, Hi, Rights, Align, AHi) is a check of [Lo, Hi) whose own access needs only [Lo, AHi): the bytes [AHi, Hi) are checked early for later accesses through the same base, as filcc's check scheduler does. It may trap earlier than the reference program, but only on runs that would trap later anyway. included), an uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2). access, undefined behaviour, or unreachable reached. Returns and OutOfFuel are not.

The configuration c fails in the genv ge: its 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. ends in a failure, is stuck (the run left the model: an external call, code outside 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., an ill-formed word), or asks for an allocation with a negative extent, which the machine cannot take. An allocation the runtime refuses is not a failure: it ends the run with trap(out_of_memory), a refusal.

The labelled machine's ending why is a failure: a core failure, a stuck core step, or a contract violation at a call. A process exit is not.

A refusal is a resource ending of a call, and back.

A trap that ends a call for lack of resources is not a failure.

The step result r, of a configuration in the memory m, is safe for the invariant inv: a next configuration in inv, an ending that is not a failure, or an allocation with a nonnegative extent whose every fresh base in m gives a configuration in inv. Never stuck.

The property over any 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.