BLOCKDATA redesign

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}
 

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}

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

block_data/binarities.tex

@@ -0,0 +1,14 @@
+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$
+	\end{enumerate}
+\end{multicols}

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

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

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}

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}

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}

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}