diff --git a/block_hash/_all_block_hash.tex b/block_hash/_all_block_hash.tex index 2006696..b364d6c 100644 --- a/block_hash/_all_block_hash.tex +++ b/block_hash/_all_block_hash.tex @@ -1,13 +1,14 @@ -\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} \usepackage{../pkg/bin} \usepackage{../pkg/wc3} \usepackage{../pkg/ram} +\usepackage{../pkg/mmu} \usepackage{../pkg/alu} \usepackage{../pkg/env} \usepackage{../pkg/warm} @@ -25,6 +26,7 @@ \usepackage{../pkg/block_hash} \usepackage{../pkg/iomf_done} \usepackage{../pkg/offset_processor} +\usepackage{../pkg/xkeyval_macros/wcp_calls} \usepackage{../pkg/draculatheme} diff --git a/block_hash/_inputs.tex b/block_hash/_inputs.tex index 946575d..e07d49c 100644 --- a/block_hash/_inputs.tex +++ b/block_hash/_inputs.tex @@ -1,10 +1,9 @@ +\input{_local} \section{\blockHashMod{} module} -\subsection{Introduction} \label{block hash: intro} \input{intro} -\subsection{Columns} \label{block hash: columns} \input{columns} +\subsection{Introduction} \label{block hash: intro} \input{intro} +\subsection{Columns} \label{block hash: columns} \input{columns} -\section{Constraints} -\subsection{Heartbeat} \label{block hash: heartbeat} \input{heartbeat} -\subsection{Byte Decomposition} \label{block hash: byte decomposition} \input{byte_decomposition} -\subsection{Consistency constraint} \label{block hash: consistency} \input{consistency} - -\section{Lookups} \label{block hash lookups} \input{lookups/_inputs} +\section{Generalities} \label{block hash: generalities} \input{generalities/_inputs} +\section{Processing} \label{block hash: processing} \input{processing/_inputs} +\section{Consistency constraints} \label{block hash: consistency} \input{consistency} +\section{Lookups} \label{block hash lookups} \input{lookups/_inputs} diff --git a/block_hash/_local.tex b/block_hash/_local.tex new file mode 100644 index 0000000..050a1d8 --- /dev/null +++ b/block_hash/_local.tex @@ -0,0 +1,26 @@ +\def\nRowsMacro {\texttt{nrows\_macro}} +\def\nRowsPreprocessing {\texttt{nrows\_prprc}} +\def\blockhashDepth {\texttt{depth}} +\def\nRowsMacroValue {\yellowm{1}} +\def\nRowsPreprocessingValue {\yellowm{5}} +\def\blockhashDepthValue {\yellowm{6}} +\def\locFlagSum {\col{flag\_sum}} +\def\locMaxCtSum {\col{ct\_max\_sum}} +\def\locFlagSum {\col{flag\_sum}} +\def\locWeightedSum {\col{wght\_sum}} +\def\locTransitionBit {\col{transition\_bit}} +\def\exoInstruction {\col{EXO\_}\instruction} + +\def\locNotFirst {\col{not\_first}} +\def\locBlockHashArg {\col{BH\_arg}} +\def\locSameBlockHashArgument {\col{same\_}\locBlockHashArg} +\def\locCurrBlockHashArg {\col{curr\_}\locBlockHashArg} +\def\locPrevBlockHashArg {\col{prev\_}\locBlockHashArg} +\def\locCurrBlockHashArgHi {\locCurrBlockHashArg\col{\_hi}} +\def\locCurrBlockHashArgLo {\locCurrBlockHashArg\col{\_lo}} +\def\locPrevBlockHashArgHi {\locPrevBlockHashArg\col{\_hi}} +\def\locPrevBlockHashArgLo {\locPrevBlockHashArg\col{\_lo}} +\def\locMinimalReachable {\col{minimal\_reachable}} +\def\locUpperBoundOk {\col{upper\_bound\_ok}} +\def\locLowerBoundOk {\col{lower\_bound\_ok}} +\def\locArgumentInBounds {\col{arg\_in\_bounds}} diff --git a/block_hash/byte_decomposition.tex b/block_hash/byte_decomposition.tex deleted file mode 100644 index d24b4ef..0000000 --- a/block_hash/byte_decomposition.tex +++ /dev/null @@ -1,21 +0,0 @@ -We impose bytehood constraints on the following columns -\begin{multicols}{2} -\begin{enumerate} - \item $\byteCol{HI\_k}$, $k = 0, 1, \dots, \llargeMO$ - \item $\byteCol{LO\_k}$, $k = 0, 1, \dots, \llargeMO$ -% \item $\byteCol{$\Delta$}$ -\end{enumerate} -\end{multicols} -\noindent We impose horizontal byte decomposition constraints: -\[ -\left\{ -\begin{array}{lcl} - \blockHash\high_{i} - & \!\!\! = \!\!\! & - \displaystyle \sum_{k = 0}^{\llargeMO} 256^{\llargeMO - k} \cdot \byteCol{HI\_k}_{i} \\ - \blockHash\low_{i} - & \!\!\! = \!\!\! & - \displaystyle \sum_{k = 0}^{\llargeMO} 256^{\llargeMO - k} \cdot \byteCol{LO\_k}_{i} \\ -\end{array} -\right. -\] diff --git a/block_hash/columns.tex b/block_hash/columns.tex index 92335cd..ff20831 100644 --- a/block_hash/columns.tex +++ b/block_hash/columns.tex @@ -1,24 +1,45 @@ +The following set of columns are used to define the heartbeat of the present module. \begin{enumerate} - \item \iomf: - monotonous bit column that lights up for non-padding rows; - \item $\blockNumber\high$ and $\blockNumber\low$: - high and low parts of \inst{BLOCKHASH} opcode argument; - \item $\resHi$ and $\resLo$: - high and low parts of \inst{BLOCKHASH} opcode result; + \item $\iomf$: + binary column indicating non padding rows; + \item $\isMacro$: + binary column indicating a request to the \blockHashMod{} module; + \item $\isPreprocessing$: + binary column indicating processing rows of the \blockHashMod{} module; + \item \ct: + counter column; + \item \ctMax: + maximum counter value; +\end{enumerate} +\saNote{} +There is no real purpose to the $\iomf$ column. +We do it so as to remain in line with other, similar, modules. + +\noindent The following columns pertain to the ``macro-instruction'' data: +\begin{enumerate}[resume] \item \relBlock{}: relative block number in a given conflation, starts at $1$; \item \absBlock{}: absolute block number; - \item \lowerBoundCheck{}: - bit column that lights up if \blockNumber{} is big enough; - \item \upperBoundCheck{}: - bit column that lights up if \blockNumber{} is small enough; - \item \inRange{}: - bit column that lights up if the input is in the range - $[\![ \, \inst{NUMBER} - \blockHashInstMaxHistory, \inst{NUMBER} - 1 \, ]\!]$ - %\item \blockShift{}: - %is between $1$ and $256$ for well-formed argument of the $\inst{BLOCKHASH}$ opcode; - \item $\blockHash\high$ and $\blockHash\low$: - high and low part of the block hash of the block; - \item $\byteCol{HI\_k}$, and $\byteCol{LO\_k}$, $k = 0, 1, \dots, \llargeMO$: + \item $\blockHashValue\high$ and $\blockHashValue\low$: + high and low part of the block hash of some block; + \item $\blockHashArgument\high$ and $\blockHashArgument\low$: + high and low parts of \inst{BLOCKHASH} opcode argument; + \item $\blockHashResult\high$ and $\blockHashResult\low$: + high and low parts of \inst{BLOCKHASH} opcode result; +\end{enumerate} +\saNote{} +The interpretation of $\blockHashArgument\high$ and $\blockHashArgument\low$ is that they represent +(the high and low parts of) $\bm{\mu}_\textbf{s}\big[0\big]$ +while $\blockHashResult\high$ and $\blockHashResult\low$ ought to represent +(the high and low parts of) $\bm{\mu}_\textbf{s}'\big[0\big]$. + +\noindent The following columns pertain to the ``instruction-processing'' data: +\begin{enumerate}[resume] + \item $\instruction$: + exogenous instruction column; + \item $\argOneHi$, $\argOneLo$, $\argTwoHi$, $\argTwoLo$: + exogenous argument columns; + \item $\res$: + exogenous result column; \end{enumerate} diff --git a/block_hash/consistency.tex b/block_hash/consistency.tex index 7ff0fac..3f43634 100644 --- a/block_hash/consistency.tex +++ b/block_hash/consistency.tex @@ -1,11 +1,10 @@ We impose that: \begin{enumerate} - \item $\inRange_{i} = \lowerBoundCheck_{i} \cdot \upperBoundCheck_{i}$ - \item $\resHi_{i} = \inRange_{i} \cdot \blockHash\high_{i}$ - \item $\resLo_{i} = \inRange_{i} \cdot \blockHash\low_{i}$ - \item \If $\blockNumber\low_{i} = \blockNumber\low_{i-1}$ \Then: - \begin{enumerate} - \item $\blockHash\high_{i} = \blockHash\high_{i-1}$ - \item $\blockHash\low _{i} = \blockHash\low _{i-1}$ - \end{enumerate} + \item \If $\isMacro _{i} = 1$ \et $\locNotFirst = 1$ \et $\locSameBlockHashArgument$ \Then + \[ + \left\{ \begin{array}{lcl} + \blockHashValue \high _{i} & = & \blockHashValue \high _{i - \blockhashDepthValue} \\ + \blockHashValue \low _{i} & = & \blockHashValue \low _{i - \blockhashDepthValue} \\ + \end{array} \right. + \] \end{enumerate} diff --git a/block_hash/generalities/_inputs.tex b/block_hash/generalities/_inputs.tex new file mode 100644 index 0000000..3a8dc8c --- /dev/null +++ b/block_hash/generalities/_inputs.tex @@ -0,0 +1,4 @@ +\subsection{Shorthands} \label{block hash: generalities: shorthands} \input{generalities/shorthands} +\subsection{Binary constraints} \label{block hash: generalities: binary constraints} \input{generalities/binarities} +\subsection{Constancy constraints} \label{block hash: generalities: constancy constraints} \input{generalities/constancies} +\subsection{Heartbeat} \label{block hash: generalities: heartbeat} \input{generalities/heartbeat} diff --git a/block_hash/generalities/binarities.tex b/block_hash/generalities/binarities.tex new file mode 100644 index 0000000..ed98748 --- /dev/null +++ b/block_hash/generalities/binarities.tex @@ -0,0 +1,8 @@ +We impose binary constraints on the following columns (and shorthands): +\begin{multicols}{3} + \begin{enumerate} + \item $\isMacro$ + \item $\isPreprocessing$ + \item $\iomf$ + \end{enumerate} +\end{multicols} diff --git a/block_hash/generalities/constancies.tex b/block_hash/generalities/constancies.tex new file mode 100644 index 0000000..52b5912 --- /dev/null +++ b/block_hash/generalities/constancies.tex @@ -0,0 +1,8 @@ +As per usual, we define 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 counter-constancy on +\begin{enumerate} + \item \locWeightedSum +\end{enumerate} diff --git a/block_hash/generalities/heartbeat.tex b/block_hash/generalities/heartbeat.tex new file mode 100644 index 0000000..4d1e91f --- /dev/null +++ b/block_hash/generalities/heartbeat.tex @@ -0,0 +1,47 @@ +The heartbeat is standard and simple. We start with constraints pertaining to $\iomf$: +\begin{enumerate} + \item we unconditionally impose $\iomf _{i} = \locFlagSum _{i}$ + \item $\iomf_{0} = 0$ + \item \If $\iomf_{i} = 0$ \Then: + \begin{enumerate} + \item $\ct _{i } = 0$ + \item $\ct _{i + 1} = 0$ + \item \label{block hash: non padding starts on macro instruction} $\isPreprocessing _{i + 1} = 0$ + \end{enumerate} + one may further impose + \begin{multicols}{2} + \begin{enumerate} + \item $\blockHashArgument \high _{i} = 0$ ~ (\trash) + \item $\blockHashValue \high _{i} = 0$ ~ (\trash) + \item $\blockHashResult \high _{i} = 0$ ~ (\trash) + \item $\blockHashArgument \low _{i} = 0$ ~ (\trash) + \item $\blockHashValue \low _{i} = 0$ ~ (\trash) + \item $\blockHashResult \low _{i} = 0$ ~ (\trash) + \end{enumerate} + \end{multicols} + \item \If $\iomf_{i} = 1$ \Then $\iomf _{i + 1} = 1$ +\end{enumerate} +\saNote{} +Constraint~(\ref{block hash: non padding starts on macro instruction}) enforces that the first time +the \iomf{} flag turns on, so does $\isMacro$. + +\noindent We now deal with the counter columns: +\begin{enumerate}[resume] + \item we unconditionally impose $\maxCt _{i} = \locMaxCtSum _{i}$ + \item \If $\iomf _{i} \neq 0$ \Then + \begin{enumerate} + \item \If $\ct _{i} \neq \maxCt _{i}$ \Then $\ct _{i + 1} = 1 + \ct _{i}$ + \item \If $\ct _{i} = \maxCt _{i}$ \Then $\locTransitionBit _{i} = 1$ + \end{enumerate} + \item \If $\locTransitionBit _{i} = 1$ \Then $\ct _{i + 1} = 0$ +\end{enumerate} +We further impose finalization constraints +\begin{enumerate}[resume] + \item \If $\iomf _{N} = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \isPreprocessing _{N} & = & 1 \\ + \ct _{N} & = & \maxCt _{N} \\ + \end{array} \right. + \] +\end{enumerate} diff --git a/block_hash/generalities/shorthands.tex b/block_hash/generalities/shorthands.tex new file mode 100644 index 0000000..77f43c6 --- /dev/null +++ b/block_hash/generalities/shorthands.tex @@ -0,0 +1,36 @@ +We further define the following shorthands +\[ + \left\{ \begin{array}{lcl} + \locFlagSum _{i} & \define & + \left[ \begin{array}{cl} + + & \isMacro _{i} \\ + + & \isPreprocessing _{i} \\ + \end{array} \right] \vspace{2mm} \\ + \locWeightedSum _{i} & \define & + \left[ \begin{array}{rcl} + + \; 1 & \!\!\!\cdot\!\!\! & \isMacro _{i} \\ + + \; 2 & \!\!\!\cdot\!\!\! & \isPreprocessing _{i} \\ + \end{array} \right] \vspace{2mm} \\ + \locTransitionBit _{i} & \define & + \left[ \begin{array}{clcl} + + & (1 - \isMacro _{i}) & \!\!\!\cdot\!\!\! & \isMacro _{i + 1} \\ + + & (1 - \isPreprocessing _{i}) & \!\!\!\cdot\!\!\! & \isPreprocessing _{i + 1} \\ + \end{array} \right] + \end{array} \right. +\] +and +\[ + \locMaxCtSum _{i} \define + \left[ \begin{array}{crcl} + + & (\nRowsMacro - 1) & \cdot & \isMacro _{i} \\ + + & (\nRowsPreprocessing - 1) & \cdot & \isPreprocessing _{i} \\ + \end{array} \right] \\ +\] +where we set +\[ + \left\{ \begin{array}{lcl} + \nRowsMacro & \define & \nRowsMacroValue \\ + \nRowsPreprocessing & \define & \nRowsPreprocessingValue \\ + \blockhashDepth & \define & \blockhashDepthValue \\ + \end{array} \right. +\] diff --git a/block_hash/heartbeat.tex b/block_hash/heartbeat.tex deleted file mode 100644 index d221fd9..0000000 --- a/block_hash/heartbeat.tex +++ /dev/null @@ -1,15 +0,0 @@ -The heartbeat is very simple: -\begin{enumerate} - \item $\iomf_{0} = 0$ - \item \If $\iomf_{i} = 0$ \Then: - \begin{enumerate} - \item $\inRange _{i} = 0$ - \item $\blockNumber\high_{i}=0$ - \item $\blockNumber\low_{i}=0$ - \end{enumerate} - \item \If $\iomf_{i} \neq 0$ \Then: - \begin{enumerate} - \item $\iomf _{i} = 1$ - \item $\iomf_{i+1} = \iomf_{i}$ - \end{enumerate} -\end{enumerate} diff --git a/block_hash/lookups/_inputs.tex b/block_hash/lookups/_inputs.tex index 93f1e64..23b2f9d 100644 --- a/block_hash/lookups/_inputs.tex +++ b/block_hash/lookups/_inputs.tex @@ -1,4 +1,2 @@ -\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{} module: lower bound of $\blockNumber$} \label{block hash: lookups: wcp: lower bound} \input{lookups/into_wcp_lower_bound} -\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{} module: upper bound of $\blockNumber$} \label{block hash: lookups: wcp: upper bound} \input{lookups/into_wcp_upper_bound} -\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{} module: lexicographic ordering of $\blockNumber$} \label{block hash: lookups: wcp: lexicographic ordering} \input{lookups/into_wcp_lex_ordering} -\subsection{\blockHashMod{} $\hookrightarrow$ \btcMod{} module: $\blockNumber$ extraction} \label{block hash: lookups: block data: (block)number extraction} \input{lookups/into_block_data} +\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{}} \label{block hash: lookups: wcp: lower bound} \input{lookups/into_wcp} +\subsection{\blockHashMod{} $\hookrightarrow$ \btcMod{}} \label{block hash: lookups: block data: (block)number extraction} \input{lookups/into_block_data} diff --git a/block_hash/lookups/into_block_data.tex b/block_hash/lookups/into_block_data.tex index c1e00bb..682be81 100644 --- a/block_hash/lookups/into_block_data.tex +++ b/block_hash/lookups/into_block_data.tex @@ -1,13 +1,13 @@ The purpose of the present lookup argument is to extract the true \inst{NUMBER} as defined by the \btcMod{} module. The lookup is structured as follows: \begin{description} - \item[\underline{Selector:}] non required: + \item[\underline{Selector:}] we use the $\isMacro$ column; \item[\underline{Source columns:}] --- \begin{multicols}{3} \begin{enumerate} - \item \relBlock{}: - \item \absBlock{}: - \item $\iomf \cdot \inst{NUMBER}$ + \item \relBlock{} + \item \absBlock{} + \item \inst{NUMBER} \end{enumerate} \end{multicols} \item[\underline{Target columns:}] --- diff --git a/block_hash/lookups/into_wcp_upper_bound.tex b/block_hash/lookups/into_wcp.tex similarity index 65% rename from block_hash/lookups/into_wcp_upper_bound.tex rename to block_hash/lookups/into_wcp.tex index c949ba8..7036b9f 100644 --- a/block_hash/lookups/into_wcp_upper_bound.tex +++ b/block_hash/lookups/into_wcp.tex @@ -1,16 +1,16 @@ -The purpose of the present lookup argument is to delegate the proof of the lower bond of \blockNumber{} to the \wcpMod{} module. +The purpose of the present lookup argument is to delegate the proof of the lower bond of \blockHashArgument{} to the \wcpMod{} module. The lookup is structured as follows: \begin{description} - \item[\underline{Selector:}] $\iomf$: + \item[\underline{Selector:}] $\isPreprocessing$: \item[\underline{Source columns:}] --- \begin{multicols}{3} \begin{enumerate} - \item $\blockNumber\high_{i}$ - \item $\blockNumber\low_{i}$ - \item $0$ - \item $\absBlock_{i}$ - \item $\upperBoundCheck_{i}$ - \item $\inst{LT}$ + \item $\argOneHi$ + \item $\argOneLo$ + \item $\argTwoHi$ + \item $\argTwoLo$ + \item $\res$ + \item $\instruction$ \end{enumerate} \end{multicols} \item[\underline{Target columns:}] --- diff --git a/block_hash/lookups/into_wcp_lex_ordering.tex b/block_hash/lookups/into_wcp_lex_ordering.tex deleted file mode 100644 index fc4ef7c..0000000 --- a/block_hash/lookups/into_wcp_lex_ordering.tex +++ /dev/null @@ -1,27 +0,0 @@ -The purpose of the present lookup argument is to delegate the proof of lexicographic ordering of $\blockNumber\low$ to the \wcpMod{} module. -The lookup is structured as follows: -\begin{description} - \item[\underline{Selector:}] $\iomf$: - \item[\underline{Source columns:}] --- - \begin{multicols}{3} - \begin{enumerate} - \item $\blockNumber\high_{i}$ - \item $\blockNumber\low_{i}$ - \item $\blockNumber\high_{i-1}$ - \item $\blockNumber\low_{i-1}$ - \item $1$ - \item $\inst{GEQ}$ - \end{enumerate} - \end{multicols} - \item[\underline{Target columns:}] --- - \begin{multicols}{3} - \begin{enumerate} - \item $\argOneHi$ - \item $\argOneLo$ - \item $\argTwoHi$ - \item $\argTwoLo$ - \item $\resLo$ - \item $\INST$ - \end{enumerate} - \end{multicols} -\end{description} diff --git a/block_hash/lookups/into_wcp_lower_bound.tex b/block_hash/lookups/into_wcp_lower_bound.tex deleted file mode 100644 index 6fb22d4..0000000 --- a/block_hash/lookups/into_wcp_lower_bound.tex +++ /dev/null @@ -1,27 +0,0 @@ -The purpose of the present lookup argument is to delegate the proof of the lower bond of \blockNumber{} to the \wcpMod{} module. -The lookup is structured as follows: -\begin{description} - \item[\underline{Selector:}] $\iomf$: - \item[\underline{Source columns:}] --- - \begin{multicols}{3} - \begin{enumerate} - \item $\blockNumber\high_{i}$ - \item $\blockNumber\low_{i}$ - \item $0$ - \item $\absBlock_{i}-\blockHashInstMaxHistory$ - \item $\lowerBoundCheck_{i}$ - \item $\inst{GEQ}$ - \end{enumerate} - \end{multicols} - \item[\underline{Target columns:}] --- - \begin{multicols}{3} - \begin{enumerate} - \item $\argOneHi$ - \item $\argOneLo$ - \item $\argTwoHi$ - \item $\argTwoLo$ - \item $\resLo$ - \item $\INST$ - \end{enumerate} - \end{multicols} -\end{description} diff --git a/block_hash/lua/representation.lua.tex b/block_hash/lua/representation.lua.tex new file mode 100644 index 0000000..31c3246 --- /dev/null +++ b/block_hash/lua/representation.lua.tex @@ -0,0 +1,35 @@ +% !TeX TS-program = lualatex +\documentclass[varwidth=\maxdimen,margin=0.5cm,multi={verbatim}]{standalone} + +\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} + +|-------+-------+----+--------+-----+-----+-----------+-----------+-----------+-----------+-------------+-----------------+------+----------+----------+------| +| MACRO | MICRO | CT | CT_MAX | ABS | REL | BH_ARG_HI | BH_ARG_LO | BH_RES_HI | BH_RES_LO | ARG_1_HI | ARG_1_LO | INST | ARG_2_HI | ARG_2_LO | RES | +|:-----:+:-----:+:--:+:------:+:---:+:---:+:---------:+:---------:+:---------:+:---------:+:-----------:+:---------------:+:----:+:--------:+:--------:+:----:| +| 1 | | 0 | 0 | abs | rel | n_hi | n_lo | r_hi | r_lo | | | | | | | +|-------+-------+----+--------+-----+-----+-----------+-----------+-----------+-----------+-------------+-----------------+------+----------+----------+------| +| | 1 | 0 | 4 | | | | | | | n_hi | n_lo | LEQ | n_hi | n_lo | true | +| | 1 | 1 | 4 | | | | | | | n_hi | n_lo | EQ | n_hi | n_lo | | +| | 1 | 2 | 4 | | | | | | | | 256 | LEQ | | abs | | +| | 1 | 3 | 4 | | | | | | | n_hi | n_lo | LEQ | | abs | | +| | 1 | 4 | 4 | | | | | | | | (abs - 256) ∨ 0 | LEQ | n_hi | n_lo | | +|-------+-------+----+--------+-----+-----+-----------+-----------+-----------+-----------+-------------+-----------------+------+----------+----------+------| + +NOTE. In the above we have abbreviated BLOCKHASH to BH. +\end{verbatim} +\end{document} diff --git a/block_hash/processing/_inputs.tex b/block_hash/processing/_inputs.tex new file mode 100644 index 0000000..e5b241b --- /dev/null +++ b/block_hash/processing/_inputs.tex @@ -0,0 +1,6 @@ +\subsection{Shorthands} \label{block hash: processing: shorthands} \input{processing/shorthands} +\subsection{Introduction} \label{block hash: processing: introduction} \input{processing/intro} +\subsection{Representation} \label{block hash: processing: representation} \input{processing/representation} +\subsection{Module calls} \label{block hash: processing: module calls} \input{processing/calls} +\subsection{Processing constraints} \label{block hash: processing: processing constraints} \input{processing/processing} +\subsection{Result constraints} \label{block hash: processing: result constraints} \input{processing/result} diff --git a/block_hash/processing/calls.tex b/block_hash/processing/calls.tex new file mode 100644 index 0000000..c13e63a --- /dev/null +++ b/block_hash/processing/calls.tex @@ -0,0 +1,64 @@ +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} + \instruction _{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} & = & \relevantValue \\ + \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} + \instruction _{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} & = & \relevantValue \\ + \end{array} \right. \vspace{2mm} \\ + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \wcpCallToEq { + 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} + \instruction _{i + \relof} & = & \inst{EQ} \\ + \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} & = & \relevantValue \\ + \end{array} \right. \vspace{2mm} \\ + \multicolumn{3}{l}{ + \resultMustBeTrue { + anchorRow = i , + relOffset = \relof , + } \define \res _{i + \relof} = \redm{1} + } \\ + \end{array} \right. +\] +\saNote{} +The result of all comparisons is required to be \texttt{true} except for \inst{ISZERO}. + diff --git a/block_hash/processing/intro.tex b/block_hash/processing/intro.tex new file mode 100644 index 0000000..745d313 --- /dev/null +++ b/block_hash/processing/intro.tex @@ -0,0 +1,16 @@ +The purpose of the processing phase is to carry out the following comparisons: +\begin{itemize} + \item $\locPrevBlockHashArg \leq \locCurrBlockHashArg$, expecting the result to be true + \item $\locPrevBlockHashArg = \locCurrBlockHashArg$ + \item $\redm{256} \leq \absBlock$ + \item $\locCurrBlockHashArg < \absBlock$ + \item $\locCurrBlockHashArg \geq \big[ \absBlock - \redm{256} \big]^+$ +\end{itemize} +Given the results of these comparisons the \blockHashMod{} module determines the value to write in the +$\blockHashResult\high$ and $\blockHashResult\low$ columns. + +\saNote{} +We remind the reader that we set, for integer $x$, +\[ + x^+ \define 0 \vee x\define \max \big\{ 0, x \big\} +\] diff --git a/block_hash/processing/processing.tex b/block_hash/processing/processing.tex new file mode 100644 index 0000000..92ceac3 --- /dev/null +++ b/block_hash/processing/processing.tex @@ -0,0 +1,97 @@ +\[ + \boxed{\text{All constraints in this subsection assume } \isMacro _{i} = 1 } +\] +To this end We impose the following constraints +\begin{description} + \def\nRows{\yellowm{1}}\item[\underline{Processing row $n^\circ(i + \nRows)$:}] + we impose that + \[ + \wcpCallToLeq { + anchorRow = i , + relOffset = \nRows , + argOneHi = \locPrevBlockHashArgHi , + argOneLo = \locPrevBlockHashArgLo , + argTwoHi = \locCurrBlockHashArgHi , + argTwoLo = \locCurrBlockHashArgLo , + } + \] + we further impose that + \[ + \resultMustBeTrue { + anchorRow = i , + relOffset = \nRows , + } + \] + \saNote{} + The above enforces that $\locPrevBlockHashArg \leq \locCurrBlockHashArg$. + This is a \textbf{crucial feature} of the present module. + It enforces that (unexcepional) invocations of the \inst{BLOCKHASH} opcode be listed in + \textbf{ascending order of their arguments}. + This order may clash with the temporal order of execution. + \def\nRows{\yellowm{2}}\item[\underline{Processing row $n^\circ(i + \nRows)$:}] + we impose that + \[ + \wcpCallToEq { + anchorRow = i , + relOffset = \nRows , + argOneHi = \locPrevBlockHashArgHi , + argOneLo = \locPrevBlockHashArgLo , + argTwoHi = \locCurrBlockHashArgHi , + argTwoLo = \locCurrBlockHashArgLo , + } + \] + and we define the following shorthand + \[ + \locSameBlockHashArgument \define \res _{i + \nRows} + \] + \def\nRows{\yellowm{3}}\item[\underline{Processing row $n^\circ(i + \nRows)$:}] + we impose that + \[ + \wcpCallToLeq { + anchorRow = i , + relOffset = \nRows , + argOneHi = 0 , + argOneLo = \redm{256} , + argTwoHi = 0 , + argTwoLo = \absBlock _{i} , + } + \] + and we define the following shorthand + \[ + \locMinimalReachable \define \res _{i + \nRows} \cdot \Big( \absBlock _{i} - \redm{256} \Big) + \] + \saNote{} + In other words $\locMinimalReachable \equiv \big[ \absBlock _{i} - \redm{256} \big]^+$ + \def\nRows{\yellowm{4}}\item[\underline{Processing row $n^\circ(i + \nRows)$:}] + we impose that + \[ + \wcpCallToLt { + anchorRow = i , + relOffset = \nRows , + argOneHi = \locCurrBlockHashArgHi , + argOneLo = \locCurrBlockHashArgLo , + argTwoHi = 0 , + argTwoLo = \absBlock _{i} , + } + \] + and we define the following shorthand + \[ + \locUpperBoundOk \define \res _{i + \nRows} + \] + \def\nRows{\yellowm{5}}\item[\underline{Processing row $n^\circ(i + \nRows)$:}] + we impose that + \[ + \wcpCallToLeq { + anchorRow = i , + relOffset = \nRows , + argOneHi = 0 , + argOneLo = \locMinimalReachable , + argTwoHi = \locCurrBlockHashArgHi , + argTwoLo = \locCurrBlockHashArgLo , + } + \] + and we define the following shorthand + \[ + \locLowerBoundOk \define \res _{i + \nRows} + \] +\end{description} diff --git a/block_hash/processing/representation.tex b/block_hash/processing/representation.tex new file mode 100644 index 0000000..bad628f --- /dev/null +++ b/block_hash/processing/representation.tex @@ -0,0 +1 @@ +\includepdf[fitpaper=true, pages={1}]{lua/representation.pdf} diff --git a/block_hash/processing/result.tex b/block_hash/processing/result.tex new file mode 100644 index 0000000..011bdf8 --- /dev/null +++ b/block_hash/processing/result.tex @@ -0,0 +1,20 @@ +\[ + \boxed{\text{All constraints in this subsection assume } \isMacro _{i} = 1 } +\] +The present constraints set the \inst{BLOCKHASH} result in terms of the pre-processing of the previous section. +\begin{enumerate} + \item we unconditionally impose that + \[ + \left\{ \begin{array}{lcl} + \blockHashResult \high _{i} & = & \locArgumentInBounds \cdot \blockHashValue \high _{i} \\ + \blockHashResult \low _{i} & = & \locArgumentInBounds \cdot \blockHashValue \low _{i} \\ + \end{array} \right. + \] + where we set + \[ + \locArgumentInBounds \define + \locLowerBoundOk + \cdot + \locUpperBoundOk + \] +\end{enumerate} diff --git a/block_hash/processing/shorthands.tex b/block_hash/processing/shorthands.tex new file mode 100644 index 0000000..1387ce6 --- /dev/null +++ b/block_hash/processing/shorthands.tex @@ -0,0 +1,10 @@ +We define the following shorthands: +\[ + \left\{ \begin{array}{lcl} + \locNotFirst & \define & \isMacro _{i - \blockhashDepthValue} \vspace{2mm} \\ + \locPrevBlockHashArgHi & \define & \locNotFirst \cdot \blockHashArgument \high _{i - \blockhashDepthValue} \\ + \locPrevBlockHashArgLo & \define & \locNotFirst \cdot \blockHashArgument \low _{i - \blockhashDepthValue} \vspace{2mm} \\ + \locCurrBlockHashArgHi & \define & \blockHashArgument \high _{i} \\ + \locCurrBlockHashArgLo & \define & \blockHashArgument \low _{i} \\ + \end{array} \right. +\] diff --git a/hub/lookups/into_block_hash.tex b/hub/lookups/into_block_hash.tex index 935c244..d563155 100644 --- a/hub/lookups/into_block_hash.tex +++ b/hub/lookups/into_block_hash.tex @@ -32,8 +32,8 @@ \begin{enumerate} \item $\relBlock _{j}$ \item[\vspace{\fill}] - \item $\blockNumber\high _{j}$ - \item $\blockNumber\low _{j}$ + \item $\blockHashArgument\high _{j}$ + \item $\blockHashArgument\low _{j}$ \item $\resHi _{j}$ \item $\resLo _{j}$ \end{enumerate} diff --git a/pkg/block_hash.sty b/pkg/block_hash.sty index 6baa90b..cd52658 100644 --- a/pkg/block_hash.sty +++ b/pkg/block_hash.sty @@ -1,7 +1,8 @@ \newcommand{\blockNumberOfFirstBlockInConflation} {\col{FIRST\_BLOCK\_NUMBER}} \newcommand{\blockShift} {\col{BLOCK\_SHIFT}} -\newcommand{\blockNumber} {\col{BLOCK\_NUMBER}} -\newcommand{\blockHash} {\col{BLOCK\_HASH}} +\newcommand{\blockHashArgument} {\col{BLOCKHASH\_ARG}} +\newcommand{\blockHashValue} {\col{BLOCKHASH\_VAL}} +\newcommand{\blockHashResult} {\col{BLOCKHASH\_RES}} \newcommand{\lowerBoundCheck} {\col{LOWER\_BOUND\_CHECK}} \newcommand{\upperBoundCheck} {\col{UPPER\_BOUND\_CHECK}} \newcommand{\inRange} {\col{IN\_RANGE}} diff --git a/pkg/xkeyval_macros/wcp_calls.sty b/pkg/xkeyval_macros/wcp_calls.sty index 4d23e8c..747b7d2 100644 --- a/pkg/xkeyval_macros/wcp_calls.sty +++ b/pkg/xkeyval_macros/wcp_calls.sty @@ -101,4 +101,16 @@ \end{array} \right] } +\newcommand{\resultMustBeFalseName} {\texttt{resultMustBeFalse}} +\newcommand{\resultMustBeFalse} [1] { + \setkeys[WCP]{var}{#1} + \resultMustBeFalseName _{\cmdWCP@var@anchorRow} + \big[ \, \cmdWCP@var@relOffset \, \big]} + +\newcommand{\resultMustBeTrueName} {\texttt{resultMustBeTrue}} +\newcommand{\resultMustBeTrue} [1] { + \setkeys[WCP]{var}{#1} + \resultMustBeTrueName _{\cmdWCP@var@anchorRow} + \big[ \, \cmdWCP@var@relOffset \, \big]} + \makeatother diff --git a/txn_data/_local.tex b/txn_data/_local.tex index 71c40c4..e903b76 100644 --- a/txn_data/_local.tex +++ b/txn_data/_local.tex @@ -73,6 +73,3 @@ \utt{Row offset:} & #2 \\ \utt{Argument 1:} & #3 \\ \end{array} \right]} - -\newcommand{\resultMustBeFalse} [2] {\texttt{resultMustBeFalse} _{#1} \big[ \, #2 \, \big]} -\newcommand{\resultMustBeTrue} [2] {\texttt{resultMustBeTrue} _{#1} \big[ \, #2 \, \big]} diff --git a/txn_data/constraint_systems.tex b/txn_data/constraint_systems.tex index 41d9e37..2f4ad34 100644 --- a/txn_data/constraint_systems.tex +++ b/txn_data/constraint_systems.tex @@ -56,7 +56,13 @@ \argOneLo _{i + \relof} & = & \col{arg\_1} \\ \argTwoLo _{i + \relof} & = & \col{arg\_2} \\ \end{array} \right. \vspace{4mm} \\ - \resultMustBeFalse {i}{\relof} & \iff & \res _{i + \relof} = \rZero \\ - \resultMustBeTrue {i}{\relof} & \iff & \res _{i + \relof} = \rOne \\ + \resultMustBeFalse { + anchorRow = i , + relOffset = \relof , + } & \iff & \res _{i + \relof} = \rZero \\ + \resultMustBeTrue { + anchorRow = i , + relOffset = \relof , + } & \iff & \res _{i + \relof} = \rOne \\ \end{array} \right. \] diff --git a/txn_data/cumulative.tex b/txn_data/cumulative.tex index e359e7b..35f921f 100644 --- a/txn_data/cumulative.tex +++ b/txn_data/cumulative.tex @@ -30,8 +30,10 @@ {\blockGasLimit} \vspace{2mm} \\ - \resultMustBeTrue - {i}{\maxCtTypeZero + 1} + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxCtTypeZero + 1 , + } \\ \end{array} \right. \] @@ -44,8 +46,10 @@ {\blockGasLimit} \vspace{2mm} \\ - \resultMustBeTrue - {i}{\maxCtTypeOne + 1} + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxCtTypeOne + 1 , + } \\ \end{array} \right. \] @@ -58,8 +62,10 @@ {\blockGasLimit} \vspace{2mm} \\ - \resultMustBeTrue - {i}{\maxCtTypeTwo + 1} + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxCtTypeTwo + 1 , + } \\ \end{array} \right. \] diff --git a/txn_data/shared_computations.tex b/txn_data/shared_computations.tex index fc331e8..00b77fc 100644 --- a/txn_data/shared_computations.tex +++ b/txn_data/shared_computations.tex @@ -14,8 +14,10 @@ {\maxNonce} \vspace{2mm} \\ - \resultMustBeTrue - {i}{\nonceRowOffset} + \resultMustBeTrue { + anchorRow = i , + relOffset = \nonceRowOffset , + } \\ \end{array}\right. \] @@ -33,8 +35,10 @@ {\txInitialBalance_{i}} \vspace{2mm} \\ - \resultMustBeTrue - {i}{\balanceRowOffset} + \resultMustBeTrue { + anchorRow = i , + relOffset = \balanceRowOffset , + } \\ \end{array}\right. \] @@ -50,8 +54,10 @@ {\locGasLimit} \vspace{2mm} \\ - \resultMustBeTrue - {i}{\gasLimitRowOffset} + \resultMustBeTrue { + anchorRow = i , + relOffset = \gasLimitRowOffset , + } \\ \end{array}\right. \] @@ -156,8 +162,10 @@ {\locMaximalGasPrice} \vspace{2mm} \\ - \resultMustBeTrue - {i}{\maxFeeVsBaseFeeRowOffset} + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxFeeVsBaseFeeRowOffset , + } \\ \end{array} \right. \] diff --git a/txn_data/specialized_computations.tex b/txn_data/specialized_computations.tex index c949c51..e8bdd79 100644 --- a/txn_data/specialized_computations.tex +++ b/txn_data/specialized_computations.tex @@ -17,8 +17,10 @@ {\locMaxFee } \vspace{2mm} \\ - \resultMustBeTrue - {i}{\maxFeeVsMaxPriorityFee} + \resultMustBeTrue { + anchorRow = i , + relOffset = \maxFeeVsMaxPriorityFee , + } \\ \end{array} \right. \]