EIP-3855: PUSH0 instruction

hub/instruction_handling/push_pop/_local.tex

@@ -1,4 +1,5 @@
 \def\locIsPush       {\col{is\_push}}
 \def\locIsPop        {\col{is\_pop}}
+\def\locIsPushZero   {\col{is\_push\_zero}}
 \def\locResultHi     {\col{result\_hi}}
 \def\locResultLo     {\col{result\_lo}}

hub/instruction_handling/push_pop/constraints.tex

@@ -11,28 +11,60 @@
 \begin{description}
 	\item[\underline{Setting the stack pattern:}] we impose
 	\begin{enumerate}
-		\item \If $\locIsPop  = 1$ \Then $\oneZeroSP_{i}$
-		\item \If $\locIsPush = 1$ \Then $\zeroOneSP_{i}$
+		\item \If $\locIsPop      = 1$ \Then $\oneZeroSP_{i}$
+		\item \If $\locIsPush     = 1$ \Then $\zeroOneSP_{i}$
+		\item \If $\locIsPushZero = 1$ \Then $\zeroOneSP_{i}$
 	\end{enumerate}
-	\item[\underline{Setting $\nonStackRows$:}] we impose $\nonStackRows_{i} = \cmc_{i}$;
-	\item[\underline{Setting the peeking flags:}] we don't need to set any;
+		\saNote{}
+		The $\locIsPush$ and $\locIsPushZero$ cases
+		can be merged into one by replacing the condition with
+		``\If $\locIsPush + \locIsPushZero = 1$ \Then \dots''.
+	\item[\underline{Setting $\nonStackRows$:}]
+		we impose $\nonStackRows_{i} = \cmc_{i}$;
+	\item[\underline{Setting the peeking flags:}]
+		we don't need to set any;
 
-	\saNote{} Implicitly of course $\cmc_{i} \cdot \peekContext_{i + 1} = \cmc_{i}$ (\trash);
-	\item[\underline{Setting the gas cost:}] we impose that $\gasCost_{i} = \decStaticGas_{i}$;
+		\saNote{}
+		Implicitly of course $\cmc_{i} \cdot \peekContext_{i + 1} = \cmc_{i}$ (\trash);
+	\item[\underline{Setting the gas cost:}]
+		we impose that $\gasCost_{i} = \decStaticGas_{i}$;
 	\item[\underline{Value constraints:}]
-		 \If $\locIsPush = 1$ \Then
-		\[
-			\begin{cases}
-				\locResultHi = \stackPushParamHi_{i} \\
-				\locResultLo = \stackPushParamLo_{i} \\
-			\end{cases}
-		\]
+		we impose the following:
+		\begin{description}
+			\item[\underline{The ``\inst{PUSHX}, $\inst{X} > 0$'' case:}] 
+				\label{hub: instruction handling: push pop: setting result to push value for PUSHX}
+				\If $\locIsPush = 1$ \Then
+				\[
+					\begin{cases}
+						\locResultHi = \stackPushParamHi_{i} \\
+						\locResultLo = \stackPushParamLo_{i} \\
+					\end{cases}
+				\]
+			\item[\underline{The ``\inst{PUSH0}'' case:}] 
+				\label{hub: instruction handling: push pop: setting result to zero for PUSH0}
+				\If $\locIsPushZero = 1$ \Then
+				\[
+					\begin{cases}
+						\locResultHi = 0 \\
+						\locResultLo = 0 \\
+					\end{cases}
+				\]
+		\end{description}
 	\item[\underline{Setting $\pc\new$:}]
 		we impose that
 		\begin{enumerate}
-			\item \If $\locIsPop  = 1$ \Then $\pc\new_{i} = 1 + \pc_{i}$
-			\item \If $\locIsPush = 1$ \Then $\pc\new_{i} = 1 + \pc_{i} + (\stackInst_{i} - \inst{PUSH1} + 1)$
+			\item \If $\locIsPop      = 1$ \Then $\pc\new_{i} = 1 + \pc_{i}$
+			\item \If $\locIsPush     = 1$ \Then $\pc\new_{i} = 1 + \pc_{i} + (\stackInst_{i} - \inst{PUSH1} + 1)$
+			\item \If $\locIsPushZero = 1$ \Then $\pc\new_{i} = 1 + \pc_{i}$
 		\end{enumerate}
+		\saNote{}
+		The $\locIsPush$ and $\locIsPushZero$ cases
+		can, again, be combined.
+		Indeed, given that
+		$\inst{PUSH0} \equiv \texttt{0x\,5f}$ and
+		$\inst{PUSH1} \equiv \texttt{0x\,60}$,
+		the ``\inst{PUSH0} case'' has
+		$\stackInst - \inst{PUSH1} + 1 \equiv \inst{PUSH0} - \inst{PUSH1} + 1 \equiv 0$.
 \end{description}
 \saNote{}
 We only require setting values in the case of \inst{PUSH}-type instructions.

