feat: TRM redesign (#106)

Signed-off-by: F Bojarski <[email protected]>
Co-authored-by: Olivier Bégassat <[email protected]>
Co-authored-by: Olivier Bégassat <[email protected]>

Author: letypequividelespoubelles

.github/workflows/compile.yml

@@ -12,7 +12,7 @@ jobs:
       - name: Install JetBrainsMono
         run: mkdir JetBrainsMono
              && cd JetBrainsMono
-             && wget https://download.jetbrains.com/fonts/JetBrainsMono-2.304.zip
+              && wget https://download.jetbrains.com/fonts/JetBrainsMono-2.304.zip
              && unzip JetBrainsMono-2.304.zip
              && sudo mv fonts/ttf/*.ttf /usr/share/fonts/
              && cd -

pkg/trm.sty

@@ -1,7 +1,9 @@
-\newcommand{\iAddrHi}              {\imported{\addr\high}}
-\newcommand{\iAddrLo}              {\imported{\addr\low}}
 \newcommand{\trmAddrHi}            {\trmMod\col{\_}\addr\col{\_HI}}
 \newcommand{\rawAddrHi}            {\col{RAW\_ADDR\_HI}}
 \newcommand{\rawAddrLo}            {\col{RAW\_ADDR\_LO}}
 \newcommand{\isPrecompile}         {\col{IS\_PRECOMPILE}}
-\newcommand{\plateauBit}           {\col{PLATEAU\_BIT}}
+\newcommand{\trmLeadHi}            {\col{leading\_bytes}}
+\newcommand{\first}                {\col{FIRST}}
+
+\newcommand{\maxPrecompileAddressName} {\red{\texttt{MAX\_PRC\_ADDRESS}}}
+\newcommand{\maxPrecompileAddress}     {\red{9}}

trm/.DS_Store

@@ -1,6 +1,7 @@
-\documentclass{article}
+\documentclass[fleqn]{report}
 \usepackage[dvipsnames]{xcolor}
 \usepackage{../pkg/common}
+\usepackage{xkeyval}
 % \usepackage{../pkg/dark_theme}
 \usepackage{../pkg/std}
 \usepackage{../pkg/flags_stamps_selectors}
@@ -14,6 +15,10 @@
 \usepackage{../pkg/exponent}
 \usepackage{../pkg/thm_env}
 \usepackage{../pkg/offset_processor}
+\usepackage{../pkg/wc3}
+\usepackage{../pkg/xkeyval_macros/wcp_calls}
+\usepackage{../pkg/draculatheme}
+\usepackage{../pkg/iomf_done}
 
 \title{Address trimming module}
 \author{Rollup team}

trm/_all_trm.tex

@@ -1,3 +1,4 @@
+\input{_local}
 \section{Address trimming module}
 \subsection{Introduction}               \input{introduction}
 \subsection{Columns}                    \input{columns}
@@ -6,7 +7,5 @@ \section{Constraints}
 \subsection{Heartbeat}                  \label{sec: heartbeat} \input{heartbeat}
 \subsection{Counter constancies}        \input{constancies}
 \subsection{Binary constraints}         \input{binary}
-\subsection{\plateauBit{} contraints}   \input{plateau}
-\subsection{Byte decomposition}         \input{byteDec}
-\subsection{Target constraints}         \input{target}
-\subsection{Identifying precompiles}    \input{precompiles}
+\subsection{Computations}               \input{setting_wcp_arg}
+\subsection{Lookup}                     \input{lookup}

trm/_inputs.tex

@@ -0,0 +1,12 @@
+\def\locCtMaxTrm                            {\yellowm{3}}
+\def\locCtMaxTrmName                        {\yellowm{{\texttt{ct\_max\_trm}}}}
+\def\locAddressIsZero                       {\col{address\_is\_zero}}
+\def\locAddressIsNonzero                    {\col{address\_is\_nonzero}}
+\def\locAddressIsAtMostMaxPrecompileAddress {\col{address\_at\_most\_max\_PRC}}
+%
+\def\anchorRow                              {\redm{4}}
+%
+\def\rowOffsetAddress                       {\redm{0}}
+\def\rowOffsetAddressTrm                    {\redm{1}}
+\def\rowOffsetNonZeroAddr                   {\redm{2}}
+\def\rowOffsetPrcAddr                       {\redm{3}}

trm/_local.tex

@@ -1,8 +1,8 @@
 The following columns are binary:
 \begin{multicols}{3}
 \begin{enumerate}
-	\item $\isPrecompile$
-	\item $\plateauBit$
-	\item $\bit{1}$
+	\item $\iomf$
+	\item $\first$        \quad (\trash)
+	\item $\isPrecompile$ \quad (\trash)
 \end{enumerate}
 \end{multicols}

trm/binary.tex

@@ -1,25 +1,24 @@
 \begin{enumerate}
-	\item $\trmStamp$:
-		stamp column; starts at $0$ and grows by 1 with every served request; like many other stamp columns its main purpose is to separate the different requests to that module;
-	\item $\rawAddrHi$ and $\rawAddrLo$:
+	\item $\iomf$:
+	monotonous bit column that lights up for non-padding rows;
+	\item $\first$:
+		bit column that lights up precisely at the first row of all counter-loop;
+	\item
 		\godGiven{}
+		$\rawAddrHi$ and $\rawAddrLo$:
 		\ccc{}; contains the high and low part of some stack value which ought to be interpreted as an address;
-	\item $\trmAddrHi$:
+	\item
+		\markAsJustifiedHere{}
 		\godGiven{}
+		$\trmAddrHi$:
 		\ccc{}; contains the trimmed version of the high part of the address argument;
-	\item $\isPrecompile$:
+	\item
+		\markAsJustifiedHere{}
 		\godGiven{}
-		\ccbc{}; equals $1$ \emph{if and only if} the trimmed address is in the range $\{1, 2,\dots, 9\}$;
+		$\isPrecompile$:
+		\ccbc{}; equals $1$ \emph{if and only if} the trimmed address is in the range $\{1, 2,\dots, \maxPrecompileAddress\}$;
 	\item $\ct$:
-		counter column: counts continuously from $0$ to $\llargeMO$ and resets;
-	\item $\byteCol{HI}$ and $\acc{HI}$:
-		byte column and associated accumulator column;
-	\item $\byteCol{LO}$ and $\acc{LO}$:
-		byte column and associated accumulator column;
-	\item $\acc{T}$:
-		accumulator column; accumulates some of the bytes from $\byteCol{HI}$;
-	\item $\plateauBit$:
-		binary column that implements a \textbf{binary plateau constraint} in that it switches from $0$ to $1$ when $\ct_{i} = 12$;
-	\item $\bit{1}$:
-		binary column; used in establishing that a (trimmed) address is that of a precompile.
+		counter column: counts continuously from $0$ to $\locCtMaxTrmName$ ($= \locCtMaxTrm$) and resets;
+	\item $\argOneHi$, $\argOneLo$, $\argTwoHi$, $\argTwoLo$, $\res$, $\INST$:
+		arguments for calls to the \wcpMod{} module;
 \end{enumerate}

trm/byteDec.tex

@@ -3,11 +3,11 @@
 	\If \ct_{i} \neq 0 ~ \Then \col{X}_{i} = \col{X}_{i - 1}. 
 \]
 We impose that the following columns be counter constant:
-\begin{multicols}{4}
+\begin{multicols}{2}
 \begin{enumerate}
-	\item $\rawAddrHi$
-	\item $\rawAddrLo$
-	\item $\trmAddrHi$
+	\item $\rawAddrHi$   
+	\item $\rawAddrLo$   
+	\item $\trmAddrHi$   
 	\item $\isPrecompile$
 \end{enumerate}
 \end{multicols}

trm/columns.tex

@@ -1,28 +1,24 @@
-The heartbeat of the address trimming module is very simple: the \ct{} column counts from $0$ to $\llargeMO$ unless the $\trmStamp$ is zero, in which case it hovers at $0$.
+The heartbeat of the address trimming module is very simple: the \ct{} column counts from $0$ to $\locCtMaxTrm$ unless $\iomf$ is zero, in which case it hovers at $0$.
 \begin{enumerate}
-	\item $\trmStamp_{0} = 0$
-	\item $\trmStamp_{i + 1} \in \{ \trmStamp_{i}, 1 + \trmStamp_{i} \}$
-	\item \If $\trmStamp_{i} = 0$ \Then
-	\[
-	\left\{	\begin{array}{lcl}
-		\rawAddrHi_{i}		& \!\!\! = \!\!\! & 0 \\
-		\rawAddrLo_{i}		& \!\!\! = \!\!\! & 0 \\
-		\trmAddrHi_{i}		& \!\!\! = \!\!\! & 0 \\
-		\isPrecompile_{i}	& \!\!\! = \!\!\! & 0 \\
-	\end{array} \right.
-	\qquad
-	\left\{ \begin{array}{lcl}
-		\ct_{i}			& \!\!\! = \!\!\! & 0 \quad (\trash) \\
-		\byteCol{HI}_{i}	& \!\!\! = \!\!\! & 0 \quad (\trash) \\
-		\byteCol{LO}_{i}	& \!\!\! = \!\!\! & 0 \quad (\trash) \\
-	\end{array} \right.
-	\]
-	%$\ct_{i} = 0$
-	\item \If $\trmStamp_{i + 1} \neq \trmStamp_{i}$ \Then $\ct_{i + 1} = 0$
-	\item \If $\trmStamp_{i} \neq 0$ \Then
+	\item $\iomf_{0} = 0$
+	\item $\iomf_{i + 1} \in \{ \iomf_{i}, 1 + \iomf_{i} \}$
+	\item \If $\iomf_{i} = 0$ \Then 
 	\begin{enumerate}
-		\item \If $\ct_{i} \neq \llargeMO$ \Then $\ct_{i + 1} = 1 + \ct_{i}$
-		\item \If $\ct_{i} =    \llargeMO$ \Then $\trmStamp_{i + 1} = 1 + \trmStamp_{i}$
+    	\item $\rawAddrHi_{i}      = 0 $  
+		\item $\rawAddrLo_{i}      = 0 $  
+		\item $\trmAddrHi_{i}      = 0 $  
+		\item $\isPrecompile_{i}   = 0 $
+		\item $\ct_{i+1}           = 0 $
 	\end{enumerate}
-	\item \If $\trmStamp_{N} \neq 0$ \Then $\ct_{N} = \llargeMO$
+	\item \If $\iomf_{i} = 1$ \Then
+		\begin{enumerate}
+		\item \If $\ct_{i} =    0$ \Then $\first_{i} = 1$
+		\item \If $\ct_{i} \neq 0$ \Then $\first_{i} = 0$ (\trash)
+		\item \If $\ct_{i} \neq \locCtMaxTrm$ \Then $\ct_{i + 1} = 1 + \ct_{i}$
+		\item \If $\ct_{i} = \locCtMaxTrm$ \Then $\ct_{i + 1} = 0$
+		\end{enumerate}
+	\item \If $\iomf_{N} = 1$ \Then $\ct_{i} = \locCtMaxTrm$
 \end{enumerate}
+\saNote{}
+There is actually no need to constrain $\first$ to vanish outside of the first row.
+If one writes different values in this column outside of the first row traces will fail.

trm/constancies.tex

@@ -1,25 +1,33 @@
-The \textbf{address trimming module} is a tiny module whose purpose is twofold:
+The \textbf{address trimming module} is a tiny module whose purpose is manyfold:
 (\emph{a})
 reduce 32 byte strings modulo $2^{160}$
 (\emph{b})
 identify addresses of precompiles.
+%(\emph{c})
+%proving the smallness of addresses on behalf of \rlpTxnMod{}. TODO reenable with RLP_TXN update
 Recall that some opcodes take an address stack argument which may require trimming to be interpreted as an address.
 Furthermore when computing a deployment address associated with an invokation of a \inst{CREATE}-type instruction the \rlpAddrMod{} module is called, too, to trim down the raw \texttt{KECCAK} hash.
 Also every new address appearing in the \hubMod{} module is automatically trimmed upon first encounter.
 Note that carrying out the first of these tasks boils down to trimming off the leading bytes off of the high part of the imported address. The following opcodes may trigger it:
 \begin{multicols}{4}
-\begin{enumerate}
-	\item \inst{BALANCE}
-	\item \inst{EXTCODESIZE}
-	\item \inst{EXTCODECOPY}
-	\item \inst{EXTCODEHASH}
-	\item \inst{CALL}
-	\item \inst{CALLCODE}
-	\item \inst{STATICCALL}
-	\item \inst{DELEGATECALL}
-	\item \inst{SELFDESTRUCT}
-	\item[\vspace{\fill}]
-\end{enumerate}
+	\begin{enumerate}
+		\item \inst{BALANCE}
+		\item[\vspace{\fill}]
+		\item[\vspace{\fill}]
+		\item[\vspace{\fill}]
+		\item \inst{EXTCODESIZE}
+		\item \inst{EXTCODECOPY}
+		\item \inst{EXTCODEHASH}
+		\item[\vspace{\fill}]
+		\item \inst{CALL}
+		\item \inst{CALLCODE}
+		\item \inst{STATICCALL}
+		\item \inst{DELEGATECALL}
+		\item \inst{SELFDESTRUCT}
+		\item[\vspace{\fill}]
+		\item[\vspace{\fill}]
+		\item[\vspace{\fill}]
+	\end{enumerate}
 \end{multicols}
 These are precisely the instructions which raise the $\trmFlag$ in the \hubMod{}.
 

trm/heartbeat.tex

@@ -0,0 +1,25 @@
+\begin{description}
+	\item[\underline{Selector:}] none
+	\item[\underline{Source columns:}] ---
+		\begin{multicols}{3}
+			\begin{enumerate}
+				\item $\argOneHi$
+				\item $\argOneLo$
+				\item $\argTwoHi$
+				\item $\argTwoLo$
+				\item $\res$
+				\item $\INST$
+			\end{enumerate}
+		\end{multicols}
+	\item[\underline{Target columns:}] ---
+		\begin{multicols}{3}
+		\begin{enumerate}
+			\item $\argOneHi$
+			\item $\argOneLo$
+			\item $\argTwoHi$
+			\item $\argTwoLo$
+			\item $\res$
+			\item $\INST$
+		\end{enumerate}
+		\end{multicols}
+\end{description}