\section{Instruction Set}
\label{sec:instr}

\subsection{The Instruction Cycle}
The instruction cycle is a function $\State\to\State$. It is defined as
follows:

$$\mathit{cycle}(\prog,\mem) \eqdef (\prog, \instr{\mem.\pc}{\mem})$$

Here, $\instrop$ is a function that maps words to instructions: $\instrop :
\Word6 \to \Mem \to \Mem$. It is defined in \autoref{sec:instr}.

\subsection{Instructions}
The binary representations of the commands defined can be found in
\autoref{fig:instr:instr-set}.

\begin{table}[b]
	\centering
	{\tt
	\begin{tabular}{!>{\normalfont}l | ^l | *{6}{|^c}}
		\rowstyle{\normalfont\bfseries}
		Instruction name & Assembly & 5 & 4 & 3 & 2 & 1 & 0 \\\hline
		Addition         & add      & 1 & 0 & 0 & 0 & 0 & 0 \\\hline
		Logical NAND     & nand     & 1 & 0 & 0 & 0 & 0 & 1 \\\hline
		Equality         & eq       & 1 & 0 & 0 & 0 & 1 & 0 \\\hline
		Conditional jump & cjmp     & 1 & 1 & 0 & 0 & 0 & 0 \\\hline
		Store register   & str      & 1 & 1 & 1 & 1 & 1 & 0 \\\hline
		Load register    & ld       & 1 & 1 & 1 & 1 & 1 & 1 \\\hline
		Store literal 1  & lit1     & 0 & 0 & \multicolumn{4}{c}{$k$} \\\hline
		Store literal 2  & lit2     & 0 & 1 & \multicolumn{4}{c}{$k$} \\
	\end{tabular}
	}
	\caption{Instruction set\label{fig:instr:instr-set}}
\end{table}

The instructions are now described. For this we define an auxiliary function
$\incpcop$, which increments the program counter:
$$\incpc{\mem} = \update{\mem}{\pc\mapsto\mem.\pc+1}$$

\subsubsection{Addition}
$$
	\instr{\texttt{100000}}{\mem} \eqdef
	\incpc{\update{\mem}{\acc1\mapsto\mem.\acc1+\mem.\acc2}}
$$

\subsubsection{Logical NAND}
$$
	\instr{\texttt{100001}}{\mem} \eqdef
	\incpc{\update{\mem}{\acc1\mapsto\nand{\mem.\acc1}{\mem.\acc2}}}
$$

\subsubsection{Equality}
$$
	\instr{\texttt{100001}}{\mem} \eqdef
	\incpc{\update{\mem}{\acc1\mapsto\xnor{\mem.\acc1}{\mem.\acc2}}}
$$

\subsubsection{Conditional jump}
$$
	\instr{\texttt{110000}}{\mem} \eqdef
	\begin{cases}
		\update{\mem}{\pc\mapsto\mem.\acc2} & \text{if $\mem.\acc1\neq0$}\\
		\incpc{\mem} & \text{otherwise}
	\end{cases}
$$

\subsubsection{Store register}
$$
	\instr{\texttt{111110}}{\mem} \eqdef
	\incpc{\update{\mem}{\mem.\acc2\mapsto\mem.\acc1}}
$$

\subsubsection{Load register}
$$
	\instr{\texttt{111111}}{\mem} \eqdef
	\incpc{\update{\mem}{\acc1\mapsto\mem.(\mem.\acc2)}}
$$

\subsubsection{Store literal}
\begin{align*}
	\instr{\texttt{00}k}{\mem} &\eqdef
	\incpc{\update{\mem}{\acc1\mapsto(\mem.\acc1 \land \texttt{0xf0})\lor k}} \\
	\instr{\texttt{01}k}{\mem} &\eqdef
	\incpc{\update{\mem}{\acc1\mapsto(\mem.\acc1 \land \texttt{0x0f})\lor (k \ll 4)}}
\end{align*}