A phi phitmpD, K, Pred−Value gives D the value paired with the block control came from. A block's phis run together on entry, each reading its operand as it stood at the end of the predecessor.

• Syntax.v's phi; Semantics.v's phis_env, applied when a frame at Enter names the block it came from; interp.pl does the same in interp:block_outcome/7interp.plblock_outcome+Ctx, +Label, +Pred, +Env₀, +S₀, -Out, -SnondetOut and S are the outcome and final state of running the block Label, entered from Pred (from(L) or entry), and everything after it. Each block costs one unit of fuel..

• The validator treats a phi's operand as used at the end of its predecessor, and its own 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. as index -1 of its block (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.). Phi destinations end the live factslive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own. and needsneed nanofilA need is the validator's backward fact for check_ahead: need(B) = H at a point says every path from it reaches a raw heap access through a pointer of which B is an exact base, whose bytes reach B + H, and reaches it first: before any instruction that is not ahead-transparent, any poll edge, edge back or end, and before B is redefined. that name them.

• On a poll edge the pollcheck runs after the phis' copies.

The subtlety: a phi counts as a definition, so its destination can be a single definitionsingle 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. (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.), yet it is not replayable: its value depends on the edge taken, and no reuse rule reads a relation through it.

Natively a phi has a shadowshadow nanofilA shadow is a slot that holds a copy on the side, in two unrelated places. In the backends, a phi's shadow slot holds the incoming value during a parallel copy (it may be a home). In launder.pl, a local integer's capability shadow is a pointer slot that holds the capability of the value last stored in the integer (launder:launder_func/4, launder). slot for the parallel copy.