Fix stack output for SLOAD

hub/instruction_handling/storage/constraints.tex

@@ -20,6 +20,7 @@
 		\inst{SSLOAD} may only raise stack exceptions or \oogxSH{}
 		while \inst{SSTORE} may raise stack exceptions, \staticxSH{}, \sstorexSH{} or \oogxSH{}.
 	\item[\underline{Setting $\nonStackRows$ and peeking flags:}]
+		\label{hub: instruction handling: storage: non stack rows and peeking flags}
 		storage operations can provoke exceptions in multiple ways and are rollback sensitive;
 		they thus have some inherent complexity;
 		we impose the following:
@@ -75,7 +76,7 @@
 
 		\saNote{} Recall that (among instructions raising the $\stackDecStoFlag$ flag) only \inst{SSTORE} may raise a \staticxSH{}.
 	\item[\underline{Setting the miscellaneous-row:}]
-		\If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then 
+		\If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then
 		\begin{enumerate}
 			\item we impose that \inst{SSTORE} instructions trigger the \oobMod{}
 				\[
@@ -103,7 +104,7 @@
 		\end{enumerate}
 	\item[\underline{Justifying the \stackSstorex{} flag:}]
 		\begin{enumerate}
-		\If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then 
+		\If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then
 			\item \If $\locIsSstore = 1$ \Then we impose that $\stackSstorex_{i} = \miscOobDataCol{7}_{i + \locMiscRowOffset}$
 		\end{enumerate}
 \end{description}
@@ -145,27 +146,38 @@
 			\end{array} \right.
 		\]
 	\item[\underline{Defining storage value operations:}]
-		\If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then
+		we impose that
 		\begin{description}
 			\item[\underline{The \inst{SLOAD} case:}]
 				\If $\locIsSload = 1$ \Then
-				\[
-					\left\{ \begin{array}{lcl}
-						\multicolumn{3}{l}{\storageReading{i}{\locFirstStoRowOffset}} \\
-						\locLoadedValueHi & \!\!\! = \!\!\! & \stoCurrValueHi_{i + \locFirstStoRowOffset} \\
-						\locLoadedValueLo & \!\!\! = \!\!\! & \stoCurrValueLo_{i + \locFirstStoRowOffset} \\
-					\end{array} \right.
-				\]
+				\begin{enumerate}
+				        \item \If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then $\storageReading{i}{\locFirstStoRowOffset}$
+				        \item \If $(1 - \xAhoy_{i}) = 1$ \Then
+						\[
+							\left\{ \begin{array}{lcl}
+								\locLoadedValueHi & \!\!\! = \!\!\! & \stoCurrValueHi_{i + \locFirstStoRowOffset} \\
+								\locLoadedValueLo & \!\!\! = \!\!\! & \stoCurrValueLo_{i + \locFirstStoRowOffset} \\
+							\end{array} \right.
+						\]
+				\end{enumerate}
+				\saNote{}
+				In other words: \inst{SLOAD} instructions that lead to the production of \textbf{storage-rows}, as witnessed by
+				$\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$, see (\ref{hub: instruction handling: storage: non stack rows and peeking flags}),
+				(\emph{a}) don't modify the value in storage and
+				(\emph{b}) if unexceptional, as witnessed by $(1 - \xAhoy_{i}) = 1$, write the value in storage to the stack.
 			\item[\underline{The \inst{SSTORE} case:}]
 				\If $\locIsSstore = 1$ \Then
-				\[
-					\left\{ \begin{array}{lcl}
-						\stoNextValueHi _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreHi \\
-						\stoNextValueLo _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreLo \\
-					\end{array} \right.
-				\]
+				\begin{enumerate}
+					\item \If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then
+						\[
+							\left\{ \begin{array}{lcl}
+								\stoNextValueHi _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreHi \\
+								\stoNextValueLo _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreLo \\
+							\end{array} \right.
+						\]
+				\end{enumerate}
 			\item[\underline{The inverse, undoing operation:}]
-				\If $\cnWillRev_{i} = 1$ \Then 
+				\If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \et $\cnWillRev_{i} = 1$ \Then
 				\[
 					\left\{ \begin{array}{lcl}
 						\stoSameStorageSlot          {i}{\locSecondStoRowOffset}{\locFirstStoRowOffset} \\
@@ -201,7 +213,7 @@
 		\locNextNotCurr & \!\!\! \define \!\!\! & 1 - \locNextIsCurr \\
 	\end{array} \right.
 \]
-\begin{description} 
+\begin{description}
 	\item[\underline{Setting the gas cost:}]
 		\If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then
 		\begin{description}
@@ -277,7 +289,7 @@
 					\end{array} \right]
 					\cdot
 					\locOrigNotZero
-					\cdot 
+					\cdot
 					\left[ \begin{array}{cr}
 						- & \locCurrIsZero \\
 						+ & \locNextIsZero \\
@@ -300,7 +312,7 @@
 					\end{array} \right]
 					\cdot
 					\locNextIsOrig
-					\cdot 
+					\cdot
 					\left[ \begin{array}{crcl}
 						+ & \locOrigIsZero  & \cdot & \big(G_\text{sset}   - G_\text{warmaccess}\big) \\
 						+ & \locOrigNotZero & \cdot & \big(G_\text{sreset} - G_\text{warmaccess}\big) \\