concepts · nanofil · Filnix wiki

The terms nanofil's Prolog, its Rocq model and its documents share, each explained once, in docs/concepts. Comments and documents link to one with [[name]] and draw it in place with ![[name]]. How Fil-C works tells the Fil-C ones as one story, and How Iris works the Iris ones.

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 sizeof(void*) 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 and variadics. 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 outside the core subset.
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 invN 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 [H₁ H₂], 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: WPe {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.