feat: RLP redesign

pkg/rlp_patterns.sty

@@ -4,5 +4,21 @@
 \newcommand{\rlpByteCounting}           {\texttt{byteCountAndPower}}
 \newcommand{\compareFiftyFive}          {\texttt{compTo55}}
 \newcommand{\fiftyFive}                 {\red{55}}
+\newcommand{\fiftySix}                  {\red{56}}
+% \newcommand{\oneTwoEight}               {\red{128}}
 \newcommand{\Power}{\col{POWER}}
-\newcommand{\limbShifting}{\texttt{limbShifting}}
+\newcommand{\limbShifting}{\texttt{limbShifting}}
+
+
+%Special RLP numbers
+\newcommand{\rlprefixShortInt}                        {\redm{128}} % base RLP prefix of a short integer (<56 bytes long)
+\newcommand{\rlprefixAddress}                         {\redm{148}} % base RLP prefix of an address (148 = 128 + 20)
+\newcommand{\rlprefixStorage}                         {\redm{160}} % base RLP prefix of an address (160 = 128 + 32)
+\newcommand{\rlprefixLongInt}                         {\redm{183}} % base RLP prefix of a long integer (>= 56 bytes long)
+\newcommand{\rlprefixShortList}                       {\redm{192}} % base RLP prefix of a short list (<56 bytes long)
+\newcommand{\rlprefixLongList}                        {\redm{247}} % base RLP prefix of a long list (>= 56 bytes long)
+
+\newcommand{\rlpAddress}                 {\texttt{rlpAddress}}
+\newcommand{\rlpStorageKey}              {\texttt{rlpStorageKey}}
+\newcommand{\rlpInteger}              {\texttt{rlpInteger}}
+\newcommand{\rlpBytestringPrefix}              {\texttt{rlpByteStringPrefix}}

pkg/rlp_tx.sty

@@ -63,13 +63,6 @@
 \newcommand{\phaseR}                                  {\col{IS\_PHASE\_R}}
 \newcommand{\phaseS}                                  {\col{IS\_PHASE\_S}}
 
-
-%Special RLP numbers
-\newcommand{\rlprefixShortInt}                        {\redm{128}} % base RLP prefix of a short integer (<56 bytes long)
-\newcommand{\rlprefixLongInt}                         {\redm{183}} % base RLP prefix of a long integer (>= 56 bytes long)
-\newcommand{\rlprefixShortList}                       {\redm{192}} % base RLP prefix of a short list (<56 bytes long)
-\newcommand{\rlprefixLongList}                        {\redm{247}} % base RLP prefix of a long list (>= 56 bytes long)
-
 %EIP155 value
 \newcommand{\unprotectedV}							  {\redm{27}}
 \newcommand{\unprotectedVPO}						  {\redm{28}}

pkg/wc3.sty

@@ -48,6 +48,8 @@
 \newcommand{\isGeq}                      {\col{IS\_GEQ}}
 \newcommand{\isLeq}                      {\col{IS\_LEQ}}
 
+\newcommand{\wcpCtMax}                      {\col{WCP\_CT\_MAX}}
+
 \newcommand{\iARGONEHI}                 {\imported{\ARGONEHI}}
 \newcommand{\iARGONELO}                 {\imported{\ARGONELO}}
 \newcommand{\iARGTWOHI}                 {\imported{\ARGTWOHI}}

rlp_patterns/_inputs.tex

@@ -5,4 +5,9 @@ \subsection{Comparison to 55}                       \input{fifty_five}
 \subsection{Byte counting constraints}                         \input{byte_counting}
 \subsection{RLP prefix constraints for a small (less than 16 bytes long) integer}              \input{rlp_prefix_int}
 \subsection{RLP prefix constraints for a bytestring}              \input{rlp_prefix_bytestring}
-\subsection{Limb Shifting} \input{limb_shifting}
+\subsection{Limb Shifting} \input{limb_shifting}
+
+\subsection{Address} \input{address}
+\subsection{Storage Key} \input{storage}
+\subsection{Integer} \input{integer}
+\subsection{RLP pefix of a bytestring} \input{bytestring}

rlp_patterns/address.tex

