fix: TXN instrutions write the result to the stack only if unexceptio…

…nal (#26)

hub/instruction_handling/_inputs.tex

@@ -16,7 +16,7 @@ \subsection{Instructions raising the $\stackDecKecFlag$           \lispDone{}}
 \subsection{Instructions raising the $\stackDecConFlag$           \lispDone{}}   \label{hub: instruction handling: con}                    \input{instruction_handling/context/_inputs}
 \subsection{Instructions raising the $\stackDecAccFlag$           \lispDone{}}   \label{hub: instruction handling: acc}                    \input{instruction_handling/account/_inputs}
 \subsection{Instructions raising the $\stackDecCopyFlag$          \lispDone{}}   \label{hub: instruction handling: copy}                   \input{instruction_handling/copy/_inputs}
-\subsection{Instructions raising the $\stackDecTxnFlag$           \lispDone{}}   \label{hub: instruction handling: txn}                    \input{instruction_handling/txn}
+\subsection{Instructions raising the $\stackDecTxnFlag$           \lispDone{}}   \label{hub: instruction handling: txn}                    \input{instruction_handling/txn/_inputs}
 \subsection{Instructions raising the $\stackDecBtcFlag$           \lispDone{}}   \label{hub: instruction handling: btc}                    \input{instruction_handling/btc}
 \subsection{Instructions raising the $\stackDecStackRamFlag$      \lispDone{}}   \label{hub: instruction handling: stackRam}               \input{instruction_handling/stack_ram/_inputs}
 \subsection{Instructions raising the $\stackDecStoFlag$           \lispDone{}}   \label{hub: instruction handling: sto}                    \input{instruction_handling/storage/_inputs}

hub/instruction_handling/txn/_inputs.tex

@@ -0,0 +1,5 @@
+\input{instruction_handling/txn/_local}
+\subsubsection{Supported instructions and flags}    \label{hub: instruction handling: txn: instructions}     \input{instruction_handling/txn/instructions}
+\subsubsection{Shorthands           \lispDone{}}    \label{hub: instruction handling: txn: shorthands}       \input{instruction_handling/txn/shorthands}
+\subsubsection{Constraints          \lispDone{}}    \label{hub: instruction handling: txn: constraints}      \input{instruction_handling/txn/constraints}
+

hub/instruction_handling/txn/_local.tex

@@ -0,0 +1,4 @@
+\def\locTxnRow                    {\yellowm{1}}
+\def\locConRow                    {\orangem{2}}
+\def\locIsOrigin                  {\col{is\_ORIGIN}}
+\def\locIsGasPrice                {\col{is\_GASPRICE}}

hub/instruction_handling/txn/constraints.tex

@@ -0,0 +1,44 @@
+\begin{center}
+	\boxed{%
+		\text{The stack constraints presented below assume }
+		\begin{cases}
+			\peekStack       _{i} = 1           \\
+			\stackDecTxnFlag _{i} = 1           \\
+			\stackSux _{i} + \stackSox _{i} = 0 \\
+		\end{cases}}
+\end{center}
+We impose the following constraints:
+\begin{description}
+	\item[\underline{Setting the stack pattern:}] we impose $\zeroOneSP_{i}$;
+	\item[\underline{Setting $\nonStackRows$:}] we impose $\nonStackRows_{i} = 1 + \cmc_{i}$;
+	\item[\underline{Setting the peeking flags:}] we impose
+		\[
+			\left[ \begin{array}{lrcl}
+				+ & \peekTransaction _{i + \locTxnRow} \\
+				+ & \peekContext     _{i + \locConRow}  & \!\!\!\cdot\!\!\! & \cmc_{i} \\
+			\end{array} \right]
+			=
+			\nonStackRows_{i}
+		\]
+	\item[\underline{Setting the gas cost:}] we impose that $\gasCost_{i} = \decStaticGas_{i}$;
+	\item[\underline{Value constraints:}]
+		\If $\xAhoy _{i} = 0$ \Then we impose that
+		\begin{enumerate}
+			\item \If $\locIsOrigin = 1$ \Then
+				\[
+					\left\{ \begin{array}{lcl}
+						\stackItemValHi{4}_{i} & \!\!\! = \!\!\! & \txFrom\high_{i + \locTxnRow} \\
+						\stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txFrom\low_{i + \locTxnRow} \\
+					\end{array} \right.
+				\]
+			\item \If $\locIsGasPrice = 1$ \Then
+				\[
+					\left\{ \begin{array}{lcl}
+						\stackItemValHi{4}_{i} & \!\!\! = \!\!\! & 0 \\
+						\stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txGasPrice_{i + \locTxnRow} \\
+					\end{array} \right.
+				\]
+		\end{enumerate}
+\end{description}
+\saNote{}
+For instructions raising the $\stackDecTxnFlag$ one has $\cmc = \xAhoy$.

hub/instruction_handling/txn/instructions.tex

@@ -0,0 +1,9 @@
+\[
+	\begin{array}{|l||c||c|c|c|}
+		\hline
+		\INST           & \tli  & \stackDecTxnFlag & \decFlag{1} & \decFlag{2} \\ \hline\hline
+		\inst{ORIGIN}   & \zero & \oneCell         & \oneCell    & \zero       \\ \hline
+		\inst{GASPRICE} & \zero & \oneCell         & \zero       & \oneCell    \\ \hline
+	\end{array}
+\]
+

hub/instruction_handling/txn/shorthands.tex

@@ -0,0 +1,7 @@
+We further introduce the following shorthands
+\[
+	\left\{ \begin{array}{lcl}
+		\locIsOrigin   & \define & \decFlag {1} _{i} \\
+		\locIsGasPrice & \define & \decFlag {2} _{i} \\
+	\end{array} \right.
+\]