Skip to content

Commit 4f70e04

Browse files
OlivierBBBOlivierBBB
committed
fix: MODEXP related OOB instructions
1 parent ad8e35b commit 4f70e04

File tree

2 files changed

+75
-34
lines changed

2 files changed

+75
-34
lines changed

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
(defun (prc-modexp-lead---standard-precondition) IS_MODEXP_LEAD)
1111
(defun (prc-modexp-lead---bbs) [DATA 1])
1212
(defun (prc-modexp-lead---ebs) [DATA 3])
13-
(defun (prc-modexp-lead---load-lead) [DATA 4])
13+
(defun (prc-modexp-lead---extract-leading-word) [DATA 4])
1414
(defun (prc-modexp-lead---cds-cutoff) [DATA 6])
1515
(defun (prc-modexp-lead---ebs-cutoff) [DATA 7])
1616
(defun (prc-modexp-lead---sub-ebs_32) [DATA 8])
@@ -19,6 +19,8 @@
1919
(defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2))
2020
(defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3))
2121

22+
;; ""
23+
2224
(defconstraint prc-modexp-lead---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition)))
2325
(call-to-ISZERO 0 0 (prc-modexp-lead---ebs)))
2426

@@ -37,7 +39,7 @@
3739
32)))
3840

3941
(defconstraint prc-modexp-lead---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition)))
40-
(begin (eq! (prc-modexp-lead---load-lead)
42+
(begin (eq! (prc-modexp-lead---extract-leading-word)
4143
(* (prc-modexp-lead---call-data-contains-exponent-bytes)
4244
(- 1 (prc-modexp-lead---ebs-is-zero))))
4345
(if-zero (prc-modexp-lead---call-data-contains-exponent-bytes)

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

Lines changed: 71 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -7,35 +7,74 @@
77
;; ;;
88
;;;;;;;;;;;;;;;;;;;;;;;;;;;;
99

10-
(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS)
11-
(defun (prc-modexp-xbs---xbs-hi) [DATA 1])
12-
(defun (prc-modexp-xbs---xbs-lo) [DATA 2])
13-
(defun (prc-modexp-xbs---ybs-lo) [DATA 3])
14-
(defun (prc-modexp-xbs---compute-max) [DATA 4])
15-
(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7])
16-
(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8])
17-
(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO)
18-
(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO))
19-
20-
(defconstraint prc-modexp-xbs---compare-xbs-hi-against-513 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
21-
(call-to-LT 0 (prc-modexp-xbs---xbs-hi) (prc-modexp-xbs---xbs-lo) 0 513))
22-
23-
(defconstraint prc-modexp-xbs---compare-xbs-against-ybs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
24-
(call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo)))
25-
26-
(defconstraint prc-modexp-xbs---check-xbs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
27-
(call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo)))
28-
29-
(defconstraint additional-prc-modexp-xbs (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
30-
(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)))
32-
33-
(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
34-
(if-zero (prc-modexp-xbs---compute-max)
35-
(begin (vanishes! (prc-modexp-xbs---max-xbs-ybs))
36-
(vanishes! (prc-modexp-xbs---xbs-nonzero)))
37-
(begin (eq! (prc-modexp-xbs---xbs-nonzero)
38-
(- 1 (shift OUTGOING_RES_LO 2)))
39-
(if-zero (prc-modexp-xbs---comp)
40-
(eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---xbs-lo))
41-
(eq! (prc-modexp-xbs---max-xbs-ybs) (prc-modexp-xbs---ybs-lo))))))
10+
(defun (prc-modexp-xbs---standard-precondition) IS_MODEXP_XBS)
11+
(defun (prc-modexp-xbs---xbs-hi) [DATA 1])
12+
(defun (prc-modexp-xbs---xbs-lo) [DATA 2])
13+
(defun (prc-modexp-xbs---ybs-lo) [DATA 3])
14+
(defun (prc-modexp-xbs---compute-max) [DATA 4])
15+
(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7])
16+
(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8])
17+
(defun (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) OUTGOING_RES_LO)
18+
(defun (prc-modexp-xbs---xbs-is-LT-ybs) (next OUTGOING_RES_LO)) ;; ""
19+
20+
(defconstraint prc-modexp-xbs---compare-xbs-against-MODEXP-upper-byte-size-bound
21+
(:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
22+
(call-to-LT 0
23+
(prc-modexp-xbs---xbs-hi)
24+
(prc-modexp-xbs---xbs-lo)
25+
0
26+
(+ EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1)
27+
))
28+
29+
30+
(defconstraint prc-modexp-xbs---compare-xbs-against-ybs
31+
(:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
32+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
33+
(call-to-LT 1 0 (prc-modexp-xbs---xbs-lo) 0 (prc-modexp-xbs---ybs-lo)))
34+
35+
36+
(defconstraint prc-modexp-xbs---check-xbs-is-zero
37+
(:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
38+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
39+
(call-to-ISZERO 2 0 (prc-modexp-xbs---xbs-lo)))
40+
41+
42+
(defconstraint additional-prc-modexp-xbs
43+
(:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
44+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
45+
(begin (or! (eq! 0 (prc-modexp-xbs---compute-max)) (eq! 1 (prc-modexp-xbs---compute-max)))
46+
(eq! (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound) 1)))
47+
48+
49+
(defconstraint prc-modexp-xbs---justifying-hub-predictions---nonzeroness-bit
50+
(:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
51+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
52+
(if-zero (prc-modexp-xbs---compute-max)
53+
;; comupte max = false
54+
(begin (vanishes! (prc-modexp-xbs---max-xbs-ybs))
55+
(vanishes! (prc-modexp-xbs---xbs-nonzero)))
56+
;; comupte max = false
57+
(begin (eq! (prc-modexp-xbs---xbs-nonzero)
58+
(- 1 (shift OUTGOING_RES_LO 2)))
59+
)))
60+
61+
62+
(defconstraint prc-modexp-xbs---justifying-hub-predictions---value-of-max
63+
(:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
64+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
65+
(if-zero (prc-modexp-xbs---compute-max)
66+
;; comupte_max = false
67+
(vanishes! (prc-modexp-xbs---max-xbs-ybs))
68+
;; comupte_max = false
69+
(if-zero (prc-modexp-xbs---xbs-is-LEQ-the-MODEXP-upper-bound)
70+
;; false case
71+
(vanishes! (prc-modexp-xbs---max-xbs-ybs))
72+
;; true case
73+
(if-zero (prc-modexp-xbs---xbs-is-LT-ybs)
74+
;; false case
75+
(eq! (prc-modexp-xbs---max-xbs-ybs)
76+
(prc-modexp-xbs---xbs-lo))
77+
;; true case
78+
(eq! (prc-modexp-xbs---max-xbs-ybs)
79+
(prc-modexp-xbs---ybs-lo))
80+
))))

0 commit comments

Comments
 (0)