@@ -0,0 +1,39 @@
+The present describes a contraint system that writes the \rlp{}-ization of an address.
+
+We shall assume the following: we are provided with columns
+\begin{itemize}
+    \item $\col{input1}$ and $\col{input2}$: two 16 bytes columns;
+    \item $\col{ct}$: a counter;
+    \item $\col{ctMax}$: a column which specifies the size of the ct-loop;\\
+    \item $\col{trmFlag}$: a flag column;
+    \item $\col{limb}$: a column where the output is written;
+    \item $\col{lc}$: a bit column, is 1 when something is written in the $\col{limb}$, else 0;
+    \item $\col{nBytes}$: number of meaningfull bytes of the $\col{limb}$;
+\end{itemize}
+
+\noindent We subsume under the short hand
+\[
+    \rlpAddress_{i}
+    \left(
+	\begin{array}{r}
+    \col{input1},
+    \col{input2},
+    \col{ct},
+    \col{ctMax}; \\
+    \col{trmFlag},
+    \col{limb},
+    \col{lc},
+    \col{nBytes}; \\
+    \end{array}
+	\right)
+\]
+
+\begin{enumerate}
+    \item $\col{ctMax}_{i} = 1$
+    \item $\col{trmFlag}_{i} = 1$
+    \item $\col{lc}_{i} = 1$
+    \item $\col{limb}_{i}=\rlprefixAddress \cdot (256 ^{\llargeMO}) + \col{input1}_{i} \cdot (256 ^{11})$
+    \item $\col{nBytes}_{i} = 5$
+    \item $\col{limb}_{i+1}=\col{input2}_{i}$
+    \item $\col{nBytes}_{i+1} = \llarge $
+\end{enumerate}

rlp_patterns/bytestring.tex

@@ -0,0 +1,52 @@
+The present describes a contraint system that writes the \rlp{} prefix of a byte string.
+
+We shall assume the following: we are provided with columns
+\begin{itemize}
+    \item $\col{input 1}$: containing the length of the byte string;
+    \item $\col{input 2}$: containing the value of the first byte of the byte string;
+    \item $\col{ct}$: a counter;
+    \item $\col{ctMax}$: a column which specifies the size of the ct-loop;
+
+    \item $\col{rlpUtilFlag}$: a flag column;
+    \item $\col{inst}$: a column containing the instruction;
+    \item $\col{resNoRlpPrefix}$: binary result column;
+    \item $\col{resValueRlpPrefix}$: result column;
+    \item $\col{resNBytes}$: result column;
+    \item $\col{isList}$: binary column to discriminate between the bytestring of a list or not;
+
+    \item $\col{limb}$: a column where the output is written;
+    \item $\col{lc}$: a bit column, is 1 when something is written in the $\col{limb}$, else 0;
+    \item $\col{nBytes}$: number of meaningfull bytes of the $\col{limb}$;
+\end{itemize}
+
+\noindent We subsume under the short hand
+\[
+    \rlpBytestringPrefix_{i}
+    \left(
+	\begin{array}{r}
+    \col{input1},
+    \col{input2},
+    \col{ct},
+    \col{ctMax}; \\
+    \col{rlpUtilFlag},
+    \col{inst},
+    \col{resNoRlpPrefix},
+    \col{resValueRlpPrefix},
+    \col{resNBytes},
+    \col{resPower}; \\
+    \col{limb},
+    \col{lc},
+    \col{nBytes}; \\
+    \end{array}
+	\right)
+\]
+
+\begin{enumerate}
+    \item $\col{rlpUtilFlag}_{i} = 1$
+    \item $\col{inst}_{i} = \inst{BYTESTRING}$
+    \item $\col{ctMax}_{i} = 0$
+
+    \item $\col{lc}_{i} = \col{resNoRlpPrefix}_{i}$
+    \item $\col{limb}_{i} = \col{resValueRlpPrefix}_{i} \cdot \col{resPower}_{i}$
+    \item $\col{nBytes}_{i} = \col{resNBytes}_{i}$
+\end{enumerate}

rlp_patterns/integer.tex

