Skip to content

Commit abe3d55

Browse files
OlivierBBBOlivierBBB
authored
EIP-3855: PUSH0 instruction (#145)
1 parent 624e3b3 commit abe3d55

File tree

9 files changed

+100
-34
lines changed

9 files changed

+100
-34
lines changed

‎hub/instruction_handling/push_pop/_local.tex

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\def\locIsPush {\col{is\_push}}
22
\def\locIsPop {\col{is\_pop}}
3+
\def\locIsPushZero {\col{is\_push\_zero}}
34
\def\locResultHi {\col{result\_hi}}
45
\def\locResultLo {\col{result\_lo}}

‎hub/instruction_handling/push_pop/constraints.tex

Lines changed: 47 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -11,28 +11,60 @@
1111
\begin{description}
1212
\item[\underline{Setting the stack pattern:}] we impose
1313
\begin{enumerate}
14-
\item \If $\locIsPop = 1$ \Then $\oneZeroSP_{i}$
15-
\item \If $\locIsPush = 1$ \Then $\zeroOneSP_{i}$
14+
\item \If $\locIsPop = 1$ \Then $\oneZeroSP_{i}$
15+
\item \If $\locIsPush = 1$ \Then $\zeroOneSP_{i}$
16+
\item \If $\locIsPushZero = 1$ \Then $\zeroOneSP_{i}$
1617
\end{enumerate}
17-
\item[\underline{Setting $\nonStackRows$:}] we impose $\nonStackRows_{i} = \cmc_{i}$;
18-
\item[\underline{Setting the peeking flags:}] we don't need to set any;
18+
\saNote{}
19+
The $\locIsPush$ and $\locIsPushZero$ cases
20+
can be merged into one by replacing the condition with
21+
``\If $\locIsPush + \locIsPushZero = 1$ \Then \dots''.
22+
\item[\underline{Setting $\nonStackRows$:}]
23+
we impose $\nonStackRows_{i} = \cmc_{i}$;
24+
\item[\underline{Setting the peeking flags:}]
25+
we don't need to set any;
1926

20-
\saNote{} Implicitly of course $\cmc_{i} \cdot \peekContext_{i + 1} = \cmc_{i}$ (\trash);
21-
\item[\underline{Setting the gas cost:}] we impose that $\gasCost_{i} = \decStaticGas_{i}$;
27+
\saNote{}
28+
Implicitly of course $\cmc_{i} \cdot \peekContext_{i + 1} = \cmc_{i}$ (\trash);
29+
\item[\underline{Setting the gas cost:}]
30+
we impose that $\gasCost_{i} = \decStaticGas_{i}$;
2231
\item[\underline{Value constraints:}]
23-
\If $\locIsPush = 1$ \Then
24-
\[
25-
\begin{cases}
26-
\locResultHi = \stackPushParamHi_{i} \\
27-
\locResultLo = \stackPushParamLo_{i} \\
28-
\end{cases}
29-
\]
32+
we impose the following:
33+
\begin{description}
34+
\item[\underline{The ``\inst{PUSHX}, $\inst{X} > 0$'' case:}]
35+
\label{hub: instruction handling: push pop: setting result to push value for PUSHX}
36+
\If $\locIsPush = 1$ \Then
37+
\[
38+
\begin{cases}
39+
\locResultHi = \stackPushParamHi_{i} \\
40+
\locResultLo = \stackPushParamLo_{i} \\
41+
\end{cases}
42+
\]
43+
\item[\underline{The ``\inst{PUSH0}'' case:}]
44+
\label{hub: instruction handling: push pop: setting result to zero for PUSH0}
45+
\If $\locIsPushZero = 1$ \Then
46+
\[
47+
\begin{cases}
48+
\locResultHi = 0 \\
49+
\locResultLo = 0 \\
50+
\end{cases}
51+
\]
52+
\end{description}
3053
\item[\underline{Setting $\pc\new$:}]
3154
we impose that
3255
\begin{enumerate}
33-
\item \If $\locIsPop = 1$ \Then $\pc\new_{i} = 1 + \pc_{i}$
34-
\item \If $\locIsPush = 1$ \Then $\pc\new_{i} = 1 + \pc_{i} + (\stackInst_{i} - \inst{PUSH1} + 1)$
56+
\item \If $\locIsPop = 1$ \Then $\pc\new_{i} = 1 + \pc_{i}$
57+
\item \If $\locIsPush = 1$ \Then $\pc\new_{i} = 1 + \pc_{i} + (\stackInst_{i} - \inst{PUSH1} + 1)$
58+
\item \If $\locIsPushZero = 1$ \Then $\pc\new_{i} = 1 + \pc_{i}$
3559
\end{enumerate}
60+
\saNote{}
61+
The $\locIsPush$ and $\locIsPushZero$ cases
62+
can, again, be combined.
63+
Indeed, given that
64+
$\inst{PUSH0} \equiv \texttt{0x\,5f}$ and
65+
$\inst{PUSH1} \equiv \texttt{0x\,60}$,
66+
the ``\inst{PUSH0} case'' has
67+
$\stackInst - \inst{PUSH1} + 1 \equiv \inst{PUSH0} - \inst{PUSH1} + 1 \equiv 0$.
3668
\end{description}
3769
\saNote{}
3870
We only require setting values in the case of \inst{PUSH}-type instructions.

‎hub/instruction_handling/push_pop/instructions_and_flags.tex

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
11
\[
2-
\begin{array}{|l||c||c|c|c|}
2+
\begin{array}{|l||c||c|c|c|c|}
33
\hline
4-
\INST & \tli & \stackDecPushPopFlag & \decFlag{1} & \decFlag{2} \\ \hline\hline
5-
\inst{POP} & \zero & \oneCell & \oneCell & \zero \\ \hline
6-
\inst{PUSH1-32} & \zero & \oneCell & \zero & \oneCell \\ \hline
4+
\INST & \tli & \stackDecPushPopFlag & \decFlag{1} & \decFlag{2} & \decFlag{3} \\ \hline\hline
5+
\inst{POP} & \zero & \oneCell & \oneCell & \zero & \zero \\ \hline
6+
\inst{PUSH1-32} & \zero & \oneCell & \zero & \oneCell & \zero \\ \hline
7+
\inst{PUSH0} & \zero & \oneCell & \zero & \zero & \oneCell \\ \hline
78
\end{array}
89
\]
10+
\saNote{}
11+
We separate the \inst{PUSH0} from the other \inst{PUSHX}, $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$, instructions.
12+
This stems from the fact that they are treated differently in the \romMod{} module:
13+
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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
We define some shorthands
22
\[
33
\left\{ \begin{array}{lcl}
4-
\locIsPop & \define & \decFlag {1} _{i} \\
5-
\locIsPush & \define & \decFlag {2} _{i} \\
4+
\locIsPop & \define & \decFlag {1} _{i} \\
5+
\locIsPush & \define & \decFlag {2} _{i} \\
6+
\locIsPushZero & \define & \decFlag {3} _{i} \\
67
\end{array} \right.
78
\quad
89
\left\{ \begin{array}{lcl}

‎rom_v3/_inputs.tex

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
\input{_local}
22
\section{The \romMod{} module} \label{rom}
33
\subsection{Introduction} \label{rom: intro} \input{intro}
4+
\subsection{Convention} \label{rom: convention} \input{convention}
45
\subsection{Column description} \label{rom: columns} \input{columns}
56
\subsection{Generalities} \label{rom: constraints} \input{generalities/_inputs}
67
\subsection{Connecting \pbcb{} to \opc{} and related flags} \label{rom: opcode related constraints} \input{opcode/_inputs}

‎rom_v3/columns.tex

Lines changed: 20 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,9 @@
7373
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}$);
7474
in all other circumstances \( \opc{} = \PBCB{} \);
7575
\item \IP{}:
76-
lights up precisely when $\opc \equiv \inst{PUSHX}$ for some $\inst{X} \in \{ 1, 2, \dots, \evmWordSize \}$;
76+
lights up precisely when
77+
$\opc \equiv \inst{PUSHX}$\footnote{Recall our convention~(\ref{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0})}
78+
for some $\inst{X}$;
7779
abbreviated to \ip{};
7880
\item \IPD{}:
7981
binary flag;
@@ -89,3 +91,20 @@
8991
The \opc{} and \pbcb{} columns differ in that bytes that are ``obscured'' by a previous \inst{PUSHX} opcode
9092
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}).
9193
As such the above precisely recognizes valid jump destinations as specified in the \cite{EYP}.
94+
95+
\saNote{}
96+
\label{rom: columns: IS_PUSH_FLAG does not light up for PUSH0}
97+
We draw attention to the fact that the \romMod{} module
98+
doesn't deal with the \inst{PUSH0} instruction of \cite{EIP-3855} as it does with
99+
\inst{PUSHX} instructions\footnote{Recall our convention~(\ref{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0})}.
100+
For one, it doesn't construct a ``push value'' for \inst{PUSH0} instructions.
101+
As a consequence, the \inst{PUSH0} opcode \textbf{does not raise} the \IP{} flag while the other \inst{PUSHX} instructions do,
102+
see diagram~(\ref{rom: instruction decoding: relevant portion of ID module}).
103+
104+
\saNote{}
105+
\label{rom: columns: push values for PUSH0 vs PUSHX in the HUB}
106+
Given that the ``push value'' of a \inst{PUSH0} instruction is zero by definition,
107+
the \hubMod{} module knows to push \inst{0x\,00} to the stack for that opcode,
108+
see section~(\ref{hub: instruction handling: push pop: setting result to zero for PUSH0}).
109+
For \inst{PUSHX} instructions the \hubMod{} module is reliant on the $\PV$ constructed in the present module,
110+
see section~(\ref{hub: instruction handling: push pop: setting result to push value for PUSHX}).

