A guide to nanofil

nanofil is a C compiler written in Prolog. It emits x86-64 assembly for Fil-C's memory-safe ABI, so its objects link with code clang builds for Fil-C. It is also an executable account of what that safety consists of: every check Fil-C makes is a term in nanofil's IR, an interpreter gives the IR a meaning, and one validator decides whether a module's checks cover its accesses.

This guide follows one small C function from source text to assembly through every stage, showing what each stage actually produces and which module and predicate produce it. After the walkthrough come the ideas you need to keep in mind, a map of the 31 modules, the concepts, recipes for common changes, and a reading order through the rest of the documentation. It assumes you know C and some Prolog, and nothing about Fil-C.

Every output block below is generated. nanofil/tests/guide.sh recomputes each block from nanofil's own commands and from tests/guide.pl, which calls the stage predicates that have no command of their own. The Nix check fails if any block differs from what the compiler now produces, so the outputs here are the current compiler's.

The pipeline at a glance

C source

c_pp:pp_file/3 ── c_lexpreprocess, lex

tokenstokT, File:Line

c_parse:c_parse/2parse

syntaxfundef/4, decl/3, at(Loc, S), bin/3 …

c_lower:c_module/2lower, asking c_types:elaborate/4 for each full expression's typed tree

unchecked IRfunc/5, data/4, context/2 (ir.pl)

ir:valid_module/1validate

opt:optimize/3-O only: inline, promote, copy, simplify, local_storage

unchecked IR, optimized

pizlonate:pizlonate_module/2make every check explicit

checked IRcheck, raw_load, flight, poll(L) …

check_reuse (--checks)reuse, renew, guard evidence

ir:valid_module/1validate the evidence

filc_abi:lower_function/5frames, roots, calls, entries

filc_amd64emit; frame_slots places slots

amd64_regs + amd64_regs_check-O: register homes, validated

asm.pl line terms

asm:print_asm/1

GNU as text

nanofil cc always takes this Fil-C path. IR text read by nanofil compile may instead be in plain mode (no p, no external call; ir:module_mode/2, below), and then goes to amd64:module_asm/2, the plain SysV backend. The diagram is the order of the stages, not of the calls: filc_amd64 drives the last three, fusing each check with its access before it asks filc_abi for the plan, and amd64_regs runs its own checker. The interpreter, interp:run/5, can run any IR module at any point on this path. The tests use it as the oracle the native code is compared with.

The walkthrough

Setting up

The commands below run from nanofil/docs/guide, with the tools from AGENTS.md:

export SWIPL=/tmp/swipl/bin/swipl FILCC=/tmp/filcc/bin/clang
cd nanofil/docs/guide
../../bin/nanofil cc-ir list.c </dev/null

bin/nanofil runs src/main.pl on SWI-Prolog. FILCC names Fil-C's clang. nanofil uses it to learn the target's predefined macros and include paths and, in the build harnesses, to assemble and link, but never to compile the program.

The program

docs/guide/list.c sums a linked list. sum has one load of an int and one load of a pointer in a loop, which is enough to show both kinds of access check, a pointer load's extra work and the safepoint every loop must have. three is there so the interpreter has something to run at the end.

struct node

int

value

struct node

*next

int sumstruct node *n IR

int s ≔ 0

while n

s += n→value

n ← n→next

return s

int threevoid IR

struct node c ≔ 3, 0, b ≔ 2, &c, a ≔ 1, &b

return sum&a

1. The driver: main.pl

main/0 reads the options. -O selects the middle end, and each of --registers, --branches, --checks, --memcpy, --inline and --simplify can be chosen on its own, with defaults that depend on -O. GNU vector types are on by default; --no-vectors (or --vectors=off, NANOFIL_VECTORS=0) refuses them. It then calls command/4main.plcommand+Opt, +Registers, +Checks, +ArgsdetRuns the command Args, [Command|Operands], such as [cc, File]; the header comment's table lists the commands. Opt is the middle end's selection: o0 without -O, else o1, o1(Inline) or o1(Inline, full) (opt.pl). Registers is the emission choice emit(Registers, Branches, Copies), and Checks the check passes (checks_module/3). Only native emission needs Register…. For cc FILE that is:

command(Opt, Registers, Checks, [cc, File]) :- !,
    c_file_module(File, Module0, AsmLines),   % frontend, then valid_module/1
    release_stacks,
    once(optimize(Opt, Module0, Module)),     % opt.pl; o0 does nothing
    release_stacks,
    mode_print_asm(filc, Registers, Checks, Module),
    forall(member(Line, AsmLines), format("~w~n", [Line])).

mode_print_asm/4 calls checked_module/3, which pizlonates the module, validates it, and runs the check passes --checks selects. filc_module_emit/3 then prints the assembly one item at a time. The other commands (cc-ir, tokens, check, print, compile, run, difftest) stop at an earlier stage or start from IR text. They are listed at the top of main.pl, the impure driver. check FILE validates hand-edited IR, checked or not, and prints ok or the validator's complaint. It is a plain file, not a module, so it has no exports.

2. Preprocessing and lexing: c_pp.pl, c_lex.pl

c_pp:pp_profile/2 asks $FILCC once for its predefined macros (-dM -E) and its #include <...> search path. c_pp:pp_file/3 then does all of the preprocessing itself: includes, macros with hide sets, conditionals (whose #if expressions it hands to c_types' constant-expression evaluator), #pragma once and push_macro. It lexes each resulting preprocessing token with c_lex and keeps the location of the token it came from. The result is a list of tokT, File:Line. Line 9, s += n→value;, comes out as:

tokids, 'list.c':9

tokp+=, 'list.c':9

tokidn, 'list.c':9

tokp(->), 'list.c':9

tokidvalue, 'list.c':9

tokp(;), 'list.c':9

nanofil tokens FILE prints the same tokens without their locations. The token forms are tabled in c_lex.pl's header, and preprocessing tokens and the preprocessor's environment in c_pp.pl's.

3. Parsing: c_parse.pl

c_parse:c_parse/2 is a DCG over the token list that produces a list of items. Its only semantic state is the set of typedef names in scope, which C's grammar needs in order to tell declarations from expressions. Everything else (types, constants, tags) is resolved later. sum parses to:

fundef'list.c':6, tspecint, dclsomesum, funcbase, paramsparamsustruct, somenode, none, [], dclsomen, ptrbase, [], none, fixed, none, at'list.c':6, blockdecl'list.c':7, tspecint, initdclsomes, base, none, num0, none−other, at'list.c':8, whileidn, at'list.c':8, blockat'list.c':9, exprassign+=, ids, arrowidn, value, at'list.c':10, exprassign=, idn, arrowidn, next, at'list.c':12, returnids

Declarators are built around the atom base, which stands for the type the specifiers give: n's ptrbase, [] means "pointer to whatever struct node is". Statements are atLoc, S so that every later stage knows its line. The full grammar of items, declarators, specifiers, statements and expressions is in c_parse.pl's header.

4. Types and elaboration: c_types.pl

c_types.pl is C's type system as relations: specifiers and declarators become type terms (ptrT, structId, funcRet, Params, Arity, ...), and from those come sizes, layouts, the integer conversions and the values of constant expressions. Its central relation is elaborate/3, which reads a C expression in an environment and gives its typed tree. Lowering asks elaborate/4 (the same with a location, raising C's diagnostic when the expression cannot be typed) for each full expression it meets. For the two assignments in the loop it gives:

% assign+=, ids, arrowidn, value

valint, assign+=, objint, ids, valint, loadobjint, memberobjstruct0, derefvalptrstruct0, loadobjptrstruct0, idn, value

% assign=, idn, arrowidn, next

valptrstruct0, assign=, objptrstruct0, idn, valptrstruct0, loadobjptrstruct0, memberobjstruct0, derefvalptrstruct0, loadobjptrstruct0, idn, next

The tree states what C leaves implicit. The category is the principal functor: valType, Node for a value, objType, Place for an lvalue, and fun for a function designator. Reading an lvalue is an explicit load node, C11's lvalue conversion (6.3.2.1). n→value is memberobjstruct0, deref..., value, as 6.5.2.3p4 defines ->. struct0 is the first struct of the environment's Defs table, whose layout puts value at offset 0 and next at offset 8.