@@ -0,0 +1,57 @@
+The present describes a contraint system that writes the \rlp{}-ization of a (up to) 32-bytes integer.
+
+We shall assume the following: we are provided with columns
+\begin{itemize}
+    \item $\col{input 1}$ and $\col{input 2}$: two 16 bytes columns;
+    \item $\col{ct}$: a counter;
+    \item $\col{ctMax}$: a column which specifies the size of the ct-loop;
+    \item $\col{rlpUtilFlag}$: a flag column;
+    \item $\col{inst}$: a column containing the instruction;
+    \item $\col{resNoRlpPrefix}$: binary result column;
+    \item $\col{resBigInt}$: binary result column;
+    \item $\col{resValueRlpPrefix}$: result column;
+    \item $\col{resNBytes}$: result column;
+    \item $\col{limb}$: a column where the output is written;
+    \item $\col{lc}$: a bit column, is 1 when something is written in the $\col{limb}$, else 0;
+    \item $\col{nBytes}$: number of meaningfull bytes of the $\col{limb}$;
+\end{itemize}
+
+\noindent We subsume under the short hand
+\[
+    \rlpStorageKey_{i}
+    \left(
+	\begin{array}{r}
+    \col{input1},
+    \col{input2},
+    \col{ct},
+    \col{ctMax}; \\
+    \col{rlpUtilFlag},
+    \col{inst},
+    \col{resNoRlpPrefix},
+    \col{resBigInt},
+    \col{resValueRlpPrefix},
+    \col{resNBytes}; \\
+    \col{limb},
+    \col{lc},
+    \col{nBytes}; \\
+    \end{array}
+	\right)
+\]
+
+\begin{enumerate}
+    \item $\col{rlpUtilFlag}_{i} = 1$
+    \item $\col{inst}_{i} = \inst{INTEGER}$
+    \item $\col{ctMax}_{i} = 2$
+
+    \item $\col{lc}_{i} = \col{resNoRlpPrefix}_{i}$
+    \item $\col{limb}_{i} = \col{resValueRlpPrefix}_{i} \cdot (256 ^{\llargeMO})$
+    \item $\col{nBytes}_{i} = 1 \cdot \col{resNoRlpPrefix}_{i}$
+
+    \item $\col{lc}_{i+1} = \col{resBigInt}_{i}$
+    \item $\col{limb}_{i+1}=\col{input1}_{i}$
+    \item $\col{nBytes}_{i+1} = \col{resBigInt}_{i} \cdot \col{resNBytes}_{i}$
+
+    \item $\col{lc}_{i+2} = 1$
+    \item $\col{limb}_{i+2}=\col{input2}_{i}$
+    \item $\col{nBytes}_{i+2} = \llarge $
+\end{enumerate}

rlp_patterns/storage.tex

@@ -0,0 +1,52 @@
+The present describes a contraint system that writes the \rlp{}-ization of a storage key.
+
+We shall assume the following: we are provided with columns
+\begin{itemize}
+    \item $\col{input 1}$ and $\col{input 2}$: two 16 bytes columns;
+    \item $\col{ct}$: a counter;
+    \item $\col{ctMax}$: a column which specifies the size of the ct-loop;
+    \item $\col{wcpFlag}$: a flag column;
+    \item $\col{wcpArg2hi}$, $\col{wcpArg2lo}$: argument columns for the \wcpMod{} module;
+    \item $\col{wcpRes}$: result column for the \wcpMod{} module;
+    \item $\col{inst}$: a column containing the instruction;
+    \item $\col{limb}$: a column where the output is written;
+    \item $\col{lc}$: a bit column, is 1 when something is written in the $\col{limb}$, else 0;
+    \item $\col{nBytes}$: number of meaningfull bytes of the $\col{limb}$;
+\end{itemize}
+
+\noindent We subsume under the short hand
+\[
+    \rlpStorageKey_{i}
+    \left(
+	\begin{array}{r}
+    \col{input1},
+    \col{input2},
+    \col{ct},
+    \col{ctMax}; \\
+    \col{wcpFlag},
+    \col{inst},
+    \col{wcpArg2hi},
+    \col{wcpArg2lo},
+    \col{wcpRes}; \\
+    \col{limb},
+    \col{lc},
+    \col{nBytes}; \\
+    \end{array}
+	\right)
+\]
+
+\begin{enumerate}
+    \item $\col{ctMax}_{i} = 2$
+    \item $\col{wcpFlag}_{i} = 1$
+    \item $\col{inst}_{i} = \inst{LEQ}$
+    \item $\col{wcpArg2hi}_{i} = (256 ^{\llarge} -1) $
+    \item $\col{wcpArg2lo}_{i} = (256 ^{\llarge} -1) $
+    \item $\col{wcpRes}_{i} = 1$
+    \item $\col{lc}_{i} = 1$
+    \item $\col{limb}_{i}=\rlprefixStorage \cdot (256 ^{\llargeMO})$
+    \item $\col{nBytes}_{i} = 1$
+    \item $\col{limb}_{i+1}=\col{input1}_{i}$
+    \item $\col{nBytes}_{i+1} = \llarge $
+    \item $\col{limb}_{i+2}=\col{input2}_{i}$
+    \item $\col{nBytes}_{i+2} = \llarge $
+\end{enumerate}

rlp_utils/_all_rlp_utils.tex

