Skip to content

EIP-7823: Set upper bounds for MODEXP --- OOB side #813

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 10 commits into
base: master
Choose a base branch
from
Open

EIP-7823: Set upper bounds for MODEXP --- OOB side #813

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
605b792
ras
OlivierBBB Oct 10, 2025
c6e8c34
ras
OlivierBBB Oct 13, 2025
eeaa0f9
feat: OOB_INST_modexp_xbs instruction update
OlivierBBB Oct 13, 2025
4caa0a3
ras
OlivierBBB Oct 22, 2025
f0b1bc9
Merge branch 'master' into EIP-7823-set-upper-bounds-for-MODEXP
OlivierBBB Oct 22, 2025
2e2d359
ras: reflecting spec changes
OlivierBBB Oct 22, 2025
f43d5d1
ras
OlivierBBB Oct 22, 2025
24e287b
feat: MODEXP pricing instruction in the OOB module
OlivierBBB Oct 22, 2025
53eaa71
fix: make it compile
OlivierBBB Oct 22, 2025
b73e423
ras: "documentation"
OlivierBBB Oct 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions constants/constants.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,7 @@
GAS_CONST_IDENTITY 15
GAS_CONST_IDENTITY_WORD 3
GAS_CONST_MODEXP 200
GAS_CONST_MODEXP_EIP_7823 500
GAS_CONST_ECADD 150
GAS_CONST_ECMUL 6000
GAS_CONST_ECPAIRING 45000
Expand Down Expand Up @@ -269,6 +270,7 @@
HISTORY_STORAGE_ADDRESS_HI 0x0000f908
HISTORY_STORAGE_ADDRESS_LO 0x27f1c53a10cb7a02335b175320002935
EIP_7825_TRANSACTION_GAS_LIMIT_CAP 0x1000000 ;; 2^24 == 16777216 appears in OSAKA
EIP_7823_MODEXP_UPPER_BYTE_SIZE_BOUND 1024
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; LINEA MISC ;;
Expand Down
4 changes: 2 additions & 2 deletions oob/cancun/precompiles/modexp/xbs.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
(defun (prc-modexp-xbs---compute-max) [DATA 4])
(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7])
(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8])
(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO)
(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO)
(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO))

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

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

(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
(if-zero (prc-modexp-xbs---compute-max)
Expand Down
4 changes: 2 additions & 2 deletions oob/london/precompiles/modexp/xbs.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
(defun (prc-modexp-xbs---compute-max) [DATA 4])
(defun (prc-modexp-xbs---max-xbs-ybs) [DATA 7])
(defun (prc-modexp-xbs---xbs-nonzero) [DATA 8])
(defun (prc-modexp-xbs---compo-to_512) OUTGOING_RES_LO)
(defun (prc-modexp-xbs---comparison-to-512) OUTGOING_RES_LO)
(defun (prc-modexp-xbs---comp) (next OUTGOING_RES_LO))

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

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

(defconstraint prc-modexp-xbs---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-xbs---standard-precondition)))
(if-zero (prc-modexp-xbs---compute-max)
Expand Down
4 changes: 2 additions & 2 deletions oob/osaka/precompiles/modexp/lead.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@
(defun (prc-modexp-lead---ebs-is-zero) OUTGOING_RES_LO)
(defun (prc-modexp-lead---ebs-less-than_32) (next OUTGOING_RES_LO))
(defun (prc-modexp-lead---call-data-contains-exponent-bytes) (shift OUTGOING_RES_LO 2))
(defun (prc-modexp-lead---comp) (shift OUTGOING_RES_LO 3))
(defun (prc-modexp-lead---result-of-comparison) (shift OUTGOING_RES_LO 3))

(defconstraint prc-modexp-lead---check-ebs-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-lead---standard-precondition)))
(call-to-ISZERO 0 0 (prc-modexp-lead---ebs)))
Expand All @@ -42,7 +42,7 @@
(- 1 (prc-modexp-lead---ebs-is-zero))))
(if-zero (prc-modexp-lead---call-data-contains-exponent-bytes)
(vanishes! (prc-modexp-lead---cds-cutoff))
(if-zero (prc-modexp-lead---comp)
(if-zero (prc-modexp-lead---result-of-comparison)
(eq! (prc-modexp-lead---cds-cutoff) 32)
(eq! (prc-modexp-lead---cds-cutoff)
(- (prc---cds) (+ 96 (prc-modexp-lead---bbs))))))
Expand Down
225 changes: 183 additions & 42 deletions oob/osaka/precompiles/modexp/pricing.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,47 +7,188 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun (prc-modexp-pricing---standard-precondition) IS_MODEXP_PRICING)

