EIP-7951: Precompile for secp256r1 Curve Support

Makefile

@@ -12,7 +12,8 @@ ALU := alu/add/add.zkasm alu/ext alu/mod alu/mul
 
 BIN := bin/bin.zkasm
 
-BLAKE2f_MODEXP_DATA := blake2fmodexpdata
+BLAKE2f_MODEXP_DATA_LONDON := blake2fmodexpdata/london
+BLAKE2f_MODEXP_DATA_OSAKA  := blake2fmodexpdata/osaka
 
 # constraints used in prod for LINEA, with linea block gas limit
 BLOCKDATA_LONDON := blockdata/london
@@ -53,7 +54,8 @@ LOG_DATA := logdata
 LOG_INFO_LONDON := loginfo/london
 LOG_INFO_CANCUN := loginfo/cancun
 
-MMU :=  mmu
+MMU_LONDON :=  mmu/london
+MMU_OSAKA  :=  mmu/osaka
 
 MMIO_LONDON := mmio/london
 MMIO_CANCUN := mmio/cancun
@@ -118,7 +120,6 @@ endef
 ZKEVM_MODULES_COMMON := ${CONSTANTS} \
 		 ${ALU} \
 		 ${BIN} \
-		 ${BLAKE2f_MODEXP_DATA} \
 		 ${BLOCKHASH} \
 		 ${EUC} \
 		 ${EXP} \
@@ -136,6 +137,7 @@ ZKEVM_MODULES_COMMON := ${CONSTANTS} \
 ZKEVM_MODULES_LONDON := ${ZKEVM_MODULES_COMMON} \
 		 ${CONSTANTS_LONDON} \
 		 ${TABLES_LONDON} \
+		 ${BLAKE2f_MODEXP_DATA_LONDON} \
 		 ${BLOCKDATA_LONDON} \
 		 ${EC_DATA_LONDON} \
 		 ${HUB_LONDON} \
@@ -155,6 +157,7 @@ ZKEVM_MODULES_LONDON := ${ZKEVM_MODULES_COMMON} \
 ZKEVM_MODULES_SHANGHAI := ${ZKEVM_MODULES_COMMON} \
 		 ${CONSTANTS_LONDON} \
 		 ${TABLES_LONDON} \
+		 ${BLAKE2f_MODEXP_DATA_LONDON} \
 		 ${BLOCKDATA_PARIS} \
 		 ${EC_DATA_LONDON} \
 		 ${HUB_SHANGHAI} \
@@ -169,8 +172,9 @@ ZKEVM_MODULES_SHANGHAI := ${ZKEVM_MODULES_COMMON} \
 		 ${TXN_DATA_SHANGHAI}
 
 ZKEVM_MODULES_CANCUN := ${ZKEVM_MODULES_COMMON} \
-         ${CONSTANTS_CANCUN} \
+		 ${CONSTANTS_CANCUN} \
 		 ${TABLES_CANCUN} \
+		 ${BLAKE2f_MODEXP_DATA_LONDON} \
 		 ${BLOCKDATA_CANCUN} \
 		 ${BLS_CANCUN} \
 		 ${EC_DATA_LONDON} \
@@ -189,6 +193,7 @@ ZKEVM_MODULES_CANCUN := ${ZKEVM_MODULES_COMMON} \
 ZKEVM_MODULES_PRAGUE := ${ZKEVM_MODULES_COMMON} \
 		 ${CONSTANTS_PRAGUE} \
 		 ${TABLES_PRAGUE} \
+		 ${BLAKE2f_MODEXP_DATA_LONDON} \
 		 ${BLOCKDATA_CANCUN} \
 		 ${BLS_PRAGUE} \
 		 ${EC_DATA_LONDON} \
@@ -207,6 +212,7 @@ ZKEVM_MODULES_PRAGUE := ${ZKEVM_MODULES_COMMON} \
 ZKEVM_MODULES_OSAKA := ${ZKEVM_MODULES_COMMON} \
 		 ${CONSTANTS_OSAKA} \
 		 ${TABLES_PRAGUE} \
+		 ${BLAKE2f_MODEXP_DATA_OSAKA} \
 		 ${BLOCKDATA_CANCUN} \
 		 ${BLS_PRAGUE} \
 		 ${EC_DATA_OSAKA} \

