MXP redesign

Makefile

@@ -29,6 +29,7 @@ mmio:         view-mmio
 modexp:       view-modexp_data
 mmu:          view-mmu
 mxp:          view-mxp
+mxp_v3:       view-mxp_v3
 oob:          view-oob
 prc:   	      view-prc
 rlp_addr:     view-rlp_addr
@@ -64,6 +65,7 @@ rmmio:         recompile-mmio
 rmodexp:       recompile-modexp_data
 rmmu:          recompile-mmu
 rmxp:          recompile-mxp
+rmxp_v3:       recompile-mxp_v3
 roob:          recompile-oob
 rprc:          recompile-prc
 rrlp_addr:     recompile-rlp_addr

mxp_v3/_all_mxp_v3.tex

@@ -0,0 +1,39 @@
+\documentclass[fleqn]{article}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{xkeyval}
+\usepackage{../pkg/common}
+%\usepackage{../pkg/dark_theme}
+\usepackage{../pkg/std}
+\usepackage{../pkg/IEEEtrantools}
+\usepackage{../pkg/rom}
+\usepackage{../pkg/env}
+\usepackage{../pkg/euc}
+\usepackage{../pkg/ram}
+\usepackage{../pkg/wc3}
+\usepackage{../pkg/stack}
+\usepackage{../pkg/call_stack}
+\usepackage{../pkg/access}
+\usepackage{../pkg/expansion}
+\usepackage{../pkg/thm_env}
+\usepackage{../pkg/offset_processor}
+\usepackage{../pkg/flags_stamps_selectors}
+\usepackage{../pkg/instruction_flags}
+\usepackage{../pkg/exceptions}
+\usepackage{../pkg/draculatheme}
+\usepackage{../pkg/xkeyval_macros/wcp_calls}
+\usepackage{../pkg/xkeyval_macros/euc_calls}
+
+\usepackage{../pkg/draculatheme}
+
+\title{Memory expansion module}
+\author{Rollup team}
+\date{August 2022}
+
+\begin{document}
+
+\maketitle
+\tableofcontents
+
+\input{_inputs}
+
+\end{document}

mxp_v3/_inputs.tex

@@ -0,0 +1,10 @@
+\input{_local}
+
+\section{Introduction                    \lispNone{}}      \label{mxp: intro}                       \input{intro}
+\section{Instruction decoder             \lispNone{}}      \label{mxp: instruction decoder}         \input{instruction_decoder_representation}
+\section{\hubMod{} / \mxpMod{} interface \lispNone{}}      \label{mxp: hub mxp interface}           \input{hub_mxp_interface}
+\section{Columns                         \lispDone{}}      \label{mxp: columns}                     \input{columns/_inputs}
+\section{Generalities                    \lispDone{}}      \label{mxp: generalities}                \input{generalities/_inputs}
+\section{Computations                    \lispTodo{}}      \label{mxp: computations}                \input{computations/_inputs}
+\section{Consistency                     \lispTodo{}}      \label{mxp: consistency}                 \input{consistency/_inputs}
+\section{Lookups                         \lispTodo{}}      \label{mxp: lookups}                     \input{lookups/_inputs}

mxp_v3/_local.tex

