Skip to content

Commit 008b715

Browse files
OlivierBBBOlivierBBB
committed
feat: P256_VERIFY constraints HUB-side
1 parent 52ff6ac commit 008b715

File tree

2 files changed

+213
-52
lines changed

2 files changed

+213
-52
lines changed

‎hub/osaka/constraints/instruction-handling/call/precompiles/common/generalities.lisp‎

Lines changed: 131 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,9 @@
3030
(eq! (shift misc/MMU_FLAG 1) (precompile-processing---common---OOB-extract-call-data))
3131
))
3232

33-
(defconstraint precompile-processing---common---setting-OOB-instruction (:guard (precompile-processing---common---precondition))
33+
(defconstraint precompile-processing---common---setting-OOB-instruction
34+
(:guard (precompile-processing---common---precondition))
35+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3436
(set-OOB-instruction---common precompile-processing---common---1st-misc-row---row-offset ;; offset
3537
(precompile-processing---common---OOB-instruction) ;; relevant OOB instruction
3638
(precompile-processing---dup-call-gas) ;; call gas i.e. gas provided to the precompile
@@ -71,16 +73,51 @@
7173
(defun (precompile-processing---common---OOB-empty-call-data) (shift [misc/OOB_DATA 7] precompile-processing---common---1st-misc-row---row-offset))
7274
(defun (precompile-processing---common---OOB-r@c-nonzero) (shift [misc/OOB_DATA 8] precompile-processing---common---1st-misc-row---row-offset)) ;; ""
7375

74-
(defproperty precompile-processing---common---sanity-checks-for-BLS-precompiles-and-P256-verify
75-
(if-not-zero (precompile-processing---common---precondition)
76-
(if-not-zero (force-bin (+ (scenario-shorthand---PRC---common-BLS-address-bit-sum) scenario/PRC_P256_VERIFY))
77-
(begin
78-
(eq! (precompile-processing---common---OOB-extract-call-data)
79-
(precompile-processing---common---OOB-hub-success))
80-
(eq! (precompile-processing---common---OOB-empty-call-data)
81-
0)))))
8276

83-
(defconstraint precompile-processing---common---setting-MMU-instruction (:guard (precompile-processing---common---precondition))
77+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
78+
;; OOB shorthands formal properties and sanity checks ;;
79+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
80+
81+
(defproperty precompile-processing---common---sanity-checks---binarities
82+
(begin
83+
(is-binary (precompile-processing---common---OOB-hub-success) )
84+
(is-binary (precompile-processing---common---OOB-extract-call-data) )
85+
(is-binary (precompile-processing---common---OOB-empty-call-data) )
86+
(is-binary (precompile-processing---common---OOB-r@c-nonzero) )
87+
))
88+
89+
(defproperty precompile-processing---common---sanity-checks---unconditional-extract-empty-exclusivity
90+
(vanishes! (* (precompile-processing---common---OOB-extract-call-data)
91+
(precompile-processing---common---OOB-empty-call-data)
92+
)))
93+
94+
(defproperty precompile-processing---common---sanity-checks---the-empty-call-data-bit-must-vanish-starting-with-Cancun
95+
(if-not-zero (+ (scenario-shorthand---PRC---common-Cancun-address-bit-sum)
96+
(scenario-shorthand---PRC---common-Prague-address-bit-sum)
97+
(scenario-shorthand---PRC---common-Osaka-address-bit-sum))
98+
(vanishes! (precompile-processing---common---OOB-empty-call-data))
99+
))
100+
101+
(defproperty precompile-processing---common---sanity-checks---neat-splitting-of-hub-success-bit-prior-to-Osaka
102+
(if-not-zero (+ (scenario-shorthand---PRC---common-London-address-bit-sum)
103+
(scenario-shorthand---PRC---common-Cancun-address-bit-sum)
104+
(scenario-shorthand---PRC---common-Prague-address-bit-sum))
105+
(eq! (precompile-processing---common---OOB-hub-success)
106+
(+ (precompile-processing---common---OOB-extract-call-data)
107+
(precompile-processing---common---OOB-empty-call-data)
108+
))))
109+
110+
;; we verify empirically that 0 ≤ extract_call_data ≤ hub_success (≤ 1)
111+
(defproperty precompile-processing---common---sanity-checks---not-so-neat-splitting-of-hub-success-for-Osaka
112+
(if-not-zero (scenario-shorthand---PRC---common-Osaka-address-bit-sum)
113+
(if-not-zero (precompile-processing---common---OOB-extract-call-data)
114+
(eq! (precompile-processing---common---OOB-hub-success)
115+
1
116+
))))
117+
118+
(defconstraint precompile-processing---common---setting-MMU-instruction
119+
(:guard (precompile-processing---common---precondition))
120+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
84121
(if-not-zero (shift misc/MMU_FLAG precompile-processing---common---1st-misc-row---row-offset)
85122
(begin
86123
(if-not-zero scenario/PRC_IDENTITY
@@ -131,18 +168,18 @@
131168
(* 96 scenario/PRC_ECMUL )
132169
(* (precompile-processing---dup-cds) scenario/PRC_ECPAIRING )
133170
(* (precompile-processing---dup-cds) (scenario-shorthand---PRC---common-BLS-address-bit-sum) )
134-
(* 160 scenario/PRC_P256_VERIFY )
171+
(* (precompile-processing---dup-cds) scenario/PRC_P256_VERIFY )
135172
))
136173

137174
(defun (precompile-processing---common---MMU-exo-sum)
138-
(+ (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECRECOVER )
139-
(* EXO_SUM_WEIGHT_RIPSHA scenario/PRC_SHA2-256 )
140-
(* EXO_SUM_WEIGHT_RIPSHA scenario/PRC_RIPEMD-160 )
141-
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECADD )
142-
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECMUL )
143-
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECPAIRING )
144-
(* EXO_SUM_WEIGHT_BLSDATA (scenario-shorthand---PRC---common-BLS-address-bit-sum) )
145-
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_P256_VERIFY )
175+
(+ (* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECRECOVER )
176+
(* EXO_SUM_WEIGHT_RIPSHA scenario/PRC_SHA2-256 )
177+
(* EXO_SUM_WEIGHT_RIPSHA scenario/PRC_RIPEMD-160 )
178+
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECADD )
179+
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECMUL )
180+
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_ECPAIRING )
181+
(* EXO_SUM_WEIGHT_BLSDATA (scenario-shorthand---PRC---common-BLS-address-bit-sum) )
182+
(* EXO_SUM_WEIGHT_ECDATA scenario/PRC_P256_VERIFY )
146183
))
147184

