How a run ends (the table above): a return of one wordword nanofilA word is the value a temporary holds at run time: an integer, a pointer (an address with its capability), or a limit's opaque snapshot. The temporary's class says how it is read., of several, or of none; an unreachable jump reached; undefined behaviour; 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. with its reason; 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, which only a broken pass produces; or no fuelfuel nanofilThe interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5). left.

A function the module names: one with a body in 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, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside., or one outside it, kept only by its name n.

The global environment: the module ready to run (module_prepared/2's Fns and Globals, each global's name with its pointer), and 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.'s free that a call of libc's free runs: Memory.v's free_res in the interpreter, R.free of a Runtime R (Run.v's Driver, Machine.v).

The function or outside function of the module items named n, not looking through aliases.

The target of the alias named n among the module items, if there is one.

The function a call of the name n runs, as get_assoc(F, Fns, Fn) finds it in the prepared module's Fns: a function by its own name, or an alias of one by the alias's name.

An environment: each temporarytemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR. assigned so far, with its wordword nanofilA word is the value a temporary holds at run time: an integer, a pointer (an address with its capability), or a limit's opaque snapshot. The temporary's class says how it is read..

As value_x/5: the IR value v read at classclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). k in the environment e. A constant at p is a pointer with no 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.; a symbol the module does not define is ptr(0, ext(Name)), a pointer with an external capability.

f applied to every element of xs, or None if it fails on any.

f applied to the elements of xs and ys pairwise, or None if it fails on any pair or the lists differ in length.

As arg_x/4: a call argument's value read at its own classclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3)..

As flight_arg_x/4: an argument of a flightflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it.'s address computation. An address projection takes the low 64 bits of a pointer's address; any other argument is read at class l.

As flight_cap/4: the 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. a flightflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it. gives its pointer. A lowerlower Fil-CThe lower is how Fil-C represents a capability natively: the address of the first byte of the object a pointer may access, kept beside the pointer's intval in a flight pointer. The object header sits just below it: the upper bound at lower−16 and the aux word at lower−8, whose low 48 bits point at the aux allocation and whose top 16 bits hold the object's flags (free, read-only, global, ...). A null lower accesses nothing, and free sets upper to lower, so every access through any lower of a freed object fails. filc_abi:lower_function/5 keeps each live one in a root. source copies its pointer's capability, and so the object's identityidentity nanofilAn object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object.; none gives no capability.

Where a frameframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point. is in its function:

• Snapshotxs l: a variadic callee about to take the snapshot of its arguments xs, an allocation, before entering its entry block l;
• Enterl from: about to run blockblock nanofilA block is a labelled straight line of a function: phis, then instructions, then one jump (goto, branch, ret, rets, ret, unreachable). The first block is the entry and has no phis; its label is the name edges use. l, entered from the block from (None for the entry); entering costs one unit of fuelfuel nanofilThe interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5)., and with none left the run is OutOfFuel, as block_outcome/7 says;
• Execl insts j: inside block l, with the instructions insts and then the jump j left to run.

One invocation of a function: the function, its environment of temporariestemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR., each named local with its object's base once allocated, the reason it is doomeddoomed frame nanofilA frame is doomed after a check_ahead whose early bytes failed: the check yields its pointer anyway and the frame records the failure, because the validator promised that the frame will reach an access that fails on those bytes before anything observable happens. if an early 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. failed, and where it is.

How a suspended caller reads its callee's 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.: the call's Res, the temporaries it binds, and for a call through the generic entryfast and generic conventions Fil-CFil-C's two ways into a function, from its optimized calling convention: the fast entry takes the arguments in registers, for a caller that agrees on the signature; the generic entry takes them in the thread's CC buffers, one for bytes and one for lowers, for any caller. A function object holds both entries and a 64-bit signature, an arithmetic encoding of its type that is 0 when only the generic entry exists. the caller's and callee's word classesclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). (indirect_call_conv/7's conv(CallerWords, CalleeWords)).

A configurationframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point.: the running frameframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point., the suspended callers innermost first, each with how it reads the result, the memory, and the fuelfuel nanofilThe interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5). left (the table above).

The frame fr moved to the point pt, all else kept.

The new frame of a function f called with the words xs, as call_outcome/8 starts it: parameters bound to the first arguments as they are, each local declared and not yet allocated, at the entry block; a variadic callee first takes the snapshot of all its arguments (entry_snapshot/6). None if there are fewer arguments than parameters or f has no blocks.

The name of the environment's hidden entry that holds the pointer to a variadic callee's argument snapshot, which va_args reads.

