-
Notifications
You must be signed in to change notification settings - Fork 14
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
d42f83f
commit 4c50ea7
Showing
33 changed files
with
506 additions
and
167 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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}} |
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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. | ||
\] |
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
16 changes: 8 additions & 8 deletions
16
block_hash/lookups/into_wcp_upper_bound.tex → block_hash/lookups/into_wcp.tex
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.