c_types is the one module documented with doc/3 facts instead of comments. Each typing rule cites the paragraph of C11 it implements, and its examples run as tests (docs/dterm.md). The same tree is folded three ways: lowered to IR by c_lower, evaluated as an integer constant by const_eval/4 (also for #if), and evaluated as an address constant for static initializers.

5. Lowering: c_lower.pl

c_lower:c_module/2 turns the items into an IR module. function/8c_lower.plfunction+Loc, +Name, +Type, +DclType, +Body, +Env₀, -Env, -FuncdetFunc is the IR for the definition of function Name, of type Type, with declarator DclType and body Body: the list [func(Sym, Linkage, RetClass, Params, Blocks), context(Sym, Records)], the function and its provenance records (provenance.pl), which function_/8 builds. Env is Env0 with what the body defined outside its own scope. Lowering is deterministic; onc… lowers one definition: every named parameter and local variable gets an alloc, hoisted into the entry block, except a variable length array's, which is allocated where its declaration is reached (C11 6.2.4p7); statements and expressions become instructions in blocks. The lowering nonterminals (stmt//2, lower//3 for values, place//3 for objects) thread one state term, stEnv, Cur, Insts, Blocks, N, Labels, Cases, Build, through a DCG as semicontext; the fields are tabled in c_lower.pl's header. nanofil cc-ir list.c prints the result:

funcsum, export, w, paramp, %v₀, blockstart, [], let%v₁, p, alloc8, const8, let%v₂, p, alloc4, const4, storep, %v₀, %v₁, storew, const0, %v₂, goto'L3', block'L3', [], let%v₆, p, loadp, %v₁, let%v₇, l, ptoi, %v₆, let%v₈, w, cmpne, l, %v₇, const0, branch%v₈, 'L4', 'L5', block'L4', [], let%v₉, w, loadsw, %v₂, let%v₁₀, p, loadp, %v₁, let%v₁₁, w, loadsw, %v₁₀, let%v₁₂, w, add, %v₉, %v₁₁, storew, %v₁₂, %v₂, let%v₁₃, p, loadp, %v₁, let%v₁₄, p, add, %v₁₃, const8, let%v₁₅, p, loadp, %v₁₄, storep, %v₁₅, %v₁, goto'L3', block'L5', [], let%v₁₆, w, loadsw, %v₂, ret%v₁₆

This is nanofil's IR, which ir.pl defines. A function is funcName, Linkage, Ret, Params, Blocks, and a block is blockLabel, Phis, Insts, Jump. Every value has a class: w and l are 32- and 64-bit integers, s and d floats, and p a pointer, which in Fil-C carries a capability. v1 is the 8-byte slot of the parameter n and v2 the 4-byte slot of s. while n became the loop L3/L4 with exit L5. n→value is a loadp of n's slot followed by a loadsw (a signed word) at the pointer read, and n→next is an add of 8 and a loadp. In this unchecked IR a load at a p address means "Fil-C's check, then the access"; no check is written yet.

cc-ir also prints a contextsum, Records item after the function, left out above. It is explanatory metadata (provenance.pl): which C declaration and which typed tree node each temporary and instruction came from. Its first records:

origin0, at'list.c', 6, statementfunction, []

bindingv1, n, ptrstruct0, at'list.c', 6

origin1, at'list.c', 6, statementblock, 0

origin2, at'list.c', 7, statementdecl, 1

bindingv2, s, int, at'list.c', 7

origin3, at'list.c', 7, typedval, int, int0, 2

origin4, at'list.c', 8, statementwhile, 1

origin5, at'list.c', 8, statementloop, 4

Passes carry the context along as they rewrite, so the playground can show source lines beside optimized IR. Context never takes part in control flow or in the safety argument.

6. Validation: ir.pl

ir:valid_module/1 checks every module the frontend produces against the IR's grammar: operand and result classes (op_arg_classes/4, op_result_ok/3), labels, that each use of a temporary is dominated by a definition (definitions_dominate/3ir.pldefinitions_dominate+Fn, +Params, +BlocksdetIn 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 de…), and, in the checked stage, the evidence rules of step 9. It throws nanofil_errorMessage naming the first problem. A lowering bug therefore usually stops the compile with a validator message rather than producing wrong assembly.

7. The middle end (-O): opt.pl and its passes

Without -O, the IR goes to pizlonation exactly as lowering made it. That path is the reference: the simplest translation, which every optimization is compared with. With -O, opt:optimize/3 runs a fixed sequence of passes, each an ordinary relation from module to module:

Pass	Module	Does
inline	inline.pl	inlines small `local` leaf functions (`sum` is exported, so it stays a call in `three`), in two rounds, the second with simplified callees (`inline_simplified`)
promote	promote.pl	turns allocs whose address never escapes (escape.pl) into SSA temporaries with phis
copy	copy.pl	removes copies and trivial phis
simplify	simplify.pl	folds constants and branches, removes dead code, merges blocks, strength-reduces multiplies, divides and remainders by 2^k, and reuses pure values computed in dominating blocks
local_storage	local_storage.pl	turns remaining non-escaping allocs into named locals with fixed-offset accesses

After promotion alone, n and s are phis named pr.1 and pr.2, and every load and store of their slots is a copy:

funcsum, export, w, paramp, %v₀, blockstart, [], [], goto'L3', block'L3', phi%pr₂, w, 'L4'−%v₁₂, start−const0, phi%pr₁, p, 'L4'−%v₁₅, start−%v₀, let%v₆, p, copy, %pr₁, let%v₇, l, ptoi, %v₆, let%v₈, w, cmpne, l, %v₇, const0, branch%v₈, 'L4', 'L5', block'L4', [], let%v₉, w, copy, %pr₂, let%v₁₀, p, copy, %pr₁, let%v₁₁, w, loadsw, %v₁₀, let%v₁₂, w, add, %v₉, %v₁₁, let%v₁₃, p, copy, %pr₁, let%v₁₄, p, add, %v₁₃, const8, let%v₁₅, p, loadp, %v₁₄, goto'L3', block'L5', [], let%v₁₆, w, copy, %pr₂, ret%v₁₆

After all the passes (nanofil -O cc-ir list.c), the copies are gone:

funcsum, export, w, paramp, %v₀, blockstart, [], [], goto'L3', block'L3', phi%pr₂, w, 'L4'−%v₁₂, start−const0, phi%pr₁, p, 'L4'−%v₁₅, start−%v₀, let%v₇, l, ptoi, %pr₁, let%v₈, w, cmpne, l, %v₇, const0, branch%v₈, 'L4', 'L5', block'L4', [], let%v₁₁, w, loadsw, %pr₁, let%v₁₂, w, add, %pr₂, %v₁₁, let%v₁₄, p, add, %pr₁, const8, let%v₁₅, p, loadp, %v₁₄, goto'L3', block'L5', [], [], ret%pr₂

The middle end is not re-proved on each compile. Its passes keep to rules their headers state (promote only takes allocs whose every access is in bounds, and simplify only rewrites pure operations, never a load, store, call or trap), and the tests validate them by translation: nanofil -O difftest runs every test input on the original and the optimized module in the interpreter and requires each optimized outcome to refine the original one (opt:refines/2). The playground shows each pass's real output. docs/m5.md describes the passes and their validation.

8. Pizlonation: pizlonate.pl

pizlonate:pizlonate_module/2, named after Fil-C's LLVM pass FilPizlonator, writes out the checks that unchecked IR leaves implicit. Each access becomes a check, whose result of class a is a proven address, followed by a raw access that reads it. Pointer arithmetic becomes flight, which states where the address and the capability each come from. Every edge back to an earlier block gets a pollcheck. sum after -O:

funcsum, export, w, paramp, %v₀, blockstart, [], [], goto'L3', block'L3', phi%pr₂, w, 'L4'−%v₁₂, start−const0, phi%pr₁, p, 'L4'−%v₁₅, start−%v₀, let%v₇, l, ptoi, %pr₁, let%v₈, w, cmpne, l, %v₇, const0, branch%v₈, 'L4', 'L5', block'L4', [], let%chk₀, a, check0, 4, read, 1, %pr₁, let%v₁₁, w, raw_loadsw, 0, %chk₀, let%v₁₂, w, add, %pr₂, %v₁₁, flight%v₁₄, add, address%pr₁, const8, lower%pr₁, let%chk₁, a, check0, 8, read, 8, %v₁₄, let%v₁₅, p, raw_load_pointer0, aux_read, lower_resolve, address_read, %chk₁, gotopoll'L3', block'L5', [], [], ret%pr₂

check0, 4, read, 1 traps unless pr.1's capability allows reading bytes [0, 4) at it. Its proof chk0 is the only thing the raw_loadsw, 0 after it may read. Like filcc (needToCheckAlignment), nanofil checks alignment for pointer slots, atomics and vectors (accessK, A, Size, Align at the least of the ABI alignment, the access size and 8), and checks plain integer and float scalars at alignment 1, as here (ir:access_size_align/3).
flight%v₁₄, add, address%pr₁, const8, lower%pr₁ is &n→next: its address is pr.1's plus 8, and its capability ("lower") is pr.1's. Pizlonation states both; the backend emits them and infers neither.
The pointer load reads an 8-aligned slot (check0, 8, read, 8), and its effect list [aux_read, lower_resolve, address_read] spells out how Fil-C finds a pointer's capability in memory: in the object's aux array, not beside the address (ir:pointer_memory_effects/2ir.plpointer_memory_effects?Access, ?EffectsnondetEffects is the closed, ordered protocol of a pointer access of kind Access: load, store, local_load, local_store, atomic_load, atomic_store or cas. For an ordinary heap load, aux_read reads the encoded lower (or none) and lower_resolve unboxes it without taking the box's address. A store ensures aux (may exit), barriers the value's lower (may call, cannot ex…).
gotopoll'L3' is a pollcheck on the back edge: a safepoint where the thread answers the collector. Every cycle of a checked function must contain one.

Pizlonation is deliberately naive: one check right before each access (a vector's accessK, A, Size, Align becomes one full-width check and a touch before its chunks), and a poll on every backward edge. docs/pizlonation.md is the contract.

9. Check evidence and the validator: check_reuse.pl, ir.pl

After pizlonation, --checks selects how much of that naivety to undo (checks_module/3main.plchecks_module+Checks, +Checked₀, -CheckeddetChecked is the checked module Checked0 after the check passes of Checks (--checks; docs/m7.md): reference keeps pizlonate's naive checks; reuse deletes a check an earlier live one covers; renew also replaces a dominated check by a test of only the free and read-only flags; guard also puts a span test before a loop and makes its checks renew_if; combined, the… in main.pl; docs/m7.md):

`--checks=`	Does	Default
`reference`	every check stays	without `-O`
`reuse`	deletes a check whose access an earlier, still-valid heap check already covers
`renew`	reuse, then replaces a check dominated by an earlier check of the same pointer with a `renew` that tests only the free and read-only flags
`guard`	renew, then puts a `span_test` before a loop and turns its checks into `renew_if`
`hoist`	renew, then puts a `limit` before a loop and turns its full checks of a root defined before it into `check_limit` (bounds.md)
`forward`	reuse that also serves pointer loads and covers a check by the hull of its object's live facts, then renewal at any distance; moves no trap (forward.md)
`schedule`	renew, then widens a check over the bytes every path ahead needs from its base (`check_ahead`) and renews what it covers at a distance; may trap earlier, as filcc -O2 does (schedule.md)
`half`	renew, then turns a check whose object an earlier dominating check proved at another range into a `half_check` that tests only the unknown bound (half.md)
`combined`	forward, then half checks; `-O` also shares null tests and uppers between checks of one object (`--share=upper`, perf.md item 17)	with `-O`

Each pass's result must pass its *_refines/2 check, which confirms that only checks changed. Then valid_module/1 checks the evidence again with its own rule, without trusting the pass. In sum, renewal finds nothing to do: each iteration checks a different n, and the two checks in a block cover disjoint bytes.

% unchanged

The validator's rule is the centre of nanofil's safety argument. In a checked function (ir:stage_func/6, ir:checked_insts/5ir.plchecked_insts+Insts, +Fn, +Mode, +Live, -LiveOutdetEach check in Insts is followed by an access it covers, its first use, so no safepoint can come between them; no other instruction accesses memory unchecked. Live are the heap proofs live(Q, P, Lo, Hi, Rights, Align) whose evidence still holds (docs/m7.md): a later scalar raw access may read one that covers it. An instruction that is not evidence_preservin…), every raw access must read a proof that covers its bytes, alignment and rights, and that proof must still be valid: no instruction between them may free memory or reach a safepoint (evidence_preserving/1). Evidence crosses a block edge only if every incoming edge carries it; a poll edge carries none, and neither does an edge from a block not yet processed in block order (checked_block/6). Only heap checks make live evidence; check_local proves its access and nothing after it. Weaken one check of sum so it covers 2 bytes instead of 4, and the validator refuses the module:

% let%chk₀, a, check0, 2, read, 1, %pr₁

in sum: check tmp(chk0) is not followed by an access it covers

Deleting the check instead fails earlier: the load then reads an undefined temporary, and reading the pointer pr.1 itself is a class error (p used as a). nanofil check FILE reports either on hand-edited IR.

Whatever produced the checked IR (pizlonation, the check passes, or a future proof search), it is accepted only if this rule accepts it. What that does and does not establish is in Ideas to hold.

10. ABI lowering: filc_abi.pl

filc_abi:lower_function/5 turns a checked function into a plan for the Fil-C calling convention before any instruction is chosen: the frame's slots and GC roots, the entry and exit actions, each call's word layout, and the function object and origins the runtime reads. The plan below is the -O module's: pr.1 and pr.2 exist only after promotion, so §11's no--O listing has none. For sum, the frame and entry actions are:

framestoragescalar, 0, storagescalar, 1, storagescalar, 2, storagepointer, 0, storagepointer, 1, shadow'pr.1', shadow'pr.2', thread, aux, lowerstoragepointer, 0, lowerstoragepointer, 1, lowershadow'pr.1', %pr₁−storagepointer, 0, lower%pr₁−lowerstoragepointer, 0, %pr₂−storagescalar, 0, %v₀−storagepointer, 0, lower%v₀−lowerstoragepointer, 0, %v₁₁−storagescalar, 1, %v₁₂−storagescalar, 2, %v₁₄−storagepointer, 1, lower%v₁₄−lowerstoragepointer, 1, %v₁₅−storagepointer, 0, lower%v₁₅−lowerstoragepointer, 0, %v₇−storagescalar, 1, %v₈−storagescalar, 2

native_frameregisters, stack_check, save_thread, save_returnregisters, zero_roots3, push_framec, receiveregisters, wfl, %v₀, wfl, lower%v₀, snapshots[], shadow'pr.1', shadow'pr.2', %pr₁, %pr₂, %v₀, %v₁₁, %v₁₂, %v₁₄, %v₁₅, %v₇, %v₈

framePlain, Roots, Aliases: Plain lists the frame's slots, Roots the lowers[] entries the collector scans, and Aliases which slot each temporary uses. A p temporary takes two words, its address in a pointer slot and its capability in that slot's lower... root, so every live capability is somewhere the GC can see. zero_roots3 clears the three roots before push_framec links the frame into the thread's frame list. receiveregisters, ... takes the parameter n as two words, wfl, %v₀ its address and wfl, lower%v₀ its lower. A pointer argument to a call is laid out the same way, invokeentryg, Sig, registers, wfl, addrtmpP, wfl, lowertmpP; a direct call to a global needs no check_function, only a call through a pointer does. shadow'pr.1' is the slot of the phi pr.1's shadow: each incoming edge first writes every incoming value to its phi's shadow and then copies the shadows into the phis, a parallel copy. Temporaries whose live ranges do not overlap share slots (frame_slots.pl): pr.1, v0 and v15 all use storagepointer, 0.

11. Emission: filc_amd64.pl, asm.pl

filc_amd64.pl places the plan's words in the frame and selects instructions, producing a list of asm.pl line terms (insmov, q, ..., labelS, directives), which asm:print_asm/1 prints as AT&T text. Before it asks filc_abi for the plan, it fuses each check with the access after it (fusedCheck, Access), so the two are emitted together. In the reference emission (nanofil cc list.c, no -O), every temporary lives in a frame slot. Here is the start of block L4, reading s from its alloc:

.Lsum.L4:
	movq -48(%rbp), %rax
	movq -88(%rbp), %rcx
	testq %rcx, %rcx
	jz .Lsum..fail.4.0.1
	cmpq %rcx, %rax
	jb .Lsum..fail.4.0.1
	movq -16(%rcx), %rdx
	subq $4, %rdx
	jb .Lsum..fail.4.0.1
	cmpq %rdx, %rax
	ja .Lsum..fail.4.0.1
	movl (%rax), %eax
	movq %rax, -8(%rbp)

The pointer is in %rax and its capability (the object's lower) in %rcx. A null capability fails, an address below the object fails, and the upper bound, stored 16 bytes below the lower, must leave room for 4 bytes. Each failure jumps to a block that calls the runtime's filc_optimized_access_check_fail with a static description of the check. For a pointer access, the emitted check also tests alignment (testb $7, %al).

12. Register homes and their checker: amd64_regs.pl, amd64_regs_check.pl

With -O, --registers=pointers is the default. The emitter first produces a stack-homed stream, in which every temporary has a frame home: it has -O's instruction and branch selection and a save slot per callee-saved register, so it is not the no--O emission of §11 (note the missing borrow test below), though amd64_regs_check calls it the reference stream. amd64_regs:regs_asm/6amd64_regs.plregs_asm+Mode, +Metadata, +Before, -After, -Checked, -ReportdetMode is map (3a's map alone, unchecked, for a layout choice; Final is then not to be emitted) or frame(Cells) (step 3a, then step 3b's operand rewrite with the frame cells of docs/perf.md 5a-loads). Metadata is regs_metadata(Setjmp, Impl, Homes, Saves) with a save slot for every callee-saved register. Checked is the metadata and map the checker validated: ch… then proposes a map from homes to registers: callee-saved rbx and r12–r15 for homes live across a call, and r10 and r11 as well for the others. Pointer address words may get registers, but a lower never does. amd64_regs:regs_asm/6amd64_regs.plregs_asm+Mode, +Metadata, +Before, -After, -Checked, -ReportdetMode is map (3a's map alone, unchecked, for a layout choice; Final is then not to be emitted) or frame(Cells) (step 3a, then step 3b's operand rewrite with the frame cells of docs/perf.md 5a-loads). Metadata is regs_metadata(Setjmp, Impl, Homes, Saves) with a save slot for every callee-saved register. Checked is the metadata and map the checker validated: ch… itself calls amd64_regs_check:check_regs/5amd64_regs_check.plcheck_regs+Metadata, +Map, +Before, +After, +AnalysissemidetAs check_regs/4, with the effects, CFG and home liveness of Before's implementation body already computed by body_analysis/3 (the driver computes it once and shares it with the allocator). The analysis must be of that very body and cover every mapped home; liveness bits are independent per home, so extra homes change nothing., which rebuilds the stream the map implies and checks that every mapped register holds its home's value wherever the reference could read it. A failed check stops the compile; nanofil never falls back to unchecked output. A second untrusted step follows the map: amd64_regs:operands_rewrite/4 (docs/perf.md step 3b) forwards values and lets instructions read and write registers directly, and amd64_regs_check:check_operands/4amd64_regs_check.plcheck_operands+A, +B, +Lives, +CellssemidetAs check_operands/3, with frame cells (docs/perf.md, 5a-loads). Cells is cells(Ds, Others): the rbp displacements of the 8-byte frame words the emitter lists as cells, and the Disp-Bytes ranges of the other frame storage (locals, wide and save slots) they must stay apart from. Stores to cells stay paired lines, so frame memory is the same in A and B at every… validates it. The loop below shows both steps' work: movq %rbx, %rax and movl (%rax), %r10d are the rewrite's. Two kinds of function keep the stack-homed stream: those that call setjmp (excludedsetjmp) and those whose stream the preflight refuses (excludedunsupported). A function with more than 16 scalar homes is lowered twice, and the first map decides how slots are pooled (filc_amd64:temps_first/5filc_amd64.pltemps_first+Homes, +Symbols, +Branches, +Item, -Firsttemps mode's first lowering, with a home per w/l temporary. First is placed(Lines, Report) when it has at most own_frame_limit/1 such homes, else again(Groups, Fused, Ranges) with each temporary's group for the second lowering, from a function-mode (3a) allocation of the first, and the fused blocks and live ranges the second reuses (the groups change only wh…). The map for sum, where allocated8, 2 means 8 homes mapped and 2 callee-saved registers saved (rbx and r12, as the prologue shows):

% allocated8, 2

home-8, w → r12

home-16, l → r10

home-24, w stays in the frame

home-32, w → r10

home-40, w → r10

home-72, a → r11

home-64, w → r10

home-48, a → rbx

home-56, a → r11

root-168, 40 the frame record, never a home

homeD, Classes is the 8-byte frame word at D(%rbp) and the classes of the temporaries that share it (a is a pointer's address word). The frame record at -168(%rbp), which holds lowers[], is a root range, and the checker refuses any map that would put a home there. The resulting -O assembly begins with the prologue:

pizlonatedFIP1066_sum:
	pushq %rbp
	movq %rsp, %rbp
	subq $176, %rsp
	cmpq %rsp, (%rdi)
	jae filc_stack_overflow_failure@PLT
	movq %rbx, -96(%rbp)
	movq %r12, -104(%rbp)
	movq %rdi, -80(%rbp)
	xorl %eax, %eax
	movq %rax, -152(%rbp)
	movq %rax, -144(%rbp)
	movq %rax, -136(%rbp)
	movq 16(%rdi), %rax
	movq %rax, -168(%rbp)
	leaq .Lsum..origin_c(%rip), %rax
	movq %rax, -160(%rbp)
	leaq -168(%rbp), %rax
	movq %rax, 16(%rdi)
	movq %rcx, -152(%rbp)
	movq %rdx, %rbx
.Lsum.start:

The prologue checks for stack overflow against the limit the thread holds (cmpq %rsp, (%rdi)), saves the callee-saved registers the map uses, zeroes the roots, and pushes the frame record (parent, origin, lowers[]) onto the thread's frame list at 16(%rdi). The loop follows:

.Lsum.L3:
	cmpq $0, %rbx
	movq %rbx, %rax
	je .Lsum.L5
.Lsum.L4:
	movq %rbx, %rax
	movq -152(%rbp), %rcx
	testq %rcx, %rcx
	jz .Lsum..fail.4.0.1
	cmpq %rcx, %rax
	jb .Lsum..fail.4.0.1
	movq -16(%rcx), %rdx
	subq $4, %rdx
	cmpq %rdx, %rax
	ja .Lsum..fail.4.0.1
	movl (%rax), %eax
	leal (%rax,%r12), %r10d
	leaq 8(%rbx), %rax
	movq -152(%rbp), %rcx
	movq %rcx, -144(%rbp)
	movq -16(%rcx), %rdx
	subq $8, %rdx
	cmpq %rdx, %rax
	ja .Lsum..fail.8.0.8
	testb $7, %al
	jnz .Lsum..fail.8.0.8
	movq -8(%rcx), %rdx
	movabsq $281474976710655, %rsi
	andq %rsi, %rdx
	jz .Lsum.L4..3.nolower
	movq %rax, %rsi
	subq %rcx, %rsi
	movq (%rdx,%rsi), %rsi
	testb $1, %sil
	jz .Lsum.L4..3.have
	andq $-2, %rsi
	movq 8(%rsi), %rsi
	jmp .Lsum.L4..3.have
.Lsum.L4..3.nolower:
	xorl %esi, %esi
.Lsum.L4..3.have:
	movq (%rax), %rbx
	movq %rsi, -152(%rbp)
	movq %rsi, -136(%rbp)
	movq %rsi, -152(%rbp)
	movq -80(%rbp), %rax
	testb $14, 8(%rax)
	movq %rsi, %rcx
	movq %rax, %rdi
	movq %rcx, %rax
	movl %r10d, %r12d
	jz .Lsum.L4..j.poll
	leaq .Lsum..origin_n(%rip), %rsi
	call filc_pollcheck_slow@PLT
.Lsum.L4..j.poll:
	jmp .Lsum.L3
.Lsum.L5:

s stays in %r12 and n's address in %rbx, while n's lower is reloaded from its frame slot at -152(%rbp), which is a root. The int load's check is the same as before, without the borrow test, which checks of at most 16 bytes do not need (docs/perf.md item 6a). The pointer load's check of n→next tests only the upper end: the int load's check just before proved n's object not null and its address at or above lower, so -O's combined checks make it a half check (docs/half.md). The pointer load reads the aux word at -8(%rcx). If the object has an aux array, it takes the loaded pointer's lower from the matching aux slot, unboxing it when the low bit says it is boxed. An object without aux gives a null lower (the .nolower path, xorl %esi, %esi). Then it loads the address. Before the back edge, testb $14, 8(%rdi) asks whether the thread has a pending safepoint request and calls filc_pollcheck_slow if it has.

The rest of the output (not shown) is the function's public face: the pizlonated_sum getter, a generic entry for callers that do not know its signature, and the function object whose address C code takes. 1066 in pizlonatedFIP1066_sum encodes the signature intptr (filc_abi:signature/3filc_abi.plsignature+Ret, +ParamKs, -SigdetSig is Fil-C's fast-call signature number for a function returning Ret (a class, void or tuple([K1, K2])) on parameters of classes ParamKs: 1 + R + 133 * A, R and A the bijective base-11 encodings of the return and argument word digits, independent of native locations. More than 16 argument words have no fast signature, and get never_signature/1. It names pr…).

13. Running it: interp.pl

interp.pl is the IR's meaning: a relation from a module, a function, arguments and fuel to an outcome (retV, trapReason, ubReason, unchecked(Why), ...). Integer arithmetic is CLP(Z), so arguments may be unknown and the relation can search for inputs. Memory, capabilities, free and Fil-C's traps are modelled concretely.

$ nanofil run list.c three
ret 6
$ nanofil -O run list.c three
ret 6

The tests compare three things on the same inputs: the interpreter, the native code nanofil emits, and for C files the native code clang emits (nanofil difftest, tests/difftest.sh, tests/progtest.sh). A raw access whose proof does not cover it runs to unchecked(Why), an outcome distinct from both a trap and undefined behaviour, so a missing check shows up as a mismatch. An asm_fixed instruction the interpreter cannot model stops at unknownasmM, Xs, which difftest reports as not comparable (docs/asm-fixed.md).

The interpreter's trap reasons are coarse: past the end, below the start, freed, and a function object all trap as out_of_bounds. So difftest compares trap kinds, and the exact reason text is compared natively: progtest against filcc, and tests/renew-trap.sh.

Ideas to hold

The IR is the contract

ir.pl's term grammar is what the frontend writes, what the interpreter runs, what the passes transform and what the backends compile. Its header is the reference for every term. Three properties are worth memorising:

Ground terms in SSA. Temporaries are tmpName with ground names, each use dominated by a definition (definitions_dominate/3ir.pldefinitions_dominate+Fn, +Params, +BlocksdetIn 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 de…). The validator allows a temporary several definitions; the middle end works on strict SSA, one definition each (promote:strict_ssa/3). No logic variable appears in IR. A module is ordinary data you can print (ir_text.pl), read back, and compare.
Classes. w l s d x are scalars, p is a pointer with its capability, and the checked stage adds a (a proven address) and f (a proven function). They are never parameters, phis, call arguments or stored values. A raw access reads a proof only while its evidence is live; a renew may also name an earlier dominating check's proof, for its bounds only.
Mode and stage are read off the vocabulary. A module is in filc mode if it uses anything Fil-C-specific (a p, a call to an external function, ...), otherwise in plain mode (ir:module_mode/2). It is in the checked stage if it contains any check, raw access, flight or poll edge, otherwise unchecked (ir:module_stage/2). No flag can disagree with the contents.

Address is not authority

A Fil-C pointer is two words: the address, and a lower, the address of the first byte of the object it may access. The object's header sits in the 16 bytes below the lower: its upper bound, and a word holding its flags (freed, read-only, ...) and its aux array. Computing an address never conjures a capability. flight makes the two sources explicit, and integer-to-pointer conversion gives a null capability unless the integer is laundered. In registers, the pair travels together. In memory, the address is stored in the object and the lower in the object's aux array, which is why a pointer load or store has an effect list (ir:pointer_memory_effects/2ir.plpointer_memory_effects?Access, ?EffectsnondetEffects is the closed, ordered protocol of a pointer access of kind Access: load, store, local_load, local_store, atomic_load, atomic_store or cas. For an ordinary heap load, aux_read reads the encoded lower (or none) and lower_resolve unboxes it without taking the box's address. A store ensures aux (may exit), barriers the value's lower (may call, cannot ex…). On the stack, lowers live in the frame record's lowers[], which the collector scans. docs/abi-findings.md records how each of these was established against the pinned Fil-C.

Checks, proofs and one validator

Fil-C's safety obligation is that every access is allowed by its pointer's capability. nanofil separates the requirement (this access needs read rights on these bytes), the evidence that discharges it (a check just before it, or an earlier check that still holds), and the implementation (the instructions the emitter writes for the check). In checked IR, evidence is structural: a raw access names its proof temporary, and valid_module/1 decides whether that proof covers it and is still valid. Every producer of checked IR, now and in future, must get its output past that one rule.

Be precise about what this gives. The validator checks each module against a rule. That the rule is sound (that validated checked IR never reaches unchecked in the interpreter) was first an argument made in docs/pizlonation.md and docs/m7.md and tested by mutation; it is now proved in Rocq (soundness, valid_no_unchecked in Soundness.v) for the core subset, under the runtime axioms, of Validate.v's transcription of the rule. That the transcription is the rule is checked by agreement with valid_module/1 on every core-subset mutant of the corpus, not proved. That the emitted assembly does what the checked IR says, and that the runtime keeps its side of the bargain, are separate claims, supported by differential and native tests. docs/campaign.md states these three obligations and keeps them apart, and the README is careful in the same way.

Safepoints and GC roots

Fil-C's collector runs concurrently and asks each thread to stop at safepoints: pollchecks, calls, allocations, and a few helpers that may exit to the runtime. Two rules follow, and nanofil enforces both structurally:

A proof dies at a safepoint. A call can run code that frees the object, and so can a pollcheck, through a deferred signal handler (the collector itself never frees a reachable object). So no raw access may use a proof across one: the validator ends all live evidence at any instruction that is not evidence_preserving/1. Two forms are exceptions, because they test again what a free changes. An object's bounds change only by free, which sets its upper to its lower, and the flag test catches that.
- renew names an earlier check's proof for its bounds. The check and its pointer have one definition each and dominate the renew, the renewed pointer is at a constant distance from the checked one through one base, the check's span covering the renew's shifted by it (pointer_distance/4; distance 0 is same_pointer/3ir.plsame_pointer+Once, +P, +P₁semidetAt any point both P and P1 dominate, they hold the same address and capability: both reach one single-definition base B through guard_chain/3 at point offsets equal modulo 2^64 (P == P1 included). After B's last execution before that point, each definition on either chain ran again, since each dominates it and B dominates each, so both were computed from B's…), and the function has no setjmp. It tests the freed and read-only flags again.
- renew_if reads a guard's span_test result G instead of live evidence. The validator accepts it through guard_covers/5 (single-definition G and P0, and the access inside the span), so it holds across the calls and polls in the loop. It tests the flags and the alignment, and when G failed it runs the full check out of line.
Every live capability is a root at every safepoint. The ABI plan gives each live p a lowers[] entry in the frame record. The register checker refuses any home that overlaps the record, so registers never hold the only copy of a lower. A function that calls setjmp keeps the reference emission (docs/setjmp.md).

Every cycle of a checked function must contain a poll edge (polls_every_cycle/1), so a loop cannot keep the collector waiting.

Plain and -O

Every -O choice is independently selectable, and its absence is the reference path, which is the simplest correct translation:

Choice	Reference (no `-O`)	`-O` default	How the `-O` choice is checked
middle end	none	inline, promote, copy, simplify, local_storage	interpreter refinement per test input (`difftest -O`); the passes' own preconditions
`--checks`	`reference`	`renew`	`*_refines/2` and the validator, on every compile
`--registers`	`stack`	`pointers`	`amd64_regs_check`, on every compile
`--branches`	`reference`	`selected`	differential and native tests
`--memcpy`	`call`	`inline`	differential tests; the inline copy is taken only when the runtime's checks would pass

tests/snapshot.sh compares every output of a change with the previous revision's, byte for byte, in the reference and in fixed -O modes. A refactoring must leave the snapshot unchanged.

Trusted and checked

On every compile	By the tests	Trusted
IR well-formedness, SSA dominance and class rules (`valid_module/1`)	the frontend against clang on every test and corpus program	that Validate.v transcribes the evidence rule (compared on every core-subset mutant), the runtime axioms its soundness proof rests on, and the rule outside the core subset (argued and reviewed)
checked-IR evidence: every raw access covered by a live proof, every cycle polled	the middle end, by interpreter refinement	the emitter's check, pointer-access and call sequences (reviewed against Fil-C's, tested natively and under `FUGC_SCRIBBLE`/`FUGC_VERIFY`)
check passes change only checks (`*_refines/2`)	pizlonation, by agreement of unchecked and checked runs in the interpreter	the ABI facts in docs/abi-findings.md
register homes hold their values, and no home overlaps a GC root (`check_regs`, `check_operands`)	the emitted code against the interpreter and clang (difftest, progtest, whole programs)	the root ranges the emitter reports to the register checker
		the emitter's home classes, and that only `%rbp`-relative operands reach a home, so homes and save slots never escape
		amd64_contract's audited instruction effects (a form it does not know fails)
		the Prolog host, the assembler, the linker and the Fil-C runtime

The module map

The 31 modules of nanofil/src, in pipeline order. Each module's header is the full statement of what it owns. These paragraphs say where it sits and what to read next. On the Pages site each module is drawn as terms, with its predicates' documentation.

Driver

main.pl: the command line. It parses options, runs the stages for a command, and prints. It owns the option defaults (registers_default/2main.plregisters_default+Opt, ?RegistersdetRegisters is the register mode for optimization level Opt (o0 or o1) when no --registers option or NANOFIL_REGISTERS chose one: stack, the reference emission, without -O, and pointers, a home per scalar temporary and per pointer address word (amd64_regs.pl), with it. branches_default/2 does the same for branch selection: reference without -O, selected with i… and the others), checked_module/3, and difftest's three-way validation (mode_pizlonation_agrees/5main.plmode_pizlonation_agrees+Mode, +Checks, +File, +Module−Prepared, +RunsdetFor a filc module, the checked Module (checked_module/3 with Checks) has the same outcome as Module on every run of Runs, traps and their reasons included, or the command throws: the explicit checks are exactly the implicit ones. A missing or too weak check shows as the outcome unchecked(Why). Both run with the same fuel, since pizlonate keeps every block. A…, report_validation/4). It is the impure driver, a plain file with no exports. Next: opt.pl for the middle end's selection.

Frontend

c_lex.pl: C tokens. Input is preprocessed text or single preprocessing tokens; output is tokT, File:Line. It also owns the character classes and punctuators c_pp shares, #pragma pack, and C23 keywords. Next: c_pp.

c_pp.pl: the preprocessor. Input is a file and a target profile; output is c_lex tokens with source locations. It is self-contained: clang is asked only for the profile (pp_profile/2), never to preprocess. The environment envMacros, IncludeDirs, Features, Once, File holds macros, include dirs, feature answers and #pragma once files. Next: c_parse.

c_parse.pl: the grammar. Input is tokens; output is items (declLoc, Specs, Inits, fundefLoc, Specs, Dcl, Body, ...). It tracks typedef names only. Its header is the reference for the syntax tree. Next: c_types' specs_type/4 and apply_declarator/5.

c_types.pl: C's types and typing rules as relations, documented by doc/3 with C11 citations and runnable examples. It owns type terms, layouts (type_size_align/4, su_layout), the environment eOrds, Tags, Defs, Next, the conversions, the elaborator (elaborate/3,4) and constant evaluation (const_eval/4, pp_value/2). Invariant: each C rule has one home here, and consumers read it. Next: c_lower's lower//3.

c_lower.pl: lowering to IR, in the style of cproc. Input is items; output is a filc-mode module with contextFn, Records items. Every local lives in an alloc. Expressions are lowered from typed trees (lower//3, place//3), statements by stmt//2, static initializers by folding trees to data chunks (address_constant/5c_lower.pladdress_constant+XV, +Loc, +Env₀, -Env, -RdetThe value tree XV is an address constant (C11 6.6p9), R = sym(Symbol, Offset), or a null pointer, R = null, or an integer constant cast to a pointer, R = int(Address). It is the address of a static object or a function, perhaps cast, plus or minus an integer constant; string literals and compound literals become data of their own (Env). An address built from…). It also owns the SysV eightbyte classification of struct arguments and returns, builtins (builtin//4), atomics as cas loops, vectors as 8-byte chunks, VLAs and cleanup attributes. It is the largest module; its %% sections are the way in. Next: ir.pl for what it must produce.

launder.pl: the last step of c_module/2. Gives each itop the capability of the one pointer its integer came from (launder): Fil-C's analysis, read on the SSA form promote.pl defines, with shadow slots for local integers, so the result is the same with and without -O.

The IR and its meaning

ir.pl: the IR's grammar and validator. Its header tables every term; valid_module/1 checks a module, including the checked stage's evidence rules (stage_func/6, checked_insts/5ir.plchecked_insts+Insts, +Fn, +Mode, +Live, -LiveOutdetEach check in Insts is followed by an access it covers, its first use, so no safepoint can come between them; no other instruction accesses memory unchecked. Live are the heap proofs live(Q, P, Lo, Hi, Rights, Align) whose evidence still holds (docs/m7.md): a later scalar raw access may read one that covers it. An instruction that is not evidence_preservin…). It also owns the shared facts other modules read (op_kind/2, access_size_align/3, pointer_memory_effects/2ir.plpointer_memory_effects?Access, ?EffectsnondetEffects is the closed, ordered protocol of a pointer access of kind Access: load, store, local_load, local_store, atomic_load, atomic_store or cas. For an ordinary heap load, aux_read reads the encoded lower (or none) and lower_resolve unboxes it without taking the box's address. A store ensures aux (may exit), barriers the value's lower (may call, cannot ex…, module_mode/2). Changing the grammar needs the orchestrating thread's agreement (AGENTS.md). Next: interp.pl.

interp.pl: the IR's semantics, as a relation that can run with unknown integer inputs (CLP(Z)). It owns the memory model (regions, explicit free, aux capabilities), Fil-C's trap reasons and the unchecked outcome. Every differential test uses it as the oracle. Next: docs/lifetime.md for free.

ieee.pl: IEEE binary32, binary64 and x87 extended arithmetic on integer bit patterns, for the interpreter and for constant folding. No host floats. Next: docs/float.md.

ir_text.pl: IR as Prolog clauses, read and printed with a host-independent printer; also runFn, Args facts in test files. Next: tests/fixtures.

provenance.pl: the contextFn, Records items that explain where IR came from (bindings, typed origins, sites, aliases), and the helpers passes use to carry them along. Invariant: context never participates in control flow or safety. Next: promote's promote_context/5 for how a pass maintains it.

Analyses

cfg.pl: control-flow graph, dominators, dominance frontiers, natural loops and liveness, as functions from IR to assocs. Every pass that needs them uses this module.

cfg_tabled.pl: the same analyses as tabled relations, kept to answer PLAN's question about tabling by measurement (docs/m5.md). No pass uses it.

escape.pl: which allocs are reached only through their own address at known offsets (local), for promote and local_storage.

alias.pl: each address of a strict SSA function as base plus constant offset. Its header says explicitly what the facts do not justify.

Middle end (-O)

opt.pl: the pass sequence (optimization_passes/2), one pass at a time for the playground (optimize_pass/3), and refines/2, the outcome relation that validates them. Checked modules pass through untouched.

inline.pl: inlining of small static leaf functions, with its eligibility rules tabled in the header.

promote.pl: memory slots to SSA temporaries (pruned SSA, phis named pr.N), with the exact conditions under which an alloc is promotable. Also owns strict_ssa/3, which the other passes use as a precondition.

copy.pl: copy propagation and trivial phi removal.

simplify.pl: constant folding, identities, value numbering, branch folding, dead code and block merging, all on pure values only. Its rule table is in the header.

local_storage.pl: non-escaping entry allocs that promotion left become named local objects (local_alloc, local_load, local_store), whose address is never a value. Next: docs/m5.md, Nonescaping local storage.

Checked IR

pizlonate.pl: unchecked to checked IR: one check per access (a vector's accessK, A, Size, Align becomes a full-width check and a touch before its chunks' own checks), flight for pure pointer operations, a poll on every backward edge. Next: docs/pizlonation.md.

check_reuse.pl: the evidence passes reuse, renew and guard, and their *_refines/2 checks. Next: docs/m7.md.

Fil-C backend

filc_abi.pl: the ABI plan of a checked function: frame slots and roots, entry and exit actions, call layouts, fast and generic entries, setjmp snapshots, origins and signatures. It never inserts instructions. Next: filc_amd64's Functions section.

frame_slots.pl: slot sharing by disjoint closed live intervals, in pools (pointer, scalar, float, wide, and address for derived pointers).

lower_roots.pl and lowers_check.pl: opt-in shared lowers, a flight or phi rooted through its lower root's lowers[] entry, and the checker that validates every such frame against the GC-root contract. Next: docs/lowers.md.

filc_amd64.pl: places the plan and emits instructions. Its %% sections are the map: ABI facts, frame layout, functions, blocks and jumps, instructions, the fast convention as data, access checks, function objects, data objects (getters and relocations), thread-locals, static data. Next: docs/m3.md, then docs/abi-findings.md.

amd64_regs.pl: proposes the register map for frame homes (greedy colouring weighted by loop depth) and the operand rewrite. Nothing it decides is trusted.

amd64_regs_check.pl: translation validation of the map and of the register operands, per half-register liveness on the reference stream's CFG. Its header tables the obligations. Next: docs/perf.md items 3 and 5.

amd64_contract.pl: the audited effects of each machine instruction form (registers read and written, memory, flags, control). An unknown form fails, so the checker never guesses.

Plain backend and assembly

amd64.pl: the naive SysV backend for plain-mode modules (milestone 2), and the scalar instruction selection (compute_op//5, loads, stores, conversions) that filc_amd64 reuses.

asm.pl: assembly lines as terms and the only AT&T printer.

Host support

src/swi/ maps the Trealla dialect nanofil is written in onto SWI-Prolog (swi/compat.pl) and supplies the small libraries (dcgs, format, pio, clpz) under Trealla's names. See docs/archive/hosts.md.

Glossary

Each term is a concept node in concepts/, one short page shared by the Prolog, the Rocq model and the documents. Comments and documents link to one with [[name]] and draw it in place with a line ![[name]]; an emphasized or code mention of a term links to it too.

Fil-C (18)

Concepts of Fil-C itself: they hold of any Fil-C program, whatever compiled it, and link to Fil-C's documentation and source.

alloc: An allocation: letD, p, allocAlign, 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).
aux: An object's aux allocation, as large as its payload: where Fil-C keeps the lowerslower 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 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: A 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.
check: An access check: checkLo, 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).
fast and generic conventions: Fil-C's two ways into a function, from its optimized calling convention: the fast entry takes the arguments in registers, for a caller that agrees on the signature; the generic entry takes them in the thread's CC buffers, one for bytes and one for lowers, for any caller. A function object holds both entries and a 64-bit signature, an arithmetic encoding of its type that is 0 when only the generic entry exists.
flight pointer: A flight pointer is a pointer held in a variable or register rather than in memory. It has two words: its intval, the address the C program sees, prints and computes with, which nothing trusts; and its 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., the capability, which only an allocation creates and the program can neither see nor forge. Stored to memory it becomes a pointer at rest: the intval goes in the object's bytes and the lower in the object's 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. allocation, where no capability reaches. That invisibility gives InvisiCaps their name, and it keeps sizeofvoid * at 8.
FUGC: FUGC, Fil's Unbelievable Garbage Collector, is what reclaims memory in Fil-C. It marks and sweeps on its own threads, in parallel, while the program runs, and never moves an object. It never stops the world: it asks each thread for work, such as scanning its stack, by a soft handshake, which the thread answers at its next 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).. While it marks, a store barrier marks the target of every pointer stored to the heap. It finds pointers exactly: on stacks through the roots the compiler keeps, and in objects only in their 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. allocation.
getter: A getter is the function that returns a global's or function's address with its capability, initializing it on first use. Upstream every symbol is renamed pizlonated_ plus its name, and that symbol is its getter, returning a flight pointerflight pointer Fil-CA flight pointer is a pointer held in a variable or register rather than in memory. It has two words: its intval, the address the C program sees, prints and computes with, which nothing trusts; and its lower, the capability, which only an allocation creates and the program can neither see nor forge. Stored to memory it becomes a pointer at rest: the intval goes in the object's bytes and the lower in the object's aux allocation, where no capability reaches. That invisibility gives InvisiCaps their name, and it keeps sizeof(void*) at 8.; the program checks the result like any pointer. In IR a getter call is lettmpD, p, copy, globalG; calling one is a 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). (filc_amd64:object_getter//2), so it ends every live fact, except a repeated getter.
GIMSO: GIMSO, garbage in, memory safety out, is Fil-C's promise. Fil-C's LLVM pass, FilPizlonator, gives every module a memory-safe meaning, however buggy or adversarial its code. Each operation does what C means or ends in a Fil-C panic, and no access touches bytes its capability does not cover. It does not promise that a program never panics, nor does it remove bugs that stay inside memory safety, such as integer overflow or wrong logic.
launder: Laundering gives an integer converted back to a pointer the capability of the pointer it came from, as Fil-C does when its analysis can follow the integer: through arithmetic, promotable local variables and phis, never through memory or a call, and only from one pointer (launder:launder_func/4, m4.md, Pointer-as-int laundering). Otherwise the pointer gets no capability and dereferencing it traps.
lower: The 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 pointerflight pointer Fil-CA flight pointer is a pointer held in a variable or register rather than in memory. It has two words: its intval, the address the C program sees, prints and computes with, which nothing trusts; and its lower, the capability, which only an allocation creates and the program can neither see nor forge. Stored to memory it becomes a pointer at rest: the intval goes in the object's bytes and the lower in the object's aux allocation, where no capability reaches. That invisibility gives InvisiCaps their name, and it keeps sizeof(void*) at 8.. 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 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. 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.
origin: An origin is a static record the runtime reads to name a function and source location in a trap or backtrace (filc_amd64:function_origins//3). In context records the word means something else: a typed source node (provenance.pl).
poll: A 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 pollL, 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).
region: An 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, regionBase, End, Kind, Life: its bounds [Base, End), its kind (stack, heap or global data) and whether it is live or freed.
rights: Rights 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.
root: A 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 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 a jmpbuf root (filc_abi:lower_function/5, amd64_regs_check:valid_map/3). Every live 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. is in one at every 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)., so registers never hold the only copy.
runtime: The runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGCFUGC Fil-CFUGC, Fil's Unbelievable Garbage Collector, is what reclaims memory in Fil-C. It marks and sweeps on its own threads, in parallel, while the program runs, and never moves an object. It never stops the world: it asks each thread for work, such as scanning its stack, by a soft handshake, which the thread answers at its next pollcheck. While it marks, a store barrier marks the target of every pointer stored to the heap. It finds pointers exactly: on stacks through the roots the compiler keeps, and in objects only in their aux allocation.: where a new object goes, what free does, and what the collector may change while the program waits at a 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).. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c.
trap: A trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trapReason, 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.

nanofil (84)

nanofil's own: its IR, validator, interpreter and Rocq model. Each names the Fil-C concept it builds on.

access: A vector's full-width access check: accessK, Addr, Size, Align traps as a K (read or write) access of Size bytes at Addr with alignment Align would, and moves no data. It comes before the vector's 8-byte chunks, so the vector traps as one access (vector-access.md).
address space: The address space is where objects may lie: every object within [0, 2^48], native Fil-C's bound (libpas's PAS_ADDRESS_BITS). objects_fit says this of a memory, and the runtime axiom address_space says it of every memory the runtime is ready in; the runtime may also refuse an allocation it cannot hold, and the run traps out_of_memory.
adequacy: Adequacy is the one theorem that ties a program logic to the machine: if a program's proof in the logic can be derived, then no state any of its runs reaches fails. It is proved once; after it, proving a program never panics is deriving its proof, with no reasoning about runs.
ahead-transparent: An instruction is ahead-transparent when it may stand between a check_ahead and the access whose need it checks early: it reaches no safepoint, calls nothing, cannot free, and is not a division, whose fault would end the program other than by a Fil-C trap.
asm_fixed: An inline asm statement of one fixed-register instruction: asm_fixedM, Ins, Outs runs M (cpuid, xgetbv, rdtsc, rdtscp, or the operand-free lfence, sfence and pause) on w inputs in the registers M reads, defining w temporaries from the registers it writes (ir:asm_fixed_regs/3, asm-fixed.md).
block: A 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.
campaign: A campaign is one numbered stage of nanofil's formal plan in formal.md, from Campaign 0 (measure which checks survive) to Campaign 7 (prove one program never panics). Each ends with a note in docs/ saying what it found.
cas: Compare-and-exchange, the one atomic read-modify-write term in the IR: casT reads the T at an address and, if it equals Expected, writes New there, as one sequentially consistent step. Every other atomic operation is a loop of it (c_lower:rmw//7c_lower.plrmw+U, +Addr, +Op, +V, +Ctx, -Old, -New//the atomic read-modify-write of the U at Addr, New being Old combined with the value V by Op (a binary operator, or xchg, nand, max or min): read the U, then repeat a cas of the read value for its combination until the cas finds it unchanged (ir.pl). The first read of a pointer is atomic, so the pair it combines is one; a float or double goes through its bit…).
check_ahead: check_aheadLo, 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.
class: A 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).
context: An explanatory item of a module: contextFn, 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).
core subset: The 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, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside.
covered access: A raw access is covered by a check when it lies inside the checked bytes, at an alignment the check's implies, with rights the check allows. Its own access check, which the raw access makes again without trapping, then passes too.
dominance: Block A dominates block B when every path from the entry to B passes through A. The validator decides it with the dominator tree's preorder intervals: each label gets the numbers of its subtree, and A dominates B when B's number lies in A's interval.
doomed frame: A frame is doomed after a check_ahead whose early bytes failed: the check yields its pointer anyway and the frame records the failure, because the validator promised that the frame will reach an access that fails on those bytes before anything observable happens.
elaborate: To elaborate is to read a C expression into its typed tree, the frontend's step between parsing and lowering (c_types:elaborate/3). The formal model has no counterpart: it starts at the IR. See guide.md, 4. Types and elaboration.
evidence invariant: The evidence invariant says that along every run, at the running frame's point, the live facts the evidence pass computed for that point hold: each fact's check passes in the current memory, and its pointer has a single definitionsingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. dominating the point. It is how the pass's static bookkeeping becomes a fact about runs.
evidence pass: The evidence pass is the validator's forward walk over a checked function: it tracks live facts and accepts each raw access only where its own check, a live fact or a reuse rule covers it. It visits the blocks once, in order; a block's entry facts are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited.
evidence: Evidence 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 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. form's trust: for renew a dominating check, for renew_if a guard's span test.
exact base: An exact base of a pointer P is a single-definitionsingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. name B on P's guard chain whose offset interval is one point, B−iK, K: P's address is B's plus exactly K, modulo 2^64, with B's capability.
exit facts: A block's exit facts are what a validator pass knows at its jump; its entry facts are what it knows before its phis. Two passes keep them, over the same edge rule: entry facts are the meet over incoming edges, nothing comes over a poll edge, and an edge from a block the pass has not yet reached carries nothing.
external call: An external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings.
extraction: Extraction compiles the Rocq model to OCaml so that it can be run beside the Prolog on the same inputs. judge is the extracted function that reads one run line nanofil printed, runs it in the model, and answers agree, disagree, outside or stuck_both.
flight: A flight builds a pointer from two independent sources: flightD, 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.
frame: A configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point.
fresh base: A 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.
fuel: The interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5).
global environment: The global environment is what every step of a run reads but never changes: the module, each global's pointer, and the free that a call of libc's free runs.
guard chain: A pointer's guard chain lists its bases with the offset of its address from each: P itself at i0, 0, then each base B reached through single-definition add, sub and copy flights whose lower donor is their address operand, with an interval for P's address minus B's, modulo 2^64. P has the capability of every base on its chain.
guard: Range guards, --checks=guard: a span test before a loop proves its accesses' bounds once, and the loop's checks become renew_if, which tests only the flags and alignment when the guard passed and runs the full check out of line otherwise (check_reuse:guard_checks/2, m7.md, Range guards (round 5)).
half_check: half_checkBound, 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.
home: A home is the 8-byte frame word that holds a temporary, a phi's shadow or a pointer's address word in the stack-homed stream amd64_regs starts from (guide.md, 12. Register homes). Scalar homes are w or l only; float temporaries are kept out of them.
identity: An object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object.
interpreter: The interpreter is interp.pl, nanofil's executable meaning of the IR: a relation from a module, a function, arguments and fuel to an outcome, with CLP(Z) integers so that it runs in every direction. The Rocq model transcribes it, and the outcome gate checks that the two agree on every run line of the corpus.
limit: limitSize of a pointer P0 is an opaque class-l snapshot of P0's capability and its object's bounds; check_limit0, Size, Rights, Align of [P, U] is exactly a check of P, whose bounds are tested natively against the snapshot U rather than the object's header (plus the free flag, and read-only for a write). A hoisted limit makes a loop's bounds test cheap.
live fact: A live fact liveQ, P, Lo, Hi, Rights, Align is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own.
live: A live token, live b, is permission to rely on the object of identity b not being freed. It is the temporal half of a check: the bounds come from b's metameta nanofilA meta fact, meta b n k, says that the object of identity b was allocated with extent n bytes and kind k (heap, global data, stack). It is the persistent half of owning an object in the planned program logic: once true it stays true, so it can be copied and shared freely, because nothing after an allocation changes what was allocated. With the pointer's offset from b it decides a check's bounds by arithmetic alone; whether the object is still there is the live token's part. fact, and the free flag passes as long as the token is held. Free consumes it, so whoever frees an object must own it, and an object no one else owns cannot be freed behind the owner's back. For a heap object it is exclusive, or split into fractions for readers; for global data, which is never freed, it is persistent.
lower chain: A lower chain from P to B says P carries B's capability: P is B, or a single-definition flight whose lower donor has B's lower, whatever its address.
machine: The machine of a runtime R, Machine R, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs.
meta: A meta fact, meta b n k, says that the object of identity b was allocated with extent n bytes and kind k (heap, global data, stack). It is the persistent half of owning an object in the planned program logic: once true it stays true, so it can be copied and shared freely, because nothing after an allocation changes what was allocated. With the pointer's offset from b it decides a check's bounds by arithmetic alone; whether the object is still there is the livelive nanofilA live token, live b, is permission to rely on the object of identity b not being freed. It is the temporal half of a check: the bounds come from b's meta fact, and the free flag passes as long as the token is held. Free consumes it, so whoever frees an object must own it, and an object no one else owns cannot be freed behind the owner's back. For a heap object it is exclusive, or split into fractions for readers; for global data, which is never freed, it is persistent. token's part.
mode: A module's mode is plain or filc: filc if it uses anything Fil-C-specific (a p, a call to an external function, ...), plain otherwise, read off its contents (ir:module_mode/2).
mutant: A mutant is a checked module with one item changed, inserted or deleted: a check deleted or moved, its bounds, rights or alignment changed, a raw access's offset moved by one, a free inserted between evidence and its use, a reuse form given another proof, a poll edge removed, or a data object's or alias's linkage, target or name changed. Prolog's and Rocq's validators judge each, and must agree.
name map: A name map is a finite map keyed by IR names, the model's counterpart of SWI-Prolog's library(assoc), which ir.pl and cfg.pl use for every table indexed by a label or a temporary: the single-definition map, the evidence indexes, dominator intervals.
near offset: A near offset is one within 2^62 of 0. The validator's offsets between pointers (guard chains, pointer distances) are exact only modulo 2^64, because address arithmetic wraps; for a near offset the integer is the true signed distance, so the validator counts only near ones where it compares positions.
need: A 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.
obligation: An obligation is something a proof leaves to be shown or trusted elsewhere, named rather than assumed away. A realization obligation is the trusted claim that native code realizes a logical model: that pinned libc's FILE, buffering and dispatch behave as Stdio.v's protocol and Libio.v's memory view say.
offset interval: An offset interval bounds the values an integer name can hold, derived through its single definitionssingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point., so that a flight's offset from its base is known to lie in [Lo, Hi]. At class w it bounds the signed word itself; at l it bounds some integer congruent to the value modulo 2^64, which is all address arithmetic needs.
outcome: An outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares.
parked: A waiting caller is a frame suspended at a call until its callee returns; the configuration keeps them in c_callers, each with how it will read the result (pending). interp.pl has none: its callers wait on Prolog's own stack.
phi: A phi phitmpD, 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.
pizlonate: To pizlonate is to make Fil-C's checks explicit: turn unchecked IR into checked IR, each access becoming a check and a raw access that names its proof, and each pointer operation a flight (after FilPizlonator, Fil-C's LLVM pass; pizlonate:pizlonate_module/2).
pointer distance: The pointer distance from P1 to P is a constant D such that P's address is P1's plus D modulo 2^64, and P has P1's capability. The validator finds it when both pointers reach one exact base on their guard chains: D is the difference of their offsets from it.
proof: A 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).
raw access: A 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).
ready: A runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states.
reference path: The reference path is nanofil without -O: every choice at its simplest correct translation, against which each optimization is compared (main:registers_default/2main.plregisters_default+Opt, ?RegistersdetRegisters is the register mode for optimization level Opt (o0 or o1) when no --registers option or NANOFIL_REGISTERS chose one: stack, the reference emission, without -O, and pointers, a home per scalar temporary and per pointer address word (amd64_regs.pl), with it. branches_default/2 does the same for branch selection: reference without -O, selected with i…). For checks it is --checks=reference, every access with its own check, and check_ahead's contract is stated against it. See guide.md, Plain and -O.
refines: opt:refines/2 is the outcome relation that translation validationtranslation validation nanofilTranslation validation checks each transformation's result rather than proving the transformation once: nanofil's register checker, the check passes' *_refines/2, and the interpreter refinement of difftest -O (amd64_regs_check:check_regs/5, opt:refines/2, refines). A wrong pass then makes a compile fail rather than produce a wrong output, as far as the checker is right. of the middle end uses: the original's undefined behaviour allows anything, an unknown value allows any consistent one, and otherwise the outcomes must be equal. An optimized run may go on where the original ran out of memory, a runtime's choice; too_big must stay.
renew source: A renew source is an earlier proof that a reuse form trusts for bounds: a single-definition proof Q1 of a single-definition pointer P1, made by a check, check_ahead, renew_if, check_limit or half_check, recorded with its range and alignment.
renew: A renew reuses an earlier check's bounds: renewLo, 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).
renew_hull: The hull of several passed checks of one object is the interval from the least lower end to the greatest upper end of their spans; since an object is one interval, every byte of the hull is in it. renew_hullLo, Hi, Rights, Align of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi.
renew_if: A renew whose bounds come from a guard: renew_ifLo, Hi, Rights, Align of [P, G] is exactly a check of P, but where the span test G passed it natively tests only the flags and alignment, and where G failed it runs the full check out of line. The validator accepts it through ir:guard_covers/5, following P's guard chain (ir:guard_chain/3).
repeated getter: A repeated getter is a call of a gettergetter Fil-CA getter is the function that returns a global's or function's address with its capability, initializing it on first use. Upstream every symbol is renamed pizlonated_ plus its name, and that symbol is its getter, returning a flight pointer; the program checks the result like any pointer. In IR a getter call is let(tmp(D), p, copy, [global(G)]); calling one is a safepoint (filc_amd64:object_getter//2), so it ends every live fact, except a repeated getter. that another call of the same getter dominates in the same activation: a single-definition lettmpD, p, copy, globalG, G defined in this module with local linkage. The first call has returned, so the repeat takes the fast path: no safepoint, no free, no store. The evidence pass lets live facts survive it.
replay: A single definitionsingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. replays at a point when its name holds what its own instruction's step made, in some earlier frame that agrees with the current one on the instruction's single-definition operands, and the current memory persists from the memory that step left, which lay in the address space.
retention: Retention is the runtime axiom that free changes no byte and no stored capability: a freed object's memory stays as it was while anything can name it. Only its header changes, so every access through a capability to it traps, but bytes read through a check that passed before the free are the same bytes.
reuse: Reuse 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.
run: A run is the execution of one function of a module from its initial memory, step after step, to an outcome or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too.
scope: A frame's scope is the set of single definitionssingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. whose site dominates its point: the names 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. rules may read relations off there. The single-definition invariant says every one of them replays.
shadow: A shadow is a slot that holds a copy on the side, in two unrelated places. In the backends, a phi's shadow slot holds the incoming value during a parallel copy (it may be a home). In launder.pl, a local integer's capability shadow is a pointer slot that holds the capability of the value last stored in the integer (launder:launder_func/4, launderlaunder Fil-CLaundering gives an integer converted back to a pointer the capability of the pointer it came from, as Fil-C does when its analysis can follow the integer: through arithmetic, promotable local variables and phis, never through memory or a call, and only from one pointer (launder:launder_func/4, m4.md, *Pointer-as-int laundering*). Otherwise the pointer gets no capability and dereferencing it traps.).
single definition: A single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. 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. forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point.
site: A site is where a temporary is defined: param for a parameter, or atL, I for index I of block L, with phis at index -1. A site dominates a position when it comes before it on every path from the entry: the same block at an earlier index, or a block that strictly dominates it.
snapshot: Three things share the name. tests/snapshot.sh is the byte-identity gate across revisions: a refactoring must leave every output unchanged. A setjmp function keeps snapshots, copies of every temporary (filc_amd64:setjmp_snapshots//3, setjmp.md). And a variadic callee's argument snapshot is the read-only heap object its extra arguments are copied into at entry.
soundness of checking: Soundness of checking is the validator's theorem: every run of every valid checked module avoids unchecked, so the checks the validator demands, and those it lets a pass remove or reuse, are enough, and a check that fails is the run's whole story. It does not say a check never fails: a module that reads past an array is valid and traps.
span_test: span_testLo, Hi of a pointer P0 is 1 when P0's object contains [P0+Lo, P0+Hi), addresses taken modulo 2^64 and compared unsigned, and 0 otherwise, including for a null, function, external or freed capability. It never traps and reaches no safepoint: it is the guard that --checks=guard puts before a loop.
spares: spares says that at a safepoint just before an instruction the evidence pass keeps facts across, the runtime changes no region. Every runtime meets it, so the generic soundness theorem, once stated under it, no longer takes it as a hypothesis.
strict SSA: Strict SSA is the form of a function in which every use of a temporary is dominated by a definition of it. nanofil uses the name in two strengths: the middle end's promote:strict_ssa/3 also asks that each temporary have exactly one definition, while the validator's ir:definitions_dominate/3ir.pldefinitions_dominate+Fn, +Params, +BlocksdetIn 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 de… allows several and asks only that one dominate each use.
checked IR: The two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2).
step: A step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck.
temporary: A temporary is a function-local IR name, tmpN, 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.
touch: A touch uses a vector check's proof without accessing anything: touchtmpQ follows the check that an access pizlonates to, so the check has its covering use (pizlonate:checked_access/4). It is ir:evidence_preserving/1 and 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, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside.: the model steps it as interp.pl does, doing nothing (Semantics.v's inst_step, Touch).
translation validation: Translation validation checks each transformation's result rather than proving the transformation once: nanofil's register checker, the check passes' *_refines/2, and the interpreter refinement of difftest -O (amd64_regs_check:check_regs/5amd64_regs_check.plcheck_regs+Metadata, +Map, +Before, +After, +AnalysissemidetAs check_regs/4, with the effects, CFG and home liveness of Before's implementation body already computed by body_analysis/3 (the driver computes it once and shares it with the allocator). The analysis must be of that very body and cover every mapped home; liveness bits are independent per home, so extra homes change nothing., opt:refines/2, refines). A wrong pass then makes a compile fail rather than produce a wrong output, as far as the checker is right.
transport: Transport is the crossing between Prolog terms and the model: decoding a checked module that nanofil printed into Syntax.v's syntax, and encoding the model's outcome back as the term interp:run/5 would give, so that the two can be compared with ==.
unchecked: uncheckedWhy is the outcome of a raw access its capability does not allow, or of a 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. 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).
validator: The 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.
word: A 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.