hub/instruction_handling/push_pop/instructions_and_flags.tex

@@ -1,8 +1,13 @@
 \[
-	\begin{array}{|l||c||c|c|c|}
+	\begin{array}{|l||c||c|c|c|c|}
 		\hline
-		\INST           & \tli  & \stackDecPushPopFlag & \decFlag{1} & \decFlag{2} \\ \hline\hline
-		\inst{POP}      & \zero & \oneCell             & \oneCell    & \zero       \\ \hline
-		\inst{PUSH1-32} & \zero & \oneCell             & \zero       & \oneCell    \\ \hline
+		\INST           & \tli  & \stackDecPushPopFlag & \decFlag{1} & \decFlag{2} & \decFlag{3} \\ \hline\hline
+		\inst{POP}      & \zero & \oneCell             & \oneCell    & \zero       & \zero       \\ \hline
+		\inst{PUSH1-32} & \zero & \oneCell             & \zero       & \oneCell    & \zero       \\ \hline
+		\inst{PUSH0}    & \zero & \oneCell             & \zero       & \zero       & \oneCell    \\ \hline
 	\end{array}
 \]
+\saNote{}
+We separate the \inst{PUSH0} from the other \inst{PUSHX}, $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$, instructions.
+This stems from the fact that they are treated differently in the \romMod{} module:
+the \romMod{} module does not construct a ``push value'' for the \inst{PUSH0} instruction, and \inst{PUSH0} does not raise the \pushFlag{}.

hub/instruction_handling/push_pop/shorthands.tex