148185
(defun (precompile-processing---common---MMU-phase)
@@ -163,41 +200,102 @@
163200
(* PHASE_P256_VERIFY_DATA scenario/PRC_P256_VERIFY )
164201
))
165202

166-
;; ECRECOVER related shorthands
167-
(defun (precompile-processing---common---address-recovery-failure)
168-
(+ (precompile-processing---common---OOB-empty-call-data)
169-
(* (precompile-processing---common---OOB-extract-call-data)
170-
(- 1 (precompile-processing---common---MMU-success-bit)))))
171-
(defun (precompile-processing---common---address-recovery-success)
172-
(* (precompile-processing---common---OOB-extract-call-data)
173-
(precompile-processing---common---MMU-success-bit)))
203+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
204+
;; ECRECOVER related shorthands ;;
205+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
206+
207+
(defun (precompile-processing---common---address-recovery-failure) (+ (precompile-processing---common---OOB-empty-call-data)
208+
(* (precompile-processing---common---OOB-extract-call-data)
209+
(- 1 (precompile-processing---common---MMU-success-bit)))
210+
))
211+
(defun (precompile-processing---common---address-recovery-success) (* (precompile-processing---common---OOB-extract-call-data)
212+
(precompile-processing---common---MMU-success-bit)
213+
))
214+
215+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
216+
;; ECRECOVER related shorthands sanity checks ;;
217+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
218+
219+
(defproperty precompile-processing---common---address-recovery-success-shorthands-sanity-checks
220+
(begin
221+
(is-binary (precompile-processing---common---address-recovery-failure))
222+
(is-binary (precompile-processing---common---address-recovery-success))
223+
(eq! (precompile-processing---common---OOB-hub-success)
224+
(+ (precompile-processing---common---address-recovery-failure)
225+
(precompile-processing---common---address-recovery-success)
226+
))))
227+
228+
229+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
230+
;; ECADD, ECMUL, ECPAIRING and BLS related shorthands ;;
231+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
174232