@@ -0,0 +1,95 @@
+\def\rOne                                    {\redm{1}}
+\def\locPerspectiveSum                       {\col{persp\_sum}}
+\def\locWeightSum                            {\col{persp\_wght\_sum}}
+\def\locCtMaxSum                             {\col{ct\_max\_sum}}
+\def\locStampIncrement                       {\col{stamp\_increment}}
+\def\locScenarioSum                          {\mxpScenarioColumn{scenario\_sum}}
+\def\locMxpScenarioNotMsize                  {\mxpScenarioColumn{not\_msize}}
+\def\locMxpScenarioNotMsizeNorTrivial        {\mxpScenarioColumn{not\_msize\_nor\_trivial}}
+\def\locMxpScenarioStateUpdate               {\mxpScenarioColumn{state\_update}}
+\def\locMxpScenarioNoStateUpdate             {\mxpScenarioColumn{no\_state\_update}}
+
+\def\locCtMaxMsize                  {\yellowm{1}}  \def\locCtMaxMsizeName                  {\yellowm{{\texttt{CT\_MAX\_MSIZE}}}}
+\def\locCtMaxTrivialOperation       {\yellowm{2}}  \def\locCtMaxTrivialOperationName       {\yellowm{{\texttt{CT\_MAX\_TRIV}}}}
+\def\locCtMaxMxpx                   {\yellowm{6}}  \def\locCtMaxMxpxName                   {\yellowm{{\texttt{CT\_MAX\_MXPX}}}}
+\def\locCtMaxStateUpdateWordPricing {\yellowm{10}} \def\locCtMaxStateUpdateWordPricingName {\yellowm{{\texttt{CT\_MAX\_UPDT\_W}}}}
+\def\locCtMaxStateUpdateBytePricing {\yellowm{11}} \def\locCtMaxStateUpdateBytePricingName {\yellowm{{\texttt{CT\_MAX\_UPDT\_B}}}}
+% \def\locCtMaxSingleMaxOffsetAndWordPricing {\yellowm{4}} \def\locCtMaxSingleMaxOffsetAndWordPricingName {\yellowm{{\texttt{ct\_max\_1offw}}}}
+% \def\locCtMaxSingleMaxOffsetAndBytePricing {\yellowm{5}} \def\locCtMaxSingleMaxOffsetAndBytePricingName {\yellowm{{\texttt{ct\_max\_1offb}}}}
+% \def\locCtMaxDoubleMaxOffsetAndWordPricing {\yellowm{6}} \def\locCtMaxDoubleMaxOffsetAndWordPricingName {\yellowm{{\texttt{ct\_max\_2offw}}}}
+% \def\locCtMaxDoubleMaxOffsetAndBytePricing {\yellowm{7}} \def\locCtMaxDoubleMaxOffsetAndBytePricingName {\yellowm{{\texttt{ct\_max\_2offb}}}}
+
+\def\locDecoderToMacroRowOffset            {\yellowm{1}} \def\locMacroToDecoderRowOffset                {\locDecoderToMacroRowOffset}
+\def\locMacroToScenarioRowOffset           {\yellowm{1}} \def\locScenarioToMacroRowOffset               {\locMacroToScenarioRowOffset}
+\def\locDecoderToScenarioRowOffset         {\yellowm{2}} \def\locScenarioToDecoderRowOffset             {\locDecoderToScenarioRowOffset}
+
+\def\locOffsetOneHi                        {\col{offset\_1\_hi}}
+\def\locOffsetOneLo                        {\col{offset\_1\_lo}}
+\def\locSizeOneHi                          {\col{size\_1\_hi}}
+\def\locSizeOneLo                          {\col{size\_1\_lo}}
+
+\def\locOffsetTwoHi                        {\col{offset\_2\_hi}}
+\def\locOffsetTwoLo                        {\col{offset\_2\_lo}}
+\def\locSizeTwoHi                          {\col{size\_2\_hi}}
+\def\locSizeTwoLo                          {\col{size\_2\_lo}}
+
+\def\locSizeOneIsZero                      {\col{size\_1\_is\_zero}}
+\def\locSizeOneIsNonZero                   {\col{size\_1\_is\_nonzero}}
+
+\def\locSizeTwoIsZero                      {\col{size\_2\_is\_zero}}
+\def\locSizeTwoIsNonZero                   {\col{size\_2\_is\_nonzero}}
+
+\def\locSizeOneIsSmall                     {\col{size\_1\_is\_small}}
+\def\locSizeOneIsLarge                     {\col{size\_1\_is\_large}}
+
+\def\locSizeTwoIsSmall                     {\col{size\_2\_is\_small}}
+\def\locSizeTwoIsLarge                     {\col{size\_2\_is\_large}}
+
+\def\locOffsetOneIsSmall                   {\col{offset\_1\_is\_small}}
+\def\locOffsetOneIsLarge                   {\col{offset\_1\_is\_large}}
+
+\def\locOffsetTwoIsSmall                   {\col{offset\_2\_is\_small}}
+\def\locOffsetTwoIsLarge                   {\col{offset\_2\_is\_large}}
+
+\def\locMxpComputationMxpxExpressionOne    {\col{mxpx\_expression\_1}}
+\def\locMxpComputationMxpxExpressionTwo    {\col{mxpx\_expression\_2}}
+\def\locMxpComputationMxpxExpression       {\col{mxpx\_expression}}
+
+\def\locMaxOffset                          {\col{max\_offset}}
+
+\def\locMaxOne                             {\col{max\_1}}
+\def\locMaxTwo                             {\col{max\_2}}
+\def\locMaxOffsetOne                       {\col{max\_offset\_1}}
+\def\locMaxOffsetTwo                       {\col{max\_offset\_2}}
+
+\def\locUseParameterSetOne                 {\col{use\_params\_1}}
+\def\locUseParameterSetTwo                 {\col{use\_params\_2}}
+
+\def\locDoubleOffsetOpcode                 {\col{double\_offset}}
+\def\locSingleOffsetOpcode                 {\col{single\_offset}}
+\def\locWordPricingOpcode                  {\col{word\_pricing}}
+\def\locBytePricingOpcode                  {\col{byte\_pricing}}
+\def\locNumberOfWords                      {\col{number\_of\_words}}
+\def\locNumberOfBytes                      {\col{number\_of\_bytes}}
+\def\locWordPrice                          {\col{gas\_per\_word}}
+\def\locBytePrice                          {\col{gas\_per\_byte}}
+\def\locExtraWordCost                      {\col{extra\_word\_cost}}
+\def\locExtraByteCost                      {\col{extra\_byte\_cost}}
+
+\def\locFloor                              {\col{floor}}
+\def\locEypA                               {\col{EYP\_a}}
+\def\locQuadraticPart                      {\col{quadratic\_part}}
+\def\locCmemQuadPart                       {\col{cmem\_quad\_part}}
+\def\locCmemLinrPart                       {\col{cmem\_linear\_part}}
+\def\locUpdateInternalState                {\col{update\_internal\_state}}
+\def\locWords                              {\col{words}}
+
+\def\locSizeOne                            {\col{size\_1}}
+\def\locCeil                               {\col{ceil}}
+
+\def\locCompRequired                       {\col{comp\_required}}
+\def\locComp                               {\col{comp}}
+
+\def\locMxpxExpressionOne                  {\col{mxpx\_expression\_1}}
+\def\locMxpxExpressionTwo                  {\col{mxpx\_expression\_2}}
+\def\locMxpxExpression                     {\col{mxpx\_expression}}