blake2fmodexpdata/osaka/columns.lisp

@@ -0,0 +1,18 @@
+(module blake2fmodexpdata)
+
+(defcolumns
+  (STAMP                :i16)
+  (ID                   :i32)
+  (PHASE                :byte)
+  (INDEX                :byte :display :dec)
+  (INDEX_MAX            :byte :display :dec)
+  (LIMB                 :i128 :display :bytes)
+  (IS_MODEXP_BASE       :binary@prove)
+  (IS_MODEXP_EXPONENT   :binary@prove)
+  (IS_MODEXP_MODULUS    :binary@prove)
+  (IS_MODEXP_RESULT     :binary@prove)
+  (IS_BLAKE_DATA        :binary@prove)
+  (IS_BLAKE_PARAMS      :binary@prove)
+  (IS_BLAKE_RESULT      :binary@prove)
+  )
+

blake2fmodexpdata/osaka/constants.lisp

@@ -0,0 +1,13 @@
+(module blake2fmodexpdata)
+
+(defconst
+  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
+  INDEX_MAX_MODEXP_RESULT   INDEX_MAX_MODEXP
+  INDEX_MAX_BLAKE_DATA      12
+  INDEX_MAX_BLAKE_PARAMS    1
+  INDEX_MAX_BLAKE_RESULT    3)
+
+

blake2fmodexpdata/osaka/constraints.lisp

@@ -0,0 +1,76 @@
+(module blake2fmodexpdata)
+
+(defun (flag-sum)
+  (+ IS_MODEXP_BASE
+     IS_MODEXP_EXPONENT
+     IS_MODEXP_MODULUS
+     IS_MODEXP_RESULT
+     IS_BLAKE_DATA
+     IS_BLAKE_PARAMS
+     IS_BLAKE_RESULT))
+
+(defun (phase-sum)
+  (+ (* PHASE_MODEXP_BASE IS_MODEXP_BASE)
+     (* PHASE_MODEXP_EXPONENT IS_MODEXP_EXPONENT)
+     (* PHASE_MODEXP_MODULUS IS_MODEXP_MODULUS)
+     (* PHASE_MODEXP_RESULT IS_MODEXP_RESULT)
+     (* PHASE_BLAKE_DATA IS_BLAKE_DATA)
+     (* PHASE_BLAKE_PARAMS IS_BLAKE_PARAMS)
+     (* PHASE_BLAKE_RESULT IS_BLAKE_RESULT)))
+
+(defun (index-max-sum)
+  (+ (* INDEX_MAX_MODEXP_BASE IS_MODEXP_BASE)
+     (* INDEX_MAX_MODEXP_EXPONENT IS_MODEXP_EXPONENT)
+     (* INDEX_MAX_MODEXP_MODULUS IS_MODEXP_MODULUS)
+     (* INDEX_MAX_MODEXP_RESULT IS_MODEXP_RESULT)
+     (* INDEX_MAX_BLAKE_DATA IS_BLAKE_DATA)
+     (* INDEX_MAX_BLAKE_PARAMS IS_BLAKE_PARAMS)
+     (* INDEX_MAX_BLAKE_RESULT IS_BLAKE_RESULT)))
+
+(defconstraint no-stamp-no-flag ()
+  (if-zero STAMP
+           (vanishes! (flag-sum))
+           (eq! (flag-sum) 1)))
+
+(defconstraint set-phase-and-index ()
+  (begin (eq! PHASE (phase-sum))
+         (eq! INDEX_MAX (index-max-sum))))
+
+(defconstraint stamp-constancies ()
+  (stamp-constancy STAMP ID))
+
+(defconstraint index-constancies (:guard INDEX)
+  (remained-constant! (phase-sum)))
+
+(defconstraint first-row (:domain {0})
+  (vanishes! STAMP))
+
+(defconstraint no-stamp-nothing ()
+  (if-zero STAMP
+           (begin (vanishes! ID)
+                  (vanishes! (next INDEX)))))
+
+(defun (stamp-increment)
+  (force-bin  (+ (* (- 1 IS_MODEXP_BASE) (next IS_MODEXP_BASE))
+                 (* (- 1 IS_BLAKE_DATA) (next IS_BLAKE_DATA)))))
+
+(defconstraint stamp-increases ()
+  (will-inc! STAMP (stamp-increment)))
+
+(defun (transition-bit)
+  (force-bin  (+ (* IS_MODEXP_BASE (next IS_MODEXP_EXPONENT))
+                 (* IS_MODEXP_EXPONENT (next IS_MODEXP_MODULUS))
+                 (* IS_MODEXP_MODULUS (next IS_MODEXP_RESULT))
+                 (* IS_MODEXP_RESULT
+                    (+ (next IS_MODEXP_BASE) (next IS_BLAKE_DATA)))
+                 (* IS_BLAKE_DATA (next IS_BLAKE_PARAMS))
+                 (* IS_BLAKE_PARAMS (next IS_BLAKE_RESULT))
+                 (* IS_BLAKE_RESULT
+                    (+ (next IS_MODEXP_BASE) (next IS_BLAKE_DATA))))))
+
+(defconstraint heartbeat (:guard STAMP)
+  (if-zero (- INDEX_MAX INDEX)
+           (eq! (transition-bit) 1)
+           (will-inc! INDEX 1)))
+
+