175-
;; ECADD, ECMUL and ECPAIRING related shorthands
176233
(defun (precompile-processing---common---malformed-data) (* (precompile-processing---common---OOB-extract-call-data)
177234
(- 1 (precompile-processing---common---MMU-success-bit))))
178235
(defun (precompile-processing---common---wellformed-data) (+ (precompile-processing---common---OOB-empty-call-data)
179236
(* (precompile-processing---common---OOB-extract-call-data)
180237
(precompile-processing---common---MMU-success-bit))))
181238

239+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
240+
;; ECADD, ECMUL, ECPAIRING and BLS related shorthands sanity checks ;;
241+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
242+
243+
(defproperty precompile-processing---common---well-and-mal-formed-data-shorthands-sanity-checks
244+
(begin
245+
(is-binary (precompile-processing---common---malformed-data))
246+
(is-binary (precompile-processing---common---wellformed-data))
247+
(eq! (precompile-processing---common---OOB-hub-success)
248+
(+ (precompile-processing---common---malformed-data)
249+
(precompile-processing---common---wellformed-data)
250+
))))
251+
252+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
253+
;; P256_VERIFY related shorthands ;;
254+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
255+
256+
(defun (precompile-processing---common---p256-sufficient-gas-wrong-cds) (- (precompile-processing---common---OOB-hub-success)
257+
(precompile-processing---common---OOB-extract-call-data)
258+
))
259+
(defun (precompile-processing---common---p256-sig-verification-failure) (* (precompile-processing---common---OOB-extract-call-data)
260+
(- 1 (precompile-processing---common---MMU-success-bit))
261+
))
262+
(defun (precompile-processing---common---p256-sig-verification-success) (* (precompile-processing---common---OOB-extract-call-data)
263+
(precompile-processing---common---MMU-success-bit)
264+
))
182265

183-
;; (defconstraint precompile-processing---common---debug-constraints-for-address-recovery (:guard (precompile-processing---common---precondition)))
184-
;; (defconstraint precompile-processing---common---debug-constraints-for-data-integrity (:guard (precompile-processing---common---precondition)))
185-
;; (defconstraint precompile-processing---common---debug-constraints-for-automatic-success-bit-vanishing (:guard (precompile-processing---common---precondition)))
266+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
267+
;; P256_VERIFY related shorthands sanity checks ;;
268+
;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~;;
186269

187-
(defconstraint precompile-processing---common---justifying-success-scenario (:guard (precompile-processing---common---precondition))
270+
(defproperty precompile-processing---common---address-recovery-success-shorthands-sanity-checks
271+
(begin
272+
(is-binary (precompile-processing---common---p256-sufficient-gas-wrong-cds))
273+
(is-binary (precompile-processing---common---p256-sig-verification-failure))
274+
(is-binary (precompile-processing---common---p256-sig-verification-success))
275+
(eq! (precompile-processing---common---OOB-hub-success)
276+
(+ (precompile-processing---common---p256-sufficient-gas-wrong-cds)
277+
(precompile-processing---common---p256-sig-verification-failure)
278+
(precompile-processing---common---p256-sig-verification-success)
279+
))))
280+
281+
282+
283+
(defconstraint precompile-processing---common---justifying-success-scenario
284+
(:guard (precompile-processing---common---precondition))
285+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
188286
(eq! (scenario-shorthand---PRC---success)
189287
(+ (* (precompile-processing---common---OOB-hub-success)
190288
(+ scenario/PRC_ECRECOVER
191289
scenario/PRC_SHA2-256
192290
scenario/PRC_RIPEMD-160
193291
scenario/PRC_IDENTITY
292+
scenario/PRC_P256_VERIFY
194293
))
195294
(* (precompile-processing---common---wellformed-data)
196295
(+ scenario/PRC_ECADD
197296
scenario/PRC_ECMUL
198297
scenario/PRC_ECPAIRING
199298
(scenario-shorthand---PRC---common-BLS-address-bit-sum)
200-
scenario/PRC_P256_VERIFY
201299
))
202300
)))
203301

@@ -212,7 +310,6 @@
212310
scenario/PRC_ECMUL
213311
scenario/PRC_ECPAIRING
214312
(scenario-shorthand---PRC---common-BLS-address-bit-sum)
215-
scenario/PRC_P256_VERIFY
216313
))))
217314

218315
(defconstraint precompile-processing---common---justifying-return-gas-prediction (:guard (precompile-processing---common---precondition))

0 commit comments

Comments
 (0)