Iris (14)

Iris and the program logics before it: ideas that hold for any language. Each says where nanofil meets it; How Iris works tells them as one story.

camera: A camera is the kind of resource Iris's propositions are about: a set with a composition ⋅ of two pieces, a validity ✓ saying which compositions are possible, and a step-indexed equality. Owning two pieces is owning their composition. A frame-preserving update a ~~> a' changes a piece to another that stays valid with anything another party could own. Choosing a camera is choosing what can be owned and how it may change.
concurrent separation logic: Concurrent separation logic carries ownershipseparation logic IrisSeparation logic is Hoare logic whose assertions describe the part of memory a piece of code owns. ℓ ↦ v owns one cell, P ∗ Q holds of memory that splits into a part where P holds and a disjoint part where Q holds, and the frame rule lets code proved on what it owns run inside any larger memory, which it leaves alone. Aliasing is ruled out by the assertions, not by side conditions. across threads: threads that own disjoint resources run in parallel without interfering, and a lock guards a resource invariant that the thread taking the lock receives and must restore before releasing it. The decade after it produced a logic per sharing pattern (RGSep, CAP, iCAP, TaDA and more), each with its own soundness proof; Iris reduced them to ghost state and invariants.
ghost state: Ghost state exists only in the proof. own γ a owns the piece a of the ghost location γ, where a belongs to a cameracamera IrisA camera is the kind of resource Iris's propositions are about: a set with a composition ⋅ of two pieces, a validity ✓ saying which compositions are possible, and a step-indexed equality. Owning two pieces is owning their composition. A frame-preserving update a ~~> a' changes a piece to another that stays valid with anything another party could own. Choosing a camera is choosing what can be owned and how it may change.; it is allocated and changed by updates, never by the program. It records what the program's memory does not: shares, histories, a protocol's phase, or a whole map that the state interpretationstate interpretation IrisThe state interpretation is the proposition a language instance ties to the machine's real state. The WP receives it before every step and must give it back for the new state, so it is an invariant of every run; a proof never sees the state itself, only what owning fragments and the interpretation together imply. For heap_lang it is the authoritative ghost heap, which equals the real heap. ties to the real heap.
Hoare triple: A Hoare triple {P} c {Q} says that if P holds when c starts and c finishes, Q holds when it does. Hoare logic gives one rule per construct: assignment substitutes into the postcondition, sequencing chains triples, a loop needs an invariant each iteration keeps. It is partial correctness: a run that never finishes satisfies every triple.
Iris invariant: An Iris invariant inv N P says that P holds, of resources no one owns, between every two steps of the program. It is persistent, so every thread may know it; a thread opens it for one atomic step, takes P out under a laterlater modality IrisIris's propositions hold or fail at each step index, a budget of program steps still to run, and ▷ P ("later P") holds at n + 1 when P holds at n. Stored propositions, in invariants or ghost state, come back only under a ▷, and each program step lets a proof remove one. Löb induction, (▷ P → P) ⊢ P, proves P while assuming it one step later; loops, recursion and the weakest precondition itself are proved or defined that way., and puts P back before the step ends. Masks record which invariants are open, so none opens twice at once. Since Iris 3 it is defined in the logic from ghost state and fancy updates.
Iris Proof Mode: The Iris Proof Mode is a set of Rocq tactics that give separation-logic goals their own context: hypotheses named by strings, a persistent zone that can be used again and a spatial zone whose hypotheses tactics consume. iIntros, iDestruct "H" as "[H1 H2]", iFrame, iSplitL, iMod, iNext and iLöb do the splitting, framing and modal reasoning that would otherwise be lemma chains; typeclasses make them extensible.
Iris: Iris is a higher-order concurrent separation logicconcurrent separation logic IrisConcurrent separation logic carries ownership across threads: threads that own disjoint resources run in parallel without interfering, and a lock guards a resource invariant that the thread taking the lock receives and must restore before releasing it. The decade after it produced a logic per sharing pattern (RGSep, CAP, iCAP, TaDA and more), each with its own soundness proof; Iris reduced them to ghost state and invariants. framework in Rocq. Its propositions describe owned resources, may quantify over propositions, and are shared through invariantsIris invariant IrisAn Iris invariant inv N P says that P holds, of resources no one owns, between every two steps of the program. It is persistent, so every thread may know it; a thread opens it for one atomic step, takes P out under a later, and puts P back before the step ends. Masks record which invariants are open, so none opens twice at once. Since Iris 3 it is defined in the logic from ghost state and fancy updates.; user-defined ghost state expresses protocols. A language joins it by giving its step relation, and adequacy turns a weakest preconditionweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it. proved in the logic into a fact about every run.
later modality: Iris's propositions hold or fail at each step index, a budget of program steps still to run, and ▷ P ("later P") holds at n + 1 when P holds at n. Stored propositions, in invariants or ghost state, come back only under a ▷, and each program step lets a proof remove one. Löb induction, (▷ P → P) ⊢ P, proves P while assuming it one step later; loops, recursion and the weakest preconditionweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it. itself are proved or defined that way.
magic wand: The magic wand P -∗ Q holds of resources that, joined with any disjoint resources where P holds, give resources where Q holds. It is a structure with a hole that P fills: a function's precondition is a wand to its weakest precondition, and a structure that lends out a part owns part ∗ (part -∗ whole).
persistent proposition: A persistent proposition is knowledge rather than ownership: it owns nothing exclusive, so it can be copied, □ P giving □ P ∗ □ P, and kept after it is used. Pure facts ⌜φ⌝, invariantsIris invariant IrisAn Iris invariant inv N P says that P holds, of resources no one owns, between every two steps of the program. It is persistent, so every thread may know it; a thread opens it for one atomic step, takes P out under a later, and puts P back before the step ends. Masks record which invariants are open, so none opens twice at once. Since Iris 3 it is defined in the logic from ghost state and fancy updates., a cell that never changes again (ℓ ↦□ v) and specifications of functions are persistent; ℓ ↦ v is not.
separation logic: Separation logic is Hoare logic whose assertions describe the part of memory a piece of code owns. ℓ ↦ v owns one cell, P ∗ Q holds of memory that splits into a part where P holds and a disjoint part where Q holds, and the frame rule lets code proved on what it owns run inside any larger memory, which it leaves alone. Aliasing is ruled out by the assertions, not by side conditions.
state interpretation: The state interpretation is the proposition a language instance ties to the machine's real state. The WPweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it. receives it before every step and must give it back for the new state, so it is an invariant of every run; a proof never sees the state itself, only what owning fragments and the interpretation together imply. For heap_lang it is the authoritative ghost heap, which equals the real heap.
update modality: An update modality says a proposition holds after a change the proof makes on its own, with no program step. The basic update |==> P changes ghost state by frame-preserving updates and allocates new ghost locations. The fancy update |={E1,E2}=> P may also open and close invariantsIris invariant IrisAn Iris invariant inv N P says that P holds, of resources no one owns, between every two steps of the program. It is persistent, so every thread may know it; a thread opens it for one atomic step, takes P out under a later, and puts P back before the step ends. Masks record which invariants are open, so none opens twice at once. Since Iris 3 it is defined in the logic from ghost state and fancy updates., from the mask E1 of closed invariants to E2; P ={E}=∗ Q is P -∗ |={E}=> Q.
weakest precondition: WP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretationstate interpretation IrisThe state interpretation is the proposition a language instance ties to the machine's real state. The WP receives it before every step and must give it back for the new state, so it is an invariant of every run; a proof never sees the state itself, only what owning fragments and the interpretation together imply. For heap_lang it is the authoritative ghost heap, which equals the real heap. of any state, e can step (when stuckness is NotStuck), and after every step it can take, one laterlater modality IrisIris's propositions hold or fail at each step index, a budget of program steps still to run, and ▷ P ("later P") holds at n + 1 when P holds at n. Stored propositions, in invariants or ghost state, come back only under a ▷, and each program step lets a proof remove one. Löb induction, (▷ P → P) ⊢ P, proves P while assuming it one step later; loops, recursion and the weakest precondition itself are proved or defined that way. on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it.

