diff --git a/block_data/_all_block_data.tex b/block_data/_all_block_data.tex index b9803b5..d845da7 100644 --- a/block_data/_all_block_data.tex +++ b/block_data/_all_block_data.tex @@ -1,7 +1,7 @@ -\documentclass{article} +\documentclass[fleqn]{article} \usepackage[dvipsnames]{xcolor} \usepackage{../pkg/common} -% \usepackage{../pkg/dark_theme} +\usepackage{xkeyval} \usepackage{../pkg/std} \usepackage{../pkg/IEEEtrantools} \usepackage{../pkg/rom} @@ -24,6 +24,10 @@ \usepackage{../pkg/block_data} \usepackage{../pkg/block_hash} \usepackage{../pkg/txn_data} +\usepackage{../pkg/iomf_done} +\usepackage{../pkg/xkeyval_macros/wcp_calls} +\usepackage{../pkg/xkeyval_macros/euc_calls} +\usepackage{../pkg/euc} \usepackage{../pkg/draculatheme} diff --git a/block_data/_inputs.tex b/block_data/_inputs.tex index 8793306..995ba2c 100644 --- a/block_data/_inputs.tex +++ b/block_data/_inputs.tex @@ -1,13 +1,18 @@ +\input{_local} + \section{Block data module} -\subsection{Introduction} \label{block data: intro} \input{intro} -\subsection{Columns} \label{block data: columns} \input{columns} +\subsection{Introduction} \label{block data: intro} \input{intro} +\subsection{Columns} \label{block data: columns} \input{columns} +\subsection{Module call macros} \label{block data: module calls} \input{calls} \section{Constraints} -\subsection{Heartbeat} \label{block data: heartbeat} \input{heartbeat} -\subsection{Constancies} \label{block data: constancies} \input{constancies} -\subsection{Bytehood and byte decomposition constraints} \label{block data: byte decomposition} \input{byteDec} -\subsection{Value Constraints} \label{block data: value constraints} \input{value_constraint} +\subsection{Shorthands} \label{block data: shorthands} \input{shorthands} +\subsection{Binary constraints} \label{block data: binarities} \input{binarities} +\subsection{Unconditional constraints} \label{block data: unconditional} \input{unconditional} +\subsection{Constancies} \label{block data: constancies} \input{constancies} +\subsection{Heartbeat} \label{block data: heartbeat} \input{heartbeat} +\subsection{Representation} \label{block data: representation} \input{representation} -\section{Lookups} \label{block data: lookups} \input{lookups/_inputs} +\section{Computations and checks} \label{block data: computations and checks} \input{computations/_inputs} - +\section{Lookups} \label{block data: lookups} \input{lookups/_inputs} diff --git a/block_data/_local.tex b/block_data/_local.tex new file mode 100644 index 0000000..841eb4c --- /dev/null +++ b/block_data/_local.tex @@ -0,0 +1,37 @@ +\def\rOne {\redm{1}} + +\def\locIsCoinbase {\col{is\_CB}} +\def\locIsTimestamp {\col{is\_TS}} +\def\locIsNumber {\col{is\_NB}} +\def\locIsDifficulty {\col{is\_DF}} +\def\locIsGaslimit {\col{is\_GL}} +\def\locIsChainid {\col{is\_ID}} +\def\locIsBasefee {\col{is\_BF}} + +\def\locIsCurrConf {\col{is\_curr}} +\def\locIsPrevConf {\col{is\_prev}} +\def\locPrevCurrWghtSum {\col{curr\_prev\_wght\_sum}} + +\def\locFlagSum {\col{flag\_sum}} +\def\locWghtSum {\col{wght\_sum}} +\def\locInstSum {\col{inst\_sum}} +\def\locMaxCtSum {\col{ct\_max\_sum}} +\def\locPhaseEntry {\col{phase\_entry}} +\def\locSamePhase {\col{same\_phase}} +\def\locLegalTransitions {\col{allowable\_transitions}} + +\def\ctMaxCoinbase {\redm{\kappa_{\texttt{cb}}}} +\def\ctMaxTimestamp {\redm{\kappa_{\texttt{ts}}}} +\def\ctMaxNumber {\redm{\kappa_{\texttt{nb}}}} +\def\ctMaxDifficulty {\redm{\kappa_{\texttt{df}}}} +\def\ctMaxGaslimit {\redm{\kappa_{\texttt{gl}}}} +\def\ctMaxChainid {\redm{\kappa_{\texttt{id}}}} +\def\ctMaxBasefee {\redm{\kappa_{\texttt{bf}}}} +\def\kappaDots {\redm{\kappa_{\texttt{xx}}}} +\def\blockDataDepth {\redm{\kappa_{\texttt{depth}}}} + +\def\exoInstruction {\col{EXO\_}\instruction} +\def\previousGasLimit {\col{prev\_gas\_limit}} +\def\maxDeviation {\col{max\_deviation}} + +\def\locFirstBlockIsGenesisBlock {\col{first\_block\_is\_genesis\_block}} diff --git a/block_data/binarities.tex b/block_data/binarities.tex new file mode 100644 index 0000000..6ba61b3 --- /dev/null +++ b/block_data/binarities.tex @@ -0,0 +1,15 @@ +We impose \textbf{binary} constraints on the following columns: +\begin{multicols}{3} + \begin{enumerate} + \item $\iomf$ + \item $\previousConflation$ + \item $\currentConflation$ + \item $\isCoinbase$ + \item $\isTimestamp$ + \item $\isNumber$ + \item $\isDifficulty$ + \item $\isGaslimit$ + \item $\isChainid$ + \item $\isBasefee$ + \end{enumerate} +\end{multicols} diff --git a/block_data/calls.tex b/block_data/calls.tex new file mode 100644 index 0000000..b3c68a5 --- /dev/null +++ b/block_data/calls.tex @@ -0,0 +1,106 @@ +We define several simple constraint systems to simplify the writing of constraints. +\[ + \left\{ \begin{array}{lcl} + \wcpCallToLt { + anchorRow = i , + relOffset = \relof , + argOneHi = \col{a\_hi} , + argOneLo = \col{a\_lo} , + argTwoHi = \col{b\_hi} , + argTwoLo = \col{b\_lo} , + } & \define & + \left\{ \begin{array}{lcl} + \wcpFlag _{i + \relof} & = & \rOne \\ + \exoInstruction _{i + \relof} & = & \inst{LT} \\ + \argOneHi _{i + \relof} & = & \col{a\_hi} \\ + \argOneLo _{i + \relof} & = & \col{a\_lo} \\ + \argTwoHi _{i + \relof} & = & \col{b\_hi} \\ + \argTwoLo _{i + \relof} & = & \col{b\_lo} \\ + \res _{i + \relof} & = & 1 \\ + \end{array} \right. \vspace{2mm} \\ + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \wcpCallToGt { + anchorRow = i , + relOffset = \relof , + argOneHi = \col{a\_hi} , + argOneLo = \col{a\_lo} , + argTwoHi = \col{b\_hi} , + argTwoLo = \col{b\_lo} , + } & \define & + \left\{ \begin{array}{lcl} + \wcpFlag _{i + \relof} & = & \rOne \\ + \exoInstruction _{i + \relof} & = & \inst{GT} \\ + \argOneHi _{i + \relof} & = & \col{a\_hi} \\ + \argOneLo _{i + \relof} & = & \col{a\_lo} \\ + \argTwoHi _{i + \relof} & = & \col{b\_hi} \\ + \argTwoLo _{i + \relof} & = & \col{b\_lo} \\ + \res _{i + \relof} & = & 1 \\ + \end{array} \right. \vspace{2mm} \\ + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \wcpCallToLeq { + anchorRow = i , + relOffset = \relof , + argOneHi = \col{a\_hi} , + argOneLo = \col{a\_lo} , + argTwoHi = \col{b\_hi} , + argTwoLo = \col{b\_lo} , + } & \define & + \left\{ \begin{array}{lcl} + \wcpFlag _{i + \relof} & = & \rOne \\ + \exoInstruction _{i + \relof} & = & \inst{LEQ} \\ + \argOneHi _{i + \relof} & = & \col{a\_hi} \\ + \argOneLo _{i + \relof} & = & \col{a\_lo} \\ + \argTwoHi _{i + \relof} & = & \col{b\_hi} \\ + \argTwoLo _{i + \relof} & = & \col{b\_lo} \\ + \res _{i + \relof} & = & 1 \\ + \end{array} \right. \vspace{2mm} \\ + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \wcpCallToGeq { + anchorRow = i , + relOffset = \relof , + argOneHi = \col{a\_hi} , + argOneLo = \col{a\_lo} , + argTwoHi = \col{b\_hi} , + argTwoLo = \col{b\_lo} , + } & \define & + \left\{ \begin{array}{lcl} + \wcpFlag _{i + \relof} & = & \rOne \\ + \exoInstruction _{i + \relof} & = & \inst{GEQ} \\ + \argOneHi _{i + \relof} & = & \col{a\_hi} \\ + \argOneLo _{i + \relof} & = & \col{a\_lo} \\ + \argTwoHi _{i + \relof} & = & \col{b\_hi} \\ + \argTwoLo _{i + \relof} & = & \col{b\_lo} \\ + \res _{i + \relof} & = & 1 \\ + \end{array} \right. \vspace{2mm} \\ + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \wcpCallToIszero { + anchorRow = i , + relOffset = \relof , + argOneHi = \col{a\_hi} , + argOneLo = \col{a\_lo} , + } & \define & + \left\{ \begin{array}{lcl} + \wcpFlag _{i + \relof} & = & \rOne \\ + \exoInstruction _{i + \relof} & = & \inst{ISZERO} \\ + \argOneHi _{i + \relof} & = & \col{a\_hi} \\ + \argOneLo _{i + \relof} & = & \col{a\_lo} \\ + \argTwoHi _{i + \relof} & = & 0 \\ + \argTwoLo _{i + \relof} & = & 0 \\ + \res _{i + \relof} & = & \relevantValue \\ + \end{array} \right. \vspace{2mm} \\ + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \eucCall { + anchorRow = i , + relOffset = \relof , + argOne = \col{a} , + argTwo = \col{b} , + } & \define & + \left\{ \begin{array}{lcl} + \eucFlag _{i + \relof} & = & \rOne \\ + \argOneLo _{i + \relof} & = & \col{a} \\ + \argTwoLo _{i + \relof} & = & \col{b} \\ + \end{array} \right. \\ + \end{array} \right. +\] +\saNote{} +The result of all comparisons is required to be \texttt{true} except for \inst{ISZERO}. diff --git a/block_data/columns.tex b/block_data/columns.tex index d0679df..f142495 100644 --- a/block_data/columns.tex +++ b/block_data/columns.tex @@ -1,17 +1,33 @@ We remind the reader that \ccc{} stands for ``counter-constant column.'' +The first set of columns will be used to define the heartbeat of the \btcMod{} module. \begin{enumerate} + \item $\iomf$: + nondecreasing binary column; + \item $\previousConflation$: + binary column indicating the rows pertaining to the last block of the previous conflation; + \item $\currentConflation$: + binary column indicating the rows pertaining to the blocks of the current conflation; + \item $\maxCt$: + counter-constant column; \item $\ct$: - counter column; hovers around zero and then cycles from $0$ to $\maxCtBtcData$; - \item \blockNumberOfFirstBlockInConflation{}: - ``conflation-constant'' column containing the block number\footnote{In the sense of the \evm{}} of the first block of this conflation; - \item $\relBlock$: - \ccc{} containing the relative block number; - \item $\relTxMax$: - \ccc{} containing the number of transactions in this block; - \item $\INST$: + counter column; hovers around zero and then cycles from $0$ to $\maxCt$; +\end{enumerate} +We introduce some binary columns linked to the instructions that the present module deals with: +\begin{multicols}{3} + \begin{enumerate}[resume] + \item $\isCoinbase$ + \item $\isTimestamp$ + \item $\isNumber$ + \item $\isDifficulty$ + \item $\isGaslimit$ + \item $\isChainid$ + \item $\isBasefee$ + \end{enumerate} +\end{multicols} +\noindent The following columns contain data which is reflected in the \txnDataMod{} module. +\begin{enumerate}[resume, start=13] + \item $\instruction$: instruction column; - \item $\blockDataHi$, $\blockDataLo$: - columns containing block data; \item $\coinbase\high$ and $\coinbase\low$: \ccc{} containing the coinbase address; @@ -21,9 +37,19 @@ \item \basefee{}: \ccc{} containing the base fee; - \item $\byteCol{HI\_k}$, and $\byteCol{LO\_k}$, $k = 0, 1, \dots, \llargeMO$: - \item $\wcpFlag$: +\end{enumerate} +The following columns pertain to transaction and block numbers. +\begin{enumerate}[resume] + \item \blockNumberOfFirstBlockInConflation{}: + ``conflation-constant'' column containing the block number\footnote{In the sense of the \evm{}} of the first block of this conflation; + \item $\relBlock$: + \ccc{} containing the relative block number; + \item $\relTxMax$: + \ccc{} containing the number of transactions in this block; + \item $\blockDataHi$, $\blockDataLo$: + columns containing block data; + \item $\argOneHi$, $\argOneLo$, $\argTwoHi$, $\argTwoLo$, $\res$, $\exoInstruction$ + columns containing arguments for computations performed by foreign modules; + \item $\wcpFlag$, $\eucFlag$: binary flags used as selector for lookups; \end{enumerate} -\saNote{} -The \INST{} column is $0$ during padding then cycles through a selection of ``block data'' specific opcodes e.g. \texttt{0x\,10} (i.e. \inst{COINBASE}), \texttt{0x\,46} (i.e. \inst{CHAINID}) etc\dots{} see section~(\ref{block data: value constraints}). diff --git a/block_data/computations/_inputs.tex b/block_data/computations/_inputs.tex new file mode 100644 index 0000000..0086f66 --- /dev/null +++ b/block_data/computations/_inputs.tex @@ -0,0 +1,7 @@ +\subsection{For \inst{COINBASE }} \label{block data: computations and checks: coinbase} \input{computations/coinbase} +\subsection{For \inst{TIMESTAMP }} \label{block data: computations and checks: timestamp} \input{computations/timestamp} +\subsection{For \inst{NUMBER }} \label{block data: computations and checks: number} \input{computations/number} +\subsection{For \inst{DIFFICULTY}} \label{block data: computations and checks: difficulty} \input{computations/difficulty} +\subsection{For \inst{GASLIMIT }} \label{block data: computations and checks: gaslimit} \input{computations/gaslimit} +\subsection{For \inst{CHAINID }} \label{block data: computations and checks: chainid} \input{computations/chainid} +\subsection{For \inst{BASEFEE }} \label{block data: computations and checks: basefee} \input{computations/basefee} diff --git a/block_data/computations/basefee.tex b/block_data/computations/basefee.tex new file mode 100644 index 0000000..9f820fe --- /dev/null +++ b/block_data/computations/basefee.tex @@ -0,0 +1,37 @@ +\begin{center} + \boxed{\text{% + The following constraints assume that + $\left\{ \begin{array}{lcl} + \isBasefee _{i - 1} & = & 0 \\ + \isBasefee _{i} & = & 1 \\ + \end{array} \right.$}} +\end{center} + +\begin{description} + \item[\underline{\underline{Setting \inst{BASEFEE}:}}] + we impose + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & 0 \\ + \blockDataLo _{i} & = & \basefee _{i} \\ + \end{array} \right. + \] + \saNote{} + Implementations may further impose, by means of a constraint, the value returned by the \inst{BASEFEE} opcode to some network constant + $\lineaBaseFee{}$. + \item[\underline{\underline{\inst{BASEFEE} bound:}}] + \def\rowOffset{\yellowm{0}} + we impose + \[ + \wcpCallToGeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = 0 , + } + \] + \saNote{} + The above ensures that $\basefee _{i} \geq 0$ is well formed (in terms of its high and low parts being $\llarge$-byte integers.) +\end{description} diff --git a/block_data/computations/chainid.tex b/block_data/computations/chainid.tex new file mode 100644 index 0000000..3c13a6e --- /dev/null +++ b/block_data/computations/chainid.tex @@ -0,0 +1,41 @@ +\begin{center} + \boxed{\text{% + The following constraints assume that + $\left\{ \begin{array}{lcl} + \isChainid _{i - 1} & = & 0 \\ + \isChainid _{i} & = & 1 \\ + \end{array} \right.$}} +\end{center} + +\begin{description} + \item[\underline{\underline{Setting \inst{CHAINID}:}}] + we cannot \emph{a priori} constrain \inst{CHAINID}; + + \saNote{} + Implementations may impose the value returned by the \inst{CHAINID} opcode to some network constant + $\lineaChainId$. + \item[\underline{\underline{Permanence of \inst{CHAINID}:}}] + \If $\locIsCurrConf _{i} = 1$ \Then + we impose + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & \blockDataHi _{i - \blockDataDepth} \\ + \blockDataLo _{i} & = & \blockDataLo _{i - \blockDataDepth} \\ + \end{array} \right. + \] + \item[\underline{\underline{\inst{CHAINID} bound:}}] + \def\rowOffset{\yellowm{0}} + we impose + \[ + \wcpCallToGeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = 0 , + } + \] + \saNote{} + The above ensures that $\inst{CHAINID} \geq 0$ is well formed (in terms of its high and low parts being $\llarge$-byte integers.) +\end{description} diff --git a/block_data/computations/coinbase.tex b/block_data/computations/coinbase.tex new file mode 100644 index 0000000..f96c183 --- /dev/null +++ b/block_data/computations/coinbase.tex @@ -0,0 +1,33 @@ +\begin{center} + \boxed{\text{% + The following constraints assume that + $\left\{ \begin{array}{lcl} + \isCoinbase _{i - 1} & = & 0 \\ + \isCoinbase _{i} & = & 1 \\ + \end{array} \right.$}} +\end{center} +\begin{description} + \item[\underline{\underline{Setting \inst{COINBASE}:}}] + we impose + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & \coinbase\high _{i} \\ + \blockDataLo _{i} & = & \coinbase\low _{i} \\ + \end{array} \right. + \] + \item[\underline{\underline{\inst{GASLIMIT} deviation lower bound:}}] + \def\rowOffset{\yellowm{0}} + \If $\locIsCurrConf _{i} = 1$ \Then + \[ + \wcpCallToLt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 256^\ssmall , + argTwoLo = 0 , + } + \] + \saNote{} + The above ensures that \inst{COINBASE} fits in a $\addressSize$-byte integer. +\end{description} diff --git a/block_data/computations/difficulty.tex b/block_data/computations/difficulty.tex new file mode 100644 index 0000000..065bcb4 --- /dev/null +++ b/block_data/computations/difficulty.tex @@ -0,0 +1,31 @@ +\begin{center} + \boxed{\text{% + The following constraints assume that + $\left\{ \begin{array}{lcl} + \isDifficulty _{i - 1} & = & 0 \\ + \isDifficulty _{i} & = & 1 \\ + \end{array} \right.$}} +\end{center} +\begin{description} + \item[\underline{\underline{Setting \inst{DIFFICULTY}:}}] + we cannot \emph{a priori} constrain \inst{DIFFICULTY}; + + \saNote{} + Implementations may impose the value returned by the \inst{DIFFICULTY} opcode to some network constant, + e.g. $\lineaDifficulty= 2$. + \item[\underline{\underline{\inst{DIFFICULTY} bound:}}] + \def\rowOffset{\yellowm{0}} + we impose + \[ + \wcpCallToGeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = 0 , + } + \] + \saNote{} + The above ensures that $\inst{DIFFICULTY} \geq 0$ is well formed (in terms of its high and low parts being $\llarge$-byte integers.) +\end{description} diff --git a/block_data/computations/gaslimit.tex b/block_data/computations/gaslimit.tex new file mode 100644 index 0000000..6aec94f --- /dev/null +++ b/block_data/computations/gaslimit.tex @@ -0,0 +1,100 @@ +\begin{center} + \boxed{\text{% + The following constraints assume that + $\left\{ \begin{array}{lcl} + \isGaslimit _{i - 1} & = & 0 \\ + \isGaslimit _{i} & = & 1 \\ + \end{array} \right.$}} +\end{center} +We impose the following: +\begin{description} + \item[\underline{\underline{Setting \inst{GASLIMIT}:}}] + we impose + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & 0 \\ + \blockDataLo _{i} & = & \blockGasLimit _{i} \\ + \end{array} \right. + \] + \item[\underline{\underline{\inst{GASLIMIT} lower bound:}}] + \def\rowOffset{\yellowm{0}} + we impose + \[ + \wcpCallToGeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = \texttt{61\_000\_000} , + } + \] + \saNote{} + The above ensures that $\blockGasLimit_{i} \geq \texttt{61\_000\_000}$. + \item[\underline{\underline{\inst{GASLIMIT} upper bound:}}] + \def\rowOffset{\yellowm{1}} + we impose + \[ + \wcpCallToLeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = \texttt{2\_000\_000\_000} , + } + \] + \saNote{} + The above ensures that $\blockGasLimit_{i} \leq \texttt{2\_000\_000\_000}$. + \item[\underline{\underline{Maximum deviation:}}] + \def\rowOffset{\yellowm{2}} + \If $\locIsCurrConf _{i} = 1$ \Then + we impose + \[ + \eucCall{ + anchorRow = i , + relOffset = \rowOffset , + argOne = \previousGasLimit , + argTwo = 1024 , + } + \] + where we set + \[ + \left\{ \begin{array}{lcl} + \previousGasLimit & \define & \blockGasLimit _{i - \blockDataDepth} \\ + \maxDeviation & \define & \res _{i + \rowOffset} \\ + \end{array} \right. + \] + \saNote{} + By definition, $\maxDeviation \equiv \left\lfloor \frac\previousGasLimit{1024} \right\rfloor$. + \item[\underline{\underline{\inst{GASLIMIT} deviation upper bound:}}] + \def\rowOffset{\yellowm{3}} + \If $\locIsCurrConf _{i} = 1$ \Then + \[ + \wcpCallToLt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = \previousGasLimit + \maxDeviation , + } + \] + \saNote{} + The above ensures that $\blockGasLimit_{i} < \previousGasLimit + \maxDeviation$. + \item[\underline{\underline{\inst{GASLIMIT} deviation lower bound:}}] + \def\rowOffset{\yellowm{4}} + \If $\locIsCurrConf _{i} = 1$ \Then + \[ + \wcpCallToGt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = \previousGasLimit - \maxDeviation , + } + \] + \saNote{} + The above ensures that $\blockGasLimit_{i} > \previousGasLimit - \maxDeviation$. +\end{description} diff --git a/block_data/computations/number.tex b/block_data/computations/number.tex new file mode 100644 index 0000000..354db0e --- /dev/null +++ b/block_data/computations/number.tex @@ -0,0 +1,95 @@ +\begin{center} + \boxed{\text{% + The following constraints assume that + $\left\{ \begin{array}{lcl} + \isNumber _{i - 1} & = & 0 \\ + \isNumber _{i} & = & 1 \\ + \end{array} \right.$}} +\end{center} +\begin{description} + \item[\underline{\underline{Comparing :}}] + \def\rowOffset{\yellowm{0}} + we impose that + \[ + \wcpCallToIszero { + anchorRow = i , + relOffset = \rowOffset , + argOneHi = 0 , + argOneLo = \blockNumberOfFirstBlockInConflation _{i} , + } + \] + and we set + \[ + \locFirstBlockIsGenesisBlock \define \res _{i + \rowOffset} + \] + \item[\underline{\underline{\inst{NUMBER} upper bound:}}] + \def\rowOffset{\yellowm{1}} + \If $\locIsPrevConf _{i} = 1$ \Then + we impose that + \[ + \wcpCallToLt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = 256^\medium , + } + \] + \saNote{} + The above ensures that \inst{NUMBER} is a $\medium$-byte integer. + \item[\underline{\underline{Setting \inst{NUMBER}:}}] + since we include ``the final block of the preceding conflation'' for reference, + special care has to be taken when setting \inst{NUMBER} if the present conflation of blocks contains the genesis block. + \begin{enumerate} + \item \If $\locIsPrevConf _{i} = 1$ \Then + \begin{enumerate} + \item \If $\locFirstBlockIsGenesisBlock = 1$ \Then + we impose that + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & 0 \\ + \blockDataLo _{i} & = & 0 \\ + \end{array} \right. + \] + \item \If $\locFirstBlockIsGenesisBlock = 0$ \Then + we impose that + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & 0 \\ + \blockDataLo _{i} & = & \blockNumberOfFirstBlockInConflation _{i} - 1 \\ + \end{array} \right. + \] + \end{enumerate} + \item \If $\locIsCurrConf _{i} = 1$ \Then + we impose that + \begin{enumerate} + \item \If $\locFirstBlockIsGenesisBlock = 1$ \Then + \begin{enumerate} + \item \If $\locIsPrevConf _{i - \blockDataDepth} = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & 0 \\ + \blockDataLo _{i} & = & 0 \\ + \end{array} \right. + \] + \item \If $\locIsCurrConf _{i - \blockDataDepth} = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & \blockDataHi _{i - \blockDataDepth} \\ + \blockDataLo _{i} & = & \blockDataLo _{i - \blockDataDepth} + 1 \\ + \end{array} \right. + \] + \end{enumerate} + we impose that + \item \If $\locFirstBlockIsGenesisBlock = 0$ \Then + we impose that + \[ + \left\{ \begin{array}{lcl} + \blockDataHi _{i} & = & \blockDataHi _{i - \blockDataDepth} \\ + \blockDataLo _{i} & = & \blockDataLo _{i - \blockDataDepth} + 1 \\ + \end{array} \right. + \] + \end{enumerate} + \end{enumerate} +\end{description} diff --git a/block_data/computations/timestamp.tex b/block_data/computations/timestamp.tex new file mode 100644 index 0000000..5ce01f6 --- /dev/null +++ b/block_data/computations/timestamp.tex @@ -0,0 +1,43 @@ +\begin{center} + \boxed{\text{% + The following constraints assume that + $\left\{ \begin{array}{lcl} + \isTimestamp _{i - 1} & = & 0 \\ + \isTimestamp _{i} & = & 1 \\ + \end{array} \right.$}} +\end{center} +\begin{description} + \item[\underline{\underline{Setting \inst{TIMESTAMP}:}}] + we cannot \emph{a priori} constrain \inst{TIMESTAMP}; + \item[\underline{\underline{\inst{TIMESTAMP} upper bound:}}] + \def\rowOffset{\yellowm{0}} + we impose that + \[ + \wcpCallToLt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = 0 , + argTwoLo = 256^\medium , + } + \] + \saNote{} + The above ensures that \inst{TIMESTAMP} is a $\medium$-byte integer. + \item[\underline{\underline{\inst{TIMESTAMP} is incrementing:}}] + \def\rowOffset{\yellowm{1}} + \If $\locIsCurrConf _{i} = 1$ \Then + we impose that + \[ + \wcpCallToGt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \blockDataHi _{i} , + argOneLo = \blockDataLo _{i} , + argTwoHi = \blockDataHi _{i - \blockDataDepth} , + argTwoLo = \blockDataLo _{i - \blockDataDepth} , + } + \] + \saNote{} + The above ensures that \inst{TIMESTAMP} is incrementing from block to block. +\end{description} diff --git a/block_data/constancies.tex b/block_data/constancies.tex index e200ee1..bae7f0f 100644 --- a/block_data/constancies.tex +++ b/block_data/constancies.tex @@ -3,12 +3,21 @@ \If \ct _{i} \neq 0 ~ \Then \col{X}_{i} = \col{X}_{i - 1}. \] We impose that the following columns be counter-constant -\begin{multicols}{2} +\begin{multicols}{3} \begin{enumerate} - \item $\relTxMax$ + \item $\blockDataHi$ + \item $\blockDataLo$ \item $\coinbase\high$ \item $\coinbase\low$ - \item \blockGasLimit - \item \basefee + \item $\relTxMax$ + \item $\blockGasLimit$ + \item $\locWghtSum$ \end{enumerate} \end{multicols} +\saNote{} +The counter-constancy of $\locWghtSum$ implicitly enforces counter-constancy of all involved binary flags and thus of all expressions derived from these flags by linear combination. + +We further require that \blockNumberOfFirstBlockInConflation{} be \textbf{conflation-constant} i.e. we impose that +\begin{enumerate} + \item \If $\iomf _{i} = 1$ \et $\iomf _{i + 1} = 1$ \Then $\blockNumberOfFirstBlockInConflation _{i + 1} = \blockNumberOfFirstBlockInConflation_{i}$ +\end{enumerate} diff --git a/block_data/heartbeat.tex b/block_data/heartbeat.tex index 17eeb83..150d096 100644 --- a/block_data/heartbeat.tex +++ b/block_data/heartbeat.tex @@ -1,25 +1,67 @@ -The heartbeat is standard and simple: +We start with $\iomf$ which we require to be binary nondecreasing: \begin{enumerate} - \item $\relBlock_{0} = 0$ - \item \If $\relBlock_{i} = 0$ \Then - \[ - \left\{ \begin{array}{lcl} - \blockNumberOfFirstBlockInConflation & \!\!\! = \!\!\! & 0 \\ - \INST_{i} & \!\!\! = \!\!\! & 0 \\ - \ct_{i} & \!\!\! = \!\!\! & 0 \quad (\trash) \\ - \end{array} \right. - \] - \item $\relBlock_{i + 1} \in \{ \relBlock_{i}, 1 + \relBlock_{i} \}$ - \item \If $\relBlock_{i} \neq \relBlock_{i-1}$ \Then $\ct_{i} = 0$ - \item \If $\relBlock_{i} \neq 0$ \Then + \item $\iomf$ is binary ~ (\trash) + \item $\iomf _{0} = 0$ +\end{enumerate} +We now impose constraints related to the instruction flags \col{is\_XX}, \ct{} and \maxCt{}. +\begin{enumerate}[resume] + \item \If $\iomf _{i} = 0$ \Then \[ - \left\{ \begin{array}{lcl} - \blockNumberOfFirstBlockInConflation_{i+1} & = & \blockNumberOfFirstBlockInConflation_{i} \\ - \If \ct_{i} \neq \maxCtBtcData ~ \Then \ct_{i + 1} & = & 1 + \ct_{i} \\ - \If \ct_{i} = \maxCtBtcData ~ \Then \relBlock_{i + 1} & = & 1 + \relBlock_{i} \vspace{2mm} \\ + \left\{ \begin{array}{lclr} + \ct _{i} & = & 0 \\ + \ct _{i + 1} & = & 0 & (\sanityCheck) \\ \end{array} \right. \] - \item $\ct_{N} = \maxCtBtcData$ + \item \If $\iomf _{i} = 0$ \et $\iomf _{i + 1} = 1$ \Then $\locIsCoinbase _{i + 1} = 1$ + \item \If $\locPhaseEntry _{i} = 1$ \Then $\ct _{i + 1} = 0$ +\end{enumerate} +\begin{enumerate}[resume] + \item \If $\iomf_{i} = 1$ \Then + \begin{enumerate} + \item \If $\ct _{i} \neq \maxCt _{i}$ \Then $\ct _{i + 1} = 1 + \ct _{i}$\footnote{ + \saNote{} + This has the following implicit consequences + \[ + \left\{ \begin{array}{lclr} + \locPhaseEntry _{i} & = & 0 & (\sanityCheck) \\ + \locSamePhase _{i} & = & 1 & (\sanityCheck) \\ + \locLegalTransitions _{i} & = & 0 & (\sanityCheck) \\ + \end{array} \right. + \]} + \item \If $\ct _{i} = \maxCt _{i}$ \Then $\locLegalTransitions _{i} = 1$\footnote{ + \saNote{} + This has the following implicit consequences + \[ + \left\{ \begin{array}{lclr} + \ct _{i + 1} & = & 0 & (\sanityCheck) \\ + \locPhaseEntry _{i} & = & 1 & (\sanityCheck) \\ + \locSamePhase _{i} & = & 0 & (\sanityCheck) \\ + \end{array} \right. + \]} + \end{enumerate} +\end{enumerate} +We now impose constraints on $\relBlock$. +\begin{enumerate}[resume] + \item $\relBlock _{0} = 0$ + \item $\relBlock_{i + 1} \in \{ \relBlock_{i}, 1 + \relBlock_{i} \}$ \quad (\sanityCheck) + \item $\relBlock _{i + 1} = \relBlock _{i} + \locIsBasefee _{i} \cdot \locIsCoinbase _{i + 1}$ +\end{enumerate} +The following constraints pin down $\locIsPrevConf$ and $\locIsCurrConf$. +\begin{enumerate}[resume] + \item \If $\locIsCurrConf _{i} = 1$ \Then $\locIsCurrConf _{i + 1} = 1$ + \item \If $\iomf _{i} = 0$ \et $\iomf _{i + 1} = 1$ \Then $\locIsPrevConf _{i + 1} = 1$ + \item \If $\iomf _{i} = 1$ \et $\relBlock _{i + 1} = \relBlock _{i}$% + \footnote{In the implementation: ``\If $\iomf_{i} = 1$ \et $\relBlock _{i + 1} \neq 1 + \relBlock _{i}$ \Then $\dots$''} + \Then + \[ \locPrevCurrWghtSum _{i + 1} = \locPrevCurrWghtSum _{i} \] + \item \If $\relBlock _{i + 1} = 1 + \relBlock _{i}$% + \footnote{In the implementation: ``\If $\relBlock _{i + 1} \neq \relBlock _{i}$ \Then $\dots$''} + \Then $\locIsCurrConf _{i + 1} = 1$ +\end{enumerate} +We end on ``finalization'' constraints. +The \zkEvm{} expects to process blocks, as such we impose these constraints unconditionally. +\begin{enumerate}[resume] + \item $\locIsCurrConf _{N} = 1$ + \item $\locIsBasefee _{N} = 1$ + \item $\ct _{N} = \maxCt _{N}$ \end{enumerate} -\saNote{} -We impose the ``finalization'' constraint unconditionally as the \zkEvm{} cannot process empty conflations. diff --git a/block_data/intro.tex b/block_data/intro.tex index a8bc0e7..ef63bf8 100644 --- a/block_data/intro.tex +++ b/block_data/intro.tex @@ -1,13 +1,14 @@ The \textbf{block data} module \btcMod{} is the \zkEvm{}'s storage place for \evm{}-relevant block data of the blocks in a conflation. As such it serves the \hubMod{} data to the following instructions: -\begin{multicols}{3} +\begin{multicols}{4} \begin{enumerate} \item \inst{COINBASE} \item \inst{TIMESTAMP} \item \inst{NUMBER} - \item \inst{PREVRANDAO} + \item \inst{DIFFICULTY} \item \inst{GASLIMIT} \item \inst{CHAINID} + \item \inst{BASEFEE} \end{enumerate} \end{multicols} Along with the \textsc{rom} and the \textsc{transaction data} module it serves as an entry point of outside data into the \zkEvm{}. diff --git a/block_data/lookups/_inputs.tex b/block_data/lookups/_inputs.tex index 6b61c42..851a715 100644 --- a/block_data/lookups/_inputs.tex +++ b/block_data/lookups/_inputs.tex @@ -1,2 +1,3 @@ -\subsection{Into \wcpMod{}} \label{block_data: lookups: into_wcp} \input{lookups/btcdata_into_wcp} -\subsection{Into \txnDataMod{}} \label{block_data: lookups: into_txnDAta} \input{lookups/btcdata_into_txndata} +\subsection{Into \wcpMod{}} \label{block data: lookups: into wcp} \input{lookups/blockdata_into_wcp} +\subsection{Into \eucMod{}} \label{block data: lookups: into euc} \input{lookups/blockdata_into_euc} +\subsection{Into \txnDataMod{}} \label{block data: lookups: into txn data} \input{lookups/blockdata_into_txndata} diff --git a/block_data/lookups/blockdata_into_euc.tex b/block_data/lookups/blockdata_into_euc.tex new file mode 100644 index 0000000..232a409 --- /dev/null +++ b/block_data/lookups/blockdata_into_euc.tex @@ -0,0 +1,22 @@ +The lookup is structured as follows: +\begin{description} + \item[\underline{Selector:}] we use $\col{euc\_selector} \define \eucFlag _{i}$ + \item[\underline{Source columns:}] --- + \begin{multicols}{4} + \begin{enumerate} + \item $1$ + \item $\argOneLo _{i}$ + \item $\argTwoLo _{i}$ + \item $\res _{i}$ + \end{enumerate} + \end{multicols} + \item[\underline{Target columns:}] --- + \begin{multicols}{4} + \begin{enumerate} + \item $\iomf _{j}$ + \item $\dividend _{j}$ + \item $\divisor _{j}$ + \item $\quotient _{j}$ + \end{enumerate} + \end{multicols} +\end{description} diff --git a/block_data/lookups/blockdata_into_txndata.tex b/block_data/lookups/blockdata_into_txndata.tex new file mode 100644 index 0000000..940d993 --- /dev/null +++ b/block_data/lookups/blockdata_into_txndata.tex @@ -0,0 +1,12 @@ +The lookup is structured as follows: +\begin{description} + \item[\underline{Selector:}] none required. + \item[\underline{Source columns:}] --- + \begin{enumerate} + \item $\relBlock$ + \end{enumerate} + \item[\underline{Target columns:}] --- + \begin{enumerate} + \item $\relBlock$ + \end{enumerate} +\end{description} diff --git a/block_data/lookups/blockdata_into_wcp.tex b/block_data/lookups/blockdata_into_wcp.tex new file mode 100644 index 0000000..caf214a --- /dev/null +++ b/block_data/lookups/blockdata_into_wcp.tex @@ -0,0 +1,26 @@ +The lookup is structured as follows: +\begin{description} + \item[\underline{Selector:}] we use $\col{wcp\_selector} \define \wcpFlag _{i}$ + \item[\underline{Source columns:}] --- + \begin{multicols}{3} + \begin{enumerate} + \item $\argOneHi _{i}$ + \item $\argOneLo _{i}$ + \item $\argTwoHi _{i}$ + \item $\argTwoLo _{i}$ + \item $\res _{i}$ + \item $\exoInstruction _{i}$ + \end{enumerate} + \end{multicols} + \item[\underline{Target columns:}] --- + \begin{multicols}{3} + \begin{enumerate} + \item $\argOneHi _{j}$ + \item $\argOneLo _{j}$ + \item $\argTwoHi _{j}$ + \item $\argTwoLo _{j}$ + \item $\res _{j}$ + \item $\INST _{j}$ + \end{enumerate} + \end{multicols} +\end{description} diff --git a/block_data/lua/flags_and_ct.lua.tex b/block_data/lua/flags_and_ct.lua.tex new file mode 100644 index 0000000..f06e2d3 --- /dev/null +++ b/block_data/lua/flags_and_ct.lua.tex @@ -0,0 +1,115 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{../../pkg/draculatheme} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback + ("emojifallback", + { + "NotoColorEmoji:mode=harf;" + } + )} + +\setmonofont{JetBrains Mono NF Regular}[ + RawFeature={fallback=emojifallback} +] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +███████\ ██\ ██████\ ██████\ ██\ ██\ ███████\ ██████\ ████████\ ██████\ +██ __██\ ██ | ██ __██\ ██ __██\ ██ | ██ |██ __██\ ██ __██\\__██ __|██ __██\ +██ | ██ |██ | ██ / ██ |██ / \__|██ |██ / ██ | ██ |██ / ██ | ██ | ██ / ██ | +███████\ |██ | ██ | ██ |██ | █████ / ██ | ██ |████████ | ██ | ████████ | +██ __██\ ██ | ██ | ██ |██ | ██ ██< ██ | ██ |██ __██ | ██ | ██ __██ | +██ | ██ |██ | ██ | ██ |██ | ██\ ██ |\██\ ██ | ██ |██ | ██ | ██ | ██ | ██ | +███████ |████████\ ██████ |\██████ |██ | \██\ ███████ |██ | ██ | ██ | ██ | ██ | +\_______/ \________|\______/ \______/ \__| \__|\_______/ \__| \__| \__| \__| \__| + + + + ██████\ ██████\ ██\ ██\ ██\ + ██ __██\ ██ __██\ ██ | ██ |\__| + ███████\ ███████\ ██████\ ██ / \__|██ / \__|██████\ ██ | ███████ |██\ ███████\ ██████\ +██ _____|██ _____|\____██\ ████\ ████\ ██ __██\ ██ |██ __██ |██ |██ __██\ ██ __██\ +\██████\ ██ / ███████ |██ _| ██ _| ██ / ██ |██ |██ / ██ |██ |██ | ██ |██ / ██ | + \____██\ ██ | ██ __██ |██ | ██ | ██ | ██ |██ |██ | ██ |██ |██ | ██ |██ | ██ | +███████ |\███████\\███████ |██ | ██ | \██████ |██ |\███████ |██ |██ | ██ |\███████ | +\_______/ \_______|\_______|\__| \__| \______/ \__| \_______|\__|\__| \__| \____██ | + ██\ ██ | + \██████ | + \______/ + + +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| IOMF | is_CB | is_TS | is_NB | is_DF | is_GL | is_ID | is_BF | CT_MAX | CT | INST | is_prev | is_curr | RELBLOCK | +|:----:+:-----:+:-----:+:-----:+:-----:+:-----:+:-----:+:-----:+:------:+:--:+-----------:+:-------:+:-------:+:--------:| +| ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | | +| | | | | | | | | | | | | | | +| 0 | | | | | | | 0 | | | | | | | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | 1 | | | | | | | 0 | 0 | COINBASE | 1 | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | 1 | | | | | | 1 | 0 | TIMESTAMP | 1 | | 0 | +| 1 | | 1 | | | | | | 1 | 1 | TIMESTAMP | 1 | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | 1 | | | | | 1 | 0 | NUMBER | 1 | | 0 | +| 1 | | | 1 | | | | | 1 | 1 | NUMBER | 1 | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | 1 | | | | 0 | 0 | DIFFICULTY | 1 | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | 1 | | | 4 | 0 | GASLIMIT | 1 | | 0 | +| 1 | | | | | 1 | | | 4 | 1 | GASLIMIT | 1 | | 0 | +| 1 | | | | | 1 | | | 4 | 2 | GASLIMIT | 1 | | 0 | +| 1 | | | | | 1 | | | 4 | 3 | GASLIMIT | 1 | | 0 | +| 1 | | | | | 1 | | | 4 | 4 | GASLIMIT | 1 | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | | 1 | | 0 | 0 | CHAINID | 1 | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | | | 1 | 0 | 0 | BASEFEE | 1 | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | 1 | | | | | | | 0 | 0 | COINBASE | | 1 | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | 1 | | | | | | 1 | 0 | TIMESTAMP | | 1 | 1 | +| 1 | | 1 | | | | | | 1 | 1 | TIMESTAMP | | 1 | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | 1 | | | | | 1 | 0 | NUMBER | | 1 | 1 | +| 1 | | | 1 | | | | | 1 | 1 | NUMBER | | 1 | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | 1 | | | | 0 | 0 | DIFFICULTY | | 1 | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | 1 | | | 4 | 0 | GASLIMIT | | 1 | 1 | +| 1 | | | | | 1 | | | 4 | 1 | GASLIMIT | | 1 | 1 | +| 1 | | | | | 1 | | | 4 | 2 | GASLIMIT | | 1 | 1 | +| 1 | | | | | 1 | | | 4 | 3 | GASLIMIT | | 1 | 1 | +| 1 | | | | | 1 | | | 4 | 4 | GASLIMIT | | 1 | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | | 1 | | 0 | 0 | CHAINID | | 1 | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | | | 1 | 0 | 0 | BASEFEE | | 1 | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | 1 | | | | | | | 0 | 0 | COINBASE | | 1 | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | 1 | | | | | | 1 | 0 | TIMESTAMP | | 1 | 2 | +| 1 | | 1 | | | | | | 1 | 1 | TIMESTAMP | | 1 | 2 | +| | | | | | | | | | | | | | | +| ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | +| | | | | | | | | | | | | | | +| 1 | | | | | 1 | | | 4 | 2 | GASLIMIT | | 1 | b | +| 1 | | | | | 1 | | | 4 | 3 | GASLIMIT | | 1 | b | +| 1 | | | | | 1 | | | 4 | 4 | GASLIMIT | | 1 | b | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | | 1 | | 0 | 0 | CHAINID | | 1 | b | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| +| 1 | | | | | | | 1 | 0 | 0 | BASEFEE | | 1 | b | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+---------+---------+----------| + + +NOTE. As per usual, empty cells contain the value 0. +NOTE. The letter `b` stands for the total number of blocks in the conflation. + +\end{verbatim} +\end{document} diff --git a/block_data/lua/layout.lua.tex b/block_data/lua/layout.lua.tex index f19e06a..ecde05a 100644 --- a/block_data/lua/layout.lua.tex +++ b/block_data/lua/layout.lua.tex @@ -20,26 +20,28 @@ \begin{document} \begin{verbatim} -███████\ ██\ -██ __██\ ██ | -██ | ██ | ██████\ ██████\ ██████\ -██ | ██ | \____██\\_██ _| \____██\ -██ | ██ | ███████ | ██ | ███████ | -██ | ██ |██ __██ | ██ |██\ ██ __██ | -███████ |\███████ | \████ |\███████ | -\_______/ \_______| \____/ \_______| - -██\ ██\ -██ | ██ | -██ | ██████\ ██\ ██\ ██████\ ██\ ██\ ██████\ -██ | \____██\ ██ | ██ |██ __██\ ██ | ██ |\_██ _| -██ | ███████ |██ | ██ |██ / ██ |██ | ██ | ██ | -██ |██ __██ |██ | ██ |██ | ██ |██ | ██ | ██ |██\ -██ |\███████ |\███████ |\██████ |\██████ | \████ | -\__| \_______| \____██ | \______/ \______/ \____/ - ██\ ██ | - \██████ | - \______/ + ███████\ ██\ + ██ __██\ ██ | + ██ | ██ | ██████\ ██████\ ██████\ + ██ | ██ | \____██\\_██ _| \____██\ + ██ | ██ | ███████ | ██ | ███████ | + ██ | ██ |██ __██ | ██ |██\ ██ __██ | + ███████ |\███████ | \████ |\███████ | + \_______/ \_______| \____/ \_______| + + ██\ ██\ + ██ | ██ | + ██ | ██████\ ██\ ██\ ██████\ ██\ ██\ ██████\ + ██ | \____██\ ██ | ██ |██ __██\ ██ | ██ |\_██ _| + ██ | ███████ |██ | ██ |██ / ██ |██ | ██ | ██ | + ██ |██ __██ |██ | ██ |██ | ██ |██ | ██ | ██ |██\ + ██ |\███████ |\███████ |\██████ |\██████ | \████ | + \__| \_______| \____██ | \______/ \______/ \____/ + ██\ ██ | + \██████ | + \______/ + + |-------+-----+----------+----+-------------------+----------------+-----------------| diff --git a/block_data/representation.tex b/block_data/representation.tex new file mode 100644 index 0000000..54df267 --- /dev/null +++ b/block_data/representation.tex @@ -0,0 +1 @@ +\includepdf[fitpaper=true, pages={1}]{lua/flags_and_ct.pdf} diff --git a/block_data/shorthands.tex b/block_data/shorthands.tex new file mode 100644 index 0000000..61d0ef1 --- /dev/null +++ b/block_data/shorthands.tex @@ -0,0 +1,123 @@ +We shall often use the following shorthands for +\[ + \left\{ \begin{array}{lcl} + \previousConflation & \longleftrightarrow & \locIsPrevConf \\ + \currentConflation & \longleftrightarrow & \locIsCurrConf \\ + \isCoinbase & \longleftrightarrow & \locIsCoinbase \\ + \isTimestamp & \longleftrightarrow & \locIsTimestamp \\ + \isNumber & \longleftrightarrow & \locIsNumber \\ + \isDifficulty & \longleftrightarrow & \locIsDifficulty \\ + \isGaslimit & \longleftrightarrow & \locIsGaslimit \\ + \isChainid & \longleftrightarrow & \locIsChainid \\ + \isBasefee & \longleftrightarrow & \locIsBasefee \\ + \end{array} \right. +\] +\noindent We further define the following shorthands +\[ + \begin{array}{lcrlcr} + \locFlagSum _{i} & \define & + \left[ \begin{array}{cl} + + & \locIsCoinbase _{i} \\ + + & \locIsTimestamp _{i} \\ + + & \locIsNumber _{i} \\ + + & \locIsDifficulty _{i} \\ + + & \locIsGaslimit _{i} \\ + + & \locIsChainid _{i} \\ + + & \locIsBasefee _{i} \\ + \end{array} \right] , & + \quad \locWghtSum _{i} & \define & + \left[ \begin{array}{crcl} + + & 1 & \cdot & \locIsCoinbase _{i} \\ + + & 2 & \cdot & \locIsTimestamp _{i} \\ + + & 3 & \cdot & \locIsNumber _{i} \\ + + & 4 & \cdot & \locIsDifficulty _{i} \\ + + & 5 & \cdot & \locIsGaslimit _{i} \\ + + & 6 & \cdot & \locIsChainid _{i} \\ + + & 7 & \cdot & \locIsBasefee _{i} \\ + \end{array} \right] + \end{array} +\] +and +\[ + \begin{array}{lcrlcr} + \locInstSum _{i} & \define & + \left[ \begin{array}{crcl} + + & \inst{COINBASE} & \cdot & \locIsCoinbase _{i} \\ + + & \inst{TIMESTAMP} & \cdot & \locIsTimestamp _{i} \\ + + & \inst{NUMBER} & \cdot & \locIsNumber _{i} \\ + + & \inst{DIFFICULTY} & \cdot & \locIsDifficulty _{i} \\ + + & \inst{GASLIMIT} & \cdot & \locIsGaslimit _{i} \\ + + & \inst{CHAINID} & \cdot & \locIsChainid _{i} \\ + + & \inst{BASEFEE} & \cdot & \locIsBasefee _{i} \\ + \end{array} \right] , & + \quad \locMaxCtSum _{i} & \define & + \left[ \begin{array}{crcl} + + & (\ctMaxCoinbase - 1) & \cdot & \locIsCoinbase _{i} \\ + + & (\ctMaxTimestamp - 1) & \cdot & \locIsTimestamp _{i} \\ + + & (\ctMaxNumber - 1) & \cdot & \locIsNumber _{i} \\ + + & (\ctMaxDifficulty - 1) & \cdot & \locIsDifficulty _{i} \\ + + & (\ctMaxGaslimit - 1) & \cdot & \locIsGaslimit _{i} \\ + + & (\ctMaxChainid - 1) & \cdot & \locIsChainid _{i} \\ + + & (\ctMaxBasefee - 1) & \cdot & \locIsBasefee _{i} \\ + \end{array} \right] \\ + \end{array} +\] +where we set +\[ + \left\{ \begin{array}{lcl} + \ctMaxCoinbase & \define & \yellowm{1} \\ + \ctMaxTimestamp & \define & \yellowm{2} \\ + \ctMaxNumber & \define & \yellowm{2} \\ + \ctMaxDifficulty & \define & \yellowm{1} \\ + \end{array} \right. + \quad\text{and}\quad + \left\{ \begin{array}{lcl} + \ctMaxGaslimit & \define & \yellowm{5} \\ + \ctMaxChainid & \define & \yellowm{1} \\ + \ctMaxBasefee & \define & \yellowm{1} \\ + \blockDataDepth & \define & \sum \kappaDots \equiv \yellowm{13} \\ + \end{array} \right. +\] +We further define the following shorthands +\[ + \locPhaseEntry _{i} \define + \left[ \begin{array}{clcl} + + & (1 - \locIsCoinbase _{i}) & \cdot & \locIsCoinbase _{i + 1} \\ + + & (1 - \locIsTimestamp _{i}) & \cdot & \locIsTimestamp _{i + 1} \\ + + & (1 - \locIsNumber _{i}) & \cdot & \locIsNumber _{i + 1} \\ + + & (1 - \locIsDifficulty _{i}) & \cdot & \locIsDifficulty _{i + 1} \\ + + & (1 - \locIsGaslimit _{i}) & \cdot & \locIsGaslimit _{i + 1} \\ + + & (1 - \locIsChainid _{i}) & \cdot & \locIsChainid _{i + 1} \\ + + & (1 - \locIsBasefee _{i}) & \cdot & \locIsBasefee _{i + 1} \\ + \end{array} \right] + \quad\text{and}\quad + \locSamePhase _{i} \define + \left[ \begin{array}{clcl} + + & \locIsCoinbase _{i} & \cdot & \locIsCoinbase _{i + 1} \\ + + & \locIsTimestamp _{i} & \cdot & \locIsTimestamp _{i + 1} \\ + + & \locIsNumber _{i} & \cdot & \locIsNumber _{i + 1} \\ + + & \locIsDifficulty _{i} & \cdot & \locIsDifficulty _{i + 1} \\ + + & \locIsGaslimit _{i} & \cdot & \locIsGaslimit _{i + 1} \\ + + & \locIsChainid _{i} & \cdot & \locIsChainid _{i + 1} \\ + + & \locIsBasefee _{i} & \cdot & \locIsBasefee _{i + 1} \\ + \end{array} \right] +\] +and +\[ + \locLegalTransitions _{i} \define + \left[ \begin{array}{clcl} + + & \locIsCoinbase _{i} & \cdot & \locIsTimestamp _{i + 1} \\ + + & \locIsTimestamp _{i} & \cdot & \locIsNumber _{i + 1} \\ + + & \locIsNumber _{i} & \cdot & \locIsDifficulty _{i + 1} \\ + + & \locIsDifficulty _{i} & \cdot & \locIsGaslimit _{i + 1} \\ + + & \locIsGaslimit _{i} & \cdot & \locIsChainid _{i + 1} \\ + + & \locIsChainid _{i} & \cdot & \locIsBasefee _{i + 1} \\ + + & \locIsBasefee _{i} & \cdot & \locIsCoinbase _{i + 1} \\ + \end{array} \right] +\] +Finally, we define +\[ + \locPrevCurrWghtSum _{i} + \define + \locIsCurrConf _{i} + 2 \cdot \locIsPrevConf _{i} +\] diff --git a/block_data/unconditional.tex b/block_data/unconditional.tex new file mode 100644 index 0000000..76b6c3e --- /dev/null +++ b/block_data/unconditional.tex @@ -0,0 +1,16 @@ +We unconditionally impose that +\[ + \left\{ \begin{array}{lcl} + \iomf _{i} & = & \locFlagSum _{i} \\ + \iomf _{i} & = & \locIsPrevConf _{i} + \locIsCurrConf _{i} \\ + \maxCt _{i} & = & \locMaxCtSum _{i} \\ + \instruction _{i} & = & \locInstSum _{i} \\ + \end{array} \right. +\] +\saNote{} +The first two constraints implicitly impose flag exclusivity constraints. +They further imply that all of +$\locPhaseEntry$, +$\locSamePhase$ and +$\locLegalTransitions$ +are \textbf{binary}. diff --git a/hub/lookups/into_block_data.tex b/hub/lookups/into_block_data.tex index 3b85e8e..edc923f 100644 --- a/hub/lookups/into_block_data.tex +++ b/hub/lookups/into_block_data.tex @@ -12,8 +12,10 @@ \end{array} \right] \] \item[Source columns:] --- - \begin{multicols}{2} + \begin{multicols}{3} \begin{enumerate} + \item $1$ + \item[\vspace{\fill}] \item $\relativeBlockNumber _{i}$ \item $\stackInst _{i}$ \item $\stackItemValHi {4} _{i}$ @@ -21,12 +23,14 @@ \end{enumerate} \end{multicols} \item[Target columns:] --- - \begin{multicols}{2} + \begin{multicols}{3} \begin{enumerate} - \item $\relBlock _{j}$ - \item $\INST _{j}$ - \item $\blockDataHi _{j}$ - \item $\blockDataLo _{j}$ + \item $\currentConflation _{j}$ + \item[\vspace{\fill}] + \item $\relBlock _{j}$ + \item $\INST _{j}$ + \item $\blockDataHi _{j}$ + \item $\blockDataLo _{j}$ \end{enumerate} \end{multicols} \end{description} diff --git a/pkg/block_data.sty b/pkg/block_data.sty index 711b158..9caa890 100644 --- a/pkg/block_data.sty +++ b/pkg/block_data.sty @@ -23,3 +23,13 @@ \newcommand{\rowShiftGaslimit} {\redm{4}} \newcommand{\rowShiftChainId} {\redm{5}} \newcommand{\rowShiftBaseFee} {\redm{6}} + +\newcommand{\isCoinbase} {\col{IS\_COINBASE}} +\newcommand{\isTimestamp} {\col{IS\_TIMESTAMP}} +\newcommand{\isNumber} {\col{IS\_NUMBER}} +\newcommand{\isDifficulty} {\col{IS\_DIFFICULTY}} +\newcommand{\isGaslimit} {\col{IS\_GASLIMIT}} +\newcommand{\isChainid} {\col{IS\_CHAINID}} +\newcommand{\isBasefee} {\col{IS\_BASEFEE}} +\newcommand{\previousConflation} {\col{PREVIOUS\_CONFLATION}} +\newcommand{\currentConflation} {\col{CURRENT\_CONFLATION}} diff --git a/pkg/env.sty b/pkg/env.sty index 7b7576d..daa8a5e 100644 --- a/pkg/env.sty +++ b/pkg/env.sty @@ -334,9 +334,11 @@ \newcommand{\stoFirst} {\order{\storageSignifier\first}} \newcommand{\stoFinal} {\order{\storageSignifier\final}} -\newcommand{\blockData} {\blockSignifier\col{DATA}} -\newcommand{\blockDataHi} {\blockData\col{\_HI}} -\newcommand{\blockDataLo} {\blockData\col{\_LO}} +\newcommand{\blockData} {\blockSignifier\col{DATA}} +\newcommand{\blockDataHi} {\blockData\col{\_HI}} +\newcommand{\blockDataLo} {\blockData\col{\_LO}} +\newcommand{\auxiliaryDataHi} {\col{AUX\_DATA\_HI}} +\newcommand{\auxiliaryDataLo} {\col{AUX\_DATA\_LO}} \newcommand{\gas}{\col{GAS}} \newcommand{\gasExpected} {\gas\col{\_XPCT}} diff --git a/pkg/rom.sty b/pkg/rom.sty index 26342f8..5b7c04d 100644 --- a/pkg/rom.sty +++ b/pkg/rom.sty @@ -96,6 +96,7 @@ \newcommand{\pfb}{\col{PFB}} \newcommand{\INST}{\col{INST}} +\newcommand{\instruction}{\col{INST}} \newcommand{\HIGH}{\col{\_HIGH}} \newcommand{\LOW}{\col{\_LOW}} diff --git a/pkg/xkeyval_macros/euc_calls.sty b/pkg/xkeyval_macros/euc_calls.sty new file mode 100644 index 0000000..d022f99 --- /dev/null +++ b/pkg/xkeyval_macros/euc_calls.sty @@ -0,0 +1,32 @@ +\makeatletter +% DEFINING KEYS + +\define@cmdkey [EUC] {var} {anchorRow} {} % "i" in the spec, ALWAYS use this name +\define@cmdkey [EUC] {var} {relOffset} {} % relative offset, ALWAYS use this name +\define@cmdkey [EUC] {var} {argOne} {} +\define@cmdkey [EUC] {var} {argTwo} {} +\define@cmdkey [EUC] {var} {result} {} +% the above defines macros à la "\cmdWCP@var@anchorRow" + +% DEFAULT VALUES +\presetkeys [EUC] {var} { + anchorRow = \missingParameter, + relOffset = \missingParameter, + argOne = \missingParameter, + argTwo = \missingParameter, + result = \missingParameter, +}{} + +% "call to LEQ" macro +\newcommand{\eucCallName} {\texttt{eucCall}} +\newcommand{\eucCall} [1] { + \setkeys[EUC]{var}{#1} + \eucCallName _{\cmdEUC@var@anchorRow} + \left[ \begin{array}{ll} + \utt{Rel. row offset:} & \cmdEUC@var@relOffset \\ + \utt{First argument:} & \cmdEUC@var@argOne \\ + \utt{Second argument:} & \cmdEUC@var@argTwo \\ + \end{array} \right] +} + +\makeatother diff --git a/pkg/xkeyval_macros/wcp_calls.sty b/pkg/xkeyval_macros/wcp_calls.sty index a4d97b7..4d23e8c 100644 --- a/pkg/xkeyval_macros/wcp_calls.sty +++ b/pkg/xkeyval_macros/wcp_calls.sty @@ -19,33 +19,59 @@ argTwoLo = \missingParameter, }{} +% "call to LEQ" macro +\newcommand{\wcpCallToLeqName} {\texttt{wcpCallToLEQ}} +\newcommand{\wcpCallToLeq} [1] { + \setkeys[WCP]{var}{#1} + \wcpCallToLeqName _{\cmdWCP@var@anchorRow} + \left[ \begin{array}{ll} + \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ + \utt{First argument hi:} & \cmdWCP@var@argOneHi \\ + \utt{First argument lo:} & \cmdWCP@var@argOneLo \\ + \utt{Second argument hi:} & \cmdWCP@var@argTwoHi \\ + \utt{Second argument lo:} & \cmdWCP@var@argTwoLo \\ + \end{array} \right] +} + +% "call to GEQ" macro +\newcommand{\wcpCallToGeqName} {\texttt{wcpCallToGEQ}} +\newcommand{\wcpCallToGeq} [1] { + \setkeys[WCP]{var}{#1} + \wcpCallToGeqName _{\cmdWCP@var@anchorRow} + \left[ \begin{array}{ll} + \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ + \utt{First argument hi:} & \cmdWCP@var@argOneHi \\ + \utt{First argument lo:} & \cmdWCP@var@argOneLo \\ + \utt{Second argument hi:} & \cmdWCP@var@argTwoHi \\ + \utt{Second argument lo:} & \cmdWCP@var@argTwoLo \\ + \end{array} \right] +} + % "call to LT" macro \newcommand{\wcpCallToLtName} {\texttt{wcpCallToLT}} \newcommand{\wcpCallToLt} [1] { \setkeys[WCP]{var}{#1} \wcpCallToLtName _{\cmdWCP@var@anchorRow} \left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ - \utt{First argument (high):} & \cmdWCP@var@argOneHi \\ - \utt{First argument (low):} & \cmdWCP@var@argOneLo \\ - \utt{Second argument (high):} & \cmdWCP@var@argTwoHi \\ - \utt{Second argument (low):} & \cmdWCP@var@argTwoLo \\ + \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ + \utt{First argument hi:} & \cmdWCP@var@argOneHi \\ + \utt{First argument lo:} & \cmdWCP@var@argOneLo \\ + \utt{Second argument hi:} & \cmdWCP@var@argTwoHi \\ + \utt{Second argument lo:} & \cmdWCP@var@argTwoLo \\ \end{array} \right] } -% Note: \utt{...} is a Latex macro for \underline{\texttt{...}} -% \utt is the recommended style for such macros % "call to GT" macro \newcommand{\wcpCallToGtName} {\texttt{wcpCallToGT}} \newcommand{\wcpCallToGt} [1] { \setkeys[WCP]{var}{#1} - \wcpCallToLtName _{\cmdWCP@var@anchorRow} + \wcpCallToGtName _{\cmdWCP@var@anchorRow} \left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ - \utt{First argument (high):} & \cmdWCP@var@argOneHi \\ - \utt{First argument (low):} & \cmdWCP@var@argOneLo \\ - \utt{Second argument (high):} & \cmdWCP@var@argTwoHi \\ - \utt{Second argument (low):} & \cmdWCP@var@argTwoLo \\ + \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ + \utt{First argument hi:} & \cmdWCP@var@argOneHi \\ + \utt{First argument lo:} & \cmdWCP@var@argOneLo \\ + \utt{Second argument hi:} & \cmdWCP@var@argTwoHi \\ + \utt{Second argument lo:} & \cmdWCP@var@argTwoLo \\ \end{array} \right] } @@ -55,11 +81,11 @@ \setkeys[WCP]{var}{#1} \wcpCallToEqName _{\cmdWCP@var@anchorRow} \left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ - \utt{First argument (high):} & \cmdWCP@var@argOneHi \\ - \utt{First argument (low):} & \cmdWCP@var@argOneLo \\ - \utt{Second argument (high):} & \cmdWCP@var@argTwoHi \\ - \utt{Second argument (low):} & \cmdWCP@var@argTwoLo \\ + \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ + \utt{First argument hi:} & \cmdWCP@var@argOneHi \\ + \utt{First argument lo:} & \cmdWCP@var@argOneLo \\ + \utt{Second argument hi:} & \cmdWCP@var@argTwoHi \\ + \utt{Second argument lo:} & \cmdWCP@var@argTwoLo \\ \end{array} \right] } @@ -69,9 +95,9 @@ \setkeys[WCP]{var}{#1} \wcpCallToIszeroName _{\cmdWCP@var@anchorRow} \left[ \begin{array}{ll} - \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ - \utt{Argument (high):} & \cmdWCP@var@argOneHi \\ - \utt{Argument (low):} & \cmdWCP@var@argOneLo \\ + \utt{Rel. row offset:} & \cmdWCP@var@relOffset \\ + \utt{First argument hi:} & \cmdWCP@var@argOneHi \\ + \utt{First argument lo:} & \cmdWCP@var@argOneLo \\ \end{array} \right] } diff --git a/txn_data/lookups/into_block_data.tex b/txn_data/lookups/into_block_data.tex index 6475730..be43731 100644 --- a/txn_data/lookups/into_block_data.tex +++ b/txn_data/lookups/into_block_data.tex @@ -1,28 +1,37 @@ Several columns are direct imports from the \btcMod{} module. The present lookup justifies them: \begin{description} - \item[\underline{Selector:}] none required; + \item[\underline{Selector:}] + we define the following selector + \begin{enumerate} + \item \If $\absTxNum _{i} = 0$ \Then $\col{sel}_{i} \define 0$ + \item \If $\absTxNum _{i} \neq 0$ \Then $\col{sel}_{i} \define 1$ + \end{enumerate} \item[\underline{Source columns:}] --- - \begin{multicols}{2} + \begin{multicols}{4} \begin{enumerate} - \item $\relBlock$ - \item $\txCoinbase\high$ - \item $\txCoinbase\low$ - \item $\relTxMax$ - \item $\txBasefee$ - \item $\blockGasLimit$ + \item $\relBlock _{i}$ + \item $\relTxMax _{i}$ + \item $\txCoinbase\high _{i}$ + \item $\txCoinbase\low _{i}$ + \item $\txBasefee _{i}$ + \item $\blockGasLimit _{i}$ + \item $1$ + \item[\vspace{\fill}] %\item[\vspace{\fill}] \end{enumerate} \end{multicols} \item[\underline{Target columns:}] --- - \begin{multicols}{2} + \begin{multicols}{4} \begin{enumerate} - \item $\relBlock$ - \item $\coinbase\high$ - \item $\coinbase\low$ - \item $\relTxMax$ - \item $\basefee$ - \item $\blockGasLimit$ + \item $\relBlock _{j}$ + \item $\relTxMax _{j}$ + \item $\coinbase\high _{j}$ + \item $\coinbase\low _{j}$ + \item $\basefee _{j}$ + \item $\blockGasLimit _{j}$ + \item $\currentConflation _{j}$ + \item[\vspace{\fill}] %\item[\vspace{\fill}] \end{enumerate} \end{multicols} diff --git a/zzz_block_data/_all_block_data.tex b/zzz_block_data/_all_block_data.tex new file mode 100644 index 0000000..b9803b5 --- /dev/null +++ b/zzz_block_data/_all_block_data.tex @@ -0,0 +1,41 @@ +\documentclass{article} +\usepackage[dvipsnames]{xcolor} +\usepackage{../pkg/common} +% \usepackage{../pkg/dark_theme} +\usepackage{../pkg/std} +\usepackage{../pkg/IEEEtrantools} +\usepackage{../pkg/rom} +\usepackage{../pkg/bin} +\usepackage{../pkg/wc3} +\usepackage{../pkg/ram} +\usepackage{../pkg/alu} +\usepackage{../pkg/env} +\usepackage{../pkg/warm} +\usepackage{../pkg/storage} +\usepackage{../pkg/call_stack} +\usepackage{../pkg/access} +\usepackage{../pkg/expansion} +\usepackage{../pkg/exceptions} +\usepackage{../pkg/exponent} +\usepackage{../pkg/thm_env} +\usepackage{../pkg/trm} +\usepackage{../pkg/flags_stamps_selectors} +\usepackage{../pkg/instruction_flags} +\usepackage{../pkg/block_data} +\usepackage{../pkg/block_hash} +\usepackage{../pkg/txn_data} + +\usepackage{../pkg/draculatheme} + +\title{Block data module} +\author{Rollup team} +\date{March 2023} + +\begin{document} + +\maketitle +\tableofcontents + +\input{_inputs} + +\end{document} diff --git a/zzz_block_data/_inputs.tex b/zzz_block_data/_inputs.tex new file mode 100644 index 0000000..8793306 --- /dev/null +++ b/zzz_block_data/_inputs.tex @@ -0,0 +1,13 @@ +\section{Block data module} +\subsection{Introduction} \label{block data: intro} \input{intro} +\subsection{Columns} \label{block data: columns} \input{columns} + +\section{Constraints} +\subsection{Heartbeat} \label{block data: heartbeat} \input{heartbeat} +\subsection{Constancies} \label{block data: constancies} \input{constancies} +\subsection{Bytehood and byte decomposition constraints} \label{block data: byte decomposition} \input{byteDec} +\subsection{Value Constraints} \label{block data: value constraints} \input{value_constraint} + +\section{Lookups} \label{block data: lookups} \input{lookups/_inputs} + + diff --git a/block_data/byteDec.tex b/zzz_block_data/byteDec.tex similarity index 100% rename from block_data/byteDec.tex rename to zzz_block_data/byteDec.tex diff --git a/zzz_block_data/columns.tex b/zzz_block_data/columns.tex new file mode 100644 index 0000000..d0679df --- /dev/null +++ b/zzz_block_data/columns.tex @@ -0,0 +1,29 @@ +We remind the reader that \ccc{} stands for ``counter-constant column.'' +\begin{enumerate} + \item $\ct$: + counter column; hovers around zero and then cycles from $0$ to $\maxCtBtcData$; + \item \blockNumberOfFirstBlockInConflation{}: + ``conflation-constant'' column containing the block number\footnote{In the sense of the \evm{}} of the first block of this conflation; + \item $\relBlock$: + \ccc{} containing the relative block number; + \item $\relTxMax$: + \ccc{} containing the number of transactions in this block; + \item $\INST$: + instruction column; + \item $\blockDataHi$, $\blockDataLo$: + columns containing block data; + \item $\coinbase\high$ and $\coinbase\low$: + \ccc{} containing the + coinbase address; + \item \blockGasLimit{}: + \ccc{} containing the + block gas limit; + \item \basefee{}: + \ccc{} containing the + base fee; + \item $\byteCol{HI\_k}$, and $\byteCol{LO\_k}$, $k = 0, 1, \dots, \llargeMO$: + \item $\wcpFlag$: + binary flags used as selector for lookups; +\end{enumerate} +\saNote{} +The \INST{} column is $0$ during padding then cycles through a selection of ``block data'' specific opcodes e.g. \texttt{0x\,10} (i.e. \inst{COINBASE}), \texttt{0x\,46} (i.e. \inst{CHAINID}) etc\dots{} see section~(\ref{block data: value constraints}). diff --git a/zzz_block_data/constancies.tex b/zzz_block_data/constancies.tex new file mode 100644 index 0000000..e200ee1 --- /dev/null +++ b/zzz_block_data/constancies.tex @@ -0,0 +1,14 @@ +As per usual we declare a column \col{X} to be \textbf{counter-constant} if it satisfies +\[ + \If \ct _{i} \neq 0 ~ \Then \col{X}_{i} = \col{X}_{i - 1}. +\] +We impose that the following columns be counter-constant +\begin{multicols}{2} + \begin{enumerate} + \item $\relTxMax$ + \item $\coinbase\high$ + \item $\coinbase\low$ + \item \blockGasLimit + \item \basefee + \end{enumerate} +\end{multicols} diff --git a/zzz_block_data/heartbeat.tex b/zzz_block_data/heartbeat.tex new file mode 100644 index 0000000..17eeb83 --- /dev/null +++ b/zzz_block_data/heartbeat.tex @@ -0,0 +1,25 @@ +The heartbeat is standard and simple: +\begin{enumerate} + \item $\relBlock_{0} = 0$ + \item \If $\relBlock_{i} = 0$ \Then + \[ + \left\{ \begin{array}{lcl} + \blockNumberOfFirstBlockInConflation & \!\!\! = \!\!\! & 0 \\ + \INST_{i} & \!\!\! = \!\!\! & 0 \\ + \ct_{i} & \!\!\! = \!\!\! & 0 \quad (\trash) \\ + \end{array} \right. + \] + \item $\relBlock_{i + 1} \in \{ \relBlock_{i}, 1 + \relBlock_{i} \}$ + \item \If $\relBlock_{i} \neq \relBlock_{i-1}$ \Then $\ct_{i} = 0$ + \item \If $\relBlock_{i} \neq 0$ \Then + \[ + \left\{ \begin{array}{lcl} + \blockNumberOfFirstBlockInConflation_{i+1} & = & \blockNumberOfFirstBlockInConflation_{i} \\ + \If \ct_{i} \neq \maxCtBtcData ~ \Then \ct_{i + 1} & = & 1 + \ct_{i} \\ + \If \ct_{i} = \maxCtBtcData ~ \Then \relBlock_{i + 1} & = & 1 + \relBlock_{i} \vspace{2mm} \\ + \end{array} \right. + \] + \item $\ct_{N} = \maxCtBtcData$ +\end{enumerate} +\saNote{} +We impose the ``finalization'' constraint unconditionally as the \zkEvm{} cannot process empty conflations. diff --git a/zzz_block_data/intro.tex b/zzz_block_data/intro.tex new file mode 100644 index 0000000..a8bc0e7 --- /dev/null +++ b/zzz_block_data/intro.tex @@ -0,0 +1,14 @@ +The \textbf{block data} module \btcMod{} is the \zkEvm{}'s storage place for \evm{}-relevant block data of the blocks in a conflation. +As such it serves the \hubMod{} data to the following instructions: +\begin{multicols}{3} + \begin{enumerate} + \item \inst{COINBASE} + \item \inst{TIMESTAMP} + \item \inst{NUMBER} + \item \inst{PREVRANDAO} + \item \inst{GASLIMIT} + \item \inst{CHAINID} + \end{enumerate} +\end{multicols} +Along with the \textsc{rom} and the \textsc{transaction data} module it serves as an entry point of outside data into the \zkEvm{}. +As such one of its duties is to make sure the data it serves is correctly segmented (i.e. satisfies size constraints.) diff --git a/zzz_block_data/lookups/_inputs.tex b/zzz_block_data/lookups/_inputs.tex new file mode 100644 index 0000000..6b61c42 --- /dev/null +++ b/zzz_block_data/lookups/_inputs.tex @@ -0,0 +1,2 @@ +\subsection{Into \wcpMod{}} \label{block_data: lookups: into_wcp} \input{lookups/btcdata_into_wcp} +\subsection{Into \txnDataMod{}} \label{block_data: lookups: into_txnDAta} \input{lookups/btcdata_into_txndata} diff --git a/block_data/lookups/btcdata_into_txndata.tex b/zzz_block_data/lookups/btcdata_into_txndata.tex similarity index 100% rename from block_data/lookups/btcdata_into_txndata.tex rename to zzz_block_data/lookups/btcdata_into_txndata.tex diff --git a/block_data/lookups/btcdata_into_wcp.tex b/zzz_block_data/lookups/btcdata_into_wcp.tex similarity index 100% rename from block_data/lookups/btcdata_into_wcp.tex rename to zzz_block_data/lookups/btcdata_into_wcp.tex diff --git a/zzz_block_data/lua/layout.lua.tex b/zzz_block_data/lua/layout.lua.tex new file mode 100644 index 0000000..f19e06a --- /dev/null +++ b/zzz_block_data/lua/layout.lua.tex @@ -0,0 +1,74 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\usepackage{../../pkg/draculatheme} + +\usepackage{fontspec} +\directlua{luaotfload.add_fallback + ("emojifallback", + { + "NotoColorEmoji:mode=harf;" + } + )} + +\setmonofont{JetBrains Mono NF Regular}[ + RawFeature={fallback=emojifallback} +] + +\usepackage{../../pkg/draculatheme} + +\begin{document} +\begin{verbatim} + +███████\ ██\ +██ __██\ ██ | +██ | ██ | ██████\ ██████\ ██████\ +██ | ██ | \____██\\_██ _| \____██\ +██ | ██ | ███████ | ██ | ███████ | +██ | ██ |██ __██ | ██ |██\ ██ __██ | +███████ |\███████ | \████ |\███████ | +\_______/ \_______| \____/ \_______| + +██\ ██\ +██ | ██ | +██ | ██████\ ██\ ██\ ██████\ ██\ ██\ ██████\ +██ | \____██\ ██ | ██ |██ __██\ ██ | ██ |\_██ _| +██ | ███████ |██ | ██ |██ / ██ |██ | ██ | ██ | +██ |██ __██ |██ | ██ |██ | ██ |██ | ██ | ██ |██\ +██ |\███████ |\███████ |\██████ |\██████ | \████ | +\__| \_______| \____██ | \______/ \______/ \____/ + ██\ ██ | + \██████ | + \______/ + + +|-------+-----+----------+----+-------------------+----------------+-----------------| +| BTC_∞ | BTC | REL_∞ | CT | INST | BTC_DATA_HI | BTC_DATA_LO | +|:-----:+:---:+:--------:+:--:+:------------------+:--------------:+:---------------:| +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | a | r_∞[b-1] | ⋯ | ⋯ | ⋯ | ⋯ | +|-------+-----+----------+----+-------------------+----------------+-----------------| +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | b | r_∞[b] | 0 | 0x40 (BLOCKHASH) | 0 | 0 | +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | b | r_∞[b] | 1 | 0x41 (COINBASE) | COINBASE_HI | COINBASE_HI | +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | b | r_∞[b] | 2 | 0x42 (TIMESTAMP) | 0 | TIME_STAMP | +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | b | r_∞[b] | 3 | 0x43 (NUMBER) | 0 | BLOCK_NUMBER | +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | b | r_∞[b] | 4 | 0x44 (PREVRANDAO) | PREV_RANDAO_HI | PREV_RANDAO_LO | +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | b | r_∞[b] | 5 | 0x45 (GASLIMIT) | 0 | BLOCK_GAS_LIMIT | +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | b | r_∞[b] | 6 | 0x46 (CHAINID) | 0 | LINEA_CHAIN_ID | +|-------+-----+----------+----+-------------------+----------------+-----------------| +|-------+-----+----------+----+-------------------+----------------+-----------------| +| b_∞ | c | r_∞[b-1] | ⋯ | ⋯ | ⋯ | ⋯ | + +NOTE. The above contains BLOCKHASH which is incorrect. This opcode is dealt with +differently. Atm the design is "spit out the correct (unjustified) result." We could +easily improve on this design (see #382) but for now we will just deal with the opcode +as specified in the design docs. +\end{verbatim} +\end{document} diff --git a/block_data/value_constraint.tex b/zzz_block_data/value_constraint.tex similarity index 100% rename from block_data/value_constraint.tex rename to zzz_block_data/value_constraint.tex