Bugfix for GAS_NEXT of CREATE's

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           \\

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$.

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.)

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.}

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};

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}

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} \;

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 \\

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{};

hub/instruction_handling/create/_local.tex

@@ -16,10 +16,12 @@
 \def\locMxpx                                        {\col{STACK\_mxpx}}
 \def\locOogx                                        {\col{STACK\_oogx}}
 %
-\def\relevantValue                               {\texttt{<rel. val.>}}
+\def\relevantValue                                  {\texttt{<rel. val.>}}
 %
 \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}}
@@ -101,7 +103,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}}

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
@@ -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}
@@ -199,23 +208,23 @@
 		\]
 		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          \\
 						\locAuxId  & \define & 1 + \hubStamp_{i} \\
 						\locExoSum & \define & \exoWeightKec     \\
 					\end{array} \right.
 				\]
-			\item \If $\locHashInitCodeAndSendToRom = 1$ \Then 
+			\item \If $\locHashInitCodeAndSendToRom = 1$ \Then
 				\[
 					\left\{ \begin{array}{lcl}
 						\locTgtId  & \define & \locDepCfi                    \\
 						\locAuxId  & \define & 1 + \hubStamp_{i}             \\
 						\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 +243,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}