Where to start

Add a builtin. Give its result type in c_types:builtin_type/2, with a doc/3 example if it adds a case, and lower it in a c_lower:builtin//4 clause, which receives the source arguments. If it is a library function under a __builtin_ name, a library_proto/3 fact is enough. Put the builtin//4 clause before the catch-all that reports "wrong arguments"; that catch-all is also how a wrong argument count is refused. If the builtin must work in constant expressions (array sizes, static initializers), add a c_types:folded/3c_types.plfolded+XV, +Env, -VsemidetXV is a constant expression of value V. Its types are the tree's: the conversions are those the elaborator chose, so this is arithmetic only. A node that is not a constant (a load, a call, an assignment, an address) does not fold. A comma operator folds, as an extension, only when both operands do: one with an effect on its left, as in the length of int[(c++, 5)], is not a constant, so that array has variable length and the effect happens. clause. A new c_types helper that c_lower calls must be exported. Pizlonation and the validator need nothing as long as the lowering emits existing IR ops; a builtin that needs a new op is Add an IR term or op below. __has_builtin is answered by $FILCC's clang, not nanofil. Add a function with // run: lines to a file in tests/c (difftest compares the interpreter, nanofil and clang, so clang must know the builtin; otherwise test it in IR or with the interpreter), and a tests/c/reject case if some use must be refused.

