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 dominatesdominance nanofilBlock 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. it.

• ir.pl: ir:block_sites//1ir.plblock_sites+Blocks//N-at(L, I) for each definition of tmp(N), at index I of block L, a phi's at -1. records every definition's site, ir:site_dominates/4ir.plsite_dominates+Def, +L, +I, +Intervalsthe definition Def comes before position I of block L on every path from the entry. orders them, and 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 a dominating one for each use. Validate.v: site (SParam, SAt), temp_sites, site_dominates.

• Sites.v joins these sites with the list 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. filters, through one list def_positions; Single.v's point_site reads a frame's point as a site, so the invariant compares like with like.

• A phi's operand is used at the end of its predecessor, not at the phi.

The subtlety: the proofs use the validator's own sites rather than a second notion of position, so site_dominates is exactly the order the run-level invariants are stated in.

See rocq.md, Where a name is defined and Sites.v.