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.

• 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. builds the map ir.pl calls Once; Validate.v transcribes it as single_definitions. Sites.v gives each one 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. (once_position) and proves use_dominated and no_use_redefined.

• Single.v states the invariant: in every frame (the running one 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 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.) each single definition in its scopescope 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. 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. (scope_holds, sinv). mreachable_sinv proves it for any runtime whose free keeps identities; interp_sinv proves it for the interpreter with no hypothesis but a ready start.

The subtlety: ir.pl lets a temporary be defined more than once, since 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… asks only that one definition dominate each use (ssastrict SSA nanofilStrict 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/3 allows several and asks only that one dominate each use.). Names defined twice may change under a reuse rule's feet, so no rule follows one.

See rocq.md, The single-definition invariant.