String equality, written as Prolog's ==.

The integer the term t is.

The name of the atom t.

The elements of the list t.

The arguments of t when it is the compound f/n.

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). an atom names: w, l, p, a, f, s, d or x.

The name of the 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. tmp(N).

An IR value: a temporary, an integer constant, or a global symbol.

The access rightsrights Fil-CRights are what an access asks of a capability: read or write, where write allows reading too. Every check, renew and raw access names the rights it needs. read or write.

The bound a half checkhalf_check nanofilhalf_check(Bound, Lo, Hi, Rights, Align) of [Q1, P] is exactly a check of [Lo, Hi) at P that natively tests only one bound, upper or lower; the other end is known from Q1's earlier check of the same object, P being at a known distance from Q1's pointer. tests: upper or lower.

A narrow integer width with its signedness: sw, uw, sh, uh, sb or ub (signed or unsigned word, half or byte).

The type a raw load reads: l, s, d, x, or a narrow width.

A comparison's condition: equality, signed and unsigned integer order, float order, and whether two floats are ordered or not.

One memory effect of a raw pointer load or store, such as reading 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. or resolving the 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..

A list of memory effects.

The width of a store or a data item: b, h, w, l, p, s, d or x.

The four bounds arguments Lo, Hi, Rights, Align of a checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4)., given to k to make the op.

An Op of ir.pl's table, 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 and variadics. A function that uses anything else decodes to IOutside.: arithmetic, conversions, comparisons, checks, raw loads and the rest.

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.: address(V), a pointer's address, or a plain value.

A flight's capability source: none, or lower(V), the 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. of the pointer V.

One result result(tmp(D), K) of a call: the temporary it binds and its class.

How a call reads its result: void, a tuple of results, or one result.

A call argument arg(K, V): a value and its class.

A list of call arguments.

An instruction 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.; None for any other.

A jump target: poll(L), a poll edgepoll 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). to L, or a plain label.

The jump that ends a block: goto, branch, return of one or several values or of none, or unreachable.

One L − V pair of a phi: a predecessor's label and the value for the edge from it.

A phiphi 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. phi(tmp(D), K, Pairs).

A 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. block(L, Phis, Insts, Jump), every part decoded.

A function's return type: void, a tuple of classes l, p, s or d, or one class w, l, p, s or d.

A parameter param(K, tmp(D)): its class and temporary.

A function from the arguments of its func(N, Lk, R, Ps, Bs) term; None if any part is 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 item's linkage; one the model does not know is kept as its term.

One item of a data object: a string of bytes, a pointer to a symbol plus an offset, a constant of a width, or zero bytes; any other is kept as its term.

An item of the module: 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 and variadics. A function that uses anything else decodes to IOutside. if dfunc fails, data or an alias; Some None for an explanatory context(_, _) item (contextcontext nanofilAn explanatory item of a module: context(Fn, Records) holds binding, typed-origin, value, alias and site records that say where Fn's IR came from (provenance.pl). Nothing runs it; only provenance's own check reads it (provenance:valid_contexts/1).).

The module module(Items), its context items dropped.

A 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. as the interpreter writes it: none, obj(B), ro(B), fn(F) or ext(N).

A 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 the interpreter writes it: an integer, ptr(Addr, Cap) or limit(Cap, Size).

A trap reasontrap 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. as the interpreter writes it, an atom, or early(R) and ahead(R) around another.