@@ -0,0 +1,50 @@
+\documentclass{article}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{xkeyval}
+\usepackage{../pkg/common}
+\usepackage{xkeyval}
+% \usepackage{../pkg/dark_theme}
+\usepackage{../pkg/std}
+\usepackage{../pkg/env}
+\usepackage{../pkg/flags_stamps_selectors}
+\usepackage{../pkg/instruction_flags}
+\usepackage{../pkg/IEEEtrantools}
+\usepackage{../pkg/access}
+\usepackage{../pkg/trm}
+\usepackage{../pkg/alu_old}
+\usepackage{../pkg/bin}
+\usepackage{../pkg/call_stack}
+\usepackage{../pkg/comparisons}
+\usepackage{../pkg/exceptions}
+\usepackage{../pkg/expansion}
+\usepackage{../pkg/exponent}
+\usepackage{../pkg/gas}
+\usepackage{../pkg/offset_processor}
+\usepackage{../pkg/oob}
+\usepackage{../pkg/public}
+\usepackage{../pkg/ram}
+\usepackage{../pkg/rom}
+\usepackage{../pkg/storage}
+\usepackage{../pkg/warm}
+\usepackage{../pkg/wc3}
+\usepackage{../pkg/shifting}
+\usepackage{../pkg/rlp_tx}
+\usepackage{../pkg/precompiles}
+\usepackage{../pkg/rlp_log}
+\usepackage{../pkg/rlp_patterns}
+\usepackage{../pkg/txn_data}
+\usepackage{../pkg/alu}
+
+\usepackage{../pkg/draculatheme}
+
+\title{Transaction RLP module}
+\author{Rollup team}
+\date{May 2023}
+
+\begin{document}
+
+\maketitle
+\tableofcontents
+\input{_inputs}
+
+\end{document}

rlp_utils/_inputs.tex

@@ -0,0 +1,15 @@
+\input{_local}
+\section{RLP Utils module}
+\subsection{Introduction}                \input{introduction}
+\section{Column descriptions}            \label{rlputils: column descriptions}             \input{columns}
+
+\section{Constraints}
+\subsection{Heartbeat}                   \input{heartbeat}
+\subsection{Counter constancies}        \input{constancies}
+\subsection{Binary constraints}         \input{binary}
+\subsection{\inst{INTEGER} processing}         \input{instruction/integer}
+\subsection{\inst{BYTESTRING} processing}         \input{instruction/bytestring}
+
+\section{Lookups}
+\subsection{Into \wcpMod{} module}                   \input{lookups/rlputils_into_wcp}
+\subsection{Into \shfMod{} module}                   \input{lookups/rlputils_into_shf}

rlp_utils/_local.tex

@@ -0,0 +1,36 @@
+% columns
+\def\shfFlag {\col{SHF\_FLAG}}
+\def\shfArg {\col{SHF\_ARG}}
+\def\shfRes {\col{SHF\_RES}}
+
+% INTEGER instruction
+\def\integerCtMax {\redm{1}}
+
+\def\rowOffsetHighZero {\redm{0}}
+\def\locBigInt {\col{input\_is\_big\_int}}
+\def\locNBytes {\col{n\_bytes}}
+\def\locTotalSize {\col{total\_size}}
+
+\def\rowOffsetSmallInt {\redm{1}}
+\def\locSmallInt                       			{\col{input\_is\_leq\_128}}
+
+
+% BYTESTRING instruction
+\def\locBaseRlpPrefixShort {\col{base\_rlp\_prefix\_short}}
+\def\locBaseRlpPrefixLong {\col{base\_rlp\_prefix\_long}}
+
+\def\bytestringEmptyCtMax {\redm{0}}
+\def\bytestringNonEmptyCtMax {\redm{2}}
+
+\def\locIsList {\col{is\_list}}
+
+\def\rowOffsetNullString  {\redm{0}}
+\def\rowOffsetLengthIsOne {\redm{1}}
+\def\rowOffsetCompareOneTwoEight {\redm{2}}
+\def\rowOffsetCompareFiftyFive {\redm{2}}
+
+\def\locNullBytestring {\col{empty\_bytestring}}
+\def\locLengthIsOne {\col{bytestring\_length\_is\_one}}
+\def\locByteIsLeqOneTwoEight {\col{byte\_leq\_one\_two\_eight}}
+\def\locLengthLtFiftySix {\col{lengtgh\_lt\_fifty\_six}}
+\def\locbytestringLengthBytesize {\col{bytestring\_size\_bytesize}}

rlp_utils/binary.tex

@@ -0,0 +1,6 @@
+The following columns are binary:
+\begin{multicols}{1}
+\begin{enumerate}
+	\item $\iomf$
+\end{enumerate}
+\end{multicols}