Skip to content

Commit 00e31bc

Browse files
OlivierBBBOlivierBBB
authored
EIP-7823: Set upper bounds for MODEXP --- HUB side (#815)
1 parent 78ad636 commit 00e31bc

File tree

13 files changed

+612
-88
lines changed

13 files changed

+612
-88
lines changed

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

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
(module hub)
2+
3+
;;;;;;;;;;;;;;;;;;;;;;;;
4+
;;;;;;;;;;;;;;;;;;;;;;;;
5+
;;;; ;;;;
6+
;;;; X.Y CALL ;;;;
7+
;;;; ;;;;
8+
;;;;;;;;;;;;;;;;;;;;;;;;
9+
;;;;;;;;;;;;;;;;;;;;;;;;
10+
11+
12+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
13+
;; ;;
14+
;; X.Y.Z.4 MODEXP common processing ;;
15+
;; ;;
16+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
17+
18+
19+
20+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
21+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
22+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CALL_DATA_SIZE analysis row ;;
23+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
24+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
25+
26+
27+
(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-module-flags
28+
(:guard (precompile-processing---MODEXP---standard-precondition))
29+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
30+
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis)
31+
MISC_WEIGHT_OOB))
32+
33+
34+
(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-OOB-instruction
35+
(:guard (precompile-processing---MODEXP---standard-precondition))
36+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
37+
(set-OOB-instruction---modexp-cds precompile-processing---MODEXP---misc-row-offset---cds-analysis ;; row offset
38+
(precompile-processing---dup-cds))) ;; call data size
39+
40+
41+
(defun (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 3] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; ""
42+
(defun (precompile-processing---MODEXP---extract-ebs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; ""
43+
(defun (precompile-processing---MODEXP---extract-mbs) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; ""

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

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
(module hub)
2+
3+
;;;;;;;;;;;;;;;;;;;;;;;;
4+
;;;;;;;;;;;;;;;;;;;;;;;;
5+
;;;; ;;;;
6+
;;;; X.Y CALL ;;;;
7+
;;;; ;;;;
8+
;;;;;;;;;;;;;;;;;;;;;;;;
9+
;;;;;;;;;;;;;;;;;;;;;;;;
10+
11+
12+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
13+
;; ;;
14+
;; X.Y.Z.4 MODEXP common processing ;;
15+
;; ;;
16+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
17+
18+
19+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
20+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
21+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; bbs extraction and analysis row ;;
22+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
23+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
24+
25+
26+
(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-misc-module-flags
27+
(:guard (precompile-processing---MODEXP---standard-precondition))
28+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
29+
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)
30+
(+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs))
31+
MISC_WEIGHT_OOB)
32+
))
33+
34+
35+
(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-MMU-instruction
36+
(:guard (precompile-processing---MODEXP---standard-precondition))
37+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
38+
(if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)
39+
(set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset
40+
CONTEXT_NUMBER ;; source ID
41+
;; tgt_id ;; target ID
42+
;; aux_id ;; auxiliary ID
43+
;; src_offset_hi ;; source offset high
44+
0 ;; source offset low
45+
;; tgt_offset_lo ;; target offset low
46+
;; size ;; size
47+
(precompile-processing---dup-cdo) ;; reference offset
48+
(precompile-processing---dup-cds) ;; reference size
49+
;; success_bit ;; success bit
50+
(shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE
51+
(shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE
52+
;; exo_sum ;; weighted exogenous module flag sum
53+
;; phase ;; phase
54+
)))
55+
56+
(defun (precompile-processing---MODEXP---bbs-hi) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)))
57+
(defun (precompile-processing---MODEXP---bbs-lo) (* (precompile-processing---MODEXP---extract-bbs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)))
58+
59+
60+
(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-OOB-instruction
61+
(:guard (precompile-processing---MODEXP---standard-precondition))
62+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
63+
(set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset
64+
(precompile-processing---MODEXP---bbs-hi) ;; high part of some {b,e,m}bs
65+
(precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs
66+
0 ;; low part of some {b,e,m}bs
67+
0 ;; bit indicating whether to compute max(xbs, ybs) or not
68+
))
69+
70+
71+
(defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; ""
72+
(defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; ""
73+
(defun (precompile-processing---MODEXP---bbs-normalized) (* (precompile-processing---MODEXP---bbs-lo)
74+
(precompile-processing---MODEXP---bbs-within-bounds)))

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

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
(module hub)
2+
3+
;;;;;;;;;;;;;;;;;;;;;;;;
4+
;;;;;;;;;;;;;;;;;;;;;;;;
5+
;;;; ;;;;
6+
;;;; X.Y CALL ;;;;
7+
;;;; ;;;;
8+
;;;;;;;;;;;;;;;;;;;;;;;;
9+
;;;;;;;;;;;;;;;;;;;;;;;;
10+
11+
12+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
13+
;; ;;
14+
;; X.Y.Z.4 MODEXP common processing ;;
15+
;; ;;
16+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
17+
18+
19+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
20+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
21+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ebs extraction and analysis row ;;
22+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
23+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
24+
25+
26+
(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-misc-module-flags
27+
(:guard (precompile-processing---MODEXP---standard-precondition))
28+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
29+
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)
30+
(+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs))
31+
MISC_WEIGHT_OOB)
32+
))
33+
34+
35+
(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-MMU-instruction
36+
(:guard (precompile-processing---MODEXP---standard-precondition))
37+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
38+
(if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)
39+
(set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset
40+
CONTEXT_NUMBER ;; source ID
41+
;; tgt_id ;; target ID
42+
;; aux_id ;; auxiliary ID
43+
;; src_offset_hi ;; source offset high
44+
32 ;; source offset low
45+
;; tgt_offset_lo ;; target offset low
46+
;; size ;; size
47+
(precompile-processing---dup-cdo) ;; reference offset
48+
(precompile-processing---dup-cds) ;; reference size
49+
;; success_bit ;; success bit
50+
(shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE
51+
(shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE
52+
;; exo_sum ;; weighted exogenous module flag sum
53+
;; phase ;; phase
54+
)))
55+
56+
57+
(defun (precompile-processing---MODEXP---ebs-hi) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)))
58+
(defun (precompile-processing---MODEXP---ebs-lo) (* (precompile-processing---MODEXP---extract-ebs) (shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)))
59+
60+
61+
(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-OOB-instruction
62+
(:guard (precompile-processing---MODEXP---standard-precondition))
63+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
64+
(set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset
65+
(precompile-processing---MODEXP---ebs-hi) ;; high part of some {b,e,m}bs
66+
(precompile-processing---MODEXP---ebs-lo) ;; low part of some {b,e,m}bs
67+
0 ;; low part of some {b,e,m}bs
68+
0 ;; bit indicating whether to compute max(xbs, ybs) or not
69+
))
70+
71+
72+
(defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis))
73+
(defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)) ;; ""
74+
(defun (precompile-processing---MODEXP---ebs-normalized) (* (precompile-processing---MODEXP---ebs-lo)
75+
(precompile-processing---MODEXP---ebs-within-bounds)))

0 commit comments

Comments
 (0)