Skip to content

Commit a3a00be

Browse files
lorenzogentile404lorenzogentile404
authored
Arithmetization of MXP redesign (#103)
1 parent 7a5f25a commit a3a00be

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

60 files changed

+2464
-3
lines changed

Diff for: ‎Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ mmio: view-mmio
2929
modexp: view-modexp_data
3030
mmu: view-mmu
3131
mxp: view-mxp
32+
mxp_v3: view-mxp_v3
3233
oob: view-oob
3334
prc: view-prc
3435
rlp_addr: view-rlp_addr
@@ -64,6 +65,7 @@ rmmio: recompile-mmio
6465
rmodexp: recompile-modexp_data
6566
rmmu: recompile-mmu
6667
rmxp: recompile-mxp
68+
rmxp_v3: recompile-mxp_v3
6769
roob: recompile-oob
6870
rprc: recompile-prc
6971
rrlp_addr: recompile-rlp_addr

Diff for: ‎mxp_v3/_all_mxp_v3.tex

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
\documentclass[fleqn]{article}
2+
\usepackage[dvipsnames]{xcolor}
3+
\usepackage{xkeyval}
4+
\usepackage{../pkg/common}
5+
%\usepackage{../pkg/dark_theme}
6+
\usepackage{../pkg/std}
7+
\usepackage{../pkg/IEEEtrantools}
8+
\usepackage{../pkg/rom}
9+
\usepackage{../pkg/env}
10+
\usepackage{../pkg/euc}
11+
\usepackage{../pkg/ram}
12+
\usepackage{../pkg/wc3}
13+
\usepackage{../pkg/stack}
14+
\usepackage{../pkg/call_stack}
15+
\usepackage{../pkg/access}
16+
\usepackage{../pkg/expansion}
17+
\usepackage{../pkg/thm_env}
18+
\usepackage{../pkg/offset_processor}
19+
\usepackage{../pkg/flags_stamps_selectors}
20+
\usepackage{../pkg/instruction_flags}
21+
\usepackage{../pkg/exceptions}
22+
\usepackage{../pkg/draculatheme}
23+
\usepackage{../pkg/xkeyval_macros/wcp_calls}
24+
\usepackage{../pkg/xkeyval_macros/euc_calls}
25+
26+
\usepackage{../pkg/draculatheme}
27+
28+
\title{Memory expansion module}
29+
\author{Rollup team}
30+
\date{August 2022}
31+
32+
\begin{document}
33+
34+
\maketitle
35+
\tableofcontents
36+
37+
\input{_inputs}
38+
39+
\end{document}

Diff for: ‎mxp_v3/_inputs.tex

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
\input{_local}
2+
3+
\section{Introduction \lispNone{}} \label{mxp: intro} \input{intro}
4+
\section{Instruction decoder \lispNone{}} \label{mxp: instruction decoder} \input{instruction_decoder_representation}
5+
\section{\hubMod{} / \mxpMod{} interface \lispNone{}} \label{mxp: hub mxp interface} \input{hub_mxp_interface}
6+
\section{Columns \lispDone{}} \label{mxp: columns} \input{columns/_inputs}
7+
\section{Generalities \lispDone{}} \label{mxp: generalities} \input{generalities/_inputs}
8+
\section{Computations \lispTodo{}} \label{mxp: computations} \input{computations/_inputs}
9+
\section{Consistency \lispTodo{}} \label{mxp: consistency} \input{consistency/_inputs}
10+
\section{Lookups \lispTodo{}} \label{mxp: lookups} \input{lookups/_inputs}

Diff for: ‎mxp_v3/_local.tex

+95
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
\def\rOne {\redm{1}}
2+
\def\locPerspectiveSum {\col{persp\_sum}}
3+
\def\locWeightSum {\col{persp\_wght\_sum}}
4+
\def\locCtMaxSum {\col{ct\_max\_sum}}
5+
\def\locStampIncrement {\col{stamp\_increment}}
6+
\def\locScenarioSum {\mxpScenarioColumn{scenario\_sum}}
7+
\def\locMxpScenarioNotMsize {\mxpScenarioColumn{not\_msize}}
8+
\def\locMxpScenarioNotMsizeNorTrivial {\mxpScenarioColumn{not\_msize\_nor\_trivial}}
9+
\def\locMxpScenarioStateUpdate {\mxpScenarioColumn{state\_update}}
10+
\def\locMxpScenarioNoStateUpdate {\mxpScenarioColumn{no\_state\_update}}
11+
12+
\def\locCtMaxMsize {\yellowm{1}} \def\locCtMaxMsizeName {\yellowm{{\texttt{CT\_MAX\_MSIZE}}}}
13+
\def\locCtMaxTrivialOperation {\yellowm{2}} \def\locCtMaxTrivialOperationName {\yellowm{{\texttt{CT\_MAX\_TRIV}}}}
14+
\def\locCtMaxMxpx {\yellowm{6}} \def\locCtMaxMxpxName {\yellowm{{\texttt{CT\_MAX\_MXPX}}}}
15+
\def\locCtMaxStateUpdateWordPricing {\yellowm{10}} \def\locCtMaxStateUpdateWordPricingName {\yellowm{{\texttt{CT\_MAX\_UPDT\_W}}}}
16+
\def\locCtMaxStateUpdateBytePricing {\yellowm{11}} \def\locCtMaxStateUpdateBytePricingName {\yellowm{{\texttt{CT\_MAX\_UPDT\_B}}}}
17+
% \def\locCtMaxSingleMaxOffsetAndWordPricing {\yellowm{4}} \def\locCtMaxSingleMaxOffsetAndWordPricingName {\yellowm{{\texttt{ct\_max\_1offw}}}}
18+
% \def\locCtMaxSingleMaxOffsetAndBytePricing {\yellowm{5}} \def\locCtMaxSingleMaxOffsetAndBytePricingName {\yellowm{{\texttt{ct\_max\_1offb}}}}
19+
% \def\locCtMaxDoubleMaxOffsetAndWordPricing {\yellowm{6}} \def\locCtMaxDoubleMaxOffsetAndWordPricingName {\yellowm{{\texttt{ct\_max\_2offw}}}}
20+
% \def\locCtMaxDoubleMaxOffsetAndBytePricing {\yellowm{7}} \def\locCtMaxDoubleMaxOffsetAndBytePricingName {\yellowm{{\texttt{ct\_max\_2offb}}}}
21+
22+
\def\locDecoderToMacroRowOffset {\yellowm{1}} \def\locMacroToDecoderRowOffset {\locDecoderToMacroRowOffset}
23+
\def\locMacroToScenarioRowOffset {\yellowm{1}} \def\locScenarioToMacroRowOffset {\locMacroToScenarioRowOffset}
24+
\def\locDecoderToScenarioRowOffset {\yellowm{2}} \def\locScenarioToDecoderRowOffset {\locDecoderToScenarioRowOffset}
25+
26+
\def\locOffsetOneHi {\col{offset\_1\_hi}}
27+
\def\locOffsetOneLo {\col{offset\_1\_lo}}
28+
\def\locSizeOneHi {\col{size\_1\_hi}}
29+
\def\locSizeOneLo {\col{size\_1\_lo}}
30+
31+
\def\locOffsetTwoHi {\col{offset\_2\_hi}}
32+
\def\locOffsetTwoLo {\col{offset\_2\_lo}}
33+
\def\locSizeTwoHi {\col{size\_2\_hi}}
34+
\def\locSizeTwoLo {\col{size\_2\_lo}}
35+
36+
\def\locSizeOneIsZero {\col{size\_1\_is\_zero}}
37+
\def\locSizeOneIsNonZero {\col{size\_1\_is\_nonzero}}
38+
39+
\def\locSizeTwoIsZero {\col{size\_2\_is\_zero}}
40+
\def\locSizeTwoIsNonZero {\col{size\_2\_is\_nonzero}}
41+
42+
\def\locSizeOneIsSmall {\col{size\_1\_is\_small}}
43+
\def\locSizeOneIsLarge {\col{size\_1\_is\_large}}
44+
45+
\def\locSizeTwoIsSmall {\col{size\_2\_is\_small}}
46+
\def\locSizeTwoIsLarge {\col{size\_2\_is\_large}}
47+
48+
\def\locOffsetOneIsSmall {\col{offset\_1\_is\_small}}
49+
\def\locOffsetOneIsLarge {\col{offset\_1\_is\_large}}
50+
51+
\def\locOffsetTwoIsSmall {\col{offset\_2\_is\_small}}
52+
\def\locOffsetTwoIsLarge {\col{offset\_2\_is\_large}}
53+
54+
\def\locMxpComputationMxpxExpressionOne {\col{mxpx\_expression\_1}}
55+
\def\locMxpComputationMxpxExpressionTwo {\col{mxpx\_expression\_2}}
56+
\def\locMxpComputationMxpxExpression {\col{mxpx\_expression}}
57+
58+
\def\locMaxOffset {\col{max\_offset}}
59+
60+
\def\locMaxOne {\col{max\_1}}
61+
\def\locMaxTwo {\col{max\_2}}
62+
\def\locMaxOffsetOne {\col{max\_offset\_1}}
63+
\def\locMaxOffsetTwo {\col{max\_offset\_2}}
64+
65+
\def\locUseParameterSetOne {\col{use\_params\_1}}
66+
\def\locUseParameterSetTwo {\col{use\_params\_2}}
67+
68+
\def\locDoubleOffsetOpcode {\col{double\_offset}}
69+
\def\locSingleOffsetOpcode {\col{single\_offset}}
70+
\def\locWordPricingOpcode {\col{word\_pricing}}
71+
\def\locBytePricingOpcode {\col{byte\_pricing}}
72+
\def\locNumberOfWords {\col{number\_of\_words}}
73+
\def\locNumberOfBytes {\col{number\_of\_bytes}}
74+
\def\locWordPrice {\col{gas\_per\_word}}
75+
\def\locBytePrice {\col{gas\_per\_byte}}
76+
\def\locExtraWordCost {\col{extra\_word\_cost}}
77+
\def\locExtraByteCost {\col{extra\_byte\_cost}}
78+
79+
\def\locFloor {\col{floor}}
80+
\def\locEypA {\col{EYP\_a}}
81+
\def\locQuadraticPart {\col{quadratic\_part}}
82+
\def\locCmemQuadPart {\col{cmem\_quad\_part}}
83+
\def\locCmemLinrPart {\col{cmem\_linear\_part}}
84+
\def\locUpdateInternalState {\col{update\_internal\_state}}
85+
\def\locWords {\col{words}}
86+
87+
\def\locSizeOne {\col{size\_1}}
88+
\def\locCeil {\col{ceil}}
89+
90+
\def\locCompRequired {\col{comp\_required}}
91+
\def\locComp {\col{comp}}
92+
93+
\def\locMxpxExpressionOne {\col{mxpx\_expression\_1}}
94+
\def\locMxpxExpressionTwo {\col{mxpx\_expression\_2}}
95+
\def\locMxpxExpression {\col{mxpx\_expression}}

Diff for: ‎mxp_v3/columns/_inputs.tex

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
\subsection{Common columns \lispDone{}} \label{mxp: columns: common} \input{columns/common}
2+
\subsection{Instruction decoder columns \lispDone{}} \label{mxp: columns: instruction decoder} \input{columns/decoder}
3+
\subsection{Macro instruction columns \lispDone{}} \label{mxp: columns: macro instruction} \input{columns/macro}
4+
\subsection{Scenario columns \lispDone{}} \label{mxp: columns: scenario} \input{columns/scenario/_inputs}
5+
\subsection{Computation columns \lispDone{}} \label{mxp: columns: computation} \input{columns/computation/_inputs}

Diff for: ‎mxp_v3/columns/common.tex

+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
We introduce a stamp column as well as various perspective columns.
2+
We shall also require counter columns.
3+
\begin{enumerate}
4+
\item $\mxpStamp$:
5+
stamp column for the \mxpMod{} module;
6+
\item $\mxpContextNumber$:
7+
stamp-constant column containing the relevant context number;
8+
\item $\isMxpInstructionDecoder$:
9+
binary column;
10+
\item $\isMxpMacro$
11+
binary column;
12+
\item $\isMxpScenario$:
13+
binary column; contains a prediction as to the nature of the operation and the required computations;
14+
\item $\isMxpComputation$:
15+
binary column;
16+
\item $\ct$:
17+
counter column;
18+
\item $\maxCt$:
19+
max counter value;
20+
perspective and scenario dependent.
21+
\end{enumerate}
22+
We introduce the following nomenclature:
23+
rows where
24+
$\isMxpInstructionDecoder \equiv \rOne$ will be called \textbf{decoding-rows},
25+
$\isMxpMacro \equiv \rOne$ will be called \textbf{macro-instruction-rows},
26+
$\isMxpScenario \equiv \rOne$ will be called \textbf{scenario-rows} and
27+
$\isMxpComputation \equiv \rOne$ will be called \textbf{computation-rows}.

Diff for: ‎mxp_v3/columns/computation/_inputs.tex

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

Diff for: ‎mxp_v3/columns/computation/calls.tex

+75
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
We define several simple constraint systems to simplify the writing of constraints.
2+
\[
3+
\left\{ \begin{array}{lcl}
4+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5+
\wcpCallToLt {
6+
anchorRow = i ,
7+
relOffset = \relof ,
8+
argOneHi = \col{a\_hi} ,
9+
argOneLo = \col{a\_lo} ,
10+
argTwoHi = \col{b\_hi} ,
11+
argTwoLo = \col{b\_lo} ,
12+
} & \define &
13+
\left\{ \begin{array}{lcl}
14+
\mxpComputationWcpFlag _{i + \relof} & = & \rOne \\
15+
\mxpComputationExoInst _{i + \relof} & = & \inst{LT} \\
16+
\mxpComputationArgOneHi _{i + \relof} & = & \col{a\_hi} \\
17+
\mxpComputationArgOneLo _{i + \relof} & = & \col{a\_lo} \\
18+
\mxpComputationArgTwoHi _{i + \relof} & = & \col{b\_hi} \\
19+
\mxpComputationArgTwoLo _{i + \relof} & = & \col{b\_lo} \\
20+
\end{array} \right. \vspace{2mm} \\
21+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
22+
\wcpCallToLeq {
23+
anchorRow = i ,
24+
relOffset = \relof ,
25+
argOneHi = \col{a\_hi} ,
26+
argOneLo = \col{a\_lo} ,
27+
argTwoHi = \col{b\_hi} ,
28+
argTwoLo = \col{b\_lo} ,
29+
} & \define &
30+
\left\{ \begin{array}{lcl}
31+
\mxpComputationWcpFlag _{i + \relof} & = & \rOne \\
32+
\mxpComputationExoInst _{i + \relof} & = & \inst{LEQ} \\
33+
\mxpComputationArgOneHi _{i + \relof} & = & \col{a\_hi} \\
34+
\mxpComputationArgOneLo _{i + \relof} & = & \col{a\_lo} \\
35+
\mxpComputationArgTwoHi _{i + \relof} & = & \col{b\_hi} \\
36+
\mxpComputationArgTwoLo _{i + \relof} & = & \col{b\_lo} \\
37+
\end{array} \right. \vspace{2mm} \\
38+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
39+
\wcpCallToIszero {
40+
anchorRow = i ,
41+
relOffset = \relof ,
42+
argOneHi = \col{a\_hi} ,
43+
argOneLo = \col{a\_lo} ,
44+
} & \define &
45+
\left\{ \begin{array}{lcl}
46+
\mxpComputationWcpFlag _{i + \relof} & = & \rOne \\
47+
\mxpComputationExoInst _{i + \relof} & = & \inst{ISZERO} \\
48+
\mxpComputationArgOneHi _{i + \relof} & = & \col{a\_hi} \\
49+
\mxpComputationArgOneLo _{i + \relof} & = & \col{a\_lo} \\
50+
\mxpComputationArgTwoHi _{i + \relof} & = & 0 \\
51+
\mxpComputationArgTwoLo _{i + \relof} & = & 0 \\
52+
\end{array} \right. \vspace{2mm} \\
53+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54+
\eucCall {
55+
anchorRow = i ,
56+
relOffset = \relof ,
57+
argOne = \col{a} ,
58+
argTwo = \col{b} ,
59+
} & \define &
60+
\left\{ \begin{array}{lcl}
61+
\mxpComputationEucFlag _{i + \relof} & = & \rOne \\
62+
\mxpComputationArgOneLo _{i + \relof} & = & \col{a} \\
63+
\mxpComputationArgTwoLo _{i + \relof} & = & \col{b} \\
64+
\end{array} \right. \\
65+
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
66+
% \multicolumn{3}{l}{
67+
% \resultMustBeTrue {
68+
% anchorRow = i ,
69+
% relOffset = \relof ,
70+
% } \define \mxpMacroRes _{i + \relof} = \redm{1}
71+
% } \\
72+
\end{array} \right.
73+
\]
74+
\saNote{}
75+
When using these constraints, one must make sure that the row index $i+\relof$ is that of a computation row.

Diff for: ‎mxp_v3/columns/computation/columns.tex

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
The following columns are used in the lookups
2+
$\mxpMod \hookrightarrow \wcpMod$ and
3+
$\mxpMod \hookrightarrow \eucMod$, see
4+
section~(\ref{mxp: lookups: wcp}) and
5+
section~(\ref{mxp: lookups: euc}) respectively.
6+
\begin{enumerate}
7+
\item
8+
$\mxpComputationWcpFlag$:
9+
binary column triggering the lookup to the \wcpMod{} module;
10+
\item
11+
$\mxpComputationEucFlag$:
12+
binary column triggering the lookup to the \eucMod{} module;
13+
\item
14+
$\mxpComputationExoInst$:
15+
instruction column for either lookup;
16+
\end{enumerate}
17+
The following columns are argument and result columns for these lookups
18+
\begin{multicols}{3}
19+
\begin{enumerate}[resume]
20+
\item
21+
$\mxpComputationArgOneHi$
22+
\item
23+
$\mxpComputationArgOneLo$
24+
\item
25+
$\mxpComputationArgTwoHi$
26+
\item
27+
$\mxpComputationArgTwoLo$
28+
\item
29+
$\mxpComputationResA$
30+
\item
31+
$\mxpComputationResB$
32+
\end{enumerate}
33+
\end{multicols}
34+
\saNote{}
35+
Only the lookup to the \eucMod{} module requires two result columns.

Diff for: ‎mxp_v3/columns/decoder.tex

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
\begin{enumerate}
2+
\item $\mxpDecoderInst$:
3+
byte column containing an opcode;
4+
\item $\mxpDecoderIsMsize$:
5+
binary column;
6+
lights up precisely for the \inst{MSIZE} instruction;
7+
\item $\mxpDecoderIsReturn$:
8+
binary column;
9+
lights up precisely for the \inst{RETURN} instruction;
10+
\item $\mxpDecoderIsMcopy$:
11+
binary column;
12+
lights up precisely for the \inst{MCOPY} instruction;
13+
\item $\mxpDecoderIsFixedSizeThirtyTwo$:
14+
binary column;
15+
lights up precisely for \inst{MLOAD} and \inst{MSTORE};
16+
\item $\mxpDecoderIsFixedSizeOne$:
17+
binary column;
18+
lights up precisely for \inst{MSTORE8};
19+
\item $\mxpDecoderIsSingleMaxOffset$:
20+
binary column;
21+
lights up precisely for instructions producing a single ``max offset'' in memory;
22+
\item $\mxpDecoderIsDoubleMaxOffset$:
23+
binary column;
24+
lights up precisely for instructions producing two ``max offsets'' in memory;
25+
these are the \inst{CALL}-type instructions and \inst{MCOPY};
26+
\item $\mxpDecoderIsWordPricing$:
27+
binary column;
28+
lights up precisely for the instructions which feature a linear-in-words extra cost on top of the memory expansion cost proper;
29+
\item $\mxpDecoderIsBytePricing$:
30+
binary column;
31+
lights up precisely for the instructions which feature a linear-in-bytes extra cost on top of the memory expansion cost proper;
32+
\item $\mxpDecoderGWord$:
33+
contains a ``cost per \evm{} word'' applicable to the instruction;
34+
\item $\mxpDecoderGByte$:
35+
contains a ``cost per \evm{} byte'' applicable to the instruction;
36+
\end{enumerate}

0 commit comments

Comments
 (0)