Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

TX_INIT and TX_FINL redesign #12

Open
wants to merge 18 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 12 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions hub/generalities/revert/constants.tex
Original file line number Diff line number Diff line change
@@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

syntax: you defined 1 line before what's col{max}

\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}
Expand Down
115 changes: 67 additions & 48 deletions hub/generalities/revert/dom_and_sub.tex
Original file line number Diff line number Diff line change
Expand Up @@ -5,59 +5,59 @@
\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.
\]
and
\[
\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}
\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.
\]
and
\[
\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
\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.
\]
and
\[
\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.
Expand All @@ -66,51 +66,70 @@
\[
\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.
\]
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}
\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.
\]
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.
Expand All @@ -119,18 +138,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;
Expand Down
2 changes: 1 addition & 1 deletion hub/heartbeat/hub_stamp.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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}).

Expand Down
4 changes: 3 additions & 1 deletion hub/heartbeat/peeking_flags.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
18 changes: 9 additions & 9 deletions hub/heartbeat/phase_flags.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}
Expand Down
10 changes: 5 additions & 5 deletions hub/tx_finl/_inputs.tex
Original file line number Diff line number Diff line change
@@ -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}
42 changes: 28 additions & 14 deletions hub/tx_finl/_local.tex
Original file line number Diff line number Diff line change
@@ -1,17 +1,31 @@
\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\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}}
Loading