A temporary is a function-local IR name, tmpN, holding one wordword nanofilA word is the value a temporary holds at run time: an integer, a pointer (an address with its capability), or a limit's opaque snapshot. The temporary's class says how it is read. of one classclass nanofilA value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with its capability, and in checked IR a (a proven address) and f (a proven function) (ir:class/3).. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR.

• ir.pl's header ("Temps are ground names"); Syntax.v's value Tmp. At run time Semantics.v's environment env maps each temporary assigned so far to its word, as interp.pl's Env does; Term.v's lookup and put read and write it.

• Proofsproof nanofilA proof is a temporary of class a or f, the result of a check: it holds the checked pointer itself and certifies that the check passed. A raw access names the proof it relies on, so evidence is structural (ir:proof_use/6). (classes a and f) are temporaries too, but never parameters, phis, call arguments or stored values.

• Named locals are a separate namespace: objects declared by local_alloc, not temporaries.

The subtlety: a temporary may have more than one definition (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 only that one dominate each use), so "the value of tmpN" depends on where you stand; the reuse rules follow only 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.. Reading a temporary before it is assigned is Stuck in the model, an instantiation error in interp.pl.

See guide.md, The IR is the contract.