Eip 2537 precompile for bls12 381 curve operations

Makefile

@@ -23,6 +23,8 @@ BLOCKDATA := $(wildcard blockdata/*.lisp) \
 
 BLOCKHASH := blockhash
 
+BLS := bls
+
 CONSTANTS := constants/constants.lisp
 
 EC_DATA := ecdata
@@ -101,6 +103,7 @@ ZKEVM_MODULES_COMMON := ${CONSTANTS} \
 		 ${BLAKE2f_MODEXP_DATA} \
 		 ${BLOCKDATA} \
 		 ${BLOCKHASH} \
+		 ${BLS} \
 		 ${EC_DATA} \
 		 ${EUC} \
 		 ${EXP} \

bls/columns.lisp

@@ -0,0 +1,100 @@
+(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_G1_ADD_FLAG                   :binary@prove)
+  (DATA_G1_MSM_FLAG                   :binary@prove)
+  (DATA_G2_ADD_FLAG                   :binary@prove)
+  (DATA_G2_MSM_FLAG                   :binary@prove)
+  (DATA_PAIRING_CHECK_FLAG            :binary@prove)
+  (DATA_MAP_FP_TO_G1_FLAG             :binary@prove)
+  (DATA_MAP_FP2_TO_G2_FLAG            :binary@prove)
+
+  (RSLT_POINT_EVALUATION_FLAG         :binary@prove)
+  (RSLT_G1_ADD_FLAG                   :binary@prove)
+  (RSLT_G1_MSM_FLAG                   :binary@prove)
+  (RSLT_G2_ADD_FLAG                   :binary@prove)
+  (RSLT_G2_MSM_FLAG                   :binary@prove)
+  (RSLT_PAIRING_CHECK_FLAG            :binary@prove)
+  (RSLT_MAP_FP_TO_G1_FLAG             :binary@prove)
+  (RSLT_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_C1_MEMBERSHIP    :binary@prove)
+  (CIRCUIT_SELECTOR_G1_MEMBERSHIP    :binary@prove)
+  (CIRCUIT_SELECTOR_C2_MEMBERSHIP    :binary@prove)
+  (CIRCUIT_SELECTOR_G2_MEMBERSHIP    :binary@prove)
+  (CIRCUIT_SELECTOR_PAIRING          :binary@prove)
+  (CIRCUIT_SELECTOR_G1_ADD           :binary@prove)
+  (CIRCUIT_SELECTOR_G2_ADD           :binary@prove)
+  (CIRCUIT_SELECTOR_G1_MSM           :binary@prove)
+  (CIRCUIT_SELECTOR_G2_MSM           :binary@prove)
+  (CIRCUIT_SELECTOR_MAP_FP_TO_G1      :binary@prove)
+  (CIRCUIT_SELECTOR_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_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_PAIRING          CIRCUIT_SELECTOR_PAIRING
+  CS_G1_ADD           CIRCUIT_SELECTOR_G1_ADD
+  CS_G2_ADD           CIRCUIT_SELECTOR_G2_ADD
+  CS_G1_MSM           CIRCUIT_SELECTOR_G1_MSM
+  CS_G2_MSM           CIRCUIT_SELECTOR_G2_MSM
+  CS_MAP_FP_TO_G1     CIRCUIT_SELECTOR_MAP_FP_TO_G1
+  CS_MAP_FP2_TO_G2    CIRCUIT_SELECTOR_MAP_FP2_TO_G2
+)
+
+

bls/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/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/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/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_G1_ADD_FLAG RSLT_G1_ADD_FLAG))
+
+(defun (is_g1_msm)
+    (+ DATA_G1_MSM_FLAG RSLT_G1_MSM_FLAG))
+
+(defun (is_g2_add)
+    (+ DATA_G2_ADD_FLAG RSLT_G2_ADD_FLAG))
+
+(defun (is_g2_msm)
+    (+ DATA_G2_MSM_FLAG RSLT_G2_MSM_FLAG))
+
+(defun (is_pairing_check)
+    (+ DATA_PAIRING_CHECK_FLAG RSLT_PAIRING_CHECK_FLAG))
+
+(defun (is_map_fp_to_g1)
+    (+ DATA_MAP_FP_TO_G1_FLAG RSLT_MAP_FP_TO_G1_FLAG))
+
+(defun (is_map_fp2_to_g2)
+    (+ DATA_MAP_FP2_TO_G2_FLAG RSLT_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/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/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/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/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_G1_ADD_FLAG (next DATA_G1_ADD_FLAG))
+       (* DATA_G1_MSM_FLAG (next DATA_G1_MSM_FLAG))
+       (* DATA_G2_ADD_FLAG (next DATA_G2_ADD_FLAG))
+       (* DATA_G1_MSM_FLAG (next DATA_G2_ADD_FLAG))
+       (* DATA_PAIRING_CHECK_FLAG (next DATA_PAIRING_CHECK_FLAG))
+       (* DATA_MAP_FP_TO_G1_FLAG (next DATA_MAP_FP_TO_G1_FLAG))
+       (* DATA_MAP_FP2_TO_G2_FLAG (next DATA_MAP_FP2_TO_G2_FLAG))))
+
+(defun (same_data_to_result)
+    (+ (* DATA_POINT_EVALUATION_FLAG (next RSLT_POINT_EVALUATION_FLAG))
+       (* DATA_G1_ADD_FLAG (next RSLT_G1_ADD_FLAG))
+       (* DATA_G1_MSM_FLAG (next RSLT_G1_MSM_FLAG))
+       (* DATA_G2_ADD_FLAG (next RSLT_G2_ADD_FLAG))
+       (* DATA_G1_MSM_FLAG (next RSLT_G2_ADD_FLAG))
+       (* DATA_PAIRING_CHECK_FLAG (next RSLT_PAIRING_CHECK_FLAG))
+       (* DATA_MAP_FP_TO_G1_FLAG (next RSLT_MAP_FP_TO_G1_FLAG))
+       (* DATA_MAP_FP2_TO_G2_FLAG (next RSLT_MAP_FP2_TO_G2_FLAG))))
+
+(defun (same_result_to_result)
+    (+ (* RSLT_POINT_EVALUATION_FLAG (next RSLT_POINT_EVALUATION_FLAG))
+       (* RSLT_G1_ADD_FLAG (next RSLT_G1_ADD_FLAG))
+       (* RSLT_G1_MSM_FLAG (next RSLT_G1_MSM_FLAG))
+       (* RSLT_G2_ADD_FLAG (next RSLT_G2_ADD_FLAG))
+       (* RSLT_G1_MSM_FLAG (next RSLT_G2_ADD_FLAG))
+       (* RSLT_PAIRING_CHECK_FLAG (next RSLT_PAIRING_CHECK_FLAG))
+       (* RSLT_MAP_FP_TO_G1_FLAG (next RSLT_MAP_FP_TO_G1_FLAG))
+       (* RSLT_MAP_FP2_TO_G2_FLAG (next RSLT_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)) 

bls/generalities/setting_acc_inputs.lisp

@@ -0,0 +1,20 @@
+(module bls)
+
+(defun (is_variable_size_data)
+    (+ DATA_G1_MSM_FLAG
+       DATA_G2_MSM_FLAG
+       DATA_PAIRING_CHECK_FLAG))
+
+(defconstraint acc-inputs-init ()
+    (if-zero (is_variable_size_data)
+        (begin (vanishes! ACC_INPUTS)
+               (eq! (next ACC_INPUTS) (next (is_variable_size_data))))))
+
+(defconstraint acc-inputs-increment ()
+    (if-not-zero (is_variable_size_data)
+        (if-eq-else (next (is_variable_size_data)) 0
+            (vanishes! (next ACC_INPUTS))
+            (eq! (next ACC_INPUTS)
+                 (+ ACC_INPUTS
+                    1
+                    (will_switch_from_second_to_first))))))

bls/generalities/setting_ct_max.lisp

@@ -0,0 +1,24 @@
+(module bls)
+
+(defun (ct_max_first_input)
+    (+ (* CT_MAX_POINT_EVALUATION DATA_POINT_EVALUATION_FLAG)
+       (* CT_MAX_SMALL_POINT DATA_G1_ADD_FLAG)
+       (* CT_MAX_SMALL_POINT DATA_G1_MSM_FLAG)
+       (* CT_MAX_LARGE_POINT DATA_G2_ADD_FLAG)
+       (* CT_MAX_LARGE_POINT DATA_G2_MSM_FLAG)
+       (* CT_MAX_SMALL_POINT DATA_PAIRING_CHECK_FLAG)
+       (* CT_MAX_MAP_FP_TO_G1 DATA_MAP_FP_TO_G1_FLAG)
+       (* CT_MAX_MAP_FP2_TO_G2 DATA_MAP_FP2_TO_G2_FLAG)))
+
+(defun (ct_max_second_input)
+    (+ (* CT_MAX_SMALL_POINT RSLT_G1_ADD_FLAG)
+       (* CT_MAX_SCALAR RSLT_G1_MSM_FLAG)
+       (* CT_MAX_LARGE_POINT RSLT_G2_ADD_FLAG)
+       (* CT_MAX_SCALAR RSLT_G2_MSM_FLAG)
+       (* CT_MAX_LARGE_POINT RSLT_PAIRING_CHECK_FLAG)))
+
+(defconstraint set-ct-max ()
+    (eq! CT_MAX 
+         (+ (* (ct_max_first_input) IS_FIRST_INPUT)
+            (* (ct_max_second_input) IS_SECOND_INPUT)
+            (* INDEX_MAX (is_result)))))

bls/generalities/setting_index.lisp

@@ -0,0 +1,22 @@
+(module bls)
+
+(defconstraint vanishing-values ()
+  (if-zero (flag_sum)
+           (begin (vanishes! INDEX_MAX)                 
+                  (vanishes! INDEX)
+                  (vanishes! ID))))
+
+(defconstraint index-reset ()
+  (if-not-zero (transition_bit)
+               (vanishes! (next INDEX))))
+
+(defconstraint index-increment ()
+  (if-not-zero (flag_sum)
+               (if-eq-else INDEX INDEX_MAX
+                           (eq! (transition_bit) 1)
+                           (eq! (next INDEX) (+ 1 INDEX)))))
+
+(defconstraint final-row (:domain {-1})
+  (if-not-zero (flag_sum)
+               (begin (eq! (is_result) 1)
+                      (eq! INDEX INDEX_MAX))))