Skip to content

Commit 56f55da

Browse files
OlivierBBBOlivierBBB
committed
Merge branch 'main' into fix/p256-verify
2 parents e645c66 + 1fa6fba commit 56f55da

File tree

7 files changed

+198
-49
lines changed

7 files changed

+198
-49
lines changed

‎_notes/MODEXP-Osaka tests.md‎

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
# `MODEXP` test vectors for Osaka
2+
3+
## MODEXP pricing + the 500 boundary testing
4+
5+
With MODEXP pricing we have several interesting questions
6+
- the new pricing of the log of the exponent
7+
- the comparison to 500
8+
9+
The cost of MODEXP is now
10+
11+
cost ≡ 500 ∨ ζ
12+
ζ ≡ (l + 16 ∙ x) ∙ 2 ∙ words^2
13+
14+
with l ≡ lead_log, x ≡ (ebs - 32) ∨ 0, words ≡ ⌈max(mbs, bbs)/8⌉.
15+
16+
Testing will explore these variables somewhat extensively. We should test like so
17+
```
18+
bbs / mbs pairs
19+
===============
20+
21+
(bbs, mbs) ∈ { (0,0), (0, 3), (21, 37), (56, 55) }
22+
23+
|------------|-----|-------|---------|
24+
| (bbs, mbs) | max | words | words^2 |
25+
|------------|-----|-------|---------|
26+
| (0, 0) | 0 | 0 | 0 |
27+
| (0, 3) | 3 | 1 | 1 |
28+
| (21, 23) | 23 | 3 | 9 |
29+
| (56, 55) | 56 | 7 | 49 |
30+
|------------|-----|-------|---------|
31+
32+
NOTE: The (0,3) case gives us the most fine grained exploration of the 500 vs ζ boundary
33+
34+
⇒ there are 4 options
35+
36+
cds options:
37+
============
38+
39+
cds ≡ 96 + bbs + extra, extra ∈ { ebs / 2, ebs, ebs + mbs }
40+
41+
⇒ there are 3 options
42+
43+
ebs options:
44+
============
45+
46+
ebs ≡ 0, 1, 16, 27, 32, 39, 173 where the first (ebs ∧ 32) bytes are, in base two,
47+
48+
0b 00 .. 00 11 .. 11
49+
50+
with z ∈ {0, 1, ..., 8 ∙ (ebs ∧ 32) } one's (and lead_log ≡ 0, 1, ..., 8 ∙ (ebs ∧ 32))
51+
52+
⇒ there are (0 + 1 + 16 + 27 + 32 + 32 + 32) ∙ 8 + 7 ≡ 1127 options
53+
54+
Total options:
55+
==============
56+
57+
4 ∙ 3 ∙ 1127 ≡ 13524 variants
58+
```
59+
60+
Dimensions of testing
61+
- xbs'
62+
```
63+
valid ranges:
64+
0x0000
65+
0x0001
66+
0x0020
67+
0x0100
68+
0x0200
69+
0x02?? // only for cds = 32 - 1, 64 - 1, 96 - 1
70+
0x 00 .. 00 ?? .. ?? // and cds = 32 - l
71+
<k bytes> <32 - k bytes>
72+
73+
invalid ranges:
74+
0x201
75+
0x <leading> <trailing>
76+
<--16B--> <--16B-->
77+
78+
<leading> = 0x 00 .. 00
79+
| 0x 00 .. 01
80+
| 0x <random>
81+
| 0x ff .. ff
82+
83+
<trailing> ≡ <valid>
84+
| 0x <random>
85+
| 0x ff .. ff
86+
```
87+
88+
families of tests
89+
90+
- call_data_only_covers_parts_of_bbs: 00 < cds ≤ 32
91+
- call_data_only_covers_parts_of_ebs: 32 < cds ≤ 64
92+
- call_data_only_covers_parts_of_mbs: 64 < cds ≤ 96
93+
94+
Those tests we can do the (k,l) testing
95+
96+
```
97+
invalid_bbs_call_data ≡ 0x 00 .. 02 ff | ff .. ff ff | ff .. ff ff
98+
<---bbs---> | <---ebs---> | <---mbs--->
99+
100+
invalid_ebs_call_data ≡ 0x 00 .. 01 00 | 00 .. 02 ff | ff .. ff ff
101+
<---bbs---> | <---ebs---> | <---mbs--->
102+
103+
invalid_mbs_call_data ≡ 0x 00 .. 01 00 | 00 .. 01 80 | 00 .. 02 ff
104+
<---bbs---> | <---ebs---> | <---mbs--->
105+
106+
we apply a mask
107+
108+
bbs_mask(k) ≡ 0x 00 .. 00 03 ff .. ff | 'ff'.repeat(32) | 'ff'.repeat(32)
109+
bbs_cds(k) ≡
110+
```

