This is the machine the modern analysis of algorithms is stated on. Its format is that of Cook and Reckhow (Time bounded random access machines, JCSS 7, 1973): memory cells are the only storage, an instruction is $cell ← f(cells)$, literals enter through one instruction and indirection through two. Its numbers are bounded rather than its instruction set, which is the discipline of Fredman and Willard (Surpassing the information theoretic bound with fusion trees, JCSS 47, 1993) and of Hagerup (Sorting and searching on the word RAM, STACS 1998): cells hold $w$-bit words, $w$ is large enough to address the input — $w ≥ log n$, here always written as an explicit inequality against $2 ^ w$ at the point of use — and a word operation costs one time unit because on words it is one instruction of a real machine. Multiplication, division, bitwise operations and shifts are then unproblematic, and this is what makes the model the one in which the results of the algorithms literature are actually stated. The formats in which those results are written down simulate one another with constant overhead (van Emde Boas, Machine models and simulations, Handbook of Theoretical Computer Science A, 1990, §2).

Truncation is definitional and follows a single rule, applied everywhere and with no exceptions: every value the machine produces is reduced modulo $2 ^ w$ at the point of production, and every address is reduced modulo $2 ^ w$ at the point of use. Values are produced into memory, where $setCell$ carries the reduction, and onto the output tape, where $Instr.effect$ writes it out; addresses are used by every operand of every instruction, by the address $load$ and $store$ fetch out of a cell, and by $setCell$ when it writes. A literal is not reduced where it is written down — that would be a second rule — but the value it produces is, so an oversized literal is never observable except through a word, and only a program's own literals can be oversized in the first place, since every value it can read out of memory is a word. Two consequences make the rule worth its uniformity: every cell the machine can reach holds a word, by construction rather than by an invariant to be proved; and the memory, although indexed by all of $ℕ$, is touched only at the residues below $2 ^ w$, so it is exactly the canonical $2 ^ w$-cell store. For the instructions whose results cannot leave the words — truncated subtraction, division, conjunction, complement — the reduction does nothing; it is written anyway, because a rule without exceptions is easier to review than a case distinction.

Subtraction is natural-number monus, truncated at zero, so that a comparison is $sub$ followed by $jzero$. The complement is $2 ^ w - 1 - m[b]$, the one value that depends on the word length other than through truncation; with $and$ and $shiftl$ beside it, every bitwise operation and both shifts take a number of instructions independent of $w$. A program measures $w$ itself, by counting the doublings of a cell from $1$ until it wraps to zero, so the model needs no instruction reporting the word length and one program serves every word length. The remaining standard operations are derived at constant cost; with $t$ and $u$ cells the program spares:

$read$ reduces the number it takes off the input tape modulo $2 ^ w$, like every other value, so the machine is total in its input and honesty about inputs whose entries do not fit into a word lives on the statement side, in the set of admissible inputs a claim quantifies over.

Reading and writing are total: a $halt$ instruction halts the machine, an out-of-range program counter halts it, a read from an exhausted input tape halts it, and every memory cell holds a number, so no error states are needed. $Instr.effect$ is the whole of the instruction semantics and $step$ adds only the fetch, returning $none$ exactly when the machine has halted, so the semantics is deterministic and total by construction. $run w p t$ is $t$-fold application of $step$, and it is $none$ as soon as the machine halts, which is what makes "halts after exactly $t$ steps" in $RunsTo$ a statement about the number of instructions executed: the time measure is intrinsic to the machine and is not an annotation carried alongside the program. $RunsTo$ constrains the output tape and nothing else: memory is scratch space and is left unconstrained on halting.

The input and output tapes are what makes the machine's memory start out empty, and hence what lets a program address it by fixed cell numbers; an input laid out in memory instead would begin at a cell number depending on the input length. A program that wants random access to its input copies it into memory first, at a cost of one instruction per number.

Time is the machine's own step count, one unit per instruction, and it is honest for multiplication precisely because the factors are words. There is no space measure: it would be a further definition over $run$, and space is in any case bounded by the $2 ^ w$ cells the machine can address. Randomness is absent as well; a randomized program is a deterministic program that consumes a word list of random numbers, which is definable downstream over this same machine, with no change to the model.