diff --git a/hub/instruction_handling/call/generalities/_inputs.tex b/hub/instruction_handling/call/generalities/_inputs.tex index 02e6830..9fa6cf4 100644 --- a/hub/instruction_handling/call/generalities/_inputs.tex +++ b/hub/instruction_handling/call/generalities/_inputs.tex @@ -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} diff --git a/hub/instruction_handling/call/generalities/universal.tex b/hub/instruction_handling/call/generalities/universal.tex index b25e600..87d954c 100644 --- a/hub/instruction_handling/call/generalities/universal.tex +++ b/hub/instruction_handling/call/generalities/universal.tex @@ -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 \[ diff --git a/hub/misc/stp/call.tex b/hub/misc/stp/call.tex index d34e6ff..7e6d062 100644 --- a/hub/misc/stp/call.tex +++ b/hub/misc/stp/call.tex @@ -9,8 +9,8 @@ gasLo = \locGasLo, valueHi = \locValueHi, valueLo = \locValueLo, - warmth = \locTargetExists, - exists = \locTargetWarmth, + exists = \locTargetExists, + warmth = \locTargetWarmth, mxpGas = \locMxpGasMxp, } \vspace{4mm}\\ diff --git a/pkg/xkeyval_macros/stp_instructions.sty b/pkg/xkeyval_macros/stp_instructions.sty index 9f77d1a..30d48cf 100644 --- a/pkg/xkeyval_macros/stp_instructions.sty +++ b/pkg/xkeyval_macros/stp_instructions.sty @@ -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] } diff --git a/stp/vanishing.tex b/stp/vanishing.tex index 6c4c25d..e2b2113 100644 --- a/stp/vanishing.tex +++ b/stp/vanishing.tex @@ -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.}