Option binding: let* x ≔ e in b is b with x the value of e, or none if e has none.

As sign_extension(M, H, U, S): the two's-complement reading of the low bits of u, for a field of modulus m with sign threshold h, from which values read as negative.

As signed(K, U, S): the integer u of class k read as signed; none for a class that is not an integer class.

As extension(T, X, S): the low bytes of x that the narrow type t names, sign- or zero-extended.

As cond_bit(Cond, K, X, Y, B): 1 when x c y holds at the integer class k, else 0; a float condition has none here (float_compare).

As shift_factor(K, Y, P): the power of two a shift by y at class k multiplies or divides by; the count is taken modulo the class width.

As unsigned_division/4: the division or remainder f of x by y, where a zero divisor gives 0.

As signed_division/5: the division or remainder f of x by y read as signed at class k. A zero divisor gives 0, and the quotient truncates toward zero (Prolog's // and rem), then wraps, so the most negative value divided by -1 is itself.

As alu(Op, K, Xs, Res): the integer op o of class k on the words xs, wrapping to the class's modulus; add and sub are integer here (additive_res adds to pointers). No word for arguments of the wrong form.

As additive_res(K, Op, Xs, Res): add or sub at class k. A pointer plus or minus an l offset keeps its capability, its address wrapping modulo 2^64; integer add and sub are alu's.

As checked_res(Res0, P, Res): 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).'s result from its access check r: the pointer p, now proven, or r's trap.

As raw_res(Res0, Res): a raw accessraw 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). is the access its check covers, made again without trapping; what would have trapped is 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)..

As renew_res(Res0, P, Mem, Res): a renewrenew nanofilA renew reuses an earlier check's bounds: renew(Lo, Hi, Rights, Align) of [Q1, P] trusts the dominating check that made Q1 for P's bounds and tests again only what a free changes, that the object is not freed (and, for a write, not read-only). It is the −O default (check_reuse:renew_checks/2, m7.md, round 4).'s result from the access check r of the check it replaced, of the pointer p. It traps as that check would on a freed object or a write to a read-only one; any other failure means the earlier check's bounds did not cover this access: unchecked Span.

As half_bound(Bound, B, Size, Base, End, Life): the one 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 natively, for size bytes at the address b of the object from base up to end_ of life l. The upper bound holds if the bytes end at or below end_; the lower if base is at or below b read as signed, and never for a freed object.

As half_passes(Bound, Mem, B, Size, Cap, Rights, Align, Passes): a half check's whole native test at the address b: the bound bd, the read-only flag for a write, and the alignment. Its inner none is for a capability that is not an object's, whose header no half check may read.

As half_res(Res0, Passes, P, Res): a half check's result from the full check's r and the native test. Where they agree it is theirs; where they disagree, the bound the validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. took as known was false: unchecked Half.

As extended_res(Res0, T, K, Res) of a loaded u: u extended from the narrow type t, as a word of class k.

As load_op_res(T, K, filc, [ptr(A, Cap)], ...) for a non-pointer load type t: the access check of the address a through the capability c (read, alignment 1), then the bytes, extended for a narrow t.

One step e of a pointer load's protocol at the address a. The state st is 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. capability read so far and the pointer being assembled (interp.pl's loaded(C, P, Mem)); a store's step has none here.

As pointer_load_effects_res(ok, Effects, A, Mem0, val(P), Mem): the pointer the protocol es loads from the address a, run from loaded(none, ptr(0, none)).

As pointer_store_effect(A, P, Effect, Mem0, Mem): one step e of storing the pointer x at the address a. Ensure, barrier and reload are identities here (no garbage collector, no aux allocation); the writes happen in list order, 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. before the primary address.

The memory after a pointer store's protocol es, each step by pointer_store_effect in turn.

As store_res(filc, Width, Mem0, ptr(A, Cap), X, Res, Mem): a store of the word x at width w to the address a through the capability c. The access check (alignment 8 for a pointer and for x, else 1, width_word/5), then its bytes, and for a pointer its capability in aux; a failed check leaves memory as it was.

The width a store of a value of class k writes, as width_bytes(K, Size) reads a class as a width; none for a proof class.

As va_cell(K, Step, Align): a va_arg of class k takes Step bytes at an Align-aligned cursor, as Fil-C's runtime does: a long double's cell is 16 bytes at 16, of which it reads its 10.

As kind_res(va_arg, _, K, filc, [P], S0, Res, S): the next variadic argument, of class k, through the va_list p. The cursor is the pointer stored at p (pointer_load_res/5); its cell is checked for reading, the cursor moves past it with an l store at p, and the value is the cell's bytes, a pointer with its stored capability for p (va_cursor_res/6 and va_checked_res/8).

What an op yields: a partial result and the memory after it, undefined behaviour (ub(Why), only an invalid float-to-integer conversion here), or a request for a fresh object and what follows from its base.

The ieee.pl format of a float class k; none for the others.

The ieee.pl condition of a comparison's condition c; none for the integer orders, which condition/2 never holds.

As op_res(cmp(C, CK), ...) at a float CK: 1 if the bit patterns a and b of format ck compare by c, else 0 (ieee_compare/5).

As float_arithmetic(Op, K, Xs, R): add, sub, mul, div, neg and copy in the float format k, on bit patterns. A copy only checks that its word is an integer.

As kind_res(float_convert, Op, K, ...): the float x converted by the op o to class k, rounded to nearest: ext(s) to any float class, ext(d) to x, truncd to s, truncx to any float class, and sqrt, the square root at k (ieee_sqrt).

As float_integer(Op, K, X, Res): the float x of format from truncated toward zero, if it is finite and fits the class k signed or unsigned, else the undefined behaviour ub(float_conversion).

As integer_source(Op, X, N): the integer an int-to-float op reads from the word x of class ik, signed or unsigned.

As kind_res/8 for the core subset's integer, pointer and checked ops: what the op o of result class k does on the words xs in the memory m, or none where the interpreter fails (arguments of the wrong form, a capability it cannot follow, or a setjmp, which kind_res/8 refuses since it does not return twice). The checks read memory and never change it; Alloc asks for an allocation.