From 0e6bab660b2d77fa5f910da20131ff2973725853 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 26 Dec 2024 01:04:20 +0100 Subject: [PATCH 1/9] feat: BLOCKHASH redesign wip --- block_hash/_all_block_hash.tex | 6 +- block_hash/_inputs.tex | 15 ++-- block_hash/_local.tex | 24 ++++++ block_hash/byte_decomposition.tex | 21 ----- block_hash/columns.tex | 48 +++++++---- block_hash/generalities/_inputs.tex | 4 + block_hash/generalities/binarities.tex | 8 ++ block_hash/generalities/constancies.tex | 8 ++ block_hash/generalities/heartbeat.tex | 37 ++++++++ block_hash/generalities/shorthands.tex | 36 ++++++++ block_hash/heartbeat.tex | 15 ---- block_hash/lua/representation.lua.tex | 34 ++++++++ block_hash/processing/_inputs.tex | 4 + block_hash/processing/calls.tex | 64 ++++++++++++++ block_hash/processing/intro.tex | 9 ++ block_hash/processing/processing.tex | 102 +++++++++++++++++++++++ block_hash/processing/representation.tex | 1 + 17 files changed, 374 insertions(+), 62 deletions(-) create mode 100644 block_hash/_local.tex delete mode 100644 block_hash/byte_decomposition.tex create mode 100644 block_hash/generalities/_inputs.tex create mode 100644 block_hash/generalities/binarities.tex create mode 100644 block_hash/generalities/constancies.tex create mode 100644 block_hash/generalities/heartbeat.tex create mode 100644 block_hash/generalities/shorthands.tex delete mode 100644 block_hash/heartbeat.tex create mode 100644 block_hash/lua/representation.lua.tex create mode 100644 block_hash/processing/_inputs.tex create mode 100644 block_hash/processing/calls.tex create mode 100644 block_hash/processing/intro.tex create mode 100644 block_hash/processing/processing.tex create mode 100644 block_hash/processing/representation.tex 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..f670427 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 constraints} \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..7a683fa --- /dev/null +++ b/block_hash/_local.tex @@ -0,0 +1,24 @@ +\def\ctMaxMacro {\texttt{ct\_max\_macro}} +\def\ctMaxPreprocessing {\texttt{ct\_max\_prprc}} +\def\blockhashDepth {\texttt{depth}} +\def\ctMaxMacroValue {\yellowm{1}} +\def\ctMaxPreprocessingValue {\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\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}} 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..87778eb 100644 --- a/block_hash/columns.tex +++ b/block_hash/columns.tex @@ -1,24 +1,40 @@ \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} +The following column 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 $\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 $\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$: +\end{enumerate} +\saNote{} +The interpretation of $\blockNumber\high$ and $\blockNumber\low$ is that they represent +(the high and low parts of) $\bm{\mu}_\textbf{s}\big[0\big]$ +while $\resHi$ and $\resLo$ ought to represent +(the high and low parts of) $\bm{\mu}_\textbf{s}'\big[0\big]$. + +\noindent The following column pertain to the ``micro-instruction processing'' data: +\begin{enumerate}[resume] + \item $\exoInstruction$: + exogenous instruction column; + \item $\argOneHi$, $\argOneHi$, $\argTwoHi$, $\argTwoHi$: + exogenous argument columns; + \item $\res$: + exogenous result column; \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..527598c --- /dev/null +++ b/block_hash/generalities/heartbeat.tex @@ -0,0 +1,37 @@ +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 $\blockNumber\high _{i} = 0$ + \item $\blockNumber\low _{i} = 0$ + \item $\ct _{i} = 0$ + \item \label{block hash: non padding starts on macro instruction} $\isPreprocessing _{i + 1} = 0$ + \end{enumerate} + \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..a2dde1c --- /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} + + & (\ctMaxMacro - 1) & \cdot & \isMacro _{i} \\ + + & (\ctMaxPreprocessing - 1) & \cdot & \isPreprocessing _{i} \\ + \end{array} \right] \\ +\] +where we set +\[ + \left\{ \begin{array}{lcl} + \ctMaxMacro & \define & \ctMaxMacroValue \\ + \ctMaxPreprocessing & \define & \ctMaxPreprocessingValue \\ + \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/lua/representation.lua.tex b/block_hash/lua/representation.lua.tex new file mode 100644 index 0000000..c7c89fb --- /dev/null +++ b/block_hash/lua/representation.lua.tex @@ -0,0 +1,34 @@ +% !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 | NUMBER_HI | NUMBER_LO | RES_HI | 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 | | +|-------+-------+----+--------+-----+-----+-----------+-----------+--------+--------+-------------+-----------------+------+----------+----------+------| + +\end{verbatim} +\end{document} diff --git a/block_hash/processing/_inputs.tex b/block_hash/processing/_inputs.tex new file mode 100644 index 0000000..ae7a399 --- /dev/null +++ b/block_hash/processing/_inputs.tex @@ -0,0 +1,4 @@ +\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} diff --git a/block_hash/processing/calls.tex b/block_hash/processing/calls.tex new file mode 100644 index 0000000..f8b1041 --- /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} + \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} & = & \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} + \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} & = & \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} + \exoInstruction _{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..d58b87b --- /dev/null +++ b/block_hash/processing/intro.tex @@ -0,0 +1,9 @@ +We introduce relevant processing instructions. +Their purpose 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 0 \vee \big[ \absBlock - \redm{256} \big]$ +\end{itemize} diff --git a/block_hash/processing/processing.tex b/block_hash/processing/processing.tex new file mode 100644 index 0000000..867c707 --- /dev/null +++ b/block_hash/processing/processing.tex @@ -0,0 +1,102 @@ +\[ + \boxed{\text{All constraints in this subsection assume } \isMacro _{i} = 1 } +\] +To this end we define the following shorthands: +\[ + \left\{ \begin{array}{lcl} + \locPrevBlockHashArgHi & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockNumber \high _{i - \blockhashDepthValue} \\ + \locPrevBlockHashArgLo & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockNumber \low _{i - \blockhashDepthValue} \vspace{2mm} \\ + \locCurrBlockHashArgHi & \define & \blockNumber \high _{i} \\ + \locCurrBlockHashArgLo & \define & \blockNumber \low _{i} \\ + \end{array} \right. +\] +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$ + \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} From 67aa7067ae3e9a0b431863883b4a586ac0d5d081 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 26 Dec 2024 13:17:14 +0100 Subject: [PATCH 2/9] feat: setting BLOCKHASH result wip --- block_hash/_local.tex | 1 + block_hash/processing/_inputs.tex | 1 + block_hash/processing/result.tex | 28 ++++++++++++++++++++++++++++ 3 files changed, 30 insertions(+) create mode 100644 block_hash/processing/result.tex diff --git a/block_hash/_local.tex b/block_hash/_local.tex index 7a683fa..7ea296c 100644 --- a/block_hash/_local.tex +++ b/block_hash/_local.tex @@ -22,3 +22,4 @@ \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/processing/_inputs.tex b/block_hash/processing/_inputs.tex index ae7a399..8df9737 100644 --- a/block_hash/processing/_inputs.tex +++ b/block_hash/processing/_inputs.tex @@ -2,3 +2,4 @@ \subsection{Introduction} \label{block hash: processing: intr \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/result.tex b/block_hash/processing/result.tex new file mode 100644 index 0000000..504676b --- /dev/null +++ b/block_hash/processing/result.tex @@ -0,0 +1,28 @@ +\[ + \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} + \resHi _{i} & = & \locArgumentInBounds \cdot \blockHash\high _{i} \\ + \resLo _{i} & = & \locArgumentInBounds \cdot \blockHash\low _{i} \\ + \end{array} \right. + \] + where we set + \[ + \locArgumentInBounds \define + \locLowerBoundOk + \cdot + \locUpperBoundOk + \] + \item \If $\locSameBlockHashArgument _{i} = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \blockHash\high _{i} & = & \locArgumentInBounds \cdot \blockHash\high _{i - \blockhashDepthValue} \\ + \blockHash\low _{i} & = & \locArgumentInBounds \cdot \blockHash\low _{i - \blockhashDepthValue} \\ + \end{array} \right. + \] +\end{enumerate} +where From c61332a5ab7f9dbc0c8295e577c87049a6371d36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 26 Dec 2024 13:50:04 +0100 Subject: [PATCH 3/9] ras: renaming --- block_hash/columns.tex | 8 ++++---- block_hash/consistency.tex | 10 +++++----- block_hash/generalities/heartbeat.tex | 4 ++-- block_hash/lookups/_inputs.tex | 8 ++++---- block_hash/lookups/into_wcp_lex_ordering.tex | 10 +++++----- block_hash/lookups/into_wcp_lower_bound.tex | 6 +++--- block_hash/lookups/into_wcp_upper_bound.tex | 6 +++--- block_hash/processing/processing.tex | 8 ++++---- block_hash/processing/result.tex | 8 ++++---- hub/lookups/into_block_hash.tex | 4 ++-- pkg/block_hash.sty | 4 ++-- 11 files changed, 38 insertions(+), 38 deletions(-) diff --git a/block_hash/columns.tex b/block_hash/columns.tex index 87778eb..1a3fa33 100644 --- a/block_hash/columns.tex +++ b/block_hash/columns.tex @@ -16,15 +16,15 @@ relative block number in a given conflation, starts at $1$; \item \absBlock{}: absolute block number; - \item $\blockNumber\high$ and $\blockNumber\low$: + \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 $\resHi$ and $\resLo$: high and low parts of \inst{BLOCKHASH} opcode result; - \item $\blockHash\high$ and $\blockHash\low$: - high and low part of the block hash of the block; \end{enumerate} \saNote{} -The interpretation of $\blockNumber\high$ and $\blockNumber\low$ is that they represent +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 $\resHi$ and $\resLo$ ought to represent (the high and low parts of) $\bm{\mu}_\textbf{s}'\big[0\big]$. diff --git a/block_hash/consistency.tex b/block_hash/consistency.tex index 7ff0fac..8d23042 100644 --- a/block_hash/consistency.tex +++ b/block_hash/consistency.tex @@ -1,11 +1,11 @@ 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: + \item $\resHi_{i} = \inRange_{i} \cdot \blockHashValue\high_{i}$ + \item $\resLo_{i} = \inRange_{i} \cdot \blockHashValue\low_{i}$ + \item \If $\blockHashArgument\low_{i} = \blockHashArgument\low_{i-1}$ \Then: \begin{enumerate} - \item $\blockHash\high_{i} = \blockHash\high_{i-1}$ - \item $\blockHash\low _{i} = \blockHash\low _{i-1}$ + \item $\blockHashValue\high_{i} = \blockHashValue\high_{i-1}$ + \item $\blockHashValue\low _{i} = \blockHashValue\low _{i-1}$ \end{enumerate} \end{enumerate} diff --git a/block_hash/generalities/heartbeat.tex b/block_hash/generalities/heartbeat.tex index 527598c..8ffdf5d 100644 --- a/block_hash/generalities/heartbeat.tex +++ b/block_hash/generalities/heartbeat.tex @@ -4,8 +4,8 @@ \item $\iomf_{0} = 0$ \item \If $\iomf_{i} = 0$ \Then: \begin{enumerate} - \item $\blockNumber\high _{i} = 0$ - \item $\blockNumber\low _{i} = 0$ + \item $\blockHashArgument\high _{i} = 0$ + \item $\blockHashArgument\low _{i} = 0$ \item $\ct _{i} = 0$ \item \label{block hash: non padding starts on macro instruction} $\isPreprocessing _{i + 1} = 0$ \end{enumerate} diff --git a/block_hash/lookups/_inputs.tex b/block_hash/lookups/_inputs.tex index 93f1e64..cc45cda 100644 --- a/block_hash/lookups/_inputs.tex +++ b/block_hash/lookups/_inputs.tex @@ -1,4 +1,4 @@ -\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{} module: lower bound of $\blockHashArgument$} \label{block hash: lookups: wcp: lower bound} \input{lookups/into_wcp_lower_bound} +\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{} module: upper bound of $\blockHashArgument$} \label{block hash: lookups: wcp: upper bound} \input{lookups/into_wcp_upper_bound} +\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{} module: lexicographic ordering of $\blockHashArgument$} \label{block hash: lookups: wcp: lexicographic ordering} \input{lookups/into_wcp_lex_ordering} +\subsection{\blockHashMod{} $\hookrightarrow$ \btcMod{} module: $\blockHashArgument$ extraction} \label{block hash: lookups: block data: (block)number extraction} \input{lookups/into_block_data} diff --git a/block_hash/lookups/into_wcp_lex_ordering.tex b/block_hash/lookups/into_wcp_lex_ordering.tex index fc4ef7c..bf681ba 100644 --- a/block_hash/lookups/into_wcp_lex_ordering.tex +++ b/block_hash/lookups/into_wcp_lex_ordering.tex @@ -1,14 +1,14 @@ -The purpose of the present lookup argument is to delegate the proof of lexicographic ordering of $\blockNumber\low$ to the \wcpMod{} module. +The purpose of the present lookup argument is to delegate the proof of lexicographic ordering of $\blockHashArgument\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 $\blockHashArgument\high_{i}$ + \item $\blockHashArgument\low_{i}$ + \item $\blockHashArgument\high_{i-1}$ + \item $\blockHashArgument\low_{i-1}$ \item $1$ \item $\inst{GEQ}$ \end{enumerate} diff --git a/block_hash/lookups/into_wcp_lower_bound.tex b/block_hash/lookups/into_wcp_lower_bound.tex index 6fb22d4..40e28c1 100644 --- a/block_hash/lookups/into_wcp_lower_bound.tex +++ b/block_hash/lookups/into_wcp_lower_bound.tex @@ -1,12 +1,12 @@ -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{Source columns:}] --- \begin{multicols}{3} \begin{enumerate} - \item $\blockNumber\high_{i}$ - \item $\blockNumber\low_{i}$ + \item $\blockHashArgument\high_{i}$ + \item $\blockHashArgument\low_{i}$ \item $0$ \item $\absBlock_{i}-\blockHashInstMaxHistory$ \item $\lowerBoundCheck_{i}$ diff --git a/block_hash/lookups/into_wcp_upper_bound.tex b/block_hash/lookups/into_wcp_upper_bound.tex index c949ba8..bc9ff1a 100644 --- a/block_hash/lookups/into_wcp_upper_bound.tex +++ b/block_hash/lookups/into_wcp_upper_bound.tex @@ -1,12 +1,12 @@ -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{Source columns:}] --- \begin{multicols}{3} \begin{enumerate} - \item $\blockNumber\high_{i}$ - \item $\blockNumber\low_{i}$ + \item $\blockHashArgument\high_{i}$ + \item $\blockHashArgument\low_{i}$ \item $0$ \item $\absBlock_{i}$ \item $\upperBoundCheck_{i}$ diff --git a/block_hash/processing/processing.tex b/block_hash/processing/processing.tex index 867c707..7dfdc0b 100644 --- a/block_hash/processing/processing.tex +++ b/block_hash/processing/processing.tex @@ -4,10 +4,10 @@ To this end we define the following shorthands: \[ \left\{ \begin{array}{lcl} - \locPrevBlockHashArgHi & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockNumber \high _{i - \blockhashDepthValue} \\ - \locPrevBlockHashArgLo & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockNumber \low _{i - \blockhashDepthValue} \vspace{2mm} \\ - \locCurrBlockHashArgHi & \define & \blockNumber \high _{i} \\ - \locCurrBlockHashArgLo & \define & \blockNumber \low _{i} \\ + \locPrevBlockHashArgHi & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockHashArgument \high _{i - \blockhashDepthValue} \\ + \locPrevBlockHashArgLo & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockHashArgument \low _{i - \blockhashDepthValue} \vspace{2mm} \\ + \locCurrBlockHashArgHi & \define & \blockHashArgument \high _{i} \\ + \locCurrBlockHashArgLo & \define & \blockHashArgument \low _{i} \\ \end{array} \right. \] We impose the following constraints diff --git a/block_hash/processing/result.tex b/block_hash/processing/result.tex index 504676b..91baff6 100644 --- a/block_hash/processing/result.tex +++ b/block_hash/processing/result.tex @@ -6,8 +6,8 @@ \item we unconditionally impose that \[ \left\{ \begin{array}{lcl} - \resHi _{i} & = & \locArgumentInBounds \cdot \blockHash\high _{i} \\ - \resLo _{i} & = & \locArgumentInBounds \cdot \blockHash\low _{i} \\ + \resHi _{i} & = & \locArgumentInBounds \cdot \blockHashValue\high _{i} \\ + \resLo _{i} & = & \locArgumentInBounds \cdot \blockHashValue\low _{i} \\ \end{array} \right. \] where we set @@ -20,8 +20,8 @@ \item \If $\locSameBlockHashArgument _{i} = 1$ \Then \[ \left\{ \begin{array}{lcl} - \blockHash\high _{i} & = & \locArgumentInBounds \cdot \blockHash\high _{i - \blockhashDepthValue} \\ - \blockHash\low _{i} & = & \locArgumentInBounds \cdot \blockHash\low _{i - \blockhashDepthValue} \\ + \blockHashValue\high _{i} & = & \locArgumentInBounds \cdot \blockHashValue\high _{i - \blockhashDepthValue} \\ + \blockHashValue\low _{i} & = & \locArgumentInBounds \cdot \blockHashValue\low _{i - \blockhashDepthValue} \\ \end{array} \right. \] \end{enumerate} 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..7a959c7 100644 --- a/pkg/block_hash.sty +++ b/pkg/block_hash.sty @@ -1,7 +1,7 @@ \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{\lowerBoundCheck} {\col{LOWER\_BOUND\_CHECK}} \newcommand{\upperBoundCheck} {\col{UPPER\_BOUND\_CHECK}} \newcommand{\inRange} {\col{IN\_RANGE}} From c3d1e3a02d5e8c3d6e1c1315f8e9c29feda88939 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sat, 28 Dec 2024 09:44:02 +0100 Subject: [PATCH 4/9] feat: finishing BLOCKHASH --- block_hash/_inputs.tex | 2 +- block_hash/_local.tex | 1 + block_hash/columns.tex | 15 +++++--- block_hash/consistency.tex | 15 ++++---- block_hash/generalities/heartbeat.tex | 22 ++++++++---- block_hash/lookups/_inputs.tex | 6 ++-- block_hash/lookups/into_block_data.tex | 8 ++--- ...{into_wcp_upper_bound.tex => into_wcp.tex} | 14 ++++---- block_hash/lookups/into_wcp_lex_ordering.tex | 27 -------------- block_hash/lookups/into_wcp_lower_bound.tex | 27 -------------- block_hash/processing/_inputs.tex | 1 + block_hash/processing/calls.tex | 36 +++++++++---------- block_hash/processing/intro.tex | 13 +++++-- block_hash/processing/processing.tex | 17 ++++----- block_hash/processing/result.tex | 12 ++----- block_hash/processing/shorthands.tex | 10 ++++++ 16 files changed, 95 insertions(+), 131 deletions(-) rename block_hash/lookups/{into_wcp_upper_bound.tex => into_wcp.tex} (72%) delete mode 100644 block_hash/lookups/into_wcp_lex_ordering.tex delete mode 100644 block_hash/lookups/into_wcp_lower_bound.tex create mode 100644 block_hash/processing/shorthands.tex diff --git a/block_hash/_inputs.tex b/block_hash/_inputs.tex index f670427..e07d49c 100644 --- a/block_hash/_inputs.tex +++ b/block_hash/_inputs.tex @@ -4,6 +4,6 @@ \subsection{Introduction} \label{block hash: intro} \subsection{Columns} \label{block hash: columns} \input{columns} \section{Generalities} \label{block hash: generalities} \input{generalities/_inputs} -\section{Processing constraints} \label{block hash: processing} \input{processing/_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 index 7ea296c..549bf9f 100644 --- a/block_hash/_local.tex +++ b/block_hash/_local.tex @@ -11,6 +11,7 @@ \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} diff --git a/block_hash/columns.tex b/block_hash/columns.tex index 1a3fa33..5c1bc1b 100644 --- a/block_hash/columns.tex +++ b/block_hash/columns.tex @@ -1,3 +1,4 @@ +The following set of columns are used to define the heartbeat of the present module. \begin{enumerate} \item $\iomf$: binary column indicating non padding rows; @@ -10,7 +11,11 @@ \item \ctMax: maximum counter value; \end{enumerate} -The following column pertain to the ``macro-instruction'' data: +\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$; @@ -20,18 +25,18 @@ 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 $\resHi$ and $\resLo$: + \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 $\resHi$ and $\resLo$ ought to represent +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 column pertain to the ``micro-instruction processing'' data: +\noindent The following columns pertain to the ``instruction-processing'' data: \begin{enumerate}[resume] - \item $\exoInstruction$: + \item $\instruction$: exogenous instruction column; \item $\argOneHi$, $\argOneHi$, $\argTwoHi$, $\argTwoHi$: exogenous argument columns; diff --git a/block_hash/consistency.tex b/block_hash/consistency.tex index 8d23042..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 \blockHashValue\high_{i}$ - \item $\resLo_{i} = \inRange_{i} \cdot \blockHashValue\low_{i}$ - \item \If $\blockHashArgument\low_{i} = \blockHashArgument\low_{i-1}$ \Then: - \begin{enumerate} - \item $\blockHashValue\high_{i} = \blockHashValue\high_{i-1}$ - \item $\blockHashValue\low _{i} = \blockHashValue\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/heartbeat.tex b/block_hash/generalities/heartbeat.tex index 8ffdf5d..4d1e91f 100644 --- a/block_hash/generalities/heartbeat.tex +++ b/block_hash/generalities/heartbeat.tex @@ -3,12 +3,22 @@ \item we unconditionally impose $\iomf _{i} = \locFlagSum _{i}$ \item $\iomf_{0} = 0$ \item \If $\iomf_{i} = 0$ \Then: - \begin{enumerate} - \item $\blockHashArgument\high _{i} = 0$ - \item $\blockHashArgument\low _{i} = 0$ - \item $\ct _{i} = 0$ - \item \label{block hash: non padding starts on macro instruction} $\isPreprocessing _{i + 1} = 0$ - \end{enumerate} + \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{} diff --git a/block_hash/lookups/_inputs.tex b/block_hash/lookups/_inputs.tex index cc45cda..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 $\blockHashArgument$} \label{block hash: lookups: wcp: lower bound} \input{lookups/into_wcp_lower_bound} -\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{} module: upper bound of $\blockHashArgument$} \label{block hash: lookups: wcp: upper bound} \input{lookups/into_wcp_upper_bound} -\subsection{\blockHashMod{} $\hookrightarrow$ \wcpMod{} module: lexicographic ordering of $\blockHashArgument$} \label{block hash: lookups: wcp: lexicographic ordering} \input{lookups/into_wcp_lex_ordering} -\subsection{\blockHashMod{} $\hookrightarrow$ \btcMod{} module: $\blockHashArgument$ 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 72% rename from block_hash/lookups/into_wcp_upper_bound.tex rename to block_hash/lookups/into_wcp.tex index bc9ff1a..a3fcc9b 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 \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 $\blockHashArgument\high_{i}$ - \item $\blockHashArgument\low_{i}$ - \item $0$ - \item $\absBlock_{i}$ - \item $\upperBoundCheck_{i}$ - \item $\inst{LT}$ + \item $\argOneHi$ + \item $\argOneHi$ + \item $\argTwoHi$ + \item $\argTwoHi$ + \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 bf681ba..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 $\blockHashArgument\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 $\blockHashArgument\high_{i}$ - \item $\blockHashArgument\low_{i}$ - \item $\blockHashArgument\high_{i-1}$ - \item $\blockHashArgument\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 40e28c1..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 \blockHashArgument{} 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 $\blockHashArgument\high_{i}$ - \item $\blockHashArgument\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/processing/_inputs.tex b/block_hash/processing/_inputs.tex index 8df9737..e5b241b 100644 --- a/block_hash/processing/_inputs.tex +++ b/block_hash/processing/_inputs.tex @@ -1,3 +1,4 @@ +\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} diff --git a/block_hash/processing/calls.tex b/block_hash/processing/calls.tex index f8b1041..c13e63a 100644 --- a/block_hash/processing/calls.tex +++ b/block_hash/processing/calls.tex @@ -10,12 +10,12 @@ argTwoLo = \col{b\_lo} , } & \define & \left\{ \begin{array}{lcl} - \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} & = & \relevantValue \\ + \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 { @@ -27,12 +27,12 @@ argTwoLo = \col{b\_lo} , } & \define & \left\{ \begin{array}{lcl} - \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} & = & \relevantValue \\ + \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 { @@ -44,12 +44,12 @@ argTwoLo = \col{b\_lo} , } & \define & \left\{ \begin{array}{lcl} - \exoInstruction _{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 \\ + \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 { diff --git a/block_hash/processing/intro.tex b/block_hash/processing/intro.tex index d58b87b..745d313 100644 --- a/block_hash/processing/intro.tex +++ b/block_hash/processing/intro.tex @@ -1,9 +1,16 @@ -We introduce relevant processing instructions. -Their purpose is to carry out the following comparisons: +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 0 \vee \big[ \absBlock - \redm{256} \big]$ + \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 index 7dfdc0b..65b34c4 100644 --- a/block_hash/processing/processing.tex +++ b/block_hash/processing/processing.tex @@ -1,16 +1,7 @@ \[ \boxed{\text{All constraints in this subsection assume } \isMacro _{i} = 1 } \] -To this end we define the following shorthands: -\[ - \left\{ \begin{array}{lcl} - \locPrevBlockHashArgHi & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockHashArgument \high _{i - \blockhashDepthValue} \\ - \locPrevBlockHashArgLo & \define & \isMacro _{i - \blockhashDepthValue} \cdot \blockHashArgument \low _{i - \blockhashDepthValue} \vspace{2mm} \\ - \locCurrBlockHashArgHi & \define & \blockHashArgument \high _{i} \\ - \locCurrBlockHashArgLo & \define & \blockHashArgument \low _{i} \\ - \end{array} \right. -\] -We impose the following constraints +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 @@ -32,7 +23,11 @@ } \] \saNote{} - The above enforces that $\locPrevBlockHashArg \leq \locCurrBlockHashArg$ + 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 \[ diff --git a/block_hash/processing/result.tex b/block_hash/processing/result.tex index 91baff6..011bdf8 100644 --- a/block_hash/processing/result.tex +++ b/block_hash/processing/result.tex @@ -6,8 +6,8 @@ \item we unconditionally impose that \[ \left\{ \begin{array}{lcl} - \resHi _{i} & = & \locArgumentInBounds \cdot \blockHashValue\high _{i} \\ - \resLo _{i} & = & \locArgumentInBounds \cdot \blockHashValue\low _{i} \\ + \blockHashResult \high _{i} & = & \locArgumentInBounds \cdot \blockHashValue \high _{i} \\ + \blockHashResult \low _{i} & = & \locArgumentInBounds \cdot \blockHashValue \low _{i} \\ \end{array} \right. \] where we set @@ -17,12 +17,4 @@ \cdot \locUpperBoundOk \] - \item \If $\locSameBlockHashArgument _{i} = 1$ \Then - \[ - \left\{ \begin{array}{lcl} - \blockHashValue\high _{i} & = & \locArgumentInBounds \cdot \blockHashValue\high _{i - \blockhashDepthValue} \\ - \blockHashValue\low _{i} & = & \locArgumentInBounds \cdot \blockHashValue\low _{i - \blockhashDepthValue} \\ - \end{array} \right. - \] \end{enumerate} -where 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. +\] From 5def7c8326e9538853733c2b212315bf57ea088c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Sat, 28 Dec 2024 09:54:10 +0100 Subject: [PATCH 5/9] ras: resultMustBeTrue/False refactor --- block_hash/processing/processing.tex | 4 ++-- pkg/block_hash.sty | 1 + pkg/xkeyval_macros/wcp_calls.sty | 12 ++++++++++++ txn_data/_local.tex | 3 --- txn_data/constraint_systems.tex | 10 ++++++++-- txn_data/cumulative.tex | 18 ++++++++++++------ txn_data/shared_computations.tex | 24 ++++++++++++++++-------- txn_data/specialized_computations.tex | 6 ++++-- 8 files changed, 55 insertions(+), 23 deletions(-) diff --git a/block_hash/processing/processing.tex b/block_hash/processing/processing.tex index 65b34c4..92ceac3 100644 --- a/block_hash/processing/processing.tex +++ b/block_hash/processing/processing.tex @@ -18,8 +18,8 @@ we further impose that \[ \resultMustBeTrue { - anchorRow = i, - relOffset = \nRows, + anchorRow = i , + relOffset = \nRows , } \] \saNote{} diff --git a/pkg/block_hash.sty b/pkg/block_hash.sty index 7a959c7..cd52658 100644 --- a/pkg/block_hash.sty +++ b/pkg/block_hash.sty @@ -2,6 +2,7 @@ \newcommand{\blockShift} {\col{BLOCK\_SHIFT}} \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. \] From 945fc84e5f0a895ccc0bcdaec57d118e6899d962 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 6 Jan 2025 13:37:08 +0100 Subject: [PATCH 6/9] fix: missing LO's + ct_max -> nrows --- block_hash/_local.tex | 8 ++++---- block_hash/columns.tex | 2 +- block_hash/generalities/shorthands.tex | 8 ++++---- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/block_hash/_local.tex b/block_hash/_local.tex index 549bf9f..050a1d8 100644 --- a/block_hash/_local.tex +++ b/block_hash/_local.tex @@ -1,8 +1,8 @@ -\def\ctMaxMacro {\texttt{ct\_max\_macro}} -\def\ctMaxPreprocessing {\texttt{ct\_max\_prprc}} +\def\nRowsMacro {\texttt{nrows\_macro}} +\def\nRowsPreprocessing {\texttt{nrows\_prprc}} \def\blockhashDepth {\texttt{depth}} -\def\ctMaxMacroValue {\yellowm{1}} -\def\ctMaxPreprocessingValue {\yellowm{5}} +\def\nRowsMacroValue {\yellowm{1}} +\def\nRowsPreprocessingValue {\yellowm{5}} \def\blockhashDepthValue {\yellowm{6}} \def\locFlagSum {\col{flag\_sum}} \def\locMaxCtSum {\col{ct\_max\_sum}} diff --git a/block_hash/columns.tex b/block_hash/columns.tex index 5c1bc1b..ff20831 100644 --- a/block_hash/columns.tex +++ b/block_hash/columns.tex @@ -38,7 +38,7 @@ \begin{enumerate}[resume] \item $\instruction$: exogenous instruction column; - \item $\argOneHi$, $\argOneHi$, $\argTwoHi$, $\argTwoHi$: + \item $\argOneHi$, $\argOneLo$, $\argTwoHi$, $\argTwoLo$: exogenous argument columns; \item $\res$: exogenous result column; diff --git a/block_hash/generalities/shorthands.tex b/block_hash/generalities/shorthands.tex index a2dde1c..77f43c6 100644 --- a/block_hash/generalities/shorthands.tex +++ b/block_hash/generalities/shorthands.tex @@ -22,15 +22,15 @@ \[ \locMaxCtSum _{i} \define \left[ \begin{array}{crcl} - + & (\ctMaxMacro - 1) & \cdot & \isMacro _{i} \\ - + & (\ctMaxPreprocessing - 1) & \cdot & \isPreprocessing _{i} \\ + + & (\nRowsMacro - 1) & \cdot & \isMacro _{i} \\ + + & (\nRowsPreprocessing - 1) & \cdot & \isPreprocessing _{i} \\ \end{array} \right] \\ \] where we set \[ \left\{ \begin{array}{lcl} - \ctMaxMacro & \define & \ctMaxMacroValue \\ - \ctMaxPreprocessing & \define & \ctMaxPreprocessingValue \\ + \nRowsMacro & \define & \nRowsMacroValue \\ + \nRowsPreprocessing & \define & \nRowsPreprocessingValue \\ \blockhashDepth & \define & \blockhashDepthValue \\ \end{array} \right. \] From 239bdee6ddadaee16a0744c27784efbbddeb78d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 6 Jan 2025 13:48:30 +0100 Subject: [PATCH 7/9] ras: updated BLOCKHASH diagram --- block_hash/lua/representation.lua.tex | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/block_hash/lua/representation.lua.tex b/block_hash/lua/representation.lua.tex index c7c89fb..31c3246 100644 --- a/block_hash/lua/representation.lua.tex +++ b/block_hash/lua/representation.lua.tex @@ -18,17 +18,18 @@ \begin{document} \begin{verbatim} -|-------+-------+----+--------+-----+-----+-----------+-----------+--------+--------+-------------+-----------------+------+----------+----------+------| -| MACRO | MICRO | CT | CT_MAX | ABS | REL | NUMBER_HI | NUMBER_LO | RES_HI | 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 | | -|-------+-------+----+--------+-----+-----+-----------+-----------+--------+--------+-------------+-----------------+------+----------+----------+------| +|-------+-------+----+--------+-----+-----+-----------+-----------+-----------+-----------+-------------+-----------------+------+----------+----------+------| +| 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} From 97db531be377544cfce07cc37639b2d00486c181 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Mon, 6 Jan 2025 15:54:02 +0100 Subject: [PATCH 8/9] fix: BLOCKHASH into HUB lookup fix --- block_hash/lookups/into_wcp.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/block_hash/lookups/into_wcp.tex b/block_hash/lookups/into_wcp.tex index a3fcc9b..7036b9f 100644 --- a/block_hash/lookups/into_wcp.tex +++ b/block_hash/lookups/into_wcp.tex @@ -6,9 +6,9 @@ \begin{multicols}{3} \begin{enumerate} \item $\argOneHi$ - \item $\argOneHi$ - \item $\argTwoHi$ + \item $\argOneLo$ \item $\argTwoHi$ + \item $\argTwoLo$ \item $\res$ \item $\instruction$ \end{enumerate} From 46eb3b36b3de66b9f3e2c8201b34f96555c8ac88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 10 Jan 2025 14:36:57 +0100 Subject: [PATCH 9/9] fix: SLOAD only writes to the stack if unexceptional --- .../storage/constraints.tex | 52 ++++++++++++------- 1 file changed, 32 insertions(+), 20 deletions(-) diff --git a/hub/instruction_handling/storage/constraints.tex b/hub/instruction_handling/storage/constraints.tex index d24f5a1..6e450f2 100644 --- a/hub/instruction_handling/storage/constraints.tex +++ b/hub/instruction_handling/storage/constraints.tex @@ -20,6 +20,7 @@ \inst{SSLOAD} may only raise stack exceptions or \oogxSH{} while \inst{SSTORE} may raise stack exceptions, \staticxSH{}, \sstorexSH{} or \oogxSH{}. \item[\underline{Setting $\nonStackRows$ and peeking flags:}] + \label{hub: instruction handling: storage: non stack rows and peeking flags} storage operations can provoke exceptions in multiple ways and are rollback sensitive; they thus have some inherent complexity; we impose the following: @@ -75,7 +76,7 @@ \saNote{} Recall that (among instructions raising the $\stackDecStoFlag$ flag) only \inst{SSTORE} may raise a \staticxSH{}. \item[\underline{Setting the miscellaneous-row:}] - \If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then + \If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then \begin{enumerate} \item we impose that \inst{SSTORE} instructions trigger the \oobMod{} \[ @@ -103,7 +104,7 @@ \end{enumerate} \item[\underline{Justifying the \stackSstorex{} flag:}] \begin{enumerate} - \If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then + \If $\peekMisc_{i + \locMiscRowOffset} = 1$ \Then \item \If $\locIsSstore = 1$ \Then we impose that $\stackSstorex_{i} = \miscOobDataCol{7}_{i + \locMiscRowOffset}$ \end{enumerate} \end{description} @@ -145,27 +146,38 @@ \end{array} \right. \] \item[\underline{Defining storage value operations:}] - \If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then + we impose that \begin{description} \item[\underline{The \inst{SLOAD} case:}] \If $\locIsSload = 1$ \Then - \[ - \left\{ \begin{array}{lcl} - \multicolumn{3}{l}{\storageReading{i}{\locFirstStoRowOffset}} \\ - \locLoadedValueHi & \!\!\! = \!\!\! & \stoCurrValueHi_{i + \locFirstStoRowOffset} \\ - \locLoadedValueLo & \!\!\! = \!\!\! & \stoCurrValueLo_{i + \locFirstStoRowOffset} \\ - \end{array} \right. - \] + \begin{enumerate} + \item \If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then $\storageReading{i}{\locFirstStoRowOffset}$ + \item \If $(1 - \xAhoy_{i}) = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \locLoadedValueHi & \!\!\! = \!\!\! & \stoCurrValueHi_{i + \locFirstStoRowOffset} \\ + \locLoadedValueLo & \!\!\! = \!\!\! & \stoCurrValueLo_{i + \locFirstStoRowOffset} \\ + \end{array} \right. + \] + \end{enumerate} + \saNote{} + In other words: \inst{SLOAD} instructions that lead to the production of \textbf{storage-rows}, as witnessed by + $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$, see (\ref{hub: instruction handling: storage: non stack rows and peeking flags}), + (\emph{a}) don't modify the value in storage and + (\emph{b}) if unexceptional, as witnessed by $(1 - \xAhoy_{i}) = 1$, write the value in storage to the stack. \item[\underline{The \inst{SSTORE} case:}] \If $\locIsSstore = 1$ \Then - \[ - \left\{ \begin{array}{lcl} - \stoNextValueHi _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreHi \\ - \stoNextValueLo _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreLo \\ - \end{array} \right. - \] + \begin{enumerate} + \item \If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then + \[ + \left\{ \begin{array}{lcl} + \stoNextValueHi _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreHi \\ + \stoNextValueLo _{i + \locFirstStoRowOffset} & \!\!\! = \!\!\! & \locValueToStoreLo \\ + \end{array} \right. + \] + \end{enumerate} \item[\underline{The inverse, undoing operation:}] - \If $\cnWillRev_{i} = 1$ \Then + \If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \et $\cnWillRev_{i} = 1$ \Then \[ \left\{ \begin{array}{lcl} \stoSameStorageSlot {i}{\locSecondStoRowOffset}{\locFirstStoRowOffset} \\ @@ -201,7 +213,7 @@ \locNextNotCurr & \!\!\! \define \!\!\! & 1 - \locNextIsCurr \\ \end{array} \right. \] -\begin{description} +\begin{description} \item[\underline{Setting the gas cost:}] \If $\stackOogx_{i} + (1 - \xAhoy_{i}) = 1$ \Then \begin{description} @@ -277,7 +289,7 @@ \end{array} \right] \cdot \locOrigNotZero - \cdot + \cdot \left[ \begin{array}{cr} - & \locCurrIsZero \\ + & \locNextIsZero \\ @@ -300,7 +312,7 @@ \end{array} \right] \cdot \locNextIsOrig - \cdot + \cdot \left[ \begin{array}{crcl} + & \locOrigIsZero & \cdot & \big(G_\text{sset} - G_\text{warmaccess}\big) \\ + & \locOrigNotZero & \cdot & \big(G_\text{sreset} - G_\text{warmaccess}\big) \\