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 persistsidentity nanofilAn 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. from the memory that step left, which lay in the address spaceaddress space nanofilThe 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..
replays in Single.v. Only replayable instructions replay: a let that is not an alloc, and a flightflight nanofilA flight builds a pointer from two independent sources: flight(D, 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.. A call or an allocation does not continue with a value, and no reuse rule reads through one.
There is no table of per-op relations: each reuse form reads what it needs off inst_step for the op it trusts. So a check that passed then passes again or traps (persists_access), and a flight's capability is its lower donor's.
Weaker scopesscope nanofilA frame's scope is the set of single definitions whose site dominates its point: the names the reuse rules may read relations off there. The single-definition invariant says every one of them replays.: scope_plain (Ahead.v) asks every single definition but a check_aheadcheck_ahead nanofilcheck_ahead(Lo, 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. to replay; scope_weak (Doomed.v) lets a doomed check_ahead hold its pointer instead.
On the Prolog side this is the dominance argument of m7.md's round 4, cited in the comments of ir:same_pointer/3ir.plsame_pointer+Once, +P, +P1semidetAt 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 ir:lower_chain/3ir.pllower_chain+Once, +P, +BsemidetP has B's lower: P is B, or a single-definition flight whose lower donor has B's lower, whatever its address. At any point that P's definitions dominate, P's lower is B's current one, by round 4's dominance argument (docs/m7.md), since every name on the way has one definition. Once maps each single-definition name to its definition.: every definition on a chain dominates the point and was computed from its operands' current values.
Defined in Single.v.