blake2fmodexpdata/osaka/lookups/blakemodexp_into_wcp.lisp

@@ -0,0 +1,28 @@
+(defun (blake2fmodexpdata-into-wcp-oob-into-wcp-activation-flag)
+  (force-bin (* (~ blake2fmodexpdata.STAMP)
+                (- blake2fmodexpdata.STAMP (prev blake2fmodexpdata.STAMP)))))
+
+(defclookup
+  blake2fmodexpdata-into-wcp
+  ;; target colums (in WCP)
+  (
+    wcp.ARG_1_HI
+    wcp.ARG_1_LO
+    wcp.ARG_2_HI
+    wcp.ARG_2_LO
+    wcp.RES
+    wcp.INST
+  )
+  ;; source selector
+  (blake2fmodexpdata-into-wcp-oob-into-wcp-activation-flag)
+  ;; source columns
+  (
+    0
+    (prev blake2fmodexpdata.ID)
+    0
+    blake2fmodexpdata.ID
+    1
+    EVM_INST_LT
+  ))
+
+

constants/constants.lisp

@@ -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
@@ -244,6 +245,7 @@
   GAS_CONST_BLS_MAP_FP2_TO_G2               23800
   GAS_CONST_BLS_PAIRING_CHECK               37700
   GAS_CONST_BLS_PAIRING_CHECK_PAIR          32600
+  GAS_CONST_P256_VERIFY                     6900
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;           ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;  EVM MISC ;;
@@ -270,6 +272,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 ;;
@@ -326,6 +329,7 @@
   PRECOMPILE_CALL_DATA_UNIT_SIZE___BLS_PAIRING_CHECK       384
   PRECOMPILE_CALL_DATA_SIZE___FP_TO_G1                      64
   PRECOMPILE_CALL_DATA_SIZE___FP2_TO_G2                    128
+  PRECOMPILE_CALL_DATA_SIZE___P256_VERIFY                  160
 
   PRC_ECPAIRING_SIZE                                       (* 6 WORD_SIZE)
   PRECOMPILE_CALL_DATA_SIZE___BLAKE2F                      213
@@ -340,6 +344,7 @@
   PRECOMPILE_RETURN_DATA_SIZE___BLS_PAIRING_CHECK           32
   PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP_TO_G1           128
   PRECOMPILE_RETURN_DATA_SIZE___BLS_MAP_FP2_TO_G2          256
+  PRECOMPILE_RETURN_DATA_SIZE___P256_VERIFY                 32
 
   PRC_BLS_G1_MSM_MAX_DISCOUNT                              519
   PRC_BLS_G2_MSM_MAX_DISCOUNT                              524
@@ -403,6 +408,8 @@
   PHASE_ECMUL_RESULT                        0x070B
   PHASE_ECPAIRING_DATA                      0x080A
   PHASE_ECPAIRING_RESULT                    0x080B
