The reason of a trap(Why) or an unchecked(Why), interp.pl's Why:

• the access check's: NullCapability, OutOfBounds, Misaligned, Readonly;
• a call's: NotAFunction, ArgumentSize (fewer arguments than the callee's parameters), ReturnSize (the caller expects more result words than the callee returns);
• free's: InvalidFree, DoubleFree;
• an allocation's (alloc_res/6): TooBig, OutOfMemory;
• the 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). reasons of the 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. vocabulary, which only a broken pass produces: Alias, a renew of another object; Span, a renew whose source does not cover the access; Half, a half check whose bound taken as known is false; WhyLimit, interp.pl's limit, a CheckLimit whose limit does not match.

A partial result, interp.pl's Res. The interpreter's ub(Why) comes only from float conversions and plain mode, both outside the core subset.

Success with nothing to return, interp.pl's ok.

Where an object lives: on the stack (a named local, gone when its invocation ends), on the heap, or in global data. Only a heap object may be passed to free.

Equality of kinds.

Whether an object is live or has been freed.

As region(Base, End, Kind, Life): an object of memory, the regionregion Fil-CAn object is one allocation a capability can name, its bytes what upstream calls the payload: a heap object, a named local, a data item or a variadic argument snapshot. A region is the model's record of it, region(Base, End, Kind, Life): its bounds [Base, End), its kind (stack, heap or global data) and whether it is live or freed. its capability names by its base.

The memory, interp.pl's mem(Bytes, Regions, Next, Aux) without Next.

As object_region(Base, Rs, Region): the first region of the list rs whose identity is base. Capabilities refer to registered identities; an unregistered base is outside the model.

The regions rs without the first one of identity base.

As select(Region, Rs0, Rest) on the first region of identity base, with that region replaced by r at the front, as free and the end of an invocation do; none if no region has that identity.

As aligned_res(A, Align, Res): ok if the address a is a multiple of align, else a Misaligned trap.

As readonly_access_res(Kind, A, Align, Res): the last steps of the access check in bounds of a read-only object: a write traps Readonly, and a read checks the alignment.

As cap_access_res(Cap, Rs, A, Size, Kind, Align, Res): Fil-C's access check of size bytes at the address a, with the rights r and the alignment align, through the capability c among the regions rs. The trap reasons come in the backend's order: a null capability, then the bounds, then the read-only flag for a write, then the alignment. A function's capability has zero size, so every access through it is out of bounds. An external symbol's capability gives no answer: the interpreter cannot follow it, and neither does the model.

As access_res(Mem, A, Cap, Size, Kind, Align, Res): the access check cap_access_res against the regions of the memory m.

As raw_address(A, Off, B): the address a plus the constant off, modulo 2^64.

As le_bytes(N, X, Bytes), byte i of them: the i-th lowest byte of x, counting from 0, little-endian.

As le_value(Bytes, U) of the size bytes at the address a: their little-endian integer.

As written_bytes(Xs, A, Bytes0, Bytes): the memory m with the size low bytes of x written at the address a, little-endian.

As stored_aux(cap(C), A, Aux0, Aux): the memory m whose 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. slot at the address a now holds the capability c.

The capability a pointer store left at the address a, or CNone (get_assoc(A, Aux, C) -> true ; C = none).

As object_free_res(Base, A, Mem0, Res, Mem): free of the address a through a capability of the object of identity base. Address 0 is a no-op even with an object's 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.. Otherwise it traps InvalidFree unless the object is on the heap and a is its base, and DoubleFree if it is freed already; else its region becomes empty and freed. Kind and address are validated before the free flag, as Fil-C's object_for_deallocate precedes free_impl.

As cap_free_res(Cap, A, Mem0, Res, Mem): free of the address a through any capability c. One with no object, or a function's, frees only address 0, as a no-op, and traps InvalidFree otherwise; an external symbol's gives no answer.

As free_res(P, Mem0, Res, Mem): the pinned runtime's free of the word x. An integer held at p has no capability. Runtime.v proves that it changes a region only as the lifetime axiom allows (free_lifetime).

What an allocationalloc 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). asks for: alignment, extent (the object's size in bytes) and kind, alloc_base/6's Align, Extent and Kind.

The address base may be the identity and address of a new object of the request q in the memory m: a fresh basefresh 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.. It is a positive, aligned address; it is no object's identity, live or freed; the new bytes overlap no object's current bounds; they end at or below 2^64 (Runtime.v's address_space then bounds them by 2^48, native's address space); and they read as zero with no stored capability, as Fil-C's allocations do. The interpreter never reuses an address; the model allows any choice that satisfies this. Runtime.v's fresh_allocation asks every runtime's choice to satisfy it.

Objects are what object_region finds, as everywhere else: a region behind another of the same identity is no object.

The address a rounded up to a multiple of align.

The memory m after allocating the request q at base: the same bytes and aux, with the new object's region, live, in front.

As max_allocation_size/1: Fil-C refuses a heap object of more bytes (FILC_MAX_ALLOCATION_SIZE, 2^48 - 1).

As alloc_extent/4 and alloc_align/3 in filc mode: the request of a heap object of size bytes at the alignment align. Its bounds are its size rounded up to 16, at an alignment of at least 16.

The request of a named local of size bytes: exact size, 16-aligned, on the stack.