Read-back: Def_SmaleNinth_BSSMachine.lean (namespace SmaleNinth)

BSSInstr. An inductive type with exactly ten constructors, each carrying the listed data:

• $\mathsf{const}(dst, c)$ with $dst \in \mathbb{Z}$ and $c \in \mathbb{R}$;
• $\mathsf{add}(dst, i, j)$, $\mathsf{sub}(dst, i, j)$, $\mathsf{mul}(dst, i, j)$, $\mathsf{div}(dst, i, j)$, each with $dst, i, j \in \mathbb{Z}$;
• $\mathsf{shiftL}$ and $\mathsf{shiftR}$, carrying no data;
• $\mathsf{jle}(i, target)$ with $i \in \mathbb{Z}$ and $target \in \mathbb{N}$;
• $\mathsf{accept}$ and $\mathsf{reject}$, carrying no data.

At the level of the type itself these are pure data; the constructors acquire operational meaning only through BSSStep below. Note that the constant $c$ in $\mathsf{const}$ may be any real number, with no restriction (e.g. to rationals or computable reals), and the addresses $dst, i, j$ may be any integers, including negative ones. The jump target of $\mathsf{jle}$ is a natural number and is not required to lie within any program.

BSSProgram. Definitionally, a finite list of BSSInstr values (possibly empty). Instructions are indexed by their position in the list, starting at $0$.

BSSConfig. A structure with two fields: a program counter $pc \in \mathbb{N}$, and a tape $tape : \mathbb{Z} \to \mathbb{R}$, i.e. an assignment of one real number to every integer address (a bi-infinite tape of real registers). There is no constraint relating $pc$ to any program, and the tape is an arbitrary function with no finiteness or support condition.

BSSStep. A (noncomputable) total function taking a program $P$ and a configuration $s = (pc, x)$, where $x : \mathbb{Z} \to \mathbb{R}$ is the tape, and returning a new configuration, by case analysis on the optional lookup of the $pc$-th element of the list $P$:

• If $pc \ge |P|$ (the lookup returns nothing), the result is $s$ itself, unchanged.
• If the instruction at position $pc$ is:
  • $\mathsf{const}(dst, c)$: the new configuration is $(pc+1,\; x[dst \mapsto c])$, where $x[dst \mapsto v]$ denotes the function equal to $x$ everywhere except at address $dst$, where it takes the value $v$;
  • $\mathsf{add}(dst,i,j)$: $(pc+1,\; x[dst \mapsto x_i + x_j])$; similarly $\mathsf{sub}$ gives $x[dst \mapsto x_i - x_j]$, $\mathsf{mul}$ gives $x[dst \mapsto x_i \cdot x_j]$, and $\mathsf{div}$ gives $x[dst \mapsto x_i / x_j]$. In all four cases the operands $x_i, x_j$ are read from the old tape (so even when $dst = i$ or $dst = j$ the old values are used), and the division is Lean's total real division, under which $r / 0 = 0$ for every real $r$;
  • $\mathsf{shiftL}$: $(pc+1,\; k \mapsto x_{k+1})$ — every cell takes the old value of its right neighbour;
  • $\mathsf{shiftR}$: $(pc+1,\; k \mapsto x_{k-1})$ — every cell takes the old value of its left neighbour;
  • $\mathsf{jle}(i, target)$: if $x_i \le 0$ then $(target,\; x)$, otherwise $(pc+1,\; x)$; the tape is unchanged in both branches;
  • $\mathsf{accept}$ or $\mathsf{reject}$: the result is $s$ itself, unchanged.

Thus a configuration whose counter sits on $\mathsf{accept}$, on $\mathsf{reject}$, or beyond the end of the program is a fixed point of the step function. A $\mathsf{jle}$ may jump to a position outside the program, after which the configuration is likewise fixed.

BSSRun. For a program $P$, an initial tape $x : \mathbb{Z} \to \mathbb{R}$, and $t \in \mathbb{N}$, $\mathrm{BSSRun}(P, x, t)$ is the $t$-fold iterate of $\mathrm{BSSStep}(P, \cdot)$ applied to the configuration $(0, x)$ — i.e. the configuration after exactly $t$ steps, starting with program counter $0$ and tape $x$. For $t = 0$ it is $(0, x)$ itself.