As snapshot_values/5: the memory m with the argument words xs stored from address a on, 8 bytes apart, each as p if it is a pointer (its address in the bytes, its 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. in 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.), else as l. The stores are into a freshfresh base nanofilA fresh base is an address where a new object may be placed: positive, aligned, no object's identity (live or freed), overlapping no object's bounds, ending at or below 2^64, and reading as zero with no stored capability, as Fil-C's allocations do. object of 8 bytes per argument, so their checks pass.

The words snapshot_values/5 can store: integers and pointers.

The blockblock nanofilA block is a labelled straight line of a function: phis, then instructions, then one jump (goto, branch, ret, rets, ret, unreachable). The first block is the entry and has no phis; its label is the name edges use. labelled l among bs.

As phis_env/6: the environment after a block's phisphi nanofilA phi phi(tmp(D), K, [Pred-Value]) gives D the value paired with the block control came from. A block's phis run together on entry, each reading its operand as it stood at the end of the predecessor., entered from the block from. Each phi reads its value for the edge from that predecessor in the environment e0 as it was on entry, so they all bind at once. An entry block (from None) has no phis.

As invalidate_locals/3: an invocation's named locals end with it. Their identitiesidentity nanofilAn object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object., bytes and 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. stay; their bounds become empty, so any later access through them traps.

As function_check_res/3: the pointer p designates a function only with that function's 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. at its exact callable address; otherwise the check traps. A pointer with an external capability has no answer here.

As result_words/2: the classesclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). of the words a call site reads.

As return_words(Ret, Ks) in interp.pl: the classesclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). of the words a function returns.

The kinds of word a call passes or returns: integer, pointer, single float and double float.

As word_class/2: the kind of word a classclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). k is. Classes w and l are the same word; p, s and d are each their own.

Whether two word kinds are the same.

The -> condition of indirect_call_conv/7: both lists of words have word classes, and the same ones.

As generic_word/4: the word x written at classclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). from and read at class to through the generic entryfast and generic conventions Fil-CFil-C's two ways into a function, from its optimized calling convention: the fast entry takes the arguments in registers, for a caller that agrees on the signature; the generic entry takes them in the thread's CC buffers, one for bytes and one for lowers, for any caller. A function object holds both entries and a 64-bit signature, an arithmetic encoding of its type that is 0 when only the generic entry exists.. An integer read as a pointer has no 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.; a pointer read as an integer or a float is its address.

What converting a call through a function pointer gives: 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., or the converted arguments ys and, if the result words need converting too, the caller's and callee's word classes.

As indirect_call_conv/7: a call through a pointer to f, reading its result as r, with arguments args whose values are xs. It traps if the caller passes fewer arguments than f has parameters or reads more result words than f returns; otherwise each argument is read as f's parameter through the generic entryfast and generic conventions Fil-CFil-C's two ways into a function, from its optimized calling convention: the fast entry takes the arguments in registers, for a caller that agrees on the signature; the generic entry takes them in the thread's CC buffers, one for bytes and one for lowers, for any caller. A function object holds both entries and a 64-bit signature, an arithmetic encoding of its type that is 0 when only the generic entry exists. (generic_word).

As outcome_words/2: the words a returning 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. returns; None for one that does not return.

The returning outcome that returns the words ys.

As converted_outcome/4: the callee's outcome o as a call site that reads the word classes caller reads it, each word converted from the callee's class by generic_word. An outcome that does not return passes unchanged.

As call_outcome_result/5 for a returning outcome o: the caller's environment e with the returned words bound as its Res r reads them.

What one instruction does: continue with an environment, locals and memory; stop with an 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.; call a function with the words xs, the caller to read the result as pd says; allocate for the request q, going on as k says of the new base; or call a function 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, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside..

As res_result/5: an operation's result r bound to the temporary d, or its 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. or 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). reason as the outcome.

As store_res_result/4: a store's result r, going on with nothing bound, or its trap or unchecked reason as the outcome.

As width_value_class/2 (filc_amd64.pl): the classclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3). at which a raw store of width w reads the value it stores.

The name of libc's free, the one external callexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings. the model runs.

A call of a name f the module does not define as a function: inst_result/5's call of global(F). Data the module defines is not a function, and the call traps, as native code's function check does. Otherwise it is external_call_outcome/9: only libc's void freep is modeled, through 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.'s free, the genv's ge_free; any other external call is stuck until Campaign 4 gives it a contractexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings..

As inst_result/5 for 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, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside.: what the instruction i does in the frame fr with memory m. None where the interpreter throws or fails, such as a temporarytemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR. read before it is assigned or an access through an external capability.