Skip to content

Commit 0ffcd01

Browse files
OlivierBBBOlivierBBB
authored
EIP-5656: MCOPY - Memory copying instruction (#140)
1 parent 65797a0 commit 0ffcd01

25 files changed

+539
-121
lines changed

‎_notes/EIP-5656: MCOPY - Memory copying instruction.md

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
# Tasks
2+
3+
## HUB module
4+
5+
- new `(3,0)-stack-pattern`
6+
- new MXP instruction macro for the HUB's misc/ perspective
7+
- new instruction family ? YES, for simplicity. Alternatively we could expand the `KEC` family.
8+
- processing (assuming no `SUX`)
9+
- unconditionally impose `PEEK_AT_MISC[i + 1] ≡ 1` and fill the `MXP_INST`
10+
- we will have
11+
```rust
12+
trigger_MXP ≡ 1
13+
trigger_MMU ≡ (1 - XAHOY) ∙ S1NZNOMXPX
14+
```
15+
- both for `MXPX ≡ 1` and `OOGX ≡ 1`
16+
```rust
17+
STACK // already accounted for
18+
MISC
19+
(CON) // automatic
20+
```
21+
- `XAHOY ≡ 0` ∧ `trigger_MMU ≡ 0`
22+
```rust
23+
STACK // already accounted for
24+
MISC
25+
```
26+
- `XAHOY ≡ 0` ∧ `trigger_MMU ≡ 1`
27+
```rust
28+
STACK // already accounted for
29+
MISC
30+
MISC
31+
```
32+
33+
## MXP module
34+
35+
- `MCOPY` supported as of [MXP redesign #60](https://github.com/Consensys/linea-specification/issues/60)

‎hub/instruction_handling/_inputs.tex

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ \subsection{Instructions raising the $\stackDecShfFlag$ \lispDone{}}
1313
\subsection{Instructions raising the $\stackDecWcpFlag$ \lispDone{}} \label{hub: instruction handling: wcp} \input{instruction_handling/wcp}
1414
\subsection{Constraints for the preceding instruction families \lispDone{}} \label{hub: instruction handling: stateless constraints} \input{instruction_handling/stateless_constraints}
1515
\subsection{Instructions raising the $\stackDecKecFlag$ \lispDone{}} \label{hub: instruction handling: kec} \input{instruction_handling/kec}
16+
\subsection{Instructions raising the $\stackDecMcopyFlag$ \lispTodo{}} \label{hub: instruction handling: mcopy} \input{instruction_handling/mcopy/_inputs}
1617
\subsection{Instructions raising the $\stackDecConFlag$ \lispDone{}} \label{hub: instruction handling: con} \input{instruction_handling/context/_inputs}
1718
\subsection{Instructions raising the $\stackDecAccFlag$ \lispDone{}} \label{hub: instruction handling: acc} \input{instruction_handling/account/_inputs}
1819
\subsection{Instructions raising the $\stackDecCopyFlag$ \lispDone{}} \label{hub: instruction handling: copy} \input{instruction_handling/copy/_inputs}

‎hub/instruction_handling/kec.tex

Lines changed: 1 addition & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -117,57 +117,13 @@ \subsubsection{Constraints}
117117
exoSum = \exoWeightKec ,
118118
phase = \nothing ,
119119
}
120-
% \setMmuInstructionParametersRamToExoWithPadding {i}{\miscRowOffset}
121-
% \left[ \begin{array}{ll}
122-
% \utt{Source ID:} & \cn_{i} \\
123-
% \utt{Target ID:} & \nothing \\
124-
% \utt{Auxiliary ID:} & 1 + \hubStamp_{i} \\
125-
% % \utt{Source offset high:} & \col{src\_offset\_hi} \\
126-
% \utt{Source offset low:} & \locOffsetLo \\
127-
% % \utt{Target offset low:} & \col{tgt\_offset\_lo} \\
128-
% \utt{Size:} & \locSizeLo \\
129-
% % \utt{Reference offset:} & \col{ref\_offset} \\
130-
% \utt{Reference size:} & \locSizeLo \\
131-
% \utt{Success bit:} & \nothing \\
132-
% % \utt{Limb one:} & \col{limb\_1} \\
133-
% % \utt{Limb two:} & \col{limb\_2} \\
134-
% \utt{Exo sum:} & \exoWeightKec \\
135-
% \utt{Phase:} & \nothing \\
136-
% \end{array} \right]
137120
\]
138-
% \[
139-
% \left\{ \begin{array}{lclr}
140-
% \miscMmuFlag _{i + \miscRowOffset} & = & \one & (\trash) \vspace{2mm} \\
141-
% \miscMmuInst _{i + \miscRowOffset} & = & \locInst \\
142-
% \miscMmuInstParamOne _{i + \miscRowOffset} & = & \hashInfoStamp_{i} \\
143-
% \miscMmuInstParamTwo _{i + \miscRowOffset} & = & 0 & (\trash) \\
144-
% % \miscMmuReturner _{i + \miscRowOffset} & = & 0 & (\trash) \\
145-
% \miscMmuInfo _{i + \miscRowOffset} & = & 0 \\
146-
% \miscMmuRefOffset _{i + \miscRowOffset} & = & 0 \\
147-
% \miscMmuRefSize _{i + \miscRowOffset} & = & 0 \\
148-
% \miscMmuOffsetOneLo _{i + \miscRowOffset} & = & \locOffsetLo \\
149-
% \miscMmuOffsetTwoHi _{i + \miscRowOffset} & = & 0 & (\trash) \\
150-
% \miscMmuOffsetTwoLo _{i + \miscRowOffset} & = & 0 & (\trash) \\
151-
% \miscMmuSize _{i + \miscRowOffset} & = & \locSizeLo \\
152-
% \miscMmuStackValHi _{i + \miscRowOffset} & = & 0 & (\trash) \\
153-
% \miscMmuStackValLo _{i + \miscRowOffset} & = & 0 & (\trash) \\
154-
% \miscMmuExoSum _{i + \miscRowOffset} & = & \ob{TODO!} \\
155-
% \end{array} \right.
156-
% \]
157-
\saNote{} The current context and caller context (which may own the call data) are provided by the lookup.
158-
159-
\saNote{} We are providing extra information to the \mmuMod{} in case of a \inst{CALLDATALOAD}:
160-
(\emph{a})
161-
the knowledge whether the current execution context is the root context
162-
(\emph{b})
163-
the absolute transaction number.
164-
The purpose of the former is to be able to retrieve the \textbf{transaction call data} whenever we are executing a \inst{CALLDATALOAD} in the root context of a transaction.
165121
\item[\underline{Justifying the \mxpxSH{}:}]
166122
we impose that $\stackMxpx_{i} = \locMxpx$
167123
\item[\underline{Setting the gas cost:}]
168124
we impose that
169125
\begin{enumerate}
170-
\item \If $\locMxpx = 0$ \Then \( \gasCost_{i} = \decStaticGas_{i} + \locMxpGas \)
126+
\item \If $\locMxpx = 0$ \Then \( \gasCost_{i} = \stackStaticGas _{i} + \locMxpGas \)
171127
\item \If $\locMxpx = 1$ \Then \( \gasCost_{i} = 0 \)
172128
\end{enumerate}
173129
\item[\underline{Constraining \stackHashInfoFlag{}:}] we impose $\stackHashInfoFlag_{i} = \locCallMmu$;
@@ -186,7 +142,6 @@ \subsubsection{Constraints}
186142
\left\{ \begin{array}{lclr}
187143
\locKeccakHi & = & \stackHashInfoValHi_{i} \\
188144
\locKeccakLo & = & \stackHashInfoValLo_{i} \\
189-
% \locSizeLo & = & \stackHashInfoSize_{i} \\
190145
\end{array} \right.
191146
\]
192147
\end{enumerate}

‎hub/instruction_handling/mcopy/_inputs.tex

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
\input{instruction_handling/mcopy/_local}
2+
\subsubsection{Supported instructions and flags \lispTodo{}} \label{hub: instruction handling: mcopy: instructions and flags} \input{instruction_handling/mcopy/instructions_and_flags}
3+
\subsubsection{Shorthands \lispTodo{}} \label{hub: instruction handling: mcopy: shorthands} \input{instruction_handling/mcopy/shorthands}
4+
\subsubsection{Constraints \lispTodo{}} \label{hub: instruction handling: mcopy: constraints} \input{instruction_handling/mcopy/constraints}
5+

‎hub/instruction_handling/mcopy/_local.tex

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
\def\locMcopyFrstMiscOffset {\yellowm{1}}
2+
\def\locMcopyScndMiscOffset {\yellowm{2}}
3+
\def\locMcopyExceptionalContextOffset {\yellowm{2}}
4+
5+
\def\locTriggerMxp {\col{trigger\_MXP}}
6+
\def\locTriggerMmu {\col{trigger\_MMU}}
7+
8+
\def\locSrcOffsetHi {\col{src\_offset\_hi}}
9+
\def\locSrcOffsetLo {\col{src\_offset\_lo}}
10+
\def\locTgtOffsetHi {\col{tgt\_offset\_hi}}
11+
\def\locTgtOffsetLo {\col{tgt\_offset\_lo}}
12+
13+
\def\locMcopyMxpGas {\col{gas\_mxp}}
14+
\def\locMcopyMxpSizeOneNonZeroNoMxpx {\col{s1nznomxpx}}
15+
\def\locMcopyMxpMxpx {\col{mxpx}}

‎hub/instruction_handling/mcopy/constraints.tex

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
1+
\begin{center}
2+
\boxed{%
3+
\text{The stack constraints presented below assume }
4+
\begin{cases}
5+
\peekStack _{i} = 1 \\
6+
\stackDecMcopyFlag _{i} = 1 \\
7+
\stackSux _{i} + \stackSox _{i} = 0 \\
8+
\end{cases}}
9+
\end{center}
10+
The constraints are as follows:
11+
\begin{description}
12+
\item[\underline{Setting the stack pattern:}]
13+
we impose $\threeZeroSP_{i}$;
14+
\end{description}
15+
We deal with the \inst{MCOPY} instruction slightly differently from other instructions.
16+
The typical \emph{modus operandi} is to specify peeking flags and then to fill the relevant lookups etc\dots{}
17+
With the present instruction we begin by specifying a single miscellaneous-row which is unconditionally present.
18+
\begin{description}
19+
\item[\underline{The first row must be a miscellaneous-row:}]
20+
we unconditionally impose that $\peekMisc _{i + \locMcopyFrstMiscOffset} = 1$;
21+
\item[\underline{Calling the \mxpMod{}-module:}]
22+
we unconditionally call the \mxpMod{} module
23+
$\miscMxpFlag _{i + \locMcopyFrstMiscOffset} = 1$;
24+
\item[\underline{Defining the \mxpMod{}-instruction:}]
25+
we impose
26+
\[
27+
\setMxpInstructionMcopy {
28+
anchorRow = i ,
29+
relOffset = \locMcopyFrstMiscOffset ,
30+
targetOffsetHi = \locTgtOffsetHi ,
31+
targetOffsetLo = \locTgtOffsetLo ,
32+
sourceOffsetHi = \locSrcOffsetHi ,
33+
sourceOffsetLo = \locSrcOffsetLo ,
34+
sizeHi = \locSizeHi ,
35+
sizeLo = \locSizeLo ,
36+
}
37+
\]
38+
\item[\underline{Defining module triggers:}]
39+
the module triggers will be used to
40+
unconditionally call the \mxpMod{} module
41+
and call the \mmuMod{} module \emph{iff}
42+
the underlying \inst{MCOPY} instruction is unexceptional ($\xAhoy \equiv 0$)
43+
and its size parameter is nonzero ($\locMcopyMxpSizeOneNonZeroNoMxpx \equiv 1$.)
44+
\[
45+
\left\{ \begin{array}{lcl}
46+
\locTriggerMxp & \define & 1 \\
47+
\locTriggerMmu & \define & (1 - \xAhoy _{i}) \cdot \locMcopyMxpSizeOneNonZeroNoMxpx \\
48+
\end{array} \right.
49+
\]
50+
In other words
51+
\begin{enumerate}
52+
\item \If $\xAhoy_{i} = 1$ \Then $\locTriggerMmu = 0$ \quad (\trash)
53+
\item \If $\xAhoy_{i} = 0$ \Then
54+
\begin{enumerate}
55+
\item \If $\locSizeLo = 0$ \Then $\locTriggerMmu = 0$ \quad (\trash)
56+
\item \If $\locSizeLo \neq 0$ \Then $\locTriggerMmu = 1$ \quad (\trash)
57+
\end{enumerate}
58+
\end{enumerate}
59+
\end{description}
60+
We are now in a position to specify the peeking flags.
61+
\begin{description}
62+
\item[\underline{Setting $\nonStackRows$ and peeking flags:}]
63+
we impose that
64+
\begin{enumerate}
65+
\item \If $\xAhoy _{i} = 1$ \Then $\nonStackRows_{i} = 2$.
66+
\item \If $\xAhoy _{i} = 0$ \Then $\nonStackRows_{i} = 1 + \locTriggerMmu$.
67+
\end{enumerate}
68+
\item[\underline{Setting the peeking flags:}]
69+
we impose that
70+
\begin{enumerate}
71+
\item \If $\xAhoy _{i} = 1$ \Then $\nonStackRows_{i} = 2$ and
72+
\[
73+
\left[ \begin{array}{r}
74+
+ \peekMisc _{i + \locMcopyFrstMiscOffset} \\
75+
+ \peekContext _{i + \locMcopyExceptionalContextOffset} \\
76+
\end{array} \right]
77+
= \nonStackRows_{i}
78+
\]
79+
\saNote{}
80+
We don't need to (and won't) specify the contents of the final context row in the case that $\xAhoy \equiv 1$.
81+
This is already implicitly taken care of with
82+
section~(\ref{hub: generalities: context: exceptions lead to providing empty return data}).
83+
84+
\saNote{}
85+
For instructions raising the $\stackDecMcopyFlag$ one has $\cmc \equiv \xAhoy$.
86+
\item \If $\xAhoy _{i} = 0$ \Then $\nonStackRows_{i} = 1 + \locTriggerMmu$ and
87+
\[
88+
\left[ \begin{array}{cr}
89+
+ & \peekMisc _{i + \locMcopyFrstMiscOffset} \\
90+
+ & \locTriggerMmu \cdot \peekMisc _{i + \locMcopyScndMiscOffset} \\
91+
\end{array} \right]
92+
= \nonStackRows_{i}
93+
\]
94+
\end{enumerate}
95+
\item[\underline{Justiyfing the \stackMxpx{} flag:}]
96+
we impose that
97+
\[
98+
\stackMxpx _{i}
99+
=
100+
\locMcopyMxpMxpx
101+
\]
102+
\item[\underline{Setting the gas cost:}]
103+
we impose that
104+
\begin{enumerate}
105+
\item \If $\stackMxpx _{i} = 0$ \Then \( \gasCost_{i} = \stackStaticGas _{i} + \locMcopyMxpGas \)
106+
\item \If $\stackMxpx _{i} = 1$ \Then \( \gasCost_{i} = 0 \)
107+
\end{enumerate}
108+
\item[\underline{Miscellaneous-row $n^°(i + \locMcopyFrstMiscOffset)$: flags:}]
109+
we impose that
110+
\[
111+
\weightedMiscFlagSum {i}{\locMcopyFrstMiscOffset}
112+
=
113+
\left[ \begin{array}{llcl}
114+
+ & \miscMmuWeight & \!\!\!\cdot\!\!\! & \locCallMmu \\
115+
+ & \miscMxpWeight \\
116+
\end{array} \right]
117+
\]
118+
in other words
119+
\[
120+
\left\{ \begin{array}{lclr}
121+
\miscExpFlag _{i + \locMcopyFrstMiscOffset} & = & \gZero & (\trash) \\
122+
\miscMmuFlag _{i + \locMcopyFrstMiscOffset} & = & \locCallMmu & (\trash) \\
123+
\miscMxpFlag _{i + \locMcopyFrstMiscOffset} & = & \one & (\trash) \\
124+
\miscOobFlag _{i + \locMcopyFrstMiscOffset} & = & \gZero & (\trash) \\
125+
\miscStpFlag _{i + \locMcopyFrstMiscOffset} & = & \gZero & (\trash) \\
126+
\end{array} \right.
127+
\]
128+
\item[\underline{Miscellaneous-row $n^°(i + \locMcopyScndMiscOffset)$: flags:}]
129+
\If $\locTriggerMmu = 1$ \Then we impose that
130+
\[
131+
\weightedMiscFlagSum {i}{\locMcopyScndMiscOffset}
132+
=
133+
\miscMmuWeight
134+
\]
135+
in other words
136+
\[
137+
\left\{ \begin{array}{lclr}
138+
\miscExpFlag _{i + \locMcopyScndMiscOffset} & = & \gZero & (\trash) \\
139+
\miscMmuFlag _{i + \locMcopyScndMiscOffset} & = & \one & (\trash) \\
140+
\miscMxpFlag _{i + \locMcopyScndMiscOffset} & = & \gZero & (\trash) \\
141+
\miscOobFlag _{i + \locMcopyScndMiscOffset} & = & \gZero & (\trash) \\
142+
\miscStpFlag _{i + \locMcopyScndMiscOffset} & = & \gZero & (\trash) \\
143+
\end{array} \right.
144+
\]
145+
\saNote{} The binary flag \locCallMmu{} will be defined below.
146+
\end{description}
147+
The \zkEvm{} carries out the \inst{MCOPY} instruction in two steps,
148+
similarly to how it deals with the \inst{IDENTITY} precompile,
149+
see section~(\ref{hub: instruction handling: call: precompiles: identity}).
150+
The first step is to carry out a full copy of the specified (\emph{nonempty}) source memory span into a new,
151+
hitherto untouched, memory span with fresh (and as of yet, unclaimed) identifier $1 + \hubStamp_{i}$.
152+
The second step is to copy the contents over from that new memory span to the target memory span.
153+
In the above the source memory span starts at offset $\locSrcOffsetLo$ an occupies $\locSizeLo$ many bytes, and
154+
the target memory span starts at offset $\locTgtOffsetLo$ an (also) occupies $\locSizeLo$ many bytes.
155+
Both have identifier $\cn _{i}$.
156+
157+
This approach avoids difficulties related to
158+
(\emph{a}) overlapping source and target memory spans
159+
(\emph{b}) relative position of the source and target spans (source on the left of target and \emph{vice versa}.)
160+
\begin{description}
161+
\item[\underline{Miscellaneous-row $n^°(i + \locMcopyFrstMiscOffset)$: \mmuMod{} data:}]
162+
\If $\locTriggerMmu = 1$ \Then
163+
\[
164+
\setMmuInstructionParametersRamToRamSansPadding {
165+
anchorRow = i ,
166+
relOffset = \locMcopyFrstMiscOffset ,
167+
sourceId = \cn_{i} ,
168+
targetId = 1 + \hubStamp_{i} ,
169+
% auxiliaryId = 1 + \hubStamp_{i} ,
170+
% sourceOffsetHi = \col{src\_offset\_hi} ,
171+
sourceOffsetLo = \locSrcOffsetLo ,
172+
% targetOffsetLo = \locTgtOffsetLo ,
173+
size = \locSizeLo ,
174+
referenceOffset = 0 ,
175+
referenceSize = \locSizeLo ,
176+
% successBit = \nothing ,
177+
% limbOne = \col{limb\_1} ,
178+
% limbTwo = \col{limb\_2} ,
179+
% exoSum = \exoWeightKec ,
180+
% phase = \nothing ,
181+
}
182+
\]
183+
\item[\underline{Miscellaneous-row $n^°(i + \locMcopyScndMiscOffset)$: \mmuMod{} data:}]
184+
\If $\locTriggerMmu = 1$ \Then
185+
\[
186+
\setMmuInstructionParametersRamToRamSansPadding {
187+
anchorRow = i ,
188+
relOffset = \locMcopyScndMiscOffset ,
189+
sourceId = 1 + \hubStamp_{i} ,
190+
targetId = \cn_{i} ,
191+
% auxiliaryId = \nothing ,
192+
% sourceOffsetHi = \col{src\_offset\_hi} ,
193+
sourceOffsetLo = 0 ,
194+
% targetOffsetLo = \locTgtOffsetLo ,
195+
size = \locSizeLo ,
196+
referenceOffset = \locTgtOffsetLo ,
197+
referenceSize = \locSizeLo ,
198+
% successBit = \nothing ,
199+
% limbOne = \col{limb\_1} ,
200+
% limbTwo = \col{limb\_2} ,
201+
% exoSum = \exoWeightKec ,
202+
% phase = \nothing ,
203+
}
204+
\]
205+
\saNote{}
206+
The current context and caller context (which may own the call data) are provided by the lookup.
207+
\end{description}

‎hub/instruction_handling/mcopy/instructions_and_flags.tex

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
\[
2+
\begin{array}{|l||c||c||c|}
3+
\hline
4+
\INST & \tli & \stackDecMcopyFlag & \stackDecMxpFlag \\ \hline\hline
5+
\inst{MCOPY} & \zero & \oneCell & \oneCell \\ \hline
6+
\end{array}
7+
\]

‎hub/instruction_handling/mcopy/shorthands.tex

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
We will use the following shorthands
2+
\[
3+
\left\{ \begin{array}{lcl}
4+
\locTgtOffsetHi & \define & \stackItemValHi {1} _{i} \\
5+
\locTgtOffsetLo & \define & \stackItemValLo {1} _{i} \vspace{2mm} \\
6+
\locSrcOffsetHi & \define & \stackItemValHi {2} _{i} \\
7+
\locSrcOffsetLo & \define & \stackItemValLo {2} _{i} \\
8+
\end{array} \right.
9+
\quad\text{and}\quad
10+
\left\{ \begin{array}{lcl}
11+
\locSizeHi & \define & \stackItemValHi {3} _{i} \\
12+
\locSizeLo & \define & \stackItemValLo {3} _{i} \vspace{2mm} \\
13+
\locMcopyMxpMxpx & \define & \miscMxpMxpx _{i + \locMcopyFrstMiscOffset} \\
14+
\locMcopyMxpGas & \define & \miscMxpGasMxp _{i + \locMcopyFrstMiscOffset} \\
15+
\locMcopyMxpSizeOneNonZeroNoMxpx & \define & \miscMxpSizeOneNonzeroNoMxpx _{i + \locMcopyFrstMiscOffset} \\
16+
\end{array} \right.
17+
\]
18+

0 commit comments

Comments
 (0)