‎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

‎oob/_local.tex‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -164,7 +164,7 @@
164164
\def\locBeyondBaseByLessThanAnEvmWord {\loc{by\_less\_than\_an\_EVM\_word}}
165165
\def\locNDataBytes {\loc{up\_to\_32\_call\_data\_bytes}}
166166
\def\locExtractLeadingWord {\loc{extract\_leading\_word}}
167-
\def\locCallDataContainsExponentBytes {\loc{call\_data\_contains\_exponent\_bytes}}
167+
\def\locCallDataExtendsBeyondBase {\loc{call\_data\_extends\_beyond\_base}}
168168
\def\locCallDataExtendsBeyondExponent {\loc{call\_data\_extends\_beyond\_exponent}}
169169
% MODEXP: pricing
170170
\def\locWordCostDominates {\loc{word\_cost\_dominates}}

‎oob/precompiles/modexp/_local.tex‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,5 @@
1414
\def\roffXbsModexpXbsVsEipMaxByteSize {\roffConstYellow{0}}
1515
\def\roffXbsModexpXbsVsYbs {\roffConstYellow{1}}
1616
\def\roffXbsModexpXbsIszeroCheck {\roffConstYellow{2}}
17+
18+
\def\locCumulativeLengthOfByteSizes {\numConst{96}}

‎oob/precompiles/modexp/lead.tex‎

Lines changed: 52 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@
44
\boxed{\text{All constraints in this subsection further assume } \oobInstIsModexpLead_{i} = 1}
55
\]
66
What the present system of constraints aims to verify the following predictions made in the \hubMod{} module:
7-
\green{(\emph{a})} compute the small integer $32\wedge \big[ \locCds - (96 + \locBbs) \big]^+$
8-
\green{(\emph{b})} compute the bit $[ \locCds > (96 + \locBbs) ] \wedge [ \locEbs \neq 0 ]$.
7+
\green{(\emph{a})} compute the small integer $\evmWordSize \wedge \big[ \locCds - (\locCumulativeLengthOfByteSizes + \locBbs) \big]^+$
8+
\green{(\emph{b})} compute the bit $[ \locCds > (\locCumulativeLengthOfByteSizes + \locBbs) ] \wedge [ \locEbs \neq 0 ]$.
99