‎rom_v3/convention.tex

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
\label{rom: intro: convention: PUSHX implicitly refers to PUSH1 through PUSH32 but not PUSH0}
2+
Throughout the specification of the \romMod{} module, whenever we write
3+
``\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} \}$.
4+
The \inst{PUSH0} instruction of \cite{EIP-3855} is dealt with differently than the other \inst{PUSHX} instructions,
5+
see section~(\ref{rom: columns: IS_PUSH_FLAG does not light up for PUSH0}) for more details.

‎rom_v3/intro.tex

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,16 @@
1-
The \romMod{} module compiles the \emph{nonempty} bytecodes, initialization codes and deployed byte codes alike, used during the execution of a conflation of blocks.
1+
The \romMod{} module compiles the \textbf{nonempty} bytecodes, initialization codes and deployed byte codes alike, used during the execution of a conflation of blocks.
22
Its main role in the overall design is to provide the \hubMod{} module with the correct sequence of instructions.
3-
It furthermore assembles the \inst{PUSH}-values from the bytes following a \inst{PUSHX} instruction.
4-
It also tags (in)valid jump destinations as such as required by \textsc{jump destination analysis}.
5-
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).
3+
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} \}$.
4+
It also tags (in)valid jump destinations as such, as is required by \textsc{jump destination analysis}.
5+
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).
66

