A shadow is a slot that holds a copy on the side, in two unrelated places. In the backends, a phiphi nanofilA phi phi(tmp(D), 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.'s shadow slot holds the incoming value during a parallel copy (it may be a homehome nanofilA home is the 8-byte frame word that holds a temporary, a phi's shadow or a pointer's address word in the stack-homed stream amd64_regs starts from (guide.md, 12. Register homes). Scalar homes are w or l only; float temporaries are kept out of them.). In launder.pl, a local integer's capability shadow is a pointer slot that holds the capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees. of the value last stored in the integer (launder:launder_func/4launder.pllaunder_func+F₀, +Records₀, -F, -RecordsdetF is the function F0 with each itop of an integer computed from one capability given that capability (this module's header), and Records is its context Records0 with instruction sites moved accordingly., launderlaunder Fil-CLaundering gives an integer converted back to a pointer the capability of the pointer it came from, as Fil-C does when its analysis can follow the integer: through arithmetic, promotable local variables and phis, never through memory or a call, and only from one pointer (launder:launder_func/4, m4.md, *Pointer-as-int laundering*). Otherwise the pointer gets no capability and dereferencing it traps.).

Neither appears in the formal model.