Skip to content

EIP 7823 and 7883 --- Osaka MODEXP changes #823

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 and 7883 --- Osaka MODEXP changes #823

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
2f23e74
EIP-7823: Set upper bounds for `MODEXP` --- `OOB` side (#813)
OlivierBBB Nov 7, 2025
40959eb
EIP-7823: Set upper bounds for `MODEXP` --- `BLAKE_MODEXP` side (#812)
OlivierBBB Nov 7, 2025
c483d9e
EIP-7823: Set upper bounds for `MODEXP` --- `MMU` side (#814)
OlivierBBB Nov 7, 2025
78ad636
Automatic vanishing constraints of `misc/XXX_?` columns when `misc/XX…
OlivierBBB Nov 7, 2025
00e31bc
EIP-7823: Set upper bounds for `MODEXP` --- `HUB` side (#815)
OlivierBBB Nov 7, 2025
9914745
fix
OlivierBBB Nov 7, 2025
0d92723
fix: prague and osaka variants of the BLAKE_MODEXP module
OlivierBBB Nov 7, 2025
d02b8ca
ras: renaming
OlivierBBB Nov 7, 2025
fdfa1a9
feat: update Makefile
OlivierBBB Nov 7, 2025
14de596
ras: remove old file
OlivierBBB Nov 7, 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: 1 addition & 1 deletion blake2fmodexpdata/constants.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(module blake2fmodexpdata)

(defconst
INDEX_MAX_MODEXP 31
INDEX_MAX_MODEXP 63
INDEX_MAX_MODEXP_BASE INDEX_MAX_MODEXP
INDEX_MAX_MODEXP_EXPONENT INDEX_MAX_MODEXP
INDEX_MAX_MODEXP_MODULUS INDEX_MAX_MODEXP
Expand Down
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 @@ -228,6 +228,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 @@ -270,6 +271,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 hub/osaka/columns/miscellaneous.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@

;; EXP columns (DONE)
( EXP_INST :i16 )
( EXP_DATA :array [5] :i128 )
( EXP_DATA :array [5] :i128 ) ;;""

;; MMU columns (DONE)
( MMU_INST :i16 :display :hex)
Expand Down Expand Up @@ -52,7 +52,7 @@

;; OOB columns
(OOB_INST :i16 )
(OOB_DATA :array[1:10] :i128 )
(OOB_DATA :array[1:10] :i128 ) ;;""

;; STP columns
( STP_INSTRUCTION :byte )
Expand Down
43 changes: 43 additions & 0 deletions ...nstruction-handling/call/precompiles/modexp/common/__01__call_data_size_analysis_row.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
(module hub)

;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;
;;;; ;;;;
;;;; X.Y CALL ;;;;
;;;; ;;;;
;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; X.Y.Z.4 MODEXP common processing ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; CALL_DATA_SIZE analysis row ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-module-flags
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---cds-analysis)
MISC_WEIGHT_OOB))


(defconstraint precompile-processing---MODEXP---call-data-size-analysis-row---setting-OOB-instruction
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(set-OOB-instruction---modexp-cds precompile-processing---MODEXP---misc-row-offset---cds-analysis ;; row offset
(precompile-processing---dup-cds))) ;; call data size


(defun (precompile-processing---MODEXP---extract-bbs) (shift [misc/OOB_DATA 3] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; ""
(defun (precompile-processing---MODEXP---extract-ebs) (shift [misc/OOB_DATA 4] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; ""
(defun (precompile-processing---MODEXP---extract-mbs) (shift [misc/OOB_DATA 5] precompile-processing---MODEXP---misc-row-offset---cds-analysis)) ;; ""
74 changes: 74 additions & 0 deletions ...traints/instruction-handling/call/precompiles/modexp/common/__02__bbs_extraction_row.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
(module hub)

;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;
;;;; ;;;;
;;;; X.Y CALL ;;;;
;;;; ;;;;
;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; X.Y.Z.4 MODEXP common processing ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; bbs extraction and analysis row ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-misc-module-flags
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)
(+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-bbs))
MISC_WEIGHT_OOB)
))


(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-MMU-instruction
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)
(set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset
CONTEXT_NUMBER ;; source ID
;; tgt_id ;; target ID
;; aux_id ;; auxiliary ID
;; src_offset_hi ;; source offset high
0 ;; source offset low
;; tgt_offset_lo ;; target offset low
;; size ;; size
(precompile-processing---dup-cdo) ;; reference offset
(precompile-processing---dup-cds) ;; reference size
;; success_bit ;; success bit
(shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE
(shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE
;; exo_sum ;; weighted exogenous module flag sum
;; phase ;; phase
)))

(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)))
(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)))


(defconstraint precompile-processing---MODEXP---bbs-extraction-and-analysis---setting-OOB-instruction
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis ;; offset
(precompile-processing---MODEXP---bbs-hi) ;; high part of some {b,e,m}bs
(precompile-processing---MODEXP---bbs-lo) ;; low part of some {b,e,m}bs
0 ;; low part of some {b,e,m}bs
0 ;; bit indicating whether to compute max(xbs, ybs) or not
))


(defun (precompile-processing---MODEXP---bbs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; ""
(defun (precompile-processing---MODEXP---bbs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---bbs-extraction-and-analysis)) ;; ""
(defun (precompile-processing---MODEXP---bbs-normalized) (* (precompile-processing---MODEXP---bbs-lo)
(precompile-processing---MODEXP---bbs-within-bounds)))
75 changes: 75 additions & 0 deletions ...traints/instruction-handling/call/precompiles/modexp/common/__03__ebs_extraction_row.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
(module hub)

;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;
;;;; ;;;;
;;;; X.Y CALL ;;;;
;;;; ;;;;
;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; X.Y.Z.4 MODEXP common processing ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ebs extraction and analysis row ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-misc-module-flags
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eq! (weighted-MISC-flag-sum precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)
(+ (* MISC_WEIGHT_MMU (precompile-processing---MODEXP---extract-ebs))
MISC_WEIGHT_OOB)
))


(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-MMU-instruction
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(if-not-zero (shift misc/MMU_FLAG precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)
(set-MMU-instruction---right-padded-word-extraction precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset
CONTEXT_NUMBER ;; source ID
;; tgt_id ;; target ID
;; aux_id ;; auxiliary ID
;; src_offset_hi ;; source offset high
32 ;; source offset low
;; tgt_offset_lo ;; target offset low
;; size ;; size
(precompile-processing---dup-cdo) ;; reference offset
(precompile-processing---dup-cds) ;; reference size
;; success_bit ;; success bit
(shift misc/MMU_LIMB_1 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 1 ;; TODO: remove SELF REFERENCE
(shift misc/MMU_LIMB_2 precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis) ;; limb 2 ;; TODO: remove SELF REFERENCE
;; exo_sum ;; weighted exogenous module flag sum
;; phase ;; phase
)))


(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)))
(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)))


(defconstraint precompile-processing---MODEXP---ebs-extraction-and-analysis---setting-OOB-instruction
(:guard (precompile-processing---MODEXP---standard-precondition))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(set-OOB-instruction---modexp-xbs precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis ;; offset
(precompile-processing---MODEXP---ebs-hi) ;; high part of some {b,e,m}bs
(precompile-processing---MODEXP---ebs-lo) ;; low part of some {b,e,m}bs
0 ;; low part of some {b,e,m}bs
0 ;; bit indicating whether to compute max(xbs, ybs) or not
))


(defun (precompile-processing---MODEXP---ebs-within-bounds) (shift [misc/OOB_DATA 9] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis))
(defun (precompile-processing---MODEXP---ebs-out-of-bounds) (shift [misc/OOB_DATA 10] precompile-processing---MODEXP---misc-row-offset---ebs-extraction-and-analysis)) ;; ""
(defun (precompile-processing---MODEXP---ebs-normalized) (* (precompile-processing---MODEXP---ebs-lo)
(precompile-processing---MODEXP---ebs-within-bounds)))
Loading
Loading