Two WordRAM models: simulation and runtime transfer

widened. For every word width $w$ whose bit count $s=w.\mathrm{bits}$ is a positive natural number, this definition returns the positive word width with exactly $s+4$ bits; it has no dependence on a program, input, or problem size.

zigzag. This function sends each integer $a\ge 0$ to the natural number $2a$, and sends each negative integer written uniquely as $-(a+1)$ with $a\in\mathbb N$ to $2a+1$. In particular, $0,-1,1,-2$ map respectively to $0,1,2,3$.

unzigzag. For every natural number $a$, this function returns the integer $a/2$ when $a$ is even, and the integer $-(\lfloor a/2\rfloor+1)$ when $a$ is odd, where natural-number division is rounded down. In particular it returns $0$ at $a=0$.

wordramAddress. For every natural-number source address $a$, this definition returns the integer target address $8+2a$, without any modular reduction. Its image is exactly the even integer addresses at least $8$.

apspAddress. For every integer source address $a$, this definition returns the natural-number target address $8+2z(a)$, where $z(a)=2a$ for $a\ge0$ and $z(-(b+1))=2b+1$ for $b\in\mathbb N$. Addresses undergo no modular reduction; the image is exactly the even natural-number addresses at least $8$.

encodeWordRAMMemory. Given a positive bit width $s$ and any memory $m:\mathbb N\to\{0,\ldots,2^s-1\}$, this defines an integer-addressed memory of $(s+4)$-bit words. Address $0$ contains the $(s+4)$-bit encoding of $s$. At every even integer address $a\ge8$, it contains the zero-extended unsigned source word $m(\lfloor(a-8)/2\rfloor)$; every other address, including every negative address, contains zero. Thus source cell $b$ is copied to cell $8+2b$. The memory may have infinitely many nonzero source cells; no finite-support assumption is imposed.

encodeAPSPMemory. Given a positive bit width $s$ and any integer-addressed memory $m$ of $s$-bit words, this defines a natural-number-addressed memory of $(s+4)$-bit words. Cell $0$ contains $s$. At an even address $a\ge8$, let $c=(a-8)/2$; the cell contains the zero-extended unsigned bit pattern of $m(c/2)$ if $c$ is even, and of $m(- (\lfloor c/2\rfloor+1))$ if $c$ is odd. Every remaining cell, including cell $1$, contains zero. Equivalently, source address $b$ is stored at $8+2z(b)$, where $z(b)=2b$ for $b\ge0$ and $z(-(j+1))=2j+1$. There is no restriction on the source memory's support.

WordRAMMemoryRelated. For every positive source bit width $s$, natural-number-addressed source memory $m$ of $s$-bit words, and integer-addressed target memory $M$ of $(s+4)$-bit words, this proposition says that for every natural address $a$, $M(8+2a)$ equals the zero-extension of the unsigned bit pattern $m(a)$. It constrains all source cells, including arbitrarily large addresses, and leaves every target cell outside these addresses unconstrained.

APSPMemoryRelated. For every positive source bit width $s$, integer-addressed source memory $m$ of $s$-bit words, and natural-number-addressed target memory $M$ of $(s+4)$-bit words, this proposition says that for every integer address $a$, $M(8+2z(a))$ equals the zero-extension of the unsigned source bit pattern $m(a)$, where $z(a)=2a$ for $a\ge0$ and $z(-(j+1))=2j+1$. All positive and negative source cells are constrained; target cells outside this image, including cells $0$ and $1$, are not constrained by this relation.

wordramHalt. Given a fixed finite width-independent multiplication-model program $P$, a positive bit width $s$, two arbitrary memories $m,M$ on natural-number addresses with $s$-bit words, and a natural fuel bound $t$, this proposition says that execution from memory $m$, program counter $0$, tick count $0$, and halt flag false, after being allowed $t$ interpreter steps, has halt flag true and memory exactly $M$. The program permits copying, addition, subtraction, multiplication modulo $2^s$, zero-filling left and right shifts by unsigned word values, bitwise AND, OR and NOT, unconditional jumps, unsigned equality/strict-order/non-strict-order branches, and explicit halt; operands may be natural immediates reduced modulo $2^s$ or memory reads, with natural direct addresses or indirect addresses obtained from unsigned pointer words. There are no native constants. Each executed instruction, including halt, costs one step; after halt the state stays fixed, and an invalid instruction fetch leaves the machine stuck without setting its halt flag. Thus this means explicit halt within $t$ steps, not first halt exactly at $t$; it is false for $t=0$, and equality of output memories includes every address.