77
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):
88
\begin{enumerate}
9-
\item loading the full bytecode of an already deployed smart contract to \inst{CALL} it or to \inst{EXTCODECOPY} from it (or both);
9+
\item loading the full bytecode of an already deployed smart contract to \inst{CALL}, \inst{CALLCODE}, \inst{STATICCALL} or \inst{DELEGATECALL} into it;
10+
\item loading the full bytecode of an already deployed smart contract to \inst{EXTCODECOPY} from it;
1011
\item deploying a smart contract through a deployment transaction or an (unexceptional, unaborted and no failure condition raising) \inst{CREATE(2)} instruction:
1112
\begin{enumerate}
12-
\item loading the initialization code into \romMod{};
13-
\item and for (temporarily) successful deployments loading the bytecode that will be deployed at the relevant address into \romMod{}.
13+
\item loading the initialization code into the \romMod{} module;
14+
\item and for (temporarily) successful deployments loading the bytecode that will be (temporarily) deployed at the relevant address into the \romMod{} module.
1415
\end{enumerate}
1516
\end{enumerate}

‎rom_v3/lookups/rom_into_instruction_decoder.tex

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -31,15 +31,16 @@
3131
\[
3232
\renewcommand{\arraystretch}{1.3}
3333
\begin{array}{|l|c|c|} \hline
34-
\opc & \idMod/\IP & \idMod/\IJD \\ \hline \hline
35-
\inst{PUSHX} & \rOne & \gZero \\ \hline
36-
\inst{JUMPDEST} & \gZero & \rOne \\ \hline
37-
\texttt{<any other byte>} & \gZero & \gZero \\ \hline
34+
\opc & \idMod\separator\IP & \idMod\separator\IJD \\ \hline \hline
35+
\inst{PUSH0} & \gZero & \gZero \\ \hline
36+
\inst{PUSHX} & \rOne & \gZero \\ \hline
37+
\inst{JUMPDEST} & \gZero & \rOne \\ \hline
38+
\texttt{<any other byte>} & \gZero & \gZero \\ \hline
3839
\end{array}
3940
\]
4041
\caption{%
4142
Relevant portion of the \idMod{} module.
42-
In the above $\inst{X} \in \{ 1, 2, \dots, \evmWordSize \}$}
43+
In the above $\inst{X} \in \{ \inst{1}, \inst{2}, \dots, \inst{32} \}$}
4344
\label{rom: instruction decoding: relevant portion of ID module}
4445
\end{figure}
4546

0 commit comments

Comments
 (0)