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 <[email protected]>

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]

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"]

halo2-ecc/src/bn254/tests/ec_add.rs

@@ -39,7 +39,7 @@ fn g2_add_test<F: BigPrimeField>(
     let points =
         _points.iter().map(|pt| g2_chip.assign_point_unchecked(ctx, *pt)).collect::<Vec<_>>();
 
-    let acc = g2_chip.sum::<G2Affine>(ctx, points);
+    let acc = g2_chip.sum_unsafe::<G2Affine>(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<F: BigPrimeField>(
     assert_eq!(answer.y, y);
 }
 
+fn g1_sum_safe_test<F: BigPrimeField>(
+    ctx: &mut Context<F>,
+    range: &RangeChip<F>,
+    params: CircuitParams,
+    _points: Vec<G1Affine>,
+) {
+    let fp_chip = FpChip::<F>::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::<Vec<_>>();
+
+    let acc = g1_chip.sum::<G1Affine>(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<dyn std::error::Error>> {
     let config_path = "configs/bn254/bench_ec_add.config";

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::<GA>(ctx, [u1_mul, u2_mul]);
+    let sum = chip.sum_unsafe::<GA>(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

halo2-ecc/src/ecc/mod.rs

@@ -936,8 +936,18 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> EccChip<'chip, F, FC> {
         EcPoint::new(P.x, self.field_chip.negate(ctx, P.y))
     }
 
+    pub fn negate_strict(
+        &self,
+        ctx: &mut Context<F>,
+        P: impl Into<StrictEcPoint<F, FC>>,
+    ) -> StrictEcPoint<F, FC> {
+        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<F>,
@@ -980,6 +990,19 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> 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<F>,
+        P: EcPoint<F, FC::FieldPoint>,
+    ) -> AssignedValue<F> {
+        // 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<F>,
@@ -990,8 +1013,8 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> 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<C>(
+    /// None of elements in `points` can be point at infinity. Sum cannot be point at infinity either.
+    pub fn sum_unsafe<C>(
         &self,
         ctx: &mut Context<F>,
         points: impl IntoIterator<Item = EcPoint<F, FC::FieldPoint>>,
@@ -1014,6 +1037,35 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> EccChip<'chip, F, FC>
 where
     FC: Selectable<F, FC::FieldPoint>,
 {
+    /// 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<C>(
+        &self,
+        ctx: &mut Context<F>,
+        points: impl IntoIterator<Item = EcPoint<F, FC::FieldPoint>>,
+    ) -> EcPoint<F, FC::FieldPoint>
+    where
+        C: CurveAffineExt<Base = FC::FieldType>,
+    {
+        let rand_point = self.load_random_point::<C>(ctx);
+        let rand_point2 = self.load_random_point::<C>(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<F>,