Strict SSA is the form of a function in which every use of a temporary is dominateddominance 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. by a definition of it. nanofil uses the name in two strengths: the middle end's promote:strict_ssa/3promote.plstrict_ssa+F, +Cfg, +IdomsemidetF is in strict SSA form: every temp has one definition, and in the blocks reachable from the entry each definition dominates each use (a phi argument is used at the end of its predecessor). Cfg and Idom are those of F. also asks that each temporary have exactly one definition, while the validator's 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… allows several and asks only that one dominate each use.

• Checked IR need only pass the validator's form (tests/fixtures/memory.ir defines a temporary twice). 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 restrict themselves to 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., which have both properties.

• Rocq: definitions_dominate in Validate.v, whose header calls it strict SSA; Sites.v's use_dominated reads it back: a single-definition name a reachable instruction uses is defined at a 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. that dominates the use.

• Phi operands are used at the end of their predecessor; unreachable blocks are not checked.

Why it matters: with strict SSA, a dominating single definition holds the value it computed from its operands' current values, which is what lets the validator reason about pointers by name.

See ir.pl's comment on 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… and guide.md, The IR is the contract.