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 sitesite nanofilA site is where a temporary is defined: param for a parameter, or at(L, 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. 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 replaysreplay nanofilA single definition 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..

• Single.v: point_site reads the frame's point as a block and index; scope_with quantifies over the replayable single definitions whose site dominates it; scope_holds asks each to replay. running and waiting ask it of the running frame (unless doomeddoomed frame nanofilA 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.) and of each waiting callerparked nanofilA 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..

• Weaker scopes: scope_plain (Ahead.v) excludes check_ahead proofs; scope_weak (Doomed.v) lets a doomed check_ahead hold its pointer instead of a passed check.

• Moving on: scope_step across one instruction, scope_after for a call's result on return, scope_mem for memory.

On the Prolog side there is no term for it: ir.pl reads Once (ir:single_definitions/3ir.plsingle_definitions+Params, +Blocks, -OncedetOnce maps each temporary with exactly one definition (temp_defs/3's forms) to it: param, its phi, or its instruction.) and relies on strict-SSA dominance (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…), as the comment on ir: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… argues.

See rocq.md, The single-definition invariant.