Skip to content

Commit 1fa6fba

Browse files
OlivierBBBOlivierBBB
authored
Osaka debugging (#327)
* ras: typo * fix: conditional OOB method calls for MODEXP_LEAD and MODEXP_PRICING We make the OOB method cals to OOB_INST_MODEXP_LEAD and OOB_INST_MODEXP_PRICING conditional to all_byte_sizes_are_in_bounds = bbs_is_in_bounds ∧ ebs_is_in_bounds ∧ mbs_is_in_bounds Otherwise we had issues in the tracer implementation getting the correct exponent lead word (as we were reading call data starting at 96 + bbs in some parts of the tracer, and 96 + normalizedBbs in others. So this spec change just makes life easier, and avoids computing exponent logs that will never be used.
1 parent 3d549f2 commit 1fa6fba

File tree

3 files changed

+209
-12
lines changed

3 files changed

+209
-12
lines changed

‎hub/instruction_handling/call/precompiles/ecrecover_p256_verify/success.tex‎

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
1+
\begin{center}
2+
\boxed{%
3+
\text{The constraints presented below assume that }
4+
\left\{ \begin{array}{lcl}
5+
\peekScenario _{i} & = & 1 \\
6+
\left[ \begin{array}{cr}
7+
+ & \scenEcrecover _{i} \\
8+
+ & \scenPVerify _{i} \\
9+
\end{array} \right]
10+
& = & 1 \\
11+
\scenPrcSuccess _{i} & = & 1 \\
12+
\end{array} \right.
13+
}
14+
\end{center}
15+
We are thus assuming that the present row is
16+
the first of the second phase of dealing with
17+
either the \instEcrecover{} precompile or
18+
either the \instPVerify{} precompile.
19+
We are also assuming that $\scenPrcSuccess \equiv 1$.
20+
We remind the reader that, for both \instEcrecover{} and \instPVerify{},
21+
\textbf{success} only means that the precompile call was provided with sufficient gas.
22+
It does \textbf{not} mean,
23+
in the \instEcrecover{} case, that an address was effectively recovered, nor
24+
in the \instPVerify{} case, that signature verification was successful.
25+
\begin{description}
26+
\item[\underline{\underline{Miscellaneous-row $n^°(i + \prcStandardSuccessSecondMiscRowOffset)$: full transfer of return data:}}] ---
27+
\begin{description}
28+
\item[\underline{Defining \locTriggerMmuFullTransfer{}:}]
29+
we define
30+
\[
31+
\locTriggerMmuFullTransfer
32+
\define
33+
\left[ \begin{array}{crcl}
34+
+ & \locAddressRecoverySuccess & \cdot & \scenEcrecover _{i} \\
35+
+ & \locSignatureVerificationSuccess & \cdot & \scenPVerify _{i} \\
36+
\end{array} \right]
37+
\]
38+
\saNote{}
39+
\locTriggerMmuFullTransfer{} is provably binary,
40+
see note~(\ref{hub: instruction handling: call: precompiles: common: generalities: ecrecover recovery success failure flags are provably binary}).
41+
\item[\underline{Setting lookup flags:}]
42+
we impose
43+
\[
44+
\weightedMiscFlagSum {
45+
anchorRow = i ,
46+
relOffset = \prcStandardSuccessSecondMiscRowOffset ,
47+
}
48+
=
49+
\miscMmuWeight \cdot \locTriggerMmuFullTransfer
50+
% OK
51+
\]
52+
in other words
53+
\[
54+
\left\{ \begin{array}{lclr}
55+
\miscExpFlag _{i + \prcStandardSuccessSecondMiscRowOffset} & = & \gZero & (\sanityCheck) \\
56+
\miscMmuFlag _{i + \prcStandardSuccessSecondMiscRowOffset} & = & \locTriggerMmuFullTransfer & (\sanityCheck) \\
57+
\miscMxpFlag _{i + \prcStandardSuccessSecondMiscRowOffset} & = & \gZero & (\sanityCheck) \\
58+
\miscOobFlag _{i + \prcStandardSuccessSecondMiscRowOffset} & = & \gZero & (\sanityCheck) \\
59+
\miscStpFlag _{i + \prcStandardSuccessSecondMiscRowOffset} & = & \gZero & (\sanityCheck) \\
60+
\end{array} \right.
61+
\]
62+
\end{description}
63+
\saNote{} In other words the ``result transfer'' step of a call to the \instEcrecover{} only required if the call is
64+
(\emph{a}) is successful (i.e. is given sufficient gas) and
65+
(\emph{b}) is successful in recovering an address (as measured by $\locAddressRecoverySuccess \equiv 1$.)
66+
\begin{description}
67+
\item[\underline{Setting \mmuMod{}-instruction data:}]
68+
\If $\miscMmuFlag_{i + \prcStandardSuccessSecondMiscRowOffset} = 1$ \Then we impose
69+
\[
70+
\setMmuInstructionParametersExoToRamTransplants {
71+
anchorRow = i ,
72+
relOffset = \prcStandardSuccessSecondMiscRowOffset ,
73+
sourceId = 1 + \hubStamp_{i} ,
74+
targetId = 1 + \hubStamp_{i} ,
75+
size = \evmWordSize ,
76+
exoSum = \exoWeightEcdata ,
77+
phase = \locMmuPhase ,
78+
}
79+
\]
80+
where
81+
\[
82+
\locMmuPhase
83+
\define
84+
\left[ \begin{array}{crcl}
85+
+ & \phaseEcrecoverResult & \cdot & \scenEcrecover _{i} \\
86+
+ & \phasePVerifyResult & \cdot & \scenPVerify _{i} \\
87+
\end{array} \right]
88+
\]
89+
\saNote{}
90+
Recall that the return data \textbf{o}
91+
of a successful call to the \instEcrecover{} precompile
92+
which successfully recovers an address is an $\evmWordSize$-byte string
93+
$\textbf{o} \in \mathbb{B}_{\evmWordSize}$
94+
composed of 12 (leading) zero bytes
95+
followed by $\addressSize$ bytes making up
96+
the recovered \ethereum{} public address.
97+
98+
\saNote{}
99+
The return data $\textbf{o}$
100+
of a successful call to the \instPVerify{} precompile
101+
which successfully verifies a signature is the $\evmWordSize$-byte string
102+
$\utt{00}\, \utt{0x\,00}\, \cdots \, \utt{01} \in \mathbb{B}_{\evmWordSize}$.
103+
\end{description}
104+
\item[\underline{\underline{Miscellaneous-row $n^°(i + \prcStandardSuccessThirdMiscRowOffset)$: partial copy of return data:}}] ---
105+
\begin{description}
106+
\item[\underline{Defining \locTriggerMmuPartialCopy{}:}]
107+
we define
108+
\[
109+
\locTriggerMmuPartialCopy
110+
\define
111+
\left[ \begin{array}{cl}
112+
\cdot & \locTriggerMmuFullTransfer \\
113+
\cdot & \locOobResultNonzeroRac \\
114+
\end{array} \right]
115+
\]
116+
\saNote{}
117+
\locTriggerMmuPartialCopy{} is provably binary.
118+
\item[\underline{Setting lookup flags:}]
119+
we impose
120+
\[
121+
\weightedMiscFlagSum {
122+
anchorRow = i ,
123+
relOffset = \prcStandardSuccessThirdMiscRowOffset ,
124+
}
125+
=
126+
\miscMmuWeight
127+
\cdot
128+
\locTriggerMmuPartialCopy
129+
% OK
130+
\]
131+
in other words
132+
\[
133+
\left\{ \begin{array}{lclc}
134+
\miscExpFlag _{i + \prcStandardSuccessThirdMiscRowOffset} & = & \gZero & (\sanityCheck) \\
135+
\miscMmuFlag _{i + \prcStandardSuccessThirdMiscRowOffset} & = & \locTriggerMmuPartialCopy & (\sanityCheck) \\
136+
\miscMxpFlag _{i + \prcStandardSuccessThirdMiscRowOffset} & = & \gZero & (\sanityCheck) \\
137+
\miscOobFlag _{i + \prcStandardSuccessThirdMiscRowOffset} & = & \gZero & (\sanityCheck) \\
138+
\miscStpFlag _{i + \prcStandardSuccessThirdMiscRowOffset} & = & \gZero & (\sanityCheck) \\
139+
\end{array} \right.
140+
\]
141+
\end{description}
142+
\saNote{}
143+
In other words the ``(partial) copy of return data to the caller's \textsc{ram}''
144+
step of a call to either the \instEcrecover{} or the \instPVerify{} precompile
145+
is only required if the call is
146+
(\emph{a}) is successful (i.e. is given sufficient gas) and
147+
(\emph{b}) is successful in recovering an address or verifiying a signature
148+
(\emph{c}) and the underlying call has a nonzero \RAC{}.
149+
\begin{description}
150+
\item[\underline{\mmuMod{} data:}]
151+
\If $\miscMmuFlag_{i + \prcStandardSuccessThirdMiscRowOffset} = 1$ \Then we impose
152+
\[
153+
\setMmuInstructionParametersRamToRamSansPadding {
154+
anchorRow = i ,
155+
relOffset = \prcStandardSuccessThirdMiscRowOffset ,
156+
sourceId = 1 + \hubStamp _{i} ,
157+
targetId = \cn _{i} ,
158+
sourceOffsetLo = 0 ,
159+
size = \evmWordSize ,
160+
referenceOffset = \locPrcRao ,
161+
referenceSize = \locPrcRac ,
162+
}
163+
\]
164+
\end{description}
165+
\item[\underline{Context-row $n^°(i + \prcStandardSuccessCallerContextRowRowOffset)$:}]
166+
we impose
167+
\[
168+
\provideReturnData {
169+
anchorRow = i ,
170+
relOffset = \prcStandardSuccessCallerContextRowRowOffset ,
171+
returnDataReceiver = \cn _{i} ,
172+
returnDataProvider = 1 + \hubStamp _{i} ,
173+
returnDataOffset = 0 ,
174+
returnDataSize = \evmWordSize \cdot \locTriggerMmuFullTransfer ,
175+
}
176+
\]
177+
\end{description}

‎hub/instruction_handling/call/precompiles/modexp/_local.tex‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,9 @@
3030

3131
\def\locAllByteSizesAreInBounds {\loc{all\_byte\_sizes\_are\_in\_bounds}}
3232

33-
\def\locCallExpForModexpToAnalyzeLeadingWord {\loc{call\_EXP\_to\_analyze\_leading\_word}}
34-
\def\locCallMmuForModexpToExtractLeadingWord {\loc{call\_MMU\_to\_extract\_leading\_word}}
33+
\def\locCallOobForModexpForLeadWordExtractionAnalysis {\loc{call\_OOB\_to\_analyze\_leading\_word}}
34+
\def\locCallExpForModexpToAnalyzeLeadingWord {\loc{call\_EXP\_to\_analyze\_leading\_word}}
35+
\def\locCallMmuForModexpToExtractLeadingWord {\loc{call\_MMU\_to\_extract\_leading\_word}}
3536

3637
\def\locCallOobForModexpPricing {\loc{call\_OOB\_for\_pricing}}
3738

‎hub/instruction_handling/call/precompiles/modexp/common.tex‎

Lines changed: 29 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -377,7 +377,7 @@
377377
\miscExpFlag _{i + \prcModexpLeadRowOffset} & = & \locExtractLeadingWord \quad \undefinedStar \\
378378
\miscMmuFlag _{i + \prcModexpLeadRowOffset} & = & \locExtractLeadingWord \quad \undefinedStar \\
379379
\miscMxpFlag _{i + \prcModexpLeadRowOffset} & = & \rZero \\
380-
\miscOobFlag _{i + \prcModexpLeadRowOffset} & = & \rOne \\
380+
\miscOobFlag _{i + \prcModexpLeadRowOffset} & = & \locAllByteSizesAreInBounds \\
381381
\miscStpFlag _{i + \prcModexpLeadRowOffset} & = & \gZero \\
382382
\end{array} \right.
383383
\]
@@ -390,7 +390,7 @@
390390
\left\{ \begin{array}{lclr}
391391
\miscExpFlag _{i + \prcModexpLeadRowOffset} & = & \locExtractLeadingWord \quad \undefinedStar \\
392392
\miscMmuFlag _{i + \prcModexpLeadRowOffset} & = & \locExtractLeadingWord \quad \undefinedStar \\
393-
\miscOobFlag _{i + \prcModexpLeadRowOffset} & = & \rOne \\
393+
\miscOobFlag _{i + \prcModexpLeadRowOffset} & = & \locAllByteSizesAreInBounds \\
394394
\multicolumn{3}{l}{
395395
\left[ \begin{array}{cl}
396396
+ \!\!\! & \miscMxpFlag _{i + \prcModexpLeadRowOffset} \\
@@ -403,11 +403,16 @@
403403
We define the following shorthands
404404
\[
405405
\left\{ \begin{array}{lcl}
406-
\locCallExpForModexpToAnalyzeLeadingWord & \define & \miscExpFlag _{i + \prcModexpLeadRowOffset} \\
407-
\locCallMmuForModexpToExtractLeadingWord & \define & \miscMmuFlag _{i + \prcModexpLeadRowOffset} \\
406+
\locCallOobForModexpForLeadWordExtractionAnalysis & \define & \miscOobFlag _{i + \prcModexpLeadRowOffset} \\
407+
\locCallExpForModexpToAnalyzeLeadingWord & \define & \miscExpFlag _{i + \prcModexpLeadRowOffset} \\
408+
\locCallMmuForModexpToExtractLeadingWord & \define & \miscMmuFlag _{i + \prcModexpLeadRowOffset} \\
408409
\end{array} \right.
409410
\]
411+
\saNote{}
412+
\locCallOobForModexpForLeadWordExtractionAnalysis{} is logically equivalent to
413+
\locAllByteSizesAreInBounds{}.
410414
\item[\underline{Setting \oobMod{} values:}]
415+
\If $\locCallOobForModexpForLeadWordExtractionAnalysis = 1$ \Then
411416
we impose
412417
\[
413418
\setOobInstructionModexpLead {
@@ -496,19 +501,27 @@
496501
relOffset = \prcModexpPricingRowOffset ,
497502
}
498503
=
499-
\miscOobWeight
504+
\miscOobWeight \cdot \locAllByteSizesAreInBounds
500505
\]
501506
in other words
502507
\[
503508
\left\{ \begin{array}{lclr}
504-
\miscExpFlag _{i + \prcModexpPricingRowOffset} & = & \gZero & (\sanityCheck) \\
505-
\miscMmuFlag _{i + \prcModexpPricingRowOffset} & = & \rZero & (\sanityCheck) \\
506-
\miscMxpFlag _{i + \prcModexpPricingRowOffset} & = & \rZero & (\sanityCheck) \\
507-
\miscOobFlag _{i + \prcModexpPricingRowOffset} & = & \rOne & (\sanityCheck) \\
508-
\miscStpFlag _{i + \prcModexpPricingRowOffset} & = & \gZero & (\sanityCheck) \\
509+
\miscExpFlag _{i + \prcModexpPricingRowOffset} & = & \gZero & (\sanityCheck) \\
510+
\miscMmuFlag _{i + \prcModexpPricingRowOffset} & = & \rZero & (\sanityCheck) \\
511+
\miscMxpFlag _{i + \prcModexpPricingRowOffset} & = & \rZero & (\sanityCheck) \\
512+
\miscOobFlag _{i + \prcModexpPricingRowOffset} & = & \locAllByteSizesAreInBounds & (\sanityCheck) \\
513+
\miscStpFlag _{i + \prcModexpPricingRowOffset} & = & \gZero & (\sanityCheck) \\
509514
\end{array} \right.
510515
\]
516+
and we set
517+
\[
518+
\locCallOobForModexpPricing \define \miscOobFlag _{i + \prcModexpPricingRowOffset} \\
519+
\]
520+
\saNote{}
521+
\locCallOobForModexpPricing{} is logically equivalent to
522+
\locAllByteSizesAreInBounds{}.
511523
\item[\underline{Setting \oobMod{} values:}]
524+
\If $\locCallOobForModexpPricing = 1$ \Then
512525
we impose
513526
\[
514527
\setOobInstructionModexpPricing {
@@ -538,6 +551,12 @@
538551
\locPrcReturnGas _{i} & = & \locReturnGas & \cdot & \locAllByteSizesAreInBounds \\
539552
\end{array} \right.
540553
\]
554+
\saNote{}
555+
Given the automatic vanishing constraints from
556+
section~(\ref{hub: misc: automatic vanishing: vanishing})
557+
there really is no need to condition the above shorthands
558+
by \locAllByteSizesAreInBounds{}.
559+
We do it regardless for clarity.
541560
\end{description}
542561
\saNote{} The above equation involving \scenPrcFailure{} and \locPrcReturnGas{} is how we justify the presence/absence of failure due to insufficient gas and the amount of returned gas.
543562

0 commit comments

Comments
 (0)