TX_INIT and TX_FINL redesign

hub/generalities/revert/constants.tex

@@ -1,15 +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           = 8$
-	\item $\revertEpsilon       = 6$
-	\item $\selfdestructEpsilon = 7$
+	\item $\hubTau              =  8$
+	\item $\hubLambda           = 16$
+	\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
+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 $0 \leq \revertEpsilon < \selfdestructEpsilon < \hubLambda$
+	\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}$

hub/generalities/revert/dom_and_sub.tex

@@ -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.
@@ -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.
@@ -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;

hub/heartbeat/hub_stamp.tex

@@ -60,18 +60,22 @@
 			\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.
 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}).
 

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.

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}

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              \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}
+\subsection{Common constraints           \lispTodo{}}   \label{hub: finalization phase: common constraints}       \input{tx_finl/rows/_collage}

hub/tx_finl/_local.tex

@@ -1,17 +1,30 @@
-\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\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}}