apspHalt. Given a finite signed-addressed program $P$, a positive bit width $s$, arbitrary integer-addressed $s$-bit input and output memories $m,M$, a natural fuel bound $t$, and a Boolean $v$, this proposition says that execution beginning at program position $0$ with memory $m$ returns exactly verdict $v$ and final memory $M$ within $t$ steps. Instructions write the constant one, add, subtract or multiply words modulo $2^s$, load or store indirectly using a pointer word's signed two's-complement value, branch to a natural program position on a negative signed word, accept, or reject; literal memory addresses are integers. Ordinary writes advance to the next instruction. Each instruction, including acceptance, rejection, or the default rejection for a fetch beyond the program, consumes one fuel step; zero fuel returns no result. Consequently the proposition is false at $t=0$, and a successful result need not first occur exactly at the supplied bound.

simulationBound. For arbitrary natural numbers $C,d,t$ and a positive word width with bit count $s$, the defined natural number is exactly $C(t+s+1)(s+1)^d$. In particular $C=0$ gives zero, $d=0$ removes the power factor, and $t=0$ still leaves the additive width term.

WordRAMToAPSP. For a fixed finite width-independent natural-addressed multiplication program $P$ without native constants, a finite integer-addressed add/subtract/multiply/load/store/negative-branch/accept/reject program $Q$, and arbitrary naturals $C,d$, this proposition requires both following implications for every positive source bit width $s$ and every source memory $m$, with no support restriction. Initialize $Q$ at width $s+4$ with cell $0$ equal to $s$, cell $8+2a$ equal to the zero-extended unsigned word $m(a)$ for every natural $a$, and all other cells zero. For every natural $t$ and memory $m'$, if $P$ from its fresh state on $m$ explicitly halts within $t$ unit instruction steps with memory $m'$, there exist a natural $u\le C(t+s+1)(s+1)^d$ and a target memory $M$ such that $Q$ from position zero accepts within $u$ steps with memory $M$, and $M(8+2a)$ equals the zero-extended $m'(a)$ for every natural $a$. Conversely, for every natural $u$, Boolean $v$, and target memory $M$, if this initialized $Q$ returns $(v,M)$ within $u$ steps, then $v$ is true and there exist $t\le u$ and a source memory $m'$ such that $P$ explicitly halts within $t$ steps with memory $m'$ and the same equality holds at every embedded source address. Source out-of-range fetches are stuck rather than successful halts; target out-of-range fetches reject. Both halting steps are counted, both start at program counter zero, and no run succeeds with zero fuel. The definition does not require $C>0$ and gives no additional conditions on target output cells outside the embedded memory.

