\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}{\prog,\mem})$$

Here, $\instrop$ is a function that maps words to instructions: $\instrop :
\Word4 \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}[h]
	\centering
	{\tt
	\begin{tabular}{!>{\normalfont}l | ^l | *{4}{|^c}}
		\rowstyle{\normalfont\bfseries}
		Instruction name & Assembly & 3 & 2 & 1 & 0 \\\hline
		Addition         & add      & 0 & 0 & 0 & 0 \\\hline
		Subtraction      & sub      & 0 & 0 & 0 & 1 \\\hline
		Rotate left      & rol      & 0 & 0 & 1 & 0 \\\hline
		Shift left       & shl      & 0 & 0 & 1 & 1 \\\hline
		Logical AND      & and      & 0 & 1 & 0 & 0 \\\hline
		Logical OR       & or       & 0 & 1 & 0 & 1 \\\hline
		Logical XOR      & xor      & 0 & 1 & 1 & 0 \\\hline
		Logical NOT      & not      & 0 & 1 & 1 & 1 \\\hline
		Store register   & str      & 1 & 1 & 0 & 0 \\\hline
		Load register    & ld       & 1 & 1 & 0 & 1 \\\hline
		Conditional jump & cjmp     & 1 & 1 & 1 & 0 \\\hline
		Load literal     & lit      & 1 & 1 & 1 & 1
	\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{k}{\mem} = \update{\mem}{\pc\mapsto\mem.\pc+k}$$

\subsubsection{Arithmetical}
\begin{align*}
	\instr{\texttt{0000}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1+\mem.\acc2}} \\
	\instr{\texttt{0001}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1-\mem.\acc2}}
\end{align*}

\subsubsection{Rotating and Shifting}
\begin{align*}
	\instr{\texttt{0010}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\rol(\mem.\acc1)}} \\
	\instr{\texttt{0011}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\shl(\mem.\acc1)}}
\end{align*}

\subsubsection{Logical operations}
\begin{align*}
	\instr{\texttt{0100}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1 \land \mem.\acc2}} \\
	\instr{\texttt{0101}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1 \lor \mem.\acc2}} \\
	\instr{\texttt{0110}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\mem.\acc1 \oplus \mem.\acc2}} \\
	\instr{\texttt{0111}}{\prog,\mem} &\eqdef
		\incpc1{\update{\mem}{\acc1\mapsto\lnot(\mem.\acc1)}}
\end{align*}

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

\subsubsection{Store register}
$$
	\instr{\texttt{1100}}{\prog,\mem} \eqdef
	\incpc1{\update{\mem}{\mem.\acc2\mapsto\mem.\acc1}}
$$

\subsubsection{Load register}
$$
	\instr{\texttt{1101}}{\prog,\mem} \eqdef
	\incpc1{\update{\mem}{\acc1\mapsto\mem.(\mem.\acc2)}}
$$

\subsubsection{Load literal}
\begin{align*}
	\instr{\texttt{1111}}{\prog,\mem} &\eqdef
	\incpc3{\update{\mem}{\acc1\mapsto(\prog.(\mem.\pc+1)\ll4)\lor(\prog.(\mem.\pc+2))}} \\
\end{align*}