From 5f24c78492c730b459030a0190a6d54da511d70c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 28 Nov 2024 19:18:04 +0700 Subject: [PATCH 01/18] fix: TX_INIT now finishes on a context row This simplifies extracting relevant data from the transaction --- hub/heartbeat/hub_stamp.tex | 2 +- hub/heartbeat/phase_flags.tex | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/hub/heartbeat/hub_stamp.tex b/hub/heartbeat/hub_stamp.tex index cc696e8..bd0e0bc 100644 --- a/hub/heartbeat/hub_stamp.tex +++ b/hub/heartbeat/hub_stamp.tex @@ -71,7 +71,7 @@ The above enforces that $\hubStamp$ remains constant throughout the processing of any transaction which requires no \textsc{evm}-execution as well as during the initialization and finalization phases of transactions that require \evm{} execution. The \hubStamp{} furthermore will jump by one (on any one of those phases) whenever the current row peeks into the transaction. We remind the reader that for these three phases (\txSkip, \txInit{} and \txFinl{}) the $\peekTransaction{}$ flag already played a special role in the previous section, see constraints (\ref{hub: heartbeat: skipping phase finishes on a transaction row}), -(\ref{hub: heartbeat: initialization phase finishes on a transaction row}) and +(\ref{hub: heartbeat: initialization phase finishes on a context row}) and (\ref{hub: heartbeat: finalization phase finishes on a transaction row}). This column also served a special purpose with respect to the \absTxNum, see constraint (\ref{hub: heartbeat: abs tx num increments}). diff --git a/hub/heartbeat/phase_flags.tex b/hub/heartbeat/phase_flags.tex index bdd34f7..a7bd261 100644 --- a/hub/heartbeat/phase_flags.tex +++ b/hub/heartbeat/phase_flags.tex @@ -23,9 +23,9 @@ \] \begin{enumerate}[resume] \label{hub:heartbeat: tx phase sum constraints} \item \If $\absTxNum_{i} = 0$ \Then $\locTransactionPhaseSum_{i} = 0$; - \item\label{hub: heartbeat: tx phase flag exclusivity} + \item \label{hub: heartbeat: tx phase flag exclusivity} \If $\absTxNum_{i} \neq 0$ \Then $\locTransactionPhaseSum_{i} = 1$; - \item\label{hub: heartbeat: acceptable tx phases at first row of new transaction} + \item \label{hub: heartbeat: acceptable tx phases at first row of new transaction} \If $\absTxNum_{i} \neq \absTxNum_{i - 1}$ \Then $\locAcceptableTransactionPhaseFlagsAtFirstRowOfNewTransaction$; \end{enumerate} The above says that on padding rows all processing flags are off while on non-padding rows \emph{precisely} one of the processing flags flags is set. Furthermore when a new transaction starts processing it either @@ -56,14 +56,14 @@ \begin{enumerate}[resume] \item \If $\txWarm_{i} = 1$ \Then $\txWarm_{i + 1} + \txInit_{i + 1} = 1$ \item - \label{hub: heartbeat: initialization phase finishes on a transaction row} + \label{hub: heartbeat: initialization phase finishes on a context row} \If $\txInit_{i} = 1$ \Then - \[ - \begin{cases} - \If \peekTransaction_{i} = 0 ~ \Then \txInit_{i + 1} = 1 \\ - \If \peekTransaction_{i} = 1 ~ \Then \txExec_{i + 1} = 1 \\ - \end{cases} - \] + \[ + \begin{cases} + \If \peekContext _{i} = 0 ~ \Then \txInit _{i + 1} = 1 \\ + \If \peekContext _{i} = 1 ~ \Then \txExec _{i + 1} = 1 \\ + \end{cases} + \] \item \If $\txExec_{i} = 1$ \Then $\txExec_{i + 1} + \txFinl_{i + 1} = 1$ \item \label{hub: heartbeat: finalization phase finishes on a transaction row} From a47d2817f5fe520b4a3def5cb7559d039e364d37 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 28 Nov 2024 23:30:23 +0700 Subject: [PATCH 02/18] fix: initialization section --- hub/_inputs.tex | 28 +++---- hub/heartbeat/peeking_flags.tex | 4 +- hub/tx_init/_inputs.tex | 8 +- hub/tx_init/_local.tex | 42 +++++++--- hub/tx_init/common.tex | 32 +------- hub/tx_init/peeking.tex | 90 ++++++++++++++++------ hub/tx_init/rows/acc_recipient_undoing.tex | 24 ++++++ hub/tx_init/rows/acc_recipient_value.tex | 83 ++++++++++++++++++++ hub/tx_init/rows/acc_sender_gas.tex | 30 ++++++++ hub/tx_init/rows/acc_sender_undoing.tex | 25 ++++++ hub/tx_init/rows/acc_sender_value.tex | 20 +++++ hub/tx_init/rows/con.tex | 53 +++++++++++++ hub/tx_init/rows/first_execution_row.tex | 24 ++++++ hub/tx_init/rows/misc.tex | 39 ++++++++++ hub/tx_init/rows/txn.tex | 21 +++++ hub/tx_init/shorthands.tex | 20 +++++ hub/tx_init/update.tex | 32 ++++++++ pkg/xkeyval_macros/context.sty | 9 ++- 18 files changed, 501 insertions(+), 83 deletions(-) create mode 100644 hub/tx_init/rows/acc_recipient_undoing.tex create mode 100644 hub/tx_init/rows/acc_recipient_value.tex create mode 100644 hub/tx_init/rows/acc_sender_gas.tex create mode 100644 hub/tx_init/rows/acc_sender_undoing.tex create mode 100644 hub/tx_init/rows/acc_sender_value.tex create mode 100644 hub/tx_init/rows/con.tex create mode 100644 hub/tx_init/rows/first_execution_row.tex create mode 100644 hub/tx_init/rows/misc.tex create mode 100644 hub/tx_init/rows/txn.tex create mode 100644 hub/tx_init/shorthands.tex create mode 100644 hub/tx_init/update.tex diff --git a/hub/_inputs.tex b/hub/_inputs.tex index 089d090..6f975d1 100644 --- a/hub/_inputs.tex +++ b/hub/_inputs.tex @@ -6,19 +6,19 @@ \section{Introduction} \label{hub: intro} \input{intro} -\input{columns/_inputs} % Done -\input{heartbeat/_inputs} % Done -\input{generalities/_inputs} % Done -\input{stack/_inputs} % Done -\input{context/_inputs} % Done -\input{account/_inputs} % Done -\input{storage/_inputs} % Done -\input{misc/_inputs} % Todo -\input{scenario/_inputs} % Wip -\input{tx_skip/_inputs} % Done -\input{tx_prewarm/_inputs} % Done +% \input{columns/_inputs} % Done +% \input{heartbeat/_inputs} % Done +% \input{generalities/_inputs} % Done +% \input{stack/_inputs} % Done +% \input{context/_inputs} % Done +% \input{account/_inputs} % Done +% \input{storage/_inputs} % Done +% \input{misc/_inputs} % Todo +% \input{scenario/_inputs} % Wip +% \input{tx_skip/_inputs} % Done +% \input{tx_prewarm/_inputs} % Done \input{tx_init/_inputs} % Done -\input{instruction_handling/_inputs} % Wip +% \input{instruction_handling/_inputs} % Wip \input{tx_finl/_inputs} % Done -\input{consistencies/_inputs} % Wip -\input{lookups/_inputs} % Wip +% \input{consistencies/_inputs} % Wip +% \input{lookups/_inputs} % Wip diff --git a/hub/heartbeat/peeking_flags.tex b/hub/heartbeat/peeking_flags.tex index 437841c..d0869ad 100644 --- a/hub/heartbeat/peeking_flags.tex +++ b/hub/heartbeat/peeking_flags.tex @@ -35,7 +35,9 @@ \] and we impose \begin{enumerate}[resume] - \item $\locPeekingFlagSum_{i} = \locTransactionPhaseSum_{i}$ + \item + \label{hub: heartbeat: peeking flag exclusivity} + $\locPeekingFlagSum_{i} = \locTransactionPhaseSum_{i}$ \end{enumerate} In other words: every non-padding row peeks into precisely one data store. The precise constraints which apply to these flags depend on the transaction processing phase. diff --git a/hub/tx_init/_inputs.tex b/hub/tx_init/_inputs.tex index 8601dad..1bcebb0 100644 --- a/hub/tx_init/_inputs.tex +++ b/hub/tx_init/_inputs.tex @@ -1,4 +1,6 @@ \input{tx_init/_local} -\section{Initialization phase \lispDone{}} -\subsection{Setting the peeking flags \lispDone{}} \label{hub: initialization phase: setting peeking flags} \input{tx_init/peeking} -\subsection{Common constraints \lispDone{}} \label{hub: initialization phase: common constraints} \input{tx_init/common} +\section{Initialization phase \lispTodo{}} +\subsection{Shorthands \lispTodo{}} \label{hub: initialization phase: shorthands} \input{tx_init/shorthands} +\subsection{Setting the peeking flags \lispTodo{}} \label{hub: initialization phase: setting peeking flags} \input{tx_init/peeking} +\subsection{Common constraints \lispTodo{}} \label{hub: initialization phase: common constraints} \input{tx_init/update} +% \subsection{Common constraints \lispDone{}} \label{hub: initialization phase: common constraints} \input{tx_init/common} diff --git a/hub/tx_init/_local.tex b/hub/tx_init/_local.tex index 683ec10..efc2291 100644 --- a/hub/tx_init/_local.tex +++ b/hub/tx_init/_local.tex @@ -1,10 +1,32 @@ -\def\locTxInitWeiCost {\col{wei\_cost}} -\def\locTxInitIsDeployment {\col{deployment}} -\def\locTxInitTriggerMmu {\col{trigger\_MMU}} -\def\locTxInitCallDataContextNumber {\col{call\_data\_context\_number}} - -\def\locTxInitSenderAccountRowOffset {\yellowm{0}} -\def\locTxInitRecipientAccountRowOffset {\yellowm{1}} -\def\locTxInitMiscRowOffset {\yellowm{2}} -\def\locTxInitContextRowOffset {\yellowm{3}} -\def\locTxInitTransactionRowOffset {\orangem{4}} +\def\locTransactionWillRevert {\col{transaction\_will\_revert}} +\def\locTransactionWontRevert {\col{transaction\_wont\_revert}} +\def\locTransactionRevertStamp {\col{transaction\_revert\_stamp}} + +\def\locTxInitGasCost {\col{gas\_cost}} +\def\locTxInitValue {\col{value}} +\def\locTxInitIsDeployment {\col{is\_deployment}} +\def\locTxInitIsMessageCall {\col{is\_message\_call}} +\def\locTxInitTriggerMmu {\col{trigger\_MMU}} +\def\locTxInitCallDataContextNumber {\col{call\_data\_context\_number}} +\def\locTxInitSenderAddressHi {\col{sender\_addr\_hi}} +\def\locTxInitSenderAddressLo {\col{sender\_addr\_lo}} +\def\locTxInitRecipientAddressHi {\col{recipient\_addr\_hi}} +\def\locTxInitRecipientAddressLo {\col{recipient\_addr\_lo}} + + +\def\locTxInitRoffMisc {\yellowm{0}} +\def\locTxInitRoffTxn {\yellowm{1}} +\def\locTxInitRoffAccDoingSndPayGas {\yellowm{2}} +\def\locTxInitRoffAccDoingSenderValueTransfer {\yellowm{3}} +\def\locTxInitRoffAccDoingRecipientValueReception {\yellowm{4}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\locTxInitRoffConUnexceptionalContextRowOffset {\orangem{5}} +\def\locTxInitRoffUnexceptionalFirstExecutionRow {\greenm {6}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\locTxInitRoffAccUndoingSenderValueTransfer {\yellowm{5}} +\def\locTxInitRoffAccUndoingRecipientValueReception {\yellowm{6}} +\def\locTxInitRoffConExceptionalContextRowOffset {\orangem{7}} +\def\locTxInitRoffExceptionalFirstExecutionRow {\greenm {8}} + +\def\nsrTxInitWillRevert {\greenm{8}} +\def\nsrTxInitWontRevert {\greenm{6}} diff --git a/hub/tx_init/common.tex b/hub/tx_init/common.tex index b39838f..11194df 100644 --- a/hub/tx_init/common.tex +++ b/hub/tx_init/common.tex @@ -23,7 +23,6 @@ domOffset = 0, } } \\ - %\standardDomSubStamps {i}{\locTxInitSenderAccountRowOffset}{0} } \\ \end{array} \right. \] where @@ -45,9 +44,6 @@ \accAddress \high _{i + \locTxInitRecipientAccountRowOffset} & = & \txTo \high _{i + \locTxInitTransactionRowOffset} \\ \accAddress \low _{i + \locTxInitRecipientAccountRowOffset} & = & \txTo \low _{i + \locTxInitTransactionRowOffset} \vspace{2mm} \\ \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxInitRecipientAccountRowOffset}{\txValue_{i + \locTxInitTransactionRowOffset}}} \\ - % \multicolumn{3}{l}{\accSameNonce {i}{\locTxInitRecipientAccountRowOffset}} \\ - % \multicolumn{3}{l}{\accSameCode {i}{\locTxInitRecipientAccountRowOffset}} \\ - % \multicolumn{3}{l}{\accSameDeployment {i}{\locTxInitRecipientAccountRowOffset}} \\ \texttt{Nonce:} & \multicolumn{2}{l}{\valueToBeSet} \\ \texttt{Code:} & \multicolumn{2}{l}{\valueToBeSet} \\ \texttt{Deployment:} & \multicolumn{2}{l}{\valueToBeSet} \\ @@ -62,7 +58,6 @@ domOffset = 1, } } \\ - % \standardDomSubStamps {i}{\locTxInitRecipientAccountRowOffset}{1}} \\ \end{array} \right. \] \saNote{} The above explicitly disallows transactions targeting a precompile address. @@ -225,34 +220,9 @@ returnAtOffset = 0 , returnAtCapacity = 0 , } - % \initializeContext{\locTxInitContextRowOffset}_{i} - % \left[ \begin{array}{llr} - % \utt{context number:} & \cn\new _{i} \\ - % \utt{call stack depth:} & \rZero \\ - % \utt{is root:} & \rOne \\ - % \utt{is static:} & \rZero \\ - % \utt{account address high:} & \txTo \high _{i + \locTxInitTransactionRowOffset} \\ - % \utt{account address low:} & \txTo \low _{i + \locTxInitTransactionRowOffset} \\ - % \utt{account deployment number:} & \accDeploymentNumber \new _{i + \locTxInitRecipientAccountRowOffset} \\ - % \utt{byte code address high:} & \txTo \high _{i + \locTxInitTransactionRowOffset} \\ - % \utt{byte code address low:} & \txTo \low _{i + \locTxInitTransactionRowOffset} \\ - % \utt{byte code deployment number:} & \accDeploymentNumber \new _{i + \locTxInitRecipientAccountRowOffset} \\ - % \utt{byte code deployment status:} & \accDeploymentStatus \new _{i + \locTxInitRecipientAccountRowOffset} \\ - % \utt{byte code code fragment index:} & \accCfi _{i + \locTxInitRecipientAccountRowOffset} \\ - % \utt{caller address high:} & \txFrom \high _{i + \locTxInitTransactionRowOffset} \\ - % \utt{caller address low:} & \txFrom \low _{i + \locTxInitTransactionRowOffset} \\ - % \utt{call value:} & \txValue _{i + \locTxInitTransactionRowOffset} \\ - % \utt{call data context number:} & \locTxInitCallDataContextNumber \\ - % \utt{call data offset:} & 0 \\ - % \utt{call data size:} & \txCallDataSize _{i + \locTxInitTransactionRowOffset} \\ - % \utt{return at offset:} & 0 \\ - % \utt{return at capacity:} & 0 \\ - % % \utt{returner context:} & \col{returnerCn} \\ - % % \utt{return data offset:} & \col{returnDataOffset} \\ - % % \utt{return data size:} & \col{returnDataSize} \\ - % \end{array} \right] \] \saNote{} Recall that $\cn\new _{i} = 1 + \hubStamp _{i}$, see section~(\ref{hub: generalities: context: context numbers}). + \item[\underline{\underline{Transaction-row n$^°~(\bm{i + \locTxInitTransactionRowOffset})$:}}] we must justify certain predictions made by the \txnDataMod{} module: \begin{description} diff --git a/hub/tx_init/peeking.tex b/hub/tx_init/peeking.tex index 9b2769f..0871e1f 100644 --- a/hub/tx_init/peeking.tex +++ b/hub/tx_init/peeking.tex @@ -1,26 +1,70 @@ \begin{center} - \boxed{\text{All constraints in this subsection assume that $\txInit_{i - 1} = 0$ and $\txInit_{i} = 1$.}} + \boxed{\text{All constraints in this subsection assume that $\txInit _{i - 1} = 0$ and $\txInit _{i} = 1$.}} \end{center} In other words we assume row $i$ is the first row of the initialization phase. -This phase peeks into -(\emph{a}) the \texttt{from} account -(\emph{b}) the \texttt{to} account -(\emph{c}) it may transfer transaction call data to \textsc{ram} under the context number $\hubStamp_{i}$ -(\emph{d}) it then \emph{defines} context data -(\emph{e}) and then peeks into transaction data. -This is ensured by the following constraint: -\[ - \left[ \begin{array}{l} - + \peekAccount _{i + \locTxInitSenderAccountRowOffset } \\ - + \peekAccount _{i + \locTxInitRecipientAccountRowOffset} \\ - + \peekMisc _{i + \locTxInitMiscRowOffset } \\ - + \peekContext _{i + \locTxInitContextRowOffset } \\ - + \peekTransaction _{i + \locTxInitTransactionRowOffset } \\ - \end{array} \right] = - \nsrTransactionInitializationPhase -\] -\saNote{} Given the heartbeat constraints, the above has several \emph{implicit} consequences\footnote{which the implemenation need \textbf{not} enforce through new constraints}. The following are some of them. -\begin{itemize} - \item $\relativeBlockNumber_{j}$, $\txNum_{j}$, $\hubStamp_{j}$, $\txSkip_{j}$ remain constant on the rows $i \leq j < i + \nsrTransactionInitializationPhase$; - \item $\txExec_{i + \nsrTransactionInitializationPhase} = 1$ and $\hubStamp_{i + \nsrTransactionInitializationPhase} = 1 + \hubStamp_{i}$; -\end{itemize} +We unconditionally impose the following +\begin{enumerate} + \item + \label{hub: initialization phase: the first rows are misc and transaction rows} + $\peekMisc _{i + \locTxInitRoffMisc} + \peekTransaction _{i + \locTxInitRoffTxn} = 2$ +\end{enumerate} +Given peeking flag exclusivity, +see section~(\ref{hub: heartbeat: peeking flag exclusivity}), +the above translates precisely to +\begin{enumerate}[resume] + \item $\peekMisc _{i + \locTxInitRoffMisc} = 1$ ~ (\trash) + \item $\peekTransaction _{i + \locTxInitRoffTxn} = 1$ ~ (\trash) +\end{enumerate} +This way the first row of the initialization phase is necessarily an miscellaneous-row and the next one a transaction row. +\begin{enumerate}[resume] + \item \If $\locTransactionWillRevert = 1$ \Then + \begin{enumerate} + \item we justify + \[ + \left\{ \begin{array}{lcr} + \locTransactionWillRevert & = & \cnSelfRev _ {i + \locTxInitRoffExceptionalFirstExecutionRow} \\ + \locTransactionRevertStamp & = & \cnRevStamp _ {i + \locTxInitRoffExceptionalFirstExecutionRow} \\ + \end{array} \right. + \] + \item we set the peeking flags + \[ + \left[ \begin{array}{cl} + + & \peekMisc _{i + \locTxInitRoffMisc } \\ + + & \peekTransaction _{i + \locTxInitRoffTxn } \\ + + & \peekAccount _{i + \locTxInitRoffAccDoingSndPayGas } \\ + + & \peekAccount _{i + \locTxInitRoffAccDoingSenderValueTransfer } \\ + + & \peekAccount _{i + \locTxInitRoffAccDoingRecipientValueReception } \\ + + & \peekAccount _{i + \locTxInitRoffAccUndoingSenderValueTransfer } \\ + + & \peekAccount _{i + \locTxInitRoffAccUndoingRecipientValueReception } \\ + + & \peekContext _{i + \locTxInitRoffConExceptionalContextRowOffset } \\ + \end{array} \right] = + \nsrTxInitWillRevert + \] + \end{enumerate} + \item \If $\locTransactionWontRevert = 1$ \Then + \begin{enumerate} + \item we justify + \[ + \left\{ \begin{array}{lcr} + \locTransactionWillRevert & = & \cnSelfRev _ {i + \locTxInitRoffUnexceptionalFirstExecutionRow} \\ + \locTransactionRevertStamp & = & \cnRevStamp _ {i + \locTxInitRoffUnexceptionalFirstExecutionRow} \\ + \end{array} \right. + \] + \item we set the peeking flags + \[ + \left[ \begin{array}{cl} + + & \peekMisc _{i + \locTxInitRoffMisc } \\ + + & \peekTransaction _{i + \locTxInitRoffTxn } \\ + + & \peekAccount _{i + \locTxInitRoffAccDoingSndPayGas } \\ + + & \peekAccount _{i + \locTxInitRoffAccDoingSenderValueTransfer } \\ + + & \peekAccount _{i + \locTxInitRoffAccDoingRecipientValueReception } \\ + + & \peekContext _{i + \locTxInitRoffConUnexceptionalContextRowOffset } \\ + \end{array} \right] = + \nsrTxInitWontRevert + \] + \end{enumerate} +\end{enumerate} +\saNote{} +We remind the reader about +constraint~(\ref{hub: heartbeat: initialization phase finishes on a context row}) +which explains why we make both sections finish on a context-row. diff --git a/hub/tx_init/rows/acc_recipient_undoing.tex b/hub/tx_init/rows/acc_recipient_undoing.tex new file mode 100644 index 0000000..7d73a51 --- /dev/null +++ b/hub/tx_init/rows/acc_recipient_undoing.tex @@ -0,0 +1,24 @@ +\If $\locTransactionWillRevert = 1$ \Then we impose that +\[ + \left\{ \begin{array}{lcl} + \multicolumn{3}{l}{\accSameAddr {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accUndoBalanceUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accUndoNonceUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accUndoCodeUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accSameWarmth {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accSameDeploymentNumber {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accUndoDeploymentStatusUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + %%%% + \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \accRomLexFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \\ + \accTrmFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \\ + \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \vspace{2mm} \\ + \multicolumn{3}{l}{ + \revertDomSubStamps { + anchorRow = i, + relOffset = \locTxInitRoffAccUndoingRecipientValueReception, + subOffset = 4, + } + } \\ + \end{array} \right. +\] diff --git a/hub/tx_init/rows/acc_recipient_value.tex b/hub/tx_init/rows/acc_recipient_value.tex new file mode 100644 index 0000000..dfca938 --- /dev/null +++ b/hub/tx_init/rows/acc_recipient_value.tex @@ -0,0 +1,83 @@ +we peek into the recipient account to transfer the transaction value +\[ + \left\{ \begin{array}{lcl} + \accAddress \high _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \locTxInitRecipientAddressHi \\ + \accAddress \low _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \locTxInitRecipientAddressLo \\ + \multicolumn{3}{l}{ + \accTrimAddress + {i}{\locTxInitRoffAccDoingRecipientValueReception} + {\locTxInitRecipientAddressHi} + {\locTxInitRecipientAddressLo}} \vspace{2mm} \\ + \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxInitRoffAccDoingRecipientValueReception}{\locTxInitValue}} \\ + \texttt{Nonce:} & \multicolumn{2}{l}{\valueToBeSet} \\ + \texttt{Code:} & \multicolumn{2}{l}{\valueToBeSet} \\ + \texttt{Deployment:} & \multicolumn{2}{l}{\valueToBeSet} \\ + \multicolumn{3}{l}{\accTurnOnWarmth {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accRetrieveCodeFragmentIndex {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accIsntPrecompile {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{ + \standardDomSubStamps { + anchorRow = i , + relOffset = \locTxInitRoffAccDoingRecipientValueReception , + domOffset = 2 , + } + } \\ + \end{array} \right. +\] +We must again distinguish between message calls ($\txIsDeployment \equiv 0$) and deployments ($\txIsDeployment \equiv 1$). +\begin{description} + \item[\underline{Message calls:}] + \If $\locTxInitIsMessageCall = 1$ \Then + \begin{description} + \item[\underline{Nonce, code and deployment:}] + \[ + \left\{ \begin{array}{lcl} + \multicolumn{3}{l}{\accSameNonce {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accSameCode {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{3}{l}{\accSameDeployment {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \end{array} \right. + \] + \end{description} + \item[\underline{Nontrivial deployments:}] + \If $\locTxInitIsDeployment = 1$ \Then + \begin{description} + \item[\underline{Nonce:}] + we impose + \[ + \left\{ \begin{array}{lclr} + \multicolumn{3}{l}{\accIncrementNonce {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \accNonce_{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 & (\trash) \vspace{2mm} \\ + \end{array} \right. + \] + \item[\underline{Code:}] + we impose + \[ + \hspace*{-1cm} + \left\{ \begin{array}{lcl} + \accHasCode _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 \\ + \accCodehashHi _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \emptyKeccakHi \quad (\trash) \\ + \accCodehashLo _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \emptyKeccakLo \quad (\trash) \\ + \accCodesize _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 \\ + \end{array} \right. + \;\text{and}\; + \left\{ \begin{array}{lclr} + \accHasCode \new _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 \\ + \accCodehashHi \new _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \emptyKeccakHi \quad (\trash) \\ + \accCodehashLo \new _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \emptyKeccakLo \quad (\trash) \\ + \accCodesize \new _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \txInitCodeSize_{i + \locTxInitRoffTxn} \\ + \end{array} \right. + \] + \item[\underline{Deployment:}] + we impose + \[ + \left\{ \begin{array}{lclr} + \multicolumn{3}{l}{\accIncrementDeploymentNumber {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \accDeploymentStatus _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 & (\trash) \\ + \accDeploymentStatus\new _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \rOne \\ + \end{array} \right. + \] + \saNote{} + The same remark about \accDeploymentNumber{} as in section~(\ref{hub: tx skip: setting peeking flags}) applies. + \end{description} +\end{description} diff --git a/hub/tx_init/rows/acc_sender_gas.tex b/hub/tx_init/rows/acc_sender_gas.tex new file mode 100644 index 0000000..e1ad059 --- /dev/null +++ b/hub/tx_init/rows/acc_sender_gas.tex @@ -0,0 +1,30 @@ +the purpose of the current row is for the sender to pay for \textbf{gas costs}: +\[ + \left\{ \begin{array}{lclr} + \accAddress \high _{i + \locTxInitRoffAccDoingSndPayGas} & = & \locTxInitSenderAddressHi \\ + \accAddress \low _{i + \locTxInitRoffAccDoingSndPayGas} & = & \locTxInitSenderAddressLo \\ + \multicolumn{3}{l}{ + \accTrimAddress + {i}{\locTxInitRoffAccDoingSndPayGas} + {\locTxInitSenderAddressHi} + {\locTxInitSenderAddressLo}} \vspace{2mm} \\ + \multicolumn{3}{l}{\accDecrementBalance {i}{\locTxInitRoffAccDoingSndPayGas}{\locTxInitGasCost}} \\ + \multicolumn{3}{l}{\accIncrementNonce {i}{\locTxInitRoffAccDoingSndPayGas}} \\ + \multicolumn{3}{l}{\accSameCode {i}{\locTxInitRoffAccDoingSndPayGas}} \\ + \multicolumn{3}{l}{\accSameDeployment {i}{\locTxInitRoffAccDoingSndPayGas}} \\ + \multicolumn{3}{l}{\accTurnOnWarmth {i}{\locTxInitRoffAccDoingSndPayGas}} \\ + \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccDoingSndPayGas}} \\ + \multicolumn{3}{l}{\accIsntPrecompile {i}{\locTxInitRoffAccDoingSndPayGas}} & (\trash) \\ + \multicolumn{3}{l}{ + \standardDomSubStamps { + anchorRow = i , + relOffset = \locTxInitRoffAccDoingSndPayGas , + domOffset = 0 , + } + } \\ + \end{array} \right. +\] +In accordance with \cite{EIP-3607} we further impose +\[ + \accHasCode _{i + \locTxInitRoffAccDoingSndPayGas} = 0 +\] diff --git a/hub/tx_init/rows/acc_sender_undoing.tex b/hub/tx_init/rows/acc_sender_undoing.tex new file mode 100644 index 0000000..614b094 --- /dev/null +++ b/hub/tx_init/rows/acc_sender_undoing.tex @@ -0,0 +1,25 @@ +\If $\locTransactionWillRevert = 1$ \Then we impose that +\[ + \left\{ \begin{array}{lcl} + \multicolumn{3}{l}{\accSameAddr {i}{\locTxInitRoffAccUndoingSenderValueTransfer}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accUndoBalanceUpdate {i}{\locTxInitRoffAccUndoingSenderValueTransfer}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameNonce {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameCode {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameWarmth {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameDeploymentNumber {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameDeploymentStatus {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + %%%% + \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \accRomLexFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \\ + \accTrmFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \\ + \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \vspace{2mm} \\ + \multicolumn{3}{l}{ + \revertDomSubStamps { + anchorRow = i, + relOffset = \locTxInitRoffAccUndoingSenderValueTransfer, + subOffset = 3, + } + } \\ + \end{array} \right. +\] + diff --git a/hub/tx_init/rows/acc_sender_value.tex b/hub/tx_init/rows/acc_sender_value.tex new file mode 100644 index 0000000..1b6733d --- /dev/null +++ b/hub/tx_init/rows/acc_sender_value.tex @@ -0,0 +1,20 @@ +the purpose of the current row is for the sender to pay for \textbf{value} in the transaction: +\[ + \left\{ \begin{array}{lclr} + \multicolumn{3}{l}{\accSameAddr {i}{\locTxInitRoffAccDoingSenderValueTransfer}{\locTxInitRoffAccDoingSndPayGas}} \\ + \multicolumn{3}{l}{\accDecrementBalance {i}{\locTxInitRoffAccDoingSenderValueTransfer}{\locTxInitValue}} \\ + \multicolumn{3}{l}{\accSameNonce {i}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameCode {i}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameDeployment {i}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameWarmth {i}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{3}{l}{\accIsntPrecompile {i}{\locTxInitRoffAccDoingSenderValueTransfer}} & (\trash) \\ + \multicolumn{3}{l}{ + \standardDomSubStamps { + anchorRow = i , + relOffset = \locTxInitRoffAccDoingSenderValueTransfer , + domOffset = 1 , + } + } \\ + \end{array} \right. +\] diff --git a/hub/tx_init/rows/con.tex b/hub/tx_init/rows/con.tex new file mode 100644 index 0000000..234eb7c --- /dev/null +++ b/hub/tx_init/rows/con.tex @@ -0,0 +1,53 @@ +since the number of rows in the initialization section depends on whether or not the transaction is predicted to be rolled back, +we must distinguish between these possibilities when defining the execution context; +given some relative row offset $\relof$ we define $\initializeRootContextName$ at that row like so: +\[ + \left\{ \begin{array}{l} + \initializeRootContext{ + anchorRow = i , + relOffset = \relof , + } ~ \define \vspace{4mm} \\ + \qquad + \initializeContext{ + anchorRow = i , + relOffset = \relof , + contextNumber = \cn\new _{i} , + callStackDepth = \rZero , + isRoot = \rOne , + isStatic = \rZero , + accountAddressHigh = \locTxInitRecipientAddressHi , + accountAddressLow = \locTxInitRecipientAddressLo , + accountDeploymentNumber = \accDeploymentNumber \new _{i + \locTxInitRoffAccDoingRecipientValueReception} , + byteCodeAddressHi = \locTxInitRecipientAddressHi , + byteCodeAddressLo = \locTxInitRecipientAddressLo , + byteCodeDeploymentNumber = \accDeploymentNumber \new _{i + \locTxInitRoffAccDoingRecipientValueReception} , + byteCodeDeploymentStatus = \accDeploymentStatus \new _{i + \locTxInitRoffAccDoingRecipientValueReception} , + byteCodeCodeFragmentIndex = \accCfi _{i + \locTxInitRoffAccDoingRecipientValueReception} , + callerAddressHi = \locTxInitSenderAddressHi , + callerAddressLo = \locTxInitSenderAddressLo , + callValue = \locTxInitValue , + callDataContextNumber = \locTxInitCallDataContextNumber , + callDataOffset = 0 , + callDataSize = \txCallDataSize _{i + \locTxInitRoffTxn} , + returnAtOffset = 0 , + returnAtCapacity = 0 , + } + \end{array} \right. +\] +\saNote{} Recall that $\cn\new _{i} = 1 + \hubStamp _{i}$, see section~(\ref{hub: generalities: context: context numbers}). +\begin{enumerate} + \item \If $\locTransactionWillRevert = 1$ \Then + \[ + \initializeRootContext{ + anchorRow = i , + relOffset = \locTxInitRoffConExceptionalContextRowOffset , + } + \] + \item \If $\locTransactionWontRevert = 1$ \Then + \[ + \initializeRootContext{ + anchorRow = i , + relOffset = \locTxInitRoffConUnexceptionalContextRowOffset , + } + \] +\end{enumerate} diff --git a/hub/tx_init/rows/first_execution_row.tex b/hub/tx_init/rows/first_execution_row.tex new file mode 100644 index 0000000..9baff91 --- /dev/null +++ b/hub/tx_init/rows/first_execution_row.tex @@ -0,0 +1,24 @@ +we impose +\begin{enumerate} + \item \If $\locTransactionWillRevert = 1$ \Then + \[ + \firstRowOfNewContext + {i}{\locTxInitRoffExceptionalFirstExecutionRow} + \left[ \begin{array}{llr} + \utt{Next caller context number:} & 0 \\ + \utt{Next code fragment index:} & \accCfi _{i + \locTxInitRoffAccDoingRecipientValueReception} \\ + \utt{Available gas in new frame:} & \txInitialGas _{i + \locTxInitRoffTxn} \\ + \end{array} \right] + \] + \item \If $\locTransactionWontRevert = 1$ \Then + \[ + \firstRowOfNewContext + {i}{\locTxInitRoffUnexceptionalFirstExecutionRow} + \left[ \begin{array}{llr} + \utt{Next caller context number:} & 0 \\ + \utt{Next code fragment index:} & \accCfi _{i + \locTxInitRoffAccDoingRecipientValueReception} \\ + \utt{Available gas in new frame:} & \txInitialGas _{i + \locTxInitRoffTxn} \\ + \end{array} \right] + \] +\end{enumerate} + diff --git a/hub/tx_init/rows/misc.tex b/hub/tx_init/rows/misc.tex new file mode 100644 index 0000000..0695cfd --- /dev/null +++ b/hub/tx_init/rows/misc.tex @@ -0,0 +1,39 @@ +we impose the following +\[ + \weightedMiscFlagSum {i}{\locTxInitRoffMisc} + = + \miscMmuWeight \cdot \txCopyTxcd _{i + \locTxInitRoffTxn} +\] +Furthermore, \If $\miscMmuFlag _{i + \locTxInitRoffMisc} = 1$ \Then +\[ + \setMmuInstructionParametersExoToRamTransplants { + anchorRow = i , + relOffset = \locTxInitRoffMisc , + sourceId = \absTxNum_{i} , + targetId = \locTxInitCallDataContextNumber , + size = \txCallDataSize _{i + \locTxInitRoffTxn} , + exoSum = \exoWeightRlpTxn , + phase = \phaseTransactionCallData , + } +\] +where we have set +\[ + \locTxInitCallDataContextNumber \define \txCopyTxcd _{i + \locTxInitRoffTxn} \cdot \hubStamp_{i} +\] +\saNote{} In other words +\[ + \left\{ \begin{array}{lclr} + \miscExpFlag _{i + \locTxInitRoffMisc} & = & \gZero & (\trash) \\ + \miscMmuFlag _{i + \locTxInitRoffMisc} & = & \txCopyTxcd _{i + \locTxInitRoffTxn} & (\trash) \\ + \miscMxpFlag _{i + \locTxInitRoffMisc} & = & \rZero & (\trash) \\ + \miscOobFlag _{i + \locTxInitRoffMisc} & = & \gZero & (\trash) \\ + \miscStpFlag _{i + \locTxInitRoffMisc} & = & \gZero & (\trash) \\ + \end{array} \right. +\] +\saNote{} +\label{hub: initialization phase: transaction call data copy} +The $\txCopyTxcd$ flag is set in the \txnDataMod{} module as the conjunction of a transaction requiring \evm{} execution and being provided with nonempty call data, +see section~(\ref{txn_data: constraints: comparisons}). +The \mmuMod{} instruction serves to transfer the transaction's call data to a fresh new \textsc{ram} segment. +Future \inst{CALLDATACOPY} and \inst{CALLDATALOAD} instructions executed in the root context will extract their data from that ``execution context's \textsc{ram}'', which contains a full copy of the transaction's call data. + diff --git a/hub/tx_init/rows/txn.tex b/hub/tx_init/rows/txn.tex new file mode 100644 index 0000000..bc7925d --- /dev/null +++ b/hub/tx_init/rows/txn.tex @@ -0,0 +1,21 @@ +we must justify certain predictions made by the \txnDataMod{} module: +\begin{description} + \item[\underline{(Partially) justifying \txRequiresEvmExecution{}:}] + we impose the following + \begin{enumerate} + \item $\txRequiresEvmExecution_{i + \locTxInitRoffTxn} = \rOne$; + \item \If $\locTxInitIsMessageCall = 1$ \Then $\accHasCode _{i + \locTxInitRoffAccDoingRecipientValueReception} = 1$ + \item \If $\locTxInitIsDeployment = 1$ \Then $\txInitCodeSize _{i + \locTxInitRoffTxn} \neq 0$ (\trash) + \end{enumerate} + \item[\underline{Justifying $\txFinalRefundCounter$:}] + cannot be set at the moment; + \item[\underline{Justifying $\txInitialBalance$:}] + we impose that $\txInitialBalance _{i + \locTxInitRoffTxn} = \accBalance _{i + \locTxInitRoffAccDoingSndPayGas}$ + \item[\underline{Justifying \txStatusCode{}:}] + cannot be set at the moment\footnote{We \textbf{could} actually set the status code of the transaction at the present time: + \[ \txStatusCode _{i + \locTxInitRoffTxn} = 1 - \cnWillRev _{i + \locTxInitRoffTxn + 1} ~ (\trash) \]}; + \item[\underline{Justifying \txNonce{}:}] + we impose $\txNonce_{i + \locTxInitRoffTxn} = \accNonce_{i + \locTxInitRoffAccDoingSndPayGas}$; + \item[\underline{Justifying $\txLeftoverGas$:}] + cannot be set at the moment; +\end{description} diff --git a/hub/tx_init/shorthands.tex b/hub/tx_init/shorthands.tex new file mode 100644 index 0000000..40b51b5 --- /dev/null +++ b/hub/tx_init/shorthands.tex @@ -0,0 +1,20 @@ +We define the following shorthands. +These only make sense provided that $\txInit _{i - 1} = 0$ and $\txInit _{i} = 1$, which will be the standing assumption starting with the next section. +We draw the attention to the reader to +(\ref{hub: initialization phase: the first rows are misc and transaction rows}) +which justifies us using various row offsets and associating them with a transaction row / a miscellaneous row. +\[ + \left\{ \begin{array}{lcl} + \locTransactionWillRevert & \define & \miscChildSelfReverts _{i + \locTxInitRoffMisc} \\ + \locTransactionWontRevert & \define & 1 - \miscChildSelfReverts _{i + \locTxInitRoffMisc} \\ + \locTransactionRevertStamp & \define & \miscChildRevertStamp _{i + \locTxInitRoffMisc} \vspace{2mm} \\ + \locTxInitSenderAddressHi & \define & \txFrom \high _{i + \locTxInitRoffTxn} \\ + \locTxInitSenderAddressLo & \define & \txFrom \low _{i + \locTxInitRoffTxn} \\ + \locTxInitRecipientAddressHi & \define & \txTo \high _{i + \locTxInitRoffTxn} \\ + \locTxInitRecipientAddressLo & \define & \txTo \low _{i + \locTxInitRoffTxn} \vspace{2mm} \\ + \locTxInitIsDeployment & \define & \txIsDeployment _{i + \locTxInitRoffTxn} \\ + \locTxInitIsMessageCall & \define & 1 - \txIsDeployment _{i + \locTxInitRoffTxn} \\ + \locTxInitGasCost & \define & \txGasPrice _{i + \locTxInitRoffTxn} \cdot \txGasLimit _{i + \locTxInitRoffTxn} \\ + \locTxInitValue & \define & \txValue _{i + \locTxInitRoffTxn} \\ + \end{array} \right. +\] diff --git a/hub/tx_init/update.tex b/hub/tx_init/update.tex new file mode 100644 index 0000000..8bbe5c6 --- /dev/null +++ b/hub/tx_init/update.tex @@ -0,0 +1,32 @@ +\begin{center} + \boxed{\text{All constraints in this subsection assume that $\txInit_{i - 1} = 0$ and $\txInit_{i} = 1$.}} +\end{center} +We deal with setting the contents of the various peeking rows. +\begin{description} + \item[\underline{\underline{Miscellaneous-row n$^°~(\bm{i + \locTxInitRoffMisc})$:}}] + \input{tx_init/rows/misc} + \item[\underline{\underline{Transaction-row n$^°~(\bm{i + \locTxInitRoffTxn})$:}}] + \input{tx_init/rows/txn} + \item[\underline{\underline{Sender account-row n$^°\bm{(i + \locTxInitRoffAccDoingSndPayGas)}$:}}] + \input{tx_init/rows/acc_sender_gas} + \item[\underline{\underline{Sender account-row n$^°\bm{(i + \locTxInitRoffAccDoingSenderValueTransfer)}$:}}] + \input{tx_init/rows/acc_sender_value} + \item[\underline{\underline{Recipient account-row n$^°\bm{(i + \locTxInitRoffAccDoingRecipientValueReception)}$:}}] + \input{tx_init/rows/acc_recipient_value} +\end{description} +The following constraints undo the value transfer in case the transaction is predicted to be rolled back. +Furthermore it undoes the changes applied to the recipient account in case of a deployment transaction (in that same roll back scenario.) +\begin{description} + \item[\underline{\underline{Sender account-undoing-row n$^°\bm{(i + \locTxInitRoffAccUndoingSenderValueTransfer)}$:}}] + \input{tx_init/rows/acc_sender_undoing} + \item[\underline{\underline{Recipient account-undoing-row n$^°\bm{(i + \locTxInitRoffAccUndoingRecipientValueReception)}$:}}] + \input{tx_init/rows/acc_recipient_undoing} +\end{description} +Finally we must define the execution context data of the root context: +\begin{description} + \item[\underline{\underline{Initializing the root context:}}] + \input{tx_init/rows/con} + \item[\underline{\underline{Setting certain context variables for the first execution row:}}] + \label{hub: initialization phase: common constraints: initializing some context variables} + \input{tx_init/rows/first_execution_row} +\end{description} diff --git a/pkg/xkeyval_macros/context.sty b/pkg/xkeyval_macros/context.sty index 821e529..7425dc0 100644 --- a/pkg/xkeyval_macros/context.sty +++ b/pkg/xkeyval_macros/context.sty @@ -112,7 +112,7 @@ \setkeys[CONTEXT]{var}{#1} \initializeContextName _{\cmdCONTEXT@var@anchorRow} \left[ \begin{array}{llr} - \utt{Rel. row offset:} & \cmdCONTEXT@var@relOffset \\ + \utt{Rel. row offset:} & \cmdCONTEXT@var@relOffset \\ \utt{Context number:} & \cmdCONTEXT@var@contextNumber \\ \utt{Call stack depth:} & \cmdCONTEXT@var@callStackDepth \\ \utt{Is root context:} & \cmdCONTEXT@var@isRoot \\ @@ -139,6 +139,13 @@ \end{array} \right] } +\newcommand{\initializeRootContextName} {\texttt{initializeRootContext}} +\newcommand{\initializeRootContext} [1] { + \setkeys[CONTEXT]{var}{#1} + \initializeRootContextName _{\cmdCONTEXT@var@anchorRow} + \Big[ \utt{Rel. row offset:} \quad \cmdCONTEXT@var@relOffset \Big] + } + \newcommand{\initializeCalleeContextName} {\texttt{initializeCalleeContext}} \newcommand{\initializeCalleeContext} [1] { \setkeys[CONTEXT]{var}{#1} From 1fc91a2de3fdbf5299ee274f6eb10a7f60ae8bd1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 28 Nov 2024 23:39:20 +0700 Subject: [PATCH 03/18] ras --- hub/generalities/revert/dom_and_sub.tex | 84 ++++++++++++------------- 1 file changed, 42 insertions(+), 42 deletions(-) diff --git a/hub/generalities/revert/dom_and_sub.tex b/hub/generalities/revert/dom_and_sub.tex index 0e808ec..42147e6 100644 --- a/hub/generalities/revert/dom_and_sub.tex +++ b/hub/generalities/revert/dom_and_sub.tex @@ -14,9 +14,9 @@ \[ \left\{ \begin{array}{l} \standardDomSubStamps { - anchorRow = i, - relOffset = \relof, - domOffset = \col{d}, + anchorRow = i , + relOffset = \relof , + domOffset = \col{d} , } \vspace{2mm} \\ \qquad \qquad \iff \left\{\begin{array}{lcl} @@ -29,11 +29,11 @@ \[ \left\{ \begin{array}{l} \genericUndoingDomSubStamps { - anchorRow = i, - relOffset = \relof, - revertStamp = \rho, - domOffset = \epsilon, - subOffset = \col{s}, + anchorRow = i , + relOffset = \relof , + revertStamp = \rho , + domOffset = \epsilon , + subOffset = \col{s} , } % \genericUndoingDomSubStamps {\relof} \big[\rho, \epsilon, \col{s}\big]_{i} \vspace{2mm} \\ \qquad \qquad \iff @@ -47,17 +47,17 @@ \[ \left\{ \begin{array}{l} \revertDomSubStamps { - anchorRow = i, - relOffset = \relof, - subOffset = \col{s}, + anchorRow = i , + relOffset = \relof , + subOffset = \col{s} , } \vspace{2mm} \\ \qquad \qquad \iff \genericUndoingDomSubStamps { - anchorRow = i, - relOffset = \relof, - revertStamp = \cnRevStamp_{i}, - domOffset = \revertEpsilon, - subOffset = \col{s}, + anchorRow = i , + relOffset = \relof , + revertStamp = \cnRevStamp_{i} , + domOffset = \revertEpsilon , + subOffset = \col{s} , } % \genericUndoingDomSubStamps\big[\cnRevStamp_{i}, \revertEpsilon, \col{s}\big]_{i} \end{array} \right. @@ -66,18 +66,18 @@ \[ \left\{ \begin{array}{l} \revertWithChildFailureDomSubStamps { - anchorRow = i, - relOffset = \relof, - subOffset = \col{s}, - childRevertStamp = \col{revst}, + anchorRow = i , + relOffset = \relof , + subOffset = \col{s} , + childRevertStamp = \col{revst} , } \vspace{2mm} \\ \qquad \qquad \iff \genericUndoingDomSubStamps { - anchorRow = i, - relOffset = \relof, - revertStamp = \col{revst}, - domOffset = \revertEpsilon, - subOffset = \col{s}, + anchorRow = i , + relOffset = \relof , + revertStamp = \col{revst} , + domOffset = \revertEpsilon , + subOffset = \col{s} , } % \genericUndoingDomSubStamps\big[\col{revstp}, \revertEpsilon, \col{s}\big]_{i} \end{array} \right. @@ -88,11 +88,11 @@ \selfdestructDomSubStamps {i}{\relof} \vspace{2mm} \\ \qquad \qquad \iff \genericUndoingDomSubStamps { - anchorRow = i, - relOffset = \relof, - revertStamp = \txEndStamp _{i}, - domOffset = \selfdestructEpsilon, - subOffset = 0, + anchorRow = i , + relOffset = \relof , + revertStamp = \txEndStamp_{i} , + domOffset = \selfdestructEpsilon , + subOffset = 0 , } % \genericUndoingDomSubStamps {\relof} \big[\txEndStamp_{i}, \selfdestructEpsilon, 0 \big]_{i} \\ \end{array} \right. @@ -100,17 +100,17 @@ Some form of \[ \standardDomSubStamps { - anchorRow = i, - relOffset = \relof, - domOffset = \col{d}, + anchorRow = i , + relOffset = \relof , + domOffset = \col{d} , } \] applies to all rows in need of the $\domStamp$ and $\subStamp$. \[ \revertDomSubStamps { - anchorRow = i, - relOffset = \relof, - subOffset = \col{s}, + anchorRow = i , + relOffset = \relof , + subOffset = \col{s} , } \] (typically) allows us to schedule the undoing of certain modifications for execution at a later point. @@ -119,18 +119,18 @@ \item the larger \col{d}, the \textbf{later} the command labeled with the $(\domStamp, \subStamp)$ time stamp \[ \standardDomSubStamps { - anchorRow = i, - relOffset = \relof, - domOffset = \col{d}, + anchorRow = i , + relOffset = \relof , + domOffset = \col{d} , } \] is carried out; \item the larger \col{s}, the \textbf{earlier} the command labeled with the $(\domStamp, \subStamp)$ time stamp \[ \revertDomSubStamps { - anchorRow = i, - relOffset = \relof, - subOffset = \col{s}, + anchorRow = i , + relOffset = \relof , + subOffset = \col{s} , } \] is carried out; From 187adc200c2676ebe65ade01ea1ae4b97d22a159 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 28 Nov 2024 23:39:49 +0700 Subject: [PATCH 04/18] fix: TX_INIT reverts with child --- hub/tx_init/rows/acc_recipient_undoing.tex | 9 +++++---- hub/tx_init/rows/acc_sender_undoing.tex | 9 +++++---- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/hub/tx_init/rows/acc_recipient_undoing.tex b/hub/tx_init/rows/acc_recipient_undoing.tex index 7d73a51..dbb4dfe 100644 --- a/hub/tx_init/rows/acc_recipient_undoing.tex +++ b/hub/tx_init/rows/acc_recipient_undoing.tex @@ -14,10 +14,11 @@ \accTrmFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \\ \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \vspace{2mm} \\ \multicolumn{3}{l}{ - \revertDomSubStamps { - anchorRow = i, - relOffset = \locTxInitRoffAccUndoingRecipientValueReception, - subOffset = 4, + \revertWithChildFailureDomSubStamps { + anchorRow = i , + relOffset = \locTxInitRoffAccUndoingRecipientValueReception , + subOffset = 4 , + childRevertStamp = \locTransactionRevertStamp , } } \\ \end{array} \right. diff --git a/hub/tx_init/rows/acc_sender_undoing.tex b/hub/tx_init/rows/acc_sender_undoing.tex index 614b094..1ecf9c1 100644 --- a/hub/tx_init/rows/acc_sender_undoing.tex +++ b/hub/tx_init/rows/acc_sender_undoing.tex @@ -14,10 +14,11 @@ \accTrmFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \\ \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \vspace{2mm} \\ \multicolumn{3}{l}{ - \revertDomSubStamps { - anchorRow = i, - relOffset = \locTxInitRoffAccUndoingSenderValueTransfer, - subOffset = 3, + \revertWithChildFailureDomSubStamps { + anchorRow = i , + relOffset = \locTxInitRoffAccUndoingSenderValueTransfer , + subOffset = 3 , + childRevertStamp = \locTransactionRevertStamp , } } \\ \end{array} \right. From 172269066181e47a8a5bfeb0404121cde9f4f30f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 28 Nov 2024 23:43:02 +0700 Subject: [PATCH 05/18] ras: restoring the input file --- hub/_inputs.tex | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/hub/_inputs.tex b/hub/_inputs.tex index 6f975d1..089d090 100644 --- a/hub/_inputs.tex +++ b/hub/_inputs.tex @@ -6,19 +6,19 @@ \section{Introduction} \label{hub: intro} \input{intro} -% \input{columns/_inputs} % Done -% \input{heartbeat/_inputs} % Done -% \input{generalities/_inputs} % Done -% \input{stack/_inputs} % Done -% \input{context/_inputs} % Done -% \input{account/_inputs} % Done -% \input{storage/_inputs} % Done -% \input{misc/_inputs} % Todo -% \input{scenario/_inputs} % Wip -% \input{tx_skip/_inputs} % Done -% \input{tx_prewarm/_inputs} % Done +\input{columns/_inputs} % Done +\input{heartbeat/_inputs} % Done +\input{generalities/_inputs} % Done +\input{stack/_inputs} % Done +\input{context/_inputs} % Done +\input{account/_inputs} % Done +\input{storage/_inputs} % Done +\input{misc/_inputs} % Todo +\input{scenario/_inputs} % Wip +\input{tx_skip/_inputs} % Done +\input{tx_prewarm/_inputs} % Done \input{tx_init/_inputs} % Done -% \input{instruction_handling/_inputs} % Wip +\input{instruction_handling/_inputs} % Wip \input{tx_finl/_inputs} % Done -% \input{consistencies/_inputs} % Wip -% \input{lookups/_inputs} % Wip +\input{consistencies/_inputs} % Wip +\input{lookups/_inputs} % Wip From 1b72a37f4f91487b2982be01e0f6322be00ceebb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 28 Nov 2024 23:46:32 +0700 Subject: [PATCH 06/18] ras --- hub/tx_init/_inputs.tex | 3 +- hub/tx_init/common.tex | 259 ------------------ hub/tx_init/{update.tex => rows/_collage.tex} | 0 3 files changed, 1 insertion(+), 261 deletions(-) delete mode 100644 hub/tx_init/common.tex rename hub/tx_init/{update.tex => rows/_collage.tex} (100%) diff --git a/hub/tx_init/_inputs.tex b/hub/tx_init/_inputs.tex index 1bcebb0..08f9233 100644 --- a/hub/tx_init/_inputs.tex +++ b/hub/tx_init/_inputs.tex @@ -2,5 +2,4 @@ \section{Initialization phase \lispTodo{}} \subsection{Shorthands \lispTodo{}} \label{hub: initialization phase: shorthands} \input{tx_init/shorthands} \subsection{Setting the peeking flags \lispTodo{}} \label{hub: initialization phase: setting peeking flags} \input{tx_init/peeking} -\subsection{Common constraints \lispTodo{}} \label{hub: initialization phase: common constraints} \input{tx_init/update} -% \subsection{Common constraints \lispDone{}} \label{hub: initialization phase: common constraints} \input{tx_init/common} +\subsection{Common constraints \lispTodo{}} \label{hub: initialization phase: common constraints} \input{tx_init/rows/_collage} diff --git a/hub/tx_init/common.tex b/hub/tx_init/common.tex deleted file mode 100644 index 11194df..0000000 --- a/hub/tx_init/common.tex +++ /dev/null @@ -1,259 +0,0 @@ -\begin{center} - \boxed{\text{All constraints in this subsection assume that $\txInit_{i - 1} = 0$ and $\txInit_{i} = 1$.}} -\end{center} -We deal with setting the contents of the various peeking rows. -\begin{description} - \item[\underline{\underline{Sender account-row n$^°~\bm{(i + \locTxInitSenderAccountRowOffset)}$:}}] - the first row peeks into the sender account: - \[ - \left\{ \begin{array}{lclr} - \accAddress \high _{i + \locTxInitSenderAccountRowOffset} & = & \txFrom \high _{i + \locTxInitTransactionRowOffset} \\ - \accAddress \low _{i + \locTxInitSenderAccountRowOffset} & = & \txFrom \low _{i + \locTxInitTransactionRowOffset} \vspace{2mm} \\ - \multicolumn{3}{l}{\accDecrementBalance {i}{\locTxInitSenderAccountRowOffset}{\locTxInitWeiCost}} \\ - \multicolumn{3}{l}{\accIncrementNonce {i}{\locTxInitSenderAccountRowOffset}} \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxInitSenderAccountRowOffset}} \\ - \multicolumn{3}{l}{\accSameDeployment {i}{\locTxInitSenderAccountRowOffset}} \\ - \multicolumn{3}{l}{\accTurnOnWarmth {i}{\locTxInitSenderAccountRowOffset}} \\ - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitSenderAccountRowOffset}} \\ - \multicolumn{3}{l}{\accIsntPrecompile {i}{\locTxInitSenderAccountRowOffset}} & (\trash) \\ - \multicolumn{3}{l}{ - \standardDomSubStamps { - anchorRow = i, - relOffset = \locTxInitSenderAccountRowOffset, - domOffset = 0, - } - } \\ - \end{array} \right. - \] - where - \[ - \locTxInitWeiCost \define - \left[ \begin{array}{cr} - + & \txValue_{i + \locTxInitTransactionRowOffset} \\ - + & \txGasPrice_{i + \locTxInitTransactionRowOffset} \cdot \txGasLimit_{i + \locTxInitTransactionRowOffset} \\ - \end{array} \right] - \] - In accordance with \cite{EIP-3607} we further impose - \[ - \accHasCode _{i + \locTxInitSenderAccountRowOffset} = 0 - \] - \item[\underline{\underline{Recipient account-row n$^°~\bm{(i + \locTxInitRecipientAccountRowOffset)}$:}}] - the second row peeks into the recipient account: - \[ - \left\{ \begin{array}{lcl} - \accAddress \high _{i + \locTxInitRecipientAccountRowOffset} & = & \txTo \high _{i + \locTxInitTransactionRowOffset} \\ - \accAddress \low _{i + \locTxInitRecipientAccountRowOffset} & = & \txTo \low _{i + \locTxInitTransactionRowOffset} \vspace{2mm} \\ - \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxInitRecipientAccountRowOffset}{\txValue_{i + \locTxInitTransactionRowOffset}}} \\ - \texttt{Nonce:} & \multicolumn{2}{l}{\valueToBeSet} \\ - \texttt{Code:} & \multicolumn{2}{l}{\valueToBeSet} \\ - \texttt{Deployment:} & \multicolumn{2}{l}{\valueToBeSet} \\ - \multicolumn{3}{l}{\accTurnOnWarmth {i}{\locTxInitRecipientAccountRowOffset}} \\ - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRecipientAccountRowOffset}} \\ - \multicolumn{3}{l}{\accRetrieveCodeFragmentIndex {i}{\locTxInitRecipientAccountRowOffset}} \\ - \multicolumn{3}{l}{\accIsntPrecompile {i}{\locTxInitRecipientAccountRowOffset}} \\ - \multicolumn{3}{l}{ - \standardDomSubStamps { - anchorRow = i, - relOffset = \locTxInitRecipientAccountRowOffset, - domOffset = 1, - } - } \\ - \end{array} \right. - \] - \saNote{} The above explicitly disallows transactions targeting a precompile address. - - We must again distinguish between message calls ($\txIsDeployment \equiv 0$) and deployments ($\txIsDeployment \equiv 1$). - We thus define the following shorthand - \[ - \locTxInitIsDeployment \define \txIsDeployment _{i + \locTxInitTransactionRowOffset} - \] - and set - \begin{description} - \item[\underline{Message calls:}] - \If $\locTxInitIsDeployment = 0$ \Then - \begin{description} - \item[Nonce, code and deployment:] - \[ - \left\{ \begin{array}{lcl} - \multicolumn{3}{l}{\accSameNonce {i}{\locTxInitRecipientAccountRowOffset}} \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxInitRecipientAccountRowOffset}} \\ - \multicolumn{3}{l}{\accSameDeployment {i}{\locTxInitRecipientAccountRowOffset}} \\ - \end{array} \right. - \] - \item[Address trimming:] - the following is used to justify the fact that the target address isn't that of a precompile: - \[ - \accTrimAddress - {i}{\locTxInitRecipientAccountRowOffset} - {\txTo \high _{i + \locTxInitTransactionRowOffset}} - {\txTo \low _{i + \locTxInitTransactionRowOffset}} - \] - \saNote{} This condition isn't strictly speaking necessary as we impose that every first occurrence of an address and deployment number, in the permuted realm, be trimmed. - \end{description} - \item[\underline{Nontrivial deployments:}] - \If $\locTxInitIsDeployment = 1$ \Then - \begin{description} - \item[Nonce:] - we impose - \[ - \left\{ \begin{array}{lclr} - \multicolumn{3}{l}{\accIncrementNonce {i}{\locTxInitRecipientAccountRowOffset}} \\ - \accNonce_{i + \locTxInitRecipientAccountRowOffset} & = & 0 & (\trash) \vspace{2mm} \\ - \end{array} \right. - \] - \item[Code:] - we impose - \[ - \left\{ \begin{array}{lclr} - \accHasCode _{i + \locTxInitRecipientAccountRowOffset} & = & 0 \\ - \accCodehashHi _{i + \locTxInitRecipientAccountRowOffset} & = & \emptyKeccakHi & (\trash) \\ - \accCodehashLo _{i + \locTxInitRecipientAccountRowOffset} & = & \emptyKeccakLo & (\trash) \\ - \accCodesize _{i + \locTxInitRecipientAccountRowOffset} & = & 0 \\ - \end{array} \right. - \;\text{and}\; - \left\{ \begin{array}{lclr} - \accHasCode \new _{i + \locTxInitRecipientAccountRowOffset} & = & 0 \\ - \accCodehashHi \new _{i + \locTxInitRecipientAccountRowOffset} & = & \emptyKeccakHi & (\trash) \\ - \accCodehashLo \new _{i + \locTxInitRecipientAccountRowOffset} & = & \emptyKeccakLo & (\trash) \\ - \accCodesize \new _{i + \locTxInitRecipientAccountRowOffset} & = & \txInitCodeSize_{i + \locTxInitTransactionRowOffset} \\ - \end{array} \right. - \] - \item[Deployment:] - we impose - \[ - \left\{ \begin{array}{lclr} - \multicolumn{3}{l}{\accIncrementDeploymentNumber {i}{\locTxInitRecipientAccountRowOffset}} \\ - \accDeploymentStatus _{i + \locTxInitRecipientAccountRowOffset} & = & 0 & (\trash) \\ - \accDeploymentStatus\new _{i + \locTxInitRecipientAccountRowOffset} & = & \rOne \\ - \end{array} \right. - \] - \saNote{} - The same remark about \accDeploymentNumber{} as in section~(\ref{hub: tx skip: setting peeking flags}) applies. - \end{description} - % \item[\underline{Retrieving the code fragment index:}] - % we impose - % \[ - % \accRetrieveCodeFragmentIndex {i}{\locTxInitRecipientAccountRowOffset} - % \] - \end{description} - \item[\underline{\underline{Miscellaneous-row n$^°~(\bm{i + \locTxInitMiscRowOffset})$:}}] - we impose the following - \[ - \weightedMiscFlagSum {i}{\locTxInitMiscRowOffset} - = - \miscMmuWeight \cdot \txCopyTxcd _{i + \locTxInitTransactionRowOffset} - \] - Furthermore, \If $\miscMmuFlag _{i + \locTxInitMiscRowOffset} = 1$ \Then - \[ - \setMmuInstructionParametersExoToRamTransplants { - anchorRow = i , - relOffset = \locTxInitMiscRowOffset , - sourceId = \absTxNum_{i} , - targetId = \locTxInitCallDataContextNumber , - size = \txCallDataSize _{i + \locTxInitTransactionRowOffset} , - exoSum = \exoWeightRlpTxn , - phase = \phaseTransactionCallData , - } - % \setMmuInstructionParametersExoToRamTransplants {i}{\locTxInitMiscRowOffset} - % \left[ \begin{array}{ll} - % \utt{Source ID:} & \absTxNum_{i} \\ - % \utt{Target ID:} & \locTxInitCallDataContextNumber \\ - % % \utt{Auxiliary ID:} & \col{aux\_id} \\ - % % \utt{Source offset high:} & \col{src\_offset\_hi} \\ - % % \utt{Source offset low:} & \col{src\_offset\_lo} \\ - % % \utt{Target offset low:} & \col{tgt\_offset\_lo} \\ - % \utt{Size:} & \txCallDataSize _{i + \locTxInitTransactionRowOffset} \\ - % % \utt{Reference offset:} & \col{ref\_offset} \\ - % % \utt{Reference size:} & \col{ref\_size} \\ - % % \utt{Success bit:} & \col{success\_bit} \\ - % % \utt{Limb one:} & \col{limb\_1} \\ - % % \utt{Limb two:} & \col{limb\_2} \\ - % \utt{Exo sum:} & \exoWeightRlpTxn \\ - % \utt{Phase:} & \phaseTransactionCallData \\ - % \end{array} \right] \vspace{2mm} \\ - \] - where we have set - \[ - \locTxInitCallDataContextNumber \define \txCopyTxcd _{i + \locTxInitTransactionRowOffset} \cdot \hubStamp_{i} - \] - \saNote{} In other words - \[ - \left\{ \begin{array}{lclr} - \miscExpFlag _{i + \locTxInitMiscRowOffset} & = & \gZero & (\trash) \\ - \miscMmuFlag _{i + \locTxInitMiscRowOffset} & = & \txCopyTxcd _{i + \locTxInitTransactionRowOffset} & (\trash) \\ - \miscMxpFlag _{i + \locTxInitMiscRowOffset} & = & \rZero & (\trash) \\ - \miscOobFlag _{i + \locTxInitMiscRowOffset} & = & \gZero & (\trash) \\ - \miscStpFlag _{i + \locTxInitMiscRowOffset} & = & \gZero & (\trash) \\ - \end{array} \right. - \] - \saNote{} - \label{hub: initialization phase: transaction call data copy} - The $\txCopyTxcd$ flag is set in the \txnDataMod{} module as the conjunction of a transaction requiring \evm{} execution and being provided with nonempty call data, - see section~(\ref{txn_data: constraints: comparisons}). - The \mmuMod{} instruction serves to transfer the transaction's call data to a fresh new \textsc{ram} segment. - Future \inst{CALLDATACOPY} and \inst{CALLDATALOAD} instructions executed in the root context will extract their data from that ``execution context's \textsc{ram}'', which contains a full copy of the transaction's call data. - - \item[\underline{\underline{Context-row n$^°~(\bm{i + \locTxInitContextRowOffset})$:}}] - we initialize the next execution context as follows: - \[ - \initializeContext{ - anchorRow = i , - relOffset = \locTxInitContextRowOffset , - contextNumber = \cn\new _{i} , - callStackDepth = \rZero , - isRoot = \rOne , - isStatic = \rZero , - accountAddressHigh = \txTo \high _{i + \locTxInitTransactionRowOffset} , - accountAddressLow = \txTo \low _{i + \locTxInitTransactionRowOffset} , - accountDeploymentNumber = \accDeploymentNumber \new _{i + \locTxInitRecipientAccountRowOffset} , - byteCodeAddressHi = \txTo \high _{i + \locTxInitTransactionRowOffset} , - byteCodeAddressLo = \txTo \low _{i + \locTxInitTransactionRowOffset} , - byteCodeDeploymentNumber = \accDeploymentNumber \new _{i + \locTxInitRecipientAccountRowOffset} , - byteCodeDeploymentStatus = \accDeploymentStatus \new _{i + \locTxInitRecipientAccountRowOffset} , - byteCodeCodeFragmentIndex = \accCfi _{i + \locTxInitRecipientAccountRowOffset} , - callerAddressHi = \txFrom \high _{i + \locTxInitTransactionRowOffset} , - callerAddressLo = \txFrom \low _{i + \locTxInitTransactionRowOffset} , - callValue = \txValue _{i + \locTxInitTransactionRowOffset} , - callDataContextNumber = \locTxInitCallDataContextNumber , - callDataOffset = 0 , - callDataSize = \txCallDataSize _{i + \locTxInitTransactionRowOffset} , - returnAtOffset = 0 , - returnAtCapacity = 0 , - } - \] - \saNote{} Recall that $\cn\new _{i} = 1 + \hubStamp _{i}$, see section~(\ref{hub: generalities: context: context numbers}). - - \item[\underline{\underline{Transaction-row n$^°~(\bm{i + \locTxInitTransactionRowOffset})$:}}] - we must justify certain predictions made by the \txnDataMod{} module: - \begin{description} - \item[\underline{(Partially) justifying \txRequiresEvmExecution{}:}] - we impose the following - \begin{enumerate} - \item $\txRequiresEvmExecution_{i + \locTxInitTransactionRowOffset} = \rOne$; - \item \If $\txIsDeployment _{i + \locTxInitTransactionRowOffset} = 0$ \Then $\accHasCode _{i + \locTxInitRecipientAccountRowOffset} = 1$ - \item \If $\txIsDeployment _{i + \locTxInitTransactionRowOffset} = 1$ \Then $\txInitCodeSize _{i + \locTxInitTransactionRowOffset} \neq 0$ (\trash) - \end{enumerate} - \item[\underline{Justifying $\txFinalRefundCounter$:}] - cannot be set at the moment; - \item[\underline{Justifying $\txInitialBalance$:}] - we impose that $\txInitialBalance _{i + \locTxInitTransactionRowOffset} = \accBalance _{i + \locTxInitSenderAccountRowOffset}$ - \item[\underline{Justifying \txStatusCode{}:}] - cannot be set at the moment\footnote{We \textbf{could} actually set the status code of the transaction at the present time: - \[ \txStatusCode _{i + \locTxInitTransactionRowOffset} = 1 - \cnWillRev _{i + \locTxInitTransactionRowOffset + 1} ~ (\trash) \]}; - \item[\underline{Justifying \txNonce{}:}] - we impose $\accNonce_{i + \locTxInitSenderAccountRowOffset} = \txNonce_{i + \locTxInitTransactionRowOffset}$; - \item[\underline{Justifying $\txLeftoverGas$:}] - cannot be set at the moment; - \end{description} - \item[\underline{\underline{Initializing some context variables:}}] - \label{hub: initialization phase: common constraints: initializing some context variables} - we impose - \[ - \firstRowOfNewContext {i}{\locTxInitTransactionRowOffset + 1} - \left[ \begin{array}{llr} - \utt{Next caller context number:} & 0 \\ - \utt{Next code fragment index:} & \accCfi _{i + \locTxInitRecipientAccountRowOffset} \\ - \utt{Available gas in new frame:} & \txInitialGas _{i + \locTxInitTransactionRowOffset} \\ - \end{array} \right] - \] -\end{description} diff --git a/hub/tx_init/update.tex b/hub/tx_init/rows/_collage.tex similarity index 100% rename from hub/tx_init/update.tex rename to hub/tx_init/rows/_collage.tex From 358952178c220f1205f7f0f5defaddc849b23847 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 29 Nov 2024 11:04:47 +0700 Subject: [PATCH 07/18] feat: intro for TX_INIT phase + ras --- hub/_inputs.tex | 28 ++++++++++++------------ hub/tx_init/_inputs.tex | 1 + hub/tx_init/intro.tex | 9 ++++++++ hub/tx_init/rows/acc_recipient_value.tex | 4 +++- pkg/common.sty | 2 +- 5 files changed, 28 insertions(+), 16 deletions(-) create mode 100644 hub/tx_init/intro.tex diff --git a/hub/_inputs.tex b/hub/_inputs.tex index 089d090..6f975d1 100644 --- a/hub/_inputs.tex +++ b/hub/_inputs.tex @@ -6,19 +6,19 @@ \section{Introduction} \label{hub: intro} \input{intro} -\input{columns/_inputs} % Done -\input{heartbeat/_inputs} % Done -\input{generalities/_inputs} % Done -\input{stack/_inputs} % Done -\input{context/_inputs} % Done -\input{account/_inputs} % Done -\input{storage/_inputs} % Done -\input{misc/_inputs} % Todo -\input{scenario/_inputs} % Wip -\input{tx_skip/_inputs} % Done -\input{tx_prewarm/_inputs} % Done +% \input{columns/_inputs} % Done +% \input{heartbeat/_inputs} % Done +% \input{generalities/_inputs} % Done +% \input{stack/_inputs} % Done +% \input{context/_inputs} % Done +% \input{account/_inputs} % Done +% \input{storage/_inputs} % Done +% \input{misc/_inputs} % Todo +% \input{scenario/_inputs} % Wip +% \input{tx_skip/_inputs} % Done +% \input{tx_prewarm/_inputs} % Done \input{tx_init/_inputs} % Done -\input{instruction_handling/_inputs} % Wip +% \input{instruction_handling/_inputs} % Wip \input{tx_finl/_inputs} % Done -\input{consistencies/_inputs} % Wip -\input{lookups/_inputs} % Wip +% \input{consistencies/_inputs} % Wip +% \input{lookups/_inputs} % Wip diff --git a/hub/tx_init/_inputs.tex b/hub/tx_init/_inputs.tex index 08f9233..cfdd31d 100644 --- a/hub/tx_init/_inputs.tex +++ b/hub/tx_init/_inputs.tex @@ -1,5 +1,6 @@ \input{tx_init/_local} \section{Initialization phase \lispTodo{}} +\subsection{Introduction \lispNone{}} \label{hub: initialization phase: shorthands} \input{tx_init/intro} \subsection{Shorthands \lispTodo{}} \label{hub: initialization phase: shorthands} \input{tx_init/shorthands} \subsection{Setting the peeking flags \lispTodo{}} \label{hub: initialization phase: setting peeking flags} \input{tx_init/peeking} \subsection{Common constraints \lispTodo{}} \label{hub: initialization phase: common constraints} \input{tx_init/rows/_collage} diff --git a/hub/tx_init/intro.tex b/hub/tx_init/intro.tex new file mode 100644 index 0000000..f9e98e0 --- /dev/null +++ b/hub/tx_init/intro.tex @@ -0,0 +1,9 @@ +The main purpose of the \textbf{initialization phase} is for the sender of a transaction +to pay for gas, +to perform the initial value transfer to the recipient, +and to initialize the execution context wherein \evm{} execution will take place. +To that list of actions one should add, whenever the transaction provides nonempty call data, +the transfer of transaction call data (at points abbreviated as \col{TXCD}) to a dedicated memory space. +Furthermore, very much like for \inst{CALL}-type and \inst{CREATE}-type instructions, +the initialization phase may include ``undoing operations'' related to certain of its own account-related actions. +Such ``undoing operations'' are included \emph{if and only if} the transaction is predicted to revert. diff --git a/hub/tx_init/rows/acc_recipient_value.tex b/hub/tx_init/rows/acc_recipient_value.tex index dfca938..4ed6b13 100644 --- a/hub/tx_init/rows/acc_recipient_value.tex +++ b/hub/tx_init/rows/acc_recipient_value.tex @@ -25,7 +25,9 @@ } \\ \end{array} \right. \] -We must again distinguish between message calls ($\txIsDeployment \equiv 0$) and deployments ($\txIsDeployment \equiv 1$). +We must distinguish between +message calls ($\locTxInitIsMessageCall~=~1$) and +deployments ($\locTxInitIsDeployment~=~1$). \begin{description} \item[\underline{Message calls:}] \If $\locTxInitIsMessageCall = 1$ \Then diff --git a/pkg/common.sty b/pkg/common.sty index 5384542..bd01788 100644 --- a/pkg/common.sty +++ b/pkg/common.sty @@ -202,7 +202,7 @@ \newcommand{\alreadySet} {\gray{\texttt{}}} \newcommand{\leftUndefined} {\gray{\texttt{}}} \newcommand{\relevantValue} {\texttt{}} -\newcommand{\valueToBeSet} {\texttt{}} +\newcommand{\valueToBeSet} {\green{\texttt{}}} \newcommand{\valueUnknown} {\gray{\texttt{}}} \newcommand{\toBeSet} {\orange{TO BE SET}} \newcommand{\justifiedByExternalCircuit}{\texttt{}} From 2cbe5255a72ba211b8ae07b65c2c9de8d3801469 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 29 Nov 2024 14:03:14 +0700 Subject: [PATCH 08/18] fix: finalization section + \finalizationDomSubStamps{...} --- hub/generalities/revert/constants.tex | 14 +-- hub/generalities/revert/dom_and_sub.tex | 31 +++++-- hub/tx_finl/_inputs.tex | 10 +- hub/tx_finl/_local.tex | 43 ++++++--- hub/tx_finl/failure.tex | 118 ------------------------ hub/tx_finl/intro.tex | 16 +--- hub/tx_finl/peeking.tex | 40 ++------ hub/tx_finl/rows/_collage.tex | 18 ++++ hub/tx_finl/rows/acc_coinbase.tex | 28 ++++++ hub/tx_finl/rows/acc_sender.tex | 27 ++++++ hub/tx_finl/rows/txn.tex | 8 ++ hub/tx_finl/shorthands.tex | 18 ++++ hub/tx_finl/success.tex | 94 ------------------- pkg/env.sty | 1 + pkg/xkeyval_macros/dom_sub_stamps.sty | 44 ++++++--- 15 files changed, 208 insertions(+), 302 deletions(-) delete mode 100644 hub/tx_finl/failure.tex create mode 100644 hub/tx_finl/rows/_collage.tex create mode 100644 hub/tx_finl/rows/acc_coinbase.tex create mode 100644 hub/tx_finl/rows/acc_sender.tex create mode 100644 hub/tx_finl/rows/txn.tex create mode 100644 hub/tx_finl/shorthands.tex delete mode 100644 hub/tx_finl/success.tex diff --git a/hub/generalities/revert/constants.tex b/hub/generalities/revert/constants.tex index b065d9e..4e05029 100644 --- a/hub/generalities/revert/constants.tex +++ b/hub/generalities/revert/constants.tex @@ -1,14 +1,16 @@ The re-ordering arguments involving dominant and subordinate stamps (i.e. $\domStamp$ and $\subStamp$) rely on some constants which we define here: \begin{itemize} - \item $\hubTau = 8$ - \item $\hubLambda = 8$ - \item $\revertEpsilon = 6$ - \item $\selfdestructEpsilon = 7$ + \item $\hubTau = 8$ + \item $\hubLambda = 11$ + \item $\revertEpsilon = 8$ + \item $\finalizationEpsilon = 9$ + \item $\selfdestructEpsilon = 10$ \end{itemize} -Two criteria have to be considered in setting these constants: +Two criteria have to be considered in setting these constants. +Let us define \col{max} as the maximum ``$\domStamp$''-offset encountered in constraints \begin{enumerate} \item for any ``dom''-offset \col{d} used in a constraint to set $\domStamp \equiv \hubLambda \cdot \col{h} + \col{d}$ (where $\col{h} \equiv \hubStamp$) it should hold that $0 \leq \col{d} < \revertEpsilon$ - \item $0 \leq \revertEpsilon < \selfdestructEpsilon < \hubLambda$ + \item $\col{max} < \revertEpsilon < \finalizationEpsilon < \selfdestructEpsilon < \hubLambda$ where \col{max} is the maximum ``$\domStamp$''-offset encountered in constraints (i.e. the \end{enumerate} Indeed reverting should happen before gas refunds and before enacting any \inst{SELFDESTRUCT}'s and ``\texttt{doing}''-actions ``taken in the moment'' should not interfere with ``\texttt{undoing}''-actions scheduled for post roll back. \begin{itemize} diff --git a/hub/generalities/revert/dom_and_sub.tex b/hub/generalities/revert/dom_and_sub.tex index 42147e6..2b23d54 100644 --- a/hub/generalities/revert/dom_and_sub.tex +++ b/hub/generalities/revert/dom_and_sub.tex @@ -5,8 +5,8 @@ \zeroDomSubStamps {i}{\relof} \vspace{2mm} \\ \qquad \qquad \iff \left\{\begin{array}{lcl} - \domStamp_{i + \relof} & \!\!\! = \!\!\! & 0 \\ - \subStamp_{i + \relof} & \!\!\! = \!\!\! & 0 \\ + \domStamp_{i + \relof} & \!\!\! = \!\!\! & 0 \\ + \subStamp_{i + \relof} & \!\!\! = \!\!\! & 0 \\ \end{array}\right. \end{array} \right. \] @@ -20,8 +20,8 @@ } \vspace{2mm} \\ \qquad \qquad \iff \left\{\begin{array}{lcl} - \domStamp_{i + \relof} & \!\!\! = \!\!\! & \hubLambda \cdot \hubStamp_{i} + \col{d} \\ - \subStamp_{i + \relof} & \!\!\! = \!\!\! & 0 \\ + \domStamp_{i + \relof} & \!\!\! = \!\!\! & \hubLambda \cdot \hubStamp_{i} + \col{d} \\ + \subStamp_{i + \relof} & \!\!\! = \!\!\! & 0 \\ \end{array}\right. \end{array} \right. \] @@ -38,8 +38,8 @@ % \genericUndoingDomSubStamps {\relof} \big[\rho, \epsilon, \col{s}\big]_{i} \vspace{2mm} \\ \qquad \qquad \iff \left\{\begin{array}{lcl} - \domStamp_{i + \relof} & \!\!\! = \!\!\! & \hubLambda \cdot \rho + \epsilon \\ - \subStamp_{i + \relof} & \!\!\! = \!\!\! & \hubLambda \cdot \hubStamp_{i} + \col{s} \\ + \domStamp_{i + \relof} & \!\!\! = \!\!\! & \hubLambda \cdot \rho + \epsilon \\ + \subStamp_{i + \relof} & \!\!\! = \!\!\! & \hubLambda \cdot \hubStamp_{i} + \col{s} \\ \end{array}\right. \end{array} \right. \] @@ -83,6 +83,25 @@ \end{array} \right. \] and +\[ + \left\{ \begin{array}{l} + \finalizationDomSubStamps { + anchorRow = i , + relOffset = \relof , + subOffset = \col{s} , + } + \vspace{2mm} \\ \qquad \qquad \iff + \genericUndoingDomSubStamps { + anchorRow = i , + relOffset = \relof , + revertStamp = \txEndStamp_{i} , + domOffset = \finalizationEpsilon , + subOffset = \col{s} , + } + % \genericUndoingDomSubStamps {\relof} \big[\txEndStamp_{i}, \selfdestructEpsilon, 0 \big]_{i} \\ + \end{array} \right. +\] +and \[ \left\{ \begin{array}{l} \selfdestructDomSubStamps {i}{\relof} diff --git a/hub/tx_finl/_inputs.tex b/hub/tx_finl/_inputs.tex index df237cc..cdc1b14 100644 --- a/hub/tx_finl/_inputs.tex +++ b/hub/tx_finl/_inputs.tex @@ -1,6 +1,6 @@ \input{tx_finl/_local} -\section{Finalization phase \lispDone{}} \label{hub: finalization phase} -\subsection{Introduction} \label{hub: finalization phase: intro} \input{tx_finl/intro} -\subsection{Peeking flags \lispDone{}} \label{hub: finalization phase: peeking} \input{tx_finl/peeking} -\subsection{The transaction success case \lispDone{}} \label{hub: finalization phase: success} \input{tx_finl/success} -\subsection{The transaction failure case \lispDone{}} \label{hub: finalization phase: failure} \input{tx_finl/failure} +\section{Finalization phase \lispDone{}} \label{hub: finalization phase} +\subsection{Introduction \lispNone{}} \label{hub: finalization phase: intro} \input{tx_finl/intro} +\subsection{Shorthands \lispTodo{}} \label{hub: finalization phase: shorthands} \input{tx_finl/shorthands} +\subsection{Peeking flags \lispTodo{}} \label{hub: finalization phase: peeking} \input{tx_finl/peeking} +\subsection{Common constraints \lispTodo{}} \label{hub: finalization phase: common constraints} \input{tx_finl/rows/_collage} diff --git a/hub/tx_finl/_local.tex b/hub/tx_finl/_local.tex index a708dfb..0e83254 100644 --- a/hub/tx_finl/_local.tex +++ b/hub/tx_finl/_local.tex @@ -1,17 +1,32 @@ -\def\locWeiRefund {\col{caller\_refund}} -\def\locWeiReward {\col{coinbase\_reward}} -% no revert -\def\locTxFinlSuccessSenderAccountOffset {\yellowm{0}} -\def\locTxFinlSuccessCoinbaseAccountOffset {\yellowm{1}} -\def\locTxFinlSuccessTransactionRowOffset {\orangem{2}} +\def\locWeiRefund {\col{sender\_gas\_refund}} +\def\locWeiReward {\col{coinbase\_reward}} +\def\locTxFinlRoffLastExecutionRow {\greenm{1}} +\def\locTxFinlRoffAccSender {\yellowm{0}} +\def\locTxFinlRoffAccCoinbase {\yellowm{1}} +\def\locTxFinlRoffTxn {\orangem{2}} + +\def\locTransactionFailure {\col{transaction\_failure}} +\def\locTransactionSuccess {\col{transaction\_success}} +\def\locTransactionEndStamp {\col{transaction\_end\_stamp}} + +\def\locTxFinlSenderAddressHi {\col{sender\_addr\_hi}} +\def\locTxFinlSenderAddressLo {\col{sender\_addr\_lo}} +\def\locTxFinlCoinbaseAddressHi {\col{coinbase\_addr\_hi}} +\def\locTxFinlCoinbaseAddressLo {\col{coinbase\_addr\_lo}} + +% +\def\locTxFinlSuccessSenderAccountOffset {\yellowm{0}} +\def\locTxFinlSuccessCoinbaseAccountOffset {\yellowm{1}} +\def\locTxFinlSuccessTransactionRowOffset {\orangem{2}} +\def\nsrTxFinl {\yellowm{3}} % revert -\def\locTxFinlFailureSenderAccountOffset {\yellowm{0}} -\def\locTxFinlFailureRecipientAccountOffset {\yellowm{1}} -\def\locTxFinlFailureCoinbaseAccountOffset {\yellowm{2}} -\def\locTxFinlFailureTransactionRowOffset {\orangem{3}} +\def\locTxFinlFailureSenderAccountOffset {\yellowm{0}} +\def\locTxFinlFailureRecipientAccountOffset {\yellowm{1}} +\def\locTxFinlFailureCoinbaseAccountOffset {\yellowm{2}} +\def\locTxFinlFailureTransactionRowOffset {\orangem{3}} % -\def\locFinlSuccessSenderRefund {\col{sender\_refund}} -\def\locFinlSuccessCoinbaseReward {\col{coinbase\_fee}} +\def\locFinlSuccessSenderRefund {\col{sender\_refund}} +\def\locFinlSuccessCoinbaseReward {\col{coinbase\_fee}} % -\def\locFinlFailureSenderRefund {\col{sender\_refund}} -\def\locFinlFailureCoinbaseReward {\col{coinbase\_fee}} +\def\locFinlFailureSenderRefund {\col{sender\_refund}} +\def\locFinlFailureCoinbaseReward {\col{coinbase\_fee}} diff --git a/hub/tx_finl/failure.tex b/hub/tx_finl/failure.tex deleted file mode 100644 index 7e623d4..0000000 --- a/hub/tx_finl/failure.tex +++ /dev/null @@ -1,118 +0,0 @@ -\begin{center} - \boxed{% - \text{The constraints presented below assume } - \left\{ \begin{array}{lcl} - \txExec _{i - 1} & = & 1 \\ - \txFinl _{i} & = & 1 \\ - \cnWillRev _{i - 1} & = & 1 \\ - \end{array} \right. - } -\end{center} -The constraints that follow pertain to transaction finalization when the underlying transaction exited with status code $0$. -\begin{description} - \item[\underline{\underline{Account row n$^°{(i + \locTxFinlSuccessSenderAccountOffset)}$:}}] - we impose the following to the \textbf{sender account}: - \[ - \left\{\begin{array}{lcl} - \accAddress\high _{i + \locTxFinlFailureSenderAccountOffset} & = & \txFrom\high _{i + \locTxFinlFailureTransactionRowOffset} \\ - \accAddress\low _{i + \locTxFinlFailureSenderAccountOffset} & = & \txFrom\low _{i + \locTxFinlFailureTransactionRowOffset} \\ - \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxFinlFailureSenderAccountOffset}{\locFinlFailureSenderRefund}} \\ - \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlFailureSenderAccountOffset} } \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlFailureSenderAccountOffset}} \\ - \multicolumn{3}{l}{\accSameDeployment {i}{\locTxFinlFailureSenderAccountOffset}} \\ - \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlFailureSenderAccountOffset}} \\ - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlFailureSenderAccountOffset}} \\ - \multicolumn{3}{l}{ - \standardDomSubStamps { - anchorRow = i, - relOffset = \locTxFinlFailureSenderAccountOffset, - domOffset = 0, - } - } \\ - % \standardDomSubStamps {i}{\locTxFinlFailureSenderAccountOffset}{0}} \\ - \end{array}\right. - \] - where - \[ - \locFinlFailureSenderRefund \define - \txGasPrice_{i + \locTxFinlFailureTransactionRowOffset} - \cdot \txEffectiveRefund_{i + \locTxFinlFailureTransactionRowOffset} - + \txValue_{i + \locTxFinlFailureTransactionRowOffset} - \] - \item[\underline{\underline{Account row n$^°{(i + \locTxFinlFailureRecipientAccountOffset)}$:}}] - we impose the following to the \textbf{recipient account}: - \[ - \left\{\begin{array}{lcl} - \accAddress\high _{i + \locTxFinlFailureRecipientAccountOffset} & = & \txTo\high _{i + \locTxFinlFailureTransactionRowOffset} \\ - \accAddress\low _{i + \locTxFinlFailureRecipientAccountOffset} & = & \txTo\low _{i + \locTxFinlFailureTransactionRowOffset} \\ - \multicolumn{3}{l}{\accDecrementBalance {i}{\locTxFinlFailureRecipientAccountOffset}{\txValue_{i + \locTxFinlFailureTransactionRowOffset}}} \\ - \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlFailureRecipientAccountOffset}} \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlFailureRecipientAccountOffset}} \\ - \multicolumn{3}{l}{\accSameDeployment {i}{\locTxFinlFailureRecipientAccountOffset}} \\ - \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlFailureRecipientAccountOffset}} \\ - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlFailureRecipientAccountOffset}} \\ - \multicolumn{3}{l}{ - \standardDomSubStamps { - anchorRow = i, - relOffset = \locTxFinlFailureRecipientAccountOffset, - domOffset = 1, - } - } \\ - % \standardDomSubStamps {i}{\locTxFinlFailureRecipientAccountOffset}{1}} \\ - % \multicolumn{3}{l}{\accOpening {\locTxFinlFailureSenderAccountOffset} _{i}} \\ - \end{array}\right. - \] - \item[\underline{\underline{Account row n$^°{(i + \locTxFinlFailureCoinbaseAccountOffset)}$:}}] - we impose the following to the \textbf{coinbase account}: - \[ - \left\{\begin{array}{lcl} - \accAddress\high _{i + \locTxFinlFailureCoinbaseAccountOffset} & = & \txCoinbase\high _{i + \locTxFinlFailureTransactionRowOffset} \\ - \accAddress\low _{i + \locTxFinlFailureCoinbaseAccountOffset} & = & \txCoinbase\low _{i + \locTxFinlFailureTransactionRowOffset} \\ - \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxFinlFailureCoinbaseAccountOffset}{\locFinlFailureCoinbaseReward}} \\ - \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlFailureCoinbaseAccountOffset} } \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlFailureCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{\accSameDeployment {i}{\locTxFinlFailureCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlFailureCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlFailureCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{ - \standardDomSubStamps { - anchorRow = i, - relOffset = \locTxFinlFailureCoinbaseAccountOffset, - domOffset = 2, - } - } \\ - % \standardDomSubStamps {i}{\locTxFinlFailureCoinbaseAccountOffset}{2} } \\ - \end{array}\right. - \] - where \locFinlFailureCoinbaseReward{} is a shorthand defined as follows: - \[ - \locFinlFailureCoinbaseReward \define - \left[ \begin{array}{cl} - \cdot & \txPriorityFeePerGas_{i + \locTxFinlFailureTransactionRowOffset} \\ - \cdot & (\txGasLimit_{i + \locTxFinlFailureTransactionRowOffset} - \txEffectiveRefund_{i + \locTxFinlFailureTransactionRowOffset}) \\ - \end{array} \right] - \] - % \begin{enumerate} - % \item \If $\txIsTypeTwo_{i + \locTxFinlFailureTransactionRowOffset} = 0$ \Then - % \[ - % \locFinlFailureCoinbaseReward \define - % \txGasPrice_{i + \locTxFinlFailureTransactionRowOffset} - % \cdot (\txGasLimit_{i + \locTxFinlFailureTransactionRowOffset} - \txEffectiveRefund_{i + \locTxFinlFailureTransactionRowOffset}) - % \] - % \item \If $\txIsTypeTwo_{i + \locTxFinlFailureTransactionRowOffset} = 1$ \Then - % \[ - % \locFinlFailureCoinbaseReward \define - % (\txGasPrice_{i + \locTxFinlFailureTransactionRowOffset} - \txBasefee_{i + \locTxFinlFailureTransactionRowOffset}) - % \cdot (\txGasLimit_{i + \locTxFinlFailureTransactionRowOffset} - \txEffectiveRefund_{i + \locTxFinlFailureTransactionRowOffset}) - % \] - % \end{enumerate} - \item[\underline{\underline{Transaction row n$^°{(i + \locTxFinlFailureTransactionRowOffset)}$:}}] - we load transaction data to have access to relevant fields but also to confirm data predicted in the \txnDataMod{}: - \[ - \left\{\begin{array}{lcll} - \txStatusCode _{i + \locTxFinlFailureTransactionRowOffset} & = & \rZero \\ - \txFinalRefundCounter _{i + \locTxFinlFailureTransactionRowOffset} & = & \refund _{i - 1} \\ - \txLeftoverGas _{i + \locTxFinlFailureTransactionRowOffset} & = & \gasNext _{i - 1} \\ - \end{array}\right. - \] -\end{description} diff --git a/hub/tx_finl/intro.tex b/hub/tx_finl/intro.tex index 43469da..345c82c 100644 --- a/hub/tx_finl/intro.tex +++ b/hub/tx_finl/intro.tex @@ -4,14 +4,8 @@ \item pay the gas refund of the transaction sender $S(T)$; \item pay the \inst{COINBASE} address the gas fee; \end{enumerate} -Furthermore, if the transaction reverts, the present phase is responsible for -\begin{enumerate}[resume] - \item undoing the initial value transfer from the transaction sender to the recipient; -\end{enumerate} -Finally it is here that the \hubMod{} gets to -\begin{enumerate}[resume] - \item confirm data predicted in the \txnDataMod{} module and made available on transaction-rows e.g. - $\txStatusCode$, - $\txFinalRefundCounter$, - $\txLeftoverGas$; -\end{enumerate} +Finally the finalization phase is where the \hubMod{} gets to confirm data predicted in the \txnDataMod{} module and made available on transaction-rows e.g. +$\txStatusCode$, +$\txFinalRefundCounter$, +$\txLeftoverGas$, +\dots{} diff --git a/hub/tx_finl/peeking.tex b/hub/tx_finl/peeking.tex index d1133b2..23b6acc 100644 --- a/hub/tx_finl/peeking.tex +++ b/hub/tx_finl/peeking.tex @@ -2,27 +2,15 @@ \boxed{% \text{The constraints presented below assume } \left\{ \begin{array}{lcl} - \txExec _{i - 1} & = & 1 \\ - \txFinl _{i} & = & 1 \\ + \txExec _{i - \locTxFinlRoffLastExecutionRow} & = & 1 \\ + \txFinl _{i} & = & 1 \\ \end{array} \right. } \end{center} In other words we assume row $i$ is the first row of the transaction finalization phase. -The purpose of this transaction processing phase is to proceed to gas refunds for the sender address and pay the coinbase address. -In case of a transaction with status code $=0$ the sender address is reimbursed the transaction value (and the recipient sees its balance reduced by the same amount.) -As such we shall peek into -(\emph{a}) -the \texttt{from} account to proceed to the gas refund -(\emph{b}) -the \texttt{coinbase} account to proceed to gas payment. -What follows depends on whether the transaction succeeds or fails. If the transaction succeeds the above is sufficient. -The \zkEvm{} finishes by loading a single transaction row to confirm data. If the transaction fails we insert two extra rows: -(\emph{c}) -we again peek into the sender account and proceed to undo the initial value transfer by crediting the account in question with the transaction value; -(\emph{d}) -we peek into the transaction recipient account and decrement its balance by the transaction value. In all cases after peeking into accounts the final row of the current transaction loads the transaction data. The constraints below ensure the desired behaviour: +We impose the following constraints on peeking flags: \begin{enumerate} - \item \If $\cnWillRev_{i - 1} = 0$ \Then + \item we impose that \[ \left[ \begin{array}{cr} + & \peekAccount _{i + \locTxFinlSuccessSenderAccountOffset } \\ @@ -30,22 +18,8 @@ + & \peekTransaction _{i + \locTxFinlSuccessTransactionRowOffset } \\ \end{array} \right] = - \nsrTransactionFinalizationPhaseWontRevert - \] - \item \If $\cnWillRev_{i - 1} = 1$ \Then - \[ - \left[ \begin{array}{cr} - + & \peekAccount _{i + \locTxFinlFailureSenderAccountOffset } \\ - + & \peekAccount _{i + \locTxFinlFailureRecipientAccountOffset } \\ - + & \peekAccount _{i + \locTxFinlFailureCoinbaseAccountOffset } \\ - + & \peekTransaction _{i + \locTxFinlFailureTransactionRowOffset } \\ - \end{array} \right] - = - \nsrTransactionFinalizationPhaseWillRevert + \nsrTxFinl \] \end{enumerate} -\saNote{} Given the heartbeat constraints, the above has several \emph{implicit} consequences\footnote{which the implemenation need \textbf{not} enforce through new constraints}. The following are some of them. -\begin{itemize} - \item $\relativeBlockNumber$, $\txNum$, $\hubStamp$, $\txSkip$ remain constant during the finalization phase; - \item $\absTxNum$ and $\hubStamp$ will jump by 1 at the end of the phase; -\end{itemize} +\saNote{} +In the first account row we will deal with the sender account, in the second one with the coinbase account. diff --git a/hub/tx_finl/rows/_collage.tex b/hub/tx_finl/rows/_collage.tex new file mode 100644 index 0000000..2935fca --- /dev/null +++ b/hub/tx_finl/rows/_collage.tex @@ -0,0 +1,18 @@ +\begin{center} + \boxed{% + \text{The constraints presented below assume } + \left\{ \begin{array}{lcl} + \txExec _{i - \locTxFinlRoffLastExecutionRow} & = & 1 \\ + \txFinl _{i} & = & 1 \\ + \end{array} \right. + } +\end{center} +We deal with setting the contents of the various peeking rows. +\begin{description} + \item[\underline{\underline{Miscellaneous-row n$^°(\bm{i + \locTxFinlRoffAccSender})$:}}] + \input{tx_finl/rows/acc_sender} + \item[\underline{\underline{Coinbase account-row n$^°\bm{(i + \locTxFinlRoffAccCoinbase)}$:}}] + \input{tx_finl/rows/acc_coinbase} + \item[\underline{\underline{Transaction-row n$^°(\bm{i + \locTxFinlRoffTxn})$:}}] + \input{tx_finl/rows/txn} +\end{description} diff --git a/hub/tx_finl/rows/acc_coinbase.tex b/hub/tx_finl/rows/acc_coinbase.tex new file mode 100644 index 0000000..6d23b6b --- /dev/null +++ b/hub/tx_finl/rows/acc_coinbase.tex @@ -0,0 +1,28 @@ +we impose the following on the \textbf{coinbase account}: +\[ + \left\{\begin{array}{lcl} + \accAddress\high _{i + \locTxFinlRoffAccCoinbase} & = & \locTxFinlCoinbaseAddressHi \\ + \accAddress\low _{i + \locTxFinlRoffAccCoinbase} & = & \locTxFinlCoinbaseAddressLo \\ + \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxFinlRoffAccCoinbase}{\locFinlSuccessCoinbaseReward}} \\ + \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlRoffAccCoinbase}} \\ + \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlRoffAccCoinbase}} \\ + \multicolumn{3}{l}{\accSameDeployment {i}{\locTxFinlRoffAccCoinbase}} \\ + \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlRoffAccCoinbase}} \\ + \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlRoffAccCoinbase}} \\ + \multicolumn{3}{l}{ + \finalizationDomSubStamps { + anchorRow = i , + txnEndStamp = \locTransactionEndStamp , + relOffset = \locTxFinlRoffAccSender , + subOffset = 1 , + } + } \\ + % \standardDomSubStamps {i}{\locTxFinlSuccessCoinbaseAccountOffset}{1}} \\ + \end{array}\right. +\] +where \locFinlSuccessCoinbaseReward{} is a shorthand defined as follows: +\[ + \locFinlSuccessCoinbaseReward \define + \Big[ \txGasLimit_{i + \locTxFinlRoffTxn} - \txEffectiveRefund_{i + \locTxFinlRoffTxn} \Big] + \cdot \txPriorityFeePerGas_{i + \locTxFinlRoffTxn} +\] diff --git a/hub/tx_finl/rows/acc_sender.tex b/hub/tx_finl/rows/acc_sender.tex new file mode 100644 index 0000000..494f333 --- /dev/null +++ b/hub/tx_finl/rows/acc_sender.tex @@ -0,0 +1,27 @@ +we impose the following to the \textbf{sender account}: +\[ + \left\{\begin{array}{lcl} + \accAddress\high _{i + \locTxFinlRoffAccSender} & = & \locTxFinlSenderAddressHi \\ + \accAddress\low _{i + \locTxFinlRoffAccSender} & = & \locTxFinlSenderAddressLo \\ + \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxFinlRoffAccSender}{\locFinlSuccessSenderRefund}} \\ + \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlRoffAccSender}} \\ + \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlRoffAccSender}} \\ + \multicolumn{3}{l}{\accSameDeployment {i}{\locTxFinlRoffAccSender}} \\ + \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlRoffAccSender}} \\ + \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlRoffAccSender}} \\ + \multicolumn{3}{l}{ + \finalizationDomSubStamps { + anchorRow = i , + txnEndStamp = \locTransactionEndStamp , + relOffset = \locTxFinlRoffAccSender , + subOffset = 0 , + } + } \\ + \end{array}\right. +\] +where +\[ + \locFinlSuccessSenderRefund \define + \txGasPrice_{i + \locTxFinlRoffTxn} + \cdot \txEffectiveRefund_{i + \locTxFinlRoffTxn} +\] diff --git a/hub/tx_finl/rows/txn.tex b/hub/tx_finl/rows/txn.tex new file mode 100644 index 0000000..de34aa6 --- /dev/null +++ b/hub/tx_finl/rows/txn.tex @@ -0,0 +1,8 @@ +we load transaction data to have access to relevant fields but also to confirm data predicted in the \txnDataMod{}: +\[ + \left\{\begin{array}{lcll} + \txStatusCode _{i + \locTxFinlRoffTxn} & = & \locTransactionSuccess \\ + \txFinalRefundCounter _{i + \locTxFinlRoffTxn} & = & \refund _{i - \locTxFinlRoffLastExecutionRow} \\ + \txLeftoverGas _{i + \locTxFinlRoffTxn} & = & \gasNext _{i - \locTxFinlRoffLastExecutionRow} \\ + \end{array}\right. +\] diff --git a/hub/tx_finl/shorthands.tex b/hub/tx_finl/shorthands.tex new file mode 100644 index 0000000..59bcd2e --- /dev/null +++ b/hub/tx_finl/shorthands.tex @@ -0,0 +1,18 @@ +We define the following shorthands. +These only make sense provided that +$\txExec _{i - \locTxFinlRoffLastExecutionRow} = 0$ and $\txFinl _{i} = 1$, +which will be the standing assumption starting with the next section. +We draw the attention to the reader to +(\ref{hub: finalization phase: peeking}) +which justifies us using various row offsets and associating them with a transaction row. +\[ + \left\{ \begin{array}{lcl} + \locTransactionFailure & \define & \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \\ + \locTransactionSuccess & \define & 1 - \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \\ + \locTransactionEndStamp & \define & \txEndStamp _{i - \locTxFinlRoffLastExecutionRow} \\ + \locTxFinlSenderAddressHi & \define & \txFrom \high _{i + \locTxFinlRoffTxn} \\ + \locTxFinlSenderAddressLo & \define & \txFrom \low _{i + \locTxFinlRoffTxn} \\ + \locTxFinlCoinbaseAddressHi & \define & \txCoinbase \high _{i + \locTxFinlRoffTxn} \\ + \locTxFinlCoinbaseAddressLo & \define & \txCoinbase \low _{i + \locTxFinlRoffTxn} \\ + \end{array} \right. +\] diff --git a/hub/tx_finl/success.tex b/hub/tx_finl/success.tex deleted file mode 100644 index 3d41039..0000000 --- a/hub/tx_finl/success.tex +++ /dev/null @@ -1,94 +0,0 @@ -\begin{center} - \boxed{% - \text{The constraints presented below assume } - \left\{ \begin{array}{lcl} - \txExec _{i - 1} & = & 1 \\ - \txFinl _{i} & = & 1 \\ - \cnWillRev _{i - 1} & = & 0 \\ - \end{array} \right. - } -\end{center} -The constraints that follow pertain to transaction finalization when the underlying transaction exited with status code $1$. -\begin{description} - \item[\underline{\underline{Account row n$^°{(i + \locTxFinlSuccessSenderAccountOffset)}$:}}] - we impose the following to the \textbf{sender account}: - \[ - \left\{\begin{array}{lcl} - \accAddress\high _{i + \locTxFinlSuccessSenderAccountOffset} & = & \txFrom\high _{i + \locTxFinlSuccessTransactionRowOffset} \\ - \accAddress\low _{i + \locTxFinlSuccessSenderAccountOffset} & = & \txFrom\low _{i + \locTxFinlSuccessTransactionRowOffset} \\ - \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxFinlSuccessSenderAccountOffset}{\locFinlSuccessSenderRefund}} \\ - \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlSuccessSenderAccountOffset}} \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlSuccessSenderAccountOffset}} \\ - \multicolumn{3}{l}{\accSameDeployment {i}{\locTxFinlSuccessSenderAccountOffset}} \\ - \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlSuccessSenderAccountOffset}} \\ - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlSuccessSenderAccountOffset}} \\ - \multicolumn{3}{l}{ - \standardDomSubStamps { - anchorRow = i, - relOffset = \locTxFinlSuccessSenderAccountOffset, - domOffset = 0, - } - } \\ - % \multicolumn{3}{l}{\accOpening {\locTxFinlSuccessSenderAccountOffset} _{i}} \\ - \end{array}\right. - \] - where - \[ - \locFinlSuccessSenderRefund \define - \txGasPrice_{i + \locTxFinlSuccessTransactionRowOffset} - \cdot \txEffectiveRefund_{i + \locTxFinlSuccessTransactionRowOffset} - \] - \item[\underline{\underline{Account row n$^°{(i + \locTxFinlSuccessCoinbaseAccountOffset)}$:}}] - we impose the following to the \textbf{coinbase account}: - \[ - \left\{\begin{array}{lcl} - \accAddress\high _{i + \locTxFinlSuccessCoinbaseAccountOffset} & = & \txCoinbase\high _{i + \locTxFinlSuccessTransactionRowOffset} \\ - \accAddress\low _{i + \locTxFinlSuccessCoinbaseAccountOffset} & = & \txCoinbase\low _{i + \locTxFinlSuccessTransactionRowOffset} \\ - \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxFinlSuccessCoinbaseAccountOffset}{\locFinlSuccessCoinbaseReward}} \\ - \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlSuccessCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlSuccessCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{\accSameDeployment {i}{\locTxFinlSuccessCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlSuccessCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlSuccessCoinbaseAccountOffset}} \\ - \multicolumn{3}{l}{ - \standardDomSubStamps { - anchorRow = i, - relOffset = \locTxFinlSuccessCoinbaseAccountOffset, - domOffset = 1, - } - } \\ - % \standardDomSubStamps {i}{\locTxFinlSuccessCoinbaseAccountOffset}{1}} \\ - \end{array}\right. - \] - where \locFinlSuccessCoinbaseReward{} is a shorthand defined as follows: - \[ - \locFinlSuccessCoinbaseReward \define - \left[ \begin{array}{cl} - \cdot & \txPriorityFeePerGas_{i + \locTxFinlSuccessTransactionRowOffset} \\ - \cdot & (\txGasLimit_{i + \locTxFinlSuccessTransactionRowOffset} - \txEffectiveRefund_{i + \locTxFinlSuccessTransactionRowOffset}) \\ - \end{array} \right] - \] - % \begin{enumerate} - % \item \If $\txIsTypeTwo_{i + \locTxFinlSuccessTransactionRowOffset} = 0$ \Then - % \[ - % \locFinlSuccessCoinbaseReward \define - % \txGasPrice_{i + \locTxFinlSuccessTransactionRowOffset} - % \cdot (\txGasLimit_{i + \locTxFinlSuccessTransactionRowOffset} - \txEffectiveRefund_{i + \locTxFinlSuccessTransactionRowOffset}) - % \] - % \item \If $\txIsTypeTwo_{i + \locTxFinlSuccessTransactionRowOffset} = 1$ \Then - % \[ - % \locFinlSuccessCoinbaseReward \define - % (\txGasPrice_{i + \locTxFinlSuccessTransactionRowOffset} - \txBasefee_{i + \locTxFinlSuccessTransactionRowOffset}) - % \cdot (\txGasLimit_{i + \locTxFinlSuccessTransactionRowOffset} - \txEffectiveRefund_{i + \locTxFinlSuccessTransactionRowOffset}) - % \] - % \end{enumerate} - \item[\underline{\underline{Transaction row n$^°{(i + \locTxFinlSuccessTransactionRowOffset)}$:}}] - we load transaction data to have access to relevant fields but also to confirm data predicted in the \txnDataMod{}: - \[ - \left\{\begin{array}{lcll} - \txStatusCode _{i + \locTxFinlSuccessTransactionRowOffset} & = & \rOne \\ - \txFinalRefundCounter _{i + \locTxFinlSuccessTransactionRowOffset} & = & \refund _{i - 1} \\ - \txLeftoverGas _{i + \locTxFinlSuccessTransactionRowOffset} & = & \gasNext _{i - 1} \\ - \end{array}\right. - \] -\end{description} diff --git a/pkg/env.sty b/pkg/env.sty index a54abf9..cf95a72 100644 --- a/pkg/env.sty +++ b/pkg/env.sty @@ -69,6 +69,7 @@ \newcommand{\hubLambda} {\redm{\lambda}} % dom stamp multiplier \newcommand{\hubTau} {\redm{\tau}} % stack stamp multiplier \newcommand{\revertEpsilon} {\redm{\epsilon_{\text{rev}}}} +\newcommand{\finalizationEpsilon} {\redm{\epsilon_{\text{finl}}}} \newcommand{\selfdestructEpsilon} {\redm{\epsilon_{\text{selfdest}}}} % \newcommand{\cPreWarming} {\red{c}_\red{pw}} % \newcommand{\cInit} {\red{c}_\red{in}} diff --git a/pkg/xkeyval_macros/dom_sub_stamps.sty b/pkg/xkeyval_macros/dom_sub_stamps.sty index a305cbf..4e3baa7 100644 --- a/pkg/xkeyval_macros/dom_sub_stamps.sty +++ b/pkg/xkeyval_macros/dom_sub_stamps.sty @@ -1,11 +1,13 @@ \makeatletter -\define@cmdkey [DOMSUB] {var} {anchorRow} {} -\define@cmdkey [DOMSUB] {var} {relOffset} {} -\define@cmdkey [DOMSUB] {var} {domOffset} {} -\define@cmdkey [DOMSUB] {var} {subOffset} {} -\define@cmdkey [DOMSUB] {var} {revertStamp} {} -\define@cmdkey [DOMSUB] {var} {childRevertStamp} {} +\define@cmdkey [DOMSUB] {var} {anchorRow} {} +\define@cmdkey [DOMSUB] {var} {relOffset} {} +\define@cmdkey [DOMSUB] {var} {domOffset} {} +\define@cmdkey [DOMSUB] {var} {subOffset} {} +\define@cmdkey [DOMSUB] {var} {revertStamp} {} +\define@cmdkey [DOMSUB] {var} {childRevertStamp} {} +\define@cmdkey [DOMSUB] {var} {txnEndStamp} {} + \presetkeys [DOMSUB] {var} { @@ -15,6 +17,7 @@ childRevertStamp = \missingParameter, domOffset = \missingParameter, subOffset = \missingParameter, + txnEndStamp = \missingParameter, }{} % \cmdDOMSUB@var@anchorRow @@ -43,7 +46,7 @@ \standardDomSubStampsName _{\cmdDOMSUB@var@anchorRow} \left[ \begin{array}{ll} \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ - \utt{Dom offset:} & \cmdDOMSUB@var@domOffset \\ + \utt{Dom offset:} & \cmdDOMSUB@var@domOffset \\ \end{array} \right] } @@ -52,10 +55,10 @@ \setkeys[DOMSUB]{var}{#1} \genericUndoingDomSubStampsName _{\cmdDOMSUB@var@anchorRow} \left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ - \utt{Revert stamp:} & \cmdDOMSUB@var@revertStamp \\ - \utt{Dom offset:} & \cmdDOMSUB@var@domOffset \\ - \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ + \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ + \utt{Revert stamp:} & \cmdDOMSUB@var@revertStamp \\ + \utt{Dom offset:} & \cmdDOMSUB@var@domOffset \\ + \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ \end{array} \right] } @@ -72,8 +75,8 @@ \setkeys[DOMSUB]{var}{#1} \revertDomSubStampsName _{\cmdDOMSUB@var@anchorRow} \left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ - \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ + \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ + \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ \end{array} \right] } @@ -83,14 +86,25 @@ % subOffset = , % } +\newcommand{\finalizationDomSubStampsName} {\stampSignifier\texttt{finalizationDomSubStamps}} +\newcommand{\finalizationDomSubStamps} [1] { + \setkeys[DOMSUB]{var}{#1} + \finalizationDomSubStampsName _{\cmdDOMSUB@var@anchorRow} +\left[ \begin{array}{ll} + \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ + \utt{Txn. end stamp:} & \cmdDOMSUB@var@txnEndStamp \\ + \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ +\end{array} \right] +} + \newcommand{\revertWithChildFailureDomSubStampsName} {\stampSignifier\texttt{revertWithChildFailureDomSubStamps}} \newcommand{\revertWithChildFailureDomSubStamps} [1] { \setkeys[DOMSUB]{var}{#1} \revertWithChildFailureDomSubStampsName _{\cmdDOMSUB@var@anchorRow} \left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ + \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ \utt{Child revert stamp:} & \cmdDOMSUB@var@childRevertStamp \\ - \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ + \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ \end{array} \right] } From 8f1d3b0c583c8cbc1d1386afa28d71ecdff8555f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 29 Nov 2024 14:03:40 +0700 Subject: [PATCH 09/18] fix: restoring hub/_inputs.tex --- hub/_inputs.tex | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/hub/_inputs.tex b/hub/_inputs.tex index 6f975d1..089d090 100644 --- a/hub/_inputs.tex +++ b/hub/_inputs.tex @@ -6,19 +6,19 @@ \section{Introduction} \label{hub: intro} \input{intro} -% \input{columns/_inputs} % Done -% \input{heartbeat/_inputs} % Done -% \input{generalities/_inputs} % Done -% \input{stack/_inputs} % Done -% \input{context/_inputs} % Done -% \input{account/_inputs} % Done -% \input{storage/_inputs} % Done -% \input{misc/_inputs} % Todo -% \input{scenario/_inputs} % Wip -% \input{tx_skip/_inputs} % Done -% \input{tx_prewarm/_inputs} % Done +\input{columns/_inputs} % Done +\input{heartbeat/_inputs} % Done +\input{generalities/_inputs} % Done +\input{stack/_inputs} % Done +\input{context/_inputs} % Done +\input{account/_inputs} % Done +\input{storage/_inputs} % Done +\input{misc/_inputs} % Todo +\input{scenario/_inputs} % Wip +\input{tx_skip/_inputs} % Done +\input{tx_prewarm/_inputs} % Done \input{tx_init/_inputs} % Done -% \input{instruction_handling/_inputs} % Wip +\input{instruction_handling/_inputs} % Wip \input{tx_finl/_inputs} % Done -% \input{consistencies/_inputs} % Wip -% \input{lookups/_inputs} % Wip +\input{consistencies/_inputs} % Wip +\input{lookups/_inputs} % Wip From 1b54458b20cbd2a78f31dec866c76ab0846746f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 29 Nov 2024 14:33:56 +0700 Subject: [PATCH 10/18] fix: finalizationDomSubStamps use TX_END_STAMP by default --- hub/tx_finl/rows/acc_coinbase.tex | 1 - hub/tx_finl/rows/acc_sender.tex | 1 - pkg/xkeyval_macros/dom_sub_stamps.sty | 1 - 3 files changed, 3 deletions(-) diff --git a/hub/tx_finl/rows/acc_coinbase.tex b/hub/tx_finl/rows/acc_coinbase.tex index 6d23b6b..79a7201 100644 --- a/hub/tx_finl/rows/acc_coinbase.tex +++ b/hub/tx_finl/rows/acc_coinbase.tex @@ -12,7 +12,6 @@ \multicolumn{3}{l}{ \finalizationDomSubStamps { anchorRow = i , - txnEndStamp = \locTransactionEndStamp , relOffset = \locTxFinlRoffAccSender , subOffset = 1 , } diff --git a/hub/tx_finl/rows/acc_sender.tex b/hub/tx_finl/rows/acc_sender.tex index 494f333..d915e14 100644 --- a/hub/tx_finl/rows/acc_sender.tex +++ b/hub/tx_finl/rows/acc_sender.tex @@ -12,7 +12,6 @@ \multicolumn{3}{l}{ \finalizationDomSubStamps { anchorRow = i , - txnEndStamp = \locTransactionEndStamp , relOffset = \locTxFinlRoffAccSender , subOffset = 0 , } diff --git a/pkg/xkeyval_macros/dom_sub_stamps.sty b/pkg/xkeyval_macros/dom_sub_stamps.sty index 4e3baa7..77826d1 100644 --- a/pkg/xkeyval_macros/dom_sub_stamps.sty +++ b/pkg/xkeyval_macros/dom_sub_stamps.sty @@ -92,7 +92,6 @@ \finalizationDomSubStampsName _{\cmdDOMSUB@var@anchorRow} \left[ \begin{array}{ll} \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ - \utt{Txn. end stamp:} & \cmdDOMSUB@var@txnEndStamp \\ \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ \end{array} \right] } From 522706aef9eded5cd16f52552122e3a4444ac7f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 29 Nov 2024 14:35:01 +0700 Subject: [PATCH 11/18] ras --- hub/tx_finl/_local.tex | 1 - hub/tx_finl/shorthands.tex | 13 ++++++------- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/hub/tx_finl/_local.tex b/hub/tx_finl/_local.tex index 0e83254..32921b1 100644 --- a/hub/tx_finl/_local.tex +++ b/hub/tx_finl/_local.tex @@ -7,7 +7,6 @@ \def\locTransactionFailure {\col{transaction\_failure}} \def\locTransactionSuccess {\col{transaction\_success}} -\def\locTransactionEndStamp {\col{transaction\_end\_stamp}} \def\locTxFinlSenderAddressHi {\col{sender\_addr\_hi}} \def\locTxFinlSenderAddressLo {\col{sender\_addr\_lo}} diff --git a/hub/tx_finl/shorthands.tex b/hub/tx_finl/shorthands.tex index 59bcd2e..0c1742a 100644 --- a/hub/tx_finl/shorthands.tex +++ b/hub/tx_finl/shorthands.tex @@ -7,12 +7,11 @@ which justifies us using various row offsets and associating them with a transaction row. \[ \left\{ \begin{array}{lcl} - \locTransactionFailure & \define & \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \\ - \locTransactionSuccess & \define & 1 - \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \\ - \locTransactionEndStamp & \define & \txEndStamp _{i - \locTxFinlRoffLastExecutionRow} \\ - \locTxFinlSenderAddressHi & \define & \txFrom \high _{i + \locTxFinlRoffTxn} \\ - \locTxFinlSenderAddressLo & \define & \txFrom \low _{i + \locTxFinlRoffTxn} \\ - \locTxFinlCoinbaseAddressHi & \define & \txCoinbase \high _{i + \locTxFinlRoffTxn} \\ - \locTxFinlCoinbaseAddressLo & \define & \txCoinbase \low _{i + \locTxFinlRoffTxn} \\ + \locTransactionFailure & \define & \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \\ + \locTransactionSuccess & \define & 1 - \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \vspace{2mm} \\ + \locTxFinlSenderAddressHi & \define & \txFrom \high _{i + \locTxFinlRoffTxn} \\ + \locTxFinlSenderAddressLo & \define & \txFrom \low _{i + \locTxFinlRoffTxn} \\ + \locTxFinlCoinbaseAddressHi & \define & \txCoinbase \high _{i + \locTxFinlRoffTxn} \\ + \locTxFinlCoinbaseAddressLo & \define & \txCoinbase \low _{i + \locTxFinlRoffTxn} \\ \end{array} \right. \] From b16a5ab863e5dc81a95d4d5523b828fecf774b2c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 29 Nov 2024 20:46:57 +0700 Subject: [PATCH 12/18] fix: review changes --- hub/_inputs.tex | 28 +++++++++++----------- hub/generalities/revert/constants.tex | 14 ++++++++--- hub/tx_finl/_inputs.tex | 2 +- hub/tx_finl/_local.tex | 1 - hub/tx_finl/rows/_collage.tex | 2 +- hub/tx_finl/rows/acc_coinbase.tex | 6 ++--- hub/tx_finl/rows/txn.tex | 6 ++--- hub/tx_finl/shorthands.tex | 1 - hub/tx_init/_local.tex | 6 ++--- hub/tx_init/rows/acc_recipient_undoing.tex | 26 ++++++++++---------- hub/tx_init/rows/acc_recipient_value.tex | 18 +++++++++++--- hub/tx_init/rows/acc_sender_gas.tex | 13 +++++++++- hub/tx_init/rows/acc_sender_undoing.tex | 26 ++++++++++---------- hub/tx_init/rows/txn.tex | 3 +-- 14 files changed, 90 insertions(+), 62 deletions(-) diff --git a/hub/_inputs.tex b/hub/_inputs.tex index 089d090..6f975d1 100644 --- a/hub/_inputs.tex +++ b/hub/_inputs.tex @@ -6,19 +6,19 @@ \section{Introduction} \label{hub: intro} \input{intro} -\input{columns/_inputs} % Done -\input{heartbeat/_inputs} % Done -\input{generalities/_inputs} % Done -\input{stack/_inputs} % Done -\input{context/_inputs} % Done -\input{account/_inputs} % Done -\input{storage/_inputs} % Done -\input{misc/_inputs} % Todo -\input{scenario/_inputs} % Wip -\input{tx_skip/_inputs} % Done -\input{tx_prewarm/_inputs} % Done +% \input{columns/_inputs} % Done +% \input{heartbeat/_inputs} % Done +% \input{generalities/_inputs} % Done +% \input{stack/_inputs} % Done +% \input{context/_inputs} % Done +% \input{account/_inputs} % Done +% \input{storage/_inputs} % Done +% \input{misc/_inputs} % Todo +% \input{scenario/_inputs} % Wip +% \input{tx_skip/_inputs} % Done +% \input{tx_prewarm/_inputs} % Done \input{tx_init/_inputs} % Done -\input{instruction_handling/_inputs} % Wip +% \input{instruction_handling/_inputs} % Wip \input{tx_finl/_inputs} % Done -\input{consistencies/_inputs} % Wip -\input{lookups/_inputs} % Wip +% \input{consistencies/_inputs} % Wip +% \input{lookups/_inputs} % Wip diff --git a/hub/generalities/revert/constants.tex b/hub/generalities/revert/constants.tex index 4e05029..12f10d9 100644 --- a/hub/generalities/revert/constants.tex +++ b/hub/generalities/revert/constants.tex @@ -1,17 +1,25 @@ The re-ordering arguments involving dominant and subordinate stamps (i.e. $\domStamp$ and $\subStamp$) rely on some constants which we define here: \begin{itemize} \item $\hubTau = 8$ - \item $\hubLambda = 11$ + \item $\hubLambda = 16$ \item $\revertEpsilon = 8$ \item $\finalizationEpsilon = 9$ \item $\selfdestructEpsilon = 10$ \end{itemize} Two criteria have to be considered in setting these constants. Let us define \col{max} as the maximum ``$\domStamp$''-offset encountered in constraints +that is +$\col{max} = \max \big\{ \, \col{d} \, \big \}$ +where the maximum is taken over all \col{d} which appear in a constraint of the form $\domStamp \equiv \hubLambda \cdot \col{h} + \col{d}$. +The constants above have to satisfy \begin{enumerate} - \item for any ``dom''-offset \col{d} used in a constraint to set $\domStamp \equiv \hubLambda \cdot \col{h} + \col{d}$ (where $\col{h} \equiv \hubStamp$) it should hold that $0 \leq \col{d} < \revertEpsilon$ - \item $\col{max} < \revertEpsilon < \finalizationEpsilon < \selfdestructEpsilon < \hubLambda$ where \col{max} is the maximum ``$\domStamp$''-offset encountered in constraints (i.e. the + \item $0 \leq \col{max} < \revertEpsilon$ + \item $0 \leq \finalizationEpsilon < \selfdestructEpsilon < \hubLambda$ \end{enumerate} +The constants proposed above satisfy the stronger condition +\[ + 0 \leq \col{max} < \revertEpsilon < \finalizationEpsilon < \selfdestructEpsilon < \hubLambda +\] Indeed reverting should happen before gas refunds and before enacting any \inst{SELFDESTRUCT}'s and ``\texttt{doing}''-actions ``taken in the moment'' should not interfere with ``\texttt{undoing}''-actions scheduled for post roll back. \begin{itemize} \item $\emptyKeccakHi = \texttt{0xc5d2460186f7233c927e7db2dcc703c0}$ diff --git a/hub/tx_finl/_inputs.tex b/hub/tx_finl/_inputs.tex index cdc1b14..d33f66e 100644 --- a/hub/tx_finl/_inputs.tex +++ b/hub/tx_finl/_inputs.tex @@ -1,5 +1,5 @@ \input{tx_finl/_local} -\section{Finalization phase \lispDone{}} \label{hub: finalization phase} +\section{Finalization phase \lispTodo{}} \label{hub: finalization phase} \subsection{Introduction \lispNone{}} \label{hub: finalization phase: intro} \input{tx_finl/intro} \subsection{Shorthands \lispTodo{}} \label{hub: finalization phase: shorthands} \input{tx_finl/shorthands} \subsection{Peeking flags \lispTodo{}} \label{hub: finalization phase: peeking} \input{tx_finl/peeking} diff --git a/hub/tx_finl/_local.tex b/hub/tx_finl/_local.tex index 32921b1..99dd10a 100644 --- a/hub/tx_finl/_local.tex +++ b/hub/tx_finl/_local.tex @@ -5,7 +5,6 @@ \def\locTxFinlRoffAccCoinbase {\yellowm{1}} \def\locTxFinlRoffTxn {\orangem{2}} -\def\locTransactionFailure {\col{transaction\_failure}} \def\locTransactionSuccess {\col{transaction\_success}} \def\locTxFinlSenderAddressHi {\col{sender\_addr\_hi}} diff --git a/hub/tx_finl/rows/_collage.tex b/hub/tx_finl/rows/_collage.tex index 2935fca..ce1d866 100644 --- a/hub/tx_finl/rows/_collage.tex +++ b/hub/tx_finl/rows/_collage.tex @@ -9,7 +9,7 @@ \end{center} We deal with setting the contents of the various peeking rows. \begin{description} - \item[\underline{\underline{Miscellaneous-row n$^°(\bm{i + \locTxFinlRoffAccSender})$:}}] + \item[\underline{\underline{Sender account-row n$^°(\bm{i + \locTxFinlRoffAccSender})$:}}] \input{tx_finl/rows/acc_sender} \item[\underline{\underline{Coinbase account-row n$^°\bm{(i + \locTxFinlRoffAccCoinbase)}$:}}] \input{tx_finl/rows/acc_coinbase} diff --git a/hub/tx_finl/rows/acc_coinbase.tex b/hub/tx_finl/rows/acc_coinbase.tex index 79a7201..a0a34ac 100644 --- a/hub/tx_finl/rows/acc_coinbase.tex +++ b/hub/tx_finl/rows/acc_coinbase.tex @@ -11,9 +11,9 @@ \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlRoffAccCoinbase}} \\ \multicolumn{3}{l}{ \finalizationDomSubStamps { - anchorRow = i , - relOffset = \locTxFinlRoffAccSender , - subOffset = 1 , + anchorRow = i , + relOffset = \locTxFinlRoffAccCoinbase , + subOffset = 1 , } } \\ % \standardDomSubStamps {i}{\locTxFinlSuccessCoinbaseAccountOffset}{1}} \\ diff --git a/hub/tx_finl/rows/txn.tex b/hub/tx_finl/rows/txn.tex index de34aa6..1eb315a 100644 --- a/hub/tx_finl/rows/txn.tex +++ b/hub/tx_finl/rows/txn.tex @@ -1,8 +1,8 @@ we load transaction data to have access to relevant fields but also to confirm data predicted in the \txnDataMod{}: \[ \left\{\begin{array}{lcll} - \txStatusCode _{i + \locTxFinlRoffTxn} & = & \locTransactionSuccess \\ - \txFinalRefundCounter _{i + \locTxFinlRoffTxn} & = & \refund _{i - \locTxFinlRoffLastExecutionRow} \\ - \txLeftoverGas _{i + \locTxFinlRoffTxn} & = & \gasNext _{i - \locTxFinlRoffLastExecutionRow} \\ + \txStatusCode _{i + \locTxFinlRoffTxn} & = & \locTransactionSuccess \\ + \txFinalRefundCounter _{i + \locTxFinlRoffTxn} & = & \refund \new _{i - \locTxFinlRoffLastExecutionRow} \\ + \txLeftoverGas _{i + \locTxFinlRoffTxn} & = & \gasNext _{i - \locTxFinlRoffLastExecutionRow} \\ \end{array}\right. \] diff --git a/hub/tx_finl/shorthands.tex b/hub/tx_finl/shorthands.tex index 0c1742a..0ad7e10 100644 --- a/hub/tx_finl/shorthands.tex +++ b/hub/tx_finl/shorthands.tex @@ -7,7 +7,6 @@ which justifies us using various row offsets and associating them with a transaction row. \[ \left\{ \begin{array}{lcl} - \locTransactionFailure & \define & \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \\ \locTransactionSuccess & \define & 1 - \cnWillRev _{i - \locTxFinlRoffLastExecutionRow} \vspace{2mm} \\ \locTxFinlSenderAddressHi & \define & \txFrom \high _{i + \locTxFinlRoffTxn} \\ \locTxFinlSenderAddressLo & \define & \txFrom \low _{i + \locTxFinlRoffTxn} \\ diff --git a/hub/tx_init/_local.tex b/hub/tx_init/_local.tex index efc2291..436a51a 100644 --- a/hub/tx_init/_local.tex +++ b/hub/tx_init/_local.tex @@ -1,6 +1,6 @@ -\def\locTransactionWillRevert {\col{transaction\_will\_revert}} -\def\locTransactionWontRevert {\col{transaction\_wont\_revert}} -\def\locTransactionRevertStamp {\col{transaction\_revert\_stamp}} +\def\locTransactionWillRevert {\col{txn\_will\_revert}} +\def\locTransactionWontRevert {\col{txn\_wont\_revert}} +\def\locTransactionRevertStamp {\col{txn\_revert\_stamp}} \def\locTxInitGasCost {\col{gas\_cost}} \def\locTxInitValue {\col{value}} diff --git a/hub/tx_init/rows/acc_recipient_undoing.tex b/hub/tx_init/rows/acc_recipient_undoing.tex index dbb4dfe..58e0a9b 100644 --- a/hub/tx_init/rows/acc_recipient_undoing.tex +++ b/hub/tx_init/rows/acc_recipient_undoing.tex @@ -1,19 +1,19 @@ \If $\locTransactionWillRevert = 1$ \Then we impose that \[ - \left\{ \begin{array}{lcl} - \multicolumn{3}{l}{\accSameAddr {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ - \multicolumn{3}{l}{\accUndoBalanceUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ - \multicolumn{3}{l}{\accUndoNonceUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ - \multicolumn{3}{l}{\accUndoCodeUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ - \multicolumn{3}{l}{\accSameWarmth {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ - \multicolumn{3}{l}{\accSameDeploymentNumber {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ - \multicolumn{3}{l}{\accUndoDeploymentStatusUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \left\{ \begin{array}{lcll} + \multicolumn{4}{l}{\accSameAddr {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{4}{l}{\accUndoBalanceUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \multicolumn{4}{l}{\accUndoNonceUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{4}{l}{\accUndoCodeUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{4}{l}{\accSameWarmth {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{4}{l}{\accSameDeploymentNumber {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \multicolumn{4}{l}{\accUndoDeploymentStatusUpdate {i}{\locTxInitRoffAccUndoingRecipientValueReception}{\locTxInitRoffAccDoingRecipientValueReception}} \\ %%%% - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ - \accRomLexFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \\ - \accTrmFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \\ - \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 \vspace{2mm} \\ - \multicolumn{3}{l}{ + \multicolumn{4}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccUndoingRecipientValueReception}} \\ + \accRomLexFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 & (\trash) \\ + \accTrmFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 & (\trash) \\ + \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingRecipientValueReception} & = & 0 & (\trash) \vspace{2mm} \\ + \multicolumn{4}{l}{ \revertWithChildFailureDomSubStamps { anchorRow = i , relOffset = \locTxInitRoffAccUndoingRecipientValueReception , diff --git a/hub/tx_init/rows/acc_recipient_value.tex b/hub/tx_init/rows/acc_recipient_value.tex index 4ed6b13..e94ab2b 100644 --- a/hub/tx_init/rows/acc_recipient_value.tex +++ b/hub/tx_init/rows/acc_recipient_value.tex @@ -25,7 +25,18 @@ } \\ \end{array} \right. \] -We must distinguish between +\saNote{} \label{hub: initialization phase: why we trim the recipient address} +The recipient address as contained in the pair +\[ + \big( \locTxInitRecipientAddressHi, \locTxInitRecipientAddressLo \big) +\] +whether coming from the \texttt{to} field of the transaction +or being deduced from the \texttt{sender} address and its current \texttt{nonce}, +requires no trimming for the same reason that the sender address requires no trimming. +Regardless, we trim said recipient address for reasons already expressed in +note~(\ref{hub: initialization phase: why we trim the sender address}). + +\noindent We must distinguish between message calls ($\locTxInitIsMessageCall~=~1$) and deployments ($\locTxInitIsDeployment~=~1$). \begin{description} @@ -47,9 +58,9 @@ \item[\underline{Nonce:}] we impose \[ - \left\{ \begin{array}{lclr} + \left\{ \begin{array}{lcl} \multicolumn{3}{l}{\accIncrementNonce {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ - \accNonce_{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 & (\trash) \vspace{2mm} \\ + \accNonce_{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 \\ \end{array} \right. \] \item[\underline{Code:}] @@ -75,6 +86,7 @@ \[ \left\{ \begin{array}{lclr} \multicolumn{3}{l}{\accIncrementDeploymentNumber {i}{\locTxInitRoffAccDoingRecipientValueReception}} \\ + \accDeploymentNumber _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 \\ \accDeploymentStatus _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & 0 & (\trash) \\ \accDeploymentStatus\new _{i + \locTxInitRoffAccDoingRecipientValueReception} & = & \rOne \\ \end{array} \right. diff --git a/hub/tx_init/rows/acc_sender_gas.tex b/hub/tx_init/rows/acc_sender_gas.tex index e1ad059..fcd4b8e 100644 --- a/hub/tx_init/rows/acc_sender_gas.tex +++ b/hub/tx_init/rows/acc_sender_gas.tex @@ -14,7 +14,7 @@ \multicolumn{3}{l}{\accSameDeployment {i}{\locTxInitRoffAccDoingSndPayGas}} \\ \multicolumn{3}{l}{\accTurnOnWarmth {i}{\locTxInitRoffAccDoingSndPayGas}} \\ \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccDoingSndPayGas}} \\ - \multicolumn{3}{l}{\accIsntPrecompile {i}{\locTxInitRoffAccDoingSndPayGas}} & (\trash) \\ + \multicolumn{3}{l}{\accIsntPrecompile {i}{\locTxInitRoffAccDoingSndPayGas}} \\ \multicolumn{3}{l}{ \standardDomSubStamps { anchorRow = i , @@ -28,3 +28,14 @@ \[ \accHasCode _{i + \locTxInitRoffAccDoingSndPayGas} = 0 \] +\saNote{} \label{hub: initialization phase: why we trim the sender address} +We impose address trimming constraints \emph{in spite} of the fact that the pair +\[ + \big( \locTxInitSenderAddressHi, \locTxInitSenderAddressLo \big) +\] +both of whose components come from the \txnDataMod{} module, +necessarily constitutes valid high and low parts of an address. +The reason for this precaution is that the present row \emph{may} constitute the first occurrence of this particular address in the present conflation of blocks. +Imposing trimming \emph{here} ensures that +constraint~(\ref{hub: consistency: account: trimming first appearance of an address}) +will automatically hold \emph{if} this row turns out to be the first encounter with that particular address. diff --git a/hub/tx_init/rows/acc_sender_undoing.tex b/hub/tx_init/rows/acc_sender_undoing.tex index 1ecf9c1..0b6f42c 100644 --- a/hub/tx_init/rows/acc_sender_undoing.tex +++ b/hub/tx_init/rows/acc_sender_undoing.tex @@ -1,19 +1,19 @@ \If $\locTransactionWillRevert = 1$ \Then we impose that \[ - \left\{ \begin{array}{lcl} - \multicolumn{3}{l}{\accSameAddr {i}{\locTxInitRoffAccUndoingSenderValueTransfer}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ - \multicolumn{3}{l}{\accUndoBalanceUpdate {i}{\locTxInitRoffAccUndoingSenderValueTransfer}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ - \multicolumn{3}{l}{\accSameNonce {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ - \multicolumn{3}{l}{\accSameCode {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ - \multicolumn{3}{l}{\accSameWarmth {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ - \multicolumn{3}{l}{\accSameDeploymentNumber {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ - \multicolumn{3}{l}{\accSameDeploymentStatus {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \left\{ \begin{array}{lcll} + \multicolumn{4}{l}{\accSameAddr {i}{\locTxInitRoffAccUndoingSenderValueTransfer}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{4}{l}{\accUndoBalanceUpdate {i}{\locTxInitRoffAccUndoingSenderValueTransfer}{\locTxInitRoffAccDoingSenderValueTransfer}} \\ + \multicolumn{4}{l}{\accSameNonce {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{4}{l}{\accSameCode {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{4}{l}{\accSameWarmth {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{4}{l}{\accSameDeploymentNumber {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \multicolumn{4}{l}{\accSameDeploymentStatus {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ %%%% - \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ - \accRomLexFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \\ - \accTrmFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \\ - \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 \vspace{2mm} \\ - \multicolumn{3}{l}{ + \multicolumn{4}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxInitRoffAccUndoingSenderValueTransfer}} \\ + \accRomLexFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 & (\trash) \\ + \accTrmFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 & (\trash) \\ + \accRlpAddrFlag _{i + \locTxInitRoffAccUndoingSenderValueTransfer} & = & 0 & (\trash) \vspace{2mm} \\ + \multicolumn{4}{l}{ \revertWithChildFailureDomSubStamps { anchorRow = i , relOffset = \locTxInitRoffAccUndoingSenderValueTransfer , diff --git a/hub/tx_init/rows/txn.tex b/hub/tx_init/rows/txn.tex index bc7925d..8b6b183 100644 --- a/hub/tx_init/rows/txn.tex +++ b/hub/tx_init/rows/txn.tex @@ -12,8 +12,7 @@ \item[\underline{Justifying $\txInitialBalance$:}] we impose that $\txInitialBalance _{i + \locTxInitRoffTxn} = \accBalance _{i + \locTxInitRoffAccDoingSndPayGas}$ \item[\underline{Justifying \txStatusCode{}:}] - cannot be set at the moment\footnote{We \textbf{could} actually set the status code of the transaction at the present time: - \[ \txStatusCode _{i + \locTxInitRoffTxn} = 1 - \cnWillRev _{i + \locTxInitRoffTxn + 1} ~ (\trash) \]}; + cannot be set at the moment\footnote{We \textbf{could} actually set the status code of the transaction at the present time as it coincides with \locTransactionWontRevert{}.}; \item[\underline{Justifying \txNonce{}:}] we impose $\txNonce_{i + \locTxInitRoffTxn} = \accNonce_{i + \locTxInitRoffAccDoingSndPayGas}$; \item[\underline{Justifying $\txLeftoverGas$:}] From 2de5034680876141e40477ddf0ae059a01418d07 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 2 Dec 2024 11:20:57 +0700 Subject: [PATCH 13/18] fix: decrementing sub stamp offsets for \finalizationDomSubStamps --- hub/tx_finl/rows/_collage.tex | 5 +++++ hub/tx_finl/rows/acc_coinbase.tex | 2 +- hub/tx_finl/rows/acc_sender.tex | 2 +- 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/hub/tx_finl/rows/_collage.tex b/hub/tx_finl/rows/_collage.tex index ce1d866..0644ddb 100644 --- a/hub/tx_finl/rows/_collage.tex +++ b/hub/tx_finl/rows/_collage.tex @@ -13,6 +13,11 @@ \input{tx_finl/rows/acc_sender} \item[\underline{\underline{Coinbase account-row n$^°\bm{(i + \locTxFinlRoffAccCoinbase)}$:}}] \input{tx_finl/rows/acc_coinbase} +\end{description} +\saNote{} +This is the one time in the \zkEvm{} specification where the \texttt{Sub stamp offset}'s are listed in decrementing order. +The interpretation is that (in the re-ordered trace) the sender refund ought to happen before the coinbase reward. +\begin{description} \item[\underline{\underline{Transaction-row n$^°(\bm{i + \locTxFinlRoffTxn})$:}}] \input{tx_finl/rows/txn} \end{description} diff --git a/hub/tx_finl/rows/acc_coinbase.tex b/hub/tx_finl/rows/acc_coinbase.tex index a0a34ac..752cbae 100644 --- a/hub/tx_finl/rows/acc_coinbase.tex +++ b/hub/tx_finl/rows/acc_coinbase.tex @@ -13,7 +13,7 @@ \finalizationDomSubStamps { anchorRow = i , relOffset = \locTxFinlRoffAccCoinbase , - subOffset = 1 , + subOffset = 0 , } } \\ % \standardDomSubStamps {i}{\locTxFinlSuccessCoinbaseAccountOffset}{1}} \\ diff --git a/hub/tx_finl/rows/acc_sender.tex b/hub/tx_finl/rows/acc_sender.tex index d915e14..81a3fd5 100644 --- a/hub/tx_finl/rows/acc_sender.tex +++ b/hub/tx_finl/rows/acc_sender.tex @@ -13,7 +13,7 @@ \finalizationDomSubStamps { anchorRow = i , relOffset = \locTxFinlRoffAccSender , - subOffset = 0 , + subOffset = 1 , } } \\ \end{array}\right. From f28e811f03781a2efd82946994e864f0909423ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 2 Dec 2024 11:21:35 +0700 Subject: [PATCH 14/18] ras: uncommented hub inputs --- hub/_inputs.tex | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/hub/_inputs.tex b/hub/_inputs.tex index 6f975d1..089d090 100644 --- a/hub/_inputs.tex +++ b/hub/_inputs.tex @@ -6,19 +6,19 @@ \section{Introduction} \label{hub: intro} \input{intro} -% \input{columns/_inputs} % Done -% \input{heartbeat/_inputs} % Done -% \input{generalities/_inputs} % Done -% \input{stack/_inputs} % Done -% \input{context/_inputs} % Done -% \input{account/_inputs} % Done -% \input{storage/_inputs} % Done -% \input{misc/_inputs} % Todo -% \input{scenario/_inputs} % Wip -% \input{tx_skip/_inputs} % Done -% \input{tx_prewarm/_inputs} % Done +\input{columns/_inputs} % Done +\input{heartbeat/_inputs} % Done +\input{generalities/_inputs} % Done +\input{stack/_inputs} % Done +\input{context/_inputs} % Done +\input{account/_inputs} % Done +\input{storage/_inputs} % Done +\input{misc/_inputs} % Todo +\input{scenario/_inputs} % Wip +\input{tx_skip/_inputs} % Done +\input{tx_prewarm/_inputs} % Done \input{tx_init/_inputs} % Done -% \input{instruction_handling/_inputs} % Wip +\input{instruction_handling/_inputs} % Wip \input{tx_finl/_inputs} % Done -% \input{consistencies/_inputs} % Wip -% \input{lookups/_inputs} % Wip +\input{consistencies/_inputs} % Wip +\input{lookups/_inputs} % Wip From 20405faef18e3137a0c880d6a2c6bb22c3f0007a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 20 Dec 2024 20:02:17 +0100 Subject: [PATCH 15/18] fix: TX_FINL requires trimming the COINBASE address This may be the first time the address is exposed --- hub/tx_finl/rows/acc_coinbase.tex | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/hub/tx_finl/rows/acc_coinbase.tex b/hub/tx_finl/rows/acc_coinbase.tex index 752cbae..11d4716 100644 --- a/hub/tx_finl/rows/acc_coinbase.tex +++ b/hub/tx_finl/rows/acc_coinbase.tex @@ -1,8 +1,12 @@ we impose the following on the \textbf{coinbase account}: \[ \left\{\begin{array}{lcl} - \accAddress\high _{i + \locTxFinlRoffAccCoinbase} & = & \locTxFinlCoinbaseAddressHi \\ - \accAddress\low _{i + \locTxFinlRoffAccCoinbase} & = & \locTxFinlCoinbaseAddressLo \\ + \accTrimAddress + {i}{\locTxFinlRoffAccCoinbase} + {\locTxFinlCoinbaseAddressHi} + {\locTxFinlCoinbaseAddressLo} \\ + % \accAddress\high _{i + \locTxFinlRoffAccCoinbase} & = & \locTxFinlCoinbaseAddressHi \\ + % \accAddress\low _{i + \locTxFinlRoffAccCoinbase} & = & \locTxFinlCoinbaseAddressLo \\ \multicolumn{3}{l}{\accIncrementBalance {i}{\locTxFinlRoffAccCoinbase}{\locFinlSuccessCoinbaseReward}} \\ \multicolumn{3}{l}{\accSameNonce {i}{\locTxFinlRoffAccCoinbase}} \\ \multicolumn{3}{l}{\accSameCode {i}{\locTxFinlRoffAccCoinbase}} \\ From bb4a849b5052cef3d59dfebf0616ae4fdfae621c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sat, 21 Dec 2024 08:27:48 +0100 Subject: [PATCH 16/18] fix: removed the \finalizationDomSubStamps The main point is that everything which happens during the TX_INIT or TX_EXEC phase (excluding SELFDESTRUCT induced account wiping) happens at the fery latest at the final HUB_STAMP of the TX_EXEC phase. During the TX_FINL phase one has HUB_STAMP == HUB_STAMP_TRANSCTION_END So we can do the gas refund payment of the sender + gas reward of the coinbase using \standardDomSubStamps with dom offsets 0 / 1 respectively. All the scheduled account wiping operations will take place at that same time stamp with DOM_STAMP offset epsilon_selfdestruct > 1 and the relevant SUB_STAMP. --- hub/generalities/revert/dom_and_sub.tex | 38 ++++++++++++------------- hub/tx_finl/rows/_collage.tex | 5 ---- hub/tx_finl/rows/acc_coinbase.tex | 4 +-- hub/tx_finl/rows/acc_sender.tex | 4 +-- pkg/xkeyval_macros/dom_sub_stamps.sty | 18 ++++++------ 5 files changed, 32 insertions(+), 37 deletions(-) diff --git a/hub/generalities/revert/dom_and_sub.tex b/hub/generalities/revert/dom_and_sub.tex index 2b23d54..cc8b742 100644 --- a/hub/generalities/revert/dom_and_sub.tex +++ b/hub/generalities/revert/dom_and_sub.tex @@ -82,25 +82,25 @@ % \genericUndoingDomSubStamps\big[\col{revstp}, \revertEpsilon, \col{s}\big]_{i} \end{array} \right. \] -and -\[ - \left\{ \begin{array}{l} - \finalizationDomSubStamps { - anchorRow = i , - relOffset = \relof , - subOffset = \col{s} , - } - \vspace{2mm} \\ \qquad \qquad \iff - \genericUndoingDomSubStamps { - anchorRow = i , - relOffset = \relof , - revertStamp = \txEndStamp_{i} , - domOffset = \finalizationEpsilon , - subOffset = \col{s} , - } - % \genericUndoingDomSubStamps {\relof} \big[\txEndStamp_{i}, \selfdestructEpsilon, 0 \big]_{i} \\ - \end{array} \right. -\] +% and +% \[ +% \left\{ \begin{array}{l} +% \finalizationDomSubStamps { +% anchorRow = i , +% relOffset = \relof , +% subOffset = \col{s} , +% } +% \vspace{2mm} \\ \qquad \qquad \iff +% \genericUndoingDomSubStamps { +% anchorRow = i , +% relOffset = \relof , +% revertStamp = \txEndStamp_{i} , +% domOffset = \finalizationEpsilon , +% subOffset = \col{s} , +% } +% % \genericUndoingDomSubStamps {\relof} \big[\txEndStamp_{i}, \selfdestructEpsilon, 0 \big]_{i} \\ +% \end{array} \right. +% \] and \[ \left\{ \begin{array}{l} diff --git a/hub/tx_finl/rows/_collage.tex b/hub/tx_finl/rows/_collage.tex index 0644ddb..ce1d866 100644 --- a/hub/tx_finl/rows/_collage.tex +++ b/hub/tx_finl/rows/_collage.tex @@ -13,11 +13,6 @@ \input{tx_finl/rows/acc_sender} \item[\underline{\underline{Coinbase account-row n$^°\bm{(i + \locTxFinlRoffAccCoinbase)}$:}}] \input{tx_finl/rows/acc_coinbase} -\end{description} -\saNote{} -This is the one time in the \zkEvm{} specification where the \texttt{Sub stamp offset}'s are listed in decrementing order. -The interpretation is that (in the re-ordered trace) the sender refund ought to happen before the coinbase reward. -\begin{description} \item[\underline{\underline{Transaction-row n$^°(\bm{i + \locTxFinlRoffTxn})$:}}] \input{tx_finl/rows/txn} \end{description} diff --git a/hub/tx_finl/rows/acc_coinbase.tex b/hub/tx_finl/rows/acc_coinbase.tex index 11d4716..2c289a9 100644 --- a/hub/tx_finl/rows/acc_coinbase.tex +++ b/hub/tx_finl/rows/acc_coinbase.tex @@ -14,10 +14,10 @@ \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlRoffAccCoinbase}} \\ \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlRoffAccCoinbase}} \\ \multicolumn{3}{l}{ - \finalizationDomSubStamps { + \standardDomSubStamps { anchorRow = i , relOffset = \locTxFinlRoffAccCoinbase , - subOffset = 0 , + domOffset = 1 , } } \\ % \standardDomSubStamps {i}{\locTxFinlSuccessCoinbaseAccountOffset}{1}} \\ diff --git a/hub/tx_finl/rows/acc_sender.tex b/hub/tx_finl/rows/acc_sender.tex index 81a3fd5..5f9e431 100644 --- a/hub/tx_finl/rows/acc_sender.tex +++ b/hub/tx_finl/rows/acc_sender.tex @@ -10,10 +10,10 @@ \multicolumn{3}{l}{\accSameWarmth {i}{\locTxFinlRoffAccSender}} \\ \multicolumn{3}{l}{\accSameMarkedForSelfdestructFlag {i}{\locTxFinlRoffAccSender}} \\ \multicolumn{3}{l}{ - \finalizationDomSubStamps { + \standardDomSubStamps { anchorRow = i , relOffset = \locTxFinlRoffAccSender , - subOffset = 1 , + domOffset = 0 , } } \\ \end{array}\right. diff --git a/pkg/xkeyval_macros/dom_sub_stamps.sty b/pkg/xkeyval_macros/dom_sub_stamps.sty index 77826d1..dad649f 100644 --- a/pkg/xkeyval_macros/dom_sub_stamps.sty +++ b/pkg/xkeyval_macros/dom_sub_stamps.sty @@ -86,15 +86,15 @@ % subOffset = , % } -\newcommand{\finalizationDomSubStampsName} {\stampSignifier\texttt{finalizationDomSubStamps}} -\newcommand{\finalizationDomSubStamps} [1] { - \setkeys[DOMSUB]{var}{#1} - \finalizationDomSubStampsName _{\cmdDOMSUB@var@anchorRow} -\left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ - \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ -\end{array} \right] -} +% \newcommand{\finalizationDomSubStampsName} {\stampSignifier\texttt{finalizationDomSubStamps}} +% \newcommand{\finalizationDomSubStamps} [1] { +% \setkeys[DOMSUB]{var}{#1} +% \finalizationDomSubStampsName _{\cmdDOMSUB@var@anchorRow} +% \left[ \begin{array}{ll} +% \utt{Rel. row offset:} & \cmdDOMSUB@var@relOffset \\ +% \utt{Sub offset:} & \cmdDOMSUB@var@subOffset \\ +% \end{array} \right] +% } \newcommand{\revertWithChildFailureDomSubStampsName} {\stampSignifier\texttt{revertWithChildFailureDomSubStamps}} \newcommand{\revertWithChildFailureDomSubStamps} [1] { From 4843ee036b98d43e2cb05d48b5876f1921294287 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sat, 21 Dec 2024 15:08:55 +0100 Subject: [PATCH 17/18] fix: TX_INIT terminates on a CONTEXT-row --- hub/heartbeat/hub_stamp.tex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/hub/heartbeat/hub_stamp.tex b/hub/heartbeat/hub_stamp.tex index bd0e0bc..216c1ef 100644 --- a/hub/heartbeat/hub_stamp.tex +++ b/hub/heartbeat/hub_stamp.tex @@ -60,12 +60,16 @@ \If \left[ \begin{array}{cccc} + & \ts_{i} \\ - + & \ti_{i} \\ + & \tf_{i} \\ \end{array} \right] \neq 0 ~ \Then \hubStamp_{i + 1} = \hubStamp_{i} + \peekTransaction_{i}. \] + \item + \[ + \If \ti_{i} \neq 0 + ~ \Then \hubStamp_{i + 1} = \hubStamp_{i} + \peekContext _{i}. + \] \end{enumerate} \saNote{} The above enforces that $\hubStamp$ remains constant throughout the processing of any transaction which requires no \textsc{evm}-execution as well as during the initialization and finalization phases of transactions that require \evm{} execution. The \hubStamp{} furthermore will jump by one (on any one of those phases) whenever the current row peeks into the transaction. From e5e2b1ebdc61c1a01a0d093f28f88f6be2987c76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 24 Dec 2024 21:09:58 +0100 Subject: [PATCH 18/18] ras --- block_hash/_all_block_hash.tex | 2 ++ block_hash/byte_decomposition.tex | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/block_hash/_all_block_hash.tex b/block_hash/_all_block_hash.tex index 811073f..2006696 100644 --- a/block_hash/_all_block_hash.tex +++ b/block_hash/_all_block_hash.tex @@ -26,6 +26,8 @@ \usepackage{../pkg/iomf_done} \usepackage{../pkg/offset_processor} +\usepackage{../pkg/draculatheme} + \title{\blockHashMod{} module} \author{Rollup team} \date{May 2024} diff --git a/block_hash/byte_decomposition.tex b/block_hash/byte_decomposition.tex index 754d632..d24b4ef 100644 --- a/block_hash/byte_decomposition.tex +++ b/block_hash/byte_decomposition.tex @@ -12,10 +12,10 @@ \begin{array}{lcl} \blockHash\high_{i} & \!\!\! = \!\!\! & - \displaystyle \sum_{k = 0}^{\llargeMO} 256^(\llargeMO - k) \cdot \byteCol{HI\_k}_{i} \\ + \displaystyle \sum_{k = 0}^{\llargeMO} 256^{\llargeMO - k} \cdot \byteCol{HI\_k}_{i} \\ \blockHash\low_{i} & \!\!\! = \!\!\! & - \displaystyle \sum_{k = 0}^{\llargeMO} 256^(\llargeMO - k) \cdot \byteCol{LO\_k}_{i} \\ + \displaystyle \sum_{k = 0}^{\llargeMO} 256^{\llargeMO - k} \cdot \byteCol{LO\_k}_{i} \\ \end{array} \right. \]