Static Single Assignment
One definition per name makes data dependencies explicit. Phi functions, construction, why so many analyses get simpler, and how you leave SSA again.
One rule, applied to a whole function: every value has exactly one defining instruction. `x = 1; x = x + 2` becomes `x1 = 1; x2 = x1 + 2`, and from that moment "which definition does this use read?" is answered by reading the operand name instead of by analysing the graph.
At a merge point no single definition reaches the use, so SSA writes `x3 = phi(x1, x2)` — "the value depends on which edge you arrived by". It is a notation, not an instruction, and nothing ever executes one. That is precisely why `[[out-of-ssa]]` has to exist.
The real algorithm, in two halves: place a phi for each variable at the iterated dominance frontier of its definitions, then rename by walking the dominator tree with a stack per variable. That is Cytron et al., that is LLVM's mem2reg, and that is exactly what `toSSA` does.
Every use has exactly one reaching definition. Cash that one fact in four places: constant propagation needs no analysis, dead code is a use count, def-use chains are the IR itself, and copy propagation cannot be wrong because nothing is ever reassigned.
Phis become copies at the end of their predecessors — and that sentence hides three classic miscompilations: the swap problem, the lost copy, and critical edges with nowhere to put the copies. AtlasLang breaks copy cycles by rescuing the value about to be *clobbered*, and the sim test proves it by simulating the moves.
Minimal, semi-pruned and pruned SSA differ only in how many phis they place and how much analysis they pay for it. Loop-closed SSA and gated SSA are different in kind, and much rarer — one is a normalization LLVM actually uses, the other is mostly a research form.