APSPToWordRAM. For a finite integer-addressed add/subtract/multiply/load/store/negative-branch/accept/reject program $P$, a fixed finite width-independent natural-addressed multiplication program $Q$ without native constants, and arbitrary naturals $C,d$, the following holds for every positive source bit width $s$ and every integer-addressed source memory $m$. Initialize $Q$ at width $s+4$ with cell $0$ equal to $s$, cell $8+2z(a)$ equal to the zero-extended unsigned word $m(a)$ for every integer $a$, and all other cells zero, where $z(a)=2a$ for $a\ge0$ and $z(-(j+1))=2j+1$. For every natural $t$, Boolean $v$, and source memory $m'$, a source return $(v,m')$ from position zero within $t$ steps implies the existence of a natural $u\le C(t+s+1)(s+1)^d$ and target memory $M$ such that $Q$ from its fresh state explicitly halts within $u$ steps with memory $M$, the unsigned value of $M(1)$ is $1$ for true $v$ and $0$ for false $v$, and $M(8+2z(a))$ is the zero-extension of $m'(a)$ for every integer $a$. Conversely, for every natural $u$ and memory $M$, any explicit halt of this initialized $Q$ within $u$ steps implies the existence of $t\le u$, a Boolean $v$, and a source memory $m'$ giving a source return $(v,m')$ within $t$ steps and exactly those same verdict-cell and embedded-memory equalities. All instruction and halting steps cost one; source out-of-range fetches reject, target invalid fetches are stuck, and zero fuel never succeeds. Neither finite support nor $C>0$ is required, and other target output cells are unconstrained.

UniformOperationalSimulation. For a natural exponent $d$, this proposition is the conjunction of two uniform existence assertions. Every finite width-independent natural-addressed multiplication program $P$ without native constants has a finite signed-addressed arithmetic/load/store/negative-branch/accept/reject simulator $Q$ and a positive natural constant $C$; every finite program $P$ of the latter kind has a finite width-independent native-free multiplication simulator $Q$ of the former kind and a positive natural constant $C$. In either direction $Q,C$ are chosen before the positive source width $s$, arbitrary source memory, and fuel bounds. The target width is $s+4$, cell $0$ initially contains $s$, every source bit pattern is zero-extended into cell $8+2a$ for natural source addresses or $8+2z(a)$ for integer source addresses, with $z(a)=2a$ for $a\ge0$ and $z(-(j+1))=2j+1$, and other target cells initially vanish. Every source halt within any bound $t$ has a target halt within some $u\le C(t+s+1)(s+1)^d$ preserving every embedded memory cell. Every target halt within any bound $u$ arises from a source halt within some $t\le u$ preserving those same cells. Natural-addressed source explicit halts become acceptance and every target verdict is true; in the reverse direction the source Boolean verdict is recorded as unsigned $0$ or $1$ in target cell $1$. Execution begins at position zero, natural-addressed runs begin unhalted with zero ticks, halting instructions cost one, signed-addressed invalid fetches reject, and natural-addressed invalid fetches do not halt. The same $d$ serves both directions and all programs; the simulators and constants may depend on the source program.

packedInitialMemory. For every positive bit width $s$, natural size $n$, and finite list of integers $x$, this defines a memory on all natural addresses: cell $0$ contains $n$ modulo $2^s$, cells $1$ through the length of $x$ contain the entries of $x$ in order, each reduced modulo $2^s$, and every later cell contains zero. The size and the list length need not agree, and no representability or magnitude assumption is made; $n=0$ and the empty list are allowed.

wordramSolvedBy. Given a problem $Q$ consisting of an instance type at each natural size, an integer input list, a decision predicate, and a predicate on integer output sequences, a natural size $n$ (an implicit argument), an instance $x$ of size $n$, a fixed finite width-independent natural-addressed multiplication program $P$ without native constants, a positive bit width $s$, and a natural bound $t$, this says that there exist a Boolean $v$ and an $s$-bit output memory $M$ such that $P$, started at position zero, unhalted and with zero ticks, explicitly halts within $t$ unit steps on the memory containing $n$ in cell $0$, $Q$'s input list in subsequent cells, and zeros elsewhere, all entries reduced modulo $2^s$. The unsigned value of $M(0)$ must equal the Boolean encoding of $v$ ($0$ or $1$), $v$ is true if and only if the decision predicate holds for $x$, and the output predicate must hold for the sequence whose term at each natural $a$ is the signed two's-complement value of $M(1+|Q.\mathrm{input}(x)|+a)$. Thus the output starts immediately after the input and is required even for a rejecting verdict. No input-size promise or adequacy of the width is assumed here; invalid fetches are not successful halts, and $t=0$ cannot satisfy the proposition.

APSPSolves. Given a problem $Q$ with size-indexed instances, integer input lists, decision and output predicates, naturals $\kappa,b$, a fixed finite signed-addressed arithmetic/load/store/negative-branch/accept/reject program $P$, and a function $T:\mathbb N\to\mathbb N$, this proposition says: for every natural size $n$ and every instance $x$ of size $n$ whose every input integer $a$ satisfies $|a|\le n^\kappa$, and for every natural bit width $W\ge b(\operatorname{log2} n+1)$, running $P$ at position zero with $n$ in cell $0$, the input list in subsequent nonnegative cells, and zeros everywhere else (including negative addresses), all values reduced modulo $2^W$, returns some Boolean $v$ and memory $M$ within $T(n)$ unit steps. It requires $v=\mathrm{true}$ if and only if $Q$'s decision predicate holds, and requires $Q$'s output predicate on the signed values $M(1+|Q.\mathrm{input}(x)|+a)$ for all natural output indices $a$. Accept, reject, and default out-of-range rejection each count as a step. The program, $b$, and $T$ are fixed for all $n,x,W$; there is no upper bound on $W$ and the runtime bound is independent of $W$. Here $\operatorname{log2}0=0$ and it is the floor of the base-two logarithm for positive $n$; sizes zero and one are included, as are $\kappa=0$ with $0^0=1$ and $b=0$, in which case width zero is also required. The input promise is vacuous for an empty input list; no instance satisfies any additional, unstated promise.

WordRAMSolves. Given a problem $Q$ with size-indexed instances, integer input lists, decision and output predicates, naturals $\kappa,b$, a fixed finite width-independent natural-addressed multiplication program $P$ without native constants, and a function $T:\mathbb N\to\mathbb N$, this requires that for every natural $n$, every instance $x$ of size $n$ whose input integers all satisfy $|a|\le n^\kappa$, and every positive bit width $s\ge b(\operatorname{log2}n+1)$, the fresh run of $P$ from position zero explicitly halts within $T(n)$ unit instruction steps on memory containing $n$, followed by the input list, followed by zeros, with every value reduced modulo $2^s$. Some Boolean $v$ and final memory $M$ must have the unsigned value of cell $0$ equal to the encoding $0$ or $1$ of $v$, have $v$ true exactly when the decision predicate holds, and satisfy the output predicate on the signed values in cells $1+|Q.\mathrm{input}(x)|+a$, for every natural output index $a$. The output condition applies to either verdict. An invalid fetch does not count as a halt. The fixed program's natural immediates are reduced at each width. All sufficiently large positive physical widths are required with the same $T(n)$ and no upper width bound; $b$ may be zero but width zero is excluded. The cases $n=0,1$, $\kappa=0$, empty input lists, and empty instance types are included, with $\operatorname{log2}0=0$ and $0^0=1$.

WordRAMSolvedInTime. For a problem $Q$ with size-indexed instances, integer input lists and decision/output predicates, and any rational $r=p/e$ in its reduced representation with positive denominator $e$, this proposition requires that for every natural input-magnitude exponent $\kappa$ there exist a finite width-independent native-free natural-addressed multiplication program $P$, a natural $b$, and $T:\mathbb N\to\mathbb N$ such that for some natural $A$, $T(n)^e\le A n^{\max(p,0)}$ for every $n\ge2$, and the following correctness holds for every natural $n$ and every size-$n$ instance whose input integers have absolute values at most $n^\kappa$: at every positive width $s\ge b(\operatorname{log2}n+1)$, $P$ explicitly halts within $T(n)$ unit steps on the packed memory consisting of $n$, the input list, then zeros, all reduced modulo $2^s$. Its final cell $0$ is unsigned $0$ or $1$, indicating the truth of the decision predicate, and the signed words immediately after the input satisfy the output predicate. The witnesses may depend on $\kappa$, but not on $n$, the instance, or the physical width. Correctness includes $n=0,1$ while the displayed growth inequality does not; $\operatorname{log2}0=0$, $0^0=1$, and $b=0$ is allowed. The definition accepts negative $r$, for which the exponent of $n$ in the growth inequality is truncated to zero rather than interpreted as a negative power.

ioBound. For arbitrary natural $K,q,n$, this defines exactly $K(n+1)^q$. In particular it is $0$ for $K=0$, it is $K$ for $q=0$, and it is $K$ at $n=0$.

FiniteIO. Given a problem $Q$ with size-indexed instances, integer input lists and decision/output predicates and naturals $K,q$, this proposition is the conjunction of: for every natural size $n$ and every size-$n$ instance $x$, the input list has length at most $B(n)=K(n+1)^q$; and for every such $n,x$ and every two integer sequences $f,g:\mathbb N\to\mathbb Z$, equality $f(a)=g(a)$ at all natural indices $a<B(n)$ implies equivalence of the output predicate evaluated at $f$ and at $g$. There is no restriction on the decision predicate, input magnitudes, or output magnitudes, and the conditions apply to all instances rather than only instances meeting a magnitude promise. At $K=0$ every input list must be empty and the output predicate must have the same truth value for every pair of sequences, though that value may be false; at $n=0$ the bound is $K$. Any condition at a size having no instances is vacuous.

transferBound. For arbitrary natural constants $C,d,K,q$, any function $T:\mathbb N\to\mathbb N$, and any natural size $n$, this defines exactly $C\bigl(T(n)+K(n+1)^q+1\bigr)(\operatorname{log2}n+1)^d$, where $\operatorname{log2}0=0$ and $\operatorname{log2}n=\lfloor\log_2n\rfloor$ for positive $n$. The expression has no physical-word-width argument. It is zero if $C=0$, its logarithmic factor is one if $d=0$ or $n\in\{0,1\}$, and it includes the input/output polynomial even if $T(n)=0$.

UniformTimeTransfer. For a natural $d$, this proposition quantifies over every problem $Q$ and every pair of naturals $K,q$ for which, at every natural size $n$ and every instance, the input length is at most $B(n)=K(n+1)^q$ and the output predicate depends only on the first $B(n)$ entries of its integer output sequence. It asserts transfer in both directions between finite signed-addressed arithmetic/load/store/negative-branch/accept/reject programs and finite width-independent native-free natural-addressed multiplication programs. In either direction, for every natural input-magnitude exponent $\kappa$, source program $P$, natural threshold coefficient $b$, and function $T:\mathbb N\to\mathbb N$, if the source correctly solves $Q$ within $T(n)$ steps for every $n$, every instance with input values bounded in absolute value by $n^\kappa$, and every source physical width at least $b(\operatorname{log2}n+1)$, then there exist a target program $P'$, natural $b'$, and positive natural $C$ solving exactly the same instances at every target width at least $b'(\operatorname{log2}n+1)$ within $C(T(n)+B(n)+1)(\operatorname{log2}n+1)^d$ steps. Widths are arbitrary naturals for the signed-addressed machine, including zero when its threshold permits, and positive naturals for the natural-addressed machine. Both solvers start at position zero on ordinary packed input $n$, then the input integers, then zeros (also zero at all negative addresses for the signed-addressed machine), with values reduced modulo $2^W$, where $W$ is the physical bit width; signed outputs immediately after the input satisfy $Q$'s output predicate. Correctness requires acceptance exactly for the decision predicate in the signed-addressed machine, and explicit halt with that Boolean encoded as unsigned $0$ or $1$ in cell zero in the natural-addressed machine. Halting steps count, signed-addressed out-of-range fetches reject, and natural-addressed invalid fetches do not halt. Witnesses $P',b',C$ may depend on all preceding source data, but not on $n$, the instance, or physical width. The assertion does not assume any growth bound on $T$, includes $n=0,1$, $\kappa=0$, $K=0$ and $q=0$, and uses $\operatorname{log2}0=0$ and $0^0=1$.

APSPBelow. For any problem $Q$ with size-indexed instances and integer input/decision/output data, and any rational threshold $R$, this proposition asserts the existence of a rational $r<R$ such that for every natural $\kappa$ there exist a finite signed-addressed arithmetic/load/store/negative-branch/accept/reject program $P$, a natural $b$, and $T:\mathbb N\to\mathbb N$ satisfying both: if $r=p/e$ has positive reduced denominator $e$, there is a natural $A$ with $T(n)^e\le A n^{\max(p,0)}$ for all $n\ge2$; and for every natural size $n$, every size-$n$ instance with all input absolute values at most $n^\kappa$, and every natural width $W\ge b(\operatorname{log2}n+1)$, $P$ returns within $T(n)$ counted instruction steps the correct Boolean verdict and a memory whose signed words immediately after the input satisfy the output predicate. The run starts at position zero with $n$, then the input list, then zeros, all reduced modulo $2^W$, and negative cells initially zero; out-of-range fetches reject. The exponent $r$ is chosen before $\kappa$; program, $b$, and $T$ may depend on $\kappa$, but not on size, instance, or width. Sizes $0,1$ still require correctness; $b=0$ includes width zero, $\operatorname{log2}0=0$, $0^0=1$, and negative rational exponents use the displayed numerator truncation.

WordRAMBelow. For any problem $Q$ with size-indexed instances and integer input/decision/output data, and any rational threshold $R$, this asserts that some rational $r<R$ has the following property: for every natural $\kappa$, there exist a fixed finite width-independent natural-addressed multiplication program $P$ without native constants, a natural $b$, and $T:\mathbb N\to\mathbb N$ such that, writing $r=p/e$ in reduced form with $e>0$, some natural $A$ satisfies $T(n)^e\le A n^{\max(p,0)}$ for every $n\ge2$, and for every natural $n$, every size-$n$ instance whose input absolute values are at most $n^\kappa$, and every positive physical width $s\ge b(\operatorname{log2}n+1)$, $P$ explicitly halts within $T(n)$ unit instruction steps on packed memory $n$, then input, then zeros, all reduced modulo $2^s$. Final cell zero must be unsigned $0$ or $1$ and indicate exactly the decision predicate, and the signed output cells immediately after the input must satisfy the output predicate. An invalid fetch is not a successful halt. The exponent is chosen before $\kappa$, and each program, $b$, and $T$ is fixed before the size, instance, and width. Correctness includes sizes $0,1$ although the growth condition does not; $b=0$ still permits only positive widths, $\operatorname{log2}0=0$, $0^0=1$, and a negative numerator is truncated to zero in the growth condition.

FineGrainedTimeEquivalence. For every problem $Q$ and naturals $K,q$ such that every size-$n$ input has length at most $K(n+1)^q$ and, for every instance and every two integer output sequences agreeing at indices below this bound, the output predicate has equivalent truth values, this proposition requires the following for every rational $R>q$: there exists a rational $r<R$ with a signed-addressed arithmetic/load/store/negative-branch/accept/reject solver of exponent $r$ if and only if there exists a rational $r'<R$ with a native-free natural-addressed multiplication solver of exponent $r'$. An exponent $p/e$ (positive reduced denominator) means that for every natural magnitude exponent $\kappa$ there are a fixed finite program, a natural $b$, and $T:\mathbb N\to\mathbb N$ with $T(n)^e\le A n^{\max(p,0)}$ for all $n\ge2$ and some natural $A$, solving every size-$n$ instance whose input absolute values are at most $n^\kappa$, at every physical width at least $b(\operatorname{log2}n+1)$, within $T(n)$ counted steps. Widths may be zero for the signed-addressed machine and must be positive for the natural-addressed machine. Runs use packed size and integer input, reduced modulo $2^W$, where $W$ is the physical bit width, with all other cells initially zero; they return the correct verdict and signed output immediately after the input, the natural-addressed verdict being encoded as unsigned $0$ or $1$ in final cell zero and requiring explicit halt. Correctness includes $n=0,1$, with $\operatorname{log2}0=0$ and $0^0=1$; the growth condition truncates negative numerators. The two rational exponents, programs, width thresholds, and runtime functions need not coincide, and the equivalence itself does not assert that either solver exists. No conclusion at $R\le q$ is included.

sourceProblem. For every problem $Q$ in the namespace EndStatement, this constructs a problem in the namespace TrulySubcubicAPSP with exactly the same instance type at every natural size $n$, exactly the same integer input list for each instance, exactly the same decision predicate, and exactly the same output predicate for every integer sequence indexed by the naturals. No encoding, restriction on instances or integer magnitudes, or change to the output condition is applied; this declaration contains no assertion about programs or runtime.