+  PHASE_P256_VERIFY_DATA                    0x100A
+  PHASE_P256_VERIFY_RESULT                  0x100B
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;                 ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; BLS DATA MODULE ;;
@@ -521,6 +528,7 @@
   OOB_INST_BLS_PAIRING_CHECK                0xFF0F
   OOB_INST_BLS_MAP_FP_TO_G1                 0xFF10
   OOB_INST_BLS_MAP_FP2_TO_G2                0xFF11
+  OOB_INST_P256_VERIFY                      0xF100
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;             ;;
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; RLP* MODULE ;;

ecdata/london/columns.lisp

@@ -36,12 +36,6 @@
   (G2_MEMBERSHIP_TEST_REQUIRED                   :binary@prove)
   (ACCEPTABLE_PAIR_OF_POINTS_FOR_PAIRING_CIRCUIT :binary@prove)
 
-  (CIRCUIT_SELECTOR_ECRECOVER      :binary@prove)
-  (CIRCUIT_SELECTOR_ECADD          :binary@prove)
-  (CIRCUIT_SELECTOR_ECMUL          :binary@prove)
-  (CIRCUIT_SELECTOR_ECPAIRING      :binary@prove)
-  (CIRCUIT_SELECTOR_G2_MEMBERSHIP  :binary@prove)
-
   (WCP_FLAG     :binary@prove)
   (WCP_ARG1_HI  :i128)
   (WCP_ARG1_LO  :i128)

ecdata/london/constraints.lisp

@@ -478,7 +478,6 @@
                                 (eq! P_is_point_at_infinity 1)
                                 (vanishes! P_is_point_at_infinity))))))
 
-;; Note: in the specs for simplicity we omit the last four arguments
 (defun (callToC1MembershipWCP k
                               _P_x_hi
                               _P_x_lo
@@ -492,7 +491,6 @@
          (callToLT (+ k 1) _P_y_hi _P_y_lo P_BN_HI P_BN_LO)
          (callToEQ (+ k 2) _P_y_square_hi _P_y_square_lo _P_x_cube_plus_three_hi _P_x_cube_plus_three_lo)))
 