Accept a C construct nanofil refuses. Find the message in the source (sema_error calls and fault/4 in c_types). Typing goes in c_types (the elaborator and its doc/3 examples), lowering in c_lower's lower_node//3 or stmt_//2. Check with tests/difftest.sh on a tests/c file and with tests/reject.sh, then run the snapshot to see what else changed.

Fix a miscompile. Reduce it to a C file with a // run: line, and compare nanofil run (the interpreter) on cc-ir output with native output from tests/difftest.sh. If the interpreter is already wrong, the bug is in the frontend; otherwise compare reference and -O, then --checks=reference, --registers=stack and the other choices one at a time to find the stage.

Add an IR term or op. Agree it with the orchestrating thread first. Then state it in ir.pl's header and validator, give it a meaning in interp.pl, and teach the backends, cfg.pl's inst_uses/2 and inst_def/2, and ir_text if it prints specially. Recent examples with their reviewed contracts: docs/asm-fixed.md and docs/vector-access.md.

Add a middle-end pass. Write it as a module-to-module relation on unchecked IR, add it to opt:optimization_passes/2 and main.pl's options, carry contexts along (provenance.pl), and validate it with difftest -O and the unit tests. docs/m5.md shows how the existing ones were validated.

Accept new evidence for an access. This is a semantic change. State the obligation, the evidence, the validator rule, the interpreter's behaviour and the emitter's sequence, and have the contract reviewed before implementing it (docs/campaign.md, AGENTS.md). docs/m7.md is the worked example, round by round.

