Skip to content

Commit

Permalink
CALL related HUB and STP fixes (#5)
Browse files Browse the repository at this point in the history
  • Loading branch information
@OlivierBBB
OlivierBBB authored Nov 21, 2024
1 parent d1774e0 commit f8a2278
Show file tree
Hide file tree
Showing 5 changed files with 41 additions and 51 deletions.
10 changes: 5 additions & 5 deletions hub/instruction_handling/call/generalities/_inputs.tex
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
\subsubsubsection{Graphical representation \lispNone{}} \label{hub: instruction handling: call: generalities} \input{instruction_handling/call/generalities/lua/_inputs}
\subsubsubsection{Universal constraints for \inst{CALL}'s \lispDone{}} \label{hub: instruction handling: call: generalities} \input{instruction_handling/call/generalities/universal}
\subsubsubsection{First set of account-rows \lispDone{}} \label{hub: instruction handling: call: first set of account rows} \input{instruction_handling/call/generalities/account_rows_first_set}
\subsubsubsection{Second set of account-rows \lispDone{}} \label{hub: instruction handling: call: second set of account rows} \input{instruction_handling/call/generalities/account_rows_second_set}
\subsubsubsection{Third set of account-rows \lispDone{}} \label{hub: instruction handling: call: third set of account rows} \input{instruction_handling/call/generalities/account_rows_third_set}
\subsubsubsection{Graphical representation \lispNone{}} \label{hub: instruction handling: call: generalities} \input{instruction_handling/call/generalities/lua/_inputs}
\subsubsubsection{Universal constraints for \inst{CALL}'s \lispDone{}} \label{hub: instruction handling: call: generalities: universal} \input{instruction_handling/call/generalities/universal}
\subsubsubsection{First set of account-rows \lispDone{}} \label{hub: instruction handling: call: generalities: first set of account rows} \input{instruction_handling/call/generalities/account_rows_first_set}
\subsubsubsection{Second set of account-rows \lispDone{}} \label{hub: instruction handling: call: generalities: second set of account rows} \input{instruction_handling/call/generalities/account_rows_second_set}
\subsubsubsection{Third set of account-rows \lispDone{}} \label{hub: instruction handling: call: generalities: third set of account rows} \input{instruction_handling/call/generalities/account_rows_third_set}
37 changes: 14 additions & 23 deletions hub/instruction_handling/call/generalities/universal.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,31 +148,22 @@
\If $\miscStpFlag_{i + \callMiscRowOffset} = 1$ \Then we impose that
\[
\setStpInstructionCall{
anchorRow = i ,
relOffset = \callMiscRowOffset ,
instruction = \locInst ,
gasHi = \locGasHi ,
gasLo = \locGasLo ,
valueHi = \locValueHi ,
valueLo = \locValueLo ,
warmth = \locCalleeExists ,
exists = \locCalleeWarmth ,
mxpGas = \locMxpMemoryExpansionGas ,
anchorRow = i ,
relOffset = \callMiscRowOffset ,
instruction = \locInst ,
gasHi = \locGasHi ,
gasLo = \locGasLo ,
valueHi = \locValueHi ,
valueLo = \locValueLo ,
exists = \locCalleeExists \cdot \locIsCall ,
warmth = \locCalleeWarmth ,
mxpGas = \locMxpMemoryExpansionGas ,
}
% \left\{ \begin{array}{lcl}
% \miscStpInst _{i + \callMiscRowOffset} & = & \locInst_{i} \\
% \miscStpGasHi _{i + \callMiscRowOffset} & = & \locGasHi \\
% \miscStpGasLo _{i + \callMiscRowOffset} & = & \locGasLo \\
% \miscStpValueHi _{i + \callMiscRowOffset} & = & \locValueHi \\
% \miscStpValueLo _{i + \callMiscRowOffset} & = & \locValueHi \\
% \miscStpAccExists _{i + \callMiscRowOffset} & = & \locCalleeExists \\
% \miscStpAccWarmth _{i + \callMiscRowOffset} & = & \locCalleeWarmth \\
% \miscStpOogx _{i + \callMiscRowOffset} & = & \locOogx \\
% \miscStpGasUpfront _{i + \callMiscRowOffset} & = & \relevantValue \\
% \miscStpGasPoop _{i + \callMiscRowOffset} & = & \relevantValue \\
% \miscStpGasStipend _{i + \callMiscRowOffset} & = & \relevantValue \\
% \end{array} \right.
\]
\saNote{} \label{hub: instruction handling: call: generalities: universal: account existence for non CALLs}
\inst{CALL} is the only \inst{CALL}-type instruction which may lead to an account being added to the state.
Recall that this happens whenever a \inst{CALL} transfers nonzero value to an address for which no account exists in the state.
As such we only care about the existence of the target account for the \inst{CALL} instruction.
\item[\underline{Justifying \oogxSH's:}]
\If $\miscStpFlag_{i + \callMiscRowOffset} = 1$ \Then we impose that
\[
Expand Down
4 changes: 2 additions & 2 deletions hub/misc/stp/call.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@
gasLo = \locGasLo,
valueHi = \locValueHi,
valueLo = \locValueLo,
warmth = \locTargetExists,
exists = \locTargetWarmth,
exists = \locTargetExists,
warmth = \locTargetWarmth,
mxpGas = \locMxpGasMxp,
}
\vspace{4mm}\\
Expand Down
4 changes: 2 additions & 2 deletions pkg/xkeyval_macros/stp_instructions.sty
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,8 @@ mxpGas = \missingParameter,
\utt{Gas low:} & \cmdSTP@var@gasLo \\
\utt{Value high:} & \cmdSTP@var@valueHi \\
\utt{Value low:} & \cmdSTP@var@valueLo \\
\utt{Target exists:} & \cmdSTP@var@warmth \\
\utt{Target warmth:} & \cmdSTP@var@exists \\
\utt{Target exists:} & \cmdSTP@var@exists \\
\utt{Target warmth:} & \cmdSTP@var@warmth \\
\utt{Memory expansion gas:} & \cmdSTP@var@mxpGas \\
\end{array} \right] }

Expand Down
37 changes: 18 additions & 19 deletions stp/vanishing.tex
View file
Original file line number Diff line number Diff line change
@@ -1,30 +1,29 @@
The present section presents vanishing constraints for columns that aren't used depeding on the instruction type. We \emph{may} impose that
The present section presents vanishing constraints for columns that aren't used depending on the instruction type. We \emph{may} impose that
\begin{description}
\item[\underline{\inst{CREATE}-type instructions:}] \If $\isCreate_{i} = 1$ \Then
\[
\left\{\begin{array}{lclr}
\gasHi_{i} & = & 0 & (\trash) \\
\gasLo_{i} & = & 0 & (\trash) \\
\warm_{i} & = & 0 & (\trash) \\
\existence_{i} & = & 0 & (\trash) \\
\gasHi _{i} & = & 0 & (\trash) \\
\gasLo _{i} & = & 0 & (\trash) \\
\end{array}\right.
\]
\item[\underline{\inst{CALL} instructions:}] \If $\stpCall_{i} = 1$ \Then we impose nothing;
\item[\underline{\inst{CALLCODE} instructions:}] \If $\stpCallCode_{i} = 1$ \Then we impose \( \existence_{i} = 1 \)
\item[\underline{\inst{DELEGATECALL} instructions:}] \If $\stpDelegateCall_{i} = 1$ \Then
\item[\underline{\inst{DELEGATECALL} and \inst{STATICCALL} instructions:}]
\If $\stpDelegateCall _{i} + \stpStaticCall _{i} = 1$
\Then we impose
\[
\left\{\begin{array}{lclr}
\valHi_{i} & = & 0 & (\trash) \\
\valLo_{i} & = & 0 & (\trash) \\
\existence_{i} & = & 1 & (\trash) \\
\end{array}\right.
\]
\item[\underline{\inst{STATICCALL} instructions:}] \If $\stpStaticCall_{i} = 1$ \Then
\[
\left\{\begin{array}{lclr}
\valHi_{i} & = & 0 & (\trash) \\
\valLo_{i} & = & 0 & (\trash) \\
\valHi _{i} & = & 0 & (\trash) \\
\valLo _{i} & = & 0 & (\trash) \\
\end{array}\right.
\]
\saNote{}
Recall that neither \inst{DELEGATECALL} nor \inst{STATICCALL} have a ``\texttt{value}'' argument.
\item[\underline{Non \inst{CALL}, \inst{CALL}-type instructions:}]
\If $\stpCallCode _{i} + \stpDelegateCall _{i} + \stpStaticCall _{i} = 1$
\Then we impose that
\[ \existence _{i} = 0 \]
\saNote{}
We justify the choice to impose $\existence \equiv 0$ for non \inst{CALL}, \inst{CALL}-type instructions in
section~(\ref{hub: instruction handling: call: generalities: universal}),
specifically in (\ref{hub: instruction handling: call: generalities: universal: account existence for non CALLs}).
\end{description}
\ob{TODO: are these restrictions desirable ? These are obviously harmless constraints, they make for slighty smaller lookups if we segregate them by instruction type, and potentially add constraints if we don't.}

0 comments on commit f8a2278

Please sign in to comment.