feat: BLS12-381 pairing

Cargo.toml

@@ -43,3 +43,4 @@ halo2-ecc = { path = "../halo2-lib/halo2-ecc" }
 [patch.crates-io]
 halo2-base = { path = "../halo2-lib/halo2-base" }
 halo2-ecc = { path = "../halo2-lib/halo2-ecc" }
+halo2curves-axiom = { git = "https://github.com/timoftime/halo2curves", branch = "support_bls12-381" }

halo2-base/src/utils/mod.rs

@@ -29,18 +29,45 @@ pub trait BigPrimeField: ScalarField {
     /// * The integer value of `val` is already less than the modulus of `Self`
     fn from_u64_digits(val: &[u64]) -> Self;
 }
+
+macro_rules! impl_big_prime_field { // Implements BigPrimeField for $field with $limbs limbs.
+    ($field:tt, $limbs:expr) => {
+        impl super::BigPrimeField for $field {
+            #[inline(always)]
+            fn from_u64_digits(val: &[u64]) -> Self {
+                let mut raw = [0u64; $limbs];
+                raw[..val.len()].copy_from_slice(val);
+                Self::from(raw)
+            }
+        }
+    };
+}
+
 #[cfg(feature = "halo2-axiom")]
-impl<F> BigPrimeField for F
-where
-    F: ScalarField + From<[u64; 4]>, // Assume [u64; 4] is little-endian. We only implement ScalarField when this is true.
-{
-    #[inline(always)]
-    fn from_u64_digits(val: &[u64]) -> Self {
-        debug_assert!(val.len() <= 4);
-        let mut raw = [0u64; 4];
-        raw[..val.len()].copy_from_slice(val);
-        Self::from(raw)
-    }
+mod bn256 {
+    use crate::halo2_proofs::halo2curves::bn256::{Fq, Fr};
+
+    impl_big_prime_field!(Fr, 4);
+
+    impl_big_prime_field!(Fq, 4);
+}
+
+#[cfg(feature = "halo2-axiom")]
+mod secp256k1 {
+    use crate::halo2_proofs::halo2curves::secp256k1::{Fp, Fq};
+
+    impl_big_prime_field!(Fp, 4);
+
+    impl_big_prime_field!(Fq, 4);
+}
+
+#[cfg(feature = "halo2-axiom")]
+mod bls12_381 {
+    use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fr};
+
+    impl_big_prime_field!(Fr, 4);
+
+    impl_big_prime_field!(Fq, 6);
 }
 
 /// Helper trait to represent a field element that can be converted into [u64] limbs.
@@ -95,7 +122,7 @@ pub trait ScalarField: PrimeField + FromUniformBytes<64> + From<bool> + Hash + O
 
 /// [ScalarField] that is ~256 bits long
 #[cfg(feature = "halo2-pse")]
-pub trait BigPrimeField = PrimeField<Repr = [u8; 32]> + ScalarField;
+pub trait BigPrimeField = PrimeField + ScalarField;
 
 /// Converts an [Iterator] of u64 digits into `number_of_limbs` limbs of `bit_len` bits returned as a [Vec].
 ///

halo2-ecc/Cargo.toml

@@ -14,7 +14,9 @@ itertools = "0.11"
 num-bigint = { version = "0.4", features = ["rand"] }
 num-integer = "0.1"
 num-traits = "0.2"
-rand_core = { version = "0.6", default-features = false, features = ["getrandom"] }
+rand_core = { version = "0.6", default-features = false, features = [
+    "getrandom",
+] }
 rand = "0.8"
 rand_chacha = "0.3.1"
 serde = { version = "1.0", features = ["derive"] }
@@ -23,6 +25,9 @@ rayon = "1.8"
 test-case = "3.1.0"
 
 halo2-base = { version = "=0.4.1", path = "../halo2-base", default-features = false }
+# Use additional axiom-crypto halo2curves for BLS12-381 chips when [feature = "halo2-pse"] is on,
+# because the PSE halo2curves does not support BLS12-381 chips and Halo2 depnds on lower major version so patching it is not possible
+halo2curves = { package = "halo2curves-axiom", version = "0.5", optional = true }
 
 # plotting circuit layout
 plotters = { version = "0.3.0", optional = true }
@@ -32,7 +37,9 @@ ark-std = { version = "0.3.0", features = ["print-trace"] }
 pprof = { version = "0.13", features = ["criterion", "flamegraph"] }
 criterion = "0.5.1"
 criterion-macro = "0.4"