Change instruction selection or the frame. Start in filc_amd64's Instructions or Frame layout section. Anything the register checker reads must stay in amd64_contract's audited forms. Prove the change with the snapshot and a native test, and measure with the benchmark gate in docs/perf.md.

Learn a fact about Fil-C's ABI. Look in docs/abi-findings.md first, then the pinned source (filc-staging-ref-src, AGENTS.md); record what you verify there.

Reading on

The other documents were written as the work happened. Some are reference; others are history whose conclusions have since moved into code or into the reference documents.

Document	Kind	Read it for
README.md	reference	what nanofil compiles, what it refuses, and its claims, stated carefully
AGENTS.md	reference	tools, tests, dialect rules and conventions
campaign.md	reference	the semantic foundation: requirement, evidence and implementation; the three obligations; current priorities
pizlonation.md	reference	the checked stage's contract: proofs, safepoints, flight, pointer effects
m7.md	reference	evidence reuse, renew and guards, round by round, with their reviews
lifetime.md	reference	the interpreter's model of free
abi-findings.md	reference	the Fil-C ABI as verified at the pin
setjmp.md, float.md, asm-fixed.md, vector-access.md	reference	contracts for setjmp, floating point, fixed-register asm and vector checks
ub.md	reference	what Fil-C and nanofil do with C's undefined behaviour
dterm.md	reference	the Pages renderer and `doc/3`
PLAN.md	both	decisions and rules (reference), milestones (history)
m3.md	history, partly reference	the first Fil-C lowering; it still states the backend's rules
m4.md	history, partly reference	the frontend, construct by construct; search it for a feature
m5.md	history, partly reference	the middle end's passes and their validation
perf.md	history, partly reference	code quality work item by item; the benchmark gate and register modes are current
corpus.md, survey.md, lua.md	measurement	what compiles, and why the rest does not
filc-tests.md	measurement	upstream Fil-C's test suite built by nanofil, failures by kind
arith.md	measurement	constant folding against the IR and clang
archive/	archive	finished or retired work kept as written: M1, M2 and M6, the frontend's typed-tree record, factorings, Prolog hosts, the handoff

