Eip 2537 precompile for bls12 381 curve operations

Makefile

@@ -23,6 +23,13 @@ BLOCKDATA_CANCUN := blockdata/cancun
 
 BLOCKHASH := blockhash
 
+BLS_CANCUN := $(wildcard bls/cancun/*.lisp) \
+	       $(wildcard bls/cancun/generalities/*.lisp) \
+	       $(wildcard bls/cancun/lookups/*.lisp) \
+	       $(wildcard bls/cancun/specialized_constraints/*.lisp) \
+	       $(wildcard bls/cancun/top_level_flags_mint_mext_wtrv_wnon/*.lisp) \
+		   $(wildcard bls/cancun/utilities/*.lisp) \
+
 CONSTANTS := constants/constants.lisp
 
 EC_DATA := ecdata
@@ -143,6 +150,7 @@ ZKEVM_MODULES_SHANGHAI := ${ZKEVM_MODULES_COMMON} \
 
 ZKEVM_MODULES_CANCUN := ${ZKEVM_MODULES_COMMON} \
  		 ${BLOCKDATA_CANCUN} \
+		 ${BLS_CANCUN} \
 		 ${HUB_CANCUN} \
 		 ${OOB_SHANGHAI} \
 		 ${INST_DECODER_CANCUN} \

bls/cancun/circuit_selectors.lisp

@@ -0,0 +1,67 @@
+(module bls)
+
+(defun (cs_G1MT_for_g1_msm)
+    (* DATA_BLS_G1_MSM_FLAG IS_FIRST_INPUT MEXT_BIT))
+
+(defun (cs_G1MT_for_g2_msm)
+    (* DATA_BLS_G2_MSM_FLAG IS_FIRST_INPUT MEXT_BIT))
+
+(defun (cs_G1MT_for_pairing_malformed)
+    (* DATA_BLS_PAIRING_CHECK_FLAG IS_FIRST_INPUT MEXT_BIT))
+
+(defun (cs_G2MT_for_pairing_malformed)
+    (* DATA_BLS_PAIRING_CHECK_FLAG IS_SECOND_INPUT MEXT_BIT))
+
+(defun (cs_G1MT_for_pairing_wellformed)
+    (* DATA_BLS_PAIRING_CHECK_FLAG IS_FIRST_INPUT (- 1 NONTRIVIAL_POP_BIT) (- 1 IS_INFINITY) (wellformed_data)))
+
+(defun (cs_G2MT_for_pairing_wellformed)
+    (* DATA_BLS_PAIRING_CHECK_FLAG IS_SECOND_INPUT (- 1 NONTRIVIAL_POP_BIT) (- 1 IS_INFINITY) (wellformed_data)))  
+
+(defun (is_nontrivial_pairing_data_or_result)
+    (+ (* DATA_BLS_PAIRING_CHECK_FLAG NONTRIVIAL_POP_BIT) RSLT_BLS_PAIRING_CHECK_FLAG))  
+
+(defconstraint set-cs-c1-membership ()
+    (eq! CS_G1_MEMBERSHIP (* MEXT_BIT DATA_BLS_G1_ADD_FLAG)))
+
+(defconstraint set-cs-c2-membership ()
+    (eq! CS_G2_MEMBERSHIP (* MEXT_BIT DATA_BLS_G2_MSM_FLAG)))
+
+(defconstraint set-cs-g1-membership ()
+    (eq! CS_G1_MEMBERSHIP 
+    (+ (cs_G1MT_for_g1_msm)
+       (cs_G1MT_for_pairing_malformed)
+       (cs_G1MT_for_pairing_wellformed))))
+
+(defconstraint set-cs-g2-membership ()
+    (eq! CS_G2_MEMBERSHIP 
+    (+ (cs_G1MT_for_g2_msm)
+       (cs_G2MT_for_pairing_malformed)
+       (cs_G2MT_for_pairing_wellformed))))
+
+(defconstraint set-cs-point-evaluation ()
+    (eq! CS_POINT_EVALUATION (* WNON (is_point_evaluation))))
+
+(defconstraint set-cs-point-evaluation-failure ()
+    (eq! CS_POINT_EVALUATION_FAILURE (* MEXT (is_point_evaluation))))
+
+(defconstraint set-cs-g1-add ()
+    (eq! CS_BLS_G1_ADD (* WNON (is_g1_add))))
+
+(defconstraint set-cs-g1-msm ()
+    (eq! CS_BLS_G1_MSM (* WNON (is_g1_msm))))
+
+(defconstraint set-cs-g2-add ()
+    (eq! CS_BLS_G2_ADD (* WNON (is_g2_add))))
+
+(defconstraint set-cs-g2-msm ()
+    (eq! CS_BLS_G2_MSM (* WNON (is_g2_msm))))
+
+(defconstraint set-cs-pairing-check ()
+    (eq! CS_BLS_PAIRING_CHECK (* WNON (is_nontrivial_pairing_data_or_result))))
+
+(defconstraint set-cs-map-fp-to-g1 ()
+    (eq! CS_BLS_MAP_FP_TO_G1 (* WNON (is_map_fp_to_g1))))
+
+(defconstraint set-cs-map-fp2-to-g2 ()
+    (eq! CS_BLS_MAP_FP2_TO_G2 (* WNON (is_map_fp2_to_g2))))

bls/cancun/columns.lisp

@@ -0,0 +1,102 @@
+(module bls)
+
+(defcolumns
+  (STAMP        :i32)
+  (ID           :i32)
+  (TOTAL_SIZE   :i16)
+  (INDEX        :i16)
+  (INDEX_MAX    :i16)
+  (LIMB         :i128)
+  (PHASE        :i16)
+  (SUCCESS_BIT  :binary@prove)
+
+  (CT           :i4)
+  (CT_MAX       :i4)
+
+  (DATA_POINT_EVALUATION_FLAG             :binary@prove) 
+  (DATA_BLS_G1_ADD_FLAG                   :binary@prove)
+  (DATA_BLS_G1_MSM_FLAG                   :binary@prove)
+  (DATA_BLS_G2_ADD_FLAG                   :binary@prove)
+  (DATA_BLS_G2_MSM_FLAG                   :binary@prove)
+  (DATA_BLS_PAIRING_CHECK_FLAG            :binary@prove)
+  (DATA_BLS_MAP_FP_TO_G1_FLAG             :binary@prove)
+  (DATA_BLS_MAP_FP2_TO_G2_FLAG            :binary@prove)
+
+  (RSLT_POINT_EVALUATION_FLAG             :binary@prove)
+  (RSLT_BLS_G1_ADD_FLAG                   :binary@prove)
+  (RSLT_BLS_G1_MSM_FLAG                   :binary@prove)
+  (RSLT_BLS_G2_ADD_FLAG                   :binary@prove)
+  (RSLT_BLS_G2_MSM_FLAG                   :binary@prove)
+  (RSLT_BLS_PAIRING_CHECK_FLAG            :binary@prove)
+  (RSLT_BLS_MAP_FP_TO_G1_FLAG             :binary@prove)
+  (RSLT_BLS_MAP_FP2_TO_G2_FLAG            :binary@prove)
+
+  (ACC_INPUTS                                    :i16)
+  (BYTE_DELTA                                    :byte@prove)
+
+  (MALFORMED_DATA_INTERNAL_BIT                    :binary@prove)
+  (MALFORMED_DATA_INTERNAL_ACC                    :binary@prove)
+  (MALFORMED_DATA_INTERNAL_ACC_TOT                :binary@prove)
+  (MALFORMED_DATA_EXTERNAL_BIT                    :binary@prove)
+  (MALFORMED_DATA_EXTERNAL_ACC                    :binary@prove)
+  (MALFORMED_DATA_EXTERNAL_ACC_TOT                :binary@prove)
+  (WELLFORMED_DATA_TRIVIAL                        :binary@prove)
+  (WELLFORMED_DATA_NONTRIVIAL                     :binary@prove)
+
+  (IS_FIRST_INPUT                                :binary@prove)
+  (IS_SECOND_INPUT                               :binary@prove)
+  (IS_INFINITY                                   :binary@prove)
+  (NONTRIVIAL_PAIR_OF_POINTS_BIT                 :binary@prove)
+  (NONTRIVIAL_PAIR_OF_POINTS_ACC                 :binary@prove)
+
+  (CIRCUIT_SELECTOR_POINT_EVALUATION           :binary@prove)
+  (CIRCUIT_SELECTOR_POINT_EVALUATION_FAILURE   :binary@prove)
+  (CIRCUIT_SELECTOR_C1_MEMBERSHIP              :binary@prove)
+  (CIRCUIT_SELECTOR_G1_MEMBERSHIP              :binary@prove)
+  (CIRCUIT_SELECTOR_C2_MEMBERSHIP              :binary@prove)
+  (CIRCUIT_SELECTOR_G2_MEMBERSHIP              :binary@prove)
+  (CIRCUIT_SELECTOR_BLS_PAIRING_CHECK          :binary@prove)
+  (CIRCUIT_SELECTOR_BLS_G1_ADD                 :binary@prove)
+  (CIRCUIT_SELECTOR_BLS_G2_ADD                 :binary@prove)
+  (CIRCUIT_SELECTOR_BLS_G1_MSM                 :binary@prove)
+  (CIRCUIT_SELECTOR_BLS_G2_MSM                 :binary@prove)
+  (CIRCUIT_SELECTOR_BLS_MAP_FP_TO_G1           :binary@prove)
+  (CIRCUIT_SELECTOR_BLS_MAP_FP2_TO_G2          :binary@prove)
+
+  (WCP_FLAG     :binary@prove)
+  (WCP_ARG1_HI  :i128)
+  (WCP_ARG1_LO  :i128)
+  (WCP_ARG2_HI  :i128)
+  (WCP_ARG2_LO  :i128)
+  (WCP_RES      :binary)
+  (WCP_INST     :byte :display :opcode)
+)
+
+;; aliases
+(defalias
+  MINT_BIT                      MALFORMED_DATA_INTERNAL_BIT
+  MINT_ACC                      MALFORMED_DATA_INTERNAL_ACC
+  MINT                          MALFORMED_DATA_INTERNAL_ACC_TOT
+  MEXT_BIT                      MALFORMED_DATA_EXTERNAL_BIT
+  MEXT_ACC                      MALFORMED_DATA_EXTERNAL_ACC
+  MEXT                          MALFORMED_DATA_EXTERNAL_ACC_TOT
+  WTRV                          WELLFORMED_DATA_TRIVIAL
+  WNON                          WELLFORMED_DATA_NONTRIVIAL
+  NONTRIVIAL_POP_BIT            NONTRIVIAL_PAIR_OF_POINTS_BIT
+  NONTRIVIAL_POP_ACC            NONTRIVIAL_PAIR_OF_POINTS_ACC
+  CS_POINT_EVALUATION           CIRCUIT_SELECTOR_POINT_EVALUATION
+  CS_POINT_EVALUATION_FAILURE   CIRCUIT_SELECTOR_POINT_EVALUATION_FAILURE
+  CS_C1_MEMBERSHIP              CIRCUIT_SELECTOR_C1_MEMBERSHIP
+  CS_G1_MEMBERSHIP              CIRCUIT_SELECTOR_G1_MEMBERSHIP
+  CS_C2_MEMBERSHIP              CIRCUIT_SELECTOR_C2_MEMBERSHIP
+  CS_G2_MEMBERSHIP              CIRCUIT_SELECTOR_G2_MEMBERSHIP
+  CS_BLS_PAIRING_CHECK          CIRCUIT_SELECTOR_BLS_PAIRING_CHECK
+  CS_BLS_G1_ADD                 CIRCUIT_SELECTOR_BLS_G1_ADD
+  CS_BLS_G2_ADD                 CIRCUIT_SELECTOR_BLS_G2_ADD
+  CS_BLS_G1_MSM                 CIRCUIT_SELECTOR_BLS_G1_MSM
+  CS_BLS_G2_MSM                 CIRCUIT_SELECTOR_BLS_G2_MSM
+  CS_BLS_MAP_FP_TO_G1           CIRCUIT_SELECTOR_BLS_MAP_FP_TO_G1
+  CS_BLS_MAP_FP2_TO_G2          CIRCUIT_SELECTOR_BLS_MAP_FP2_TO_G2
+)
+
+

bls/cancun/constants.lisp

@@ -0,0 +1,36 @@
+(module bls)
+
+(defconst
+  POINT_EVALUATION_PRIME_HI                      0x73eda753299d7d483339d80809a1d805        
+  POINT_EVALUATION_PRIME_LO                      0x1b4d2c3f4b6a0c7e8f3f5a0e9d1b2c3f
+  BLS_PRIME_3                                    0x00000000000000000000000000000000
+  BLS_PRIME_2                                    0x1a0111ea397fe69a4b1ba7b6434bacd7
+  BLS_PRIME_1                                    0x64774b84f38512bf6730d2a0f6b0f624
+  BLS_PRIME_0                                    0x1eabfffeb153ffffb9feffffffffaaab
+
+  INDEX_MAX_DATA_POINT_EVALUATION                11
+  INDEX_MAX_RSLT_POINT_EVALUATION                3
+  INDEX_MAX_DATA_G1_ADD                          15
+  INDEX_MAX_RSLT_G1_ADD                          7
+  INDEX_MAX_DATA_G1_MSM_MIN                      9
+  INDEX_MAX_RSLT_G1_MSM                          7
+  INDEX_MAX_DATA_G2_ADD                          31
+  INDEX_MAX_RSLT_G2_ADD                          15
+  INDEX_MAX_DATA_G2_MSM_MIN                      17
+  INDEX_MAX_RSLT_G2_MSM                          15
+  INDEX_MAX_DATA_PAIRING_CHECK_MIN               23
+  INDEX_MAX_RSLT_PAIRING_CHECK                   1
+  INDEX_MAX_DATA_MAP_FP_TO_G1                    3
+  INDEX_MAX_RSLT_MAP_FP_TO_G1                    7
+  INDEX_MAX_DATA_MAP_FP2_TO_G2                   7
+  INDEX_MAX_RSLT_MAP_FP2_TO_G2                   15
+
+  CT_MAX_POINT_EVALUATION                        11
+  CT_MAX_SMALL_POINT                             7
+  CT_MAX_LARGE_POINT                             15
+  CT_MAX_SCALAR                                  1
+  CT_MAX_MAP_FP_TO_G1                            3
+  CT_MAX_MAP_FP2_TO_G2                           7
+)
+
+

bls/cancun/generalities/constancy_conditions.lisp

@@ -0,0 +1,24 @@
+(module bls)
+
+(defconstraint stamp-constancy ()
+  (begin (stamp-constancy STAMP ID)
+         (stamp-constancy STAMP SUCCESS_BIT)
+         (stamp-constancy STAMP MINT)
+         (stamp-constancy STAMP MEXT)
+         (stamp-constancy STAMP WTRV)
+         (stamp-constancy STAMP WNON)))
+
+(defconstraint counter-constancy ()
+  (begin (counter-constancy INDEX PHASE) ;; NOTE: PHASE and INDEX_MAX are said to be index-constant
+         (counter-constancy INDEX INDEX_MAX)
+         (counter-constancy CT CT_MAX)
+         (counter-constancy CT IS_INFINITY)
+         (counter-constancy CT ACC_INPUTS)
+         (counter-constancy CT NONTRIVIAL_POP_ACC)
+         (counter-constancy CT MEXT_BIT)
+         (counter-constancy CT MEXT_ACC)))
+
+(defconstraint pair-of-inputs-constancy ()
+  (if-not-zero ACC_INPUTS
+               (if (will-remain-constant! ACC_INPUTS)
+                   (will-remain-constant! NONTRIVIAL_POP_BIT))))

bls/cancun/generalities/constraining_address_sum.lisp

@@ -0,0 +1,14 @@
+(module bls)
+
+(defun (address_sum)
+    (+ (* 10 (is_point_evaluation))
+       (* 11 (is_g1_add))
+       (* 12 (is_g1_msm))
+       (* 13 (is_g2_add))
+       (* 14 (is_g2_msm))
+       (* 15 (is_pairing_check))
+       (* 16 (is_map_fp_to_g1))
+       (* 17 (is_map_fp2_to_g2))))
+
+(defconstraint stamp-constancy ()
+    (stamp-constancy STAMP (address_sum)))

bls/cancun/generalities/constraining_flag_sum.lisp

@@ -0,0 +1,47 @@
+(module bls)
+
+(defun (is_point_evaluation)
+    (+ DATA_POINT_EVALUATION_FLAG RSLT_POINT_EVALUATION_FLAG))
+
+(defun (is_g1_add)
+    (+ DATA_BLS_G1_ADD_FLAG RSLT_BLS_G1_ADD_FLAG))
+
+(defun (is_g1_msm)
+    (+ DATA_BLS_G1_MSM_FLAG RSLT_BLS_G1_MSM_FLAG))
+
+(defun (is_g2_add)
+    (+ DATA_BLS_G2_ADD_FLAG RSLT_BLS_G2_ADD_FLAG))
+
+(defun (is_g2_msm)
+    (+ DATA_BLS_G2_MSM_FLAG RSLT_BLS_G2_MSM_FLAG))
+
+(defun (is_pairing_check)
+    (+ DATA_BLS_PAIRING_CHECK_FLAG RSLT_BLS_PAIRING_CHECK_FLAG))
+
+(defun (is_map_fp_to_g1)
+    (+ DATA_BLS_MAP_FP_TO_G1_FLAG RSLT_BLS_MAP_FP_TO_G1_FLAG))
+
+(defun (is_map_fp2_to_g2)
+    (+ DATA_BLS_MAP_FP2_TO_G2_FLAG RSLT_BLS_MAP_FP2_TO_G2_FLAG))
+
+(defun (flag_sum)
+    (+ (is_point_evaluation)
+       (is_g1_add)
+       (is_g1_msm)
+       (is_g2_add)
+       (is_g2_msm)
+       (is_pairing_check)
+       (is_map_fp_to_g1)
+       (is_map_fp2_to_g2)))
+
+(defconstraint first-row-sanity-check (:domain {0})
+    (debug (vanishes! (flag_sum))))
+
+(defconstraint non-decreasing-sanity-check ()
+    (debug (if-not-zero (flag_sum) (next (eq! (flag_sum) 1)))))
+
+(defconstraint flag-sum-when-stamp-is-zero ()
+    (if-zero STAMP (vanishes! (flag_sum))))
+
+(defconstraint flag-sum-when-stamp-is-not-zero ()
+    (if-not-zero STAMP (eq! (flag_sum) 1)))

bls/cancun/generalities/constraints_for_bls_stamp.lisp

@@ -0,0 +1,11 @@
+(module bls)
+
+(defconstraint first-row (:domain {0})
+  (vanishes! STAMP))
+
+(defconstraint stamp-increment-sanity-check ()
+  (begin
+    (debug (or! (will-remain-constant! STAMP) (will-inc! STAMP 1))))) ;; implied by the constraint below
+
+(defconstraint stamp-increment ()
+  (eq! (next STAMP) (+ STAMP (transition_to_data))))

bls/cancun/generalities/constraints_for_ct.lisp

@@ -0,0 +1,12 @@
+(module bls)
+
+(defconstraint vanishing-values ()
+  (if-zero (flag_sum)
+           (begin (vanishes! CT_MAX)                 
+                  (vanishes! CT)
+                  (debug (vanishes! (next CT))))))
+
+(defconstraint ct-increment ()
+  (if-eq-else CT CT_MAX
+              (vanishes! (next CT))
+              (eq! (next CT) (+ 1 CT))))

bls/cancun/generalities/id_increment_constraints.lisp

@@ -0,0 +1,11 @@
+(module bls)
+
+(defconstraint id-increment ()
+  (if-not-zero (- (next STAMP) STAMP)
+               (eq! (next ID)
+                    (+ ID
+                       1
+                       (+ (* 256 256 256 (next BYTE_DELTA))
+                          (* 256 256 (shift BYTE_DELTA 2))
+                          (* 256 (shift BYTE_DELTA 3))
+                          (shift BYTE_DELTA 4))))))

bls/cancun/generalities/legal_transition_constraints.lisp

@@ -0,0 +1,37 @@
+(module bls)
+
+(defun (same_data_to_data)
+    (+ (* DATA_POINT_EVALUATION_FLAG (next DATA_POINT_EVALUATION_FLAG))
+       (* DATA_BLS_G1_ADD_FLAG (next DATA_BLS_G1_ADD_FLAG))
+       (* DATA_BLS_G1_MSM_FLAG (next DATA_BLS_G1_MSM_FLAG))
+       (* DATA_BLS_G2_ADD_FLAG (next DATA_BLS_G2_ADD_FLAG))
+       (* DATA_BLS_G1_MSM_FLAG (next DATA_BLS_G2_ADD_FLAG))
+       (* DATA_BLS_PAIRING_CHECK_FLAG (next DATA_BLS_PAIRING_CHECK_FLAG))
+       (* DATA_BLS_MAP_FP_TO_G1_FLAG (next DATA_BLS_MAP_FP_TO_G1_FLAG))
+       (* DATA_BLS_MAP_FP2_TO_G2_FLAG (next DATA_BLS_MAP_FP2_TO_G2_FLAG))))
+
+(defun (same_data_to_result)
+    (+ (* DATA_POINT_EVALUATION_FLAG (next RSLT_POINT_EVALUATION_FLAG))
+       (* DATA_BLS_G1_ADD_FLAG (next RSLT_BLS_G1_ADD_FLAG))
+       (* DATA_BLS_G1_MSM_FLAG (next RSLT_BLS_G1_MSM_FLAG))
+       (* DATA_BLS_G2_ADD_FLAG (next RSLT_BLS_G2_ADD_FLAG))
+       (* DATA_BLS_G1_MSM_FLAG (next RSLT_BLS_G2_ADD_FLAG))
+       (* DATA_BLS_PAIRING_CHECK_FLAG (next RSLT_BLS_PAIRING_CHECK_FLAG))
+       (* DATA_BLS_MAP_FP_TO_G1_FLAG (next RSLT_BLS_MAP_FP_TO_G1_FLAG))
+       (* DATA_BLS_MAP_FP2_TO_G2_FLAG (next RSLT_BLS_MAP_FP2_TO_G2_FLAG))))
+
+(defun (same_result_to_result)
+    (+ (* RSLT_POINT_EVALUATION_FLAG (next RSLT_POINT_EVALUATION_FLAG))
+       (* RSLT_BLS_G1_ADD_FLAG (next RSLT_BLS_G1_ADD_FLAG))
+       (* RSLT_BLS_G1_MSM_FLAG (next RSLT_BLS_G1_MSM_FLAG))
+       (* RSLT_BLS_G2_ADD_FLAG (next RSLT_BLS_G2_ADD_FLAG))
+       (* RSLT_BLS_G1_MSM_FLAG (next RSLT_BLS_G2_ADD_FLAG))
+       (* RSLT_BLS_PAIRING_CHECK_FLAG (next RSLT_BLS_PAIRING_CHECK_FLAG))
+       (* RSLT_BLS_MAP_FP_TO_G1_FLAG (next RSLT_BLS_MAP_FP_TO_G1_FLAG))
+       (* RSLT_BLS_MAP_FP2_TO_G2_FLAG (next RSLT_BLS_MAP_FP2_TO_G2_FLAG))))
+
+(defconstraint legal-transitions ()
+    (eq! (+ (same_data_to_data)
+            (same_data_to_result)
+            (same_result_to_result)
+            (transition_to_data)) 1))