From d23968cd00a0a0bbfe78f8bdaa83107749c51d85 Mon Sep 17 00:00:00 2001 From: MonkeyKing-1 <67293785+MonkeyKing-1@users.noreply.github.com> Date: Tue, 9 Apr 2024 09:21:20 -0400 Subject: [PATCH] feat: safe ecc_sum and tests (#244) * feat: safe ecc_sum and tests * fix clippy + rename functions * remove unnecessary .into() * feat: add comments, remove extraneous, optimize is_inf * chore: fix `clap` version in dev-dependency to prevent rustc version issues * chore: remove unused variable --------- Co-authored-by: Jonathan Wang <31040440+jonathanpwang@users.noreply.github.com> --- halo2-base/Cargo.toml | 3 ++ halo2-ecc/Cargo.toml | 3 ++ halo2-ecc/src/bn254/tests/ec_add.rs | 57 ++++++++++++++++++++++++++++- halo2-ecc/src/ecc/ecdsa.rs | 2 +- halo2-ecc/src/ecc/mod.rs | 56 +++++++++++++++++++++++++++- 5 files changed, 117 insertions(+), 4 deletions(-) diff --git a/halo2-base/Cargo.toml b/halo2-base/Cargo.toml index fe3788c0..500107b3 100644 --- a/halo2-base/Cargo.toml +++ b/halo2-base/Cargo.toml @@ -49,6 +49,9 @@ env_logger = "0.10.0" proptest = "1.1.0" # native poseidon for testing pse-poseidon = { git = "https://github.com/axiom-crypto/pse-poseidon.git" } +clap = "=4.4" # fix clap version to prevent requiring rustc 1.74 +clap_builder = "=4.4" +clap_lex = "=0.6.0" # memory allocation [target.'cfg(not(target_env = "msvc"))'.dependencies] diff --git a/halo2-ecc/Cargo.toml b/halo2-ecc/Cargo.toml index 9eb79e86..2ac86f57 100644 --- a/halo2-ecc/Cargo.toml +++ b/halo2-ecc/Cargo.toml @@ -35,6 +35,9 @@ criterion-macro = "0.4" halo2-base = { version = "0.4.2-alpha", path = "../halo2-base", default-features = false, features = ["test-utils"] } test-log = "0.2.12" env_logger = "0.10.0" +clap = "=4.4" # fix clap version to prevent requiring rustc 1.74 +clap_builder = "=4.4" +clap_lex = "=0.6.0" [features] default = ["jemallocator", "halo2-axiom", "display"] diff --git a/halo2-ecc/src/bn254/tests/ec_add.rs b/halo2-ecc/src/bn254/tests/ec_add.rs index 1df235f1..67edd936 100644 --- a/halo2-ecc/src/bn254/tests/ec_add.rs +++ b/halo2-ecc/src/bn254/tests/ec_add.rs @@ -39,7 +39,7 @@ fn g2_add_test( let points = _points.iter().map(|pt| g2_chip.assign_point_unchecked(ctx, *pt)).collect::>(); - let acc = g2_chip.sum::(ctx, points); + let acc = g2_chip.sum_unsafe::(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()); @@ -48,6 +48,27 @@ fn g2_add_test( assert_eq!(answer.y, y); } +fn g1_sum_safe_test( + ctx: &mut Context, + range: &RangeChip, + params: CircuitParams, + _points: Vec, +) { + let fp_chip = FpChip::::new(range, params.limb_bits, params.num_limbs); + let g1_chip = EccChip::new(&fp_chip); + + let points = + _points.iter().map(|pt| g1_chip.assign_point_unchecked(ctx, *pt)).collect::>(); + + let acc = g1_chip.sum::(ctx, points); + + let answer = _points.iter().fold(G1Affine::identity(), |a, b| (a + b).to_affine()); + let x = fp_chip.get_assigned_value(&acc.x.into()); + let y = fp_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/bn254/ec_add_circuit.config"; @@ -65,6 +86,40 @@ fn test_ec_add() { .run(|ctx, range| g2_add_test(ctx, range, params, points)); } +#[test] +fn test_ec_sum_safe() { + let path = "configs/bn254/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(|_| G1Affine::random(OsRng)).collect_vec(); + + base_test() + .k(k) + .lookup_bits(params.lookup_bits) + .run(|ctx, range| g1_sum_safe_test(ctx, range, params, points)); +} + +#[test] +fn test_ec_zero_sum_safe() { + let path = "configs/bn254/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(|_| G1Affine::identity()).collect_vec(); + + base_test() + .k(k) + .lookup_bits(params.lookup_bits) + .run(|ctx, range| g1_sum_safe_test(ctx, range, params, points)); +} + #[test] fn bench_ec_add() -> Result<(), Box> { let config_path = "configs/bn254/bench_ec_add.config"; diff --git a/halo2-ecc/src/ecc/ecdsa.rs b/halo2-ecc/src/ecc/ecdsa.rs index c72b3974..798c6893 100644 --- a/halo2-ecc/src/ecc/ecdsa.rs +++ b/halo2-ecc/src/ecc/ecdsa.rs @@ -71,7 +71,7 @@ where // compute (x1, y1) = u1 * G + u2 * pubkey and check (r mod n) == x1 as integers // because it is possible for u1 * G == u2 * pubkey, we must use `EccChip::sum` - let sum = chip.sum::(ctx, [u1_mul, u2_mul]); + let sum = chip.sum_unsafe::(ctx, [u1_mul, u2_mul]); // WARNING: For optimization reasons, does not reduce x1 mod n, which is // invalid unless p is very close to n in size. // enforce x1 < n diff --git a/halo2-ecc/src/ecc/mod.rs b/halo2-ecc/src/ecc/mod.rs index 14bd0911..bef0ac15 100644 --- a/halo2-ecc/src/ecc/mod.rs +++ b/halo2-ecc/src/ecc/mod.rs @@ -936,8 +936,18 @@ impl<'chip, F: BigPrimeField, FC: FieldChip> EccChip<'chip, F, FC> { EcPoint::new(P.x, self.field_chip.negate(ctx, P.y)) } + pub fn negate_strict( + &self, + ctx: &mut Context, + P: impl Into>, + ) -> StrictEcPoint { + let P = P.into(); + StrictEcPoint::new(P.x, self.field_chip.negate(ctx, P.y)) + } + /// Assumes that P.x != Q.x /// If `is_strict == true`, then actually constrains that `P.x != Q.x` + /// Neither are points at infinity (otherwise, undefined behavior) pub fn add_unequal( &self, ctx: &mut Context, @@ -980,6 +990,19 @@ impl<'chip, F: BigPrimeField, FC: FieldChip> EccChip<'chip, F, FC> { self.field_chip.range().gate().and(ctx, x_is_equal, y_is_equal) } + /// Checks if a point is the point at infinity (represented by (0, 0)) + /// Assumes points at infinity are always serialized as (0, 0) as bigints + pub fn is_infinity( + &self, + ctx: &mut Context, + P: EcPoint, + ) -> AssignedValue { + // TODO: optimize + let x_is_zero = self.field_chip.is_soft_zero(ctx, P.x); + let y_is_zero = self.field_chip.is_soft_zero(ctx, P.y); + self.field_chip.range().gate().and(ctx, x_is_zero, y_is_zero) + } + pub fn assert_equal( &self, ctx: &mut Context, @@ -990,8 +1013,8 @@ impl<'chip, F: BigPrimeField, FC: FieldChip> EccChip<'chip, F, FC> { self.field_chip.assert_equal(ctx, P.y, Q.y); } - /// None of elements in `points` can be point at infinity. - pub fn sum( + /// None of elements in `points` can be point at infinity. Sum cannot be point at infinity either. + pub fn sum_unsafe( &self, ctx: &mut Context, points: impl IntoIterator>, @@ -1014,6 +1037,35 @@ impl<'chip, F: BigPrimeField, FC: FieldChip> EccChip<'chip, F, FC> where FC: Selectable, { + /// Expensive version of `sum_unsafe`, but works generally meaning that + /// * sum can be the point at infinity + /// * addends can be points at infinity + pub fn sum( + &self, + ctx: &mut Context, + points: impl IntoIterator>, + ) -> EcPoint + where + C: CurveAffineExt, + { + let rand_point = self.load_random_point::(ctx); + let rand_point2 = self.load_random_point::(ctx); + let neg_rand_point = self.negate(ctx, rand_point.clone()); + let mut acc = ComparableEcPoint::from(neg_rand_point.clone()); + for point in points { + let point_is_inf = self.is_infinity(ctx, point.clone()); + let addend = self.select(ctx, rand_point2.clone(), point.clone(), point_is_inf); + let _acc = self.add_unequal(ctx, acc.clone(), addend.clone(), true); + let _acc = self.select(ctx, acc.clone().into(), _acc, point_is_inf); + acc = _acc.into(); + } + let acc_is_neg_rand = self.is_equal(ctx, acc.clone().into(), neg_rand_point); + let addend = self.select(ctx, rand_point2.clone(), acc.clone().into(), acc_is_neg_rand); + let sum = self.add_unequal(ctx, addend, rand_point, true); + let inf = self.load_private_unchecked(ctx, (FC::FieldType::ZERO, FC::FieldType::ZERO)); + self.select(ctx, inf, sum, acc_is_neg_rand) + } + pub fn select( &self, ctx: &mut Context,