mxp_v3/columns/_inputs.tex

@@ -0,0 +1,5 @@
+\subsection{Common columns              \lispDone{}}      \label{mxp: columns: common}                  \input{columns/common}
+\subsection{Instruction decoder columns \lispDone{}}      \label{mxp: columns: instruction decoder}     \input{columns/decoder}
+\subsection{Macro instruction columns   \lispDone{}}      \label{mxp: columns: macro instruction}       \input{columns/macro}
+\subsection{Scenario columns            \lispDone{}}      \label{mxp: columns: scenario}                \input{columns/scenario/_inputs}
+\subsection{Computation columns         \lispDone{}}      \label{mxp: columns: computation}             \input{columns/computation/_inputs}

mxp_v3/columns/common.tex

@@ -0,0 +1,27 @@
+We introduce a stamp column as well as various perspective columns.
+We shall also require counter columns.
+\begin{enumerate}
+	\item $\mxpStamp$:
+		stamp column for the \mxpMod{} module;
+	\item $\mxpContextNumber$:
+		stamp-constant column containing the relevant context number;
+	\item $\isMxpInstructionDecoder$:
+		binary column;
+	\item $\isMxpMacro$
+		binary column;
+	\item $\isMxpScenario$:
+		binary column; contains a prediction as to the nature of the operation and the required computations;
+	\item $\isMxpComputation$:
+		binary column;
+        \item $\ct$:
+		counter column;
+        \item $\maxCt$:
+		max counter value;
+		perspective and scenario dependent.
+\end{enumerate}
+We introduce the following nomenclature:
+rows where
+$\isMxpInstructionDecoder \equiv \rOne$ will be called \textbf{decoding-rows},
+$\isMxpMacro              \equiv \rOne$ will be called \textbf{macro-instruction-rows},
+$\isMxpScenario           \equiv \rOne$ will be called \textbf{scenario-rows} and
+$\isMxpComputation        \equiv \rOne$ will be called \textbf{computation-rows}.

