The register-transfer format follows Cook and Reckhow (Time bounded random access machines, JCSS 7, 1973): instructions act on numbered cells, with indirection through a cell holding an address. Their cells hold signed integers, and their sequential input has a distinguished zero end marker outside its input alphabet. This definition instead uses unsigned words, supplies explicit EOF detection, and additionally provides indexed read-only input with its length available in constant time. It therefore specifies its own input convention; the interface is not an identification with the original Cook–Reckhow input tape.

Word operations have unit cost, as in the bounded-word models of Fredman and Willard (Surpassing the information theoretic bound with fusion trees, JCSS 47, 1993) and Hagerup (Sorting and searching on the word RAM, STACS 1998). Comparisons with other word-RAM presentations must fix the available operations, input convention, and address-space assumptions. Indexed input avoids a compulsory input scan, as in an input-array RAM. A simulation that instead starts from sequential input and loads an $n$-word array pays an additive $O(n)$ cost, giving $O(n + T)$, which is $O(T)$ only under a suitable lower bound on $T$. No unconditional constant-factor model-equivalence claim is made here.

$setCell$ reduces each value stored and each destination address modulo $2 ^ w$. Other data-memory operands and indirect addresses are reduced at use; output and input values are reduced too. From initialization, every reachable memory cell holds a word. The function representation of memory has domain $ℕ$, but execution accesses only the residues below $2 ^ w$. Program control is separate: $jump$, $jzero$, and $jeof$ use untruncated program labels, ordinary advancement increments the full program counter, and instruction fetch uses that counter.

Oversized input entries and the length are reduced rather than rejected. To recover an entry unchanged requires that entry to be below $2 ^ w$; to recover the complete original length with $inputLength$ requires $x.length < 2 ^ w$. These fitting conditions belong in the admissible domain of the theorem that needs them. EOF-based programs can process lists whose total length does not fit in a word. Indexed reads can address the prefix with indices below $2 ^ w$; the initial array itself is read-only input storage, separate from writable memory.

Subtraction is natural-number monus, so a comparison is $sub$ followed by $jzero$. Complement is $2 ^ w - 1 - m[b]$. No instruction returns the word length. The following operations are derived at constant cost, with scratch cells $t$ and $u$ whose physical addresses modulo $2 ^ w$ are distinct from each other and from every operand's physical address. Distinct natural-number literals alone do not ensure this condition:

An explicit $halt$, an exhausted $read$, or an out-of-range program counter terminates execution. $step$ returns $none$ in all three cases. $run w p k$ counts successful transitions only. $RunsTo$ adds the cost of the fetched terminal instruction: one for $halt$ or exhausted $read$, and zero for an out-of-range counter, where no instruction exists. Thus $RunsTo$ counts every executed instruction exactly once, and an empty program costs zero. Termination constrains the entire output tape; memory is left unconstrained.

The separate read-only input preserves a fixed working-memory layout. An input-in-memory convention could also reserve fixed low-address working cells and put input at a fixed base; no length-dependent input base is necessary. Copying this model's input into writable memory, when desired and when the chosen layout fits, takes constant overhead per word and linear total time: a uniform loader uses $read$ into a temporary cell, an indirect $store$, and loop maintenance.

There is no separate space measure or randomness primitive. A space measure can be defined over executions; writable memory has $2 ^ w$ cells. A deterministic program can consume additional input words to model supplied random choices.