From e48ea04ca7030f749a1cc69245439cfd7985e741 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 2 Dec 2024 12:10:57 +0700 Subject: [PATCH 1/9] fix: bugfix for GAS_NEXT of CREATE's - exceptional CREATE's consume all gas - aborted CREATE's consume only the upfront gas cost - CREATE's that raise the Failure Condition F consume the upfront gas cost + the 63/64ths given to the child context which they don't get back - CREATE's with empty init code get those 63/64ths back immediately so from the zkevm POV don't pay for it at all - CREATE's with nonempty init code consume the upfront ga cost + the 63/64th's which they provide to the child context (and may et back in part) --- hub/instruction_handling/create/_local.tex | 3 +- .../create/generalities/all.tex | 57 ++++++++++++------- 2 files changed, 39 insertions(+), 21 deletions(-) diff --git a/hub/instruction_handling/create/_local.tex b/hub/instruction_handling/create/_local.tex index 6b044ca..7eeab81 100644 --- a/hub/instruction_handling/create/_local.tex +++ b/hub/instruction_handling/create/_local.tex @@ -101,7 +101,8 @@ \def\locAuxId {\col{aux\_id}} \def\locExoSum {\col{exo\_sum}} - +\def\locCreateUpfrontGasCost {\col{upfront\_gas\_cost}} +\def\locCreateFullGasCost {\col{full\_gas\_cost}} % CALL specific row offset constants \def\createFirstStackRowOffset {\greenm{2}} diff --git a/hub/instruction_handling/create/generalities/all.tex b/hub/instruction_handling/create/generalities/all.tex index 9eb5012..bcbcf3b 100644 --- a/hub/instruction_handling/create/generalities/all.tex +++ b/hub/instruction_handling/create/generalities/all.tex @@ -6,7 +6,7 @@ \scenCreateSum _{i} & = & 1 \\ \end{array} \right.} \end{center} -The present section deals with generalities pertaining to \inst{CREATE}-type instructions. These constraints hold regardless of anything else. +The present section deals with generalities pertaining to \inst{CREATE}-type instructions. These constraints hold regardless of anything else. \begin{description} \item[\underline{Setting the stack pattern:}] we impose $\createSP_{i - \createFirstStackRowOffset}\big[ \locIsCreateTwo \big]$; @@ -47,7 +47,7 @@ \[ \locStaticx = \locIsStatic \] - \item[\underline{Setting the module flags of miscellaneous-row $n^°(i + \createMiscRowOffset)$::}] + \item[\underline{Setting the module flags of miscellaneous-row $n^°(i + \createMiscRowOffset)$::}] every processing path for \inst{CREATE}-type instructions contains a single \textbf{miscellaneous-row} \[ \weightedMiscFlagSum @@ -129,12 +129,12 @@ where we define the following shorthands: \[ \left\{ \begin{array}{lclc} - \If \locTriggerRlpAddr = 0 ~ \Then + \If \locTriggerRlpAddr = 0 ~ \Then \left\{ \begin{array}{lclc} \locCreateeNonce & = & 0 \\ \locCreateeHasCode & = & 0 \\ \end{array} \right. \\ - \If \locTriggerRlpAddr = 1 ~ \Then + \If \locTriggerRlpAddr = 1 ~ \Then \left\{ \begin{array}{lclc} \locCreateeNonce & = & \accNonce _{i + \createFirstCreateeAccountRowOffset} \\ \locCreateeHasCode & = & \accHasCode _{i + \createFirstCreateeAccountRowOffset} \\ @@ -199,7 +199,7 @@ \] where we have used the following (as of yet undefined) shorthands \locTgtId{}, \locAuxId{} and \locExoSum{} which we define as follows: \begin{enumerate} - \item \If $\locHashInitCode = 1$ \Then + \item \If $\locHashInitCode = 1$ \Then \[ \left\{ \begin{array}{lcl} \locTgtId & \define & \nothing \\ @@ -207,7 +207,7 @@ \locExoSum & \define & \exoWeightKec \\ \end{array} \right. \] - \item \If $\locHashInitCodeAndSendToRom = 1$ \Then + \item \If $\locHashInitCodeAndSendToRom = 1$ \Then \[ \left\{ \begin{array}{lcl} \locTgtId & \define & \locDepCfi \\ @@ -215,7 +215,7 @@ \locExoSum & \define & \exoWeightRom + \exoWeightKec \\ \end{array} \right. \] - \item \If $\locSendInitCodeToRom = 1$ \Then + \item \If $\locSendInitCodeToRom = 1$ \Then \[ \left\{ \begin{array}{lcl} \locTgtId & \define & \locDepCfi \\ @@ -234,24 +234,41 @@ \If \scenCreateExecutionNonEmptyInitCode _{i} = 1 & \Then & \nextContextIsNew _{i} \\ \end{array} \right. \] +\end{description} +Let us define the following shorthands: +\[ + \left\{ \begin{array}{lcl} + \locCreateUpfrontGasCost & \define & G_\text{create} + \locMxpGas \\ + \locCreateFullGasCost & \define & \locCreateUpfrontGasCost + \locStpGasPoop \\ + \end{array} \right. +\] +\begin{description} \item[\underline{Setting the \gasCost{}:}] we impose \begin{enumerate} \item \If $\locStaticx + \locMxpx = 1$ \Then $\gasCost _{i} = 0$ - \item \If $\locOogx + \scenCreateUnexceptional = 1$ \Then $\gasCost _{i} = G_\text{create} + \locMxpGas$ + \item \If $\locOogx + \scenCreateUnexceptional = 1$ \Then $\gasCost _{i} = \locCreateUpfrontGasCost$ \end{enumerate} \item[\underline{Setting the \gasNext{}:}] we impose - \begin{enumerate} - \item \If $\scenCreateException _{i} = 1$ \Then $\gasNext_{i} = 0$ (\trash) - \item \If $\scenCreateNoContextChange _{i} = 1$ \Then $\gasNext_{i} = \gasActual_{i} - \gasCost_{i}$ - \item \If $\scenCreateExecutionNonEmptyInitCode _{i} = 1$ \Then - \[ - \gasNext_{i} = \gasActual_{i} - - \left[ \begin{array}{cl} - + & \gasCost_{i} \\ - + & \locStpGasPoop \\ - \end{array} \right] - \] - \end{enumerate} + \[ + \hspace*{-0.5cm} + \left\{ \begin{array}{lcl} + \If \scenCreateException _{i} = 1 & \Then & \gasNext _{i} = 0 ~ (\trash) \\ + \If \scenCreateAbort _{i} = 1 & \Then & \gasNext _{i} = \gasActual _{i} - \locCreateUpfrontGasCost \\ + \If \scenCreateFCond _{i} = 1 & \Then & \gasNext _{i} = \gasActual _{i} - \locCreateFullGasCost \\ + \If \scenCreateExecutionEmptyInitCode _{i} = 1 & \Then & \gasNext _{i} = \gasActual _{i} - \locCreateUpfrontGasCost \\ + \If \scenCreateExecutionNonEmptyInitCode _{i} = 1 & \Then & \gasNext _{i} = \gasActual _{i} - \locCreateFullGasCost \\ + \end{array} \right. + \] + \saNote{} + We provide some details. + Exceptional \inst{CREATE}-type instructions, like any exceptional instruction, fully consume the currently available gas. + Aborted \inst{CREATE}-type instructions only pay for the \locCreateUpfrontGasCost{} (and there is no child context.) + \inst{CREATE}-type instructions that raise the \textbf{Failure Condition $\bm{F}$} pay the \locCreateFullGasCost{}, including the ``\texttt{(63/64)-ths}'' to the child context, and don't get any of it back. + \inst{CREATE}-type instructions that lead to execution pay for \locCreateFullGasCost{}. + However, if the provided initialization code is \emph{empty}, then the execution context doesn't change and gets the entire ``\texttt{(63/64)-ths}'' back immediately. + The effective gas cost is therefore the \locCreateUpfrontGasCost{}. + If the provided initialization code is \emph{nonempty} then the execution context pays the \locCreateFullGasCost{}. + It \emph{may} get some of it back later down the line. \end{description} From 024769687561072e8761285a4d80c804c6d2123a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Thu, 5 Dec 2024 10:49:54 +0700 Subject: [PATCH 2/9] Rationalization of `REFUND` increments for `SSTORE` (#22) --- hub/instruction_handling/storage/_local.tex | 12 ++ .../storage/constraints.tex | 127 +++++++++++++----- 2 files changed, 108 insertions(+), 31 deletions(-) diff --git a/hub/instruction_handling/storage/_local.tex b/hub/instruction_handling/storage/_local.tex index 69935b7..67dfedb 100644 --- a/hub/instruction_handling/storage/_local.tex +++ b/hub/instruction_handling/storage/_local.tex @@ -4,6 +4,14 @@ \def\locCurrIsOrig {\col{curr\_is\_orig}} \def\locNextIsOrig {\col{next\_is\_orig}} \def\locNextIsCurr {\col{next\_is\_curr}} + +\def\locOrigNotZero {\col{orig\_not\_zero}} +\def\locCurrNotZero {\col{curr\_not\_zero}} +\def\locNextNotZero {\col{next\_not\_zero}} +\def\locCurrNotOrig {\col{curr\_not\_orig}} +\def\locNextNotOrig {\col{next\_not\_orig}} +\def\locNextNotCurr {\col{next\_not\_curr}} + \def\locFirstCon {\yellowm{1}} \def\locStaticxSecondCon {\yellowm{2}} \def\locSstorexMisc {\yellowm{2}} @@ -28,3 +36,7 @@ \def\locLoadedValueLo {\col{loaded\_value\_lo}} \def\locValueToStoreHi {\col{value\_to\_store\_hi}} \def\locValueToStoreLo {\col{value\_to\_store\_lo}} + +\def\locCleanClear {\col{r\_clean\_clear}} +\def\locDirtyClear {\col{r\_dirty\_clear}} +\def\locDirtyReset {\col{r\_dirty\_reset}} diff --git a/hub/instruction_handling/storage/constraints.tex b/hub/instruction_handling/storage/constraints.tex index 704a061..d24f5a1 100644 --- a/hub/instruction_handling/storage/constraints.tex +++ b/hub/instruction_handling/storage/constraints.tex @@ -191,6 +191,15 @@ \locNextIsOrig & \!\!\! \define \!\!\! & \stoNextValueIsOrig_{i + \locFirstStoRowOffset} \\ \locNextIsCurr & \!\!\! \define \!\!\! & \stoNextValueIsCurr_{i + \locFirstStoRowOffset} \\ \end{array} \right. + \quad\text{and}\quad + \left\{ \begin{array}{lcl} + \locOrigNotZero & \!\!\! \define \!\!\! & 1 - \locOrigIsZero \\ + \locCurrNotZero & \!\!\! \define \!\!\! & 1 - \locCurrIsZero \\ + \locNextNotZero & \!\!\! \define \!\!\! & 1 - \locNextIsZero \\ + \locCurrNotOrig & \!\!\! \define \!\!\! & 1 - \locCurrIsOrig \\ + \locNextNotOrig & \!\!\! \define \!\!\! & 1 - \locNextIsOrig \\ + \locNextNotCurr & \!\!\! \define \!\!\! & 1 - \locNextIsCurr \\ + \end{array} \right. \] \begin{description} \item[\underline{Setting the gas cost:}] @@ -207,12 +216,12 @@ \item[\underline{The \inst{SSTORE} case:}] \If $\locIsSstore = 1$ \Then \begin{enumerate} - \item \If $\locNextIsCurr = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $ - \item \If $\locCurrIsOrig = 0$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $ - \item \If \Big($\locNextIsCurr = 0$ \et $\locCurrIsOrig = 1$\Big) + \item \If $\locNextIsCurr = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $ + \item \If $\locCurrNotOrig = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{warmaccess} $ + \item \If \Big($\locNextNotCurr = 1$ \et $\locCurrIsOrig = 1$\Big) \begin{enumerate} - \item \If $\locOrigIsZero = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sset} $ - \item \If $\locOrigIsZero = 0$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sreset} $ + \item \If $\locOrigIsZero = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sset} $ + \item \If $\locOrigNotZero = 1$ \Then $ \gasCost_{i} = \locColdStorageSlot \cdot G_\text{coldsload} + G_\text{sreset} $ \end{enumerate} \end{enumerate} where in the above we have used the following shorthand @@ -221,31 +230,87 @@ \] \end{description} \item[\underline{Setting the refund:}] - recall that among instructions raising the $\stackDecStoFlag$ only the \inst{SSTORE} instruction may grand refunds. - Futhermore refunds may only be granted in non reverting contexts. + recall that among instructions raising the $\stackDecStoFlag$ only the \inst{SSTORE} instruction ($\locIsSstore \equiv 1$) may grand refunds. + Futhermore refunds may only be granted in non reverting contexts ($\cnWillRev \equiv 0$.) See section~(\ref{hub: generalities: refunds: refunds}) for more details. - \If \Big($\cnWillRev_{i} = 0$ \et $\locIsSstore = 1$\Big) \Then we thus impose that - \begin{enumerate} - \item \If $\locNextIsCurr = 1$ \Then $\refund\new_{i} = \refund_{i}$ - \item \If $\locNextIsCurr = 0$ \Then - \begin{enumerate} - \item \If $\locCurrIsOrig = 0$ \Then - \[ - \refund\new_{i} = \refund_{i} - + - \left[ \begin{array}{crcccl} - + & (1 - \locOrigIsZero) & \cdot & (\locNextIsZero - \locCurrIsZero) & \cdot & R_\text{sclear} \\ - + & \locNextIsOrig & \cdot & \locOrigIsZero & \cdot & \big(G_\text{sset} - G_\text{warmaccess}\big) \\ - + & \locNextIsOrig & \cdot & (1 -\locOrigIsZero) & \cdot & \big(G_\text{sreset} - G_\text{warmaccess}\big) \\ - \end{array} \right] - \] - \item \If $\locCurrIsOrig = 1$ \Then - \begin{enumerate} - \item \If $\locNextIsZero = 0$ \Then $\refund\new_{i} = \refund_{i}$ - \item \If $\locNextIsZero = 1$ \Then $\refund\new_{i} = \refund_{i} + R_\text{sclear}$ - \end{enumerate} - \end{enumerate} - \end{enumerate} -\end{description} - + We therefore unconditionally impose + \[ + \refund\new _{i} = \refund_{i} + (1 - \cnWillRev_{i}) \cdot \locIsSstore \cdot + \left[ \begin{array}{cr} + + & \locCleanClear \\ + + & \locDirtyClear \\ + + & \locDirtyReset \\ + \end{array} \right] + \] + where $\locCleanClear$, $\locDirtyClear$, $\locDirtyReset$ are shorthands which we define below. + + \saNote{} + In the explanations provided below we use notations from the \cite{EYP} whereby + $v_0$ stands for the value originally in storage, + $v$ for the value currently in storage, + $v'$ for the value we are attempting to store: + \begin{description} + \item[\underline{Defining \locCleanClear{}:}] + we set + \[ + \locCleanClear \define + \left[ \begin{array}{cr} + \cdot & \locNextNotCurr \\ + \cdot & \locCurrIsOrig \\ + \cdot & \locNextIsZero \\ + \end{array} \right] + \cdot R_\text{sclear} + \] + which corresponds to + \begin{itemize} + \item $R_\text{sclear}$ whenever $[v \neq v'] \wedge [v = v_{0}] \wedge [v' = 0]$ + \item and $0$ otherwise + \end{itemize} + \item[\underline{Defining \locDirtyClear{}:}] + we set + \[ + \locDirtyClear \define + \left[ \begin{array}{cr} + \cdot & \locNextNotCurr \\ + \cdot & \locCurrNotOrig \\ + \end{array} \right] + \cdot + \locOrigNotZero + \cdot + \left[ \begin{array}{cr} + - & \locCurrIsZero \\ + + & \locNextIsZero \\ + \end{array} \right] + \cdot R_\text{sclear} + \] + which corresponds to + \begin{itemize} + \item $- R_\text{sclear}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} \neq 0] \wedge [v = 0]$, + \item $+ R_\text{sclear}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} \neq 0] \wedge [v' = 0]$, + \item and $0$ otherwise. + \end{itemize} + \item[\underline{Defining \locDirtyReset{}:}] + we set + \[ + \locDirtyReset \define + \left[ \begin{array}{cr} + \cdot & \locNextNotCurr \\ + \cdot & \locCurrNotOrig \\ + \end{array} \right] + \cdot + \locNextIsOrig + \cdot + \left[ \begin{array}{crcl} + + & \locOrigIsZero & \cdot & \big(G_\text{sset} - G_\text{warmaccess}\big) \\ + + & \locOrigNotZero & \cdot & \big(G_\text{sreset} - G_\text{warmaccess}\big) \\ + \end{array} \right] + \] + which corresponds to + \begin{itemize} + \item $G_\text{sset} - G_\text{warmaccess}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} = v'] \wedge [v_{0} = 0]$, + \item $G_\text{sreset} - G_\text{warmaccess}$ whenever $[v \neq v'] \wedge [v_{0} \neq v]$ and $[v_{0} = v'] \wedge [v_{0} \neq 0]$, + \item and $0$ otherwise. + \end{itemize} + \end{description} + \end{description} From 071a4643e4a6763eb512dd866164d4a2ac07422c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Thu, 5 Dec 2024 11:45:23 +0700 Subject: [PATCH 3/9] Provide HUB -> RLPADDR with the correct `init_code_hash` (#17) --- hub/instruction_handling/create/_local.tex | 4 +- .../create/generalities/unexceptional.tex | 63 +++++++++++++++---- .../create/shorthands.tex | 42 ++++++------- 3 files changed, 75 insertions(+), 34 deletions(-) diff --git a/hub/instruction_handling/create/_local.tex b/hub/instruction_handling/create/_local.tex index 7eeab81..fbdc8d1 100644 --- a/hub/instruction_handling/create/_local.tex +++ b/hub/instruction_handling/create/_local.tex @@ -16,10 +16,12 @@ \def\locMxpx {\col{STACK\_mxpx}} \def\locOogx {\col{STACK\_oogx}} % -\def\relevantValue {\texttt{}} +\def\relevantValue {\texttt{}} % \def\locTriggerHashInfo {\col{trigger\_\hashInfoMod}} \def\locHashInfoStamp {\col{hash\_info\_stamp}} +\def\locHashInfoKeccakHi {\hashInfoMod\col{\_kec\_hi}} +\def\locHashInfoKeccakLo {\hashInfoMod\col{\_kec\_lo}} \def\locInitCodeHashHi {\col{init\_code\_hash\_hi}} \def\locInitCodeHashLo {\col{init\_code\_hash\_lo}} \def\locInitCodeSize {\col{init\_code\_size}} diff --git a/hub/instruction_handling/create/generalities/unexceptional.tex b/hub/instruction_handling/create/generalities/unexceptional.tex index 007be8f..1fcd952 100644 --- a/hub/instruction_handling/create/generalities/unexceptional.tex +++ b/hub/instruction_handling/create/generalities/unexceptional.tex @@ -60,23 +60,62 @@ \[ \left\{ \begin{array}{lcl} % \accRlpAddrFlag _{i + \createFirstCreatorAccountRowOffset} & = & \rOne \\ - \accRlpAddrRecipe _{i + \createFirstCreatorAccountRowOffset} & = & \locRlpAddrRecipe \\ - \accRlpAddrDepAddrHi _{i + \createFirstCreatorAccountRowOffset} & = & \relevantValue \\ - \accRlpAddrDepAddrLo _{i + \createFirstCreatorAccountRowOffset} & = & \relevantValue \\ - \accRlpAddrSaltHi _{i + \createFirstCreatorAccountRowOffset} & = & \locSaltHi \\ - \accRlpAddrSaltLo _{i + \createFirstCreatorAccountRowOffset} & = & \locSaltLo \\ - \accRlpAddrKecHi _{i + \createFirstCreatorAccountRowOffset} & = & \locInitCodeHashHi \\ - \accRlpAddrKecLo _{i + \createFirstCreatorAccountRowOffset} & = & \locInitCodeHashLo \\ + \accRlpAddrRecipe _{i + \createFirstCreatorAccountRowOffset} & = & \locRlpAddrRecipe \\ + \accRlpAddrDepAddrHi _{i + \createFirstCreatorAccountRowOffset} & = & \relevantValue \\ + \accRlpAddrDepAddrLo _{i + \createFirstCreatorAccountRowOffset} & = & \relevantValue \\ + \accRlpAddrSaltHi _{i + \createFirstCreatorAccountRowOffset} & = & \locSaltHi \\ + \accRlpAddrSaltLo _{i + \createFirstCreatorAccountRowOffset} & = & \locSaltLo \\ + \accRlpAddrKecHi _{i + \createFirstCreatorAccountRowOffset} & = & \locInitCodeHashHi \\ + \accRlpAddrKecLo _{i + \createFirstCreatorAccountRowOffset} & = & \locInitCodeHashLo \\ \end{array} \right. \] where we set \[ - \locRlpAddrRecipe := - \left[ \begin{array}{lrcl} - + & \locIsCreate & \!\!\! \cdot \!\!\! & \addressCreationRecipeConstantStd \\ - + & \locIsCreateTwo & \!\!\! \cdot \!\!\! & \addressCreationRecipeConstantTwo \\ - \end{array} \right] + \left\{ \begin{array}{lcl} + \locRlpAddrRecipe & \define & + \left[ \begin{array}{lrcl} + + & \locIsCreate & \!\!\! \cdot \!\!\! & \addressCreationRecipeConstantStd \\ + + & \locIsCreateTwo & \!\!\! \cdot \!\!\! & \addressCreationRecipeConstantTwo \\ + \end{array} \right] \vspace{2mm} \\ + \locInitCodeHashHi & \define & \locIsCreateTwo \cdot + \left[ \begin{array}{crcl} + + & \locTriggerHashInfo & \cdot & \locHashInfoKeccakHi \\ + + & (1 - \locTriggerHashInfo) & \cdot & \emptyKeccakHi \\ + \end{array} \right] \vspace{2mm} \\ + \locInitCodeHashLo & \define & \locIsCreateTwo \cdot + \left[ \begin{array}{crcl} + + & \locTriggerHashInfo & \cdot & \locHashInfoKeccakLo \\ + + & (1 - \locTriggerHashInfo) & \cdot & \emptyKeccakLo \\ + \end{array} \right] \\ + \end{array} \right. \] + In other words + \begin{enumerate} + \item \If $\locIsCreateTwo = 0$ \Then + \[ + \left\{ \begin{array}{lclr} + \locInitCodeHashHi & \define & 0 & (\trash) \\ + \locInitCodeHashLo & \define & 0 & (\trash) \\ + \end{array} \right. + \] + \item \If $\locIsCreateTwo = 1$ \Then + \begin{enumerate} + \item \If $\locTriggerHashInfo = 0$ + \[ + \left\{ \begin{array}{lclr} + \locInitCodeHashHi & \define & \emptyKeccakHi & (\trash) \\ + \locInitCodeHashLo & \define & \emptyKeccakLo & (\trash) \\ + \end{array} \right. + \] + \item \If $\locTriggerHashInfo = 1$ + \[ + \left\{ \begin{array}{lclr} + \locInitCodeHashHi & \define & \locHashInfoKeccakHi & (\trash) \\ + \locInitCodeHashLo & \define & \locHashInfoKeccakLo & (\trash) \\ + \end{array} \right. + \] + \end{enumerate} + \end{enumerate} \saNote{} We remind the reader that section~(\ref{rlpAddr: create computation constants}) defines two nonzero constants $\addressCreationRecipeConstantStd$ and $\addressCreationRecipeConstantTwo$. \end{description} \saNote{} The \zkEvm{} thus loads the account whose address corresponds to $I_\text{a}$ in the \cite{EYP}. diff --git a/hub/instruction_handling/create/shorthands.tex b/hub/instruction_handling/create/shorthands.tex index 606c3f0..5361168 100644 --- a/hub/instruction_handling/create/shorthands.tex +++ b/hub/instruction_handling/create/shorthands.tex @@ -2,28 +2,28 @@ \[ \hspace*{-2.3cm} \left\{ \begin{array}{lcl} - \locInst & \define & \stackInst _{i - \createFirstStackRowOffset} \\ - \locIsCreate & \define & \decFlag{1} _{i - \createFirstStackRowOffset} \\ - \locIsCreateTwo & \define & \decFlag{2} _{i - \createFirstStackRowOffset} \\ - \locStaticx & \define & \stackStaticx _{i - \createFirstStackRowOffset} \\ - \locMxpx & \define & \stackMxpx _{i - \createFirstStackRowOffset} \\ - \locOogx & \define & \stackOogx _{i - \createFirstStackRowOffset} \\ - \locOffsetHi & \define & \stackItemValHi{1} _{i - \createFirstStackRowOffset} \\ - \locOffsetLo & \define & \stackItemValLo{1} _{i - \createFirstStackRowOffset} \\ - \locSizeHi & \define & \stackItemValHi{2} _{i - \createFirstStackRowOffset} \\ - \locSizeLo & \define & \stackItemValLo{2} _{i - \createFirstStackRowOffset} \\ - \locCnWillRevert & \define & \cnWillRev _{i - \createFirstStackRowOffset} \\ - \locCnRevertStamp & \define & \cnRevStamp _{i - \createFirstStackRowOffset} \\ - \locInitCodeHashHi & \define & \stackHashInfoValHi _{i - \createFirstStackRowOffset} \\ - \locInitCodeHashLo & \define & \stackHashInfoValLo _{i - \createFirstStackRowOffset} \\ - \locInitCodeSize & \define & \stackItemValLo{2} _{i - \createFirstStackRowOffset} \\ % TODO: make sure this is doesn't fuck things up + \locInst & \define & \stackInst _{i - \createFirstStackRowOffset} \\ + \locIsCreate & \define & \decFlag{1} _{i - \createFirstStackRowOffset} \\ + \locIsCreateTwo & \define & \decFlag{2} _{i - \createFirstStackRowOffset} \\ + \locStaticx & \define & \stackStaticx _{i - \createFirstStackRowOffset} \\ + \locMxpx & \define & \stackMxpx _{i - \createFirstStackRowOffset} \\ + \locOogx & \define & \stackOogx _{i - \createFirstStackRowOffset} \\ + \locOffsetHi & \define & \stackItemValHi{1} _{i - \createFirstStackRowOffset} \\ + \locOffsetLo & \define & \stackItemValLo{1} _{i - \createFirstStackRowOffset} \\ + \locSizeHi & \define & \stackItemValHi{2} _{i - \createFirstStackRowOffset} \\ + \locSizeLo & \define & \stackItemValLo{2} _{i - \createFirstStackRowOffset} \\ + \locCnWillRevert & \define & \cnWillRev _{i - \createFirstStackRowOffset} \\ + \locCnRevertStamp & \define & \cnRevStamp _{i - \createFirstStackRowOffset} \\ + \locHashInfoKeccakHi & \define & \stackHashInfoValHi _{i - \createFirstStackRowOffset} \\ + \locHashInfoKeccakLo & \define & \stackHashInfoValLo _{i - \createFirstStackRowOffset} \\ + \locInitCodeSize & \define & \stackItemValLo{2} _{i - \createFirstStackRowOffset} \\ % TODO: make sure this is doesn't fuck things up % - \locSaltHi & \define & \stackItemValHi{2} _{i - \createSecondStackRowOffset} \\ - \locSaltLo & \define & \stackItemValLo{2} _{i - \createSecondStackRowOffset} \\ - \locValueHi & \define & \stackItemValHi{3} _{i - \createSecondStackRowOffset} \\ - \locValueLo & \define & \stackItemValLo{3} _{i - \createSecondStackRowOffset} \\ - \locOutputHi & \define & \stackItemValHi{4} _{i - \createSecondStackRowOffset} \\ - \locOutputLo & \define & \stackItemValLo{4} _{i - \createSecondStackRowOffset} \\ + \locSaltHi & \define & \stackItemValHi{2} _{i - \createSecondStackRowOffset} \\ + \locSaltLo & \define & \stackItemValLo{2} _{i - \createSecondStackRowOffset} \\ + \locValueHi & \define & \stackItemValHi{3} _{i - \createSecondStackRowOffset} \\ + \locValueLo & \define & \stackItemValLo{3} _{i - \createSecondStackRowOffset} \\ + \locOutputHi & \define & \stackItemValHi{4} _{i - \createSecondStackRowOffset} \\ + \locOutputLo & \define & \stackItemValLo{4} _{i - \createSecondStackRowOffset} \\ \end{array} \right. \quad\text{and}\quad \left\{ \begin{array}{lcl} From 654bd278021296cdb33ded33479b6421d1f7adf7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Mon, 9 Dec 2024 13:06:17 +0700 Subject: [PATCH 4/9] fix: TXN instrutions write the result to the stack only if unexceptional (#26) --- hub/instruction_handling/_inputs.tex | 2 +- hub/instruction_handling/txn.tex | 62 ------------------- hub/instruction_handling/txn/_inputs.tex | 5 ++ hub/instruction_handling/txn/_local.tex | 4 ++ hub/instruction_handling/txn/constraints.tex | 44 +++++++++++++ hub/instruction_handling/txn/instructions.tex | 9 +++ hub/instruction_handling/txn/shorthands.tex | 7 +++ 7 files changed, 70 insertions(+), 63 deletions(-) delete mode 100644 hub/instruction_handling/txn.tex create mode 100644 hub/instruction_handling/txn/_inputs.tex create mode 100644 hub/instruction_handling/txn/_local.tex create mode 100644 hub/instruction_handling/txn/constraints.tex create mode 100644 hub/instruction_handling/txn/instructions.tex create mode 100644 hub/instruction_handling/txn/shorthands.tex diff --git a/hub/instruction_handling/_inputs.tex b/hub/instruction_handling/_inputs.tex index a44377e..da0f3ee 100644 --- a/hub/instruction_handling/_inputs.tex +++ b/hub/instruction_handling/_inputs.tex @@ -16,7 +16,7 @@ \subsection{Instructions raising the $\stackDecKecFlag$ \lispDone{}} \subsection{Instructions raising the $\stackDecConFlag$ \lispDone{}} \label{hub: instruction handling: con} \input{instruction_handling/context/_inputs} \subsection{Instructions raising the $\stackDecAccFlag$ \lispDone{}} \label{hub: instruction handling: acc} \input{instruction_handling/account/_inputs} \subsection{Instructions raising the $\stackDecCopyFlag$ \lispDone{}} \label{hub: instruction handling: copy} \input{instruction_handling/copy/_inputs} -\subsection{Instructions raising the $\stackDecTxnFlag$ \lispDone{}} \label{hub: instruction handling: txn} \input{instruction_handling/txn} +\subsection{Instructions raising the $\stackDecTxnFlag$ \lispDone{}} \label{hub: instruction handling: txn} \input{instruction_handling/txn/_inputs} \subsection{Instructions raising the $\stackDecBtcFlag$ \lispDone{}} \label{hub: instruction handling: btc} \input{instruction_handling/btc} \subsection{Instructions raising the $\stackDecStackRamFlag$ \lispDone{}} \label{hub: instruction handling: stackRam} \input{instruction_handling/stack_ram/_inputs} \subsection{Instructions raising the $\stackDecStoFlag$ \lispDone{}} \label{hub: instruction handling: sto} \input{instruction_handling/storage/_inputs} diff --git a/hub/instruction_handling/txn.tex b/hub/instruction_handling/txn.tex deleted file mode 100644 index f902520..0000000 --- a/hub/instruction_handling/txn.tex +++ /dev/null @@ -1,62 +0,0 @@ -\subsubsection{Supported instructions and flags} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -\[ -\begin{array}{|l||c||c|c|} - \hline - \INST & \tli & \stackDecTxnFlag & \decFlag{1} \\ \hline\hline - \inst{ORIGIN} & \zero & \oneCell & \zero \\ \hline - \inst{GASPRICE} & \zero & \oneCell & \oneCell \\ \hline -\end{array} -\] -\saNote{} $\decFlag{1}$ distinguishes between the two instructions raising the $\stackDecTxnFlag$ flag. - - - -\subsubsection{Constraints} -%%%%%%%%%%%%%%%%%%%%%%%%%%% -\def\locTxnRow{\yellowm{1}} -\def\locConRow{\orangem{2}} -\begin{center} - \boxed{% - \text{The stack constraints presented below assume } - \begin{cases} - \peekStack_{i} = 1 \\ - \stackDecTxnFlag_{i} = 1 \\ - \stackSux_{i} + \stackSox_{i} = 0 \\ - \end{cases}} -\end{center} -We impose the following constraints: -\begin{description} - \item[\underline{Setting the stack pattern:}] we impose $\zeroOneSP_{i}$; - \item[\underline{Setting $\nonStackRows$:}] we impose $\nonStackRows_{i} = 1 + \cmc_{i}$; - \item[\underline{Setting the peeking flags:}] we impose - \[ - \left[ \begin{array}{lrcl} - + & \peekTransaction _{i + \locTxnRow} \\ - + & \peekContext _{i + \locConRow} & \!\!\!\cdot\!\!\! & \cmc_{i} \\ - \end{array} \right] - = - \nonStackRows_{i} - \] - \item[\underline{Setting the gas cost:}] we impose that $\gasCost_{i} = \decStaticGas_{i}$; - \item[\underline{Value constraints:}] --- %\If $\cmc_{i} = 0$ \Then - \begin{enumerate} - \item \If $\decFlag{1}_{i} = 0$\footnote{i.e. $\INST_{i} = \inst{ORIGIN}$} \Then - \[ - \left\{ \begin{array}{lcl} - \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & \txFrom\high_{i + \locTxnRow} \\ - \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txFrom\low_{i + \locTxnRow} \\ - \end{array} \right. - \] - \item \If $\decFlag{1}_{i} = 1$\footnote{i.e. $\INST_{i} = \inst{GASPRICE}$} \Then - \[ - \left\{ \begin{array}{lcl} - \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & 0 \\ - \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txGasPrice_{i + \locTxnRow} \\ - \end{array} \right. - \] - \end{enumerate} -\end{description} -\saNote{} For instructions raising the $\stackDecTxnFlag$ one has $\cmc = \xAhoy$. diff --git a/hub/instruction_handling/txn/_inputs.tex b/hub/instruction_handling/txn/_inputs.tex new file mode 100644 index 0000000..9e1736f --- /dev/null +++ b/hub/instruction_handling/txn/_inputs.tex @@ -0,0 +1,5 @@ +\input{instruction_handling/txn/_local} +\subsubsection{Supported instructions and flags} \label{hub: instruction handling: txn: instructions} \input{instruction_handling/txn/instructions} +\subsubsection{Shorthands \lispDone{}} \label{hub: instruction handling: txn: shorthands} \input{instruction_handling/txn/shorthands} +\subsubsection{Constraints \lispDone{}} \label{hub: instruction handling: txn: constraints} \input{instruction_handling/txn/constraints} + diff --git a/hub/instruction_handling/txn/_local.tex b/hub/instruction_handling/txn/_local.tex new file mode 100644 index 0000000..0b40b80 --- /dev/null +++ b/hub/instruction_handling/txn/_local.tex @@ -0,0 +1,4 @@ +\def\locTxnRow {\yellowm{1}} +\def\locConRow {\orangem{2}} +\def\locIsOrigin {\col{is\_ORIGIN}} +\def\locIsGasPrice {\col{is\_GASPRICE}} diff --git a/hub/instruction_handling/txn/constraints.tex b/hub/instruction_handling/txn/constraints.tex new file mode 100644 index 0000000..77a6757 --- /dev/null +++ b/hub/instruction_handling/txn/constraints.tex @@ -0,0 +1,44 @@ +\begin{center} + \boxed{% + \text{The stack constraints presented below assume } + \begin{cases} + \peekStack _{i} = 1 \\ + \stackDecTxnFlag _{i} = 1 \\ + \stackSux _{i} + \stackSox _{i} = 0 \\ + \end{cases}} +\end{center} +We impose the following constraints: +\begin{description} + \item[\underline{Setting the stack pattern:}] we impose $\zeroOneSP_{i}$; + \item[\underline{Setting $\nonStackRows$:}] we impose $\nonStackRows_{i} = 1 + \cmc_{i}$; + \item[\underline{Setting the peeking flags:}] we impose + \[ + \left[ \begin{array}{lrcl} + + & \peekTransaction _{i + \locTxnRow} \\ + + & \peekContext _{i + \locConRow} & \!\!\!\cdot\!\!\! & \cmc_{i} \\ + \end{array} \right] + = + \nonStackRows_{i} + \] + \item[\underline{Setting the gas cost:}] we impose that $\gasCost_{i} = \decStaticGas_{i}$; + \item[\underline{Value constraints:}] + \If $\xAhoy _{i} = 0$ \Then we impose that + \begin{enumerate} + \item \If $\locIsOrigin = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & \txFrom\high_{i + \locTxnRow} \\ + \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txFrom\low_{i + \locTxnRow} \\ + \end{array} \right. + \] + \item \If $\locIsGasPrice = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \stackItemValHi{4}_{i} & \!\!\! = \!\!\! & 0 \\ + \stackItemValLo{4}_{i} & \!\!\! = \!\!\! & \txGasPrice_{i + \locTxnRow} \\ + \end{array} \right. + \] + \end{enumerate} +\end{description} +\saNote{} +For instructions raising the $\stackDecTxnFlag$ one has $\cmc = \xAhoy$. diff --git a/hub/instruction_handling/txn/instructions.tex b/hub/instruction_handling/txn/instructions.tex new file mode 100644 index 0000000..4ee588f --- /dev/null +++ b/hub/instruction_handling/txn/instructions.tex @@ -0,0 +1,9 @@ +\[ + \begin{array}{|l||c||c|c|c|} + \hline + \INST & \tli & \stackDecTxnFlag & \decFlag{1} & \decFlag{2} \\ \hline\hline + \inst{ORIGIN} & \zero & \oneCell & \oneCell & \zero \\ \hline + \inst{GASPRICE} & \zero & \oneCell & \zero & \oneCell \\ \hline + \end{array} +\] + diff --git a/hub/instruction_handling/txn/shorthands.tex b/hub/instruction_handling/txn/shorthands.tex new file mode 100644 index 0000000..304abca --- /dev/null +++ b/hub/instruction_handling/txn/shorthands.tex @@ -0,0 +1,7 @@ +We further introduce the following shorthands +\[ + \left\{ \begin{array}{lcl} + \locIsOrigin & \define & \decFlag {1} _{i} \\ + \locIsGasPrice & \define & \decFlag {2} _{i} \\ + \end{array} \right. +\] From 280e984ec2156ff2d39dddcad927d49d26d585cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Mon, 9 Dec 2024 22:00:53 +0700 Subject: [PATCH 5/9] New scenario/CREATE shorthand (#24) --- .../create/generalities/all.tex | 33 ++++++++++++------- .../create/triggers/table.tex | 20 +++-------- hub/scenario/shorthands/create.tex | 21 +++++++----- hub/scenario/tables/create.tex | 1 + pkg/scenario.sty | 1 + 5 files changed, 40 insertions(+), 36 deletions(-) diff --git a/hub/instruction_handling/create/generalities/all.tex b/hub/instruction_handling/create/generalities/all.tex index bcbcf3b..00a4a8f 100644 --- a/hub/instruction_handling/create/generalities/all.tex +++ b/hub/instruction_handling/create/generalities/all.tex @@ -115,33 +115,42 @@ we impose \If $\miscOobFlag_{i + \createMiscRowOffset} = 1$ \Then \[ \setOobInstructionCreate { - anchorRow = i, - relOffset = \createMiscRowOffset, - valueHi = \locValueHi, - valueLo = \locValueLo, - balance = \locCreatorBalance, - nonce = \locCreateeNonce, - hasCode = \locCreateeHasCode, - callStackDepth = \locCsd, - creatorNonce = \locCreatorNonce, + anchorRow = i , + relOffset = \createMiscRowOffset , + valueHi = \locValueHi , + valueLo = \locValueLo , + balance = \locCreatorBalance , + nonce = \locCreateeNonce , + hasCode = \locCreateeHasCode , + callStackDepth = \locCsd , + creatorNonce = \locCreatorNonce , } \] where we define the following shorthands: + \[ + \left\{ \begin{array}{lclcl} + \locCreateeNonce & = & \scenCreateLoadCreatee _{i} & \cdot & \accNonce _{i + \createFirstCreateeAccountRowOffset} \\ + \locCreateeHasCode & = & \scenCreateLoadCreatee _{i} & \cdot & \accHasCode _{i + \createFirstCreateeAccountRowOffset} \\ + \end{array} \right. + \] + in other words \[ \left\{ \begin{array}{lclc} - \If \locTriggerRlpAddr = 0 ~ \Then + \If \scenCreateLoadCreatee _{i} = 0 ~ \Then \left\{ \begin{array}{lclc} \locCreateeNonce & = & 0 \\ \locCreateeHasCode & = & 0 \\ \end{array} \right. \\ - \If \locTriggerRlpAddr = 1 ~ \Then + \If \scenCreateLoadCreatee _{i} = 1 ~ \Then \left\{ \begin{array}{lclc} \locCreateeNonce & = & \accNonce _{i + \createFirstCreateeAccountRowOffset} \\ \locCreateeHasCode & = & \accHasCode _{i + \createFirstCreateeAccountRowOffset} \\ \end{array} \right. \\ \end{array} \right. \] - \saNote{} We explain the conditional definitions of \locCreateeNonce{} and \locCreateeHasCode{} by the fact that the \zkEvm{} is granted access to the account of the deployment address \emph{iff} it computes that address. + \saNote{} + We explain the conditional definitions of \locCreateeNonce{} and \locCreateeHasCode{} by the fact that + the \zkEvm{} is granted access to the account of the createe \emph{iff} $\scenCreateLoadCreatee \equiv 1$. \item[\underline{Setting the \inst{CREATE}-scenario:}] we impose the following \begin{enumerate} diff --git a/hub/instruction_handling/create/triggers/table.tex b/hub/instruction_handling/create/triggers/table.tex index adcd795..dc39113 100644 --- a/hub/instruction_handling/create/triggers/table.tex +++ b/hub/instruction_handling/create/triggers/table.tex @@ -5,26 +5,14 @@ \renewcommand{\arraystretch}{1.5} \begin{array}{|l|l|c|c|c|c|c|c|c|c|c|c|c|c|} \cline{3-14} - \multicolumn{2}{c|}{} & - \createVertColStaticx & - \createVertColMxpx & - \createVertColOogx & - \columnCreateB & - \columnCreateD & - \columnCreateC & - \columnCreateF & - \columnCreateE & - \columnCreateH & - \columnCreateG & - \columnCreateJ & - \columnCreateI \\ \cline{2-14} + \multicolumn{2}{c|}{} & \createVertColStaticx & \createVertColMxpx & \createVertColOogx & \columnCreateB & \columnCreateD & \columnCreateC & \columnCreateF & \columnCreateE & \columnCreateH & \columnCreateG & \columnCreateJ & \columnCreateI \\ \cline{2-14} \multicolumn{1}{c|}{} &  \locTriggerMxp & \rCross & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark \\ \cline{2-14} \multicolumn{1}{c|}{} &  \locTriggerStp & \rCross & \rCross & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark \\ \cline{2-14} \multicolumn{1}{c|}{} &  \locTriggerOob & \rCross & \rCross & \rCross & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark \\ \hline \multirow{4}{*}{\locTriggerMmu} &  \locHashInitCode & \rCross & \rCross & \rCross & \rCross & \nonemptyCreateTwo & \nonemptyCreateTwo & \rCross & \rCross & \rCross & \rCross & \rCross & \rCross \\ \cline{2-14} - &  \locHashInitCodeAndSendToRom & \rCross & \rCross & \rCross & \rCross & \rCross & \rCross & \createTwo & \createTwo & \createTwo & \createTwo & \rCross & \rCross \\ \cline{2-14} - &  \locSendInitCodeToRom & \rCross & \rCross & \rCross & \rCross & \rCross & \rCross & \createOne & \createOne & \createOne & \createOne & \rCross & \rCross \\ \cline{2-14} - &  \locTriggerMmu & \rCross & \rCross & \rCross & \rCross & \nonemptyCreateTwo & \nonemptyCreateTwo & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \rCross & \rCross \\ \hline + &  \locHashInitCodeAndSendToRom & \rCross & \rCross & \rCross & \rCross & \rCross & \rCross & \createTwo & \createTwo & \createTwo & \createTwo & \rCross & \rCross \\ \cline{2-14} + &  \locSendInitCodeToRom & \rCross & \rCross & \rCross & \rCross & \rCross & \rCross & \createOne & \createOne & \createOne & \createOne & \rCross & \rCross \\ \cline{2-14} + &  \locTriggerMmu & \rCross & \rCross & \rCross & \rCross & \nonemptyCreateTwo & \nonemptyCreateTwo & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \rCross & \rCross \\ \hline \multicolumn{1}{c|}{} &  \locTriggerRlpAddr & \rCross & \rCross & \rCross & \rCross & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark \\ \cline{2-14} \multicolumn{1}{c|}{} &  \locTriggerHashInfo & \rCross & \rCross & \rCross & \rCross & \nonemptyCreateTwo & \nonemptyCreateTwo & \createTwo & \createTwo & \createTwo & \createTwo & \rCross & \rCross \\ \cline{2-14} \multicolumn{1}{c|}{} &  \locTriggerRomLex & \rCross & \rCross & \rCross & \rCross & \rCross & \rCross & \gCheckMark & \gCheckMark & \gCheckMark & \gCheckMark & \rCross & \rCross \\ \cline{2-14} diff --git a/hub/scenario/shorthands/create.tex b/hub/scenario/shorthands/create.tex index 9d3aa6f..1b1a85f 100644 --- a/hub/scenario/shorthands/create.tex +++ b/hub/scenario/shorthands/create.tex @@ -83,15 +83,20 @@ \end{array} \right] \end{array} \right. \] -and +and the following two equivalent shorthands which we nonetheless give two different names \[ - \scenCreateComputeAddress_{i} \define - \left[ \begin{array}{l} - % + \scenCreateException _{i} \\ - % + \scenCreateAbort _{i} \\ - + \scenCreateFCond _{i} \\ - + \scenCreateExecution _{i} \\ - \end{array} \right] + \left\{ \begin{array}{lcl} + \scenCreateComputeAddress _{i} & \define & + \left[ \begin{array}{l} + + \scenCreateFCond _{i} \\ + + \scenCreateExecution _{i} \\ + \end{array} \right] \vspace{2mm} \\ + \scenCreateLoadCreatee _{i} & \define & + \left[ \begin{array}{l} + + \scenCreateFCond _{i} \\ + + \scenCreateExecution _{i} \\ + \end{array} \right] \\ + \end{array} \right. \] and \[ diff --git a/hub/scenario/tables/create.tex b/hub/scenario/tables/create.tex index e4deefb..2c32cd8 100644 --- a/hub/scenario/tables/create.tex +++ b/hub/scenario/tables/create.tex @@ -18,5 +18,6 @@ \scenCreateSimpleRevert & \rC & \rC & \gCM & \rC & \rC & \rC & \gCM & \rC & \gCM & \rC \\ \hline \scenCreateNoContextChange & \rC & \gCM & \gCM & \gCM & \rC & \rC & \rC & \rC & \gCM & \gCM \\ \hline \scenCreateComputeAddress & \rC & \rC & \gCM & \gCM & \gCM & \gCM & \gCM & \gCM & \gCM & \gCM \\ \hline + \scenCreateLoadCreatee & \rC & \rC & \gCM & \gCM & \gCM & \gCM & \gCM & \gCM & \gCM & \gCM \\ \hline \end{array} \] diff --git a/pkg/scenario.sty b/pkg/scenario.sty index ba24861..1db4e05 100644 --- a/pkg/scenario.sty +++ b/pkg/scenario.sty @@ -203,6 +203,7 @@ \newcommand{\scenCreateNoContextChange} {\scenCreateColumn{no\_context\_change}} \newcommand{\scenCreateUnexceptional} {\scenCreateColumn{unexceptional}} \newcommand{\scenCreateComputeAddress} {\scenCreateColumn{compute\_deployment\_address}} +\newcommand{\scenCreateLoadCreatee} {\scenCreateColumn{load\_createe\_account}} \newcommand{\scenCreateFCond} {\scenCreateColumn{failure\_condition}} \newcommand{\scenCreateWillRevert} {\scenCreateColumn{will\_revert}} \newcommand{\scenCreateNoCreatorStateChange} {\scenCreateColumn{no\_creator\_state\_change}} From a76fb7697b9430f07bfa372178f37bdf2d07e657 Mon Sep 17 00:00:00 2001 From: Pavel Zaborskii Date: Mon, 9 Dec 2024 16:03:45 +0100 Subject: [PATCH 6/9] docs: refine terminology and clarify procedural details (#13) --- hub/columns/storage.tex | 2 +- hub/consistencies/context/constraints.tex | 2 +- log_info/lookups/log_info_into_rlp_log.tex | 2 +- notes/stipend.md | 2 +- pkg/env.sty | 4 ++-- txn_data/lookups.md | 2 +- 6 files changed, 7 insertions(+), 7 deletions(-) diff --git a/hub/columns/storage.tex b/hub/columns/storage.tex index 830f1f3..e580748 100644 --- a/hub/columns/storage.tex +++ b/hub/columns/storage.tex @@ -23,7 +23,7 @@ $\stoNextValueIsOrig$: binary columns whose purpose is to streamline the computation of gas costs of \inst{SSTORE} instructions. \end{enumerate} -The desired interpretation is straightfoward: +The desired interpretation is straightforward: \[ \left\{ \begin{array}{lclclcl} \stoOrigValueIsZero & \!\!\! = \!\!\! & 1 & \iff & \stoOrigValue & \!\!\! = \!\!\! & 0 \\ diff --git a/hub/consistencies/context/constraints.tex b/hub/consistencies/context/constraints.tex index 49c1cda..09ff052 100644 --- a/hub/consistencies/context/constraints.tex +++ b/hub/consistencies/context/constraints.tex @@ -79,7 +79,7 @@ Observe that whenever the \zkEvm{} spawns a new execution context it does so with $\cn \equiv \hubStamp$\footnote{And this may only happen in the \textbf{initialization phase} of a transaction, -when transfering transaction call data to a designated, fresh new execution context's \textsc{ram}; +when transferring transaction call data to a designated, fresh new execution context's \textsc{ram}; see section~(\ref{hub: initialization phase: transaction call data copy}) for details.} or $\cn \equiv 1 + \hubStamp$ where moreover $\hubStamp > 0$. diff --git a/log_info/lookups/log_info_into_rlp_log.tex b/log_info/lookups/log_info_into_rlp_log.tex index 06a314a..1f3a83f 100644 --- a/log_info/lookups/log_info_into_rlp_log.tex +++ b/log_info/lookups/log_info_into_rlp_log.tex @@ -1,4 +1,4 @@ -We describe the lookup transfering \emph{verticalized} data from the current module to the \rlpTxnRcptMod{} module. +We describe the lookup transferring \emph{verticalized} data from the current module to the \rlpTxnRcptMod{} module. \begin{description} \item[\underline{Selector:}] none. \item[\underline{Source columns:}] from the \logInfoMod{} module: diff --git a/notes/stipend.md b/notes/stipend.md index f5e24ad..2a44b4f 100644 --- a/notes/stipend.md +++ b/notes/stipend.md @@ -108,7 +108,7 @@ There must be the following: For COUNTER there are two options: -- either have a very specific behaviour, e.g. COUNTER: 0, 1, 2, 3 or 0, 1, 2 or just 0, 1 depending on CALL transfering value, CALL not transfering value or CREATE +- either have a very specific behaviour, e.g. COUNTER: 0, 1, 2, 3 or 0, 1, 2 or just 0, 1 depending on CALL transferring value, CALL not transferring value or CREATE - either have generic behaviour: COUNTER: 0, 1, 2, 3 _always_ <--- likely the best option Have some "counter-constancy" constraints on columns imported from the HUB: diff --git a/pkg/env.sty b/pkg/env.sty index a54abf9..88f994a 100644 --- a/pkg/env.sty +++ b/pkg/env.sty @@ -433,8 +433,8 @@ \newcommand{\firstRowOfNewContext} [2] {\texttt{firstRowOfNewContext} _{#1} \big[\, #2 \,\big]} \newcommand{\precompileScenarioRow} [2] {\texttt{precompileScenarioRow} _{#1} \big[\, #2 \,\big]} % -\newcommand{\unsuccessfulCall} {\texttt{unsucessfulCall}} -\newcommand{\successfulCall} {\texttt{sucessfulCall}} +\newcommand{\unsuccessfulCall} {\texttt{unsuccessfulCall}} +\newcommand{\successfulCall} {\texttt{successfulCall}} % \newcommand{\CONTEXTMAYCHANGE} {\col{CONTEXT\_MAY\_CHANGE}} \newcommand{\cmc} {\col{CMC}\flag} diff --git a/txn_data/lookups.md b/txn_data/lookups.md index e7af5e2..bb43d8f 100644 --- a/txn_data/lookups.md +++ b/txn_data/lookups.md @@ -266,7 +266,7 @@ Simple bilateral lookup to prove the prewarming of all [addresses, storage key] The TX_RLP and TX_DATA modules must be augmented slightly: - TX_DATA: - we need redundancy to reduce the number of lookups - - we need a REQURIES_EVM_EXECUTION binary column (which is justified in the hub) + - we need a REQUIRES_EVM_EXECUTION binary column (which is justified in the hub) - we should do the gas price computations (for Type 2 transactions) here - TX_RLP: - we require a transaction-constant binary column REQUIRES_EVM_EXECUTION which is justified in TX_DATA From df7eb19eaf739c125ca91bf1826ac8ff9baaf953 Mon Sep 17 00:00:00 2001 From: Anonim Date: Mon, 9 Dec 2024 18:05:21 +0300 Subject: [PATCH 7/9] fix: Correct description lines of the code (#20) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com> --- hub/generalities/context/intro.tex | 2 +- hub/heartbeat/execution_required.tex | 2 +- .../call/precompiles/ecadd_ecmul_ecpairing/empty.tex | 2 +- hub/instruction_handling/call/precompiles/modexp/success.tex | 2 +- notes/stipend.md | 2 +- oob/precompiles/common/generalities.tex | 2 +- pkg/IEEEtrantools.sty | 2 +- prc/blkmdx/columns.tex | 2 +- rlp_addr/intro.tex | 2 +- rlp_txn/generalities/constancies.tex | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) diff --git a/hub/generalities/context/intro.tex b/hub/generalities/context/intro.tex index e49f1c5..bd6e71e 100644 --- a/hub/generalities/context/intro.tex +++ b/hub/generalities/context/intro.tex @@ -20,7 +20,7 @@ This happens whenever the current instruction is either (\emph{c}) of \textbf{\inst{CALL}-type} or (\emph{d}) of \textbf{\inst{CREATE}-type}. -Determining when a context change may happen is therfore comparatively easy. +Determining when a context change may happen is therefore comparatively easy. This is the purpose of the \cmc{}. \saNote{} Whenever the execution context \emph{may change} the \zkEvm{} \textbf{must} perform various sanity checks (such as making sure that its gas supply pre-opcode is nonnegative.) diff --git a/hub/heartbeat/execution_required.tex b/hub/heartbeat/execution_required.tex index e344ec9..5e4ae13 100644 --- a/hub/heartbeat/execution_required.tex +++ b/hub/heartbeat/execution_required.tex @@ -1,4 +1,4 @@ -We explain the remaing cases i.e. those cases where \evm{} execution is required. These are: +We explain the remaining cases i.e. those cases where \evm{} execution is required. These are: \begin{itemize} \item the transaction is a \textbf{message call} and the recipient account has \textbf{nonempty byte code}; \item the transaction is a \textbf{contract deployment} with \textbf{nonempty initialization code}; diff --git a/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/empty.tex b/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/empty.tex index 6378fab..2934392 100644 --- a/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/empty.tex +++ b/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/empty.tex @@ -48,7 +48,7 @@ \end{enumerate} the first one is interpreted as the zero integer $\in \mathbb{N}_{256}$; the second one is interpreted, by \evm{} convention and as already explained, as the \textbf{point at infinity} on the \texttt{altbn} curve; - this input data is therfore well-formed and cannot trigger $\scenPrcFailureKnownToRam$; + this input data is therefore well-formed and cannot trigger $\scenPrcFailureKnownToRam$; furthermore, the return data is (the \evm{} encoding of) the point at infinity $ \utt{00} \; diff --git a/hub/instruction_handling/call/precompiles/modexp/success.tex b/hub/instruction_handling/call/precompiles/modexp/success.tex index be1d4fe..e4799b4 100644 --- a/hub/instruction_handling/call/precompiles/modexp/success.tex +++ b/hub/instruction_handling/call/precompiles/modexp/success.tex @@ -15,7 +15,7 @@ (\emph{b}) potentially extract the exponent (\emph{c}) potentially extract the modulus (\emph{d}) potentially transfer the output of the precompile to a dedicated execution context's \textsc{ram} -(\emph{e}) potentially copy part of the ouput to the current exeuction context's \textsc{ram}. +(\emph{e}) potentially copy part of the output to the current exeuction context's \textsc{ram}. \begin{description} \item[\underline{\underline{Miscellaneous row $n^°(i + \prcModexpSuccessExtractBaseRowOffset)$:}}] the \zkEvm{} triggers the \oobMod{} instruction \oobInstModexpExtract{}; diff --git a/notes/stipend.md b/notes/stipend.md index 2a44b4f..b854c4b 100644 --- a/notes/stipend.md +++ b/notes/stipend.md @@ -139,7 +139,7 @@ We can have some columns that contain the contents of things to look-up else whe The idea would be that one has - WCP_SELECTOR * EXT_SELECTOR = 0 - If STAMP = 0 Then WCP_SELECTOR + MOD_SELECTOR = 0 (i.e. both are zero) -- If WCP_SELECTOR = 1 Then LOOKUP_INST $\in$ { LT, ISZERO } (i.E. we can only request LT and ISZERO instuctions) +- If WCP_SELECTOR = 1 Then LOOKUP_INST $\in$ { LT, ISZERO } (i.E. we can only request LT and ISZERO instructions) - If MOD_SELECTOR = 1 Then LOOKUP_INST = DIV (i.e. we can only request the DIV from MOD) ### CREATE workflow diff --git a/oob/precompiles/common/generalities.tex b/oob/precompiles/common/generalities.tex index 1940a89..3c141b2 100644 --- a/oob/precompiles/common/generalities.tex +++ b/oob/precompiles/common/generalities.tex @@ -53,6 +53,6 @@ Note that at this stage the conditions that trigger $\locHubSuccess \equiv 1$ aren't set. Neither is it clear that \locHubSuccess{} is binary. \end{description} -We remind the reader that the remaing objectives of the \oobMod{} module in this particular case are to perform the following tasks +We remind the reader that the remaining objectives of the \oobMod{} module in this particular case are to perform the following tasks \green{(\emph{a})} compare the call gas to the (constant) cost of these precompiles thus justifying the \locHubSuccess{} (In case of \inst{ECPAIRING} a congruence must also be checked) \green{(\emph{b})} compute the \locReturnGas{}. diff --git a/pkg/IEEEtrantools.sty b/pkg/IEEEtrantools.sty index e4a808c..187237c 100644 --- a/pkg/IEEEtrantools.sty +++ b/pkg/IEEEtrantools.sty @@ -2483,7 +2483,7 @@ in the IEEEeqnarray column specifications.}% \toks0={##}% % make preamble advance col counter if this environment needs this \if@advanceIEEEeqncolcnt\@IEEEappendtoksA{\global\advance\@IEEEeqncolcnt by 1\relax}\fi -% insert the column defintion into the preamble, being careful not to expand +% insert the column definition into the preamble, being careful not to expand % the column definition \@IEEEappendtoksA{\tabskip=\@IEEEBPcurglue}% \@IEEEappendNOEXPANDtoksA{\begingroup\csname @IEEEeqnarraycolPRE}% diff --git a/prc/blkmdx/columns.tex b/prc/blkmdx/columns.tex index d61a279..e2155a6 100644 --- a/prc/blkmdx/columns.tex +++ b/prc/blkmdx/columns.tex @@ -22,7 +22,7 @@ The following column is a ``limb'' which contains limbs (i.e. $\llarge$-byte integers) representing data. This data may be either input data (\inst{MODEXP} base, exponent or modulus, \inst{BLAKE2f} ``\col{rounds}'' and ``\col{f}'' parameters and \col{h}, \col{m} and \col{t} parameters) -or ouput data +or output data (\inst{MODEXP} result or \inst{BLAKE2f} result.) \begin{enumerate}[resume] \item \limb{}: diff --git a/rlp_addr/intro.tex b/rlp_addr/intro.tex index 3846115..fb5c2e8 100644 --- a/rlp_addr/intro.tex +++ b/rlp_addr/intro.tex @@ -14,4 +14,4 @@ \zeta \cdot h \] -In applications this method is used by the \inst{CREATE2} opcode: the address $s$ is that of the creator account, $\zeta$ (the ``salt'') is a stack argument and $h = \texttt{KECCAK}(\textbf{i})$ is the hash of the initalization code $\textbf{i}$. +In applications this method is used by the \inst{CREATE2} opcode: the address $s$ is that of the creator account, $\zeta$ (the ``salt'') is a stack argument and $h = \texttt{KECCAK}(\textbf{i})$ is the hash of the initialization code $\textbf{i}$. diff --git a/rlp_txn/generalities/constancies.tex b/rlp_txn/generalities/constancies.tex index 653b2e9..eca449a 100644 --- a/rlp_txn/generalities/constancies.tex +++ b/rlp_txn/generalities/constancies.tex @@ -33,7 +33,7 @@ \item $\absTxNumInfty$ is block-constant. \end{enumerate} We draw the attention of the reader to the fact that the following constraints hold by construction of the relevant columns. -There is therfore no reason to explictly include the following constraints in the implementation. +There is therefore no reason to explicitly include the following constraints in the implementation. \begin{enumerate}[resume] \item $\ispadding$ is $\phaseRlpPrefix$-decrementing; \quad (\trash) \item $\done$ and $\accsize$ are $\ct$-incrementing; \quad (\trash) From a30335863e62c143ba20b9df5341f5781bf2cfbb Mon Sep 17 00:00:00 2001 From: antews Date: Mon, 9 Dec 2024 16:06:26 +0100 Subject: [PATCH 8/9] fix: correct multiple typos around files (#25) --- hub/generalities/gas/constraints.tex | 4 ++-- .../ramToRamSansPadding/micro_instruction_writing.tex | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/hub/generalities/gas/constraints.tex b/hub/generalities/gas/constraints.tex index 83f45a0..0184858 100644 --- a/hub/generalities/gas/constraints.tex +++ b/hub/generalities/gas/constraints.tex @@ -43,7 +43,7 @@ The gas cost of an instruction matters to the present arithmetization \emph{if and only if} it is either unexceptional or raises an \oogxSH{} in the arithmetization. For exceptional instructions the \zkEvm{} sets the next gas value to $0$. -For (most) unexceptional instructions the next value of gas is (unsurprisingly) obtained by substracting the gas cost from the currently avaialble gas. +For (most) unexceptional instructions the next value of gas is (unsurprisingly) obtained by subtracting the gas cost from the currently available gas. However, pricing is special for \inst{CALL}-type and \inst{CREATE}-type instructions and we defer to the relevant instruction handling section. \begin{enumerate}[resume] \item \If @@ -70,6 +70,6 @@ \end{enumerate} Some details: (\ref{hub: generalities: gas: resuming execution gas constraint}) asserts that when an execution context reaches its conclusion (as witnessed by $\cn\new_{i} = \caller_{i}$) the $\gasNext$ column on that row must contain the left over gas in the present context. -We are unable to settle the ``call gas'' or ``create gas'' provided to a child context spawned through a \inst{CREATE}-type or \inst{CALL}-type instruction at this level of generatlity, whence the \relevantValue{} in constraint~(\ref{hub: generalities: gas: spawning new context}). It is a complex question and will be settled when we deal with the processing of those instruction families. +We are unable to settle the ``call gas'' or ``create gas'' provided to a child context spawned through a \inst{CREATE}-type or \inst{CALL}-type instruction at this level of generality, whence the \relevantValue{} in constraint~(\ref{hub: generalities: gas: spawning new context}). It is a complex question and will be settled when we deal with the processing of those instruction families. \issue{Constraint~(\ref{hub: generalities: gas: could blow up}) could blow up if we don't handle precompiles, pure transfers and deployments with empty code correctly.} diff --git a/mmu/instructions/ramToRamSansPadding/micro_instruction_writing.tex b/mmu/instructions/ramToRamSansPadding/micro_instruction_writing.tex index b75bd1d..8314e5c 100644 --- a/mmu/instructions/ramToRamSansPadding/micro_instruction_writing.tex +++ b/mmu/instructions/ramToRamSansPadding/micro_instruction_writing.tex @@ -1,5 +1,5 @@ \begin{center} - \boxed{ \text{The constriants presented below assumes that } \mmuInstFlagRamToRamSansPadding _{i} = 1. } + \boxed{ \text{The constraints presented below assumes that } \mmuInstFlagRamToRamSansPadding _{i} = 1. } \end{center} \begin{description} \item[\underline{Progression:}] From 021cd1de4247676af960f3ef4d7fd0bdb641beee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Mon, 9 Dec 2024 22:17:13 +0700 Subject: [PATCH 9/9] fix: mix-up in order of operands for partialCopyOfResults for EC precompiles (#27) --- .../call/precompiles/ecadd_ecmul_ecpairing/success.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/success.tex b/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/success.tex index ff2935f..17b1684 100644 --- a/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/success.tex +++ b/hub/instruction_handling/call/precompiles/ecadd_ecmul_ecpairing/success.tex @@ -272,10 +272,10 @@ relOffset = \prcStandardSuccessThirdMiscRowOffset , sourceId = 1 + \hubStamp_{i} , targetId = \cn_{i} , - sourceOffsetLo = \locPrcRao , - size = \locPrcRac , - referenceOffset = 0 , - referenceSize = \undefinedStar \quad \locMmuRefSize , + sourceOffsetLo = 0 , + size = \undefinedStar \quad \locMmuRefSize , + referenceOffset = \locPrcRao , + referenceSize = \locPrcRac , } % \left\{ \begin{array}{lcl} % \miscMmuInst _{i + \prcStandardSuccessThirdMiscRowOffset} & = & \mmuInstRamToRamSansPadding \\