@@ -1,8 +1,9 @@
 We define some shorthands
 \[
 	\left\{ \begin{array}{lcl}
-		\locIsPop  & \define & \decFlag  {1} _{i} \\
-		\locIsPush & \define & \decFlag  {2} _{i} \\
+		\locIsPop      & \define & \decFlag  {1} _{i} \\
+		\locIsPush     & \define & \decFlag  {2} _{i} \\
+		\locIsPushZero & \define & \decFlag  {3} _{i} \\
 	\end{array} \right.
 	\quad
 	\left\{ \begin{array}{lcl}

rom_v3/_inputs.tex

@@ -1,6 +1,7 @@
 \input{_local}
 \section{The \romMod{} module}                                   \label{rom}
 \subsection{Introduction}                                        \label{rom: intro}                        \input{intro}
+\subsection{Convention}                                          \label{rom: convention}                   \input{convention}
 \subsection{Column description}                                  \label{rom: columns}                      \input{columns}
 \subsection{Generalities}                                        \label{rom: constraints}                  \input{generalities/_inputs}
 \subsection{Connecting \pbcb{} to \opc{} and related flags}      \label{rom: opcode related constraints}   \input{opcode/_inputs}

rom_v3/columns.tex

@@ -73,7 +73,9 @@
 	depends on the the context i.e. on whether the byte is shadowed by a \inst{PUSH} instruction (i.e. \( \ipd{}=1 \)) and whether the \CSR{} flag is on (at which point we impose $\pbcb=\opc=\texttt{0x00}$);
 	in all other circumstances \( \opc{} = \PBCB{} \);
     \item \IP{}:
-	lights up precisely when $\opc \equiv \inst{PUSHX}$ for some $\inst{X} \in \{ 1, 2, \dots, \evmWordSize \}$;
+	lights up precisely when
+	$\opc \equiv \inst{PUSHX}$\footnote{Recall our convention~(\ref{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0})}
+	for some $\inst{X}$;
 	abbreviated to \ip{};
     \item \IPD{}:
 	binary flag;
@@ -89,3 +91,20 @@
 The \opc{} and \pbcb{} columns differ in that bytes that are ``obscured'' by a previous \inst{PUSHX} opcode
 will appear unaltered in the \pbcb{} column, but altered to \inst{INVALID} in the \opc{} column, see section~(\ref{rom: opcode: opcode from padded byte code byte}).
 As such the above precisely recognizes valid jump destinations as specified in the \cite{EYP}.
+
+\saNote{}
+\label{rom: columns: IS_PUSH_FLAG does not light up for PUSH0}
+We draw attention to the fact that the \romMod{} module
+doesn't deal with the \inst{PUSH0} instruction of \cite{EIP-3855} as it does with
+\inst{PUSHX} instructions\footnote{Recall our convention~(\ref{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0})}.
+For one, it doesn't construct a ``push value'' for \inst{PUSH0} instructions.
+As a consequence, the \inst{PUSH0} opcode \textbf{does not raise} the \IP{} flag while the other \inst{PUSHX} instructions do,
+see diagram~(\ref{rom: instruction decoding: relevant portion of ID module}).
+
+\saNote{}
+\label{rom: columns: push values for PUSH0 vs PUSHX in the HUB}
+Given that the ``push value'' of a \inst{PUSH0} instruction is zero by definition,
+the \hubMod{} module knows to push \inst{0x\,00} to the stack for that opcode,
+see section~(\ref{hub: instruction handling: push pop: setting result to zero for PUSH0}).
+For \inst{PUSHX} instructions the \hubMod{} module is reliant on the $\PV$ constructed in the present module,
+see section~(\ref{hub: instruction handling: push pop: setting result to push value for PUSHX}).

rom_v3/convention.tex

@@ -0,0 +1,5 @@
+\label{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0}
+Throughout the specification of the \romMod{} module, whenever we write
+``\inst{PUSHX}'' we will \textbf{always} be talking about the case where $\inst{X} \neq \inst{0}$, i.e. with $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$.
+The \inst{PUSH0} instruction of \cite{EIP-3855} is dealt with differently than the other \inst{PUSHX} instructions,
+see section~(\ref{rom: columns: IS_PUSH_FLAG does not light up for PUSH0}) for more details.

rom_v3/intro.tex

@@ -1,15 +1,16 @@
-The \romMod{} module compiles the \emph{nonempty} bytecodes, initialization codes and deployed byte codes alike, used during the execution of a conflation of blocks.
+The \romMod{} module compiles the \textbf{nonempty} bytecodes, initialization codes and deployed byte codes alike, used during the execution of a conflation of blocks.
 Its main role in the overall design is to provide the \hubMod{} module with the correct sequence of instructions.
-It furthermore assembles the \inst{PUSH}-values from the bytes following a \inst{PUSHX} instruction.
-It also tags (in)valid jump destinations as such as required by \textsc{jump destination analysis}.
-Most of the arithmetization below focuses on building the \romMod{} module  as a seqence of padded byte codes and of extracting the correct push values from it (i.e. the $\inst{X}$-byte long arguments of actual \inst{PUSHX} instructions).
+It furthermore assembles the \inst{PUSH}-values from the bytes following a \inst{PUSHX} instruction, $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$.
+It also tags (in)valid jump destinations as such, as is required by \textsc{jump destination analysis}.
+Most of the arithmetization below focuses on building the \romMod{} module as a seqence of padded byte codes and of extracting the correct push values from it (i.e. the $\inst{X}$-byte long arguments of actual \inst{PUSHX} instructions).
 
 There are three kinds of accesses to bytecode that the \romMod{} module  deals with, with contract deployment being subdivided into 1 or 2 phases (since deployments may fail):
 \begin{enumerate}
-    \item loading the full bytecode of an already deployed smart contract to \inst{CALL} it or to \inst{EXTCODECOPY} from it (or both);
+    \item loading the full bytecode of an already deployed smart contract to \inst{CALL}, \inst{CALLCODE}, \inst{STATICCALL} or \inst{DELEGATECALL} into it;
+    \item loading the full bytecode of an already deployed smart contract to \inst{EXTCODECOPY} from it;
     \item deploying a smart contract through a deployment transaction or an (unexceptional, unaborted and no failure condition raising) \inst{CREATE(2)} instruction:
         \begin{enumerate}
-            \item loading the initialization code into \romMod{};
-            \item and for (temporarily) successful deployments loading the bytecode that will be deployed at the relevant address into \romMod{}.
+            \item loading the initialization code into the \romMod{} module;
+            \item and for (temporarily) successful deployments loading the bytecode that will be (temporarily) deployed at the relevant address into the \romMod{} module.
         \end{enumerate}
 \end{enumerate}

rom_v3/lookups/rom_into_instruction_decoder.tex

@@ -31,15 +31,16 @@
 	\[
 		\renewcommand{\arraystretch}{1.3}
 		\begin{array}{|l|c|c|} \hline
-			\opc                      & \idMod/\IP & \idMod/\IJD \\ \hline \hline
-			\inst{PUSHX}              & \rOne      & \gZero      \\ \hline
-			\inst{JUMPDEST}           & \gZero     & \rOne       \\ \hline
-			\texttt{<any other byte>} & \gZero     & \gZero      \\ \hline
+			\opc                      & \idMod\separator\IP & \idMod\separator\IJD \\ \hline \hline
+			\inst{PUSH0}              & \gZero              & \gZero                \\ \hline
+			\inst{PUSHX}              & \rOne               & \gZero                \\ \hline
+			\inst{JUMPDEST}           & \gZero              & \rOne                 \\ \hline
+			\texttt{<any other byte>} & \gZero              & \gZero                \\ \hline
 		\end{array}
 	\]
 	\caption{%
 		Relevant portion of the \idMod{} module.
-		In the above $\inst{X} \in \{ 1, 2, \dots, \evmWordSize \}$}
+		In the above $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$}
 		\label{rom: instruction decoding: relevant portion of ID module}
 \end{figure}