-halo2-base = { version = "=0.4.1", path = "../halo2-base", default-features = false, features = ["test-utils"] }
+halo2-base = { version = "=0.4.1", path = "../halo2-base", default-features = false, features = [
+    "test-utils",
+] }
 test-log = "0.2.12"
 env_logger = "0.10.0"
 
@@ -41,7 +48,7 @@ default = ["jemallocator", "halo2-axiom", "display"]
 dev-graph = ["halo2-base/dev-graph", "plotters"]
 display = ["halo2-base/display"]
 asm = ["halo2-base/asm"]
-halo2-pse = ["halo2-base/halo2-pse"]
+halo2-pse = ["halo2-base/halo2-pse", "halo2curves"]
 halo2-axiom = ["halo2-base/halo2-axiom"]
 jemallocator = ["halo2-base/jemallocator"]
 mimalloc = ["halo2-base/mimalloc"]

halo2-ecc/configs/bls12_381/bench_ec_add.config

@@ -0,0 +1,5 @@
+{"strategy":"Simple","degree":15,"num_advice":10,"num_lookup_advice":2,"num_fixed":1,"lookup_bits":14,"limb_bits":104,"num_limbs":5,"batch_size":100}
+{"strategy":"Simple","degree":16,"num_advice":5,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":15,"limb_bits":104,"num_limbs":5,"batch_size":100}
+{"strategy":"Simple","degree":17,"num_advice":4,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":16,"limb_bits":104,"num_limbs":5,"batch_size":100}
+{"strategy":"Simple","degree":18,"num_advice":2,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":17,"limb_bits":104,"num_limbs":5,"batch_size":100}
+{"strategy":"Simple","degree":19,"num_advice":1,"num_lookup_advice":0,"num_fixed":1,"lookup_bits":18,"limb_bits":104,"num_limbs":5,"batch_size":100}

halo2-ecc/configs/bls12_381/bench_pairing.config

@@ -0,0 +1,9 @@
+{"strategy":"Simple","degree":14,"num_advice":211,"num_lookup_advice":27,"num_fixed":1,"lookup_bits":13,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":15,"num_advice":105,"num_lookup_advice":14,"num_fixed":1,"lookup_bits":14,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":16,"num_advice":50,"num_lookup_advice":6,"num_fixed":1,"lookup_bits":15,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":17,"num_advice":25,"num_lookup_advice":3,"num_fixed":1,"lookup_bits":16,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":18,"num_advice":13,"num_lookup_advice":2,"num_fixed":1,"lookup_bits":17,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":20,"num_advice":3,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":19,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":21,"num_advice":2,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":20,"limb_bits":104,"num_limbs":5}
+{"strategy":"Simple","degree":22,"num_advice":1,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":21,"limb_bits":104,"num_limbs":5}

halo2-ecc/configs/bls12_381/ec_add_circuit.config

@@ -0,0 +1 @@
+{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":104,"num_limbs":5,"batch_size":100}

halo2-ecc/configs/bls12_381/pairing_circuit.config

@@ -0,0 +1 @@
+{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":104,"num_limbs":5}

halo2-ecc/src/bigint/carry_mod.rs

@@ -56,11 +56,10 @@ pub fn crt<F: BigPrimeField>(
     // Let n' <= quot_max_bits - n(k-1) - 1
     // If quot[i] <= 2^n for i < k - 1 and quot[k-1] <= 2^{n'} then
     // quot < 2^{n(k-1)+1} + 2^{n' + n(k-1)} = (2+2^{n'}) 2^{n(k-1)} < 2^{n'+1} * 2^{n(k-1)} <= 2^{quot_max_bits - n(k-1)} * 2^{n(k-1)}
-    let quot_last_limb_bits = quot_max_bits - n * (k - 1);
-
+    let bits_wo_last_limb: usize = n * (k - 1);
+    // it takes `out_num_limbs` to represented a native field element, any extra limbs are used to carry.
+    let out_num_limbs = modulus.bits().div_ceil(n as u64) as usize;
     let out_max_bits = modulus.bits() as usize;
-    // we assume `modulus` requires *exactly* `k` limbs to represent (if `< k` limbs ok, you should just be using that)
-    let out_last_limb_bits = out_max_bits - n * (k - 1);
 
     // these are witness vectors:
     // we need to find `out_vec` as a proper BigInt with k limbs
@@ -137,14 +136,21 @@ pub fn crt<F: BigPrimeField>(
     //}
 
     // range check limbs of `out` are in [0, 2^n) except last limb should be in [0, 2^out_last_limb_bits)
-    for (out_index, out_cell) in out_assigned.iter().enumerate() {
-        let limb_bits = if out_index == k - 1 { out_last_limb_bits } else { n };
+    for (out_index, out_cell) in out_assigned.iter().take(out_num_limbs).enumerate() {
+        // we assume `modulus` requires *exactly* `k` limbs to represent (if `< k` limbs ok, you should just be using that)
+        let limb_bits = if out_index == k - 1 { out_max_bits - bits_wo_last_limb } else { n };
         range.range_check(ctx, *out_cell, limb_bits);
     }
 
+    // enforce that extra `out` limbs are zero
+    for out_cell in out_assigned.iter().skip(out_num_limbs) {
+        let zero = ctx.load_zero();
+        ctx.constrain_equal(out_cell, &zero);
+    }
+
     // range check that quot_cell in quot_assigned is in [-2^n, 2^n) except for last cell check it's in [-2^quot_last_limb_bits, 2^quot_last_limb_bits)
-    for (q_index, quot_cell) in quot_assigned.iter().enumerate() {
-        let limb_bits = if q_index == k - 1 { quot_last_limb_bits } else { n };
+    for (q_index, quot_cell) in quot_assigned.iter().take(out_num_limbs).enumerate() {
+        let limb_bits = if q_index == k - 1 { quot_max_bits - bits_wo_last_limb } else { n };
         let limb_base =
             if q_index == k - 1 { range.gate().pow_of_two()[limb_bits] } else { limb_bases[1] };
 
@@ -153,6 +159,13 @@ pub fn crt<F: BigPrimeField>(
         range.range_check(ctx, quot_shift, limb_bits + 1);
     }
 
+    // enforce that extra quotient limbs are zero
+    for quot_cell in quot_assigned.iter().skip(out_num_limbs) {
+        let zero = ctx.load_zero();
+        ctx.constrain_equal(quot_cell, &zero);
+        continue;
+    }
+
     let check_overflow_int = OverflowInteger::new(
         check_assigned,
         max(max(limb_bits, a.truncation.max_limb_bits) + 1, 2 * n + k_bits),

halo2-ecc/src/bigint/check_carry_mod_to_zero.rs

@@ -34,7 +34,8 @@ pub fn crt<F: BigPrimeField>(
     // see carry_mod.rs for explanation
     let quot_max_bits = trunc_len - 1 + (F::NUM_BITS as usize) - 1 - (modulus.bits() as usize);
     assert!(quot_max_bits < trunc_len);
-    let quot_last_limb_bits = quot_max_bits - n * (k - 1);
+    // it takes `out_num_limbs` to represented a native field element, any extra limbs are used to carry.
+    let out_num_limbs = modulus.bits().div_ceil(n as u64) as usize;
 
     // these are witness vectors:
     // we need to find `quot_vec` as a proper BigInt with k limbs
@@ -89,8 +90,8 @@ pub fn crt<F: BigPrimeField>(
     // }
 
     // range check that quot_cell in quot_assigned is in [-2^n, 2^n) except for last cell check it's in [-2^quot_last_limb_bits, 2^quot_last_limb_bits)
-    for (q_index, quot_cell) in quot_assigned.iter().enumerate() {
-        let limb_bits = if q_index == k - 1 { quot_last_limb_bits } else { n };
+    for (q_index, quot_cell) in quot_assigned.iter().take(out_num_limbs).enumerate() {
+        let limb_bits = if q_index == k - 1 { quot_max_bits - n * (k - 1) } else { n };
         let limb_base =
             if q_index == k - 1 { range.gate().pow_of_two()[limb_bits] } else { limb_bases[1] };
 
@@ -99,6 +100,14 @@ pub fn crt<F: BigPrimeField>(
         range.range_check(ctx, quot_shift, limb_bits + 1);
     }
 
+
+    // enforce that extra quotient limbs are zero
+    for quot_cell in quot_assigned.iter().skip(out_num_limbs) {
+        let zero = ctx.load_zero();
+        ctx.constrain_equal(quot_cell, &zero);
+        continue;
+    }
+
     let check_overflow_int =
         OverflowInteger::new(check_assigned, max(a.truncation.max_limb_bits, 2 * n + k_bits));