-;; Note: in the specs for simplicity we omit the last four arguments
 (defun (callToC1MembershipEXT k
                               _P_x_hi
                               _P_x_lo
@@ -568,17 +566,17 @@
         (s_hi (shift LIMB 6))
         (s_lo (shift LIMB 7)))
        (begin (callToLT 0 r_hi r_lo SECP256K1N_HI SECP256K1N_LO)
-              (callToLT 1 0 0 r_hi r_lo)
+              (callToISZERO 1 r_hi r_lo)
               (callToLT 2 s_hi s_lo SECP256K1N_HI SECP256K1N_LO)
-              (callToLT 3 0 0 s_hi s_lo)
+              (callToISZERO 3 s_hi s_lo)
               (callToEQ 4 v_hi v_lo 0 27)
               (callToEQ 5 v_hi v_lo 0 28))))
 
 (defconstraint justify-success-bit-ecrecover (:guard (ecrecover-hypothesis))
   (let ((r_is_in_range WCP_RES)
-        (r_is_positive (next WCP_RES))
+        (r_is_positive (- 1 (next WCP_RES)))
         (s_is_in_range (shift WCP_RES 2))
-        (s_is_positive (shift WCP_RES 3))
+        (s_is_positive (- 1 (shift WCP_RES 3)))
         (v_is_27 (shift WCP_RES 4))
         (v_is_28 (shift WCP_RES 5))
         (internal_checks_passed (shift HURDLE INDEX_MAX_ECRECOVER_DATA)))
@@ -729,25 +727,20 @@
 ;; 3.7.3 Interface for ;;
 ;;       Gnark         ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;
-(defconstraint ecrecover-circuit-selector ()
-  (eq! CS_ECRECOVER (* ICP (is_ecrecover))))
+(defcomputedcolumn (CIRCUIT_SELECTOR_ECRECOVER :binary@prove) 
+  (* ICP (is_ecrecover)))
 
-(defconstraint ecadd-circuit-selector ()
-  (eq! CS_ECADD (* ICP (is_ecadd))))
+(defcomputedcolumn (CIRCUIT_SELECTOR_ECADD :binary@prove) 
+  (* ICP (is_ecadd)))
 
-(defconstraint ecmul-circuit-selector ()
-  (eq! CS_ECMUL (* ICP (is_ecmul))))
+(defcomputedcolumn (CIRCUIT_SELECTOR_ECMUL :binary@prove) 
+  (* ICP (is_ecmul)))
 
-(defconstraint ecpairing-circuit-selector ()
-  (begin 
-    (if-not-zero IS_ECPAIRING_DATA (eq! CS_ECPAIRING ACCPC))
-    (if-not-zero IS_ECPAIRING_RESULT (eq! CS_ECPAIRING (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING))))
-    (if-zero (is_ecpairing) (vanishes! CS_ECPAIRING))
-  )
-)
+(defcomputedcolumn (CIRCUIT_SELECTOR_ECPAIRING :binary@prove) 
+  (+ (* IS_ECPAIRING_DATA ACCPC) (* IS_ECPAIRING_RESULT (* SUCCESS_BIT (- 1 TRIVIAL_PAIRING)))))
 
-(defconstraint g2-membership-circuit-selector ()
-  (eq! CS_G2_MEMBERSHIP G2MTR))
+(defcomputedcolumn (CIRCUIT_SELECTOR_G2_MEMBERSHIP :binary@prove)
+  G2MTR)
 
 (defconstraint circuit-selectors-sum-binary ()
   (debug (is-binary (+ CS_ECRECOVER CS_ECADD CS_ECMUL CS_ECPAIRING CS_G2_MEMBERSHIP))))

ecdata/osaka/columns.lisp

@@ -10,14 +10,16 @@
   (INDEX_MAX    :i16)
   (SUCCESS_BIT  :binary@prove)
 
-  (IS_ECRECOVER_DATA    :binary@prove)
-  (IS_ECRECOVER_RESULT  :binary@prove)
-  (IS_ECADD_DATA        :binary@prove)
-  (IS_ECADD_RESULT      :binary@prove)
-  (IS_ECMUL_DATA        :binary@prove)
-  (IS_ECMUL_RESULT      :binary@prove)
-  (IS_ECPAIRING_DATA    :binary@prove)
-  (IS_ECPAIRING_RESULT  :binary@prove)
+  (IS_ECRECOVER_DATA     :binary@prove)
+  (IS_ECRECOVER_RESULT   :binary@prove)
+  (IS_ECADD_DATA         :binary@prove)
+  (IS_ECADD_RESULT       :binary@prove)
+  (IS_ECMUL_DATA         :binary@prove)
+  (IS_ECMUL_RESULT       :binary@prove)
+  (IS_ECPAIRING_DATA     :binary@prove)
+  (IS_ECPAIRING_RESULT   :binary@prove)
+  (IS_P256_VERIFY_DATA   :binary@prove)
+  (IS_P256_VERIFY_RESULT :binary@prove)
 
   (TOTAL_PAIRINGS                                :i16)
   (ACC_PAIRINGS                                  :i16)
@@ -36,12 +38,6 @@
   (G2_MEMBERSHIP_TEST_REQUIRED                   :binary@prove)
   (ACCEPTABLE_PAIR_OF_POINTS_FOR_PAIRING_CIRCUIT :binary@prove)
 
-  (CIRCUIT_SELECTOR_ECRECOVER      :binary@prove)
-  (CIRCUIT_SELECTOR_ECADD          :binary@prove)
-  (CIRCUIT_SELECTOR_ECMUL          :binary@prove)
-  (CIRCUIT_SELECTOR_ECPAIRING      :binary@prove)
-  (CIRCUIT_SELECTOR_G2_MEMBERSHIP  :binary@prove)
-
   (WCP_FLAG     :binary@prove)
   (WCP_ARG1_HI  :i128)
   (WCP_ARG1_LO  :i128)
@@ -71,6 +67,7 @@
   CS_ECADD         CIRCUIT_SELECTOR_ECADD
   CS_ECMUL         CIRCUIT_SELECTOR_ECMUL
   CS_ECPAIRING     CIRCUIT_SELECTOR_ECPAIRING
+  CS_P256_VERIFY   CIRCUIT_SELECTOR_P256_VERIFY
   CS_G2_MEMBERSHIP CIRCUIT_SELECTOR_G2_MEMBERSHIP)