bls MPcheck Cairo1 interfaces

keep-starknet-strange · Jul 20, 2024 · 2f6df4f · 2f6df4f
1 parent 307c711
commit 2f6df4f
Show file tree

Hide file tree

Showing 4 changed files with 287 additions and 19 deletions.
diff --git a/src/cairo/src/definitions.cairo b/src/cairo/src/definitions.cairo
@@ -1,4 +1,5 @@
 use core::circuit::{u96, u384};
+use garaga::basic_field_ops::{neg_mod_p};
 
 #[derive(Copy, Drop, Debug, PartialEq)]
 struct G1Point {
@@ -37,14 +38,95 @@ struct E12D {
     w11: u384,
 }
 
-#[derive(Drop, Debug, PartialEq)]
-struct MillerLoopResultScalingFactor {
+#[derive(Copy, Drop, Debug, PartialEq)]
+struct E12DMulQuotient {
     w0: u384,
     w1: u384,
     w2: u384,
     w3: u384,
     w4: u384,
     w5: u384,
+    w6: u384,
+    w7: u384,
+    w8: u384,
+    w9: u384,
+    w10: u384,
+}
+
+trait FieldDefinitions<F> {
+    fn one() -> F;
+    fn zero() -> F;
+    fn conjugate(self: F, curve_index: usize) -> F;
+}
+
+impl E12DDefinitions of FieldDefinitions<E12D> {
+    fn one() -> E12D {
+        E12D {
+            w0: u384 { limb0: 1, limb1: 0, limb2: 0, limb3: 0 },
+            w1: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w2: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w3: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w4: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w5: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w6: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w7: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w8: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w9: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w10: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w11: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+        }
+    }
+
+    fn zero() -> E12D {
+        E12D {
+            w0: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w1: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w2: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w3: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w4: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w5: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w6: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w7: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w8: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w9: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w10: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+            w11: u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 },
+        }
+    }
+
+    fn conjugate(self: E12D, curve_index: usize) -> E12D {
+        let p = get_p(curve_index);
+        E12D {
+            w0: self.w0,
+            w1: neg_mod_p(self.w1, p),
+            w2: self.w2,
+            w3: neg_mod_p(self.w3, p),
+            w4: self.w4,
+            w5: neg_mod_p(self.w5, p),
+            w6: self.w6,
+            w7: neg_mod_p(self.w7, p),
+            w8: self.w8,
+            w9: neg_mod_p(self.w9, p),
+            w10: self.w10,
+            w11: neg_mod_p(self.w11, p),
+        }
+    }
+}
+
+fn test_one() {
+    let one = E12DDefinitions::one();
+    let conjugate = one.conjugate(0);
+    assert_eq!(one, conjugate);
+}
+
+#[derive(Drop, Debug, PartialEq)]
+struct MillerLoopResultScalingFactor {
+    w0: u384,
+    w2: u384,
+    w4: u384,
+    w6: u384,
+    w8: u384,
+    w10: u384,
 }
 
 // From a G1G2Pair(Px, Py, Qx0, Qx1, Qy0, Qy1), returns (1/Py, -Px/Py)

diff --git a/src/cairo/src/lib.cairo b/src/cairo/src/lib.cairo
@@ -3,7 +3,7 @@ mod utils;
 mod ec_ops;
 mod pairing;
 mod circuits;
-mod groth16;
+// mod groth16;
 mod basic_field_ops;
 
 #[cfg(test)]

diff --git a/src/cairo/src/pairing.cairo b/src/cairo/src/pairing.cairo
@@ -10,11 +10,15 @@ use garaga::circuits::multi_pairing_check::{
     run_BLS12_381_MP_CHECK_PREPARE_LAMBDA_ROOT_circuit,
     run_BN254_MP_CHECK_PREPARE_LAMBDA_ROOT_circuit, run_BLS12_381_MP_CHECK_INIT_BIT_2_circuit,
     run_BLS12_381_MP_CHECK_INIT_BIT_3_circuit, run_BN254_MP_CHECK_INIT_BIT_2_circuit,
-    run_BN254_MP_CHECK_INIT_BIT_3_circuit
+    run_BN254_MP_CHECK_INIT_BIT_3_circuit, run_BN254_MP_CHECK_FINALIZE_BN_2_circuit,
+    run_BN254_MP_CHECK_FINALIZE_BN_3_circuit, run_BLS12_381_MP_CHECK_FINALIZE_BLS_2_circuit,
+    run_BLS12_381_MP_CHECK_FINALIZE_BLS_3_circuit
 };
+use garaga::circuits::extf_mul::{run_BLS12_381_FP12_MUL_ASSERT_ONE_circuit};
+
 use garaga::definitions::{
     G1Point, G2Point, G1G2Pair, u384, bn_bits, bls_bits, MillerLoopResultScalingFactor, E12D,
-    BNProcessedPair, BLSProcessedPair
+    E12DMulQuotient, BNProcessedPair, BLSProcessedPair, E12DDefinitions
 };
 use core::option::Option;
 use garaga::utils;
@@ -64,11 +68,11 @@ fn multi_pairing_check_bls12_381_2_pairs(
     pair1: G1G2Pair,
     lambda_root_inverse: E12D,
     w: MillerLoopResultScalingFactor,
-    Ris: Array<E12D>,
-    Q: Array<u384>
+    Ris: Span<E12D>,
+    big_Q: Array<u384>
 ) -> bool {
     assert!(
-        Q.len() == 54,
+        big_Q.len() == 54,
         "Wrong Q degree for BLS12-381 2-Pairs Paring check, should be degree 53 (54 coefficients)"
     );
     assert!(
@@ -78,6 +82,115 @@ fn multi_pairing_check_bls12_381_2_pairs(
         run_BLS12_381_MP_CHECK_PREPARE_PAIRS_2_circuit(
         pair0.p, pair1.p
     );
+
+    // Hash Inputs.
+
+    let _h = utils::hash_G1G2Pair(pair0, 'MPCHECK_BLS_12_381_2P');
+    let _h = utils::hash_G1G2Pair(pair1, _h);
+    // Hash Ris to obtain base random coefficient c0
+    let c_i_felt252: felt252 = utils::hash_E12D_transcript(Ris, _h);
+    let mut c_i: u384 = c_i_felt252.into();
+
+    // Hash Q = (Σ_i c_i*Q_i) to obtain random evaluation point z
+    let z_felt252: felt252 = utils::hash_u384_transcript(big_Q.span(), 0);
+    let z: u384 = z_felt252.into();
+
+    // Precompute lambda root evaluated in Z:
+    let (conjugate_c_inv_of_z, w_of_z, c_inv_of_z_frob_1): (u384, u384, u384) =
+        run_BLS12_381_MP_CHECK_PREPARE_LAMBDA_ROOT_circuit(
+        lambda_root_inverse, z, w
+    );
+
+    // init bit for bls is 1:
+    let R_0 = Ris.at(0);
+    let (_Q0, _Q1, _lhs, _f_1_of_z) = run_BLS12_381_MP_CHECK_INIT_BIT_2_circuit(
+        processed_pair0.yInv,
+        processed_pair0.xNegOverY,
+        pair0.q,
+        processed_pair1.yInv,
+        processed_pair1.xNegOverY,
+        pair1.q,
+        *R_0,
+        c_i,
+        z,
+        conjugate_c_inv_of_z
+    );
+
+    let mut Q0 = _Q0;
+    let mut Q1 = _Q1;
+    let mut LHS = _lhs;
+    let mut f_i_of_z = _f_1_of_z;
+
+    // Σ_i (Π_k (c_i*P_k(z)))  = (Σ_i c_i*Q_i(z)) * P(z) + Σ_i c_i * R_i(z)
+    // <=> Σ_i (Π_k (c_i*P_k(z))) - Σ_i c_i * R_i(z) = (Σ_i c_i*Q_i(z)) * P(z)
+    // => LHS = Σ_i (Π_k (c_i*P_k(z))) - Σ_i c_i * R_i(z)
+
+    // rest of miller loop
+    let mut bits = bls_bits.span();
+    let mut R_i_index = 1;
+
+    while let Option::Some(bit) = bits.pop_front() {
+        let R_i = Ris.at(R_i_index);
+        R_i_index += 1;
+        match *bit {
+            0 => {
+                let (
+                    _Q0, _Q1, _f_i_plus_one_of_z, _LHS, _c_i
+                ): (G2Point, G2Point, u384, u384, u384) =
+                    run_BLS12_381_MP_CHECK_BIT0_LOOP_2_circuit(
+                    processed_pair0.yInv,
+                    processed_pair0.xNegOverY,
+                    Q0,
+                    processed_pair1.yInv,
+                    processed_pair1.xNegOverY,
+                    Q1,
+                    LHS,
+                    f_i_of_z,
+                    *R_i,
+                    c_i,
+                    z
+                );
+                Q0 = _Q0;
+                Q1 = _Q1;
+                LHS = _LHS;
+                f_i_of_z = _f_i_plus_one_of_z;
+                c_i = _c_i;
+            },
+            _ => {
+                let (_Q0, _Q1, _LHS, _f_i_plus_one_of_z, _c_i) =
+                    run_BLS12_381_MP_CHECK_BIT1_LOOP_2_circuit(
+                    processed_pair0.yInv,
+                    processed_pair0.xNegOverY,
+                    Q0,
+                    pair0.q,
+                    processed_pair1.yInv,
+                    processed_pair1.xNegOverY,
+                    Q1,
+                    pair1.q,
+                    LHS,
+                    f_i_of_z,
+                    *R_i,
+                    conjugate_c_inv_of_z,
+                    c_i,
+                    z
+                );
+                Q0 = _Q0;
+                Q1 = _Q1;
+                LHS = _LHS;
+                f_i_of_z = _f_i_plus_one_of_z;
+                c_i = _c_i;
+            },
+        }
+    };
+
+    let R_64 = Ris.at(64);
+    let (check,) = run_BLS12_381_MP_CHECK_FINALIZE_BLS_3_circuit(
+        *R_64, c_i, w_of_z, z, c_inv_of_z_frob_1, LHS, f_i_of_z, big_Q
+    );
+
+    assert!(check == u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 }, "Final check failed");
+
+    assert!(*Ris.at(64) == E12DDefinitions::one());
     return true;
 }
 
@@ -88,15 +201,15 @@ fn multi_pairing_check_bls12_381_3_pairs(
     lambda_root_inverse: E12D,
     w: MillerLoopResultScalingFactor,
     Ris: Span<E12D>,
-    big_Q: Array<u384>
+    big_Q: Array<u384>,
+    precomputed_miller_loop_result: Option<E12D>,
+    small_Q: Option<E12DMulQuotient>
 ) -> bool {
     assert!(
         big_Q.len() == 70,
         "Wrong Q degree for BLS12-381 3-Pairs Paring check, should be of degree 69 (70 coefficients)"
     );
-    assert!(
-        Ris.len() == 65, "Wrong Number of Ris for BLS12-381 3-Pairs Paring check, should be 65"
-    );
+    assert!(Ris.len() == 65, "Wrong Number of Ris for BLS12-381 3-Pairs Paring check");
 
     let (
         processed_pair0, processed_pair1, processed_pair2
@@ -115,11 +228,13 @@ fn multi_pairing_check_bls12_381_3_pairs(
     let mut c_i: u384 = c_i_felt252.into();
 
     // Hash Q = (Σ_i c_i*Q_i) to obtain random evaluation point z
-    let z: u384 = utils::hash_u384_transcript(big_Q, 0).into();
+    let z_felt252: felt252 = utils::hash_u384_transcript(big_Q.span(), 0);
+    let z: u384 = z_felt252.into();
 
     // Precompute lambda root evaluated in Z:
-    let (conjugate_c_inv_of_z): (u384,) = run_BLS12_381_MP_CHECK_PREPARE_LAMBDA_ROOT_circuit(
-        lambda_root_inverse, z
+    let (conjugate_c_inv_of_z, w_of_z, c_inv_of_z_frob_1): (u384, u384, u384) =
+        run_BLS12_381_MP_CHECK_PREPARE_LAMBDA_ROOT_circuit(
+        lambda_root_inverse, z, w
     );
 
     // init bit for bls is 1:
@@ -183,6 +298,7 @@ fn multi_pairing_check_bls12_381_3_pairs(
                 Q2 = _Q2;
                 LHS = _LHS;
                 f_i_of_z = _f_i_plus_one_of_z;
+                c_i = _c_i;
             },
             _ => {
                 let (_Q0, _Q1, _Q2, _LHS, _f_i_plus_one_of_z, _c_i) =
@@ -215,6 +331,31 @@ fn multi_pairing_check_bls12_381_3_pairs(
             },
         }
     };
-    return true;
+
+    let R_64 = Ris.at(64);
+    let (check,) = run_BLS12_381_MP_CHECK_FINALIZE_BLS_3_circuit(
+        *R_64, c_i, w_of_z, z, c_inv_of_z_frob_1, LHS, f_i_of_z, big_Q
+    );
+
+    assert!(check == u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 }, "Final check failed");
+
+    match precomputed_miller_loop_result {
+        Option::Some(M) => {
+            // Use precomputed miller loop result & check conj(f) * M = 1
+            let f_conjugate = (*Ris.at(64)).conjugate(curve_index: 1);
+            let z = utils::hash_E12DMulQuotient(small_Q.unwrap(), z_felt252);
+
+            let (check) = run_BLS12_381_FP12_MUL_ASSERT_ONE_circuit(
+                f_conjugate, M, small_Q.unwrap(), z.into()
+            );
+            assert!(check == u384 { limb0: 0, limb1: 0, limb2: 0, limb3: 0 });
+            return true;
+        },
+        Option::None => {
+            // No need to conjugate as conjugate(One) = One
+            assert!(*Ris.at(64) == E12DDefinitions::one());
+            return true;
+        },
+    }
 }