BSSHaltedWith. For a program $P$, a configuration $s$, and a Boolean $b$, the proposition asserting that the lookup of the instruction at position $s.pc$ in $P$ yields exactly $\mathsf{accept}$ when $b = \mathrm{true}$, and exactly $\mathsf{reject}$ when $b = \mathrm{false}$. In particular a configuration whose counter points outside the program does not satisfy this for either value of $b$, even though it is a fixed point of the step function; and a configuration on any other instruction satisfies it for neither value of $b$.

BSSDecidesInTime. For a program $P$, an initial tape $x$, a time bound $T \in \mathbb{N}$, and a Boolean $b$, the proposition

$$\exists\, t \le T,\quad \mathrm{BSSHaltedWith}\big(P,\; \mathrm{BSSRun}(P, x, t),\; b\big),$$

i.e. there exists some number of steps $t$ with $0 \le t \le T$ (the bound is non-strict, and $t = 0$ is allowed) such that the configuration reached from $(0, x)$ after exactly $t$ steps has its program counter on $\mathsf{accept}$ (if $b = \mathrm{true}$) or on $\mathsf{reject}$ (if $b = \mathrm{false}$). Nothing in this definition asserts uniqueness of $t$ or of $b$, and nothing counts instructions in any other way: "time" here is precisely the number of iterations of the step function, each iteration costing one unit regardless of the instruction executed.

matrixEntryRM. For natural numbers $m, n$ (implicit), a real matrix $A \in \mathbb{R}^{m \times n}$ (indexed by $\{0,\dots,m-1\} \times \{0,\dots,n-1\}$), and $k \in \mathbb{N}$, this returns

$$\mathrm{matrixEntryRM}(A, k) \;=\; \begin{cases} A_{\lfloor k/n \rfloor,\; k \bmod n} & \text{if } k < m n \text{ and } 0 < n,\\[2pt] 0 & \text{otherwise,}\end{cases}$$

where $\lfloor k/n \rfloor$ and $k \bmod n$ are natural-number division and remainder (the stated side conditions guarantee both indices are in range). So it is the $k$-th entry of the row-major enumeration of $A$, with junk value $0$ whenever $k \ge mn$ or $n = 0$ (in particular it is identically $0$ when $m = 0$ or $n = 0$).

encodeLP. For natural numbers $m, n$ (implicit), a matrix $A \in \mathbb{R}^{m \times n}$, and a vector $b \in \mathbb{R}^m$ (a function on $\{0,\dots,m-1\}$), this is the tape $\mathbb{Z} \to \mathbb{R}$ defined by cases on the address $k \in \mathbb{Z}$, tested in the following order:

1. if $k = 0$: the value is the real number $m$ (the natural number $m$ cast to $\mathbb{R}$);
2. else if $k = 1$: the value is the real number $n$;
3. else if $2 \le k$ and $k < 2 + mn$ (with $m, n$ cast to $\mathbb{Z}$): the value is $\mathrm{matrixEntryRM}(A, (k-2)_{\ge 0})$, where $(\cdot)_{\ge 0}$ is the truncation of an integer to a natural number (here $k - 2 \ge 0$, so no truncation occurs); by the previous paragraph this equals the row-major entry $A_{\lfloor (k-2)/n \rfloor,\, (k-2) \bmod n}$;
4. else if $2 + mn \le k$ and $k < 2 + mn + m$: the value is $b_{(k - (2+mn))_{\ge 0}}$, the index lying in $\{0, \dots, m-1\}$ by the range condition;
5. otherwise (in particular for every negative $k$ and every $k \ge 2 + mn + m$): the value is $0$.

Edge cases the definition silently includes: when $mn = 0$ case 3 is an empty range, and when $m = 0$ case 4 is empty, so for $m = 0$ or $n = 0$ the tape holds only the two header cells (which then contain $0$ where the dimension is zero) and is $0$ elsewhere. There is no marker distinguishing genuine zero entries of $A$ or $b$ from the ambient zero padding beyond the dimensions stored in cells $0$ and $1$.