697 specification glitches oob mxp exp gas ecdata (#702)

exp/general/binary.tex

@@ -9,3 +9,8 @@
 		\item[\vspace{\fill}]
 	\end{enumerate}
 \end{multicols}
+We further constrain the $\ppWcpFlag$, which belongs to the \isPreprocessing{}-perspective, to vanish outside of preprocessing rows:
+\begin{enumerate}[resume]
+        \item \If $\isPreprocessing_{i} = 0$ \Then $\ppWcpFlag_{i} = 0$
+	\item \If $\isPreprocessing_{i} = 1$ \Then $\ppWcpFlag_{i} \cdot (1 - \ppWcpFlag_{i}) = 0$
+\end{enumerate}

exp/general/heartbeat.tex

@@ -27,14 +27,14 @@
 \saNote{} The above enforces implicitly that the ``$\isMacro$'' phase may only last one row.
 \begin{enumerate}[resume]
 	\item \If \Big($\expStamp_{i} \neq 0$ \et $\ct_{i} = \maxCt_{i}$\Big) \Then we also impose that
-	      \[
-		      \left[ \begin{array}{lrcl}
-				      + & \isComputation_{i}   & \!\!\! \cdot \!\!\! & \isMacro          _{i + 1} \\
-				      + & \isMacro_{i}         & \!\!\! \cdot \!\!\! & \isPreprocessing  _{i + 1} \\
-				      + & \isPreprocessing_{i} & \!\!\! \cdot \!\!\! & \isComputation    _{i + 1} \\
-			      \end{array} \right]
-		      = 1.
-	      \]
+		\[
+			\left[ \begin{array}{lrcl}
+				+ & \isComputation_{i}   & \!\!\! \cdot \!\!\! & \isMacro          _{i + 1} \\
+				+ & \isMacro_{i}         & \!\!\! \cdot \!\!\! & \isPreprocessing  _{i + 1} \\
+				+ & \isPreprocessing_{i} & \!\!\! \cdot \!\!\! & \isComputation    _{i + 1} \\
+			\end{array} \right]
+			= 1.
+		\]
 	      to define the allowed perspective transitions.
 	\item we specify how the counter evolves:
 	      \begin{enumerate}

exp/lookups/wcp.tex

@@ -1,6 +1,6 @@
 The lookup to the $\wcpMod$ is constructed as follows:
 \begin{description}
-	\item[\underline{Selector:}] \ppWcpFlag{}
+	\item[\underline{Selector:}] $\ppWcpFlag$
 	\item[\underline{Source columns:}] from the \expMod{} module:
 	      \begin{multicols}{3}
 		      \begin{enumerate}

mxp/binary.tex

@@ -5,7 +5,7 @@
 		\item \noop{}
 		\item \mxpx{}
 		\item \codeDeployment{}
-		\item $\decMxpType{k}$, $k = 1,\dots,5$ (\trash)
+                \item $\decMxpType{k}$, $k = 1,\dots,5$ (\trash)
 		\item \comp{}
 		\item \mexpEvent{}
 		\item \mayTriggerNonTrivialOperation{}

mxp/roob.tex

@@ -17,7 +17,7 @@
 	\begin{array}{l}
 		\If \sizeHi{1}_{i} \neq 0 ~ \Then \roob_{i} = 1 \vspace{2mm} \\
 		\If \offsetHi{1}_{i} \cdot \sizeLo{1}_{i} \neq 0 ~ \Then \roob_{i} = 1 \vspace{2mm} \\
-%		\If \roob_{i} = 1 ~ \Then \Big(\isValHi{3}_{i} \neq 0 ~ \OR \isValHi{1}_{i} \cdot \isValLo{3}_{i} \neq 0\Big) \vspace{2mm} \\
+%	
 		\If
 		\left\{
 		\begin{array}{lr}
@@ -26,11 +26,6 @@
 		\end{array}
 		\right\}
 		\Then \roob_{i} = 0
-%		\If \roob_{i} = 0 ~ \Then 
-%		\begin{cases}
-%			\isValHi{3}_{i} = 0 & \et \\
-%			\isValHi{1}_{i} \cdot \isValLo{3}_{i} = 0 \\
-%		\end{cases} \\
 	\end{array}
 	\right.
 	\]
@@ -57,16 +52,6 @@
 				~ \Then \roob_{i} = 1 \vspace{2mm} \\
 		\If \offsetHi{2}_{i} \cdot \sizeLo{2}_{i} \neq 0
 				~ \Then \roob_{i} = 1 \vspace{2mm} \\
