The nanofil IR: modules of functions and data as ground Prolog terms, the contract between the frontend, the middle end, the interpreter and the backends. This module states its grammar and checks that a module is well formed.

A function is a list of blocks; a block is phis, then instructions, then one jump. Temps are ground names; logic variables never appear in IR terms.

func(Name, Linkage, Ret, Params, Blocks)
┌───────────────────────────────┐
│ entry block: first, no phis   │
└───────────────┬───────────────┘
                ▼
┌───────────────────────────────┐
│ phis    phi(tmp(D), K, Pairs) │
│ insts   let, store, call, loc │
│ jump    goto, branch, ret ... │
└───────────────────────────────┘

Classes

Every value has a class, one letter:

A store's width may also be b (8 bits) or h (16 bits). A load and ext name the narrow types sb ub sh uh sw uw: signed or unsigned byte, halfword and word.

Items

A tupleK1, K2 return is two words, each Ki l or p: a struct of 9 to 16 bytes (filc mode only).

Phis and instructions

A call's Res is one of resulttmpD, K, void, or tupleresulttmpD1, K1, resulttmpD2, K2.

Named locals are Fil-C-only. Their ground names have a separate namespace from temporaries. Each is declared once in the entry block, before its uses, and lives until this invocation exits. Functions with setjmp cannot contain them. Off is a signed 64-bit integer; an access outside [0, Size) traps, including every access to a zero-sized object. Pointer contents have ordinary capabilities, but a local's own native address is never a p value or heap lower.

flight computes its address with copy, add or sub, using unsigned 64-bit arithmetic. Each argument is an l value or addressP, the address bits of a p value. Lower is none or lowerP, exactly P's capability identity, not an integer bound. The donors may differ: constructing a pair proves nothing about access. No getter, check, memory access or safepoint occurs inside flight; both components become one rooted p result. Projections occur only here and cannot read globals or proof classes.

Jumps

A jump's target may be pollL: a pollcheck on the edge, after the phis' copies, then L. A pollcheck is a safepoint: the thread may run signal handlers and answer the collector.

Ops

The Op of a lettmpD, K, Op, Args; op_kind/2 and valid_op/1 state these sets once, op_result_ok/3 and op_arg_classes/4 the classes.

setjmpKind: Kind is setjmp, '_setjmp' or sigsetjmp, and SaveMask must be const0 except for sigsetjmp. It returns twice natively; the snapshot and restore contract is in docs/setjmp.md.

checkLo, Hi, Rights, Align reads [p P]. It traps unless P's capability permits Rights (read or write) on [P+Lo, P+Hi) and P+Lo is Align-aligned (Align one of 1, 2, 4, 8, 16); otherwise its result is P, proven accessible.

check_local proves [Off, Off+Bytes) within the named object's exact size and 16-aligned base. Its adjacent raw access has offset zero. Pointer load/store effects are respectively [aux_read, address_read] and [lower_write, address_write]: explicit stack aux has neither a heap header nor a lower box. Validation selects this protocol by proof provenance, not list shape.

Values

Data

In dataName, Linkage, Align, Items, Linkage is export, local, roexport or rolocal, ro for read-only data (in .rodata), and Align is 1, 2, 4, 8 or 16. Items is a list of:

Modes

A module is in one of two modes, told apart by what it uses (module_mode/2):

In filc mode calls may name functions outside the module, or go through a p value. A symbol globalS is read only by lettmpD, p, copy, globalS, which yields a pointer to the data or function object; S may be defined outside the module. See docs/m3.md and docs/m4.md.

Stages

A module is in one of two stages, told apart by its vocabulary:

In the checked stage a check yields a temporary of class a, a proven address, which only raw accesses read: raw_loadT, Off and raw_storeW, Off, V, A. The check that covers an access is its address operand's definition. A raw access its check does not cover is a bug of the pass, which the interpreter reports as the outcome uncheckedWhy.

Pure pointer copies, add/sub and integer-to-pointer conversion use flight in checked IR; ordinary p copy remains only for getters. The middle end runs before pizlonation. Its entry point leaves a directly supplied checked module unchanged, even with -O.

A check_function similarly yields class f, consumed only as the callee of the immediately following raw_call. It proves the target's identity, not a signature match: raw_call still selects fast or generic argument/result handling. A bad raw target reports uncheckednot_a_function; traps from that handling or from the callee remain traps. Direct calls keep call and their ABI thunks.

Pointer accesses carry the complete ordered list described by pointer_memory_effects/2. The list is executed, not an annotation. Each access is one instruction for liveness and layout, not an atomic transaction: aux_ensure may exit/re-enter or fail without returning. rooted_reload reloads the original p pair, not the ephemeral proof. The stored value also remains rooted through the whole instruction.

Neither proof class crosses an intervening safepoint (a call, a pollcheck, alloc, setjmp, va_arg or getter), since a free may make it stale. Each check is followed immediately by its one use. The pointer store's internal ensure-aux/reload sequence is the existing Fil-C exception, not permission to move another effect between the pair.

Variable names

In the predicates below: M a module, Fn a function name, K a class, V an IR value, L a label.

definitions_dominate(+Fn, +Params, +Blocks): in every reachable block, each use of a temporary is dominated by one of its definitions: a parameter, an earlier instruction or phi of the same block, or one in a block that strictly dominates it. A phi reads its value at the end of the predecessor, if that is reachable. A temporary may be defined more than once (tests/fixtures/memory.ir); one dominating definition is enough. Unreachable blocks are not checked.