Skip to content

Commit 2f23e74

Browse files
OlivierBBBOlivierBBB
authored
EIP-7823: Set upper bounds for MODEXP --- OOB side (#813)
1 parent c29b603 commit 2f23e74

File tree

8 files changed

+323
-84
lines changed

8 files changed

+323
-84
lines changed

‎constants/constants.lisp‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -228,6 +228,7 @@
228228
GAS_CONST_IDENTITY 15
229229
GAS_CONST_IDENTITY_WORD 3
230230
GAS_CONST_MODEXP 200
231+
GAS_CONST_MODEXP_EIP_7823 500
231232
GAS_CONST_ECADD 150
232233
GAS_CONST_ECMUL 6000
233234
GAS_CONST_ECPAIRING 45000
@@ -270,6 +271,7 @@
270271
HISTORY_STORAGE_ADDRESS_HI 0x0000f908
271272
HISTORY_STORAGE_ADDRESS_LO 0x27f1c53a10cb7a02335b175320002935
272273
EIP_7825_TRANSACTION_GAS_LIMIT_CAP 0x1000000 ;; 2^24 == 16777216 appears in OSAKA
274+
EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1024
273275
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
274276
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
275277
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; LINEA MISC ;;

‎oob/cancun/precompiles/modexp/xbs.lisp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414
(defun (prc-modexp-xbs---compute-max) [DATA 4])
1515
(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7])
1616
(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8])
17-
(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO)
17+
(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO)
1818
(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO))
1919

2020
(defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
@@ -28,7 +28,7 @@
2828

2929
(defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
3030
(begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max)))
31-
(eq! (prc-modexp-xbs---compo-to_512) 1)))
31+
(eq! (prc-modexp-xbs---comparison-to-512) 1)))
3232

3333
(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
3434
(if-zero (prc-modexp-xbs---compute-max)

‎oob/london/precompiles/modexp/xbs.lisp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414
(defun (prc-modexp-xbs---compute-max) [DATA 4])
1515
(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7])
1616
(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8])
17-
(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO)
17+
(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO)
1818
(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO))
1919

2020
(defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
@@ -28,7 +28,7 @@
2828

2929
(defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
3030
(begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max)))
31-
(eq! (prc-modexp-xbs---compo-to_512) 1)))
31+
(eq! (prc-modexp-xbs---comparison-to-512) 1)))
3232

3333
(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
3434
(if-zero (prc-modexp-xbs---compute-max)

‎oob/osaka/precompiles/modexp/lead.lisp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
(defun (prc-modexp-lead---ebs-is-zero) OUTGOING_RES_LO)
1818
(defun (prc-modexp-lead---ebs-less-than_32) (next OUTGOING_RES_LO))
1919
(defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2))
20-
(defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3))
20+
(defun (prc-modexp-lead---result-of-comparison) (shift OUTGOING_RES_LO 3))
2121

