From 12a68f3b2219c405c96f1c0d9c8e6153fe5b6460 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Sat, 30 Sep 2023 20:13:54 +0200 Subject: [PATCH 01/22] add bls12 module --- halo2-ecc/src/bls12_381/final_exp.rs | 331 +++++++++++++++++++ halo2-ecc/src/bls12_381/mod.rs | 16 + halo2-ecc/src/bls12_381/notes.md | 4 + halo2-ecc/src/bls12_381/pairing.rs | 457 +++++++++++++++++++++++++++ 4 files changed, 808 insertions(+) create mode 100644 halo2-ecc/src/bls12_381/final_exp.rs create mode 100644 halo2-ecc/src/bls12_381/mod.rs create mode 100644 halo2-ecc/src/bls12_381/notes.md create mode 100644 halo2-ecc/src/bls12_381/pairing.rs diff --git a/halo2-ecc/src/bls12_381/final_exp.rs b/halo2-ecc/src/bls12_381/final_exp.rs new file mode 100644 index 00000000..575ecab7 --- /dev/null +++ b/halo2-ecc/src/bls12_381/final_exp.rs @@ -0,0 +1,331 @@ +use super::pairing::fq2_mul_by_nonresidue; +use super::{Fp12Chip, Fp2Chip, FpChip, FqPoint}; +use crate::halo2_proofs::arithmetic::Field; +use crate::{ + ecc::get_naf, + fields::{fp12::mul_no_carry_w6, vector::FieldVector, FieldChip, PrimeField}, +}; +use halo2_base::{gates::GateInstructions, utils::modulus, Context, QuantumCell::Constant}; +use halo2curves::bls12_381::{Fq, Fq12, Fq2, BLS_X, FROBENIUS_COEFF_FQ12_C1}; +use itertools::Itertools; +use num_bigint::BigUint; + +const XI_0: i64 = 1; + +impl<'chip, F: PrimeField> Fp12Chip<'chip, F> { + // computes a ** (p ** power) + // only works for p = 3 (mod 4) and p = 1 (mod 6) + pub fn frobenius_map( + &self, + ctx: &mut Context, + a: &>::FieldPoint, + power: usize, + ) -> >::FieldPoint { + assert_eq!(modulus::() % 4u64, BigUint::from(3u64)); + assert_eq!(modulus::() % 6u64, BigUint::from(1u64)); + assert_eq!(a.0.len(), 12); + let pow = power % 12; + let mut out_fp2 = Vec::with_capacity(6); + + let fp_chip = self.fp_chip(); + let fp2_chip = Fp2Chip::::new(fp_chip); + for i in 0..6 { + let frob_coeff = FROBENIUS_COEFF_FQ12_C1[pow].pow_vartime([i as u64]); + // possible optimization (not implemented): load `frob_coeff` as we multiply instead of loading first + // frobenius map is used infrequently so this is a small optimization + + let mut a_fp2 = FieldVector(vec![a[i].clone(), a[i + 6].clone()]); + if pow % 2 != 0 { + a_fp2 = fp2_chip.conjugate(ctx, a_fp2); + } + // if `frob_coeff` is in `Fp` and not just `Fp2`, then we can be more efficient in multiplication + if frob_coeff == Fq2::one() { + out_fp2.push(a_fp2); + } else if frob_coeff.c1 == Fq::zero() { + let frob_fixed = fp_chip.load_constant(ctx, frob_coeff.c0); + { + let out_nocarry = fp2_chip.0.fp_mul_no_carry(ctx, a_fp2, frob_fixed); + out_fp2.push(fp2_chip.carry_mod(ctx, out_nocarry)); + } + } else { + let frob_fixed = fp2_chip.load_constant(ctx, frob_coeff); + out_fp2.push(fp2_chip.mul(ctx, a_fp2, frob_fixed)); + } + } + + let out_coeffs = out_fp2 + .iter() + .map(|x| x[0].clone()) + .chain(out_fp2.iter().map(|x| x[1].clone())) + .collect(); + + FieldVector(out_coeffs) + } + + // exp is in little-endian + /// # Assumptions + /// * `a` is nonzero field point + pub fn pow( + &self, + ctx: &mut Context, + a: &>::FieldPoint, + exp: Vec, + ) -> >::FieldPoint { + let mut res = a.clone(); + let mut is_started = false; + let naf = get_naf(exp); + + for &z in naf.iter().rev() { + if is_started { + res = self.mul(ctx, &res, &res); + } + + if z != 0 { + assert!(z == 1 || z == -1); + if is_started { + res = if z == 1 { + self.mul(ctx, &res, a) + } else { + self.divide_unsafe(ctx, &res, a) + }; + } else { + assert_eq!(z, 1); + is_started = true; + } + } + } + res + } + + // assume input is an element of Fp12 in the cyclotomic subgroup GΦ₁₂ + // A cyclotomic group is a subgroup of Fp^n defined by + // GΦₙ(p) = {α ∈ Fpⁿ : α^{Φₙ(p)} = 1} + + // below we implement compression and decompression for an element GΦ₁₂ following Theorem 3.1 of https://eprint.iacr.org/2010/542.pdf + // Fp4 = Fp2(w^3) where (w^3)^2 = XI_0 +u + // Fp12 = Fp4(w) where w^3 = w^3 + + /// in = g0 + g2 w + g4 w^2 + g1 w^3 + g3 w^4 + g5 w^5 where g_i = g_i0 + g_i1 * u are elements of Fp2 + /// out = Compress(in) = [ g2, g3, g4, g5 ] + pub fn cyclotomic_compress(&self, a: &FqPoint) -> Vec> { + let a = &a.0; + let g2 = FieldVector(vec![a[1].clone(), a[1 + 6].clone()]); + let g3 = FieldVector(vec![a[4].clone(), a[4 + 6].clone()]); + let g4 = FieldVector(vec![a[2].clone(), a[2 + 6].clone()]); + let g5 = FieldVector(vec![a[5].clone(), a[5 + 6].clone()]); + vec![g2, g3, g4, g5] + } + + /// Input: + /// * `compression = [g2, g3, g4, g5]` where g_i are proper elements of Fp2 + /// Output: + /// * `Decompress(compression) = g0 + g2 w + g4 w^2 + g1 w^3 + g3 w^4 + g5 w^5` where + /// * All elements of output are proper elements of Fp2 and: + /// c = XI0 + u + /// if g2 != 0: + /// g1 = (g5^2 * c + 3 g4^2 - 2 g3)/(4g2) + /// g0 = (2 g1^2 + g2 * g5 - 3 g3*g4) * c + 1 + /// if g2 = 0: + /// g1 = (2 g4 * g5)/g3 + /// g0 = (2 g1^2 - 3 g3 * g4) * c + 1 + pub fn cyclotomic_decompress( + &self, + ctx: &mut Context, + compression: Vec>, + ) -> FqPoint { + let [g2, g3, g4, g5]: [_; 4] = compression.try_into().unwrap(); + + let fp_chip = self.fp_chip(); + let fp2_chip = Fp2Chip::::new(fp_chip); + let g5_sq = fp2_chip.mul_no_carry(ctx, &g5, &g5); + let g5_sq_c = mul_no_carry_w6::<_, _, XI_0>(fp_chip, ctx, g5_sq); + + let g4_sq = fp2_chip.mul_no_carry(ctx, &g4, &g4); + let g4_sq_3 = fp2_chip.scalar_mul_no_carry(ctx, &g4_sq, 3); + let g3_2 = fp2_chip.scalar_mul_no_carry(ctx, &g3, 2); + + let mut g1_num = fp2_chip.add_no_carry(ctx, &g5_sq_c, &g4_sq_3); + g1_num = fp2_chip.sub_no_carry(ctx, &g1_num, &g3_2); + // can divide without carrying g1_num or g1_denom (I think) + let g2_4 = fp2_chip.scalar_mul_no_carry(ctx, &g2, 4); + let g1_1 = fp2_chip.divide_unsafe(ctx, &g1_num, &g2_4); + + let g4_g5 = fp2_chip.mul_no_carry(ctx, &g4, &g5); + let g1_num = fp2_chip.scalar_mul_no_carry(ctx, &g4_g5, 2); + let g1_0 = fp2_chip.divide_unsafe(ctx, &g1_num, &g3); + + let g2_is_zero = fp2_chip.is_zero(ctx, &g2); + // resulting `g1` is already in "carried" format (witness is in `[0, p)`) + let g1 = fp2_chip.0.select(ctx, g1_0, g1_1, g2_is_zero); + + // share the computation of 2 g1^2 between the two cases + let g1_sq = fp2_chip.mul_no_carry(ctx, &g1, &g1); + let g1_sq_2 = fp2_chip.scalar_mul_no_carry(ctx, &g1_sq, 2); + + let g2_g5 = fp2_chip.mul_no_carry(ctx, &g2, &g5); + let g3_g4 = fp2_chip.mul_no_carry(ctx, &g3, &g4); + let g3_g4_3 = fp2_chip.scalar_mul_no_carry(ctx, &g3_g4, 3); + let temp = fp2_chip.add_no_carry(ctx, &g1_sq_2, &g2_g5); + let temp = fp2_chip.0.select(ctx, g1_sq_2, temp, g2_is_zero); + let temp = fp2_chip.sub_no_carry(ctx, &temp, &g3_g4_3); + let mut g0 = mul_no_carry_w6::<_, _, XI_0>(fp_chip, ctx, temp); + + // compute `g0 + 1` + g0[0].truncation.limbs[0] = + fp2_chip.gate().add(ctx, g0[0].truncation.limbs[0], Constant(F::one())); + g0[0].native = fp2_chip.gate().add(ctx, g0[0].native, Constant(F::one())); + g0[0].truncation.max_limb_bits += 1; + g0[0].value += 1usize; + + // finally, carry g0 + let g0 = fp2_chip.carry_mod(ctx, g0); + + let mut g0 = g0.into_iter(); + let mut g1 = g1.into_iter(); + let mut g2 = g2.into_iter(); + let mut g3 = g3.into_iter(); + let mut g4 = g4.into_iter(); + let mut g5 = g5.into_iter(); + + let mut out_coeffs = Vec::with_capacity(12); + for _ in 0..2 { + out_coeffs.append(&mut vec![ + g0.next().unwrap(), + g2.next().unwrap(), + g4.next().unwrap(), + g1.next().unwrap(), + g3.next().unwrap(), + g5.next().unwrap(), + ]); + } + FieldVector(out_coeffs) + } + + // input is [g2, g3, g4, g5] = C(g) in compressed format of `cyclotomic_compress` + // assume all inputs are proper Fp2 elements + // output is C(g^2) = [h2, h3, h4, h5] computed using Theorem 3.2 of https://eprint.iacr.org/2010/542.pdf + // all output elements are proper Fp2 elements (with carry) + // c = XI_0 + u + // h2 = 2(g2 + 3*c*B_45) + // h3 = 3(A_45 - (c+1)B_45) - 2g3 + // h4 = 3(A_23 - (c+1)B_23) - 2g4 + // h5 = 2(g5 + 3B_23) + // A_ij = (g_i + g_j)(g_i + c g_j) + // B_ij = g_i g_j + pub fn cyclotomic_square( + &self, + ctx: &mut Context, + compression: &[FqPoint], + ) -> Vec> { + assert_eq!(compression.len(), 4); + let g2 = &compression[0]; + let g3 = &compression[1]; + let g4 = &compression[2]; + let g5 = &compression[3]; + + let fp_chip = self.fp_chip(); + let fp2_chip = Fp2Chip::::new(fp_chip); + + let g2_plus_g3 = fp2_chip.add_no_carry(ctx, g2, g3); + let cg3 = mul_no_carry_w6::, XI_0>(fp_chip, ctx, g3.into()); + let g2_plus_cg3 = fp2_chip.add_no_carry(ctx, g2, &cg3); + let a23 = fp2_chip.mul_no_carry(ctx, &g2_plus_g3, &g2_plus_cg3); + + let g4_plus_g5 = fp2_chip.add_no_carry(ctx, g4, g5); + let cg5 = mul_no_carry_w6::<_, _, XI_0>(fp_chip, ctx, g5.into()); + let g4_plus_cg5 = fp2_chip.add_no_carry(ctx, g4, &cg5); + let a45 = fp2_chip.mul_no_carry(ctx, &g4_plus_g5, &g4_plus_cg5); + + let b23 = fp2_chip.mul_no_carry(ctx, g2, g3); + let b45 = fp2_chip.mul_no_carry(ctx, g4, g5); + let b45_c = mul_no_carry_w6::<_, _, XI_0>(fp_chip, ctx, b45.clone()); + + let mut temp = fp2_chip.scalar_mul_and_add_no_carry(ctx, &b45_c, g2, 3); + let h2 = fp2_chip.scalar_mul_no_carry(ctx, &temp, 2); + + temp = fp2_chip.add_no_carry(ctx, b45_c, b45); + temp = fp2_chip.sub_no_carry(ctx, &a45, temp); + temp = fp2_chip.scalar_mul_no_carry(ctx, temp, 3); + let h3 = fp2_chip.scalar_mul_and_add_no_carry(ctx, g3, temp, -2); + + const XI0_PLUS_1: i64 = XI_0 + 1; + // (c + 1) = (XI_0 + 1) + u + temp = mul_no_carry_w6::, XI0_PLUS_1>(fp_chip, ctx, b23.clone()); + temp = fp2_chip.sub_no_carry(ctx, &a23, temp); + temp = fp2_chip.scalar_mul_no_carry(ctx, temp, 3); + let h4 = fp2_chip.scalar_mul_and_add_no_carry(ctx, g4, temp, -2); + + temp = fp2_chip.scalar_mul_and_add_no_carry(ctx, b23, g5, 3); + let h5 = fp2_chip.scalar_mul_no_carry(ctx, temp, 2); + + [h2, h3, h4, h5].into_iter().map(|h| fp2_chip.carry_mod(ctx, h)).collect() + } + + /// # Assumptions + /// * `a` is a nonzero element in the cyclotomic subgroup + pub fn cyclotomic_pow(&self, ctx: &mut Context, a: FqPoint, exp: u64) -> FqPoint { + let mut res = self.load_private(ctx, Fq12::one()); + let mut found_one = false; + + for bit in (0..64).rev().map(|i| ((exp >> i) & 1) == 1) { + if found_one { + let compressed = self.cyclotomic_square(ctx, &self.cyclotomic_compress(&res)); + res = self.cyclotomic_decompress(ctx, compressed); + } else { + found_one = bit; + } + + if bit { + res = self.mul(ctx, &res, &a); + } + } + + self.conjugate(ctx, res) + } + + // out = in^{(q^12 - 1)/r} + pub fn final_exp( + &self, + ctx: &mut Context, + a: >::FieldPoint, + ) -> >::FieldPoint { + // a^{q^6} = conjugate of a + let f1 = self.conjugate(ctx, a.clone()); + let f2 = self.divide_unsafe(ctx, &f1, a); + let f3 = self.frobenius_map(ctx, &f2, 2); + + let t2 = self.mul(ctx, &f3, &f2); + let t1: FieldVector> = { + let tv = self.cyclotomic_square(ctx, &self.cyclotomic_compress(&t2)); + let tv = self.cyclotomic_decompress(ctx, tv); + self.conjugate(ctx, tv) + }; + let t3 = self.cyclotomic_pow(ctx, t2.clone(), BLS_X); + let t4 = { + let tv = self.cyclotomic_square(ctx, &self.cyclotomic_compress(&t3)); + self.cyclotomic_decompress(ctx, tv) + }; + + let t5 = self.mul(ctx, &t1, &t3); + let t1 = self.cyclotomic_pow(ctx, t5.clone(), BLS_X); + let t0 = self.cyclotomic_pow(ctx, t1.clone(), BLS_X); + let t6 = self.cyclotomic_pow(ctx, t0.clone(), BLS_X); + let t6 = self.mul(ctx, &t6, &t4); + let t4 = self.cyclotomic_pow(ctx, t6.clone(), BLS_X); + let t5 = self.conjugate(ctx, t5); + let t4 = self.mul(ctx, &t4, &t5); + let t4 = self.mul(ctx, &t4, &t2); + let t5 = self.conjugate(ctx, t2.clone()); + let t1 = self.mul(ctx, &t1, &t2); + + let t1 = self.frobenius_map(ctx, &t1, 3); + let t6 = self.mul(ctx, &t6, &t5); + let t6 = self.frobenius_map(ctx, &t6, 1); + let t3 = self.mul(ctx, &t3, &t0); + let t3 = self.frobenius_map(ctx, &t3, 2); + let t3 = self.mul(ctx, &t3, &t1); + let t3 = self.mul(ctx, &t3, &t6); + + self.mul(ctx, &t3, &t4) + } +} diff --git a/halo2-ecc/src/bls12_381/mod.rs b/halo2-ecc/src/bls12_381/mod.rs new file mode 100644 index 00000000..f2493b74 --- /dev/null +++ b/halo2-ecc/src/bls12_381/mod.rs @@ -0,0 +1,16 @@ +use crate::bigint::ProperCrtUint; +use crate::fields::vector::FieldVector; +use crate::fields::{fp, fp12, fp2}; +use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2}; + +// pub mod final_exp; +pub mod pairing; + +pub type FpChip<'range, F> = fp::FpChip<'range, F, Fq>; +pub type FpPoint = ProperCrtUint; +pub type FqPoint = FieldVector>; +pub type Fp2Chip<'chip, F> = fp2::Fp2Chip<'chip, F, FpChip<'chip, F>, Fq2>; +pub type Fp12Chip<'chip, F> = fp12::Fp12Chip<'chip, F, FpChip<'chip, F>, Fq12, 1>; + +// #[cfg(test)] +// pub(crate) mod tests; diff --git a/halo2-ecc/src/bls12_381/notes.md b/halo2-ecc/src/bls12_381/notes.md new file mode 100644 index 00000000..975ac1bc --- /dev/null +++ b/halo2-ecc/src/bls12_381/notes.md @@ -0,0 +1,4 @@ + + +## Issues: +- [From<[u64; 4]>](https://github.com/axiom-crypto/halo2-lib/blob/980b39bcca5b3327aaef6c8d73577d9381bfa899/halo2-base/src/utils/mod.rs#L35) is not implemented for bls12_381::Fq (halo2-axiom only) diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs new file mode 100644 index 00000000..65a84425 --- /dev/null +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -0,0 +1,457 @@ +#![allow(non_snake_case)] +use super::{Fp12Chip, Fp2Chip, FpChip, FpPoint, Fq, FqPoint}; +use crate::ff::PrimeField; +use crate::fields::vector::FieldVector; +use crate::halo2_proofs::halo2curves::bls12_381::{Fq12, G1Affine, G2Affine, BLS_X}; +use crate::{ + ecc::{EcPoint, EccChip}, + fields::fp12::mul_no_carry_w6, + fields::FieldChip, +}; +use halo2_base::utils::BigPrimeField; +use halo2_base::Context; + +const XI_0: i64 = 1; + +// Inputs: +// Q0 = (x_1, y_1) and Q1 = (x_2, y_2) are points in E(Fp2) +// P is point (X, Y) in E(Fp) +// Assuming Q0 != Q1 +// Output: +// line_{Psi(Q0), Psi(Q1)}(P) where Psi(x,y) = (w^2 x, w^3 y) +// - equals w^3 (y_1 - y_2) X + w^2 (x_2 - x_1) Y + w^5 (x_1 y_2 - x_2 y_1) =: out3 * w^3 + out2 * w^2 + out5 * w^5 where out2, out3, out5 are Fp2 points +// Output is [None, None, out2, out3, None, out5] as vector of `Option`s +pub fn sparse_line_function_unequal( + fp2_chip: &Fp2Chip, + ctx: &mut Context, + Q: (&EcPoint>, &EcPoint>), + P: &EcPoint>, +) -> Vec>> { + let (x_1, y_1) = (&Q.0.x, &Q.0.y); + let (x_2, y_2) = (&Q.1.x, &Q.1.y); + let (X, Y) = (&P.x, &P.y); + assert_eq!(x_1.0.len(), 2); + assert_eq!(y_1.0.len(), 2); + assert_eq!(x_2.0.len(), 2); + assert_eq!(y_2.0.len(), 2); + + let y1_minus_y2 = fp2_chip.sub_no_carry(ctx, y_1, y_2); + let x2_minus_x1 = fp2_chip.sub_no_carry(ctx, x_2, x_1); + let x1y2 = fp2_chip.mul_no_carry(ctx, x_1, y_2); + let x2y1 = fp2_chip.mul_no_carry(ctx, x_2, y_1); + + let out3 = fp2_chip.0.fp_mul_no_carry(ctx, y1_minus_y2, X); + let out4 = fp2_chip.0.fp_mul_no_carry(ctx, x2_minus_x1, Y); + let out2 = fp2_chip.sub_no_carry(ctx, &x1y2, &x2y1); + + // so far we have not "carried mod p" for any of the outputs + // we do this below + [None, Some(out2), None, Some(out3), Some(out4), None] + .into_iter() + .map(|option_nc| option_nc.map(|nocarry| fp2_chip.carry_mod(ctx, nocarry))) + .collect() +} + +// Assuming curve is of form Y^2 = X^3 + b (a = 0) to save operations +// Inputs: +// Q = (x, y) is a point in E(Fp) +// P = (P.x, P.y) in E(Fp2) +// Output: +// line_{Psi(Q), Psi(Q)}(P) where Psi(x,y) = (w^2 x, w^3 y) +// - equals (3x^3 - 2y^2)(XI_0 + u) + w^4 (-3 x^2 * Q.x) + w^3 (2 y * Q.y) =: out0 + out4 * w^4 + out3 * w^3 where out0, out3, out4 are Fp2 points +// Output is [out0, None, out2, out3, None, None] as vector of `Option`s +pub fn sparse_line_function_equal( + fp2_chip: &Fp2Chip, + ctx: &mut Context, + Q: &EcPoint>, + P: &EcPoint>, +) -> Vec>> { + let (x, y) = (&P.x, &P.y); + assert_eq!(x.0.len(), 2); + assert_eq!(y.0.len(), 2); + + let x_sq = fp2_chip.mul(ctx, x, x); + + let x_cube = fp2_chip.mul_no_carry(ctx, &x_sq, x); + let three_x_cu = fp2_chip.scalar_mul_no_carry(ctx, &x_cube, 3); + let y_sq = fp2_chip.mul_no_carry(ctx, y, y); + let two_y_sq = fp2_chip.scalar_mul_no_carry(ctx, &y_sq, 2); + let out0 = fp2_chip.sub_no_carry(ctx, &three_x_cu, &two_y_sq); + + let x_sq_Px = fp2_chip.0.fp_mul_no_carry(ctx, x_sq, &Q.x); + let out2 = fp2_chip.scalar_mul_no_carry(ctx, x_sq_Px, -3); + + let y_Py = fp2_chip.0.fp_mul_no_carry(ctx, y.clone(), &Q.y); + let out3 = fp2_chip.scalar_mul_no_carry(ctx, &y_Py, 2); + + // so far we have not "carried mod p" for any of the outputs + // we do this below + [Some(out0), None, Some(out2), Some(out3), None, None] + .into_iter() + .map(|option_nc| option_nc.map(|nocarry| fp2_chip.carry_mod(ctx, nocarry))) + .collect() +} + +// multiply Fp12 point `a` with Fp12 point `b` where `b` is len 6 vector of Fp2 points, where some are `None` to represent zero. +// Assumes `b` is not vector of all `None`s +pub fn sparse_fp12_multiply( + fp2_chip: &Fp2Chip, + ctx: &mut Context, + a: &FqPoint, + b_fp2_coeffs: &[Option>], +) -> FqPoint { + assert_eq!(a.0.len(), 12); + assert_eq!(b_fp2_coeffs.len(), 6); + let mut a_fp2_coeffs = Vec::with_capacity(6); + for i in 0..6 { + a_fp2_coeffs.push(FieldVector(vec![a[i].clone(), a[i + 6].clone()])); + } + // a * b as element of Fp2[w] without evaluating w^6 = (XI_0 + u) + let mut prod_2d = vec![None; 11]; + for i in 0..6 { + for j in 0..6 { + prod_2d[i + j] = + match (prod_2d[i + j].clone(), &a_fp2_coeffs[i], b_fp2_coeffs[j].as_ref()) { + (a, _, None) => a, + (None, a, Some(b)) => { + let ab = fp2_chip.mul_no_carry(ctx, a, b); + Some(ab) + } + (Some(a), b, Some(c)) => { + let bc = fp2_chip.mul_no_carry(ctx, b, c); + let out = fp2_chip.add_no_carry(ctx, &a, &bc); + Some(out) + } + }; + } + } + + let mut out_fp2 = Vec::with_capacity(6); + for i in 0..6 { + // prod_2d[i] + prod_2d[i+6] * w^6 + let prod_nocarry = if i != 5 { + let eval_w6 = prod_2d[i + 6] + .as_ref() + .map(|a| mul_no_carry_w6::<_, _, XI_0>(fp2_chip.fp_chip(), ctx, a.clone())); + match (prod_2d[i].as_ref(), eval_w6) { + (None, b) => b.unwrap(), // Our current use cases of 235 and 034 sparse multiplication always result in non-None value + (Some(a), None) => a.clone(), + (Some(a), Some(b)) => fp2_chip.add_no_carry(ctx, a, &b), + } + } else { + prod_2d[i].clone().unwrap() + }; + let prod = fp2_chip.carry_mod(ctx, prod_nocarry); + out_fp2.push(prod); + } + + let mut out_coeffs = Vec::with_capacity(12); + for fp2_coeff in &out_fp2 { + out_coeffs.push(fp2_coeff[0].clone()); + } + for fp2_coeff in &out_fp2 { + out_coeffs.push(fp2_coeff[1].clone()); + } + FieldVector(out_coeffs) +} + +// Input: +// - g is Fp12 point +// - P = (P0, P1) with Q0, Q1 points in E(Fp2) +// - Q is point in E(Fp) +// Output: +// - out = g * l_{Psi(Q0), Psi(Q1)}(P) as Fp12 point +pub fn fp12_multiply_with_line_unequal( + fp2_chip: &Fp2Chip, + ctx: &mut Context, + g: &FqPoint, + P: (&EcPoint>, &EcPoint>), + Q: &EcPoint>, +) -> FqPoint { + let line = sparse_line_function_unequal::(fp2_chip, ctx, P, Q); + sparse_fp12_multiply::(fp2_chip, ctx, g, &line) +} + +// Input: +// - g is Fp12 point +// - P is point in E(Fp2) +// - Q is point in E(Fp) +// Output: +// - out = g * l_{Psi(Q), Psi(Q)}(P) as Fp12 point +pub fn fp12_multiply_with_line_equal( + fp2_chip: &Fp2Chip, + ctx: &mut Context, + g: &FqPoint, + P: &EcPoint>, + Q: &EcPoint>, +) -> FqPoint { + let line = sparse_line_function_equal::(fp2_chip, ctx, Q, P); + sparse_fp12_multiply::(fp2_chip, ctx, g, &line) +} + +// Assuming curve is of form `y^2 = x^3 + b` for now (a = 0) for less operations +// Value of `b` is never used +// Inputs: +// - Q = (x, y) is a point in E(Fp2) +// - P is a point in E(Fp) +// - `pseudo_binary_encoding` is fixed vector consisting of {-1, 0, 1} entries such that `loop_count = sum pseudo_binary_encoding[i] * 2^i` +// Output: +// - f_{loop_count}(Q,P) * l_{[loop_count] Q', Frob_p(Q')}(P) * l_{[loop_count] Q' + Frob_p(Q'), -Frob_p^2(Q')}(P) +// - where we start with `f_1(Q,P) = 1` and use Miller's algorithm f_{i+j} = f_i * f_j * l_{i,j}(Q,P) +// - Q' = Psi(Q) in E(Fp12) +// - Frob_p(x,y) = (x^p, y^p) +// - Above formula is specific to BN curves +// Assume: +// - Q != O and the order of Q in E(Fp2) is r +// - r is prime, so [i]Q != [j]Q for i != j in Z/r +// - `0 <= loop_count < r` and `loop_count < p` (to avoid [loop_count]Q' = Frob_p(Q')) +// - x^3 + b = 0 has no solution in Fp2, i.e., the y-coordinate of Q cannot be 0. +pub fn miller_loop( + ecc_chip: &EccChip>, + ctx: &mut Context, + Q: &EcPoint>, + P: &EcPoint>, + pseudo_binary_encoding: &[i8], +) -> FqPoint { + todo!() +} + +// let pairs = [(a_i, b_i)], a_i in G_1, b_i in G_2 +// output is Prod_i e'(a_i, b_i), where e'(a_i, b_i) is the output of `miller_loop_BN(b_i, a_i)` +pub fn multi_miller_loop( + ecc_chip: &EccChip>, + ctx: &mut Context, + pairs: Vec<(&EcPoint>, &EcPoint>)>, +) -> FqPoint { + let fp_chip = ecc_chip.field_chip.fp_chip(); + let fp12_chip = Fp12Chip::::new(fp_chip); + + // initialize the first line function into Fq12 point with first (Q,P) pair + // this is to skip first iteration by leveraging the fact that f = 1 + let mut f = { + let sparse_f = + sparse_line_function_equal::(ecc_chip.field_chip(), ctx, pairs[0].0, pairs[0].1); + assert_eq!(sparse_f.len(), 6); + + let zero_fp = fp_chip.load_constant(ctx, Fq::zero()); + let mut f_coeffs = Vec::with_capacity(12); + for coeff in &sparse_f { + if let Some(fp2_point) = coeff { + f_coeffs.push(fp2_point[0].clone()); + } else { + f_coeffs.push(zero_fp.clone()); + } + } + for coeff in &sparse_f { + if let Some(fp2_point) = coeff { + f_coeffs.push(fp2_point[1].clone()); + } else { + f_coeffs.push(zero_fp.clone()); + } + } + FieldVector(f_coeffs) + }; + + // process second (Q,P) pair + for &(q, p) in pairs.iter().skip(1) { + f = fp12_multiply_with_line_equal::(ecc_chip.field_chip(), ctx, &f, p, q); + } + + let fp12_chip = Fp12Chip::::new(fp_chip); + + let mut r = pairs.iter().map(|pair| pair.1.clone()).collect::>(); + let mut found_one = true; + let mut prev_bit = true; + + // double P as in the first part of Miller loop + for r in r.iter_mut() { + *r = ecc_chip.double(ctx, r.clone()); + } + + // skip two bits after init (first beacuse f = 1, second because 1-ft found_one = false) + // restrucuture loop to perfrom additiona step for the previous iteration first and then doubling step + for (i, bit) in (0..62).rev().map(|i| (i as usize, ((BLS_X >> i) & 1) == 1)) { + if prev_bit { + for (r, &(q, p)) in r.iter_mut().zip(pairs.iter()) { + f = fp12_multiply_with_line_unequal::(ecc_chip.field_chip(), ctx, &f, (r, p), q); + *r = ecc_chip.add_unequal(ctx, r.clone(), p.clone(), false); + } + } + + prev_bit = bit; + + if !found_one { + found_one = bit; + continue; + } + + f = fp12_chip.mul(ctx, &f, &f); + + for (r, &(q, p)) in r.iter_mut().zip(pairs.iter()) { + f = fp12_multiply_with_line_equal::(ecc_chip.field_chip(), ctx, &f, r, q); + *r = ecc_chip.double(ctx, r.clone()); + } + } + + f +} + +fn permute_vector(v1: &Vec, indexes: &[usize]) -> Vec { + indexes.iter().map(|i| v1[*i].clone()).collect() +} + +// Frobenius coefficient coeff[1][j] = ((9+u)^{(p-1)/6})^j +// Frob_p( twist(Q) ) = ( (w^2 x)^p, (w^3 y)^p ) = twist( coeff[1][2] * x^p, coeff[1][3] * y^p ) +// Input: +// - Q = (x, y) point in E(Fp2) +// - coeff[1][2], coeff[1][3] as assigned cells: this is an optimization to avoid loading new constants +// Output: +// - (coeff[1][2] * x^p, coeff[1][3] * y^p) point in E(Fp2) +pub fn twisted_frobenius( + ecc_chip: &EccChip>, + ctx: &mut Context, + Q: impl Into>>, + c2: impl Into>, + c3: impl Into>, +) -> EcPoint> { + let Q = Q.into(); + let c2 = c2.into(); + let c3 = c3.into(); + assert_eq!(c2.0.len(), 2); + assert_eq!(c3.0.len(), 2); + + let frob_x = ecc_chip.field_chip.conjugate(ctx, Q.x); + let frob_y = ecc_chip.field_chip.conjugate(ctx, Q.y); + let out_x = ecc_chip.field_chip.mul(ctx, c2, frob_x); + let out_y = ecc_chip.field_chip.mul(ctx, c3, frob_y); + EcPoint::new(out_x, out_y) +} + +// Frobenius coefficient coeff[1][j] = ((9+u)^{(p-1)/6})^j +// -Frob_p( twist(Q) ) = ( (w^2 x)^p, -(w^3 y)^p ) = twist( coeff[1][2] * x^p, coeff[1][3] * -y^p ) +// Input: +// - Q = (x, y) point in E(Fp2) +// Output: +// - (coeff[1][2] * x^p, coeff[1][3] * -y^p) point in E(Fp2) +pub fn neg_twisted_frobenius( + ecc_chip: &EccChip>, + ctx: &mut Context, + Q: impl Into>>, + c2: impl Into>, + c3: impl Into>, +) -> EcPoint> { + let Q = Q.into(); + let c2 = c2.into(); + let c3 = c3.into(); + assert_eq!(c2.0.len(), 2); + assert_eq!(c3.0.len(), 2); + + let frob_x = ecc_chip.field_chip.conjugate(ctx, Q.x); + let neg_frob_y = ecc_chip.field_chip.neg_conjugate(ctx, Q.y); + let out_x = ecc_chip.field_chip.mul(ctx, c2, frob_x); + let out_y = ecc_chip.field_chip.mul(ctx, c3, neg_frob_y); + EcPoint::new(out_x, out_y) +} + +// To avoid issues with mutably borrowing twice (not allowed in Rust), we only store fp_chip and construct g2_chip and fp12_chip in scope when needed for temporary mutable borrows +pub struct PairingChip<'chip, F: BigPrimeField> { + pub fp_chip: &'chip FpChip<'chip, F>, +} + +impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { + pub fn new(fp_chip: &'chip FpChip) -> Self { + Self { fp_chip } + } + + pub fn load_private_g1_unchecked( + &self, + ctx: &mut Context, + point: G1Affine, + ) -> EcPoint> { + let g1_chip = EccChip::new(self.fp_chip); + g1_chip.load_private_unchecked(ctx, (point.x, point.y)) + } + + pub fn load_private_g2_unchecked( + &self, + ctx: &mut Context, + point: G2Affine, + ) -> EcPoint> { + let fp2_chip = Fp2Chip::new(self.fp_chip); + let g2_chip = EccChip::new(&fp2_chip); + g2_chip.load_private_unchecked(ctx, (point.x, point.y)) + } + + pub fn miller_loop( + &self, + ctx: &mut Context, + Q: &EcPoint>, + P: &EcPoint>, + ) -> FqPoint { + let fp2_chip = Fp2Chip::::new(self.fp_chip); + let g2_chip = EccChip::new(&fp2_chip); + // miller_loop_BN::( + // &g2_chip, + // ctx, + // Q, + // P, + // &SIX_U_PLUS_2_NAF, // pseudo binary encoding for BN254 + // ) + unimplemented!() + } + + pub fn multi_miller_loop( + &self, + ctx: &mut Context, + pairs: Vec<(&EcPoint>, &EcPoint>)>, + ) -> FqPoint { + let fp2_chip = Fp2Chip::::new(self.fp_chip); + let g2_chip = EccChip::new(&fp2_chip); + let f = multi_miller_loop::(&g2_chip, ctx, pairs); + let fp12_chip = Fp12Chip::::new(self.fp_chip); + + f + } + + pub fn final_exp(&self, ctx: &mut Context, f: FqPoint) -> FqPoint { + let fp12_chip = Fp12Chip::::new(self.fp_chip); + fp12_chip.final_exp(ctx, f) + } + + // optimal Ate pairing + pub fn pairing( + &self, + ctx: &mut Context, + Q: &EcPoint>, + P: &EcPoint>, + ) -> FqPoint { + let f0 = self.miller_loop(ctx, Q, P); + let fp12_chip = Fp12Chip::::new(self.fp_chip); + // final_exp implemented in final_exp module + fp12_chip.final_exp(ctx, f0) + } + + /* + * Conducts an efficient pairing check e(P, Q) = e(S, T) using only one + * final exponentiation. In particular, this constraints + * (e'(-P, Q)e'(S, T))^x = 1, where e' is the optimal ate pairing without + * the final exponentiation. Reduces number of necessary advice cells by + * ~30%. + */ + pub fn pairing_check( + &self, + ctx: &mut Context, + Q: &EcPoint>, + P: &EcPoint>, + T: &EcPoint>, + S: &EcPoint>, + ) { + let ecc_chip_fp = EccChip::new(self.fp_chip); + let negated_P = ecc_chip_fp.negate(ctx, P); + let mml = self.multi_miller_loop(ctx, vec![(&negated_P, Q), (S, T)]); + let fp12_chip = Fp12Chip::::new(self.fp_chip); + let fe = fp12_chip.final_exp(ctx, mml); + let fp12_one = fp12_chip.load_constant(ctx, Fq12::one()); + fp12_chip.assert_equal(ctx, fe, fp12_one); + } +} From c23d2645b2f0c97b27eb73ac926da2215c359b6a Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Sat, 30 Sep 2023 21:21:29 +0200 Subject: [PATCH 02/22] make compile --- Cargo.toml | 9 ++++ halo2-base/src/utils/mod.rs | 62 +++++++++++++++++++++++----- halo2-ecc/src/bls12_381/final_exp.rs | 16 ++++--- halo2-ecc/src/bls12_381/mod.rs | 6 +-- halo2-ecc/src/bls12_381/pairing.rs | 42 ++----------------- halo2-ecc/src/fields/fp12.rs | 31 ++++++++++++++ halo2-ecc/src/fields/fp2.rs | 14 +++++++ halo2-ecc/src/lib.rs | 1 + 8 files changed, 121 insertions(+), 60 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index b2d3ab72..09c03f33 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -39,3 +39,12 @@ debug = true [patch."https://github.com/axiom-crypto/halo2-lib.git"] halo2-base = { path = "../halo2-lib/halo2-base" } halo2-ecc = { path = "../halo2-lib/halo2-ecc" } + +[patch."https://github.com/privacy-scaling-explorations/halo2curves"] +# halo2curves = { git = "https://github.com/timoftime/halo2curves", rev = "b682183" } +halo2curves = { path = "../halo2curves" } + + +[patch."https://github.com/axiom-crypto/halo2curves"] +# halo2curves = { git = "https://github.com/timoftime/halo2curves", rev = "b682183" } +halo2curves = { path = "../halo2curves" } diff --git a/halo2-base/src/utils/mod.rs b/halo2-base/src/utils/mod.rs index 2aaa5166..6af4c935 100644 --- a/halo2-base/src/utils/mod.rs +++ b/halo2-base/src/utils/mod.rs @@ -30,19 +30,61 @@ pub trait BigPrimeField: ScalarField { fn from_u64_digits(val: &[u64]) -> Self; } #[cfg(feature = "halo2-axiom")] -impl 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 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) + } + } +} + +// mod bls12_381 { +// use super::BigPrimeField; + +// impl BigPrimeField for crate::halo2_proofs::halo2curves::bls12_381::Fq { +// fn from_u64_digits(val: &[u64]) -> Self { +// todo!() +// } +// } +// } + /// Helper trait to represent a field element that can be converted into [u64] limbs. /// /// Note: Since the number of bits necessary to represent a field element is larger than the number of bits in a u64, we decompose the integer representation of the field element into multiple [u64] values e.g. `limbs`. diff --git a/halo2-ecc/src/bls12_381/final_exp.rs b/halo2-ecc/src/bls12_381/final_exp.rs index 575ecab7..b27d0439 100644 --- a/halo2-ecc/src/bls12_381/final_exp.rs +++ b/halo2-ecc/src/bls12_381/final_exp.rs @@ -1,18 +1,16 @@ -use super::pairing::fq2_mul_by_nonresidue; use super::{Fp12Chip, Fp2Chip, FpChip, FqPoint}; -use crate::halo2_proofs::arithmetic::Field; +use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2, BLS_X, FROBENIUS_COEFF_FQ12_C1}; use crate::{ ecc::get_naf, - fields::{fp12::mul_no_carry_w6, vector::FieldVector, FieldChip, PrimeField}, + fields::{fp12::mul_no_carry_w6, vector::FieldVector, FieldChip}, }; +use halo2_base::utils::BigPrimeField; use halo2_base::{gates::GateInstructions, utils::modulus, Context, QuantumCell::Constant}; -use halo2curves::bls12_381::{Fq, Fq12, Fq2, BLS_X, FROBENIUS_COEFF_FQ12_C1}; -use itertools::Itertools; use num_bigint::BigUint; const XI_0: i64 = 1; -impl<'chip, F: PrimeField> Fp12Chip<'chip, F> { +impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { // computes a ** (p ** power) // only works for p = 3 (mod 4) and p = 1 (mod 6) pub fn frobenius_map( @@ -30,7 +28,7 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> { let fp_chip = self.fp_chip(); let fp2_chip = Fp2Chip::::new(fp_chip); for i in 0..6 { - let frob_coeff = FROBENIUS_COEFF_FQ12_C1[pow].pow_vartime([i as u64]); + let frob_coeff = FROBENIUS_COEFF_FQ12_C1[pow].pow_vartime(&[i as u64]); // possible optimization (not implemented): load `frob_coeff` as we multiply instead of loading first // frobenius map is used infrequently so this is a small optimization @@ -172,8 +170,8 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> { // compute `g0 + 1` g0[0].truncation.limbs[0] = - fp2_chip.gate().add(ctx, g0[0].truncation.limbs[0], Constant(F::one())); - g0[0].native = fp2_chip.gate().add(ctx, g0[0].native, Constant(F::one())); + fp2_chip.gate().add(ctx, g0[0].truncation.limbs[0], Constant(F::ONE)); + g0[0].native = fp2_chip.gate().add(ctx, g0[0].native, Constant(F::ONE)); g0[0].truncation.max_limb_bits += 1; g0[0].value += 1usize; diff --git a/halo2-ecc/src/bls12_381/mod.rs b/halo2-ecc/src/bls12_381/mod.rs index f2493b74..c4c22d5c 100644 --- a/halo2-ecc/src/bls12_381/mod.rs +++ b/halo2-ecc/src/bls12_381/mod.rs @@ -3,7 +3,7 @@ use crate::fields::vector::FieldVector; use crate::fields::{fp, fp12, fp2}; use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2}; -// pub mod final_exp; +pub mod final_exp; pub mod pairing; pub type FpChip<'range, F> = fp::FpChip<'range, F, Fq>; @@ -12,5 +12,5 @@ pub type FqPoint = FieldVector>; pub type Fp2Chip<'chip, F> = fp2::Fp2Chip<'chip, F, FpChip<'chip, F>, Fq2>; pub type Fp12Chip<'chip, F> = fp12::Fp12Chip<'chip, F, FpChip<'chip, F>, Fq12, 1>; -// #[cfg(test)] -// pub(crate) mod tests; +#[cfg(test)] +pub(crate) mod tests; diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs index 65a84425..5ed1f603 100644 --- a/halo2-ecc/src/bls12_381/pairing.rs +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -1,6 +1,5 @@ #![allow(non_snake_case)] use super::{Fp12Chip, Fp2Chip, FpChip, FpPoint, Fq, FqPoint}; -use crate::ff::PrimeField; use crate::fields::vector::FieldVector; use crate::halo2_proofs::halo2curves::bls12_381::{Fq12, G1Affine, G2Affine, BLS_X}; use crate::{ @@ -189,29 +188,11 @@ pub fn fp12_multiply_with_line_equal( sparse_fp12_multiply::(fp2_chip, ctx, g, &line) } -// Assuming curve is of form `y^2 = x^3 + b` for now (a = 0) for less operations -// Value of `b` is never used -// Inputs: -// - Q = (x, y) is a point in E(Fp2) -// - P is a point in E(Fp) -// - `pseudo_binary_encoding` is fixed vector consisting of {-1, 0, 1} entries such that `loop_count = sum pseudo_binary_encoding[i] * 2^i` -// Output: -// - f_{loop_count}(Q,P) * l_{[loop_count] Q', Frob_p(Q')}(P) * l_{[loop_count] Q' + Frob_p(Q'), -Frob_p^2(Q')}(P) -// - where we start with `f_1(Q,P) = 1` and use Miller's algorithm f_{i+j} = f_i * f_j * l_{i,j}(Q,P) -// - Q' = Psi(Q) in E(Fp12) -// - Frob_p(x,y) = (x^p, y^p) -// - Above formula is specific to BN curves -// Assume: -// - Q != O and the order of Q in E(Fp2) is r -// - r is prime, so [i]Q != [j]Q for i != j in Z/r -// - `0 <= loop_count < r` and `loop_count < p` (to avoid [loop_count]Q' = Frob_p(Q')) -// - x^3 + b = 0 has no solution in Fp2, i.e., the y-coordinate of Q cannot be 0. pub fn miller_loop( ecc_chip: &EccChip>, ctx: &mut Context, Q: &EcPoint>, P: &EcPoint>, - pseudo_binary_encoding: &[i8], ) -> FqPoint { todo!() } @@ -224,7 +205,6 @@ pub fn multi_miller_loop( pairs: Vec<(&EcPoint>, &EcPoint>)>, ) -> FqPoint { let fp_chip = ecc_chip.field_chip.fp_chip(); - let fp12_chip = Fp12Chip::::new(fp_chip); // initialize the first line function into Fq12 point with first (Q,P) pair // this is to skip first iteration by leveraging the fact that f = 1 @@ -270,7 +250,7 @@ pub fn multi_miller_loop( // skip two bits after init (first beacuse f = 1, second because 1-ft found_one = false) // restrucuture loop to perfrom additiona step for the previous iteration first and then doubling step - for (i, bit) in (0..62).rev().map(|i| (i as usize, ((BLS_X >> i) & 1) == 1)) { + for bit in (0..62).rev().map(|i| ((BLS_X >> i) & 1) == 1) { if prev_bit { for (r, &(q, p)) in r.iter_mut().zip(pairs.iter()) { f = fp12_multiply_with_line_unequal::(ecc_chip.field_chip(), ctx, &f, (r, p), q); @@ -287,7 +267,7 @@ pub fn multi_miller_loop( f = fp12_chip.mul(ctx, &f, &f); - for (r, &(q, p)) in r.iter_mut().zip(pairs.iter()) { + for (r, &(q, _p)) in r.iter_mut().zip(pairs.iter()) { f = fp12_multiply_with_line_equal::(ecc_chip.field_chip(), ctx, &f, r, q); *r = ecc_chip.double(ctx, r.clone()); } @@ -296,10 +276,6 @@ pub fn multi_miller_loop( f } -fn permute_vector(v1: &Vec, indexes: &[usize]) -> Vec { - indexes.iter().map(|i| v1[*i].clone()).collect() -} - // Frobenius coefficient coeff[1][j] = ((9+u)^{(p-1)/6})^j // Frob_p( twist(Q) ) = ( (w^2 x)^p, (w^3 y)^p ) = twist( coeff[1][2] * x^p, coeff[1][3] * y^p ) // Input: @@ -390,14 +366,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { ) -> FqPoint { let fp2_chip = Fp2Chip::::new(self.fp_chip); let g2_chip = EccChip::new(&fp2_chip); - // miller_loop_BN::( - // &g2_chip, - // ctx, - // Q, - // P, - // &SIX_U_PLUS_2_NAF, // pseudo binary encoding for BN254 - // ) - unimplemented!() + miller_loop::(&g2_chip, ctx, Q, P) } pub fn multi_miller_loop( @@ -407,10 +376,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { ) -> FqPoint { let fp2_chip = Fp2Chip::::new(self.fp_chip); let g2_chip = EccChip::new(&fp2_chip); - let f = multi_miller_loop::(&g2_chip, ctx, pairs); - let fp12_chip = Fp12Chip::::new(self.fp_chip); - - f + multi_miller_loop::(&g2_chip, ctx, pairs) } pub fn final_exp(&self, ctx: &mut Context, f: FqPoint) -> FqPoint { diff --git a/halo2-ecc/src/fields/fp12.rs b/halo2-ecc/src/fields/fp12.rs index bdb9f790..64b6a200 100644 --- a/halo2-ecc/src/fields/fp12.rs +++ b/halo2-ecc/src/fields/fp12.rs @@ -249,3 +249,34 @@ mod bn254 { } } } + +mod bls12_381 { + use crate::fields::FieldExtConstructor; + use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2, Fq6}; + // This means we store an Fp12 point as `\sum_{i = 0}^6 (a_{i0} + a_{i1} * u) * w^i` + // This is encoded in an FqPoint of degree 12 as `(a_{00}, ..., a_{50}, a_{01}, ..., a_{51})` + impl FieldExtConstructor for Fq12 { + fn new(c: [Fq; 12]) -> Self { + Fq12 { + c0: Fq6 { + c0: Fq2 { c0: c[0], c1: c[6] }, + c1: Fq2 { c0: c[2], c1: c[8] }, + c2: Fq2 { c0: c[4], c1: c[10] }, + }, + c1: Fq6 { + c0: Fq2 { c0: c[1], c1: c[7] }, + c1: Fq2 { c0: c[3], c1: c[9] }, + c2: Fq2 { c0: c[5], c1: c[11] }, + }, + } + } + + fn coeffs(&self) -> Vec { + let x = self; + vec![ + x.c0.c0.c0, x.c1.c0.c0, x.c0.c1.c0, x.c1.c1.c0, x.c0.c2.c0, x.c1.c2.c0, x.c0.c0.c1, + x.c1.c0.c1, x.c0.c1.c1, x.c1.c1.c1, x.c0.c2.c1, x.c1.c2.c1, + ] + } + } +} diff --git a/halo2-ecc/src/fields/fp2.rs b/halo2-ecc/src/fields/fp2.rs index 71c5d446..8068e2f5 100644 --- a/halo2-ecc/src/fields/fp2.rs +++ b/halo2-ecc/src/fields/fp2.rs @@ -130,3 +130,17 @@ mod bn254 { } } } + +mod bls12_381 { + use crate::fields::FieldExtConstructor; + use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq2}; + impl FieldExtConstructor for Fq2 { + fn new(c: [Fq; 2]) -> Self { + Fq2 { c0: c[0], c1: c[1] } + } + + fn coeffs(&self) -> Vec { + vec![self.c0, self.c1] + } + } +} diff --git a/halo2-ecc/src/lib.rs b/halo2-ecc/src/lib.rs index 5b3f191a..d87ce7fc 100644 --- a/halo2-ecc/src/lib.rs +++ b/halo2-ecc/src/lib.rs @@ -8,6 +8,7 @@ pub mod ecc; pub mod fields; pub mod bn254; +pub mod bls12_381; pub mod grumpkin; pub mod secp256k1; From 14077b45455b670dab072962acf46fef669550b7 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Sat, 30 Sep 2023 22:04:29 +0200 Subject: [PATCH 03/22] add tests; they fail :( --- halo2-base/src/utils/mod.rs | 32 +++- .../configs/bls12_381/pairing_circuit.config | 1 + halo2-ecc/src/bigint/carry_mod.rs | 12 +- .../src/bigint/check_carry_mod_to_zero.rs | 14 +- halo2-ecc/src/bls12_381/tests/mod.rs | 21 +++ halo2-ecc/src/bls12_381/tests/pairing.rs | 173 ++++++++++++++++++ 6 files changed, 235 insertions(+), 18 deletions(-) create mode 100644 halo2-ecc/configs/bls12_381/pairing_circuit.config create mode 100644 halo2-ecc/src/bls12_381/tests/mod.rs create mode 100644 halo2-ecc/src/bls12_381/tests/pairing.rs diff --git a/halo2-base/src/utils/mod.rs b/halo2-base/src/utils/mod.rs index 6af4c935..f0396980 100644 --- a/halo2-base/src/utils/mod.rs +++ b/halo2-base/src/utils/mod.rs @@ -52,6 +52,29 @@ mod bn256 { } } +#[cfg(feature = "halo2-axiom")] +mod secp256k1 { + use crate::halo2_proofs::halo2curves::secp256k1::{Fq, Fp}; + + 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}; @@ -75,15 +98,6 @@ mod bls12_381 { } } -// mod bls12_381 { -// use super::BigPrimeField; - -// impl BigPrimeField for crate::halo2_proofs::halo2curves::bls12_381::Fq { -// fn from_u64_digits(val: &[u64]) -> Self { -// todo!() -// } -// } -// } /// Helper trait to represent a field element that can be converted into [u64] limbs. /// diff --git a/halo2-ecc/configs/bls12_381/pairing_circuit.config b/halo2-ecc/configs/bls12_381/pairing_circuit.config new file mode 100644 index 00000000..070e8642 --- /dev/null +++ b/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":120,"num_limbs":4} diff --git a/halo2-ecc/src/bigint/carry_mod.rs b/halo2-ecc/src/bigint/carry_mod.rs index a9667d79..c12a0fde 100644 --- a/halo2-ecc/src/bigint/carry_mod.rs +++ b/halo2-ecc/src/bigint/carry_mod.rs @@ -44,7 +44,8 @@ pub fn crt( let k = a.truncation.limbs.len(); let trunc_len = n * k; - debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); + // FIXME: hotfix for BLS12 support + // debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); // in order for CRT method to work, we need `abs(out + modulus * quotient - a) < 2^{trunc_len - 1} * native_modulus::` // this is ensured if `0 <= out < 2^{n*k}` and @@ -56,7 +57,8 @@ pub fn crt( // 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); + // FIXME: hotfix for BLS12 support + let quot_last_limb_bits = 0; //quot_max_bits - n * (k - 1); 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) @@ -69,7 +71,8 @@ pub fn crt( let (quot_val, out_val) = a.value.div_mod_floor(modulus); debug_assert!(out_val < (BigInt::one() << (n * k))); - debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); + // FIXME: hotfix for BLS12 support + // debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); // decompose_bigint just throws away signed limbs in index >= k let out_vec = decompose_bigint::(&out_val, k, n); @@ -144,7 +147,8 @@ pub fn crt( // 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 }; + // FIXME: hotfix for BLS12 support + let limb_bits = if q_index == k - 1 { /* quot_last_limb_bits */ n } else { n }; let limb_base = if q_index == k - 1 { range.gate().pow_of_two()[limb_bits] } else { limb_bases[1] }; diff --git a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs index 13523ba5..7a2e634d 100644 --- a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs +++ b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs @@ -29,12 +29,14 @@ pub fn crt( let k = a.truncation.limbs.len(); let trunc_len = n * k; - debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); + // FIXME: hotfix for BLS12 support + // debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); // 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); + // FIXME: hotfix for BLS12 support + let quot_last_limb_bits = 0; // quot_max_bits - n * (k - 1); // these are witness vectors: // we need to find `quot_vec` as a proper BigInt with k limbs @@ -44,8 +46,9 @@ pub fn crt( let (quot_val, _out_val) = a.value.div_mod_floor(modulus); // only perform safety checks in debug mode - debug_assert_eq!(_out_val, BigInt::zero()); - debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); + // FIXME: hotfix for BLS12 support + // debug_assert_eq!(_out_val, BigInt::zero()); + // debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); let quot_vec = decompose_bigint::("_val, k, n); @@ -90,7 +93,8 @@ pub fn crt( // 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 }; + // FIXME: hotfix for BLS12 support + let limb_bits = if q_index == k - 1 { n /* quot_last_limb_bits */ } else { n }; let limb_base = if q_index == k - 1 { range.gate().pow_of_two()[limb_bits] } else { limb_bases[1] }; diff --git a/halo2-ecc/src/bls12_381/tests/mod.rs b/halo2-ecc/src/bls12_381/tests/mod.rs new file mode 100644 index 00000000..71ec5cdd --- /dev/null +++ b/halo2-ecc/src/bls12_381/tests/mod.rs @@ -0,0 +1,21 @@ +#![allow(non_snake_case)] +use super::pairing::PairingChip; +use super::*; +use crate::ecc::EccChip; +use crate::group::Curve; +use crate::{ + fields::FpStrategy, + halo2_proofs::halo2curves::bls12_381::{pairing, Fr, G1Affine}, +}; +use halo2_base::utils::fe_to_biguint; +use halo2_base::{ + gates::{flex_gate::threads::SinglePhaseCoreManager, RangeChip}, + halo2_proofs::halo2curves::bls12_381::G1, + utils::testing::base_test, +}; +use rand::rngs::StdRng; +use rand_core::SeedableRng; +use serde::{Deserialize, Serialize}; +use std::io::Write; + +pub mod pairing; diff --git a/halo2-ecc/src/bls12_381/tests/pairing.rs b/halo2-ecc/src/bls12_381/tests/pairing.rs new file mode 100644 index 00000000..fc9f2082 --- /dev/null +++ b/halo2-ecc/src/bls12_381/tests/pairing.rs @@ -0,0 +1,173 @@ +use std::{ + fs::{self, File}, + io::{BufRead, BufReader}, +}; + +use crate::fields::FieldChip; + +use super::*; +use halo2_base::{ + gates::RangeChip, halo2_proofs::{arithmetic::Field, halo2curves::bls12_381::G2Affine}, utils::BigPrimeField, Context, +}; +use serde::{Deserialize, Serialize}; + +#[derive(Clone, Copy, Debug, Serialize, Deserialize)] +struct PairingCircuitParams { + strategy: FpStrategy, + degree: u32, + num_advice: usize, + num_lookup_advice: usize, + num_fixed: usize, + lookup_bits: usize, + limb_bits: usize, + num_limbs: usize, +} + +fn pairing_test( + ctx: &mut Context, + range: &RangeChip, + params: PairingCircuitParams, + P: G1Affine, + Q: G2Affine, +) { + let fp_chip = FpChip::::new(range, params.limb_bits, params.num_limbs); + let chip = PairingChip::new(&fp_chip); + let P_assigned = chip.load_private_g1_unchecked(ctx, P); + let Q_assigned = chip.load_private_g2_unchecked(ctx, Q); + // test optimal ate pairing + let f = chip.pairing(ctx, &Q_assigned, &P_assigned); + let actual_f = pairing(&P, &Q); + let fp12_chip = Fp12Chip::new(&fp_chip); + // cannot directly compare f and actual_f because `Gt` has private field `Fq12` + assert_eq!( + format!("Gt({:?})", fp12_chip.get_assigned_value(&f.into())), + format!("{actual_f:?}") + ); +} + +#[test] +fn test_pairing() { + let path = "configs/bls12_381/pairing_circuit.config"; + let params: PairingCircuitParams = serde_json::from_reader( + File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), + ) + .unwrap(); + let mut rng = StdRng::seed_from_u64(0); + let P = G1Affine::random(&mut rng); + let Q = G2Affine::random(&mut rng); + base_test().k(params.degree).lookup_bits(params.lookup_bits).run(|ctx, range| { + pairing_test(ctx, range, params, P, Q); + }); +} + +fn pairing_check_test( + ctx: &mut Context, + range: &RangeChip, + params: PairingCircuitParams, + P: G1Affine, + Q: G2Affine, + S: G1Affine, +) { + let fp_chip = FpChip::::new(range, params.limb_bits, params.num_limbs); + let chip = PairingChip::new(&fp_chip); + let P_assigned = chip.load_private_g1_unchecked(ctx, P); + let Q_assigned = chip.load_private_g2_unchecked(ctx, Q); + let S_assigned = chip.load_private_g1_unchecked(ctx, S); + let T_assigned = chip.load_private_g2_unchecked(ctx, G2Affine::generator()); + chip.pairing_check(ctx, &Q_assigned, &P_assigned, &T_assigned, &S_assigned); +} + +/* + * Samples a random α,β in Fr and does the pairing check + * e(H_1^α, H_2^β) = e(H_1^(α*β), H_2), where H_1 is the generator for G1 and + * H_2 for G2. + */ +#[test] +fn test_pairing_check() { + let path = "configs/bls12_381/pairing_circuit.config"; + let params: PairingCircuitParams = serde_json::from_reader( + File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), + ) + .unwrap(); + let mut rng = StdRng::seed_from_u64(0); + let alpha = Fr::random(&mut rng); + let beta = Fr::random(&mut rng); + let P = G1Affine::from(G1Affine::generator() * alpha); + let Q = G2Affine::from(G2Affine::generator() * beta); + let S = G1Affine::from(G1Affine::generator() * alpha * beta); + base_test().k(params.degree).lookup_bits(params.lookup_bits).run(|ctx, range| { + pairing_check_test(ctx, range, params, P, Q, S); + }) +} + +/* + * Samples a random α,β in Fr and does an incorrect pairing check + * e(H_1^α, H_2^β) = e(H_1^α, H_2), where H_1 is the generator for G1 and + * H_2 for G2. + */ +#[test] +fn test_pairing_check_fail() { + let path = "configs/bls12_381/pairing_circuit.config"; + let params: PairingCircuitParams = serde_json::from_reader( + File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), + ) + .unwrap(); + let mut rng = StdRng::seed_from_u64(0); + let alpha = Fr::random(&mut rng); + let beta = Fr::random(&mut rng); + let P = G1Affine::from(G1Affine::generator() * alpha); + let Q = G2Affine::from(G2Affine::generator() * beta); + base_test().k(params.degree).lookup_bits(params.lookup_bits).expect_satisfied(false).run( + |ctx, range| { + pairing_check_test(ctx, range, params, P, Q, P); + }, + ) +} + +#[test] +fn bench_pairing() -> Result<(), Box> { + let config_path = "configs/bls12_381/bench_pairing.config"; + let bench_params_file = + File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); + fs::create_dir_all("results/bls12_381").unwrap(); + fs::create_dir_all("data").unwrap(); + + let results_path = "results/bls12_381/pairing_bench.csv"; + let mut fs_results = File::create(results_path).unwrap(); + writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,proof_time,proof_size,verify_time")?; + + let mut rng = StdRng::seed_from_u64(0); + let bench_params_reader = BufReader::new(bench_params_file); + for line in bench_params_reader.lines() { + let bench_params: PairingCircuitParams = + serde_json::from_str(line.unwrap().as_str()).unwrap(); + let k = bench_params.degree; + println!("---------------------- degree = {k} ------------------------------",); + + let P = G1Affine::random(&mut rng); + let Q = G2Affine::random(&mut rng); + let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( + (P, Q), + (P, Q), + |pool, range, (P, Q)| { + pairing_test(pool.main(), range, bench_params, P, Q); + }, + ); + + writeln!( + fs_results, + "{},{},{},{},{},{},{},{:?},{},{:?}", + bench_params.degree, + bench_params.num_advice, + bench_params.num_lookup_advice, + bench_params.num_fixed, + bench_params.lookup_bits, + bench_params.limb_bits, + bench_params.num_limbs, + stats.proof_time.time.elapsed(), + stats.proof_size, + stats.verify_time.time.elapsed() + )?; + } + Ok(()) +} From 29f3e82407a3021d9e57ea2539b3159e105114c0 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Sun, 1 Oct 2023 17:23:20 +0200 Subject: [PATCH 04/22] tests WIP --- halo2-base/src/utils/mod.rs | 19 ++- .../configs/bls12_381/bench_ec_add.config | 5 + .../configs/bls12_381/bench_pairing.config | 9 ++ .../configs/bls12_381/ec_add_circuit.config | 1 + halo2-ecc/results/bls12_381/pairing_bench.csv | 1 + halo2-ecc/src/bls12_381/notes.md | 4 - halo2-ecc/src/bls12_381/tests/ec_add.rs | 110 ++++++++++++++++ halo2-ecc/src/bls12_381/tests/mod.rs | 11 +- halo2-ecc/src/bls12_381/tests/pairing.rs | 122 +++++++++--------- 9 files changed, 200 insertions(+), 82 deletions(-) create mode 100644 halo2-ecc/configs/bls12_381/bench_ec_add.config create mode 100644 halo2-ecc/configs/bls12_381/bench_pairing.config create mode 100644 halo2-ecc/configs/bls12_381/ec_add_circuit.config create mode 100644 halo2-ecc/results/bls12_381/pairing_bench.csv delete mode 100644 halo2-ecc/src/bls12_381/notes.md create mode 100644 halo2-ecc/src/bls12_381/tests/ec_add.rs diff --git a/halo2-base/src/utils/mod.rs b/halo2-base/src/utils/mod.rs index f0396980..fb1d7235 100644 --- a/halo2-base/src/utils/mod.rs +++ b/halo2-base/src/utils/mod.rs @@ -54,7 +54,7 @@ mod bn256 { #[cfg(feature = "halo2-axiom")] mod secp256k1 { - use crate::halo2_proofs::halo2curves::secp256k1::{Fq, Fp}; + use crate::halo2_proofs::halo2curves::secp256k1::{Fp, Fq}; impl super::BigPrimeField for Fp { #[inline(always)] @@ -79,14 +79,14 @@ mod secp256k1 { 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 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)] @@ -98,7 +98,6 @@ mod bls12_381 { } } - /// Helper trait to represent a field element that can be converted into [u64] limbs. /// /// Note: Since the number of bits necessary to represent a field element is larger than the number of bits in a u64, we decompose the integer representation of the field element into multiple [u64] values e.g. `limbs`. diff --git a/halo2-ecc/configs/bls12_381/bench_ec_add.config b/halo2-ecc/configs/bls12_381/bench_ec_add.config new file mode 100644 index 00000000..eccbbd46 --- /dev/null +++ b/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} diff --git a/halo2-ecc/configs/bls12_381/bench_pairing.config b/halo2-ecc/configs/bls12_381/bench_pairing.config new file mode 100644 index 00000000..510a0c28 --- /dev/null +++ b/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} diff --git a/halo2-ecc/configs/bls12_381/ec_add_circuit.config b/halo2-ecc/configs/bls12_381/ec_add_circuit.config new file mode 100644 index 00000000..c17d44b9 --- /dev/null +++ b/halo2-ecc/configs/bls12_381/ec_add_circuit.config @@ -0,0 +1 @@ +{"strategy":"Simple","degree":17,"num_advice":3,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":16,"limb_bits":120,"num_limbs":4,"batch_size":100} diff --git a/halo2-ecc/results/bls12_381/pairing_bench.csv b/halo2-ecc/results/bls12_381/pairing_bench.csv new file mode 100644 index 00000000..04656bac --- /dev/null +++ b/halo2-ecc/results/bls12_381/pairing_bench.csv @@ -0,0 +1 @@ +degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,proof_time,proof_size,verify_time diff --git a/halo2-ecc/src/bls12_381/notes.md b/halo2-ecc/src/bls12_381/notes.md deleted file mode 100644 index 975ac1bc..00000000 --- a/halo2-ecc/src/bls12_381/notes.md +++ /dev/null @@ -1,4 +0,0 @@ - - -## Issues: -- [From<[u64; 4]>](https://github.com/axiom-crypto/halo2-lib/blob/980b39bcca5b3327aaef6c8d73577d9381bfa899/halo2-base/src/utils/mod.rs#L35) is not implemented for bls12_381::Fq (halo2-axiom only) diff --git a/halo2-ecc/src/bls12_381/tests/ec_add.rs b/halo2-ecc/src/bls12_381/tests/ec_add.rs new file mode 100644 index 00000000..816956c7 --- /dev/null +++ b/halo2-ecc/src/bls12_381/tests/ec_add.rs @@ -0,0 +1,110 @@ +use std::fs; +use std::fs::File; +use std::io::{BufRead, BufReader}; + +use super::*; +use crate::fields::{FieldChip, FpStrategy}; +use crate::halo2_proofs::halo2curves::bls12_381::G2Affine; +use halo2_base::gates::RangeChip; +use halo2_base::utils::testing::base_test; +use halo2_base::utils::BigPrimeField; +use halo2_base::Context; +use itertools::Itertools; +use rand_core::OsRng; + +#[derive(Clone, Copy, Debug, Serialize, Deserialize)] +struct CircuitParams { + strategy: FpStrategy, + degree: u32, + num_advice: usize, + num_lookup_advice: usize, + num_fixed: usize, + lookup_bits: usize, + limb_bits: usize, + num_limbs: usize, + batch_size: usize, +} + +fn g2_add_test( + ctx: &mut Context, + range: &RangeChip, + params: CircuitParams, + _points: Vec, +) { + let fp_chip = FpChip::::new(range, params.limb_bits, params.num_limbs); + let fp2_chip = Fp2Chip::::new(&fp_chip); + let g2_chip = EccChip::new(&fp2_chip); + + let points = + _points.iter().map(|pt| g2_chip.assign_point_unchecked(ctx, *pt)).collect::>(); + + let acc = g2_chip.sum::(ctx, points); + + let answer = _points.iter().fold(G2Affine::identity(), |a, &b| (a + b).to_affine()); + let x = fp2_chip.get_assigned_value(&acc.x.into()); + let y = fp2_chip.get_assigned_value(&acc.y.into()); + assert_eq!(answer.x, x); + assert_eq!(answer.y, y); +} + +#[test] +fn test_ec_add() { + let path = "configs/bls12_381/ec_add_circuit.config"; + let params: CircuitParams = serde_json::from_reader( + File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), + ) + .unwrap(); + + let k = params.degree; + let points = (0..params.batch_size).map(|_| G2Affine::random(OsRng)).collect_vec(); + + base_test() + .k(k) + .lookup_bits(params.lookup_bits) + .run(|ctx, range| g2_add_test(ctx, range, params, points)); +} + +// #[test] +// fn bench_ec_add() -> Result<(), Box> { +// let config_path = "configs/bls12_381/bench_ec_add.config"; +// let bench_params_file = +// File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); +// fs::create_dir_all("results/bls12_381").unwrap(); + +// let results_path = "results/bls12_381/ec_add_bench.csv"; +// let mut fs_results = File::create(results_path).unwrap(); +// writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,batch_size,proof_time,proof_size,verify_time")?; +// fs::create_dir_all("data").unwrap(); + +// let bench_params_reader = BufReader::new(bench_params_file); +// for line in bench_params_reader.lines() { +// let bench_params: CircuitParams = serde_json::from_str(line.unwrap().as_str()).unwrap(); +// let k = bench_params.degree; +// println!("---------------------- degree = {k} ------------------------------",); +// let mut rng = OsRng; + +// let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( +// vec![G2Affine::generator(); bench_params.batch_size], +// (0..bench_params.batch_size).map(|_| G2Affine::random(&mut rng)).collect_vec(), +// |pool, range, points| { +// g2_add_test(pool.main(), range, bench_params, points); +// }, +// ); +// writeln!( +// fs_results, +// "{},{},{},{},{},{},{},{},{:?},{},{:?}", +// bench_params.degree, +// bench_params.num_advice, +// bench_params.num_lookup_advice, +// bench_params.num_fixed, +// bench_params.lookup_bits, +// bench_params.limb_bits, +// bench_params.num_limbs, +// bench_params.batch_size, +// stats.proof_time.time.elapsed(), +// stats.proof_size, +// stats.verify_time.time.elapsed() +// )?; +// } +// Ok(()) +// } diff --git a/halo2-ecc/src/bls12_381/tests/mod.rs b/halo2-ecc/src/bls12_381/tests/mod.rs index 71ec5cdd..14315f7d 100644 --- a/halo2-ecc/src/bls12_381/tests/mod.rs +++ b/halo2-ecc/src/bls12_381/tests/mod.rs @@ -5,17 +5,14 @@ use crate::ecc::EccChip; use crate::group::Curve; use crate::{ fields::FpStrategy, - halo2_proofs::halo2curves::bls12_381::{pairing, Fr, G1Affine}, -}; -use halo2_base::utils::fe_to_biguint; -use halo2_base::{ - gates::{flex_gate::threads::SinglePhaseCoreManager, RangeChip}, - halo2_proofs::halo2curves::bls12_381::G1, - utils::testing::base_test, + halo2_proofs::halo2curves::bls12_381::{pairing, Fr as Scalar, G1Affine}, + halo2_proofs::halo2curves::bn256::Fr, }; +use halo2_base::utils::testing::base_test; use rand::rngs::StdRng; use rand_core::SeedableRng; use serde::{Deserialize, Serialize}; use std::io::Write; +pub mod ec_add; pub mod pairing; diff --git a/halo2-ecc/src/bls12_381/tests/pairing.rs b/halo2-ecc/src/bls12_381/tests/pairing.rs index fc9f2082..a4eb45d5 100644 --- a/halo2-ecc/src/bls12_381/tests/pairing.rs +++ b/halo2-ecc/src/bls12_381/tests/pairing.rs @@ -45,20 +45,20 @@ fn pairing_test( ); } -#[test] -fn test_pairing() { - let path = "configs/bls12_381/pairing_circuit.config"; - let params: PairingCircuitParams = serde_json::from_reader( - File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), - ) - .unwrap(); - let mut rng = StdRng::seed_from_u64(0); - let P = G1Affine::random(&mut rng); - let Q = G2Affine::random(&mut rng); - base_test().k(params.degree).lookup_bits(params.lookup_bits).run(|ctx, range| { - pairing_test(ctx, range, params, P, Q); - }); -} +// #[test] +// fn test_pairing() { +// let path = "configs/bls12_381/pairing_circuit.config"; +// let params: PairingCircuitParams = serde_json::from_reader( +// File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), +// ) +// .unwrap(); +// let mut rng = StdRng::seed_from_u64(0); +// let P = G1Affine::random(&mut rng); +// let Q = G2Affine::random(&mut rng); +// base_test().k(params.degree).lookup_bits(params.lookup_bits).run(|ctx, range| { +// pairing_test(ctx, range, params, P, Q); +// }); +// } fn pairing_check_test( ctx: &mut Context, @@ -90,8 +90,8 @@ fn test_pairing_check() { ) .unwrap(); let mut rng = StdRng::seed_from_u64(0); - let alpha = Fr::random(&mut rng); - let beta = Fr::random(&mut rng); + let alpha = Scalar::random(&mut rng); + let beta = Scalar::random(&mut rng); let P = G1Affine::from(G1Affine::generator() * alpha); let Q = G2Affine::from(G2Affine::generator() * beta); let S = G1Affine::from(G1Affine::generator() * alpha * beta); @@ -113,8 +113,8 @@ fn test_pairing_check_fail() { ) .unwrap(); let mut rng = StdRng::seed_from_u64(0); - let alpha = Fr::random(&mut rng); - let beta = Fr::random(&mut rng); + let alpha = Scalar::random(&mut rng); + let beta = Scalar::random(&mut rng); let P = G1Affine::from(G1Affine::generator() * alpha); let Q = G2Affine::from(G2Affine::generator() * beta); base_test().k(params.degree).lookup_bits(params.lookup_bits).expect_satisfied(false).run( @@ -124,50 +124,50 @@ fn test_pairing_check_fail() { ) } -#[test] -fn bench_pairing() -> Result<(), Box> { - let config_path = "configs/bls12_381/bench_pairing.config"; - let bench_params_file = - File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); - fs::create_dir_all("results/bls12_381").unwrap(); - fs::create_dir_all("data").unwrap(); +// #[test] +// fn bench_pairing() -> Result<(), Box> { +// let config_path = "configs/bls12_381/bench_pairing.config"; +// let bench_params_file = +// File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); +// fs::create_dir_all("results/bls12_381").unwrap(); +// fs::create_dir_all("data").unwrap(); - let results_path = "results/bls12_381/pairing_bench.csv"; - let mut fs_results = File::create(results_path).unwrap(); - writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,proof_time,proof_size,verify_time")?; +// let results_path = "results/bls12_381/pairing_bench.csv"; +// let mut fs_results = File::create(results_path).unwrap(); +// writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,proof_time,proof_size,verify_time")?; - let mut rng = StdRng::seed_from_u64(0); - let bench_params_reader = BufReader::new(bench_params_file); - for line in bench_params_reader.lines() { - let bench_params: PairingCircuitParams = - serde_json::from_str(line.unwrap().as_str()).unwrap(); - let k = bench_params.degree; - println!("---------------------- degree = {k} ------------------------------",); +// let mut rng = StdRng::seed_from_u64(0); +// let bench_params_reader = BufReader::new(bench_params_file); +// for line in bench_params_reader.lines() { +// let bench_params: PairingCircuitParams = +// serde_json::from_str(line.unwrap().as_str()).unwrap(); +// let k = bench_params.degree; +// println!("---------------------- degree = {k} ------------------------------",); - let P = G1Affine::random(&mut rng); - let Q = G2Affine::random(&mut rng); - let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( - (P, Q), - (P, Q), - |pool, range, (P, Q)| { - pairing_test(pool.main(), range, bench_params, P, Q); - }, - ); +// let P = G1Affine::random(&mut rng); +// let Q = G2Affine::random(&mut rng); +// let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( +// (P, Q), +// (P, Q), +// |pool, range, (P, Q)| { +// pairing_test(pool.main(), range, bench_params, P, Q); +// }, +// ); - writeln!( - fs_results, - "{},{},{},{},{},{},{},{:?},{},{:?}", - bench_params.degree, - bench_params.num_advice, - bench_params.num_lookup_advice, - bench_params.num_fixed, - bench_params.lookup_bits, - bench_params.limb_bits, - bench_params.num_limbs, - stats.proof_time.time.elapsed(), - stats.proof_size, - stats.verify_time.time.elapsed() - )?; - } - Ok(()) -} +// writeln!( +// fs_results, +// "{},{},{},{},{},{},{},{:?},{},{:?}", +// bench_params.degree, +// bench_params.num_advice, +// bench_params.num_lookup_advice, +// bench_params.num_fixed, +// bench_params.lookup_bits, +// bench_params.limb_bits, +// bench_params.num_limbs, +// stats.proof_time.time.elapsed(), +// stats.proof_size, +// stats.verify_time.time.elapsed() +// )?; +// } +// Ok(()) +// } From 701f8f45d9d23fd53a38de0a5e0019be219bb393 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Sun, 1 Oct 2023 18:14:26 +0200 Subject: [PATCH 05/22] fix miller look args names --- halo2-ecc/src/bls12_381/pairing.rs | 89 ++++++++++++++++-------------- 1 file changed, 47 insertions(+), 42 deletions(-) diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs index 5ed1f603..bd2ae790 100644 --- a/halo2-ecc/src/bls12_381/pairing.rs +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -62,10 +62,10 @@ pub fn sparse_line_function_unequal( pub fn sparse_line_function_equal( fp2_chip: &Fp2Chip, ctx: &mut Context, - Q: &EcPoint>, - P: &EcPoint>, + P: &EcPoint>, + Q: &EcPoint>, ) -> Vec>> { - let (x, y) = (&P.x, &P.y); + let (x, y) = (&Q.x, &Q.y); assert_eq!(x.0.len(), 2); assert_eq!(y.0.len(), 2); @@ -77,10 +77,10 @@ pub fn sparse_line_function_equal( let two_y_sq = fp2_chip.scalar_mul_no_carry(ctx, &y_sq, 2); let out0 = fp2_chip.sub_no_carry(ctx, &three_x_cu, &two_y_sq); - let x_sq_Px = fp2_chip.0.fp_mul_no_carry(ctx, x_sq, &Q.x); + let x_sq_Px = fp2_chip.0.fp_mul_no_carry(ctx, x_sq, &P.x); let out2 = fp2_chip.scalar_mul_no_carry(ctx, x_sq_Px, -3); - let y_Py = fp2_chip.0.fp_mul_no_carry(ctx, y.clone(), &Q.y); + let y_Py = fp2_chip.0.fp_mul_no_carry(ctx, y.clone(), &P.y); let out3 = fp2_chip.scalar_mul_no_carry(ctx, &y_Py, 2); // so far we have not "carried mod p" for any of the outputs @@ -181,19 +181,24 @@ pub fn fp12_multiply_with_line_equal( fp2_chip: &Fp2Chip, ctx: &mut Context, g: &FqPoint, - P: &EcPoint>, - Q: &EcPoint>, + P: &EcPoint>, + Q: &EcPoint>, ) -> FqPoint { - let line = sparse_line_function_equal::(fp2_chip, ctx, Q, P); + let line = sparse_line_function_equal::(fp2_chip, ctx, P, Q); sparse_fp12_multiply::(fp2_chip, ctx, g, &line) } pub fn miller_loop( ecc_chip: &EccChip>, ctx: &mut Context, - Q: &EcPoint>, P: &EcPoint>, + Q: &EcPoint>, ) -> FqPoint { + let fp_chip: &crate::fields::fp::FpChip<'_, F, Fq> = ecc_chip.field_chip.fp_chip(); + + // let sparse_f = sparse_line_function_equal::(ecc_chip.field_chip(), ctx, Q, P); + + todo!() } @@ -204,7 +209,7 @@ pub fn multi_miller_loop( ctx: &mut Context, pairs: Vec<(&EcPoint>, &EcPoint>)>, ) -> FqPoint { - let fp_chip = ecc_chip.field_chip.fp_chip(); + let fp_chip: &crate::fields::fp::FpChip<'_, F, Fq> = ecc_chip.field_chip.fp_chip(); // initialize the first line function into Fq12 point with first (Q,P) pair // this is to skip first iteration by leveraging the fact that f = 1 @@ -233,7 +238,7 @@ pub fn multi_miller_loop( }; // process second (Q,P) pair - for &(q, p) in pairs.iter().skip(1) { + for &(p, q) in pairs.iter().skip(1) { f = fp12_multiply_with_line_equal::(ecc_chip.field_chip(), ctx, &f, p, q); } @@ -249,7 +254,7 @@ pub fn multi_miller_loop( } // skip two bits after init (first beacuse f = 1, second because 1-ft found_one = false) - // restrucuture loop to perfrom additiona step for the previous iteration first and then doubling step + // resequence the loop to perfrom additiona step for the previous iteration first and then doubling step for bit in (0..62).rev().map(|i| ((BLS_X >> i) & 1) == 1) { if prev_bit { for (r, &(q, p)) in r.iter_mut().zip(pairs.iter()) { @@ -267,8 +272,8 @@ pub fn multi_miller_loop( f = fp12_chip.mul(ctx, &f, &f); - for (r, &(q, _p)) in r.iter_mut().zip(pairs.iter()) { - f = fp12_multiply_with_line_equal::(ecc_chip.field_chip(), ctx, &f, r, q); + for (r, &(p, _q)) in r.iter_mut().zip(pairs.iter()) { + f = fp12_multiply_with_line_equal::(ecc_chip.field_chip(), ctx, &f, p, r); *r = ecc_chip.double(ctx, r.clone()); } } @@ -303,31 +308,31 @@ pub fn twisted_frobenius( EcPoint::new(out_x, out_y) } -// Frobenius coefficient coeff[1][j] = ((9+u)^{(p-1)/6})^j -// -Frob_p( twist(Q) ) = ( (w^2 x)^p, -(w^3 y)^p ) = twist( coeff[1][2] * x^p, coeff[1][3] * -y^p ) -// Input: -// - Q = (x, y) point in E(Fp2) -// Output: -// - (coeff[1][2] * x^p, coeff[1][3] * -y^p) point in E(Fp2) -pub fn neg_twisted_frobenius( - ecc_chip: &EccChip>, - ctx: &mut Context, - Q: impl Into>>, - c2: impl Into>, - c3: impl Into>, -) -> EcPoint> { - let Q = Q.into(); - let c2 = c2.into(); - let c3 = c3.into(); - assert_eq!(c2.0.len(), 2); - assert_eq!(c3.0.len(), 2); - - let frob_x = ecc_chip.field_chip.conjugate(ctx, Q.x); - let neg_frob_y = ecc_chip.field_chip.neg_conjugate(ctx, Q.y); - let out_x = ecc_chip.field_chip.mul(ctx, c2, frob_x); - let out_y = ecc_chip.field_chip.mul(ctx, c3, neg_frob_y); - EcPoint::new(out_x, out_y) -} +// // Frobenius coefficient coeff[1][j] = ((9+u)^{(p-1)/6})^j +// // -Frob_p( twist(Q) ) = ( (w^2 x)^p, -(w^3 y)^p ) = twist( coeff[1][2] * x^p, coeff[1][3] * -y^p ) +// // Input: +// // - Q = (x, y) point in E(Fp2) +// // Output: +// // - (coeff[1][2] * x^p, coeff[1][3] * -y^p) point in E(Fp2) +// pub fn neg_twisted_frobenius( +// ecc_chip: &EccChip>, +// ctx: &mut Context, +// Q: impl Into>>, +// c2: impl Into>, +// c3: impl Into>, +// ) -> EcPoint> { +// let Q = Q.into(); +// let c2 = c2.into(); +// let c3 = c3.into(); +// assert_eq!(c2.0.len(), 2); +// assert_eq!(c3.0.len(), 2); + +// let frob_x = ecc_chip.field_chip.conjugate(ctx, Q.x); +// let neg_frob_y = ecc_chip.field_chip.neg_conjugate(ctx, Q.y); +// let out_x = ecc_chip.field_chip.mul(ctx, c2, frob_x); +// let out_y = ecc_chip.field_chip.mul(ctx, c3, neg_frob_y); +// EcPoint::new(out_x, out_y) +// } // To avoid issues with mutably borrowing twice (not allowed in Rust), we only store fp_chip and construct g2_chip and fp12_chip in scope when needed for temporary mutable borrows pub struct PairingChip<'chip, F: BigPrimeField> { @@ -361,12 +366,12 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { pub fn miller_loop( &self, ctx: &mut Context, - Q: &EcPoint>, P: &EcPoint>, + Q: &EcPoint>, ) -> FqPoint { let fp2_chip = Fp2Chip::::new(self.fp_chip); let g2_chip = EccChip::new(&fp2_chip); - miller_loop::(&g2_chip, ctx, Q, P) + miller_loop::(&g2_chip, ctx, P, Q) } pub fn multi_miller_loop( @@ -391,7 +396,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { Q: &EcPoint>, P: &EcPoint>, ) -> FqPoint { - let f0 = self.miller_loop(ctx, Q, P); + let f0 = self.miller_loop(ctx, P, Q); let fp12_chip = Fp12Chip::::new(self.fp_chip); // final_exp implemented in final_exp module fp12_chip.final_exp(ctx, f0) From 83553125deb8349385ed002138e5f7d4014453d5 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Sun, 1 Oct 2023 21:15:46 +0200 Subject: [PATCH 06/22] impl (single) miller_loop --- halo2-ecc/src/bls12_381/pairing.rs | 128 +++++++++++------------ halo2-ecc/src/bls12_381/tests/ec_add.rs | 82 +++++++-------- halo2-ecc/src/bls12_381/tests/mod.rs | 1 - halo2-ecc/src/bls12_381/tests/pairing.rs | 114 ++++++++++---------- 4 files changed, 162 insertions(+), 163 deletions(-) diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs index bd2ae790..cb46065c 100644 --- a/halo2-ecc/src/bls12_381/pairing.rs +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -7,6 +7,7 @@ use crate::{ fields::fp12::mul_no_carry_w6, fields::FieldChip, }; +use halo2_base::halo2_proofs::halo2curves::bls12_381::BLS_X_IS_NEGATIVE; use halo2_base::utils::BigPrimeField; use halo2_base::Context; @@ -164,10 +165,10 @@ pub fn fp12_multiply_with_line_unequal( fp2_chip: &Fp2Chip, ctx: &mut Context, g: &FqPoint, - P: (&EcPoint>, &EcPoint>), - Q: &EcPoint>, + P: &EcPoint>, + Q: (&EcPoint>, &EcPoint>), ) -> FqPoint { - let line = sparse_line_function_unequal::(fp2_chip, ctx, P, Q); + let line = sparse_line_function_unequal::(fp2_chip, ctx, Q, P); sparse_fp12_multiply::(fp2_chip, ctx, g, &line) } @@ -194,12 +195,64 @@ pub fn miller_loop( P: &EcPoint>, Q: &EcPoint>, ) -> FqPoint { - let fp_chip: &crate::fields::fp::FpChip<'_, F, Fq> = ecc_chip.field_chip.fp_chip(); + let sparse_f = sparse_line_function_equal::(ecc_chip.field_chip(), ctx, P, Q); + assert_eq!(sparse_f.len(), 6); + + let fp_chip = ecc_chip.field_chip.fp_chip(); + let zero_fp = fp_chip.load_constant(ctx, Fq::zero()); + let mut f_coeffs = Vec::with_capacity(12); + for coeff in &sparse_f { + if let Some(fp2_point) = coeff { + f_coeffs.push(fp2_point[0].clone()); + } else { + f_coeffs.push(zero_fp.clone()); + } + } + for coeff in &sparse_f { + if let Some(fp2_point) = coeff { + f_coeffs.push(fp2_point[1].clone()); + } else { + f_coeffs.push(zero_fp.clone()); + } + } + + let mut f = FieldVector(f_coeffs); + let fp12_chip = Fp12Chip::::new(fp_chip); + + let mut r = Q.clone(); + + let mut found_one = true; + let mut prev_bit = true; + + // double Q as in the first part of Miller loop + r = ecc_chip.double(ctx, r.clone()); + + // skip two bits after init (first beacuse f = 1, second because 1-ft found_one = false) + // resequence the loop to perfrom additiona step for the previous iteration first and then doubling step + for bit in (0..62).rev().map(|i| ((BLS_X >> i) & 1) == 1) { + if prev_bit { + f = fp12_multiply_with_line_unequal::(ecc_chip.field_chip(), ctx, &f, P, (&r, Q)); + r = ecc_chip.add_unequal(ctx, r.clone(), Q.clone(), false); + } + + prev_bit = bit; + + if !found_one { + found_one = bit; + continue; + } + + f = fp12_chip.mul(ctx, &f, &f); - // let sparse_f = sparse_line_function_equal::(ecc_chip.field_chip(), ctx, Q, P); + f = fp12_multiply_with_line_equal::(ecc_chip.field_chip(), ctx, &f, P, &r); + r = ecc_chip.double(ctx, r.clone()); + } + if BLS_X_IS_NEGATIVE { + f = fp12_chip.conjugate(ctx, f) + } - todo!() + f } // let pairs = [(a_i, b_i)], a_i in G_1, b_i in G_2 @@ -209,7 +262,7 @@ pub fn multi_miller_loop( ctx: &mut Context, pairs: Vec<(&EcPoint>, &EcPoint>)>, ) -> FqPoint { - let fp_chip: &crate::fields::fp::FpChip<'_, F, Fq> = ecc_chip.field_chip.fp_chip(); + let fp_chip = ecc_chip.field_chip.fp_chip(); // initialize the first line function into Fq12 point with first (Q,P) pair // this is to skip first iteration by leveraging the fact that f = 1 @@ -248,7 +301,7 @@ pub fn multi_miller_loop( let mut found_one = true; let mut prev_bit = true; - // double P as in the first part of Miller loop + // double Q as in the first part of Miller loop for r in r.iter_mut() { *r = ecc_chip.double(ctx, r.clone()); } @@ -257,9 +310,9 @@ pub fn multi_miller_loop( // resequence the loop to perfrom additiona step for the previous iteration first and then doubling step for bit in (0..62).rev().map(|i| ((BLS_X >> i) & 1) == 1) { if prev_bit { - for (r, &(q, p)) in r.iter_mut().zip(pairs.iter()) { - f = fp12_multiply_with_line_unequal::(ecc_chip.field_chip(), ctx, &f, (r, p), q); - *r = ecc_chip.add_unequal(ctx, r.clone(), p.clone(), false); + for (r, &(p, q)) in r.iter_mut().zip(pairs.iter()) { + f = fp12_multiply_with_line_unequal::(ecc_chip.field_chip(), ctx, &f, p, (r, q)); + *r = ecc_chip.add_unequal(ctx, r.clone(), q.clone(), false); } } @@ -281,59 +334,6 @@ pub fn multi_miller_loop( f } -// Frobenius coefficient coeff[1][j] = ((9+u)^{(p-1)/6})^j -// Frob_p( twist(Q) ) = ( (w^2 x)^p, (w^3 y)^p ) = twist( coeff[1][2] * x^p, coeff[1][3] * y^p ) -// Input: -// - Q = (x, y) point in E(Fp2) -// - coeff[1][2], coeff[1][3] as assigned cells: this is an optimization to avoid loading new constants -// Output: -// - (coeff[1][2] * x^p, coeff[1][3] * y^p) point in E(Fp2) -pub fn twisted_frobenius( - ecc_chip: &EccChip>, - ctx: &mut Context, - Q: impl Into>>, - c2: impl Into>, - c3: impl Into>, -) -> EcPoint> { - let Q = Q.into(); - let c2 = c2.into(); - let c3 = c3.into(); - assert_eq!(c2.0.len(), 2); - assert_eq!(c3.0.len(), 2); - - let frob_x = ecc_chip.field_chip.conjugate(ctx, Q.x); - let frob_y = ecc_chip.field_chip.conjugate(ctx, Q.y); - let out_x = ecc_chip.field_chip.mul(ctx, c2, frob_x); - let out_y = ecc_chip.field_chip.mul(ctx, c3, frob_y); - EcPoint::new(out_x, out_y) -} - -// // Frobenius coefficient coeff[1][j] = ((9+u)^{(p-1)/6})^j -// // -Frob_p( twist(Q) ) = ( (w^2 x)^p, -(w^3 y)^p ) = twist( coeff[1][2] * x^p, coeff[1][3] * -y^p ) -// // Input: -// // - Q = (x, y) point in E(Fp2) -// // Output: -// // - (coeff[1][2] * x^p, coeff[1][3] * -y^p) point in E(Fp2) -// pub fn neg_twisted_frobenius( -// ecc_chip: &EccChip>, -// ctx: &mut Context, -// Q: impl Into>>, -// c2: impl Into>, -// c3: impl Into>, -// ) -> EcPoint> { -// let Q = Q.into(); -// let c2 = c2.into(); -// let c3 = c3.into(); -// assert_eq!(c2.0.len(), 2); -// assert_eq!(c3.0.len(), 2); - -// let frob_x = ecc_chip.field_chip.conjugate(ctx, Q.x); -// let neg_frob_y = ecc_chip.field_chip.neg_conjugate(ctx, Q.y); -// let out_x = ecc_chip.field_chip.mul(ctx, c2, frob_x); -// let out_y = ecc_chip.field_chip.mul(ctx, c3, neg_frob_y); -// EcPoint::new(out_x, out_y) -// } - // To avoid issues with mutably borrowing twice (not allowed in Rust), we only store fp_chip and construct g2_chip and fp12_chip in scope when needed for temporary mutable borrows pub struct PairingChip<'chip, F: BigPrimeField> { pub fp_chip: &'chip FpChip<'chip, F>, diff --git a/halo2-ecc/src/bls12_381/tests/ec_add.rs b/halo2-ecc/src/bls12_381/tests/ec_add.rs index 816956c7..9d0b3692 100644 --- a/halo2-ecc/src/bls12_381/tests/ec_add.rs +++ b/halo2-ecc/src/bls12_381/tests/ec_add.rs @@ -64,47 +64,47 @@ fn test_ec_add() { .run(|ctx, range| g2_add_test(ctx, range, params, points)); } -// #[test] -// fn bench_ec_add() -> Result<(), Box> { -// let config_path = "configs/bls12_381/bench_ec_add.config"; -// let bench_params_file = -// File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); -// fs::create_dir_all("results/bls12_381").unwrap(); +#[test] +fn bench_ec_add() -> Result<(), Box> { + let config_path = "configs/bls12_381/bench_ec_add.config"; + let bench_params_file = + File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); + fs::create_dir_all("results/bls12_381").unwrap(); -// let results_path = "results/bls12_381/ec_add_bench.csv"; -// let mut fs_results = File::create(results_path).unwrap(); -// writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,batch_size,proof_time,proof_size,verify_time")?; -// fs::create_dir_all("data").unwrap(); + let results_path = "results/bls12_381/ec_add_bench.csv"; + let mut fs_results = File::create(results_path).unwrap(); + writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,batch_size,proof_time,proof_size,verify_time")?; + fs::create_dir_all("data").unwrap(); -// let bench_params_reader = BufReader::new(bench_params_file); -// for line in bench_params_reader.lines() { -// let bench_params: CircuitParams = serde_json::from_str(line.unwrap().as_str()).unwrap(); -// let k = bench_params.degree; -// println!("---------------------- degree = {k} ------------------------------",); -// let mut rng = OsRng; + let bench_params_reader = BufReader::new(bench_params_file); + for line in bench_params_reader.lines() { + let bench_params: CircuitParams = serde_json::from_str(line.unwrap().as_str()).unwrap(); + let k = bench_params.degree; + println!("---------------------- degree = {k} ------------------------------",); + let mut rng = OsRng; -// let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( -// vec![G2Affine::generator(); bench_params.batch_size], -// (0..bench_params.batch_size).map(|_| G2Affine::random(&mut rng)).collect_vec(), -// |pool, range, points| { -// g2_add_test(pool.main(), range, bench_params, points); -// }, -// ); -// writeln!( -// fs_results, -// "{},{},{},{},{},{},{},{},{:?},{},{:?}", -// bench_params.degree, -// bench_params.num_advice, -// bench_params.num_lookup_advice, -// bench_params.num_fixed, -// bench_params.lookup_bits, -// bench_params.limb_bits, -// bench_params.num_limbs, -// bench_params.batch_size, -// stats.proof_time.time.elapsed(), -// stats.proof_size, -// stats.verify_time.time.elapsed() -// )?; -// } -// Ok(()) -// } + let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( + vec![G2Affine::generator(); bench_params.batch_size], + (0..bench_params.batch_size).map(|_| G2Affine::random(&mut rng)).collect_vec(), + |pool, range, points| { + g2_add_test(pool.main(), range, bench_params, points); + }, + ); + writeln!( + fs_results, + "{},{},{},{},{},{},{},{},{:?},{},{:?}", + bench_params.degree, + bench_params.num_advice, + bench_params.num_lookup_advice, + bench_params.num_fixed, + bench_params.lookup_bits, + bench_params.limb_bits, + bench_params.num_limbs, + bench_params.batch_size, + stats.proof_time.time.elapsed(), + stats.proof_size, + stats.verify_time.time.elapsed() + )?; + } + Ok(()) +} diff --git a/halo2-ecc/src/bls12_381/tests/mod.rs b/halo2-ecc/src/bls12_381/tests/mod.rs index 14315f7d..53c966ae 100644 --- a/halo2-ecc/src/bls12_381/tests/mod.rs +++ b/halo2-ecc/src/bls12_381/tests/mod.rs @@ -6,7 +6,6 @@ use crate::group::Curve; use crate::{ fields::FpStrategy, halo2_proofs::halo2curves::bls12_381::{pairing, Fr as Scalar, G1Affine}, - halo2_proofs::halo2curves::bn256::Fr, }; use halo2_base::utils::testing::base_test; use rand::rngs::StdRng; diff --git a/halo2-ecc/src/bls12_381/tests/pairing.rs b/halo2-ecc/src/bls12_381/tests/pairing.rs index a4eb45d5..ee164dba 100644 --- a/halo2-ecc/src/bls12_381/tests/pairing.rs +++ b/halo2-ecc/src/bls12_381/tests/pairing.rs @@ -45,20 +45,20 @@ fn pairing_test( ); } -// #[test] -// fn test_pairing() { -// let path = "configs/bls12_381/pairing_circuit.config"; -// let params: PairingCircuitParams = serde_json::from_reader( -// File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), -// ) -// .unwrap(); -// let mut rng = StdRng::seed_from_u64(0); -// let P = G1Affine::random(&mut rng); -// let Q = G2Affine::random(&mut rng); -// base_test().k(params.degree).lookup_bits(params.lookup_bits).run(|ctx, range| { -// pairing_test(ctx, range, params, P, Q); -// }); -// } +#[test] +fn test_pairing() { + let path = "configs/bls12_381/pairing_circuit.config"; + let params: PairingCircuitParams = serde_json::from_reader( + File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), + ) + .unwrap(); + let mut rng = StdRng::seed_from_u64(0); + let P = G1Affine::random(&mut rng); + let Q = G2Affine::random(&mut rng); + base_test().k(params.degree).lookup_bits(params.lookup_bits).run(|ctx, range| { + pairing_test(ctx, range, params, P, Q); + }); +} fn pairing_check_test( ctx: &mut Context, @@ -124,50 +124,50 @@ fn test_pairing_check_fail() { ) } -// #[test] -// fn bench_pairing() -> Result<(), Box> { -// let config_path = "configs/bls12_381/bench_pairing.config"; -// let bench_params_file = -// File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); -// fs::create_dir_all("results/bls12_381").unwrap(); -// fs::create_dir_all("data").unwrap(); +#[test] +fn bench_pairing() -> Result<(), Box> { + let config_path = "configs/bls12_381/bench_pairing.config"; + let bench_params_file = + File::open(config_path).unwrap_or_else(|e| panic!("{config_path} does not exist: {e:?}")); + fs::create_dir_all("results/bls12_381").unwrap(); + fs::create_dir_all("data").unwrap(); -// let results_path = "results/bls12_381/pairing_bench.csv"; -// let mut fs_results = File::create(results_path).unwrap(); -// writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,proof_time,proof_size,verify_time")?; + let results_path = "results/bls12_381/pairing_bench.csv"; + let mut fs_results = File::create(results_path).unwrap(); + writeln!(fs_results, "degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,proof_time,proof_size,verify_time")?; -// let mut rng = StdRng::seed_from_u64(0); -// let bench_params_reader = BufReader::new(bench_params_file); -// for line in bench_params_reader.lines() { -// let bench_params: PairingCircuitParams = -// serde_json::from_str(line.unwrap().as_str()).unwrap(); -// let k = bench_params.degree; -// println!("---------------------- degree = {k} ------------------------------",); + let mut rng = StdRng::seed_from_u64(0); + let bench_params_reader = BufReader::new(bench_params_file); + for line in bench_params_reader.lines() { + let bench_params: PairingCircuitParams = + serde_json::from_str(line.unwrap().as_str()).unwrap(); + let k = bench_params.degree; + println!("---------------------- degree = {k} ------------------------------",); -// let P = G1Affine::random(&mut rng); -// let Q = G2Affine::random(&mut rng); -// let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( -// (P, Q), -// (P, Q), -// |pool, range, (P, Q)| { -// pairing_test(pool.main(), range, bench_params, P, Q); -// }, -// ); + let P = G1Affine::random(&mut rng); + let Q = G2Affine::random(&mut rng); + let stats = base_test().k(k).lookup_bits(bench_params.lookup_bits).bench_builder( + (P, Q), + (P, Q), + |pool, range, (P, Q)| { + pairing_test(pool.main(), range, bench_params, P, Q); + }, + ); -// writeln!( -// fs_results, -// "{},{},{},{},{},{},{},{:?},{},{:?}", -// bench_params.degree, -// bench_params.num_advice, -// bench_params.num_lookup_advice, -// bench_params.num_fixed, -// bench_params.lookup_bits, -// bench_params.limb_bits, -// bench_params.num_limbs, -// stats.proof_time.time.elapsed(), -// stats.proof_size, -// stats.verify_time.time.elapsed() -// )?; -// } -// Ok(()) -// } + writeln!( + fs_results, + "{},{},{},{},{},{},{},{:?},{},{:?}", + bench_params.degree, + bench_params.num_advice, + bench_params.num_lookup_advice, + bench_params.num_fixed, + bench_params.lookup_bits, + bench_params.limb_bits, + bench_params.num_limbs, + stats.proof_time.time.elapsed(), + stats.proof_size, + stats.verify_time.time.elapsed() + )?; + } + Ok(()) +} From 4cd431a0e69bdbaab059a7aa02e90cbe9cc52017 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Sun, 1 Oct 2023 21:19:53 +0200 Subject: [PATCH 07/22] cargo fix+fmt --- halo2-ecc/src/bigint/carry_mod.rs | 11 ++++++++--- halo2-ecc/src/bigint/check_carry_mod_to_zero.rs | 10 +++++++--- halo2-ecc/src/bls12_381/tests/pairing.rs | 5 ++++- halo2-ecc/src/lib.rs | 2 +- 4 files changed, 20 insertions(+), 8 deletions(-) diff --git a/halo2-ecc/src/bigint/carry_mod.rs b/halo2-ecc/src/bigint/carry_mod.rs index c12a0fde..0d8ddabd 100644 --- a/halo2-ecc/src/bigint/carry_mod.rs +++ b/halo2-ecc/src/bigint/carry_mod.rs @@ -8,7 +8,7 @@ use halo2_base::{ }; use num_bigint::BigInt; use num_integer::Integer; -use num_traits::{One, Signed}; +use num_traits::One; use super::{check_carry_to_zero, CRTInteger, OverflowInteger, ProperCrtUint, ProperUint}; @@ -58,7 +58,7 @@ pub fn crt( // 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)} // FIXME: hotfix for BLS12 support - let quot_last_limb_bits = 0; //quot_max_bits - n * (k - 1); + let _quot_last_limb_bits = 0; //quot_max_bits - n * (k - 1); 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) @@ -148,7 +148,12 @@ pub fn crt( // 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() { // FIXME: hotfix for BLS12 support - let limb_bits = if q_index == k - 1 { /* quot_last_limb_bits */ n } else { n }; + let limb_bits = if q_index == k - 1 { + /* quot_last_limb_bits */ + n + } else { + n + }; let limb_base = if q_index == k - 1 { range.gate().pow_of_two()[limb_bits] } else { limb_bases[1] }; diff --git a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs index 7a2e634d..9659e6d3 100644 --- a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs +++ b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs @@ -7,7 +7,7 @@ use halo2_base::{ }; use num_bigint::BigInt; use num_integer::Integer; -use num_traits::{One, Signed, Zero}; +use num_traits::One; use std::{cmp::max, iter}; // same as carry_mod::crt but `out = 0` so no need to range check @@ -36,7 +36,7 @@ pub fn crt( let quot_max_bits = trunc_len - 1 + (F::NUM_BITS as usize) - 1 - (modulus.bits() as usize); assert!(quot_max_bits < trunc_len); // FIXME: hotfix for BLS12 support - let quot_last_limb_bits = 0; // quot_max_bits - n * (k - 1); + let _quot_last_limb_bits = 0; // quot_max_bits - n * (k - 1); // these are witness vectors: // we need to find `quot_vec` as a proper BigInt with k limbs @@ -94,7 +94,11 @@ pub fn crt( // 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() { // FIXME: hotfix for BLS12 support - let limb_bits = if q_index == k - 1 { n /* quot_last_limb_bits */ } else { n }; + let limb_bits = if q_index == k - 1 { + n /* quot_last_limb_bits */ + } else { + n + }; let limb_base = if q_index == k - 1 { range.gate().pow_of_two()[limb_bits] } else { limb_bases[1] }; diff --git a/halo2-ecc/src/bls12_381/tests/pairing.rs b/halo2-ecc/src/bls12_381/tests/pairing.rs index ee164dba..b46e6037 100644 --- a/halo2-ecc/src/bls12_381/tests/pairing.rs +++ b/halo2-ecc/src/bls12_381/tests/pairing.rs @@ -7,7 +7,10 @@ use crate::fields::FieldChip; use super::*; use halo2_base::{ - gates::RangeChip, halo2_proofs::{arithmetic::Field, halo2curves::bls12_381::G2Affine}, utils::BigPrimeField, Context, + gates::RangeChip, + halo2_proofs::{arithmetic::Field, halo2curves::bls12_381::G2Affine}, + utils::BigPrimeField, + Context, }; use serde::{Deserialize, Serialize}; diff --git a/halo2-ecc/src/lib.rs b/halo2-ecc/src/lib.rs index d87ce7fc..3f86ba86 100644 --- a/halo2-ecc/src/lib.rs +++ b/halo2-ecc/src/lib.rs @@ -7,8 +7,8 @@ pub mod bigint; pub mod ecc; pub mod fields; -pub mod bn254; pub mod bls12_381; +pub mod bn254; pub mod grumpkin; pub mod secp256k1; From 4c107de023bb77c71eb8ac0fded595a10e9877ec Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Mon, 2 Oct 2023 13:07:29 +0200 Subject: [PATCH 08/22] add comments --- Cargo.toml | 7 ++----- halo2-ecc/src/bls12_381/final_exp.rs | 3 +-- halo2-ecc/src/bls12_381/mod.rs | 4 +++- halo2-ecc/src/bls12_381/pairing.rs | 27 +++++++++++++++++++++++---- 4 files changed, 29 insertions(+), 12 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 09c03f33..01b1acb7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -41,10 +41,7 @@ halo2-base = { path = "../halo2-lib/halo2-base" } halo2-ecc = { path = "../halo2-lib/halo2-ecc" } [patch."https://github.com/privacy-scaling-explorations/halo2curves"] -# halo2curves = { git = "https://github.com/timoftime/halo2curves", rev = "b682183" } -halo2curves = { path = "../halo2curves" } - +halo2curves = { git = "https://github.com/timoftime/halo2curves", branch = "support_bls12-381" } [patch."https://github.com/axiom-crypto/halo2curves"] -# halo2curves = { git = "https://github.com/timoftime/halo2curves", rev = "b682183" } -halo2curves = { path = "../halo2curves" } +halo2curves = { git = "https://github.com/timoftime/halo2curves", branch = "support_bls12-381" } diff --git a/halo2-ecc/src/bls12_381/final_exp.rs b/halo2-ecc/src/bls12_381/final_exp.rs index b27d0439..acc712fd 100644 --- a/halo2-ecc/src/bls12_381/final_exp.rs +++ b/halo2-ecc/src/bls12_381/final_exp.rs @@ -1,3 +1,4 @@ +use super::XI_0; use super::{Fp12Chip, Fp2Chip, FpChip, FqPoint}; use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2, BLS_X, FROBENIUS_COEFF_FQ12_C1}; use crate::{ @@ -8,8 +9,6 @@ use halo2_base::utils::BigPrimeField; use halo2_base::{gates::GateInstructions, utils::modulus, Context, QuantumCell::Constant}; use num_bigint::BigUint; -const XI_0: i64 = 1; - impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { // computes a ** (p ** power) // only works for p = 3 (mod 4) and p = 1 (mod 6) diff --git a/halo2-ecc/src/bls12_381/mod.rs b/halo2-ecc/src/bls12_381/mod.rs index c4c22d5c..e39d079f 100644 --- a/halo2-ecc/src/bls12_381/mod.rs +++ b/halo2-ecc/src/bls12_381/mod.rs @@ -6,11 +6,13 @@ use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2}; pub mod final_exp; pub mod pairing; +pub(crate) const XI_0: i64 = 1; + pub type FpChip<'range, F> = fp::FpChip<'range, F, Fq>; pub type FpPoint = ProperCrtUint; pub type FqPoint = FieldVector>; pub type Fp2Chip<'chip, F> = fp2::Fp2Chip<'chip, F, FpChip<'chip, F>, Fq2>; -pub type Fp12Chip<'chip, F> = fp12::Fp12Chip<'chip, F, FpChip<'chip, F>, Fq12, 1>; +pub type Fp12Chip<'chip, F> = fp12::Fp12Chip<'chip, F, FpChip<'chip, F>, Fq12, XI_0>; #[cfg(test)] pub(crate) mod tests; diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs index cb46065c..be44bad5 100644 --- a/halo2-ecc/src/bls12_381/pairing.rs +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -1,5 +1,5 @@ #![allow(non_snake_case)] -use super::{Fp12Chip, Fp2Chip, FpChip, FpPoint, Fq, FqPoint}; +use super::{Fp12Chip, Fp2Chip, FpChip, FpPoint, Fq, FqPoint, XI_0}; use crate::fields::vector::FieldVector; use crate::halo2_proofs::halo2curves::bls12_381::{Fq12, G1Affine, G2Affine, BLS_X}; use crate::{ @@ -11,8 +11,6 @@ use halo2_base::halo2_proofs::halo2curves::bls12_381::BLS_X_IS_NEGATIVE; use halo2_base::utils::BigPrimeField; use halo2_base::Context; -const XI_0: i64 = 1; - // Inputs: // Q0 = (x_1, y_1) and Q1 = (x_2, y_2) are points in E(Fp2) // P is point (X, Y) in E(Fp) @@ -189,6 +187,16 @@ pub fn fp12_multiply_with_line_equal( sparse_fp12_multiply::(fp2_chip, ctx, g, &line) } +// Assuming curve is of form `y^2 = x^3 + b` for now (a = 0) for less operations +// Value of `b` is never used +// Inputs: +// - Q = (x, y) is a point in E(Fp2) +// - P is a point in E(Fp) +// Output: +// - f_{loop_count}(Q,P) * l_{[loop_count] Q', Frob_p(Q')}(P) * l_{[loop_count] Q' + Frob_p(Q'), -Frob_p^2(Q')}(P) +// - where we start with `f_1(Q,P) = 1` and use Miller's algorithm f_{i+j} = f_i * f_j * l_{i,j}(Q,P) +// - Q' = Psi(Q) in E(Fp12) +// - Frob_p(x,y) = (x^p, y^p) pub fn miller_loop( ecc_chip: &EccChip>, ctx: &mut Context, @@ -331,10 +339,16 @@ pub fn multi_miller_loop( } } + // Apperently Gt conjugation can be skipped for multi miller loop. However, cannot find evidence for this. + // if BLS_X_IS_NEGATIVE { + // f = fp12_chip.conjugate(ctx, f) + // } + f } -// To avoid issues with mutably borrowing twice (not allowed in Rust), we only store fp_chip and construct g2_chip and fp12_chip in scope when needed for temporary mutable borrows +/// Pairing chip for BLS12-381. +/// To avoid issues with mutably borrowing twice (not allowed in Rust), we only store `fp_chip` and construct `g2_chip` in scope when needed for temporary mutable borrows pub struct PairingChip<'chip, F: BigPrimeField> { pub fp_chip: &'chip FpChip<'chip, F>, } @@ -344,6 +358,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { Self { fp_chip } } + /// Assigns a constant G1 point without checking if it's on the curve. pub fn load_private_g1_unchecked( &self, ctx: &mut Context, @@ -353,6 +368,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { g1_chip.load_private_unchecked(ctx, (point.x, point.y)) } + /// Assigns a constant G2 point without checking if it's on the curve. pub fn load_private_g2_unchecked( &self, ctx: &mut Context, @@ -363,6 +379,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { g2_chip.load_private_unchecked(ctx, (point.x, point.y)) } + /// Miller loop for a single pair of (G1, G2). pub fn miller_loop( &self, ctx: &mut Context, @@ -374,6 +391,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { miller_loop::(&g2_chip, ctx, P, Q) } + /// Multi-pairing Miller loop. pub fn multi_miller_loop( &self, ctx: &mut Context, @@ -384,6 +402,7 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { multi_miller_loop::(&g2_chip, ctx, pairs) } + /// Final exponentiation to complete the pairing. pub fn final_exp(&self, ctx: &mut Context, f: FqPoint) -> FqPoint { let fp12_chip = Fp12Chip::::new(self.fp_chip); fp12_chip.final_exp(ctx, f) From 1a01328043ab3ccf0b9b26b861fec93859d7a2ed Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Thu, 12 Oct 2023 15:08:08 +0200 Subject: [PATCH 09/22] use separte halo2curves with `halo2-pse` feature --- Cargo.toml | 3 --- halo2-base/src/utils/mod.rs | 2 +- halo2-ecc/Cargo.toml | 5 ++++- halo2-ecc/results/bls12_381/pairing_bench.csv | 1 - halo2-ecc/src/bls12_381/final_exp.rs | 2 +- halo2-ecc/src/bls12_381/mod.rs | 10 +++++++++- halo2-ecc/src/bls12_381/pairing.rs | 4 ++-- halo2-ecc/src/bls12_381/tests/ec_add.rs | 1 - halo2-ecc/src/bls12_381/tests/mod.rs | 10 ++++++---- halo2-ecc/src/bls12_381/tests/pairing.rs | 5 +---- halo2-ecc/src/bn254/tests/bls_signature.rs | 6 +++++- halo2-ecc/src/fields/fp12.rs | 4 ++++ halo2-ecc/src/fields/fp2.rs | 5 +++++ 13 files changed, 38 insertions(+), 20 deletions(-) delete mode 100644 halo2-ecc/results/bls12_381/pairing_bench.csv diff --git a/Cargo.toml b/Cargo.toml index 01b1acb7..43d78ff1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -40,8 +40,5 @@ debug = true halo2-base = { path = "../halo2-lib/halo2-base" } halo2-ecc = { path = "../halo2-lib/halo2-ecc" } -[patch."https://github.com/privacy-scaling-explorations/halo2curves"] -halo2curves = { git = "https://github.com/timoftime/halo2curves", branch = "support_bls12-381" } - [patch."https://github.com/axiom-crypto/halo2curves"] halo2curves = { git = "https://github.com/timoftime/halo2curves", branch = "support_bls12-381" } diff --git a/halo2-base/src/utils/mod.rs b/halo2-base/src/utils/mod.rs index fb1d7235..116459e6 100644 --- a/halo2-base/src/utils/mod.rs +++ b/halo2-base/src/utils/mod.rs @@ -150,7 +150,7 @@ pub trait ScalarField: PrimeField + FromUniformBytes<64> + From + Hash + O /// [ScalarField] that is ~256 bits long #[cfg(feature = "halo2-pse")] -pub trait BigPrimeField = PrimeField + 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]. /// diff --git a/halo2-ecc/Cargo.toml b/halo2-ecc/Cargo.toml index d3da45fc..cf15855f 100644 --- a/halo2-ecc/Cargo.toml +++ b/halo2-ecc/Cargo.toml @@ -17,6 +17,9 @@ rayon="1.6.1" test-case="3.1.0" halo2-base={ path="../halo2-base", default-features=false } +# Use additiona 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 patchign it is not possible +halo2curves = { git = "https://github.com/axiom-crypto/halo2curves", optional=true } [dev-dependencies] ark-std={ version="0.3.0", features=["print-trace"] } @@ -33,7 +36,7 @@ default=["jemallocator", "halo2-axiom", "display"] dev-graph=["halo2-base/dev-graph"] 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"] diff --git a/halo2-ecc/results/bls12_381/pairing_bench.csv b/halo2-ecc/results/bls12_381/pairing_bench.csv deleted file mode 100644 index 04656bac..00000000 --- a/halo2-ecc/results/bls12_381/pairing_bench.csv +++ /dev/null @@ -1 +0,0 @@ -degree,num_advice,num_lookup,num_fixed,lookup_bits,limb_bits,num_limbs,proof_time,proof_size,verify_time diff --git a/halo2-ecc/src/bls12_381/final_exp.rs b/halo2-ecc/src/bls12_381/final_exp.rs index acc712fd..a3608684 100644 --- a/halo2-ecc/src/bls12_381/final_exp.rs +++ b/halo2-ecc/src/bls12_381/final_exp.rs @@ -1,6 +1,6 @@ use super::XI_0; use super::{Fp12Chip, Fp2Chip, FpChip, FqPoint}; -use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2, BLS_X, FROBENIUS_COEFF_FQ12_C1}; +use super::{Fq, Fq12, Fq2, BLS_X, FROBENIUS_COEFF_FQ12_C1}; use crate::{ ecc::get_naf, fields::{fp12::mul_no_carry_w6, vector::FieldVector, FieldChip}, diff --git a/halo2-ecc/src/bls12_381/mod.rs b/halo2-ecc/src/bls12_381/mod.rs index e39d079f..3c04ef01 100644 --- a/halo2-ecc/src/bls12_381/mod.rs +++ b/halo2-ecc/src/bls12_381/mod.rs @@ -1,11 +1,19 @@ use crate::bigint::ProperCrtUint; use crate::fields::vector::FieldVector; use crate::fields::{fp, fp12, fp2}; -use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2}; pub mod final_exp; pub mod pairing; +#[cfg(feature = "halo2-axiom")] +pub(crate) use crate::halo2_proofs::halo2curves::bls12_381::{ + Fq, Fq12, Fq2, G1Affine, G2Affine, BLS_X, BLS_X_IS_NEGATIVE, FROBENIUS_COEFF_FQ12_C1, +}; +#[cfg(feature = "halo2-pse")] +pub(crate) use halo2curves::bls12_381::{ + Fq, Fq12, Fq2, G1Affine, G2Affine, BLS_X, BLS_X_IS_NEGATIVE, FROBENIUS_COEFF_FQ12_C1, +}; + pub(crate) const XI_0: i64 = 1; pub type FpChip<'range, F> = fp::FpChip<'range, F, Fq>; diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs index be44bad5..bd4ded7d 100644 --- a/halo2-ecc/src/bls12_381/pairing.rs +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -1,13 +1,13 @@ #![allow(non_snake_case)] use super::{Fp12Chip, Fp2Chip, FpChip, FpPoint, Fq, FqPoint, XI_0}; +use super::{Fq12, G1Affine, G2Affine, BLS_X, BLS_X_IS_NEGATIVE}; use crate::fields::vector::FieldVector; -use crate::halo2_proofs::halo2curves::bls12_381::{Fq12, G1Affine, G2Affine, BLS_X}; use crate::{ ecc::{EcPoint, EccChip}, fields::fp12::mul_no_carry_w6, fields::FieldChip, }; -use halo2_base::halo2_proofs::halo2curves::bls12_381::BLS_X_IS_NEGATIVE; + use halo2_base::utils::BigPrimeField; use halo2_base::Context; diff --git a/halo2-ecc/src/bls12_381/tests/ec_add.rs b/halo2-ecc/src/bls12_381/tests/ec_add.rs index 9d0b3692..8a2a566d 100644 --- a/halo2-ecc/src/bls12_381/tests/ec_add.rs +++ b/halo2-ecc/src/bls12_381/tests/ec_add.rs @@ -4,7 +4,6 @@ use std::io::{BufRead, BufReader}; use super::*; use crate::fields::{FieldChip, FpStrategy}; -use crate::halo2_proofs::halo2curves::bls12_381::G2Affine; use halo2_base::gates::RangeChip; use halo2_base::utils::testing::base_test; use halo2_base::utils::BigPrimeField; diff --git a/halo2-ecc/src/bls12_381/tests/mod.rs b/halo2-ecc/src/bls12_381/tests/mod.rs index 53c966ae..785a96ea 100644 --- a/halo2-ecc/src/bls12_381/tests/mod.rs +++ b/halo2-ecc/src/bls12_381/tests/mod.rs @@ -2,16 +2,18 @@ use super::pairing::PairingChip; use super::*; use crate::ecc::EccChip; +use crate::fields::FpStrategy; use crate::group::Curve; -use crate::{ - fields::FpStrategy, - halo2_proofs::halo2curves::bls12_381::{pairing, Fr as Scalar, G1Affine}, -}; use halo2_base::utils::testing::base_test; use rand::rngs::StdRng; use rand_core::SeedableRng; use serde::{Deserialize, Serialize}; use std::io::Write; +#[cfg(feature = "halo2-axiom")] +pub(crate) use crate::halo2_proofs::halo2curves::bls12_381::{pairing, Fr as Scalar}; +#[cfg(feature = "halo2-pse")] +pub(crate) use halo2curves::bls12_381::{pairing, Fr as Scalar}; + pub mod ec_add; pub mod pairing; diff --git a/halo2-ecc/src/bls12_381/tests/pairing.rs b/halo2-ecc/src/bls12_381/tests/pairing.rs index b46e6037..cc9ffe78 100644 --- a/halo2-ecc/src/bls12_381/tests/pairing.rs +++ b/halo2-ecc/src/bls12_381/tests/pairing.rs @@ -7,10 +7,7 @@ use crate::fields::FieldChip; use super::*; use halo2_base::{ - gates::RangeChip, - halo2_proofs::{arithmetic::Field, halo2curves::bls12_381::G2Affine}, - utils::BigPrimeField, - Context, + gates::RangeChip, halo2_proofs::arithmetic::Field, utils::BigPrimeField, Context, }; use serde::{Deserialize, Serialize}; diff --git a/halo2-ecc/src/bn254/tests/bls_signature.rs b/halo2-ecc/src/bn254/tests/bls_signature.rs index 8475f677..730340d0 100644 --- a/halo2-ecc/src/bn254/tests/bls_signature.rs +++ b/halo2-ecc/src/bn254/tests/bls_signature.rs @@ -15,7 +15,11 @@ use halo2_base::{ Context, }; extern crate pairing; -use pairing::{group::ff::Field, MillerLoopResult}; +use crate::group::ff::Field; +#[cfg(feature = "halo2-pse")] +use halo2_base::halo2_proofs::halo2curves::pairing::MillerLoopResult; +#[cfg(feature = "halo2-axiom")] +use pairing::MillerLoopResult; use rand_core::OsRng; #[derive(Clone, Copy, Debug, Serialize, Deserialize)] diff --git a/halo2-ecc/src/fields/fp12.rs b/halo2-ecc/src/fields/fp12.rs index 64b6a200..8ce8670c 100644 --- a/halo2-ecc/src/fields/fp12.rs +++ b/halo2-ecc/src/fields/fp12.rs @@ -1,5 +1,6 @@ use std::marker::PhantomData; +#[cfg(feature = "halo2-axiom")] use crate::ff::PrimeField as _; use crate::impl_field_ext_chip_common; @@ -252,7 +253,10 @@ mod bn254 { mod bls12_381 { use crate::fields::FieldExtConstructor; + #[cfg(feature = "halo2-axiom")] use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq12, Fq2, Fq6}; + #[cfg(feature = "halo2-pse")] + use halo2curves::bls12_381::{Fq, Fq12, Fq2, Fq6}; // This means we store an Fp12 point as `\sum_{i = 0}^6 (a_{i0} + a_{i1} * u) * w^i` // This is encoded in an FqPoint of degree 12 as `(a_{00}, ..., a_{50}, a_{01}, ..., a_{51})` impl FieldExtConstructor for Fq12 { diff --git a/halo2-ecc/src/fields/fp2.rs b/halo2-ecc/src/fields/fp2.rs index 8068e2f5..37dc1140 100644 --- a/halo2-ecc/src/fields/fp2.rs +++ b/halo2-ecc/src/fields/fp2.rs @@ -1,6 +1,7 @@ use std::fmt::Debug; use std::marker::PhantomData; +#[cfg(feature = "halo2-axiom")] use crate::ff::PrimeField as _; use crate::impl_field_ext_chip_common; @@ -133,7 +134,11 @@ mod bn254 { mod bls12_381 { use crate::fields::FieldExtConstructor; + #[cfg(feature = "halo2-axiom")] use crate::halo2_proofs::halo2curves::bls12_381::{Fq, Fq2}; + #[cfg(feature = "halo2-pse")] + use halo2curves::bls12_381::{Fq, Fq2}; + impl FieldExtConstructor for Fq2 { fn new(c: [Fq; 2]) -> Self { Fq2 { c0: c[0], c1: c[1] } From d1d1b92cf27037d4a217fcefea99114494881f19 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Fri, 5 Jan 2024 18:11:21 +0100 Subject: [PATCH 10/22] optimize final exp --- .../configs/bls12_381/pairing_circuit.config | 2 +- halo2-ecc/src/bls12_381/final_exp.rs | 96 ++++++++++--------- halo2-ecc/src/bls12_381/pairing.rs | 17 +++- halo2-ecc/src/bn254/tests/bls_signature.rs | 11 +-- 4 files changed, 70 insertions(+), 56 deletions(-) diff --git a/halo2-ecc/configs/bls12_381/pairing_circuit.config b/halo2-ecc/configs/bls12_381/pairing_circuit.config index 070e8642..2fc76b22 100644 --- a/halo2-ecc/configs/bls12_381/pairing_circuit.config +++ b/halo2-ecc/configs/bls12_381/pairing_circuit.config @@ -1 +1 @@ -{"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":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":112,"num_limbs":4} diff --git a/halo2-ecc/src/bls12_381/final_exp.rs b/halo2-ecc/src/bls12_381/final_exp.rs index a3608684..630dcc33 100644 --- a/halo2-ecc/src/bls12_381/final_exp.rs +++ b/halo2-ecc/src/bls12_381/final_exp.rs @@ -1,10 +1,7 @@ use super::XI_0; use super::{Fp12Chip, Fp2Chip, FpChip, FqPoint}; -use super::{Fq, Fq12, Fq2, BLS_X, FROBENIUS_COEFF_FQ12_C1}; -use crate::{ - ecc::get_naf, - fields::{fp12::mul_no_carry_w6, vector::FieldVector, FieldChip}, -}; +use super::{Fq, Fq12, Fq2, FROBENIUS_COEFF_FQ12_C1}; +use crate::fields::{fp12::mul_no_carry_w6, vector::FieldVector, FieldChip}; use halo2_base::utils::BigPrimeField; use halo2_base::{gates::GateInstructions, utils::modulus, Context, QuantumCell::Constant}; use num_bigint::BigUint; @@ -59,41 +56,6 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { FieldVector(out_coeffs) } - // exp is in little-endian - /// # Assumptions - /// * `a` is nonzero field point - pub fn pow( - &self, - ctx: &mut Context, - a: &>::FieldPoint, - exp: Vec, - ) -> >::FieldPoint { - let mut res = a.clone(); - let mut is_started = false; - let naf = get_naf(exp); - - for &z in naf.iter().rev() { - if is_started { - res = self.mul(ctx, &res, &res); - } - - if z != 0 { - assert!(z == 1 || z == -1); - if is_started { - res = if z == 1 { - self.mul(ctx, &res, a) - } else { - self.divide_unsafe(ctx, &res, a) - }; - } else { - assert_eq!(z, 1); - is_started = true; - } - } - } - res - } - // assume input is an element of Fp12 in the cyclotomic subgroup GΦ₁₂ // A cyclotomic group is a subgroup of Fp^n defined by // GΦₙ(p) = {α ∈ Fpⁿ : α^{Φₙ(p)} = 1} @@ -258,6 +220,14 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { [h2, h3, h4, h5].into_iter().map(|h| fp2_chip.carry_mod(ctx, h)).collect() } + fn cyclotomic_square_for(&self, ctx: &mut Context, a: &FqPoint, n: usize) -> FqPoint { + let mut tv = self.cyclotomic_compress(a); + for _ in 0..n { + tv = self.cyclotomic_square(ctx, &tv); + } + self.cyclotomic_decompress(ctx, tv) + } + /// # Assumptions /// * `a` is a nonzero element in the cyclotomic subgroup pub fn cyclotomic_pow(&self, ctx: &mut Context, a: FqPoint, exp: u64) -> FqPoint { @@ -280,6 +250,38 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { self.conjugate(ctx, res) } + // Optimized implementation of cyclotomic_pow on BLS_X for BLS12-381 + // Reference: https://github.com/celer-network/brevis-circuits/blob/fe7936f7f/gadgets/pairing_bls12381/tower.go#L801 + fn cyclotomic_pow_bls_x(&self, ctx: &mut Context, a: &FqPoint) -> FqPoint { + let mut tv = self.cyclotomic_compress(a); + for _ in 0..15 { + tv = self.cyclotomic_square(ctx, &tv); + } + let t0 = self.cyclotomic_decompress(ctx, tv.clone()); + + for _ in 0..32 { + tv = self.cyclotomic_square(ctx, &tv); + } + let t1 = self.cyclotomic_decompress(ctx, tv); + + let mut res = self.mul(ctx, &t0, &t1); + let mut t1 = self.cyclotomic_square_for(ctx, &t1, 9); + + res = self.mul(ctx, &res, &t1); + t1 = self.cyclotomic_square_for(ctx, &t1, 3); + + res = self.mul(ctx, &res, &t1); + t1 = self.cyclotomic_square_for(ctx, &t1, 2); + + res = self.mul(ctx, &res, &t1); + t1 = self.cyclotomic_square_for(ctx, &t1, 1); + + res = self.mul(ctx, &res, &t1); + res = self.conjugate(ctx, res); + + self.cyclotomic_square_for(ctx, &res, 1) + } + // out = in^{(q^12 - 1)/r} pub fn final_exp( &self, @@ -292,23 +294,25 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { let f3 = self.frobenius_map(ctx, &f2, 2); let t2 = self.mul(ctx, &f3, &f2); - let t1: FieldVector> = { + let t1 = { let tv = self.cyclotomic_square(ctx, &self.cyclotomic_compress(&t2)); let tv = self.cyclotomic_decompress(ctx, tv); self.conjugate(ctx, tv) }; - let t3 = self.cyclotomic_pow(ctx, t2.clone(), BLS_X); + let t3 = self.cyclotomic_pow_bls_x(ctx, &t2); let t4 = { let tv = self.cyclotomic_square(ctx, &self.cyclotomic_compress(&t3)); self.cyclotomic_decompress(ctx, tv) }; let t5 = self.mul(ctx, &t1, &t3); - let t1 = self.cyclotomic_pow(ctx, t5.clone(), BLS_X); - let t0 = self.cyclotomic_pow(ctx, t1.clone(), BLS_X); - let t6 = self.cyclotomic_pow(ctx, t0.clone(), BLS_X); + let t1 = self.cyclotomic_pow_bls_x(ctx, &t5); + + let t0 = self.cyclotomic_pow_bls_x(ctx, &t1.clone()); + + let t6 = self.cyclotomic_pow_bls_x(ctx, &t0.clone()); let t6 = self.mul(ctx, &t6, &t4); - let t4 = self.cyclotomic_pow(ctx, t6.clone(), BLS_X); + let t4 = self.cyclotomic_pow_bls_x(ctx, &t6.clone()); let t5 = self.conjugate(ctx, t5); let t4 = self.mul(ctx, &t4, &t5); let t4 = self.mul(ctx, &t4, &t2); diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs index bd4ded7d..39e08ed6 100644 --- a/halo2-ecc/src/bls12_381/pairing.rs +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -421,6 +421,18 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { fp12_chip.final_exp(ctx, f0) } + /// Multi-pairing Miller loop + final exponentiation. + pub fn batched_pairing( + &self, + ctx: &mut Context, + pairs: &[(&EcPoint>, &EcPoint>)], + ) -> FqPoint { + let mml = self.multi_miller_loop(ctx, pairs.to_vec()); + let fp12_chip = Fp12Chip::::new(self.fp_chip); + let fe = fp12_chip.final_exp(ctx, mml.clone()); + fe + } + /* * Conducts an efficient pairing check e(P, Q) = e(S, T) using only one * final exponentiation. In particular, this constraints @@ -438,10 +450,9 @@ impl<'chip, F: BigPrimeField> PairingChip<'chip, F> { ) { let ecc_chip_fp = EccChip::new(self.fp_chip); let negated_P = ecc_chip_fp.negate(ctx, P); - let mml = self.multi_miller_loop(ctx, vec![(&negated_P, Q), (S, T)]); + let gt = self.batched_pairing(ctx, &[(&negated_P, Q), (S, T)]); let fp12_chip = Fp12Chip::::new(self.fp_chip); - let fe = fp12_chip.final_exp(ctx, mml); let fp12_one = fp12_chip.load_constant(ctx, Fq12::one()); - fp12_chip.assert_equal(ctx, fe, fp12_one); + fp12_chip.assert_equal(ctx, gt, fp12_one); } } diff --git a/halo2-ecc/src/bn254/tests/bls_signature.rs b/halo2-ecc/src/bn254/tests/bls_signature.rs index de29bb76..bca2635f 100644 --- a/halo2-ecc/src/bn254/tests/bls_signature.rs +++ b/halo2-ecc/src/bn254/tests/bls_signature.rs @@ -4,7 +4,7 @@ use std::{ }; use super::*; -use crate::halo2curves::pairing::{group::ff::Field, MillerLoopResult}; +use crate::group::ff::Field; use crate::{ bn254::bls_signature::BlsSignatureChip, fields::FpStrategy, halo2_proofs::halo2curves::bn256::G2Affine, @@ -15,13 +15,12 @@ use halo2_base::{ utils::BigPrimeField, Context, }; -extern crate pairing; -use crate::group::ff::Field; +use rand_core::OsRng; + +#[cfg(feature = "halo2-axiom")] +use crate::halo2curves::pairing::MillerLoopResult; #[cfg(feature = "halo2-pse")] use halo2_base::halo2_proofs::halo2curves::pairing::MillerLoopResult; -#[cfg(feature = "halo2-axiom")] -use pairing::MillerLoopResult; -use rand_core::OsRng; #[derive(Clone, Copy, Debug, Serialize, Deserialize)] struct BlsSignatureCircuitParams { From b371954ae60da8a783facb86ec68f7bd71294c98 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Fri, 5 Jan 2024 23:45:14 +0100 Subject: [PATCH 11/22] update test config --- halo2-ecc/configs/bls12_381/pairing_circuit.config | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2-ecc/configs/bls12_381/pairing_circuit.config b/halo2-ecc/configs/bls12_381/pairing_circuit.config index 2fc76b22..9a160a5a 100644 --- a/halo2-ecc/configs/bls12_381/pairing_circuit.config +++ b/halo2-ecc/configs/bls12_381/pairing_circuit.config @@ -1 +1 @@ -{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":112,"num_limbs":4} +{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":104,"num_limbs":4} From ae455d8745328e651b6c14e52a23d87eca88ee83 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Mon, 19 Feb 2024 18:38:33 +0100 Subject: [PATCH 12/22] fix bigint for bls12-381 --- .../configs/bls12_381/pairing_circuit.config | 2 +- halo2-ecc/src/bigint/carry_mod.rs | 38 ++++++++++--------- .../src/bigint/check_carry_mod_to_zero.rs | 28 +++++++------- 3 files changed, 35 insertions(+), 33 deletions(-) diff --git a/halo2-ecc/configs/bls12_381/pairing_circuit.config b/halo2-ecc/configs/bls12_381/pairing_circuit.config index 9a160a5a..1baf52d2 100644 --- a/halo2-ecc/configs/bls12_381/pairing_circuit.config +++ b/halo2-ecc/configs/bls12_381/pairing_circuit.config @@ -1 +1 @@ -{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":104,"num_limbs":4} +{"strategy":"Simple","degree":19,"num_advice":6,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":18,"limb_bits":104,"num_limbs":5} diff --git a/halo2-ecc/src/bigint/carry_mod.rs b/halo2-ecc/src/bigint/carry_mod.rs index 0d8ddabd..098659c2 100644 --- a/halo2-ecc/src/bigint/carry_mod.rs +++ b/halo2-ecc/src/bigint/carry_mod.rs @@ -8,7 +8,7 @@ use halo2_base::{ }; use num_bigint::BigInt; use num_integer::Integer; -use num_traits::One; +use num_traits::{One, Signed}; use super::{check_carry_to_zero, CRTInteger, OverflowInteger, ProperCrtUint, ProperUint}; @@ -44,8 +44,7 @@ pub fn crt( let k = a.truncation.limbs.len(); let trunc_len = n * k; - // FIXME: hotfix for BLS12 support - // debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); + debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); // in order for CRT method to work, we need `abs(out + modulus * quotient - a) < 2^{trunc_len - 1} * native_modulus::` // this is ensured if `0 <= out < 2^{n*k}` and @@ -57,12 +56,11 @@ pub fn crt( // 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)} - // FIXME: hotfix for BLS12 support - let _quot_last_limb_bits = 0; //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 @@ -71,8 +69,7 @@ pub fn crt( let (quot_val, out_val) = a.value.div_mod_floor(modulus); debug_assert!(out_val < (BigInt::one() << (n * k))); - // FIXME: hotfix for BLS12 support - // debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); + debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); // decompose_bigint just throws away signed limbs in index >= k let out_vec = decompose_bigint::(&out_val, k, n); @@ -141,19 +138,24 @@ pub fn crt( // 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() { - // FIXME: hotfix for BLS12 support - let limb_bits = if q_index == k - 1 { - /* quot_last_limb_bits */ - n - } 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] }; diff --git a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs index 9659e6d3..26af73af 100644 --- a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs +++ b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs @@ -7,7 +7,7 @@ use halo2_base::{ }; use num_bigint::BigInt; use num_integer::Integer; -use num_traits::One; +use num_traits::{One, Signed, Zero}; use std::{cmp::max, iter}; // same as carry_mod::crt but `out = 0` so no need to range check @@ -29,14 +29,15 @@ pub fn crt( let k = a.truncation.limbs.len(); let trunc_len = n * k; - // FIXME: hotfix for BLS12 support - // debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); + debug_assert!(a.value.bits() as usize <= n * k - 1 + (F::NUM_BITS as usize) - 2); // 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); - // FIXME: hotfix for BLS12 support - let _quot_last_limb_bits = 0; // 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 @@ -46,9 +47,8 @@ pub fn crt( let (quot_val, _out_val) = a.value.div_mod_floor(modulus); // only perform safety checks in debug mode - // FIXME: hotfix for BLS12 support - // debug_assert_eq!(_out_val, BigInt::zero()); - // debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); + debug_assert_eq!(_out_val, BigInt::zero()); + debug_assert!(quot_val.abs() < (BigInt::one() << quot_max_bits)); let quot_vec = decompose_bigint::("_val, k, n); @@ -93,12 +93,12 @@ pub fn crt( // 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() { - // FIXME: hotfix for BLS12 support - let limb_bits = if q_index == k - 1 { - n /* 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] }; From 8b7948296a03d55848fb1c2afaddc4fa848cc2ba Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Tue, 20 Feb 2024 14:51:05 +0100 Subject: [PATCH 13/22] fix build --- rust-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain b/rust-toolchain index 6f6d7b39..1d77724c 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1 +1 @@ -nightly-2023-08-12 +nightly-2023-11-16 From dd8b0d2828785bb041fa6a480734a7b0775d3acb Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Tue, 20 Feb 2024 15:30:32 +0100 Subject: [PATCH 14/22] fix for halo2-pse --- halo2-ecc/Cargo.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/halo2-ecc/Cargo.toml b/halo2-ecc/Cargo.toml index 05bf6e75..fc7d87ca 100644 --- a/halo2-ecc/Cargo.toml +++ b/halo2-ecc/Cargo.toml @@ -27,7 +27,7 @@ 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-axiom = { optional = true } +halo2curves = { package = "halo2curves-axiom", version = "0.5", optional=true } # plotting circuit layout plotters = { version = "0.3.0", optional = true } @@ -46,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", "halo2curves-axiom"] +halo2-pse = ["halo2-base/halo2-pse", "halo2curves"] halo2-axiom = ["halo2-base/halo2-axiom"] jemallocator = ["halo2-base/jemallocator"] mimalloc = ["halo2-base/mimalloc"] From 019edd8f8ce454a80bc89b727cb7357ac992e3bc Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Mon, 15 Apr 2024 12:29:59 +0200 Subject: [PATCH 15/22] fix ec_add test config --- halo2-ecc/configs/bls12_381/ec_add_circuit.config | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2-ecc/configs/bls12_381/ec_add_circuit.config b/halo2-ecc/configs/bls12_381/ec_add_circuit.config index c17d44b9..f5d38d53 100644 --- a/halo2-ecc/configs/bls12_381/ec_add_circuit.config +++ b/halo2-ecc/configs/bls12_381/ec_add_circuit.config @@ -1 +1 @@ -{"strategy":"Simple","degree":17,"num_advice":3,"num_lookup_advice":1,"num_fixed":1,"lookup_bits":16,"limb_bits":120,"num_limbs":4,"batch_size":100} +{"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} From c31c6ebd27f18a9f4d84703c21cc7f365039dc54 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Mon, 22 Apr 2024 12:51:21 +0200 Subject: [PATCH 16/22] format halo-ecc/Cargo.toml --- halo2-ecc/Cargo.toml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/halo2-ecc/Cargo.toml b/halo2-ecc/Cargo.toml index fc7d87ca..9443c872 100644 --- a/halo2-ecc/Cargo.toml +++ b/halo2-ecc/Cargo.toml @@ -27,7 +27,7 @@ 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 } +halo2curves = { package = "halo2curves-axiom", version = "0.5", optional = true } # plotting circuit layout plotters = { version = "0.3.0", optional = true } @@ -37,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" From 5d4857154ac622a775c25d84532e5c1b4c4c4428 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Mon, 22 Apr 2024 14:00:35 +0200 Subject: [PATCH 17/22] refactor: bigprimefield impl into macro --- halo2-base/src/utils/mod.rs | 72 ++++++++++++------------------------- 1 file changed, 22 insertions(+), 50 deletions(-) diff --git a/halo2-base/src/utils/mod.rs b/halo2-base/src/utils/mod.rs index 116459e6..51e5ab33 100644 --- a/halo2-base/src/utils/mod.rs +++ b/halo2-base/src/utils/mod.rs @@ -29,73 +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")] 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_big_prime_field!(Fr, 4); - 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) - } - } + impl_big_prime_field!(Fq, 4); } #[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) - } - } + 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 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) - } - } + 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. From 602413f8b7f4b323de559535abd2fc6efe51168f Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Mon, 22 Apr 2024 17:49:29 +0200 Subject: [PATCH 18/22] generalize carry limbs fix --- halo2-ecc/src/bigint/carry_mod.rs | 34 ++++++++++--------- .../src/bigint/check_carry_mod_to_zero.rs | 21 ++++++------ 2 files changed, 29 insertions(+), 26 deletions(-) diff --git a/halo2-ecc/src/bigint/carry_mod.rs b/halo2-ecc/src/bigint/carry_mod.rs index 098659c2..34b1fea6 100644 --- a/halo2-ecc/src/bigint/carry_mod.rs +++ b/halo2-ecc/src/bigint/carry_mod.rs @@ -57,9 +57,8 @@ pub fn crt( // 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 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; + // 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; // these are witness vectors: @@ -137,25 +136,21 @@ pub fn crt( //} // 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() { - if has_redunant_limb && out_index == k - 1 { - let zero = ctx.load_zero(); - ctx.constrain_equal(out_cell, &zero); - continue; - } + 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() { - 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 }; + 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] }; @@ -164,6 +159,13 @@ pub fn crt( 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), diff --git a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs index 26af73af..a5c417ad 100644 --- a/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs +++ b/halo2-ecc/src/bigint/check_carry_mod_to_zero.rs @@ -34,10 +34,8 @@ pub fn crt( // 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 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; + // 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 @@ -92,12 +90,7 @@ pub fn crt( // } // 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() { - if has_redunant_limb && q_index == k - 1 { - let zero = ctx.load_zero(); - ctx.constrain_equal(quot_cell, &zero); - continue; - } + 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] }; @@ -107,6 +100,14 @@ pub fn crt( 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)); From 1db704abe3e173df61d5a10747842bec89aae231 Mon Sep 17 00:00:00 2001 From: Timofey Luin Date: Mon, 22 Apr 2024 17:49:42 +0200 Subject: [PATCH 19/22] update bench test configs --- .../configs/bls12_381/bench_ec_add.config | 10 +++++----- .../configs/bls12_381/bench_pairing.config | 18 +++++++++--------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/halo2-ecc/configs/bls12_381/bench_ec_add.config b/halo2-ecc/configs/bls12_381/bench_ec_add.config index eccbbd46..a69b5bd3 100644 --- a/halo2-ecc/configs/bls12_381/bench_ec_add.config +++ b/halo2-ecc/configs/bls12_381/bench_ec_add.config @@ -1,5 +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} +{"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} diff --git a/halo2-ecc/configs/bls12_381/bench_pairing.config b/halo2-ecc/configs/bls12_381/bench_pairing.config index 510a0c28..7cffc1a1 100644 --- a/halo2-ecc/configs/bls12_381/bench_pairing.config +++ b/halo2-ecc/configs/bls12_381/bench_pairing.config @@ -1,9 +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} +{"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} From 31ed0f38258a9de625f8eb8d0e1f8ba49c94c912 Mon Sep 17 00:00:00 2001 From: timofey Date: Wed, 15 May 2024 15:14:11 +0200 Subject: [PATCH 20/22] Fix unconstrained constant in final exp (#3) --- halo2-ecc/src/bls12_381/final_exp.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2-ecc/src/bls12_381/final_exp.rs b/halo2-ecc/src/bls12_381/final_exp.rs index 630dcc33..ea76ad69 100644 --- a/halo2-ecc/src/bls12_381/final_exp.rs +++ b/halo2-ecc/src/bls12_381/final_exp.rs @@ -231,7 +231,7 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { /// # Assumptions /// * `a` is a nonzero element in the cyclotomic subgroup pub fn cyclotomic_pow(&self, ctx: &mut Context, a: FqPoint, exp: u64) -> FqPoint { - let mut res = self.load_private(ctx, Fq12::one()); + let mut res = self.load_constant(ctx, Fq12::one()); let mut found_one = false; for bit in (0..64).rev().map(|i| ((exp >> i) & 1) == 1) { From 602417516bc048391a435ee0c14b3dfb8cc5edbf Mon Sep 17 00:00:00 2001 From: timofey Date: Wed, 15 May 2024 15:15:22 +0200 Subject: [PATCH 21/22] Fix line equation formula comment (#6) * fix comment * fix comment line unequal * update comments * fix comment --- halo2-ecc/src/bls12_381/pairing.rs | 25 +++++++++++++------------ halo2-ecc/src/bn254/pairing.rs | 24 ++++++++++++------------ 2 files changed, 25 insertions(+), 24 deletions(-) diff --git a/halo2-ecc/src/bls12_381/pairing.rs b/halo2-ecc/src/bls12_381/pairing.rs index 39e08ed6..16369e07 100644 --- a/halo2-ecc/src/bls12_381/pairing.rs +++ b/halo2-ecc/src/bls12_381/pairing.rs @@ -11,14 +11,14 @@ use crate::{ use halo2_base::utils::BigPrimeField; use halo2_base::Context; +// Assuming curve is of form Y^2 = X^3 + b (a = 0) to save operations // Inputs: -// Q0 = (x_1, y_1) and Q1 = (x_2, y_2) are points in E(Fp2) -// P is point (X, Y) in E(Fp) -// Assuming Q0 != Q1 +// Q = (Q.x, Q.y) is a point in E(Fp) +// P = (x, y) in E(Fp2) // Output: -// line_{Psi(Q0), Psi(Q1)}(P) where Psi(x,y) = (w^2 x, w^3 y) -// - equals w^3 (y_1 - y_2) X + w^2 (x_2 - x_1) Y + w^5 (x_1 y_2 - x_2 y_1) =: out3 * w^3 + out2 * w^2 + out5 * w^5 where out2, out3, out5 are Fp2 points -// Output is [None, None, out2, out3, None, out5] as vector of `Option`s +// line_{Psi(P), Psi(P)}(Q) where Psi(x,y) = (1/w^2 x, 1/w^3 y) +// - equals (3x^3 - 2y^2) + w^2 (-3 x^2 * Q.x) + w^3 (2 y * Q.y) =: out0 + out2 * w^2 + out3 * w^3 where out0, out2, out3 are Fp2 points +// Output is [None, out1, None, out3, out4, None] as vector of `Option`s pub fn sparse_line_function_unequal( fp2_chip: &Fp2Chip, ctx: &mut Context, @@ -40,11 +40,11 @@ pub fn sparse_line_function_unequal( let out3 = fp2_chip.0.fp_mul_no_carry(ctx, y1_minus_y2, X); let out4 = fp2_chip.0.fp_mul_no_carry(ctx, x2_minus_x1, Y); - let out2 = fp2_chip.sub_no_carry(ctx, &x1y2, &x2y1); + let out1 = fp2_chip.sub_no_carry(ctx, &x1y2, &x2y1); // so far we have not "carried mod p" for any of the outputs // we do this below - [None, Some(out2), None, Some(out3), Some(out4), None] + [None, Some(out1), None, Some(out3), Some(out4), None] .into_iter() .map(|option_nc| option_nc.map(|nocarry| fp2_chip.carry_mod(ctx, nocarry))) .collect() @@ -52,11 +52,12 @@ pub fn sparse_line_function_unequal( // Assuming curve is of form Y^2 = X^3 + b (a = 0) to save operations // Inputs: -// Q = (x, y) is a point in E(Fp) -// P = (P.x, P.y) in E(Fp2) +// Q0 = (x_1, y_1) and Q1 = (x_2, y_2) are points in E(Fp2) +// P is point (X, Y) in E(Fp) +// Assuming Q0 != Q1 // Output: -// line_{Psi(Q), Psi(Q)}(P) where Psi(x,y) = (w^2 x, w^3 y) -// - equals (3x^3 - 2y^2)(XI_0 + u) + w^4 (-3 x^2 * Q.x) + w^3 (2 y * Q.y) =: out0 + out4 * w^4 + out3 * w^3 where out0, out3, out4 are Fp2 points +// line_{Psi(Q0), Psi(Q1)}(P) where Psi(x,y) = (1/w^2 x, 1/w^3 y) +// - equals w^3 (y_1 - y_2) X + w^4 (x_2 - x_1) Y + w (x_1 y_2 - x_2 y_1) =: out3 * w^3 + out4 * w^4 + out2 * w where out2, out3, out4 are Fp2 points // Output is [out0, None, out2, out3, None, None] as vector of `Option`s pub fn sparse_line_function_equal( fp2_chip: &Fp2Chip, diff --git a/halo2-ecc/src/bn254/pairing.rs b/halo2-ecc/src/bn254/pairing.rs index dbd7382f..4682df98 100644 --- a/halo2-ecc/src/bn254/pairing.rs +++ b/halo2-ecc/src/bn254/pairing.rs @@ -14,14 +14,14 @@ use halo2_base::Context; const XI_0: i64 = 9; +// Assuming curve is of form Y^2 = X^3 + b (a = 0) to save operations // Inputs: -// Q0 = (x_1, y_1) and Q1 = (x_2, y_2) are points in E(Fp2) -// P is point (X, Y) in E(Fp) -// Assuming Q0 != Q1 +// Q = (x, y) is a point in E(Fp2) +// P = (P.x, P.y) in E(Fp) // Output: -// line_{Psi(Q0), Psi(Q1)}(P) where Psi(x,y) = (w^2 x, w^3 y) -// - equals w^3 (y_1 - y_2) X + w^2 (x_2 - x_1) Y + w^5 (x_1 y_2 - x_2 y_1) =: out3 * w^3 + out2 * w^2 + out5 * w^5 where out2, out3, out5 are Fp2 points -// Output is [None, None, out2, out3, None, out5] as vector of `Option`s +// line_{Psi(Q), Psi(Q)}(P) where Psi(x,y) = (w^2 x, w^3 y) +// - equals (3x^3 - 2y^2)(XI_0 + u) + w^4 (-3 x^2 * Q.x) + w^3 (2 y * Q.y) =: out0 + out4 * w^4 + out3 * w^3 where out0, out3, out4 are Fp2 points +// Output is [out0, None, out2, out3, None, None] as vector of `Option`s pub fn sparse_line_function_unequal( fp2_chip: &Fp2Chip, ctx: &mut Context, @@ -53,14 +53,14 @@ pub fn sparse_line_function_unequal( .collect() } -// Assuming curve is of form Y^2 = X^3 + b (a = 0) to save operations // Inputs: -// Q = (x, y) is a point in E(Fp2) -// P = (P.x, P.y) in E(Fp) +// Q0 = (x_1, y_1) and Q1 = (x_2, y_2) are points in E(Fp2) +// P is point (X, Y) in E(Fp) +// Assuming Q0 != Q1 // Output: -// line_{Psi(Q), Psi(Q)}(P) where Psi(x,y) = (w^2 x, w^3 y) -// - equals (3x^3 - 2y^2)(XI_0 + u) + w^4 (-3 x^2 * Q.x) + w^3 (2 y * Q.y) =: out0 + out4 * w^4 + out3 * w^3 where out0, out3, out4 are Fp2 points -// Output is [out0, None, None, out3, out4, None] as vector of `Option`s +// line_{Psi(Q0), Psi(Q1)}(P) where Psi(x,y) = (w^2 x, w^3 y) +// - equals w^3 (y_1 - y_2) X + w^2 (x_2 - x_1) Y + w^5 (x_1 y_2 - x_2 y_1) =: out3 * w^3 + out2 * w^2 + out5 * w^5 where out2, out3, out5 are Fp2 points +// Output is [None, out2, None, out3, out4, None] as vector of `Option`s pub fn sparse_line_function_equal( fp2_chip: &Fp2Chip, ctx: &mut Context, From 8c6a68ea7672e5cd9dc1ceb2a706e867c7cf9a50 Mon Sep 17 00:00:00 2001 From: timofey Date: Wed, 15 May 2024 15:25:29 +0200 Subject: [PATCH 22/22] Add missing assumption comments (#14) --- halo2-ecc/src/bls12_381/final_exp.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/halo2-ecc/src/bls12_381/final_exp.rs b/halo2-ecc/src/bls12_381/final_exp.rs index ea76ad69..adcbf763 100644 --- a/halo2-ecc/src/bls12_381/final_exp.rs +++ b/halo2-ecc/src/bls12_381/final_exp.rs @@ -59,11 +59,11 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { // assume input is an element of Fp12 in the cyclotomic subgroup GΦ₁₂ // A cyclotomic group is a subgroup of Fp^n defined by // GΦₙ(p) = {α ∈ Fpⁿ : α^{Φₙ(p)} = 1} - + // // below we implement compression and decompression for an element GΦ₁₂ following Theorem 3.1 of https://eprint.iacr.org/2010/542.pdf // Fp4 = Fp2(w^3) where (w^3)^2 = XI_0 +u // Fp12 = Fp4(w) where w^3 = w^3 - + // /// in = g0 + g2 w + g4 w^2 + g1 w^3 + g3 w^4 + g5 w^5 where g_i = g_i0 + g_i1 * u are elements of Fp2 /// out = Compress(in) = [ g2, g3, g4, g5 ] pub fn cyclotomic_compress(&self, a: &FqPoint) -> Vec> { @@ -86,7 +86,9 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { /// g0 = (2 g1^2 + g2 * g5 - 3 g3*g4) * c + 1 /// if g2 = 0: /// g1 = (2 g4 * g5)/g3 - /// g0 = (2 g1^2 - 3 g3 * g4) * c + 1 + /// g0 = (2 g1^2 - 3 g3 * g4) * c + 1 + /// + /// Warning: functions uses `divide_unsafe` so it assumes that value `g2_4`, `g3` are non-zero pub fn cyclotomic_decompress( &self, ctx: &mut Context, @@ -283,6 +285,8 @@ impl<'chip, F: BigPrimeField> Fp12Chip<'chip, F> { } // out = in^{(q^12 - 1)/r} + // + // Assumption: a != 0 pub fn final_exp( &self, ctx: &mut Context,