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

@@ -30,16 +30,71 @@ pub trait BigPrimeField: ScalarField {
     fn from_u64_digits(val: &[u64]) -> Self;
 }
 #[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 super::BigPrimeField for Fr {
+        #[inline(always)]
+        fn from_u64_digits(val: &[u64]) -> Self {
+            let mut raw = [0u64; 4];
+            raw[..val.len()].copy_from_slice(val);
+            Self::from(raw)
+        }
+    }
+
+    impl super::BigPrimeField for Fq {
+        #[inline(always)]
+        fn from_u64_digits(val: &[u64]) -> Self {
+            let mut raw = [0u64; 4];
+            raw[..val.len()].copy_from_slice(val);
+            Self::from(raw)
+        }
+    }
+}
+
+#[cfg(feature = "halo2-axiom")]
+mod secp256k1 {
+    use crate::halo2_proofs::halo2curves::secp256k1::{Fp, Fq};
+
+    impl super::BigPrimeField for Fp {
+        #[inline(always)]
+        fn from_u64_digits(val: &[u64]) -> Self {
+            let mut raw = [0u64; 4];
+            raw[..val.len()].copy_from_slice(val);
+            Self::from(raw)
+        }
+    }
+
+    impl super::BigPrimeField for Fq {
+        #[inline(always)]
+        fn from_u64_digits(val: &[u64]) -> Self {
+            let mut raw = [0u64; 4];
+            raw[..val.len()].copy_from_slice(val);
+            Self::from(raw)
+        }
+    }
+}
+
+#[cfg(feature = "halo2-axiom")]
+mod bls12_381 {
+    use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fr};
+
+    impl super::BigPrimeField for Fr {
+        #[inline(always)]
+        fn from_u64_digits(val: &[u64]) -> Self {
+            let mut raw = [0u64; 4];
+            raw[..val.len()].copy_from_slice(val);
+            Self::from(raw)
+        }
+    }
+
+    impl super::BigPrimeField for Fq {
+        #[inline(always)]
+        fn from_u64_digits(val: &[u64]) -> Self {
+            let mut raw = [0u64; 6];
+            raw[..val.len()].copy_from_slice(val);
+            Self::from(raw)
+        }
     }
 }
 
@@ -95,7 +150,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 }
@@ -41,7 +46,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":120,"num_limbs":4,"batch_size":100}
+{"strategy":"Simple","degree":16,"num_advice":5,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":15,"limb_bits":120,"num_limbs":4,"batch_size":100}
+{"strategy":"Simple","degree":17,"num_advice":4,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":16,"limb_bits":120,"num_limbs":4,"batch_size":100}
+{"strategy":"Simple","degree":18,"num_advice":2,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":17,"limb_bits":120,"num_limbs":4,"batch_size":100}
+{"strategy":"Simple","degree":19,"num_advice":1,"num_lookup_advice":0,"num_fixed":1,"lookup_bits":18,"limb_bits":120,"num_limbs":4,"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":120,"num_limbs":4}
+{"strategy":"Simple","degree":15,"num_advice":105,"num_lookup_advice":14,"num_fixed":1,"lookup_bits":14,"limb_bits":120,"num_limbs":4}
+{"strategy":"Simple","degree":16,"num_advice":50,"num_lookup_advice":6,"num_fixed":1,"lookup_bits":15,"limb_bits":120,"num_limbs":4}
+{"strategy":"Simple","degree":17,"num_advice":25,"num_lookup_advice":3,"num_fixed":1,"lookup_bits":16,"limb_bits":120,"num_limbs":4}
+{"strategy":"Simple","degree":18,"num_advice":13,"num_lookup_advice":2,"num_fixed":1,"lookup_bits":17,"limb_bits":120,"num_limbs":4}
+{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":120,"num_limbs":4}
+{"strategy":"Simple","degree":20,"num_advice":3,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":19,"limb_bits":120,"num_limbs":4}
+{"strategy":"Simple","degree":21,"num_advice":2,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":20,"limb_bits":120,"num_limbs":4}
+{"strategy":"Simple","degree":22,"num_advice":1,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":21,"limb_bits":120,"num_limbs":4}

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,11 @@ 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);
+    // `has_redunant_limb` will be true when native element can be represented in k-1 limbs, but some cases require an extra limb to carry.
+    // This is only the case for BLS12-381, which requires k=5 and n > 102 because of the check above.
+    let has_redunant_limb = quot_max_bits < bits_wo_last_limb;
     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
@@ -138,13 +138,24 @@ 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 };
+        if has_redunant_limb && out_index == k - 1 {
+            let zero = ctx.load_zero();
+            ctx.constrain_equal(out_cell, &zero);
+            continue;
+        }
+        // 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);
     }
 
     // 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 };
+        if has_redunant_limb && q_index == k - 1 {
+            let zero = ctx.load_zero();
+            ctx.constrain_equal(quot_cell, &zero);
+            continue;
+        }
+        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] };
 

halo2-ecc/src/bigint/check_carry_mod_to_zero.rs

@@ -34,7 +34,10 @@ 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);
+    let bits_wo_last_limb: usize = n * (k - 1);
+    // `has_redunant_limb` will be true when native element can be represented in k-1 limbs, but some cases require an extra limb to carry.
+    // This is only the case for BLS12-381, which requires k=5 and n > 102 because of the check above.
+    let has_redunant_limb = quot_max_bits < bits_wo_last_limb;
 
     // these are witness vectors:
     // we need to find `quot_vec` as a proper BigInt with k limbs
@@ -90,7 +93,12 @@ 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 };
+        if has_redunant_limb && q_index == k - 1 {
+            let zero = ctx.load_zero();
+            ctx.constrain_equal(quot_cell, &zero);
+            continue;
+        }
+        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] };