(defconst
ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK 0
ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK 1
ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8 2
ROFF___MODEXP_PRICING___MAX_VS_32 3
ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST 4
ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST 5
)


(defun (prc-modexp-pricing---standard-precondition) (* (assumption---fresh-new-stamp) IS_MODEXP_PRICING))
(defun (prc-modexp-pricing---exponent-log) [DATA 6])
(defun (prc-modexp-pricing---max-xbs-ybs) [DATA 7])
(defun (prc-modexp-pricing---exponent-log-is-zero) (next OUTGOING_RES_LO))
(defun (prc-modexp-pricing---f-of-max) (* (shift OUTGOING_RES_LO 2) (shift OUTGOING_RES_LO 2)))
(defun (prc-modexp-pricing---big-quotient) (shift OUTGOING_RES_LO 3))
(defun (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP) (shift OUTGOING_RES_LO 4))
(defun (prc-modexp-pricing---big-numerator) (if-zero (prc-modexp-pricing---exponent-log-is-zero)
(* (prc-modexp-pricing---f-of-max) (prc-modexp-pricing---exponent-log))
(prc-modexp-pricing---f-of-max)))
(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---big-quotient_LT_GAS_CONST_MODEXP)
(prc-modexp-pricing---big-quotient)
GAS_CONST_MODEXP))

(defconstraint prc-modexp-pricing---check--is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
(call-to-ISZERO 0 0 (prc---r@c)))

(defconstraint prc-modexp-pricing---check-exponent-log-is-zero (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
(call-to-ISZERO 1 0 (prc-modexp-pricing---exponent-log)))

(defconstraint prc-modexp-pricing---div-max-xbs-ybs-plus-7-by-8 (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
(call-to-DIV 2
0
(+ (prc-modexp-pricing---max-xbs-ybs) 7)
0
8))

(defconstraint prc-modexp-pricing---div-big-numerator-by-quaddivisor (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
(call-to-DIV 3 0 (prc-modexp-pricing---big-numerator) 0 G_QUADDIVISOR))

(defconstraint prc-modexp-pricing---compare-big-quotient-against-GAS_CONST_MODEXP (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
(call-to-LT 4 0 (prc-modexp-pricing---big-quotient) 0 GAS_CONST_MODEXP))

(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
(call-to-LT 5 0 (prc---callee-gas) 0 (prc-modexp-pricing---precompile-cost)))

(defconstraint prc-modexp-pricing---justify-hub-predictions (:guard (* (assumption---fresh-new-stamp) (prc-modexp-pricing---standard-precondition)))
(begin (eq! (prc---ram-success)
(- 1 (shift OUTGOING_RES_LO 5)))
(if-zero (prc---ram-success)
(vanishes! (prc---return-gas))
(eq! (prc---return-gas) (- (prc---callee-gas) (prc-modexp-pricing---precompile-cost))))
(eq! (prc---r@c-nonzero) (- 1 OUTGOING_RES_LO))))
(defun (prc-modexp-pricing---max-mbs-bbs) [DATA 7])
;; ""



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; row i + 0: [email protected]() check ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint prc-modexp-pricing---r@c-iszero-check
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(call-to-ISZERO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK
0
(prc---r@c)
))

(defun (prc-modex-pricing---r@c-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___R@C_ISZERO_CHECK))



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; row i + 1: exponentLog.isZero() check ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint prc-modexp-pricing---check-exponent-log-is-zero
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(call-to-ISZERO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK
0
(prc-modexp-pricing---exponent-log)
))

(defun (prc-modexp-pricing---exponent-log-is-zero) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___EXPONENT_LOG_ISZERO_CHECK))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; row i + 2: ⌈ max(mbs, bbs) / 8 ⌉ compututation ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



(defconstraint prc-modexp-pricing---computing-ceiling-of-max-mbs-bbs-over-8
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(call-to-DIV ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8
0
(+ (prc-modexp-pricing---max-mbs-bbs) 7)
0
8
))

(defun (prc-modexp-pricing---ceiling-of-max-over-8) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CEILING_OF_MAX_OVER_8))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; row i + 3: comparing max(mbs, bbs) and 32 ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint prc-modexp-pricing---max-mbs-bbs-vs-32
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(call-to-LT ROFF___MODEXP_PRICING___MAX_VS_32
0
WORD_SIZE
0
(prc-modexp-pricing---max-mbs-bbs)
))