2222
(defconstraint prc-modexp-lead---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition)))
2323
(call-to-ISZERO 0 0 (prc-modexp-lead---ebs)))
@@ -42,7 +42,7 @@
4242
(- 1 (prc-modexp-lead---ebs-is-zero))))
4343
(if-zero (prc-modexp-lead---call-data-contains-exponent-bytes)
4444
(vanishes! (prc-modexp-lead---cds-cutoff))
45-
(if-zero (prc-modexp-lead---comp)
45+
(if-zero (prc-modexp-lead---result-of-comparison)
4646
(eq! (prc-modexp-lead---cds-cutoff) 32)
4747
(eq! (prc-modexp-lead---cds-cutoff)
4848
(- (prc---cds) (+ 96 (prc-modexp-lead---bbs))))))

‎oob/osaka/precompiles/modexp/pricing.lisp‎

Lines changed: 183 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -7,47 +7,188 @@
77
;; ;;
88
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
99

10-
(defun (prc-modexp-pricing---standard-precondition) IS_MODEXP_PRICING)
10+
11+
(defconst
12+
ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK 0
13+
ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK 1
14+
ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8 2
15+
ROFF___MODEXP_PRICING___MAX_VS_32 3
16+
ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST 4
17+
ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST 5
18+
)
19+
20+
21+
(defun (prc-modexp-pricing---standard-precondition) (* (assumption---fresh-new-stamp) IS_MODEXP_PRICING))
1122
(defun (prc-modexp-pricing---exponent-log) [DATA 6])
12-
(defun (prc-modexp-pricing---max-xbs-ybs) [DATA 7])
13-
(defun (prc-modexp-pricing---exponent-log-is-zero) (next OUTGOING_RES_LO))
14-
(defun (prc-modexp-pricing---f-of-max) (* (shift OUTGOING_RES_LO 2) (shift OUTGOING_RES_LO 2)))
15-
(defun (prc-modexp-pricing---big-quotient) (shift OUTGOING_RES_LO 3))
16-
(defun (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) (shift OUTGOING_RES_LO 4))
17-
(defun (prc-modexp-pricing---big-numerator) (if-zero (prc-modexp-pricing---exponent-log-is-zero)
18-
(* (prc-modexp-pricing---f-of-max) (prc-modexp-pricing---exponent-log))
19-
(prc-modexp-pricing---f-of-max)))
20-
(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP)
21-
(prc-modexp-pricing---big-quotient)
22-
GAS_CONST_MODEXP))
23-
24-
(defconstraint prc-modexp-pricing---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
25-
(call-to-ISZERO 0 0 (prc---r@c)))
26-
27-
(defconstraint prc-modexp-pricing---check-exponent-log-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
28-
(call-to-ISZERO 1 0 (prc-modexp-pricing---exponent-log)))
29-
30-
(defconstraint prc-modexp-pricing---div-max-xbs-ybs-plus-7-by-8 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
31-
(call-to-DIV 2
32-
0
33-
(+ (prc-modexp-pricing---max-xbs-ybs) 7)
34-
0
35-
8))
36-
37-
(defconstraint prc-modexp-pricing---div-big-numerator-by-quaddivisor (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
38-
(call-to-DIV 3 0 (prc-modexp-pricing---big-numerator) 0 G_QUADDIVISOR))
39-
40-
(defconstraint prc-modexp-pricing---compare-big-quotient-against-GAS_CONST_MODEXP (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
41-
(call-to-LT 4 0 (prc-modexp-pricing---big-quotient) 0 GAS_CONST_MODEXP))
42-
43-
(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
44-
(call-to-LT 5 0 (prc---callee-gas) 0 (prc-modexp-pricing---precompile-cost)))
45-
46-
(defconstraint prc-modexp-pricing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
47-
(begin (eq! (prc---ram-success)
48-
(- 1 (shift OUTGOING_RES_LO 5)))
49-
(if-zero (prc---ram-success)
50-
(vanishes! (prc---return-gas))
51-
(eq! (prc---return-gas) (- (prc---callee-gas) (prc-modexp-pricing---precompile-cost))))
52-
(eq! (prc---r@c-nonzero) (- 1 OUTGOING_RES_LO))))
23+
(defun (prc-modexp-pricing---max-mbs-bbs) [DATA 7])
24+
;; ""
25+
26+
27+
28+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
29+
;; ;;
30+
;; row i + 0: [email protected]() check ;;
31+
;; ;;
32+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
33+
34+
(defconstraint prc-modexp-pricing---r@c-iszero-check
35+
(:guard (prc-modexp-pricing---standard-precondition))
36+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
37+
(call-to-ISZERO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK
38+
0
39+
(prc---r@c)
40+
))
41+
42+
(defun (prc-modex-pricing---r@c-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK))
43+
44+
45+
46+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
47+
;; ;;
48+
;; row i + 1: exponentLog.isZero() check ;;
49+
;; ;;
50+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
51+
52+
53+
(defconstraint prc-modexp-pricing---check-exponent-log-is-zero
54+
(:guard (prc-modexp-pricing---standard-precondition))
55+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
56+
(call-to-ISZERO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK
57+
0
58+
(prc-modexp-pricing---exponent-log)
59+
))
60+
61+
(defun (prc-modexp-pricing---exponent-log-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK))
62+
63+
64+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
65+
;; ;;
66+
;; row i + 2: ⌈ max(mbs, bbs) / 8 ⌉ compututation ;;
67+
;; ;;
68+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
69+
70+
71+
72+
(defconstraint prc-modexp-pricing---computing-ceiling-of-max-mbs-bbs-over-8
73+
(:guard (prc-modexp-pricing---standard-precondition))
74+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
75+
(call-to-DIV ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8
76+
0
77+
(+ (prc-modexp-pricing---max-mbs-bbs) 7)
78+
0
79+
8
80+
))
81+
82+
(defun (prc-modexp-pricing---ceiling-of-max-over-8) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8))
83+
84+
85+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
86+
;; ;;
87+
;; row i + 3: comparing max(mbs, bbs) and 32 ;;
88+
;; ;;
89+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
90+
91+
92+
(defconstraint prc-modexp-pricing---max-mbs-bbs-vs-32
93+
(:guard (prc-modexp-pricing---standard-precondition))
94+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
95+
(call-to-LT ROFF___MODEXP_PRICING___MAX_VS_32
96+
0
97+
WORD_SIZE
98+
0
99+
(prc-modexp-pricing---max-mbs-bbs)
100+
))
101+
102+
(defun (prc-modexp-pricing---word-cost-dominates) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___MAX_VS_32))
103+
(defun (prc-modexp-pricing---f-of-max) (* (prc-modexp-pricing---ceiling-of-max-over-8)
104+
(prc-modexp-pricing---ceiling-of-max-over-8)))
105+
(defun (prc-modexp-pricing---multiplication-complexity) (if-zero (force-bin (prc-modexp-pricing---word-cost-dominates))
106+
16
107+
(* 2 (prc-modexp-pricing---f-of-max))))
108+
(defun (prc-modexp-pricing---iteration-count-or-1) (if-zero (force-bin (prc-modexp-pricing---exponent-log-is-zero))
109+
(prc-modexp-pricing---exponent-log)
110+
1))
111+
(defun (prc-modexp-pricing---raw-cost) (* (prc-modexp-pricing---multiplication-complexity)
112+
(prc-modexp-pricing---iteration-count-or-1)))
113+
114+
115+
116+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
117+
;; ;;
118+
;; row i + 4: comparing raw_price to 500 ;;
119+
;; ;;
120+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
121+
122+
123+
124+
(defconstraint prc-modexp-pricing---compare-raw-cost-against-GAS_CONST_MODEXP-of-EIP-7823
125+
(:guard (prc-modexp-pricing---standard-precondition))
126+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
127+
(call-to-LT ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST
128+
0
129+
(prc-modexp-pricing---raw-cost)
130+
0
131+
GAS_CONST_MODEXP_EIP_7823
132+
))
133+
134+
(defun (prc-modexp-pricing---raw-cost-LT-min-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST)))
135+
(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---raw-cost-LT-min-cost)
136+
;; raw_cost_LT_min_cost ≡ faux
137+
(prc-modexp-pricing---raw-cost)
138+
;; raw_cost_LT_min_cost ≡ true
139+
GAS_CONST_MODEXP_EIP_7823))
140+
141+
142+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
143+
;; ;;
144+
;; row i + 5: comparing callee_gas to precopile_cost ;;
145+
;; ;;
146+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
147+
148+
149+
150+
(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost
151+
(:guard (prc-modexp-pricing---standard-precondition))
152+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
153+
(call-to-LT ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST
154+
0
155+
(prc---callee-gas)
156+
0
157+
(prc-modexp-pricing---precompile-cost)
158+
))
159+
160+
(defun (prc-modexp-pricing---callee-gas-LT-precompile-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST)))
161+
162+
163+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
164+
;; ;;
165+
;; justifying HUB predictions ;;
166+
;; ;;
167+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
168+
169+
(defconstraint prc-modexp-pricing---justify-hub-predictions---ram-success
170+
(:guard (prc-modexp-pricing---standard-precondition))
171+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
172+
(eq! (prc---ram-success)
173+
(- 1 (prc-modexp-pricing---callee-gas-LT-precompile-cost))
174+
))
175+
176+
(defconstraint prc-modexp-pricing---justify-hub-predictions---return-gas
177+
(:guard (prc-modexp-pricing---standard-precondition))
178+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
179+
(if-zero (force-bin (prc---ram-success))
180+
;; ram_success ≡ faux
181+
(vanishes! (prc---return-gas))
182+
;; ram_success ≡ true
183+
(eq! (prc---return-gas)
184+
(- (prc---callee-gas)
185+
(prc-modexp-pricing---precompile-cost)))
186+
))
187+
188+
(defconstraint prc-modexp-pricing---justify-hub-predictions---r@c-nonzero
189+
(:guard (prc-modexp-pricing---standard-precondition))
190+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
191+
(eq! (prc---r@c-nonzero)
192+
(- 1 (prc-modex-pricing---r@c-is-zero))
193+
))
53194

0 commit comments

Comments
 (0)