interp.pl
Relational semantics of the IR (ir.pl): the outcome of running a function of a module, as a relation that runs in every direction, so that arguments and outcome can both be partially unknown.
Entry points
| Predicate | Does |
|---|---|
run+Module, +Fn, ?Args, +Fuel, ?Outcome | prepares Module, then runs Fn |
module_prepared+Module, −Prepared | the module's mode, initial memory, and indexes of its functions and blocks |
run_prepared+Prepared, +Fn, ?Args, +Fuel, ?Outcome | runs Fn of a prepared module |
Prepare once to run many times. Args are integers or CLP(Z) variables, one per parameter, in the range of the parameter's class (ptrAddr, Cap for a p parameter).
Outcomes
| Outcome | Means |
|---|---|
retV | returned V (an integer or constrained variable) |
retsX1, X2 | returned a tuple |
ret | returned from a void function |
dataX1, ... | a data function (zreturn) returned these words, each an integer or ptrAddr, Cap |
unreachable | executed unreachable |
ubReason | undefined behaviour: float_conversion (an invalid float-to-integer conversion), or in plain mode out_of_boundsA, Size, a memory access outside every live allocation |
trapReason | a Fil-C check failed (filc mode only): null_capability, out_of_bounds, misaligned, readonly, not_a_function, argument_size, return_size, invalid_free, double_free |
uncheckedReason | a raw access (checked stage, ir.pl) that its capability does not allow: a check is missing or too weak, which only a broken pass produces. It is neither ub nor a trap, so it refines nothing. |
out_of_fuel | executed Fuel blocks without finishing |
unknownasmM, Xs | reached the fixed-register asm M (cpuid, xgetbv, rdtsc, rdtscp) on the input values Xs, whose results only the machine knows (docs/asm-fixed.md): native tests cover what follows |
Unknown values
Integer arithmetic and branches are CLP(Z) constraints, so the relation runs in every direction. Known values take a fast path (is/2 and if-then-else), which gives the same answers; only unknown values pay for constraints.
Memory addresses, allocation sizes and capabilities must be known when an access, alloc or indirect call uses them; otherwise the run raises an instantiation error, which is incomplete but never wrong.
Float values are concrete unsigned IEEE bits. Float arithmetic uses ieee.pl's integer-only SSE2 semantics, not CLP(Z) or host floats; unknown float inputs also raise an instantiation error.
Memory
Memory is memBytes, Regions, Next, Aux:
| Part | Is |
|---|---|
| Bytes | an assoc from address to byte |
| Regions | regionBase, End, Kind, Life objects; Kind is stack, heap or global, Life is live or freed |
| Next | the next allocation address; addresses are never reused |
| Aux | in filc mode, the capabilities stored in memory |
A byte nobody wrote is, in plain mode, a fresh variable in 0..255, so reading uninitialized memory gives an unknown value rather than a made-up one; in filc mode it is 0, since Fil-C zeroes allocations.
In plain mode a function's allocations die when it returns, and addresses are never reused, so use after return is an out-of-bounds access. In filc mode allocations outlive their function. External callvoid, globalfree, argp, P invalidates P's heap object: End becomes Base and Life becomes freed. A live zero-sized object also has End = Base, but may be freed once. Bytes and stored lowers stay intact; every alias consults the same region's current bounds. Module-defined functions take precedence over this external adapter.
A capability's Base is stable identity, never recovered from address bits. All exposed capabilities for an object have the same rights (objBase or roBase); snapshot initialization is private until its readonly capability is published. Memory-using injected pointer arguments must obey these invariants and name existing objects.
This is the deterministic explicit-free subset, not a GC simulator: no reclamation, concurrent or signal-handler frees, or rewriting dead lowers to the runtime's free singleton. Unknown external effects and addresses remain outside the oracle's domain. It does not justify check elimination or safepoint motion (docs/lifetime.md).
Run state
The run state is sMem, Fuel; each block costs one unit of Fuel. Inside a function the interpreter carries ctxFns, Globals, Blocks, Ret, Mode, Locals:
| Part | Is |
|---|---|
| Fns | the prepared functions |
| Globals | the address of each global |
| Blocks | the function's blocks by label |
| Ret | its return class |
| Mode | the module mode |
| Locals | this invocation's local names and fresh object identities, bound at local_alloc |
A block is entered fromPred, Pred the label of the block that jumped to it, or at entry.
Variable names
| Name | Is |
|---|---|
| K | a class |
| V | an IR value: tmpN, constN or globalN |
| X | a run-time value: an integer, a constrained variable, or in filc mode ptrAddr, Cap |
| Env | the assoc from temporary to run-time value |
| S | a run state |
| Out | an outcome |
| Res | a partial result: valX, ok, ubWhy, trapWhy or uncheckedWhy |
Env0/Env and S0/S are the state before and after.
Outcome is the result of calling the function Fn of module M on Args and executing at most Fuel blocks. With unknown Args each solution constrains them to the inputs that take one path; see run_prepared/5.
Prepared is M ready to run: its mode, the address of each global, its initial memory, and its functions and their blocks indexed by name and label. The initial memory holds integers only, so runs can share it.
Outcome is the result of calling Fn of the prepared module on Args within Fuel blocks. Args is constrained to the ranges of Fn's parameter classes. Where a branch or a division depends on an unknown value (an argument, or a byte nobody wrote), there is one solution per case, each constraining that value; comparisons are reified instead. When every such value is known the outcome is unique, though the run may leave a choice point, so callers use once/1. Fails when the module defines no Fn. Throws nanofil_error when the run needs what the interpreter does not model (a symbol the module does not define, a temporary read before any assignment), and an instantiation error when an address, allocation size or capability is unknown.
X is an argument of class K. A p argument is ptr(Addr, Cap), or an integer address with no pointer term (main.pl's canonical arguments): a defaulty case that comes from outside this module, so the cut stays. An unknown p argument is ptr(_, _).
Calling Fn on Xs in state S0 ends with Out in state S. In plain mode a callee's allocations die when it returns; in filc mode every allocation is a heap object that lives until explicitly freed. A variadic callee whose argument snapshot the address space cannot hold traps out_of_memory at its entry, as Fil-C does.
Keep identities, bytes and aux, but end just this invocation's stack lifetimes in the latest state. A trap may precede a declaration; its unbound Base is not authority to select and invalidate another object.
a variadic callee's entry takes the snapshot of its arguments. Fails when the address space cannot hold the snapshot (alloc_base/6).
promote_cc_to_heap returns null for an empty argument packet. This is distinct from alloc(0), which creates an ordinary zero-sized object.
R is the value of the integer expression Expr. Concrete fast path: when every operand is known, plain arithmetic and if-then-else give the same answers as the constraints, without propagators or choice points. Unknown operands still get constraints. The ground/1 test reads the instantiation, but both branches state the same relation, so the program stays sound for partially known Expr.
B is 1 if Test holds, else 0 (reified when unknown).
Blocks
Out and S are the outcome and final state of running the block Label, entered from Pred (from(L) or entry), and everything after it. Each block costs one unit of fuel.
Env is Env0 with each phi of Phis bound to its value for the edge from Pred, read in EntryEnv. Phis read the environment as it was on entry, so they all bind at once. An entry block has no phis.
the block's Jump continues the run unless an instruction ended it. A doomed run (a check_ahead's early failure, docs/schedule.md) must reach its trap within the block it is in or past plain edges: a return or a poll edge first means the early check was not anticipated.
Out is the outcome of Jump, ending block From, and everything after it. When the jnz condition is unknown, both edges are solutions, each constraining it; a known one takes the fast path. A pollcheck on the edge (poll(L)) changes nothing the interpreter models: explicit free calls run, but there are no asynchronous frees.
Out is what ret(P) of a data function returns, as filc_prepare_to_return_with_data does: no words for a null P, else the words from P to its object's end, each loaded as a pointer (an integer word has no capability). It traps where libpizlo's checks fail: no object, a function, a freed object, or P not 8-aligned.
Instructions
Result is cont(Env, S) when every instruction ran, or stop(Outcome, S) when one ended the run.
a check_ahead whose early bytes fail (docs/schedule.md) yields its pointer and dooms the run: from then on it must reach, through ahead_transparent/1 instructions only, an access whose reference check fails, which shows here as a renew's failed span or a raw access's unchecked bounds (a read of the widened proof itself). That is the program's trap, made early(Why); anything else first is unchecked(ahead(Why)). A renew of another object (alias) or a wrong limit stays a broken pass.
Result is the result of the instructions Insts after one whose result is Result0.
Result is cont(Env, S) after Inst, or stop(Outcome, S) when it ends the run.
One thread and no atomic boxes: an atomic pointer store is a pointer store, and a fence does nothing observable.
A vector's full-width check (docs/vector-access.md): in a Fil-C module the access check of Size bytes, which writes nothing; in a plain one nothing, since C's semantics are the chunks'. touch uses a proof.
One thread in program order: lfence, sfence and pause change nothing. The others' results are the machine's, so the run stops there.
Only libc free's ordinary signature is modeled. Resolution comes first: an in-module function or data symbol is handled above. Other signatures and external calls are explicit gaps, not silently failed relations or guessed libc effects.
P designates a function only when it carries that function's capability at its exact callable address. An unknown address is not proof; an external symbol's kind is unknown to the interpreter, which must not guess that it names a function.
A target check authorizes the call, not its signature. Only a failed target check becomes unchecked in raw_call; ABI and callee traps keep their meaning. The conversions below are shared with unchecked call.
the result of an indirect call to F on Ys, with the call's conversion Conv.
indirect_call_conv(+CalleeRet, +Params, +Res, +Args, +Xs, -Ys, -Conv): a call through a function pointer. When the classes the call site passes and expects give the callee's signature (w and l are the same word), it is a direct call. Otherwise it goes through the callee's generic entry: each argument and result word is 8 bytes with its lower beside it, so a p word read as an integer is its address and an integer read as p has no capability. Too few arguments, or fewer result words than the call site reads, fail the generic entry's size checks. Conv is same, conv(CallerWords, CalleeWords) or trap(Why).
Y is the word X written at class From and read at class To through the generic entry.
A p word read as an integer is its address. An integer held at p (see class_arg/2) is its own address: the defaulty case keeps the if-then-else.
Out is the callee's outcome Out0 as a call site that reads CallerWords reads it. An outcome that does not return passes unchanged.
res_result/5, store_res_result/4 and call_outcome_result/5 relate an operation's Res, or a callee's outcome, to the instruction's Result.
A data function's words, read as the call site reads them through the generic entry; too few fail its size check.
and rets_env(+Res, +Xs, +Env0, -Env): Env is Env0 with the returned word X, or words Xs, bound as the call site's Res reads them.
X is the word X0 taken at class K, its low bits(K) bits; a p word is itself.
A limit's snapshot (docs/bounds.md) is no integer; only check_limit reads it (ir.pl's limit_reads/2).
X is the IR value V read at class K, which takes its low bits(K) bits. value_x_/5 indexes on the value. A symbol the module does not define is ptr(0, ext(Name)) in filc mode; in plain mode (which the validator rejects) the read fails.
Flight's two components are read independently from the old environment. Projecting an address takes its low 64 bits; projecting a lower copies capability identity without inspecting it or its address.
Operations
Res is val(X), ub(Why) or trap(Why). Op is an IR term (ir.pl). Commit before integer dispatch: float bits must never get CLP(Z) arithmetic, even if a caller asks for a different result on backtracking.
as op_res/7, for Op of Kind. Loads and allocs use the memory; the rest is arithmetic.
A check_ahead (docs/schedule.md) is its check of [Lo, AHi), the access's own requirement, with that check's trap; when that passes and [Lo, Hi) does not, it traps early(Why): a trap the reference program reaches later, which only the oracle's earlier-trap rule accepts (main.pl's pizlonation_verdict/4).
A renew runs the check's whole access test on its own pointer P (docs/m7.md, round 4), which has the capability of Q1's: P may lie at a distance from Q1's pointer (docs/schedule.md). Only a freed object or a write to a read-only one is the program's trap, as the reference check's; any other failure means the span the validator relied on was false: unchecked(span).
P is not of the object Q1's check saw (pointer_distance/4 was wrong).
A renew_hull (docs/forward.md) is a renew whose two sources both have P's capability: the same access test on P, the same traps; any other failure is unchecked(span), another object's source unchecked(alias).
A half check (docs/half.md) is its check of P, which has Q1's capability. Natively it tests only Bound, upper or lower, and for lower the free flag, then the read-only flag for a write and the alignment, as the check does. Where that test and the check disagree, the bound the validator took as known was false: unchecked(half).
A span test (docs/m7.md, round 5) compares the object's current bounds with the span, addresses modulo 2^64 as native code forms them; it is 0 for any capability that is not an object's, and never traps.
renew_if is its check when G is 0. When G is 1 it runs the check's whole access test too: a freed object, a write to a read-only one and a misaligned address are the program's traps, which the native fast path tests itself; any other failure means the guard or the interval rules were wrong: unchecked(span).
A limit (docs/bounds.md) is an opaque snapshot, which only check_limit reads (ir.pl's limit_reads/2): the capability and the access size it was taken for. Natively it holds the object's upper bound then, which changes only when the object is freed, and check_limit tests the free flag too; here a free empties the bounds the check reads directly.
check_limit is its check when its limit was taken of P's capability for its size. A limit of another capability or size means the validator's lower chain or the pass was wrong: unchecked(limit).
A va_arg of class K takes Step bytes at an Align-aligned cursor, as filc_get_next_ptr_bytes_for_va_arg does: a long double's cell is 16 bytes at 16, of which it reads its 10.
A check whose access_res/7 is Res0 yields P, proven, or traps.
A renew (docs/m7.md, round 4) of P whose access_res/7 is Res0 yields P, proven, or traps as the check it replaced would: a read-only trap stands, and a freed object traps out of bounds. Any other failure means the earlier check's bounds did not cover this access, which a valid renew rules out, so it is unchecked(span), a broken pass.
Passes is true when a half check's native test passes at address B (filc_amd64's half_bounds//5): upper, B + Size =< upper; lower, B taken signed at or above lower and the object not freed; then not read-only for a write, and aligned. Fails for a capability that is not an object's, whose header no half check may read.
B is the address A plus the constant Off.
Res is the result of a load of type T at class K. A load reads Size bytes and extends them as T names; load(l) takes them as they are.
load(p) exists in filc mode only. It reads the word and the capability the last store(p, ...) left there, none if there was none.
Execute the supplied pointer-access protocol. Its local state keeps the aux word separate from the resolved lower and primary address; only the completed load publishes a pointer. Aux contains abstract capability identities, not native boxes, so resolution is identity.
Fil-C's helper reads the address and the lower (or the box's pair) as one unit; with one thread that is aux_read then address_read.
The interpreter has no GC, aux allocation or asynchronous frees. Ensure/barrier/reload are therefore abstract identities, not a claim that native helpers cannot exit or fail. The observable writes still execute in list order: lower first, then primary bytes, without another bounds check after ensure-aux. Regions and Next are carried opaquely.
the cas(T) of Expected E and New N at A (ir.pl): a write check of its width, at its width's alignment; then old, the T at A, and N written there when old's bytes are E's low bytes (for p, when the addresses are equal, whatever the capabilities). Res is old, as load(T) would give it.
Res is val(U), U the Size bytes at the address in Args, or why there is none.
A is the address of the access value A0 and Res is ok when a Size-byte read there may go ahead. Fil-C checks the capability; plain mode checks the region when it reads.
Res is the result of add or sub (Op) of class K on Xs. Pointer arithmetic keeps the capability.
Res is the result of the arithmetic Op of class K on Xs; add and sub are integer here (additive_res/4). ptoi drops the capability; itop has none.
Res is val of Expr, or val(0) when the divisor Y is zero, as Fil-C defines it since deluge (KillUB divides 0 by 1; docs/ub.md). An unknown Y gives both cases as solutions; a known one takes the fast path.
Signed division is total too, as Fil-C defines it since deluge: a zero divisor gives 0 (quotient and remainder), and MIN / -1 wraps to MIN with remainder 0, which the general rule gives, since -MIN wraps to MIN at the class width. Known operands take the fast path; otherwise the two cases are disjoint constraints.
The shift count is taken modulo the class width.
B is 1 when X Cond Y holds at class K, else 0.
S is the two's-complement reading of U at class K.
S is the two's-complement reading of the low bits of U, for a field of modulus M with sign threshold H. The first clause is the fast path for a known U; the cut commits to it, and the second clause states the same relation with constraints.
S is the low bits of X that T names, sign- or zero-extended.
Memory: mem(Bytes, Regions, Next, Aux)
Each region(Base, End, Kind, Life) is shared by every capability with that Base. Only free changes a Fil-C object's bounds, monotonically to empty. Freed regions remain so zero-sized live objects and double frees are distinguishable. No reclamation or address reuse is modeled.
Aux is used in filc mode only: it maps an 8-aligned address to the capability a store(p, ...) left there. An integer store leaves it alone, as Fil-C's aux array does.
the pinned runtime's free_with_checks, object_for_deallocate and free_impl, for objects this interpreter owns. ext(_) has a placeholder address, not a known zero; it stays unsupported. Public run/5 also accepts integer p arguments: these have no capability.
Null is a no-op even with an object's lower. Otherwise kind/address validation precedes the FREE test, as object_for_deallocate precedes free_impl. READONLY alone does not prevent deallocation of a heap object.
capabilities refer to registered identities. An injected unknown base is outside the interpreter domain, not authority for the live object that happens to contain its address.
Res is val(U), U the little-endian value of the Size bytes at A, or ub(...). In plain mode an access outside every live region is undefined. In filc mode the access was checked against its capability already. Mem is Mem0 with any unwritten byte read now made a fresh variable (plain mode).
Mem is Mem0 with X written at Addr as Width, when Res is ok.
a Fil-C store of Width writes the integer V of the value X, needs alignment Align, and Stored is cap(C) for the capability C of a store(p, ...), or none.
| 1551 | b | V | V | 1 | none |
| 1552 | h | V | V | 1 | none |
| 1553 | w | V | V | 1 | none |
| 1554 | l | V | V | 1 | none |
| 1555 | s | V | V | 1 | none |
| 1556 | d | V | V | 1 | none |
| 1557 | x | V | V | 8 | none |
| 1558 | p | ptrV, C | V | 8 | capC |
Mem is Mem0 after a checked store with result Res.
Fil-C's access check, Res ok or trap(Why). Cap is none, obj(Base) for a writable object, ro(Base) for read-only data, fn(F) for a function object (zero size, so every access fails the bounds check) or ext(Name) for a symbol defined outside the module, which the interpreter cannot follow. Cap must be known: an unknown capability (an unknown p argument) raises an instantiation error, as an unknown address does. An unregistered Base is outside the interpreter's domain. The trap reasons and their order are those of the backend's access check, so a check and the raw access it covers agree.
the access [A, A+Size) lies inside one live region. A and the regions are integers here, so the if-then-else in the callers is sound. The cut commits to the first such region.
Xs are the bytes at A, A+1, ... in Bytes0; Bytes is Bytes0 with each unwritten byte among them bound. An unwritten byte is unknown in plain mode and zero in filc mode, since Fil-C allocations are zeroed.
Bytes is Bytes0 with the bytes Xs at A, A+1, ...
the heap allocation allocAlign of Size bytes. Fil-C refuses an object of more than max_allocation_size/1 bytes before it allocates anything (filc_prepare_allocate_object/1: "attempt to allocate object that is too big"), and one its address space cannot hold ("out of memory"); both are safety errors.
FILC_MAX_ALLOCATION_SIZE, PAS_MAX_ADDRESS, 2^48 - 1.
Base is a new region of Size bytes in Mem. Allocations are aligned (Fil-C's to at least 16, as filc_allocate_with_alignment aligns them), with Fil-C bounds rounded to 16 as prepare_allocate_object does (zero stays zero). A 16-byte gap separates distinct, never-reused identities. Fails when Next would pass the end of the address space (address_space/2): the runtime is out of memory.
Next is within the address space. Fil-C's objects lie below 2^48, libpas's address space (PAS_ADDRESS_BITS), so an address never wraps inside one, and two addresses of one object are less than 2^63 apart (the Rocq model's objects_fit). Plain mode sets no limit.
initial_memory(+Mode, +M, -Globals, -Mem): Mem holds every data definition, each in its own region, with its bytes. Globals maps a name to its address, or in filc mode to a pointer value: data objects are aligned to 16 or their stricter Align with their size rounded up to 8, as Fil-C's are, and each function gets an address and a fn capability.
Globals and Rs add to Globals0 and Rs0 the address and region of Item placed at the next address from A0 that its alignment allows; a function takes no space.
Bytes (and in filc mode Aux) add the bytes (and capabilities) of Item.
place Item at the next address from A0 aligned to 16 or, if stricter, its Align. A weak declaration (extern(weak)) takes no space: its symbol stays undefined, a null pointer (undefined_symbol/3).
a table entry, never run here
Item written at At0; At is the address after it. Data items are IR terms (ir.pl); the cut commits to the pointer item before the clause for every other item.
Size is Size0 plus Item's size. The cut commits to a string before the clause for any other item of width b (a constant).
Bs are the bytes of the data Item, one per character of a string. The cut commits to a string, as in item_size/3.
Printing
Text is the atom that prints Outcome: its integer return value, or just the kind of a pointer, unknown or tuple result. A returned value is an integer, an unknown (a variable, possibly constrained) or ptr(Addr, Cap): a defaulty term, so ret_text/2 tests it.