feat: safe ecc_sum and tests

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

@@ -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_safe::<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/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,18 @@ 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))
+    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_zero(ctx, P.x);
+        let y_is_zero = self.field_chip.is_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>,
@@ -1014,6 +1036,36 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> EccChip<'chip, F, FC>
 where
     FC: Selectable<F, FC::FieldPoint>,
 {
+    pub fn sum_safe<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 zero = ctx.load_constant(F::ZERO);
+        let rand_point = into_strict_point(self.field_chip, ctx, rand_point);
+        let neg_rand_point = self.negate_strict(ctx, rand_point.clone());
+        let mut acc = StrictEcPoint::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 = into_strict_point(self.field_chip, ctx, _acc);
+            let acc_is_inf = self.is_infinity(ctx, acc.clone().into());
+            ctx.constrain_equal(&acc_is_inf, &zero);
+        }
+        let acc_is_neg_rand = self.is_equal(ctx, acc.clone().into(), neg_rand_point.into());
+        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>,