-%		\If \roob_{i} = 1 ~ \Then
-%		\left\{
-%		\begin{array}{lr}
-%			\sizeHi{1}_{i} \neq 0 & \OR \\
-%			\offsetHi{1}_{i} \cdot \isValLo{3}_{i} \neq 0 & \OR \\
-%			\sizeHi{2}_{i} \neq 0 & \OR \\
-%			\offsetHi{2}_{i} \cdot \isValLo{4}_{i} \neq 0 \\
-%		\end{array}
-%		\right.
-%		\vspace{2mm} \\
 		\If
 		\left\{
 		\begin{array}{lr}
@@ -96,6 +81,6 @@
 
 We provide some context.
 If $\decMxpType{1}_{i} = 1$ then the instruction is $\inst{MSIZE}$ which takes no size or offset arguments and can't provoke an out of bounds error. Thus $\roob_{i} = 0$ automatically.
-If $\decMxpType{2}_{i} = 1$ or $\decMxpType{3}_{i} = 1$ then the instruction is one of \inst{MLOAD}, \inst{MSTORE}, \inst{MSTORE8} and takes a single offset parameter. Offsets that are greater than 4 bytes may never occur because of gas related expenses, let alone offsets that occupy $>\llarge$ bytes (as witnessed by $\isValHi{1} \neq 0$.)
-If $\decMxpType{4}_{i} = 1$ the instruction takes \col{offset} and \col{size} arguments. For such an instruction to be ridiculously out of bounds either its size parameter has to be huge (as witnessed by $\sValHi{3}\neq0$) or its offset parameter has to be huge and its size parameter nonzero (as witnessed by $\sValHi{1}\neq0$ and $\sVal{3}\neq0$.)
+If $\decMxpType{2}_{i} = 1$ or $\decMxpType{3}_{i} = 1$ then the instruction is one of \inst{MLOAD}, \inst{MSTORE}, \inst{MSTORE8} and takes a single offset parameter. Offsets that are greater than 4 bytes may never occur because of gas related expenses, let alone offsets that occupy $>\llarge$ bytes (as witnessed by the relavant high part being nonzero).
+If $\decMxpType{4}_{i} = 1$ the instruction takes \col{offset} and \col{size} arguments. For such an instruction to be ridiculously out of bounds either its size parameter has to be huge (as witnessed by the relevant hight part of the size being nonzero) or its offset parameter has to be huge and its size parameter nonzero (as witnessed by the high part of the offset being nonzero and the size being nonzero).
 If $\decMxpType{5}_{i} = 1$ is entirely analoguous to the $\decMxpType{4}$ case except that two $(\col{offset}, \col{size})$ pairs are required.

oob/intro.tex

@@ -17,14 +17,14 @@
 			\end{cases}
 		\]
 		or not;
-		see section section~(\ref{oob: populating: rdc});
+		see section~(\ref{oob: populating: rdc});
 	\item[\underline{Trivial \inst{CALLDATALOAD} detection:}]
 		(for \inst{CALLDATACOPY} instructions) perform the comparison
 		\[
 			\col{offset} \geq \CDS
 		\]
 		(in which case \inst{CALLDATALOAD} must put $0$ on the stack);
-		see section section~(\ref{oob: populating: cdl});
+		see section~(\ref{oob: populating: cdl});
 	\item[\underline{Exceptional \inst{CALL}'s:}]
 		detect whether $\col{value} \neq 0$;
 	\item[\underline{\inst{CALL}-type abort detection:}]
@@ -35,10 +35,10 @@
 		see section~(\ref{oob: populating: create});
 	\item[\underline{\sstorexSH{} detection:}]
 		determine if $\col{gas} \leq G_\text{callstipend} = 2300$;
-		see section section~(\ref{oob: populating: sstore});
+		see section~(\ref{oob: populating: sstore});
 	\item[\underline{\maxcsxSH{} detection:}]
 		determine if a \inst{RETURN} in a deployment context returns code that is too big (i.e. $(\col{codesize} > 24576$);
-		see section section~(\ref{oob: populating: return});
+		see section~(\ref{oob: populating: return});
 \end{description}
 We furthermore use the \oobMod{} for the pricing of certain precompiles and the testing of certain conditions pertaining to some of the underlying \inst{CALL}'s parameters
 \CDS{} (recall its abbreviation \cds{}) and

oob/precompiles/blake2f/cds.tex

@@ -1,6 +1,10 @@
 \[
 	\boxed{\text{All constraints in this subsection further assume } \oobInstIsBlakeCds_{i} = 1}
 \]
+We remind the reader that the objective of the \oobMod{} module with the \oobInstBlakeCds{} instruction is to justify the \hubMod{}'s prediction as to whether
+\green{(\emph{a})} the provided call data has length $213$
+\green{(\emph{b})} the ``return capacity'' of the underlying \inst{CALL}-type instruction is zero or nonzero.
+
 We use the shorthands defined below:
 \[
 	\left\{ \begin{array}{lclr}

oob/precompiles/blake2f/params.tex

@@ -2,12 +2,14 @@
 \[
 	\boxed{\text{All constraints in this subsection further assume } \oobInstIsBlakeParams_{i} = 1 }
 \]
-We remind the reader that the objective of the \oobMod{} module in this particular case is to
+We remind the reader that the objective of the \oobMod{} module with the \oobInstBlakeParams{} instruction is to
 \green{(\emph{a})} compare the \locCalleeGas{} to the number of rounds \locBlakeR{}
 \green{(\emph{b})} verify that $\locBlakeF{} \in \{0, 1\}$
 \green{(\emph{c})} verify the \hubMod{}'s prediction as to the (non)vanishing of \locRac{}
 \green{(\emph{d})} justify the failure / success of the precompile
 \green{(\emph{e})} computed the \locRemainingGas{}.
+Recall furthermore that \locBlakeR{} and \locBlakeF{} were extracted from \textsc{ram} conditionally to
+\oobInstBlakeCds{} being successful.
 
 We thus introduce the following (local) shorthands:
 \[

oob/precompiles/common/tre.tex

@@ -50,6 +50,7 @@
 				\]
 				It follows that $\locCalleeGas < \locPrecompileCost \iff \locInsufficientGas = 1$.
 		\end{enumerate}
+	\saNote{} The shorthand \locPrecompileCost{} was defined using a division by 192. Whenever this shorthand is used in the constraints, we can replace the division by 192 with a multiplication by the same number through same basic algebra. This is the approach taken in the implementation to avoid division.
 	\item[\underline{Justifying the remaining \hubMod{} predictions:}]
 		we impose that
 		\[
@@ -63,4 +64,4 @@
 			\item \If $\locHubSuccess = 1$ \Then $\locReturnGas = \locCalleeGas - \locPrecompileCost$
 		\end{enumerate}
 \end{description}
-\saNote{} In other words $\locHubSuccess \equiv 1 \iff$ \Big($\cds \equiv 0 \mod 192$ \et{} $\locCalleeGas \geq \locPrecompileCost$\Big).
+\saNote{} In other words $\locHubSuccess \equiv 1 \iff$ \Big($\cds \equiv 0 \mod 192$ \et{} $\locCalleeGas \geq \locPrecompileCost$\Big).

oob/precompiles/modexp/xbs.tex

@@ -22,7 +22,7 @@
 If \locComputeMax{} is set we compute the maximum of \locYbsLo{} and \locXbs{}.
 The use case for this comparison is to compute the maxium $\max\{ \locBbs, \locMbs \}$ as required by the pricing of the \inst{MODEXP} precompile.
 \begin{description}
-	\item[\underline{Rows n°$(i)$ and $n^\circ(i + 1)$:}] we impose
+	\item[\underline{Rows n°$(i)$, $n^\circ(i + 1)$ and $n^\circ(i + 2)$:}] we impose
 		\[
 			\left\{ \begin{array}{l}
 				\oobCallToLt
@@ -43,8 +43,8 @@
 		we further impose the following constraints
 		\[
 			\left\{ \begin{array}{lclr}
-				\locComputeMax \cdot (1 - \locComputeMax) & = & 0 & \qquad (\trash) \\
-				\locCompToFiveTwelve                      & = & 1                   \\
+				\locComputeMax \cdot (1 - \locComputeMax) & = & 0      \\
+				\locCompToFiveTwelve                      & = & 1      \\
 			\end{array} \right.
 		\]
 		where we further define the shorthands
@@ -54,6 +54,8 @@
 				\locCmp              & \define & \outgoingResLo    _{i + 1} \\
 			\end{array} \right.
 		\]
+		\saNote{} The value \locComputeMax{}, along with the other inputs, is provided to the \hubMod{} module and will be binary in all applications.
+
 		\saNote{} The constraint $\outgoingResLo_{i} = 1$ enforces that the comparison ``$\locXbs < 512 + 1$'' i.e. ``$\locXbs \leq 512$'' return \texttt{true}.
 	\item[\underline{Justifying \hubMod{} predictions:}] we impose
 		we further impose that

prc/ecdata/constancies.tex

@@ -29,6 +29,7 @@
         \item \ecdataSuccessBit{}
         \item \totalPairings{}
         \item \internalChecksPassed{}
+        \item \locAddressSum{}
         \item[\vspace{\fill}]
     \end{enumerate}
 \end{multicols}

prc/ecdata/decoding.tex

@@ -96,13 +96,13 @@
                                        \end{array} \right]}                                                                                                   \\
         \end{array} \right.
 \]
-\saNote{} This quantity is indeed a bit.
+\saNote{} The quantity $\locTransitionBit$ is indeed a bit.
 
-and impose that
+\noindent We further impose that
 \begin{enumerate}
 	\item $\If \ecDataStamp_{i} =    0$ \Then $\locFlagSum_{i} = 0$
 	\item $\If \ecDataStamp_{i} \neq 0$ \Then $\locFlagSum_{i} = 1$
-	\item we further impose
+	\item furthermore
 		\[
 			\ecdataPhase_{i}
 			=

prc/ecdata/utils/ext.tex

@@ -44,7 +44,7 @@
         \qquad \qquad \iff
         \left\{ \begin{array}{lcl}
                     \extFlag       _{i+\relof} & = & 1             \\
-                    \extInst       _{i+\relof} & = & \inst{ADDMUL} \\
+                    \extInst       _{i+\relof} & = & \inst{MULMOD} \\
                     \extArgOneHi   _{i+\relof} & = & \col{a}       \\
                     \extArgOneLo   _{i+\relof} & = & \col{b}       \\
                     \extArgTwoHi   _{i+\relof} & = & \col{c}       \\