mxp_v3/columns/computation/_inputs.tex

@@ -0,0 +1,2 @@
+\subsubsection{Computation columns   \lispDone{}}    \label{mxp: columns: scenario: columns}            \input{columns/computation/columns}
+\subsubsection{External module calls \lispDone{}}    \label{mxp: columns: computations: module calls}   \input{columns/computation/calls}

mxp_v3/columns/computation/calls.tex

@@ -0,0 +1,75 @@
+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}
+			\mxpComputationWcpFlag        _{i + \relof} & = & \rOne       \\
+			\mxpComputationExoInst        _{i + \relof} & = & \inst{LT}   \\
+			\mxpComputationArgOneHi       _{i + \relof} & = & \col{a\_hi} \\
+			\mxpComputationArgOneLo       _{i + \relof} & = & \col{a\_lo} \\
+			\mxpComputationArgTwoHi       _{i + \relof} & = & \col{b\_hi} \\
+			\mxpComputationArgTwoLo       _{i + \relof} & = & \col{b\_lo} \\
+		\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}
+			\mxpComputationWcpFlag        _{i + \relof} & = & \rOne       \\
+			\mxpComputationExoInst        _{i + \relof} & = & \inst{LEQ}  \\
+			\mxpComputationArgOneHi       _{i + \relof} & = & \col{a\_hi} \\
+			\mxpComputationArgOneLo       _{i + \relof} & = & \col{a\_lo} \\
+			\mxpComputationArgTwoHi       _{i + \relof} & = & \col{b\_hi} \\
+			\mxpComputationArgTwoLo       _{i + \relof} & = & \col{b\_lo} \\
+		\end{array} \right. \vspace{2mm} \\
+		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+		\wcpCallToIszero  {
+			anchorRow = i           ,
+			relOffset = \relof      ,
+			argOneHi  = \col{a\_hi} ,
+			argOneLo  = \col{a\_lo} ,
+		} & \define &
+		\left\{ \begin{array}{lcl}
+			\mxpComputationWcpFlag        _{i + \relof} & = & \rOne          \\
+			\mxpComputationExoInst        _{i + \relof} & = & \inst{ISZERO}  \\
+			\mxpComputationArgOneHi       _{i + \relof} & = & \col{a\_hi}    \\
+			\mxpComputationArgOneLo       _{i + \relof} & = & \col{a\_lo}    \\
+			\mxpComputationArgTwoHi       _{i + \relof} & = & 0              \\
+			\mxpComputationArgTwoLo       _{i + \relof} & = & 0              \\
+		\end{array} \right. \vspace{2mm} \\
+		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+		\eucCall {
+			anchorRow = i       ,
+			relOffset = \relof  ,
+			argOne    = \col{a} ,
+			argTwo    = \col{b} ,
+		} & \define &
+		\left\{ \begin{array}{lcl}
+			\mxpComputationEucFlag        _{i + \relof} & = & \rOne   \\
+			\mxpComputationArgOneLo       _{i + \relof} & = & \col{a} \\
+			\mxpComputationArgTwoLo       _{i + \relof} & = & \col{b} \\
+		\end{array} \right. \\
+		% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+		% \multicolumn{3}{l}{
+		% 	\resultMustBeTrue {
+		% 		anchorRow = i      ,
+		% 		relOffset = \relof ,
+		% 	} \define \mxpMacroRes _{i + \relof} = \redm{1}
+		% } \\
+	\end{array} \right.
+\]
+\saNote{}
+When using these constraints, one must make sure that the row index $i+\relof$ is that of a computation row. 

mxp_v3/columns/computation/columns.tex

@@ -0,0 +1,35 @@
+The following columns are used in the lookups
+$\mxpMod \hookrightarrow \wcpMod$ and
+$\mxpMod \hookrightarrow \eucMod$, see
+section~(\ref{mxp: lookups: wcp}) and
+section~(\ref{mxp: lookups: euc}) respectively.
+\begin{enumerate}
+	\item
+		$\mxpComputationWcpFlag$:
+		binary column triggering the lookup to the \wcpMod{} module;
+	\item
+		$\mxpComputationEucFlag$:
+		binary column triggering the lookup to the \eucMod{} module;
+	\item
+		$\mxpComputationExoInst$:
+		instruction column for either lookup;
+\end{enumerate}
+The following columns are argument and result columns for these lookups
+\begin{multicols}{3}
+	\begin{enumerate}[resume]
+		\item
+			$\mxpComputationArgOneHi$
+		\item
+			$\mxpComputationArgOneLo$
+		\item
+			$\mxpComputationArgTwoHi$
+		\item
+			$\mxpComputationArgTwoLo$
+		\item
+			$\mxpComputationResA$
+		\item
+			$\mxpComputationResB$
+	\end{enumerate}
+\end{multicols}
+\saNote{}
+Only the lookup to the \eucMod{} module requires two result columns.

mxp_v3/columns/decoder.tex

@@ -0,0 +1,36 @@
+\begin{enumerate}
+	\item $\mxpDecoderInst$:
+		byte column containing an opcode;
+	\item $\mxpDecoderIsMsize$:
+		binary column;
+		lights up precisely for the \inst{MSIZE} instruction;
+	\item $\mxpDecoderIsReturn$:
+		binary column;
+		lights up precisely for the \inst{RETURN} instruction;
+	\item $\mxpDecoderIsMcopy$:
+		binary column;
+		lights up precisely for the \inst{MCOPY} instruction;
+	\item $\mxpDecoderIsFixedSizeThirtyTwo$:
+		binary column;
+		lights up precisely for \inst{MLOAD} and \inst{MSTORE};
+	\item $\mxpDecoderIsFixedSizeOne$:
+		binary column;
+		lights up precisely for \inst{MSTORE8};
+	\item $\mxpDecoderIsSingleMaxOffset$:
+		binary column;
+		lights up precisely for instructions producing a single ``max offset'' in memory;
+	\item $\mxpDecoderIsDoubleMaxOffset$:
+		binary column;
+		lights up precisely for instructions producing two ``max offsets'' in memory;
+		these are the \inst{CALL}-type instructions and \inst{MCOPY};
+	\item $\mxpDecoderIsWordPricing$:
+		binary column;
+		lights up precisely for the instructions which feature a linear-in-words extra cost on top of the memory expansion cost proper;
+	\item $\mxpDecoderIsBytePricing$:
+		binary column;
+		lights up precisely for the instructions which feature a linear-in-bytes extra cost on top of the memory expansion cost proper;
+	\item $\mxpDecoderGWord$:
+		contains a ``cost per \evm{} word'' applicable to the instruction;
+	\item $\mxpDecoderGByte$:
+		contains a ``cost per \evm{} byte'' applicable to the instruction;
+\end{enumerate}