\section{Components}
Our chip consists of the following static components:

\begin{itemize}
	\item An ALU: $\ALUOp \times \Word8 \times \Word8 \to \Word8$.
	\item The program memory $\prog$: $\Prog \eqdef \Word4^{256}$.
\end{itemize}

And these volatile components:

\begin{itemize}
	\item A memory $\mem$: $\Mem \eqdef \Word8^{256}$. Individual words or cells
		are addressed with one word. We write $\mem.n$ for the cell in $\mem$ at
		address $n$. We write $\update{\mem}{n\mapsto k}$ for the memory $\mem'$
		with
		$$
			\mem'.i = \begin{cases}
				k      & \text{if $i=n$,}\\
				\mem.i & \text{otherwise.}
			\end{cases}
		$$
	\item The accumulators $\acc1$ and $\acc2$ are located at address $0$ and
		$1$ of the memory, respectively.
	\item The program counter $\pc$ is located at address $2$ of the memory.
\end{itemize}

A state $\st$ can be seen as a tuple $(\prog,\mem)$. We define the set of all
states $\State \eqdef \Word4^{256} \times \Word8^{256}$. An instruction is a
function $\Mem\to\Mem$. The instruction cycle is a function $\State\to\State$.