As class(K, Kind, Bits): 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). of a value, one letter in ir.pl. Besides the integer, pointer and float classes there are the two proofproof nanofilA proof is a temporary of class a or f, the result of a check: it holds the checked pointer itself and certifies that the check passed. A raw access names the proof it relies on, so evidence is structural (ir:proof_use/6). classes of the checked stage, whose values are pointers a check has cleared.

Extended is C's long double, never a parameter, result, call argument or 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..

Equality of classes.

As float_class(K): whether the class k is a float class, s, d or x.

As int_class(K): whether the class k is an integer class, w or l.

As modulus(K, Mod): the values of class k are the integers from 0 up to Mod - 1, a float's being its bit pattern; a P value's address has the modulus of L. The proof classes have none.

As class_bits(K, Bits): the width in bits of an integer class k.

As half_modulus(K, Half): half the modulus of an integer class k; the values from Half up to Mod - 1 are the negative ones when read as signed, in two's complement.

The width of a store or of a data item, what size of value it writes: Wb and Wh are ir.pl's b and h, a byte and a 16-bit halfword, and the others are the classes w l p s d x.

As width_bytes(Width, Size): the bytes a width w writes; an x87 extended float takes 10.

A narrow integer type, the T of a narrow load and of ext(T): ir.pl's sw uw sh uh sb ub, a signed or unsigned word (4 bytes), halfword (2) or byte (1).

Whether an integer is read as signed, in two's complement, or as unsigned.

As narrow_type(T, Bytes, Signedness): the size in bytes and the signedness of the narrow type t.

The type of a raw loadraw access nanofilA raw access is a checked-stage memory access that does no checking of its own and names the proof that covers it: raw_load, raw_store, raw_load_pointer, raw_store_pointer, raw_cas and raw_call (ir:covered_access/6).: LdL for l, LdS, LdD and LdX for the float classes s d x, or a narrow type. This is load_type/1 without p, which RawLoadPointer reads instead.

A comparison's Cond: eq and ne at any numeric class, the signed and unsigned orders at w and l, and le lt ge gt o (ordered) and uo (unordered) at a float class.

The 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. an access asks for: to read, or to write, which a read-only object refuses.

Equality of rights.

Which end of an object's bounds 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 natively, ir.pl's upper or lower; an earlier check proves the other.

One step of the protocol by which a pointer load or store moves an address and its capability, as pointer_memory_effects/2 lists them:

• a heap load reads 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. word (AuxRead), resolves 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. from it (LowerResolve), then reads the address (AddressRead);
• a heap store makes sure the aux exists (AuxEnsure), applies the collector's barrier to the stored lower (LowerBarrier), reloads its destination from a rootroot Fil-CA root is a frame word the collector scans for live capabilities: an entry of the Pizderson frame's lowers[ ] (the record each function keeps on the stack: a parent link, an origin and the lowers), a local's stack aux, or a jmpbuf root (filc_abi:lower_function/5, amd64_regs_check:valid_map/3). Every live lower is in one at every safepoint, so registers never hold the only copy. (RootedReload), then writes the lower (LowerWrite) before the address (AddressWrite);
• AtomicRead and AtomicWrite are Fil-C's atomic pointer helpers, each a whole protocol.

Equality of effects.

Equality of two effect lists, step by step.

As pointer_memory_effects(load, Effects): the protocol of a heap pointer load, one of the two that evidence_preserving accepts.

As pointer_memory_effects(local_load, Effects): the protocol of a pointer load from a named local, whose explicit stack aux has no atomic box, so there is no lower to resolve.

Which of the three returns-twice calls a setjmp(Kind) is: setjmp, '_setjmp' or sigsetjmp (op_kind/2).

An operation, the Op of a let (ir.pl's Ops table): one constructor per functor in the core subset, with the functor's parameters as its arguments. The arithmetic and conversions come first, then the allocalloc Fil-CAn allocation: let(D, p, alloc(Align), [Size]) makes a fresh, zeroed heap object of Size bytes and yields a pointer to it with its capability. The frontend gives every C local one; promote and local_storage remove most of them under −O (promote:promote_module/2, local_storage.pl)., the checks of the checked stage and their reusereuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead. forms, the raw loadsraw access nanofilA raw access is a checked-stage memory access that does no checking of its own and names the proof that covers it: raw_load, raw_store, raw_load_pointer, raw_store_pointer, raw_cas and raw_call (ir:covered_access/6)., the variadic ops and setjmp. What each reads is op_arg_classes.

A value an instruction reads (ir.pl's Values table).

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 l value, or address(P), the address bits of the pointer P.

A flight's Lower, where its capability comes from: none, or lower(P), exactly the capability of the pointer P.

A call's Res, where its results go.

As arg(K, Value): a call's argument, the value v passed at class k.

An instruction of a block, in the core subset; the table at the top of the page gives each one's ir.pl term. The raw forms do no checking of their own: they read a proof of class A or F.

A jump's target: L, or poll(L), a pollcheckpoll 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). on the edge before going to L.

As edge_label(T, L): the label a target t goes to, polling or not.

The jump that ends a block (ir.pl's Jumps table).

As phi(tmp(D), K, [Pred-Value]): 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. at the head of a block, defining d, of class k, as the value paired with the block control came from.

As block(Label, Phis, Insts, Jump): 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., its phis, then its instructions, then the one jump that ends it.

A function's Ret: a class, void, or tuple([K1, K2]).

As func(Name, Linkage, Ret, Params, Blocks): a function.

As variadic_func(Func): whether the function f takes the entry argument snapshot of a variadic function, which it does with a va_args anywhere in its blocks.

A data object's Linkage (ir.pl's Data section). LExport, LLocal and LWeak are export, local and weak; LRo l is ro(L), read-only data, and LTls l is tls(L), an object each thread has its own instance of, both of the inner linkage l.

A data Item, a piece of a data object's initial contents. item(l, sym(Name, Off)) is plain mode's, outside the subset; item(p, sym(Name, Off)) is Sym.

As item_size(Item, Size0, Size): the bytes a data item takes.

The bytes a list of data items takes, the size of the object they make.

An item of a module; the table at the top of the page gives each one's ir.pl term.

A module, as module(Items): its items in order.

As op_arg_classes(Op, K, filc, Classes): the classes at which the op o reads its arguments when its result has class k; none where o cannot have a result of class k.

Whether the value v is a symbol's address, a Global.

As evidence_preserving(Inst): the instruction i reaches no safepointpoll 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). and cannot free an object or change its bounds or rights, so the evidenceevidence nanofilEvidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is a check immediately before the access, an earlier heap check whose live fact still holds, or a reuse form's trust: for renew a dominating check, for renew_if a guard's span test. of checks before it still holds after it.

As ahead_transparent(Inst): the instruction i may come between 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. and the access whose needneed nanofilA need is the validator's backward fact for check_ahead: need(B) = H at a point says every path from it reaches a raw heap access through a pointer of which B is an exact base, whose bytes reach B + H, and reaches it first: before any instruction that is not ahead-transparent, any poll edge, edge back or end, and before B is redefined. it checks early. It is evidence_preserving, and not a division, whose fault would end the program otherwise than a Fil-C 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..

As setjmp_func/1: the function f calls setjmp somewhere, reachable or not. Its second return is a control edge the blocks do not show (docs/setjmp.md), so the validator refuses what would need it.

As local_objects(Func, Objects): the named locals the function f declares, each with its size, in instruction order.