A good order for a newcomer: this guide, campaign.md, ir.pl's header, pizlonation.md, then the module headers along the walkthrough, then m7.md when you reach evidence.

Documentation conventions

These keep the modules readable and are checked.

A header per module. Each file in src/ begins with a /* ... */ comment that says what the module owns, the terms it consumes and produces (as tables of term forms), its invariants and where it fits. It is written in the little Markdown that dterm renders (docs/dterm.md, Module headers as prose): ## headings, pipe tables, prolog and diagram fences.
PlDoc for every export. Each exported predicate has a signature comment with modes and determinism, then its meaning:
```
%! valid_module(+M) is semidet.
%
%  M is a well-formed module. ...
```
A module listed in tests/unit.pl's documented_module facts (c_types) uses doc/3 facts instead, whose examples are tests. Important internal predicates of the large modules have %! comments too; smaller internal ones have a % comment that begins with their head.
Sections. A %% Title line starts a section, which dterm draws as a heading and lists in the page's navigation.
Checks. tests/docs.pl fails when a module lacks a header or an export lacks %! or doc/3. tests/guide.sh --check fails when an output in this guide differs from what the compiler produces; run it without --check to update them. It also writes the outputs' terms to guide/outputs.pl, from which the site draws them. swipl web/dterm.pl --check docs/guide.md src --concepts=docs/concepts fails when a predicate reference (name/N, module:name/N), a module file name, a link or a [[concept]] does not resolve, or a concept names no source. All three run in nix build .#checks.x86_64-linux.nanofil.
On the site. The guide is a dterm page (nanofil/guide.html, web/dterm_guide.pl): its terms are drawn as the source is, predicate references link to their definitions with the signature on hover, concept names link to their pages, and each module page links back to the sections that name it. Write a predicate reference in backticks as name/N or, when two modules define it, module:name/N; give a concept the predicate, module or Rocq definition that defines it.
Concepts. A term a reader may not know gets a page in concepts/, written once and linked from both the Prolog and the Rocq rather than explained again in each (dterm.md, Concept nodes). In a comment or document, [[name]] links to it and a line ![[name]] draws it in place.