From e4b5c181dadc37236df638db280508d373bb7fff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= <38285177+OlivierBBB@users.noreply.github.com> Date: Fri, 20 Dec 2024 11:17:14 +0700 Subject: [PATCH] BLOCKDATA redesign (#19) --- block_data/_all_block_data.tex | 8 +- block_data/_inputs.tex | 21 +-- block_data/_local.tex | 89 ++++++++++++ block_data/binarities.tex | 13 ++ block_data/calls.tex | 106 +++++++++++++++ block_data/columns.tex | 53 ++++++-- block_data/computations/_inputs.tex | 7 + block_data/computations/basefee.tex | 44 ++++++ block_data/computations/chainid.tex | 53 ++++++++ block_data/computations/coinbase.tex | 41 ++++++ block_data/computations/difficulty.tex | 39 ++++++ block_data/computations/gaslimit.tex | 126 +++++++++++++++++ block_data/computations/number.tex | 80 +++++++++++ block_data/computations/timestamp.tex | 56 ++++++++ block_data/constancies.tex | 17 ++- block_data/heartbeat.tex | 70 +++++++--- block_data/intro.tex | 5 +- block_data/lookups/_inputs.tex | 6 +- block_data/lookups/blockdata_into_euc.tex | 22 +++ block_data/lookups/blockdata_into_txndata.tex | 12 ++ block_data/lookups/blockdata_into_wcp.tex | 26 ++++ block_data/lookups/prover_data_extraction.tex | 28 ++++ block_data/lua/flags_and_ct.lua.tex | 115 ++++++++++++++++ block_data/lua/layout.lua.tex | 42 +++--- block_data/notes.md | 42 ++++++ block_data/representation.tex | 1 + block_data/shorthands.tex | 127 ++++++++++++++++++ block_data/unconditional.tex | 15 +++ hub/lookups/into_block_data.tex | 16 ++- pkg/block_data.sty | 10 ++ pkg/env.sty | 8 +- pkg/rom.sty | 1 + pkg/xkeyval_macros/euc_calls.sty | 32 +++++ pkg/xkeyval_macros/wcp_calls.sty | 68 +++++++--- txn_data/lookups/into_block_data.tex | 39 +++--- zzz_block_data/_all_block_data.tex | 41 ++++++ zzz_block_data/_inputs.tex | 13 ++ {block_data => zzz_block_data}/byteDec.tex | 0 zzz_block_data/columns.tex | 29 ++++ zzz_block_data/constancies.tex | 14 ++ zzz_block_data/heartbeat.tex | 25 ++++ zzz_block_data/intro.tex | 14 ++ zzz_block_data/lookups/_inputs.tex | 2 + .../lookups/btcdata_into_txndata.tex | 0 .../lookups/btcdata_into_wcp.tex | 0 zzz_block_data/lua/layout.lua.tex | 74 ++++++++++ .../value_constraint.tex | 0 47 files changed, 1533 insertions(+), 117 deletions(-) create mode 100644 block_data/_local.tex create mode 100644 block_data/binarities.tex create mode 100644 block_data/calls.tex create mode 100644 block_data/computations/_inputs.tex create mode 100644 block_data/computations/basefee.tex create mode 100644 block_data/computations/chainid.tex create mode 100644 block_data/computations/coinbase.tex create mode 100644 block_data/computations/difficulty.tex create mode 100644 block_data/computations/gaslimit.tex create mode 100644 block_data/computations/number.tex create mode 100644 block_data/computations/timestamp.tex create mode 100644 block_data/lookups/blockdata_into_euc.tex create mode 100644 block_data/lookups/blockdata_into_txndata.tex create mode 100644 block_data/lookups/blockdata_into_wcp.tex create mode 100644 block_data/lookups/prover_data_extraction.tex create mode 100644 block_data/lua/flags_and_ct.lua.tex create mode 100644 block_data/notes.md create mode 100644 block_data/representation.tex create mode 100644 block_data/shorthands.tex create mode 100644 block_data/unconditional.tex create mode 100644 pkg/xkeyval_macros/euc_calls.sty create mode 100644 zzz_block_data/_all_block_data.tex create mode 100644 zzz_block_data/_inputs.tex rename {block_data => zzz_block_data}/byteDec.tex (100%) create mode 100644 zzz_block_data/columns.tex create mode 100644 zzz_block_data/constancies.tex create mode 100644 zzz_block_data/heartbeat.tex create mode 100644 zzz_block_data/intro.tex create mode 100644 zzz_block_data/lookups/_inputs.tex rename {block_data => zzz_block_data}/lookups/btcdata_into_txndata.tex (100%) rename {block_data => zzz_block_data}/lookups/btcdata_into_wcp.tex (100%) create mode 100644 zzz_block_data/lua/layout.lua.tex rename {block_data => zzz_block_data}/value_constraint.tex (100%) 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..4cbde9d --- /dev/null +++ b/block_data/_local.tex @@ -0,0 +1,89 @@ +\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\locExtractor {\col{extractor}} + +\def\ctMaxCoinbase {\redm{\texttt{nRows}_{\texttt{cb}}}} +\def\ctMaxTimestamp {\redm{\texttt{nRows}_{\texttt{ts}}}} +\def\ctMaxNumber {\redm{\texttt{nRows}_{\texttt{nb}}}} +\def\ctMaxDifficulty {\redm{\texttt{nRows}_{\texttt{df}}}} +\def\ctMaxGaslimit {\redm{\texttt{nRows}_{\texttt{gl}}}} +\def\ctMaxChainid {\redm{\texttt{nRows}_{\texttt{id}}}} +\def\ctMaxBasefee {\redm{\texttt{nRows}_{\texttt{bf}}}} +\def\kappaDots {\redm{\texttt{nRows}_{\texttt{xx}}}} +\def\blockDataDepth {\redm{\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}} +\def\ethereumMinBlockGasLimit {\red{\texttt{ETHEREUM\_MIN\_BLOCK\_GAS\_LIMIT}}} +\def\lineaMinBlockGasLimit {\red{\texttt{LINEA\_MIN\_BLOCK\_GAS\_LIMIT}}} +\def\lineaMaxBlockGasLimit {\red{\texttt{LINEA\_MAX\_BLOCK\_GAS\_LIMIT}}} +\def\ethereumMinBlockGasLimitValue {\texttt{5\_000}} +\def\lineaMinBlockGasLimitValue {\texttt{61\_000\_000}} +\def\lineaMaxBlockGasLimitValue {\texttt{2\_000\_000\_000}} +\def\ethereumGasLimitAdjustmentFactor {\red{\texttt{GAS\_LIMIT\_ADJUSTMENT\_FACTOR}}} +\def\ethereumGasLimitAdjustmentFactorValue {\texttt{1024}} + +\def\locIsFirstBlock {\col{is\_first\_block}} +\def\locIsntFirstBlock {\col{isnt\_first\_block}} +\def\currDataHi {\col{curr\_data\_hi}} +\def\currDataLo {\col{curr\_data\_lo}} +\def\prevDataHi {\col{prev\_data\_hi}} +\def\prevDataLo {\col{prev\_data\_lo}} + +\def\currBaseFeeHi {\col{curr\_BASEFEE\_hi}} +\def\currBaseFeeLo {\col{curr\_BASEFEE\_lo}} +\def\prevBaseFeeHi {\col{prev\_BASEFEE\_hi}} +\def\prevBaseFeeLo {\col{prev\_BASEFEE\_lo}} + +\def\currChainIdHi {\col{curr\_CHAINID\_hi}} +\def\currChainIdLo {\col{curr\_CHAINID\_lo}} +\def\prevChainIdHi {\col{prev\_CHAINID\_hi}} +\def\prevChainIdLo {\col{prev\_CHAINID\_lo}} + +\def\currCoinbaseHi {\col{curr\_COINBASE\_hi}} +\def\currCoinbaseLo {\col{curr\_COINBASE\_lo}} +\def\prevCoinbaseHi {\col{prev\_COINBASE\_hi}} +\def\prevCoinbaseLo {\col{prev\_COINBASE\_lo}} + +\def\currDifficultyHi {\col{curr\_DIFFICULTY\_hi}} +\def\currDifficultyLo {\col{curr\_DIFFICULTY\_lo}} +\def\prevDifficultyHi {\col{prev\_DIFFICULTY\_hi}} +\def\prevDifficultyLo {\col{prev\_DIFFICULTY\_lo}} + +\def\currGasLimitHi {\col{curr\_GASLIMIT\_hi}} +\def\currGasLimitLo {\col{curr\_GASLIMIT\_lo}} +\def\prevGasLimitHi {\col{prev\_GASLIMIT\_hi}} +\def\prevGasLimitLo {\col{prev\_GASLIMIT\_lo}} + +\def\currNumberHi {\col{curr\_NUMBER\_hi}} +\def\currNumberLo {\col{curr\_NUMBER\_lo}} +\def\prevNumberHi {\col{prev\_NUMBER\_hi}} +\def\prevNumberLo {\col{prev\_NUMBER\_lo}} + +\def\currTimeStampHi {\col{curr\_TIMESTAMP\_hi}} +\def\currTimeStampLo {\col{curr\_TIMESTAMP\_lo}} +\def\prevTimeStampHi {\col{prev\_TIMESTAMP\_hi}} +\def\prevTimeStampLo {\col{prev\_TIMESTAMP\_lo}} + diff --git a/block_data/binarities.tex b/block_data/binarities.tex new file mode 100644 index 0000000..656bd46 --- /dev/null +++ b/block_data/binarities.tex @@ -0,0 +1,13 @@ +We impose \textbf{binary} constraints on the following columns: +\begin{multicols}{3} + \begin{enumerate} + \item $\iomf$ + \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..06862ea 100644 --- a/block_data/columns.tex +++ b/block_data/columns.tex @@ -1,17 +1,29 @@ 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 $\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 +33,22 @@ \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; +\end{enumerate} +The following columns are used in lookups from the \btcMod{} module into the \wcpMod{} and \eucMod{} modules. +\begin{enumerate}[resume] + \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..4d9498f --- /dev/null +++ b/block_data/computations/basefee.tex @@ -0,0 +1,44 @@ +\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} +We use the following shorthand +\[ + \left\{ \begin{array}{lc l} + \currBaseFeeHi & \define & \currDataHi \\ + \currBaseFeeLo & \define & \currDataLo \\ + \end{array} \right. +\] +We impose the following constraints +\begin{description} + \item[\underline{\underline{Horizontalization of \inst{BASEFEE}:}}] + we impose + \[ + \left\{ \begin{array}{lcl} + \currBaseFeeHi & = & 0 \\ + \currBaseFeeLo & = & \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 = \currBaseFeeHi , + argOneLo = \currBaseFeeLo , + 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..ef3c6b9 --- /dev/null +++ b/block_data/computations/chainid.tex @@ -0,0 +1,53 @@ +\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} +We use the following shorthand +\[ + \left\{ \begin{array}{lcl} + \currChainIdHi & \define & \currDataHi \\ + \currChainIdLo & \define & \currDataLo \\ + \end{array} \right. + \quad + \left\{ \begin{array}{lcl} + \prevChainIdHi & \define & \prevDataHi \\ + \prevChainIdLo & \define & \prevDataLo \\ + \end{array} \right. +\] +And we impose the following constraints +\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 $\locIsntFirstBlock = 1$ \Then + we impose + \[ + \left\{ \begin{array}{lcl} + \currChainIdHi & = & \prevChainIdHi \\ + \currChainIdLo & = & \prevChainIdLo \\ + \end{array} \right. + \] + \item[\underline{\underline{\inst{CHAINID} bound:}}] + \def\rowOffset{\yellowm{0}} + we impose + \[ + \wcpCallToGeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currChainIdHi , + argOneLo = \currChainIdLo , + 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..f8c162a --- /dev/null +++ b/block_data/computations/coinbase.tex @@ -0,0 +1,41 @@ +\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} +We use the following shorthand +\[ + \left\{ \begin{array}{lcl} + \currCoinbaseHi & \define & \currDataHi \\ + \currCoinbaseLo & \define & \currDataLo \\ + \end{array} \right. +\] +And we impose the following constraints +\begin{description} + \item[\underline{\underline{Horizontalization of \inst{COINBASE}:}}] + we impose + \[ + \left\{ \begin{array}{lcl} + \currCoinbaseHi & = & \coinbase\high _{i} \\ + \currCoinbaseLo & = & \coinbase\low _{i} \\ + \end{array} \right. + \] + \item[\underline{\underline{\inst{COINBASE} upper bound:}}] + \def\rowOffset{\yellowm{0}} + we impose + \[ + \wcpCallToLt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currCoinbaseHi , + argOneLo = \currCoinbaseLo , + 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..6b1c554 --- /dev/null +++ b/block_data/computations/difficulty.tex @@ -0,0 +1,39 @@ +\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} +We use the following shorthand +\[ + \left\{ \begin{array}{lcl} + \currDifficultyHi & \define & \currDataHi \\ + \currDifficultyLo & \define & \currDataLo \\ + \end{array} \right. +\] +And we impose the following constraints +\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 = \currDifficultyHi , + argOneLo = \currDifficultyLo , + 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..5184de3 --- /dev/null +++ b/block_data/computations/gaslimit.tex @@ -0,0 +1,126 @@ +\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 use the following shorthand +\[ + \left\{ \begin{array}{lcl} + \currGasLimitHi & \define & \currDataHi \\ + \currGasLimitLo & \define & \currDataLo \\ + \end{array} \right. + \quad + \left\{ \begin{array}{lcl} + \prevGasLimitHi & \define & \prevDataHi \\ + \prevGasLimitLo & \define & \prevDataLo \\ + \end{array} \right. +\] +We further introduce the following constants +\[ + \left\{ \begin{array}{lcr} + \ethereumMinBlockGasLimit & \define & \ethereumMinBlockGasLimitValue \\ + \lineaMinBlockGasLimit & \define & \lineaMinBlockGasLimitValue \\ + \lineaMaxBlockGasLimit & \define & \lineaMaxBlockGasLimitValue \\ + \ethereumGasLimitAdjustmentFactor & \define & \ethereumGasLimitAdjustmentFactorValue \\ + \end{array} \right. +\] +We impose the following: +\begin{description} + \item[\underline{\underline{Horizontalization of \inst{GASLIMIT}:}}] + we impose + \[ + \left\{ \begin{array}{lcl} + \currGasLimitHi & = & 0 \\ + \currGasLimitLo & = & \blockGasLimit _{i} \\ + \end{array} \right. + \] + \item[\underline{\underline{\inst{GASLIMIT} lower bound:}}] + \def\rowOffset{\yellowm{0}} + we impose + \[ + \wcpCallToGeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currGasLimitHi , + argOneLo = \currGasLimitLo , + argTwoHi = 0 , + argTwoLo = \lineaMinBlockGasLimit , + } + \] + + + \saNote{} + The above ensures that $\blockGasLimit_{i} \geq \lineaMinBlockGasLimit$. + This minimal block gas limits differs from \textsc{Ethereum}'s minimal block gas limit, \ethereumMinBlockGasLimit. + Implementations may use an arbitrary block gas limit, though preferably $\geq \ethereumMinBlockGasLimit$. + \item[\underline{\underline{\inst{GASLIMIT} upper bound:}}] + \def\rowOffset{\yellowm{1}} + we impose + \[ + \wcpCallToLeq{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currGasLimitHi , + argOneLo = \currGasLimitLo , + argTwoHi = 0 , + argTwoLo = \lineaMaxBlockGasLimit , + } + \] + \saNote{} + The above ensures that $\blockGasLimit_{i} \leq \lineaMaxBlockGasLimit$. + There is no corresponding upper limit on the block gas limit in \textsc{Ethereum}. + \item[\underline{\underline{Maximum deviation:}}] + \def\rowOffset{\yellowm{2}} + \If $\locIsntFirstBlock = 1$ \Then + we impose + \[ + \eucCall{ + anchorRow = i , + relOffset = \rowOffset , + argOne = \previousGasLimit , + argTwo = \ethereumGasLimitAdjustmentFactor , + } + \] + 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{\ethereumGasLimitAdjustmentFactorValue} \right\rfloor$. + \item[\underline{\underline{\inst{GASLIMIT} deviation upper bound:}}] + \def\rowOffset{\yellowm{3}} + \If $\locIsntFirstBlock = 1$ \Then + \[ + \wcpCallToLt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currGasLimitHi , + argOneLo = \currGasLimitLo , + 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 $\locIsntFirstBlock = 1$ \Then + \[ + \wcpCallToGt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currGasLimitHi , + argOneLo = \currGasLimitLo , + 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..e748e91 --- /dev/null +++ b/block_data/computations/number.tex @@ -0,0 +1,80 @@ +\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} +We use the following shorthand +\[ + \left\{ \begin{array}{lc l} + \currNumberHi & \define & \currDataHi \\ + \currNumberLo & \define & \currDataLo \\ + \end{array} \right. + \quad + \left\{ \begin{array}{lcl} + \prevNumberHi & \define & \prevDataHi \\ + \prevNumberLo & \define & \prevDataLo \\ + \end{array} \right. +\] +We impose the following constraints +\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 $\locIsFirstBlock = 1$ \Then + we impose that + \[ + \wcpCallToLt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currNumberHi , + argOneLo = \currNumberLo , + 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 $\locIsFirstBlock = 1$ \Then + \begin{enumerate} + \item + we unconditionally impose that + \[ + \left\{ \begin{array}{lcl} + \currNumberHi & = & 0 \\ + \currNumberLo & = & \blockNumberOfFirstBlockInConflation _{i} \\ + \end{array} \right. + \] + \end{enumerate} + \item + \If $\locIsntFirstBlock = 1$ \Then + we impose that + \[ + \left\{ \begin{array}{lcl} + \currNumberHi & = & \prevNumberHi \\ + \currNumberLo & = & \prevNumberLo + 1 \\ + \end{array} \right. + \] + \end{enumerate} +\end{description} diff --git a/block_data/computations/timestamp.tex b/block_data/computations/timestamp.tex new file mode 100644 index 0000000..3496ffd --- /dev/null +++ b/block_data/computations/timestamp.tex @@ -0,0 +1,56 @@ +\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} +We use the following shorthand +\[ + \left\{ \begin{array}{lcl} + \currTimeStampHi & \define & \currDataHi \\ + \currTimeStampLo & \define & \currDataLo \\ + \end{array} \right. + \quad + \left\{ \begin{array}{lcl} + \prevTimeStampHi & \define & \prevDataHi \\ + \prevTimeStampLo & \define & \prevDataLo \\ + \end{array} \right. +\] +And we impose the following constraints +\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 = \currTimeStampHi , + argOneLo = \currTimeStampLo , + 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 $\locIsntFirstBlock = 1$ \Then + we impose that + \[ + \wcpCallToGt{ + anchorRow = i , + relOffset = \rowOffset , + argOneHi = \currTimeStampHi , + argOneLo = \currTimeStampLo , + argTwoHi = \prevTimeStampHi , + argTwoLo = \prevTimeStampLo , + } + \] + \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..a850917 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$ \Then $\blockNumberOfFirstBlockInConflation _{i + 1} = \blockNumberOfFirstBlockInConflation_{i}$ +\end{enumerate} diff --git a/block_data/heartbeat.tex b/block_data/heartbeat.tex index 17eeb83..b94b939 100644 --- a/block_data/heartbeat.tex +++ b/block_data/heartbeat.tex @@ -1,25 +1,55 @@ -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$ + \item \If $\iomf _{i} = 1$ \Then $\iomf _{i + 1} = 1$ +\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} \neq \iomf _{i + 1}$\footnote{i.e. \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} + (1 - \locIsCoinbase _{i}) \cdot \locIsCoinbase _{i + 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 $\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..8b42f5b 100644 --- a/block_data/lookups/_inputs.tex +++ b/block_data/lookups/_inputs.tex @@ -1,2 +1,4 @@ -\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} +\subsection{Prover data extraction} \label{block data: lookups: prover data extraction} \input{lookups/prover_data_extraction} 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..b53fdad --- /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/lookups/prover_data_extraction.tex b/block_data/lookups/prover_data_extraction.tex new file mode 100644 index 0000000..3c4d40d --- /dev/null +++ b/block_data/lookups/prover_data_extraction.tex @@ -0,0 +1,28 @@ +The present section describes the extractor and columns from which the prover extracts data. +The prover connects said data to public inputs provided in the blockheader. +\begin{description} + \item[\underline{Extractor:}] we use + \[ + \locExtractor _{i} \define + \left[ \begin{array}{clcl} + + & (1 - \locIsCoinbase _{i - 1}) & \cdot & \locIsCoinbase _{i} \\ + + & (1 - \locIsTimestamp _{i - 1}) & \cdot & \locIsTimestamp _{i} \\ + + & (1 - \locIsNumber _{i - 1}) & \cdot & \locIsNumber _{i} \\ + + & (1 - \locIsDifficulty _{i - 1}) & \cdot & \locIsDifficulty _{i} \\ + + & (1 - \locIsGaslimit _{i - 1}) & \cdot & \locIsGaslimit _{i} \\ + + & (1 - \locIsChainid _{i - 1}) & \cdot & \locIsChainid _{i} \\ + + & (1 - \locIsBasefee _{i - 1}) & \cdot & \locIsBasefee _{i} \\ + \end{array} \right] + \] + \item[\underline{Source columns:}] --- + \begin{multicols}{3} + \begin{enumerate} + \item $\blockNumberOfFirstBlockInConflation _{i}$ + \item $\relBlock _{i}$ + \item $\exoInstruction _{i}$ + \item [\vspace{\fill}] + \item $\blockDataHi _{i}$ + \item $\blockDataLo _{i}$ + \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..af481ae --- /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 | RELBLOCK | +|:----:+:-----:+:-----:+:-----:+:-----:+:-----:+:-----:+:-----:+:------:+:--:+-----------:+:--------:| +| ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | | +| | | | | | | | | | | | | +| 0 | | | | | | | 0 | | | | 0 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | 1 | | | | | | | 0 | 0 | COINBASE | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | 1 | | | | | | 1 | 0 | TIMESTAMP | 1 | +| 1 | | 1 | | | | | | 1 | 1 | TIMESTAMP | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | 1 | | | | | 1 | 0 | NUMBER | 1 | +| 1 | | | 1 | | | | | 1 | 1 | NUMBER | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | 1 | | | | 0 | 0 | DIFFICULTY | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | 1 | | | 4 | 0 | GASLIMIT | 1 | +| 1 | | | | | 1 | | | 4 | 1 | GASLIMIT | 1 | +| 1 | | | | | 1 | | | 4 | 2 | GASLIMIT | 1 | +| 1 | | | | | 1 | | | 4 | 3 | GASLIMIT | 1 | +| 1 | | | | | 1 | | | 4 | 4 | GASLIMIT | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | | 1 | | 0 | 0 | CHAINID | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | | | 1 | 0 | 0 | BASEFEE | 1 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | 1 | | | | | | | 0 | 0 | COINBASE | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | 1 | | | | | | 1 | 0 | TIMESTAMP | 2 | +| 1 | | 1 | | | | | | 1 | 1 | TIMESTAMP | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | 1 | | | | | 1 | 0 | NUMBER | 2 | +| 1 | | | 1 | | | | | 1 | 1 | NUMBER | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | 1 | | | | 0 | 0 | DIFFICULTY | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | 1 | | | 4 | 0 | GASLIMIT | 2 | +| 1 | | | | | 1 | | | 4 | 1 | GASLIMIT | 2 | +| 1 | | | | | 1 | | | 4 | 2 | GASLIMIT | 2 | +| 1 | | | | | 1 | | | 4 | 3 | GASLIMIT | 2 | +| 1 | | | | | 1 | | | 4 | 4 | GASLIMIT | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | | 1 | | 0 | 0 | CHAINID | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | | | 1 | 0 | 0 | BASEFEE | 2 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | 1 | | | | | | | 0 | 0 | COINBASE | 3 | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | 1 | | | | | | 1 | 0 | TIMESTAMP | 3 | +| 1 | | 1 | | | | | | 1 | 1 | TIMESTAMP | 2 | +| | | | | | | | | | | | | +| ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | ⋮ | +| | | | | | | | | | | | | +| 1 | | | | | 1 | | | 4 | 2 | GASLIMIT | b | +| 1 | | | | | 1 | | | 4 | 3 | GASLIMIT | b | +| 1 | | | | | 1 | | | 4 | 4 | GASLIMIT | b | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | | 1 | | 0 | 0 | CHAINID | b | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| +| 1 | | | | | | | 1 | 0 | 0 | BASEFEE | b | +|------+-------+-------+-------+-------+-------+-------+-------+--------+----+------------+----------| + + +NOTE. As per usual in such diagrams, 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/notes.md b/block_data/notes.md new file mode 100644 index 0000000..88a556f --- /dev/null +++ b/block_data/notes.md @@ -0,0 +1,42 @@ +Data that will emanate from the BLOCKDATA module +- TIMESTAMP +- COINBASE +- CHAINID +- NUMBER +- DIFFICULTY +- GASLIMIT +- BASEFEE + +| IOMF | REL_BLOCK_NUMBER | INST | DATA_HI | DATA_LO | +|------+------------------+-----------+---------+-------------------| +| 0 | 0 | 0 | 0 | 0 | +|------+------------------+-----------+---------+-------------------| +| 1 | 1 | TIMESTAMP | 0 | | +| 1 | 1 | COINBASE | 4B | 16 B | +| 1 | 1 | CHAINID | 0 | | +| 1 | 1 | NUMBER | | | +| 1 | 1 | DIFFICUL | | | +| 1 | 1 | GASLIMIT | | | +| 1 | 1 | BASEFEE | | | +|------+------------------+-----------+---------+-------------------| +| 1 | 2 | TIMESTAMP | 0 | | +| 1 | 2 | COINBASE | 4B | 16 B | +| 1 | 2 | CHAINID | | | +| 1 | 2 | NUMBER | | | +| 1 | 2 | DIFFICUL | | | +| 1 | 2 | GASLIMIT | | | +| 1 | 2 | BASEFEE | | | +|------+------------------+-----------+---------+-------------------| +| 1 | 3 | TIMESTAMP | 0 | | +| 1 | 3 | COINBASE | 4B | 16 B | +| 1 | 3 | CHAINID | | | +| 1 | 3 | NUMBER | | | +| 1 | 3 | DIFFICUL | | | +| 1 | 3 | GASLIMIT | | | +| 1 | 3 | BASEFEE | | | + +We keep +- FIRST_ABSOLUTE_BLOCK_NUMBER +- RELATIVE_BLOCK_NUMBER +- selector ≡ Σ_b (1 - b[-1]) * b selects for the first occurrence of some value +- CT columns disappears 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..a768727 --- /dev/null +++ b/block_data/shorthands.tex @@ -0,0 +1,127 @@ +We shall often use the following shorthands for +\[ + \left\{ \begin{array}{lcl} + \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] +\] +We also introduce the following shorthands for improved expressivity +\[ + \left\{ \begin{array}{lc l} + \locIsFirstBlock & \define & 1 - \iomf _{i - \blockDataDepth} \\ + \locIsntFirstBlock & \define & \iomf _{i - \blockDataDepth} \\ + \currDataHi & \define & \blockDataHi _{i} \\ + \currDataLo & \define & \blockDataLo _{i} \\ + \prevDataHi & \define & \blockDataHi _{i - \blockDataDepth} \\ + \prevDataLo & \define & \blockDataLo _{i - \blockDataDepth} \\ + \end{array} \right. +\] +The interpretation being that $\locIsntFirstBlock \equiv 1$ \emph{if and only if} the current block isn't the first in the conflation of blocks. diff --git a/block_data/unconditional.tex b/block_data/unconditional.tex new file mode 100644 index 0000000..b79949b --- /dev/null +++ b/block_data/unconditional.tex @@ -0,0 +1,15 @@ +We unconditionally impose that +\[ + \left\{ \begin{array}{lcl} + \iomf _{i} & = & \locFlagSum _{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