1010
\noindent We use the shorthands defined below:
1111
\[
@@ -34,43 +34,60 @@
3434
argOneLo = \locEbs ,
3535
}
3636
\vspace{2mm} \\
37-
\wcpCallToLt {
38-
anchorRow = i ,
39-
relOffset = 1 ,
40-
argOneHi = 0 ,
41-
argOneLo = \locEbs ,
42-
argTwoHi = 0 ,
43-
argTwoLo = 32 ,
44-
}
45-
\vspace{2mm} \\
4637
\wcpCallToLt {
4738
anchorRow = i ,
48-
relOffset = 2 ,
39+
relOffset = 1 ,
4940
argOneHi = 0 ,
50-
argOneLo = 96 + \locBbs ,
41+
argOneLo = \locEbs ,
5142
argTwoHi = 0 ,
52-
argTwoLo = \locCds ,
43+
argTwoLo = \evmWordSize ,
44+
}
45+
\vspace{2mm} \\
46+
\wcpCallToLt {
47+
anchorRow = i ,
48+
relOffset = 2 ,
49+
argOneHi = 0 ,
50+
argOneLo = \locCumulativeLengthOfByteSizes + \locBbs ,
51+
argTwoHi = 0 ,
52+
argTwoLo = \locCds ,
5353
}
5454
\end{array} \right.
5555
\]
56-
and define the following shorthands
56+
and we define the following shorthands
5757
\[
5858
\left\{ \begin{array}{lcl}
59-
\locEbsIsZero & \define & \outgoingResLo_{i } \\
60-
\locEbsLtThirtyTwo & \define & \outgoingResLo_{i + 1} \\
61-
\locCallDataContainsExponentBytes & \define & \outgoingResLo_{i + 2} \\
59+
\locEbsIsZero & \define & \outgoingResLo_{i } \\
60+
\locEbsLtThirtyTwo & \define & \outgoingResLo_{i + 1} \\
61+
\locCallDataExtendsBeyondBase & \define & \outgoingResLo_{i + 2} \\
62+
\end{array} \right.
63+
\]
64+
\saNote{}
65+
The number $\locCumulativeLengthOfByteSizes = 3 \cdot \evmWordSize$ is the ``cumulative length of byte sizes''.
66+
It accounts for the first three \evm{} words in the (right zero-padded) call data holding the
67+
\textbf{base byte size},
68+
\textbf{exponent byte size} and
69+
\textbf{modulus byte size}
70+
respectively.
71+
72+
\saNote{}
73+
Thus, by definition
74+
\[
75+
\left\{ \begin{array}{rcl}
76+
\locEbsIsZero ~ \equiv ~ \true & \iff & \big[ \locEbs \equiv 0 \big] \vspace{1mm} \\
77+
\locEbsLtThirtyTwo ~ \equiv ~ \true & \iff & \big[ \locEbs < \evmWordSize \big] \vspace{1mm} \\
78+
\locCallDataExtendsBeyondBase ~ \equiv ~ \true & \iff & \big[ \locCds > \locCumulativeLengthOfByteSizes + \locBbs \big] \\
6279
\end{array} \right.
6380
\]
6481
\item[\underline{Row $n^\circ(i + 3)$:}]
65-
\If $\locCallDataContainsExponentBytes = 1$ \Then
82+
\If $\locCallDataExtendsBeyondBase = 1$ \Then
6683
\[
6784
\wcpCallToLt {
68-
anchorRow = i ,
69-
relOffset = 3 ,
70-
argOneHi = 0 ,
71-
argOneLo = \locCds - \big( 96 + \locBbs \big) ,
72-
argTwoHi = 0 ,
73-
argTwoLo = 32 ,
85+
anchorRow = i ,
86+
relOffset = 3 ,
87+
argOneHi = 0 ,
88+
argOneLo = \locCds - \big( \locCumulativeLengthOfByteSizes + \locBbs \big) ,
89+
argTwoHi = 0 ,
90+
argTwoLo = \evmWordSize ,
7491
}
7592
\]
7693
we define the following shorthand
@@ -83,34 +100,34 @@
83100
\[
84101
\locExtractLeadingWord
85102
=
86-
\locCallDataContainsExponentBytes \cdot (1 - \locEbsIsZero)
103+
\locCallDataExtendsBeyondBase \cdot (1 - \locEbsIsZero)
87104
\]
88105
\item[Constraining \locCdsCutoff{}:] we impose that
89106
\begin{enumerate}
90-
\item \If $\locCallDataContainsExponentBytes = 0$ \Then $\locCdsCutoff = 0$
91-
\item \If $\locCallDataContainsExponentBytes = 1$ \Then
107+
\item \If $\locCallDataExtendsBeyondBase = 0$ \Then $\locCdsCutoff = 0$
108+
\item \If $\locCallDataExtendsBeyondBase = 1$ \Then
92109
\begin{enumerate}
93-
\item \If $\locResultOfComparison = 0$ \Then $\locCdsCutoff = 32$
94-
\item \If $\locResultOfComparison = 1$ \Then $\locCdsCutoff = \locCds - \big( 96 + \locBbs \big)$
110+
\item \If $\locResultOfComparison = 0$ \Then $\locCdsCutoff = \evmWordSize$
111+
\item \If $\locResultOfComparison = 1$ \Then $\locCdsCutoff = \locCds - \big( \locCumulativeLengthOfByteSizes + \locBbs \big)$
95112
\end{enumerate}
96113
\end{enumerate}
97114
\item[Constraining \locEbsCutoff {}:] we impose that
98115
\begin{enumerate}
99-
\item \If $\locEbsLtThirtyTwo = 0$ \Then $\locEbsCutoff = 32$
116+
\item \If $\locEbsLtThirtyTwo = 0$ \Then $\locEbsCutoff = \evmWordSize$
100117
\item \If $\locEbsLtThirtyTwo = 1$ \Then $\locEbsCutoff = \locEbs$
101118
\end{enumerate}
102119
\item[Constraining \locEbsSubThirtyTwo {}:] we impose that
103120
\begin{enumerate}
104-
\item \If $\locEbsLtThirtyTwo = 0$ \Then $\locEbsSubThirtyTwo = \locEbs - 32$
121+
\item \If $\locEbsLtThirtyTwo = 0$ \Then $\locEbsSubThirtyTwo = \locEbs - \evmWordSize$
105122
\item \If $\locEbsLtThirtyTwo = 1$ \Then $\locEbsSubThirtyTwo = 0$
106123
\end{enumerate}
107124
\end{description}
108125
\end{description}
109126
\saNote{} The above thus computes respectively
110127
\[
111128
\left\{ \begin{array}{lcl}
112-
\locCdsCutoff & \equiv & \Big[ \locCds - \big( 96 + \locBbs \big) \Big] ^ + \wedge \, 32 \\
113-
\locEbsCutoff & \equiv & \locEbs \wedge 32 \\
114-
\locEbsSubThirtyTwo & \equiv & \Big[ \locEbs - 32 \Big] ^ + \\
129+
\locCdsCutoff & \equiv & \Big[ \locCds - \big( \locCumulativeLengthOfByteSizes + \locBbs \big) \Big] ^ + \wedge \, \evmWordSize \\
130+
\locEbsCutoff & \equiv & \locEbs \wedge \evmWordSize \\
131+
\locEbsSubThirtyTwo & \equiv & \Big[ \locEbs - \evmWordSize \Big] ^ + \\
115132
\end{array} \right.
116133
\]

‎txn_data/_local.tex‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,7 @@
219219
\def\nRowsTypeThree {\roffConstYellow{17}} \def\maxCtForTypeThree {(\nRowsTypeThree - 1)}
220220
\def\nRowsTypeFour {\roffConstYellow{17}} \def\maxCtForTypeFour {(\nRowsTypeFour - 1)}
221221

222-
\def\nRowsSysfNoop {\roffConstYellow{2}} \def\maxCtForSysfNoop {(\nRowsSysfNoop - 1)}
222+
\def\nRowsSysfNoop {\roffConstYellow{2}} \def\maxCtForSysfNoop {(\nRowsSysfNoop - 1)}
223223

224224
\def\locRlpTxnRcptPhaseSum {\loc{RLP\_TXN\_RCPT\_phase\_sum}}
225225
\def\locRlpTxnRcptOutgoing {\loc{RLP\_TXN\_RCPT\_outgoing}}

0 commit comments

Comments
 (0)