diff --git a/Makefile b/Makefile index 1cb631a7..b2a02a14 100644 --- a/Makefile +++ b/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} \ diff --git a/bls/cancun/circuit_selectors.lisp b/bls/cancun/circuit_selectors.lisp new file mode 100644 index 00000000..43eda585 --- /dev/null +++ b/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)))) \ No newline at end of file diff --git a/bls/cancun/columns.lisp b/bls/cancun/columns.lisp new file mode 100644 index 00000000..5607d6f3 --- /dev/null +++ b/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 +) + + diff --git a/bls/cancun/constants.lisp b/bls/cancun/constants.lisp new file mode 100644 index 00000000..a857ded6 --- /dev/null +++ b/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 +) + + diff --git a/bls/cancun/generalities/constancy_conditions.lisp b/bls/cancun/generalities/constancy_conditions.lisp new file mode 100644 index 00000000..4d93d0d6 --- /dev/null +++ b/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)))) \ No newline at end of file diff --git a/bls/cancun/generalities/constraining_address_sum.lisp b/bls/cancun/generalities/constraining_address_sum.lisp new file mode 100644 index 00000000..7b57e675 --- /dev/null +++ b/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))) diff --git a/bls/cancun/generalities/constraining_flag_sum.lisp b/bls/cancun/generalities/constraining_flag_sum.lisp new file mode 100644 index 00000000..e69ce9bb --- /dev/null +++ b/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))) \ No newline at end of file diff --git a/bls/cancun/generalities/constraints_for_bls_stamp.lisp b/bls/cancun/generalities/constraints_for_bls_stamp.lisp new file mode 100644 index 00000000..482debdb --- /dev/null +++ b/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)))) \ No newline at end of file diff --git a/bls/cancun/generalities/constraints_for_ct.lisp b/bls/cancun/generalities/constraints_for_ct.lisp new file mode 100644 index 00000000..a6339380 --- /dev/null +++ b/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)))) \ No newline at end of file diff --git a/bls/cancun/generalities/id_increment_constraints.lisp b/bls/cancun/generalities/id_increment_constraints.lisp new file mode 100644 index 00000000..2924bc7a --- /dev/null +++ b/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)))))) diff --git a/bls/cancun/generalities/legal_transition_constraints.lisp b/bls/cancun/generalities/legal_transition_constraints.lisp new file mode 100644 index 00000000..c59d7bd9 --- /dev/null +++ b/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)) \ No newline at end of file diff --git a/bls/cancun/generalities/setting_acc_inputs.lisp b/bls/cancun/generalities/setting_acc_inputs.lisp new file mode 100644 index 00000000..3c53229b --- /dev/null +++ b/bls/cancun/generalities/setting_acc_inputs.lisp @@ -0,0 +1,20 @@ +(module bls) + +(defun (is_variable_size_data) + (+ DATA_BLS_G1_MSM_FLAG + DATA_BLS_G2_MSM_FLAG + DATA_BLS_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)))))) \ No newline at end of file diff --git a/bls/cancun/generalities/setting_ct_max.lisp b/bls/cancun/generalities/setting_ct_max.lisp new file mode 100644 index 00000000..16c2431c --- /dev/null +++ b/bls/cancun/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_BLS_G1_ADD_FLAG) + (* CT_MAX_SMALL_POINT DATA_BLS_G1_MSM_FLAG) + (* CT_MAX_LARGE_POINT DATA_BLS_G2_ADD_FLAG) + (* CT_MAX_LARGE_POINT DATA_BLS_G2_MSM_FLAG) + (* CT_MAX_SMALL_POINT DATA_BLS_PAIRING_CHECK_FLAG) + (* CT_MAX_MAP_FP_TO_G1 DATA_BLS_MAP_FP_TO_G1_FLAG) + (* CT_MAX_MAP_FP2_TO_G2 DATA_BLS_MAP_FP2_TO_G2_FLAG))) + +(defun (ct_max_second_input) + (+ (* CT_MAX_SMALL_POINT RSLT_BLS_G1_ADD_FLAG) + (* CT_MAX_SCALAR RSLT_BLS_G1_MSM_FLAG) + (* CT_MAX_LARGE_POINT RSLT_BLS_G2_ADD_FLAG) + (* CT_MAX_SCALAR RSLT_BLS_G2_MSM_FLAG) + (* CT_MAX_LARGE_POINT RSLT_BLS_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))))) \ No newline at end of file diff --git a/bls/cancun/generalities/setting_index.lisp b/bls/cancun/generalities/setting_index.lisp new file mode 100644 index 00000000..3eb8e174 --- /dev/null +++ b/bls/cancun/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)))) \ No newline at end of file diff --git a/bls/cancun/generalities/setting_index_max.lisp b/bls/cancun/generalities/setting_index_max.lisp new file mode 100644 index 00000000..64b18dad --- /dev/null +++ b/bls/cancun/generalities/setting_index_max.lisp @@ -0,0 +1,28 @@ +(module bls) + +(defun (index_max_sum) + (+ (* INDEX_MAX_DATA_POINT_EVALUATION DATA_POINT_EVALUATION_FLAG) + (* INDEX_MAX_DATA_G1_ADD DATA_BLS_G1_ADD_FLAG) + (* INDEX_MAX_DATA_G2_ADD DATA_BLS_G2_ADD_FLAG) + (* INDEX_MAX_DATA_MAP_FP_TO_G1 DATA_BLS_MAP_FP_TO_G1_FLAG) + (* INDEX_MAX_DATA_MAP_FP2_TO_G2 DATA_BLS_MAP_FP2_TO_G2_FLAG) + (* INDEX_MAX_RSLT_POINT_EVALUATION RSLT_POINT_EVALUATION_FLAG) + (* INDEX_MAX_RSLT_G1_ADD RSLT_BLS_G1_ADD_FLAG) + (* INDEX_MAX_RSLT_G1_MSM RSLT_BLS_G1_MSM_FLAG) + (* INDEX_MAX_RSLT_G2_ADD RSLT_BLS_G2_ADD_FLAG) + (* INDEX_MAX_RSLT_G2_MSM RSLT_BLS_G2_MSM_FLAG) + (* INDEX_MAX_RSLT_PAIRING_CHECK RSLT_BLS_PAIRING_CHECK_FLAG) + (* INDEX_MAX_RSLT_MAP_FP_TO_G1 RSLT_BLS_MAP_FP_TO_G1_FLAG) + (* INDEX_MAX_RSLT_MAP_FP2_TO_G2 RSLT_BLS_MAP_FP2_TO_G2_FLAG))) + +(defconstraint index-constancy () + (counter-constancy INDEX INDEX_MAX)) + +(defconstraint set-index-max () + (eq! (* 16 INDEX_MAX) + (+ (* 16 (index_max_sum)) + (* DATA_BLS_G1_MSM_FLAG (- TOTAL_SIZE 16)) + (* DATA_BLS_G2_MSM_FLAG (- TOTAL_SIZE 16)) + (* DATA_BLS_PAIRING_CHECK_FLAG (- TOTAL_SIZE 16))))) + + \ No newline at end of file diff --git a/bls/cancun/generalities/setting_is_first_input_and_is_second_input.lisp b/bls/cancun/generalities/setting_is_first_input_and_is_second_input.lisp new file mode 100644 index 00000000..485e4e6e --- /dev/null +++ b/bls/cancun/generalities/setting_is_first_input_and_is_second_input.lisp @@ -0,0 +1,51 @@ +(module bls) + +(defun (two_input_type_prc_data) + (+ DATA_BLS_G1_ADD_FLAG + DATA_BLS_G1_MSM_FLAG + DATA_BLS_G2_ADD_FLAG + DATA_BLS_G2_MSM_FLAG + DATA_BLS_PAIRING_CHECK_FLAG)) + +(defun (one_input_type_prc_data) + (+ DATA_POINT_EVALUATION_FLAG + DATA_BLS_MAP_FP_TO_G1_FLAG + DATA_BLS_MAP_FP2_TO_G2_FLAG)) + +(defun (will_switch_from_first_to_second) + (* IS_FIRST_INPUT (next IS_SECOND_INPUT))) + +(defun (will_switch_from_second_to_first) + (* IS_SECOND_INPUT (next IS_FIRST_INPUT))) + +(defconstraint counter-constancy () + (begin (counter-constancy CT IS_FIRST_INPUT) + (counter-constancy CT IS_SECOND_INPUT))) ;; TODO: add to constancy conditions in both lisp and specs + +(defconstraint either-first-or-second () + (eq! (is_data) (+ IS_FIRST_INPUT IS_SECOND_INPUT))) + +(defconstraint data-start-with-first-input () + (if-zero (is_data) + (eq! (next IS_FIRST_INPUT) (next (is_data))))) + +(defconstraint one-input-is-first-input () + (if-not-zero (one_input_type_prc_data) + (eq! IS_FIRST_INPUT 1))) + +(defconstraint two-input-is-either-first-or-second () + (if-not-zero (two_input_type_prc_data) + (eq! (+ IS_FIRST_INPUT IS_SECOND_INPUT) 1))) + +(defconstraint two-input-transitions () + (if-not-zero (two_input_type_prc_data) + (if-eq-else CT CT_MAX + (eq! (+ (will_switch_from_first_to_second) + (will_switch_from_second_to_first)) + (next (two_input_type_prc_data))) + (vanishes! (+ (will_switch_from_first_to_second) + (will_switch_from_second_to_first)))))) + + + + diff --git a/bls/cancun/generalities/setting_phase.lisp b/bls/cancun/generalities/setting_phase.lisp new file mode 100644 index 00000000..1d7bc96a --- /dev/null +++ b/bls/cancun/generalities/setting_phase.lisp @@ -0,0 +1,30 @@ +(module bls) + +(defun (phase_sum) + (+ (* PHASE_DATA_POINT_EVALUATION DATA_POINT_EVALUATION_FLAG) + (* PHASE_RSLT_POINT_EVALUATION RSLT_POINT_EVALUATION_FLAG) + (* PHASE_DATA_G1_ADD DATA_BLS_G1_ADD_FLAG) + (* PHASE_RSLT_G1_ADD RSLT_BLS_G1_ADD_FLAG) + (* PHASE_DATA_G1_MSM DATA_BLS_G1_MSM_FLAG) + (* PHASE_RSLT_G1_MSM RSLT_BLS_G1_MSM_FLAG) + (* PHASE_DATA_G2_ADD DATA_BLS_G2_ADD_FLAG) + (* PHASE_RSLT_G2_ADD RSLT_BLS_G2_ADD_FLAG) + (* PHASE_DATA_G2_MSM DATA_BLS_G2_MSM_FLAG) + (* PHASE_RSLT_G2_MSM RSLT_BLS_G2_MSM_FLAG) + (* PHASE_DATA_PAIRING_CHECK DATA_BLS_PAIRING_CHECK_FLAG) + (* PHASE_RSLT_PAIRING_CHECK RSLT_BLS_PAIRING_CHECK_FLAG) + (* PHASE_DATA_MAP_FP_TO_G1 DATA_BLS_MAP_FP_TO_G1_FLAG) + (* PHASE_RSLT_MAP_FP_TO_G1 RSLT_BLS_MAP_FP_TO_G1_FLAG) + (* PHASE_DATA_MAP_FP2_TO_G2 DATA_BLS_MAP_FP2_TO_G2_FLAG) + (* PHASE_RSLT_MAP_FP2_TO_G2 RSLT_BLS_MAP_FP2_TO_G2_FLAG))) + +(defconstraint stamp-constancy () + (stamp-constancy STAMP PHASE)) + +(defconstraint setting-phase () + (eq! PHASE (phase_sum))) + + + + + \ No newline at end of file diff --git a/bls/cancun/generalities/setting_total_size.lisp b/bls/cancun/generalities/setting_total_size.lisp new file mode 100644 index 00000000..820bbb9f --- /dev/null +++ b/bls/cancun/generalities/setting_total_size.lisp @@ -0,0 +1,10 @@ +(module bls) + +(defconstraint setting-total-size-data () + (if-not-zero (is_data) + (if-zero (is_variable_size_data) + (eq! TOTAL_SIZE (* (+ INDEX_MAX 1) 16))))) + +(defconstraint setting-total-size-result () + (if-not-zero (is_result) + (eq! TOTAL_SIZE (* (+ INDEX_MAX 1) 16 SUCCESS_BIT)))) \ No newline at end of file diff --git a/bls/cancun/generalities/shorthands.lisp b/bls/cancun/generalities/shorthands.lisp new file mode 100644 index 00000000..fb734e95 --- /dev/null +++ b/bls/cancun/generalities/shorthands.lisp @@ -0,0 +1,30 @@ +(module bls) + +(defun (is_data) + (+ DATA_POINT_EVALUATION_FLAG + DATA_BLS_G1_ADD_FLAG + DATA_BLS_G1_MSM_FLAG + DATA_BLS_G2_ADD_FLAG + DATA_BLS_G2_MSM_FLAG + DATA_BLS_PAIRING_CHECK_FLAG + DATA_BLS_MAP_FP_TO_G1_FLAG + DATA_BLS_MAP_FP2_TO_G2_FLAG)) + +(defun (is_result) + (+ RSLT_POINT_EVALUATION_FLAG + RSLT_BLS_G1_ADD_FLAG + RSLT_BLS_G1_MSM_FLAG + RSLT_BLS_G2_ADD_FLAG + RSLT_BLS_G2_MSM_FLAG + RSLT_BLS_PAIRING_CHECK_FLAG + RSLT_BLS_MAP_FP_TO_G1_FLAG + RSLT_BLS_MAP_FP2_TO_G2_FLAG)) + +(defun (transition_to_data) + (* (- 1 (is_data) (next (is_data))))) + +(defun (transition_to_result) + (* (- 1 (is_result) (next (is_result))))) + +(defun (transition_bit) + (+ (transition_to_data) (transition_to_result))) \ No newline at end of file diff --git a/bls/cancun/lookups/bls_into_wcp.lisp b/bls/cancun/lookups/bls_into_wcp.lisp new file mode 100644 index 00000000..8e3bc0a3 --- /dev/null +++ b/bls/cancun/lookups/bls_into_wcp.lisp @@ -0,0 +1,25 @@ +(defun (bls-into-wcp-activation-flag) + bls.WCP_FLAG) + +(deflookup + bls-into-wcp + ; target columns + ( + wcp.ARGUMENT_1_HI + wcp.ARGUMENT_1_LO + wcp.ARGUMENT_2_HI + wcp.ARGUMENT_2_LO + wcp.RESULT + wcp.INST + ) + ; source columns + ( + (* bls.WCP_ARG1_HI (bls-into-wcp-activation-flag)) + (* bls.WCP_ARG1_LO (bls-into-wcp-activation-flag)) + (* bls.WCP_ARG2_HI (bls-into-wcp-activation-flag)) + (* bls.WCP_ARG2_LO (bls-into-wcp-activation-flag)) + (* bls.WCP_RES (bls-into-wcp-activation-flag)) + (* bls.WCP_INST (bls-into-wcp-activation-flag)) + )) + + diff --git a/bls/cancun/specialized_constraints/g1_add.lisp b/bls/cancun/specialized_constraints/g1_add.lisp new file mode 100644 index 00000000..7d4032ea --- /dev/null +++ b/bls/cancun/specialized_constraints/g1_add.lisp @@ -0,0 +1,15 @@ +(module bls) + +(defun (g1-add-hypothesis) + (* DATA_BLS_G1_ADD_FLAG (first_row_of_new_input))) + +(defconstraint internal-checks-g1-add (:guard (g1-add-hypothesis)) + (let ((A_x_3 LIMB) + (A_x_2 (shift LIMB 1)) + (A_x_1 (shift LIMB 2)) + (A_x_0 (shift LIMB 3)) + (A_y_3 (shift LIMB 4)) + (A_y_2 (shift LIMB 5)) + (A_y_1 (shift LIMB 6)) + (A_y_0 (shift LIMB 7))) + (wellFormedFpCoordinatesAndInfinityCheck 0 A_x_3 A_x_2 A_x_1 A_x_0 A_y_3 A_y_2 A_y_1 A_y_0))) \ No newline at end of file diff --git a/bls/cancun/specialized_constraints/g1_msm.lisp b/bls/cancun/specialized_constraints/g1_msm.lisp new file mode 100644 index 00000000..d8e82083 --- /dev/null +++ b/bls/cancun/specialized_constraints/g1_msm.lisp @@ -0,0 +1,15 @@ +(module bls) + +(defun (g1-msm-hypothesis) + (* DATA_BLS_G1_MSM_FLAG (first_row_of_new_first_input))) + +(defconstraint internal-checks-g1-msm (:guard (g1-msm-hypothesis)) + (let ((A_x_3 LIMB) + (A_x_2 (shift LIMB 1)) + (A_x_1 (shift LIMB 2)) + (A_x_0 (shift LIMB 3)) + (A_y_3 (shift LIMB 4)) + (A_y_2 (shift LIMB 5)) + (A_y_1 (shift LIMB 6)) + (A_y_0 (shift LIMB 7))) + (wellFormedFpCoordinatesAndInfinityCheck 0 A_x_3 A_x_2 A_x_1 A_x_0 A_y_3 A_y_2 A_y_1 A_y_0))) \ No newline at end of file diff --git a/bls/cancun/specialized_constraints/g2_add.lisp b/bls/cancun/specialized_constraints/g2_add.lisp new file mode 100644 index 00000000..25819b34 --- /dev/null +++ b/bls/cancun/specialized_constraints/g2_add.lisp @@ -0,0 +1,23 @@ +(module bls) + +(defun (g2-add-hypothesis) + (* DATA_BLS_G2_ADD_FLAG (first_row_of_new_input))) + +(defconstraint internal-checks-g2-add (:guard (g2-add-hypothesis)) + (let ((A_x_Im_3 LIMB) + (A_x_Im_2 (shift LIMB 1)) + (A_x_Im_1 (shift LIMB 2)) + (A_x_Im_0 (shift LIMB 3)) + (A_x_Re_3 (shift LIMB 4)) + (A_x_Re_2 (shift LIMB 5)) + (A_x_Re_1 (shift LIMB 6)) + (A_x_Re_0 (shift LIMB 7)) + (A_y_Im_3 (shift LIMB 8)) + (A_y_Im_2 (shift LIMB 9)) + (A_y_Im_1 (shift LIMB 10)) + (A_y_Im_0 (shift LIMB 11)) + (A_y_Re_3 (shift LIMB 12)) + (A_y_Re_2 (shift LIMB 13)) + (A_y_Re_1 (shift LIMB 14)) + (A_y_Re_0 (shift LIMB 15))) + (wellFormedFp2CoordinatesAndInfinityCheck 0 A_x_Im_3 A_x_Im_2 A_x_Im_1 A_x_Im_0 A_x_Re_3 A_x_Re_2 A_x_Re_1 A_x_Re_0 A_y_Im_3 A_y_Im_2 A_y_Im_1 A_y_Im_0 A_y_Re_3 A_y_Re_2 A_y_Re_1 A_y_Re_0))) \ No newline at end of file diff --git a/bls/cancun/specialized_constraints/g2_msm.lisp b/bls/cancun/specialized_constraints/g2_msm.lisp new file mode 100644 index 00000000..057a6222 --- /dev/null +++ b/bls/cancun/specialized_constraints/g2_msm.lisp @@ -0,0 +1,23 @@ +(module bls) + +(defun (g2-msm-hypothesis) + (* DATA_BLS_G2_MSM_FLAG (first_row_of_new_first_input))) + +(defconstraint internal-checks-g2-msm (:guard (g2-msm-hypothesis)) + (let ((A_x_Im_3 LIMB) + (A_x_Im_2 (shift LIMB 1)) + (A_x_Im_1 (shift LIMB 2)) + (A_x_Im_0 (shift LIMB 3)) + (A_x_Re_3 (shift LIMB 4)) + (A_x_Re_2 (shift LIMB 5)) + (A_x_Re_1 (shift LIMB 6)) + (A_x_Re_0 (shift LIMB 7)) + (A_y_Im_3 (shift LIMB 8)) + (A_y_Im_2 (shift LIMB 9)) + (A_y_Im_1 (shift LIMB 10)) + (A_y_Im_0 (shift LIMB 11)) + (A_y_Re_3 (shift LIMB 12)) + (A_y_Re_2 (shift LIMB 13)) + (A_y_Re_1 (shift LIMB 14)) + (A_y_Re_0 (shift LIMB 15))) + (wellFormedFp2CoordinatesAndInfinityCheck 0 A_x_Im_3 A_x_Im_2 A_x_Im_1 A_x_Im_0 A_x_Re_3 A_x_Re_2 A_x_Re_1 A_x_Re_0 A_y_Im_3 A_y_Im_2 A_y_Im_1 A_y_Im_0 A_y_Re_3 A_y_Re_2 A_y_Re_1 A_y_Re_0))) \ No newline at end of file diff --git a/bls/cancun/specialized_constraints/map_fp2_to_g3.lisp b/bls/cancun/specialized_constraints/map_fp2_to_g3.lisp new file mode 100644 index 00000000..50d39b33 --- /dev/null +++ b/bls/cancun/specialized_constraints/map_fp2_to_g3.lisp @@ -0,0 +1,21 @@ +(module bls) + +(defun (map-fp2-to-g2-hypothesis) + (* DATA_BLS_MAP_FP2_TO_G2_FLAG (first_row_of_new_first_input))) + +(defconstraint internal-checks-map-fp2-to-g2 (:guard (map-fp2-to-g2-hypothesis)) + (let ((e_Im_3 LIMB) + (e_Im_2 (shift LIMB 1)) + (e_Im_1 (shift LIMB 2)) + (e_Im_0 (shift LIMB 3)) + (e_Re_3 (shift LIMB 4)) + (e_Re_2 (shift LIMB 5)) + (e_Re_1 (shift LIMB 6)) + (e_Re_0 (shift LIMB 7)) + (e_Im_is_in_range WCP_RES) + (e_Re_is_in_range (shift WCP_RES 4)) + (internal_checks_passed (- 1 MINT_BIT))) + (begin (wcpGeneralizedCallToLT 0 e_Im_3 e_Im_2 e_Im_1 e_Im_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (wcpGeneralizedCallToLT 4 e_Re_3 e_Re_2 e_Re_1 e_Re_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (eq! internal_checks_passed (* e_Im_is_in_range e_Re_is_in_range)) + ))) \ No newline at end of file diff --git a/bls/cancun/specialized_constraints/map_fp_to_g1.lisp b/bls/cancun/specialized_constraints/map_fp_to_g1.lisp new file mode 100644 index 00000000..091e2841 --- /dev/null +++ b/bls/cancun/specialized_constraints/map_fp_to_g1.lisp @@ -0,0 +1,15 @@ +(module bls) + +(defun (map-fp-to-g1-hypothesis) + (* DATA_BLS_MAP_FP_TO_G1_FLAG (first_row_of_new_first_input))) + +(defconstraint internal-checks-map-fp-to-g1 (:guard (map-fp-to-g1-hypothesis)) + (let ((e_3 LIMB) + (e_2 (shift LIMB 1)) + (e_1 (shift LIMB 2)) + (e_0 (shift LIMB 3)) + (e_is_in_range WCP_RES) + (internal_checks_passed (- 1 MINT_BIT))) + (begin (wcpGeneralizedCallToLT 0 e_3 e_2 e_1 e_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (eq! internal_checks_passed (* e_is_in_range)) + ))) diff --git a/bls/cancun/specialized_constraints/pairing_check_first_input.lisp b/bls/cancun/specialized_constraints/pairing_check_first_input.lisp new file mode 100644 index 00000000..dac1d353 --- /dev/null +++ b/bls/cancun/specialized_constraints/pairing_check_first_input.lisp @@ -0,0 +1,15 @@ +(module bls) + +(defun (pairing-check-first-input-hypothesis) + (* DATA_BLS_PAIRING_CHECK_FLAG (first_row_of_new_first_input))) + +(defconstraint internal-checks-pairing-check-first-input (:guard (pairing-check-first-input-hypothesis)) + (let ((A_x_3 LIMB) + (A_x_2 (shift LIMB 1)) + (A_x_1 (shift LIMB 2)) + (A_x_0 (shift LIMB 3)) + (A_y_3 (shift LIMB 4)) + (A_y_2 (shift LIMB 5)) + (A_y_1 (shift LIMB 6)) + (A_y_0 (shift LIMB 7))) + (wellFormedFpCoordinatesAndInfinityCheck 0 A_x_3 A_x_2 A_x_1 A_x_0 A_y_3 A_y_2 A_y_1 A_y_0))) \ No newline at end of file diff --git a/bls/cancun/specialized_constraints/pairing_check_second_input.lisp b/bls/cancun/specialized_constraints/pairing_check_second_input.lisp new file mode 100644 index 00000000..3e81139d --- /dev/null +++ b/bls/cancun/specialized_constraints/pairing_check_second_input.lisp @@ -0,0 +1,23 @@ +(module bls) + +(defun (pairing-check-second-input-hypothesis) + (* DATA_BLS_PAIRING_CHECK_FLAG (first_row_of_new_second_input))) + +(defconstraint internal-checks-pairing-check-second-input (:guard (pairing-check-second-input-hypothesis)) + (let ((B_x_Im_3 LIMB) + (B_x_Im_2 (shift LIMB 1)) + (B_x_Im_1 (shift LIMB 2)) + (B_x_Im_0 (shift LIMB 3)) + (B_x_Re_3 (shift LIMB 4)) + (B_x_Re_2 (shift LIMB 5)) + (B_x_Re_1 (shift LIMB 6)) + (B_x_Re_0 (shift LIMB 7)) + (B_y_Im_3 (shift LIMB 8)) + (B_y_Im_2 (shift LIMB 9)) + (B_y_Im_1 (shift LIMB 10)) + (B_y_Im_0 (shift LIMB 11)) + (B_y_Re_3 (shift LIMB 12)) + (B_y_Re_2 (shift LIMB 13)) + (B_y_Re_1 (shift LIMB 14)) + (B_y_Re_0 (shift LIMB 15))) + (wellFormedFp2CoordinatesAndInfinityCheck 0 B_x_Im_3 B_x_Im_2 B_x_Im_1 B_x_Im_0 B_x_Re_3 B_x_Re_2 B_x_Re_1 B_x_Re_0 B_y_Im_3 B_y_Im_2 B_y_Im_1 B_y_Im_0 B_y_Re_3 B_y_Re_2 B_y_Re_1 B_y_Re_0))) \ No newline at end of file diff --git a/bls/cancun/specialized_constraints/point_evaluation.lisp b/bls/cancun/specialized_constraints/point_evaluation.lisp new file mode 100644 index 00000000..5571e28d --- /dev/null +++ b/bls/cancun/specialized_constraints/point_evaluation.lisp @@ -0,0 +1,17 @@ +(module bls) + +(defun (point-evaluation-hypothesis) + (* DATA_POINT_EVALUATION_FLAG (first_row_of_new_input))) + +(defconstraint internal-checks-point-evaluation (:guard (point-evaluation-hypothesis)) + (let ((z_hi (shift LIMB 2)) + (z_lo (shift LIMB 3)) + (y_hi (shift LIMB 4)) + (y_lo (shift LIMB 5)) + (z_is_in_range WCP_RES) + (y_is_in_range (shift WCP_RES 1)) + (internal_checks_passed (- 1 MINT_BIT))) + (begin (wcpCallToLT 0 z_hi z_lo POINT_EVALUATION_PRIME_HI POINT_EVALUATION_PRIME_LO) + (wcpCallToLT 1 y_hi y_lo POINT_EVALUATION_PRIME_HI POINT_EVALUATION_PRIME_LO) + (eq! internal_checks_passed (* z_is_in_range y_is_in_range)) + ))) diff --git a/bls/cancun/specialized_constraints/shorthands.lisp b/bls/cancun/specialized_constraints/shorthands.lisp new file mode 100644 index 00000000..b0e195a4 --- /dev/null +++ b/bls/cancun/specialized_constraints/shorthands.lisp @@ -0,0 +1,10 @@ +(module bls) + +(defun (first_row_of_new_first_input) + (* (- 1 (prev IS_FIRST_INPUT)) IS_FIRST_INPUT)) + +(defun (first_row_of_new_second_input) + (* (- 1 (prev IS_SECOND_INPUT)) IS_SECOND_INPUT)) + +(defun (first_row_of_new_input) + (+ (first_row_of_new_first_input) (first_row_of_new_second_input))) \ No newline at end of file diff --git a/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/generalities.lisp b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/generalities.lisp new file mode 100644 index 00000000..f7aa5f83 --- /dev/null +++ b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/generalities.lisp @@ -0,0 +1,45 @@ +(module bls) + +(defun (malformed_data) + (+ MINT MEXT)) + +(defun (wellformed_data) + (+ WTRV WNON)) + +(defun (case_data_sum) + (+ (malformed_data) + (wellformed_data))) + +(defconstraint case-data-sum-equal-to-flag-sum () + (eq! (case_data_sum) (flag_sum))) + +(defconstraint map-fp-to-g1-cannot-fail-externally () + (if-not-zero (is_map_fp_to_g1) + (vanishes! MEXT))) + +(defconstraint map-fp2-to-g2-cannot-fail-externally () + (if-not-zero (is_map_fp2_to_g2) + (vanishes! MEXT))) + +(defconstraint only-pairing-check-can-be-trivial () + (if-zero (is_pairing_check) + (vanishes! WTRV))) + +(defconstraint pairing-check-setting-non-trivial () + (if-not-zero (is_pairing_check) + (if-not-zero (transition_to_result) + (begin + (debug (if-not-zero (malformed_data) + (vanishes! WNON))) + (if-not-zero (wellformed_data) + (eq! WNON NONTRIVIAL_POP_ACC)))))) + +(defconstraint setting-mint-bit-along-g1-msm-scalar () + (if-not-zero DATA_BLS_G1_MSM_FLAG + (if-not-zero IS_SECOND_INPUT + (vanishes! MINT_BIT)))) + +(defconstraint setting-mint-bit-along-g2-msm-scalar () + (if-not-zero DATA_BLS_G2_MSM_FLAG + (if-not-zero IS_SECOND_INPUT + (vanishes! MINT_BIT)))) \ No newline at end of file diff --git a/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_mext_bit_mext_acc_and_mext.lisp b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_mext_bit_mext_acc_and_mext.lisp new file mode 100644 index 00000000..149f3d9d --- /dev/null +++ b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_mext_bit_mext_acc_and_mext.lisp @@ -0,0 +1,36 @@ +(module bls) + +(defconstraint if-mint-is-one-then-mext-is-not-relevant () + (if-not-zero MINT + (begin + (vanishes! MEXT_BIT) + (debug (vanishes! MEXT_ACC)) + (debug (vanishes! MEXT))))) + +(defconstraint if-is-data-is-zero-then-mext-bit-and-mext-acc-vanish () + (if-zero (is_data) + (begin + (vanishes! MEXT_BIT) + (vanishes! MEXT_ACC)))) + +(defconstraint if-is-map-fp-to-g1-is-one-then-mext-bit-and-mext-acc-and-mext-vanish () + (if-not-zero (is_map_fp_to_g1) + (begin + (vanishes! MEXT_BIT) + (debug (vanishes! MEXT_ACC)) + (debug (vanishes! MEXT))))) + +(defconstraint if-is-map-fp2-to-g2-is-one-then-mext-bit-and-mext-acc-and-mext-vanish () + (if-not-zero (is_map_fp2_to_g2) + (begin + (vanishes! MEXT_BIT) + (debug (vanishes! MEXT_ACC)) + (debug (vanishes! MEXT))))) + +(defconstraint propagate-mext-bit-into-mext-acc () + (if-not-zero (+ (transition_to_data) (will_switch_from_first_to_second) (will_switch_from_second_to_first)) + (eq! (next MEXT_ACC) (+ MEXT_ACC (next MEXT_BIT))))) + +(defconstraint propagate-mext-acc-into-mext () + (if-not-zero (transition_to_result) + (eq! MEXT MEXT_ACC))) \ No newline at end of file diff --git a/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_mint_bit_mint_acc_and_mint.lisp b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_mint_bit_mint_acc_and_mint.lisp new file mode 100644 index 00000000..e89c0614 --- /dev/null +++ b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_mint_bit_mint_acc_and_mint.lisp @@ -0,0 +1,19 @@ +(module bls) + +(defconstraint set-mint-bit-and-mint-acc-when-is-data-is-zero () + (if-zero (is_data) + (begin + (vanishes! MINT_BIT) + (vanishes! MINT_ACC) + ))) + +(defconstraint propagate-mint-bit-into-mint-acc () + (if-not-zero (+ (transition_to_data) (will_switch_from_first_to_second) (will_switch_from_second_to_first)) + (begin (if-zero MINT_ACC + (eq! (next MINT_ACC) (next MINT_BIT))) + (if-not-zero MINT_ACC + (eq! (next MINT_ACC) 1))))) + +(defconstraint propagate-mint-acc-into-mint () + (if-not-zero (transition_to_result) + (eq! MINT MINT_ACC))) \ No newline at end of file diff --git a/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_non_trivial_pop_acc.lisp b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_non_trivial_pop_acc.lisp new file mode 100644 index 00000000..b6ae19e7 --- /dev/null +++ b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_non_trivial_pop_acc.lisp @@ -0,0 +1,11 @@ +(module bls) + +(defconstraint non-trivial-pop-acc-is-only-relevant-in-pairing-check () + (if-zero DATA_BLS_PAIRING_CHECK_FLAG + (vanishes! NONTRIVIAL_POP_ACC))) + +(defconstraint set-non-trivial-pop-acc () + (if-zero (prev DATA_BLS_PAIRING_CHECK_FLAG) + (if-not-zero DATA_BLS_PAIRING_CHECK_FLAG + (eq! NONTRIVIAL_POP_ACC NONTRIVIAL_POP_BIT)))) + \ No newline at end of file diff --git a/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_non_trivial_pop_bit.lisp b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_non_trivial_pop_bit.lisp new file mode 100644 index 00000000..d63ff303 --- /dev/null +++ b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_non_trivial_pop_bit.lisp @@ -0,0 +1,17 @@ +(module bls) + +(defun (small_point_is_nontrivial) + (- 1 IS_INFINITY)) + +(defun (large_point_is_nontrivial) + (- 1 (next IS_INFINITY))) + +(defconstraint nontrivial-pop-bit-is-only-relevant-in-pairing-check () + (if-zero DATA_BLS_PAIRING_CHECK_FLAG + (vanishes! NONTRIVIAL_POP_BIT))) + +(defconstraint set-non-trivial-pop-bit () + (if-not-zero DATA_BLS_PAIRING_CHECK_FLAG + (if-not-zero (will_switch_from_first_to_second) + (eq! NONTRIVIAL_POP_BIT (* (small_point_is_nontrivial) (large_point_is_nontrivial)))))) + diff --git a/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_result_for_trivial_pairings.lisp b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_result_for_trivial_pairings.lisp new file mode 100644 index 00000000..788c6041 --- /dev/null +++ b/bls/cancun/top_level_flags_mint_mext_wtrv_wnon/setting_result_for_trivial_pairings.lisp @@ -0,0 +1,10 @@ +(module bls) + +(defconstraint set-pairing-check-result-when-trivial-pairings () + (let ((pairing_result_hi (next LIMB)) + (pairing_result_lo (shift LIMB 2))) + (if-not-zero (is_pairing_check) + (if-not-zero (transition_to_result) + (if-not-zero WTRV + (begin (vanishes! pairing_result_hi) + (eq! pairing_result_lo 1))))))) \ No newline at end of file diff --git a/bls/cancun/utilities/definition_of_isInfinity.lisp b/bls/cancun/utilities/definition_of_isInfinity.lisp new file mode 100644 index 00000000..3f50b166 --- /dev/null +++ b/bls/cancun/utilities/definition_of_isInfinity.lisp @@ -0,0 +1,9 @@ +(module bls) + +(defun (isInfinity k coordinate_sum) + (let ((P_is_point_at_infinity (shift IS_INFINITY k))) + (begin + (if-zero coordinate_sum + (eq! P_is_point_at_infinity 1)) + (if-not-zero coordinate_sum + (eq! P_is_point_at_infinity 0))))) \ No newline at end of file diff --git a/bls/cancun/utilities/definition_of_wcp_utilities.lisp b/bls/cancun/utilities/definition_of_wcp_utilities.lisp new file mode 100644 index 00000000..fa5012cd --- /dev/null +++ b/bls/cancun/utilities/definition_of_wcp_utilities.lisp @@ -0,0 +1,25 @@ +(module bls) + +(defun (wcpCallToLT k a b c d) + (begin (eq! (shift WCP_FLAG k) 1) + (eq! (shift WCP_INST k) EVM_INST_LT) + (eq! (shift WCP_ARG1_HI k) a) + (eq! (shift WCP_ARG1_LO k) b) + (eq! (shift WCP_ARG2_HI k) c) + (eq! (shift WCP_ARG2_LO k) d))) + +(defun (wcpCallToEQ k a b c d) + (begin (eq! (shift WCP_FLAG k) 1) + (eq! (shift WCP_INST k) EVM_INST_EQ) + (eq! (shift WCP_ARG1_HI k) a) + (eq! (shift WCP_ARG1_LO k) b) + (eq! (shift WCP_ARG2_HI k) c) + (eq! (shift WCP_ARG2_LO k) d))) + +(defun (wcpGeneralizedCallToLT k a b c d e f g h) + (begin (wcpCallToLT (+ k 1) a b e f) + (wcpCallToEQ (+ k 2) a b e f) + (wcpCallToLT (+ k 3) c d g h) + (eq! (shift WCP_RES k) + (+ (shift WCP_RES (+ k 1)) + (* (shift WCP_RES (+ k 2)) (shift WCP_RES (+ k 3))))))) \ No newline at end of file diff --git a/bls/cancun/utilities/definition_of_wellFormedFp2CoordinatesAndInfinityCheck.lisp b/bls/cancun/utilities/definition_of_wellFormedFp2CoordinatesAndInfinityCheck.lisp new file mode 100644 index 00000000..7d2a5278 --- /dev/null +++ b/bls/cancun/utilities/definition_of_wellFormedFp2CoordinatesAndInfinityCheck.lisp @@ -0,0 +1,21 @@ +(module bls) + +(defun (wellFormedFp2CoordinatesAndInfinityCheck k P_x_Im_3 P_x_Im_2 P_x_Im_1 P_x_Im_0 P_x_Re_3 P_x_Re_2 P_x_Re_1 P_x_Re_0 P_y_Im_3 P_y_Im_2 P_y_Im_1 P_y_Im_0 P_y_Re_3 P_y_Re_2 P_y_Re_1 P_y_Re_0) + (let ((P_x_Im_is_in_range (shift WCP_RES k)) + (P_x_Re_is_in_range (shift WCP_RES (+ k 4))) + (P_y_Im_is_in_range (shift WCP_RES (+ k 8))) + (P_y_Re_is_in_range (shift WCP_RES (+ k 12))) + (well_formed_coordinates (- 1 MINT_BIT))) + (let ((P_x_is_in_range (* P_x_Im_is_in_range P_x_Re_is_in_range)) + (P_y_is_in_range (* P_y_Im_is_in_range P_y_Re_is_in_range))) + (begin + (wcpGeneralizedCallToLT k P_x_Im_3 P_x_Im_2 P_x_Im_1 P_x_Im_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (wcpGeneralizedCallToLT (+ k 4) P_x_Re_3 P_x_Re_2 P_x_Re_1 P_x_Re_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (wcpGeneralizedCallToLT (+ k 8) P_y_Im_3 P_y_Im_2 P_y_Im_1 P_y_Im_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (wcpGeneralizedCallToLT (+ k 12) P_y_Re_3 P_y_Re_2 P_y_Re_1 P_y_Re_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (eq! well_formed_coordinates (* P_x_is_in_range P_y_is_in_range)) + (isInfinity k (+ P_x_Re_3 P_x_Re_2 P_x_Re_1 P_x_Re_0 + P_x_Im_3 P_x_Im_2 P_x_Im_1 P_x_Im_0 + P_y_Re_3 P_y_Re_2 P_y_Re_1 P_y_Re_0 + P_y_Im_3 P_y_Im_2 P_y_Im_1 P_y_Im_0)) + )))) diff --git a/bls/cancun/utilities/definition_of_wellFormedFpCoordinatesAndInfinityCheck.lisp b/bls/cancun/utilities/definition_of_wellFormedFpCoordinatesAndInfinityCheck.lisp new file mode 100644 index 00000000..7a6a8f2f --- /dev/null +++ b/bls/cancun/utilities/definition_of_wellFormedFpCoordinatesAndInfinityCheck.lisp @@ -0,0 +1,12 @@ +(module bls) + +(defun (wellFormedFpCoordinatesAndInfinityCheck k P_x_3 P_x_2 P_x_1 P_x_0 P_y_3 P_y_2 P_y_1 P_y_0) + (let ((P_x_is_in_range (shift WCP_RES k)) + (P_y_is_in_range (shift WCP_RES (+ k 4))) + (well_formed_coordinates (- 1 MINT_BIT))) + (begin + (wcpGeneralizedCallToLT k P_x_3 P_x_2 P_x_1 P_x_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (wcpGeneralizedCallToLT (+ k 4) P_y_3 P_y_2 P_y_1 P_y_0 BLS_PRIME_3 BLS_PRIME_2 BLS_PRIME_1 BLS_PRIME_0) + (eq! well_formed_coordinates (* P_x_is_in_range P_y_is_in_range)) + (isInfinity k (+ P_x_3 P_x_2 P_x_1 P_x_0 P_y_3 P_y_2 P_y_1 P_y_0)) + ))) \ No newline at end of file diff --git a/constants/constants.lisp b/constants/constants.lisp index 2a297f8f..479a2450 100644 --- a/constants/constants.lisp +++ b/constants/constants.lisp @@ -351,6 +351,27 @@ PHASE_ECPAIRING_RESULT 0x080B ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; BLS MODULE ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + PHASE_DATA_POINT_EVALUATION 0x100A + PHASE_RSLT_POINT_EVALUATION 0x100B + PHASE_DATA_G1_ADD 0x110A + PHASE_RSLT_G1_ADD 0x110B + PHASE_DATA_G1_MSM 0x120A + PHASE_RSLT_G1_MSM 0x120B + PHASE_DATA_G2_ADD 0x130A + PHASE_RSLT_G2_ADD 0x130B + PHASE_DATA_G2_MSM 0x140A + PHASE_RSLT_G2_MSM 0x140B + PHASE_DATA_PAIRING_CHECK 0x150A + PHASE_RSLT_PAIRING_CHECK 0x150B + PHASE_DATA_MAP_FP_TO_G1 0x160A + PHASE_RSLT_MAP_FP_TO_G1 0x160B + PHASE_DATA_MAP_FP2_TO_G2 0x170A + PHASE_RSLT_MAP_FP2_TO_G2 0x170B + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EXP MODULE ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/ecdata/constraints.lisp b/ecdata/constraints.lisp index 3d4b5fe8..f91e1eec 100644 --- a/ecdata/constraints.lisp +++ b/ecdata/constraints.lisp @@ -264,7 +264,7 @@ (if-not-zero (transition_to_result) (will-remain-constant! TRIVIAL_PAIRING))) -(defconstraint set-pairing-result-when-trivial-pairngs () +(defconstraint set-pairing-result-when-trivial-pairings () (let ((pairing_result_hi (next LIMB)) (pairing_result_lo (shift LIMB 2))) (if-not-zero (transition_to_result) diff --git a/zkevm_cancun.bin b/zkevm_cancun.bin new file mode 100644 index 00000000..91bc89cb Binary files /dev/null and b/zkevm_cancun.bin differ diff --git a/zkevm_paris.bin b/zkevm_paris.bin new file mode 100644 index 00000000..14eca3c2 Binary files /dev/null and b/zkevm_paris.bin differ