(defun (prc-modexp-pricing---word-cost-dominates) (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___MAX_VS_32))
(defun (prc-modexp-pricing---f-of-max) (* (prc-modexp-pricing---ceiling-of-max-over-8)
(prc-modexp-pricing---ceiling-of-max-over-8)))
(defun (prc-modexp-pricing---multiplication-complexity) (if-zero (force-bin (prc-modexp-pricing---word-cost-dominates))
16
(* 2 (prc-modexp-pricing---f-of-max))))
(defun (prc-modexp-pricing---iteration-count-or-1) (if-zero (force-bin (prc-modexp-pricing---exponent-log-is-zero))
(prc-modexp-pricing---exponent-log)
1))
(defun (prc-modexp-pricing---raw-cost) (* (prc-modexp-pricing---multiplication-complexity)
(prc-modexp-pricing---iteration-count-or-1)))



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; row i + 4: comparing raw_price to 500 ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



(defconstraint prc-modexp-pricing---compare-raw-cost-against-GAS_CONST_MODEXP-of-EIP-7823
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(call-to-LT ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST
0
(prc-modexp-pricing---raw-cost)
0
GAS_CONST_MODEXP_EIP_7823
))

(defun (prc-modexp-pricing---raw-cost-LT-min-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___RAW_COST_VS_MIN_COST)))
(defun (prc-modexp-pricing---precompile-cost) (if-zero (prc-modexp-pricing---raw-cost-LT-min-cost)
;; raw_cost_LT_min_cost ≡ faux
(prc-modexp-pricing---raw-cost)
;; raw_cost_LT_min_cost ≡ true
GAS_CONST_MODEXP_EIP_7823))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; row i + 5: comparing callee_gas to precopile_cost ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



(defconstraint prc-modexp-pricing---compare-call-gas-against-precompile-cost
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(call-to-LT ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST
0
(prc---callee-gas)
0
(prc-modexp-pricing---precompile-cost)
))

(defun (prc-modexp-pricing---callee-gas-LT-precompile-cost) (force-bin (shift OUTGOING_RES_LO ROFF___MODEXP_PRICING___CALLEE_GAS_VS_PRECOMPILE_COST)))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; justifying HUB predictions ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defconstraint prc-modexp-pricing---justify-hub-predictions---ram-success
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq! (prc---ram-success)
(- 1 (prc-modexp-pricing---callee-gas-LT-precompile-cost))
))

(defconstraint prc-modexp-pricing---justify-hub-predictions---return-gas
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-zero (force-bin (prc---ram-success))
;; ram_success ≡ faux
(vanishes! (prc---return-gas))
;; ram_success ≡ true
(eq! (prc---return-gas)
(- (prc---callee-gas)
(prc-modexp-pricing---precompile-cost)))
))

(defconstraint prc-modexp-pricing---justify-hub-predictions---r@c-nonzero
(:guard (prc-modexp-pricing---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq! (prc---r@c-nonzero)
(- 1 (prc-modex-pricing---r@c-is-zero))
))

Loading
Loading