fix: FieldChip::divide renamed divide_unsafe (#41)

Add `divide` that checks denomintor is nonzero.
Add documentation in cases where `divide_unsafe` is used.

halo2-ecc/src/bn254/final_exp.rs

@@ -68,6 +68,8 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> {
     }
 
     // exp is in little-endian
+    /// # Assumptions
+    /// * `a` is nonzero field point
     pub fn pow(
         &self,
         ctx: &mut Context<F>,
@@ -86,7 +88,11 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> {
             if z != 0 {
                 assert!(z == 1 || z == -1);
                 if is_started {
-                    res = if z == 1 { self.mul(ctx, &res, a) } else { self.divide(ctx, &res, a) };
+                    res = if z == 1 {
+                        self.mul(ctx, &res, a)
+                    } else {
+                        self.divide_unsafe(ctx, &res, a)
+                    };
                 } else {
                     assert_eq!(z, 1);
                     is_started = true;
@@ -148,11 +154,11 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> {
         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(ctx, &g1_num, &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(ctx, &g1_num, &g3);
+        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)`)
@@ -262,6 +268,8 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> {
     }
 
     // exp is in little-endian
+    /// # Assumptions
+    /// * `a` is a nonzero element in the cyclotomic subgroup
     pub fn cyclotomic_pow(
         &self,
         ctx: &mut Context<F>,
@@ -281,7 +289,11 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> {
                 assert!(z == 1 || z == -1);
                 if is_started {
                     let mut res = self.cyclotomic_decompress(ctx, compression);
-                    res = if z == 1 { self.mul(ctx, &res, &a) } else { self.divide(ctx, &res, &a) };
+                    res = if z == 1 {
+                        self.mul(ctx, &res, &a)
+                    } else {
+                        self.divide_unsafe(ctx, &res, &a)
+                    };
                     // compression is free, so it doesn't hurt (except possibly witness generation runtime) to do it
                     // TODO: alternatively we go from small bits to large to avoid this compression
                     compression = self.cyclotomic_compress(&res);
@@ -368,14 +380,16 @@ impl<'chip, F: PrimeField> Fp12Chip<'chip, F> {
     }
 
     // out = in^{ (q^6 - 1)*(q^2 + 1) }
+    /// # Assumptions
+    /// * `a` is nonzero field point
     pub fn easy_part(
         &self,
         ctx: &mut Context<F>,
         a: &<Self as FieldChip<F>>::FieldPoint,
     ) -> <Self as FieldChip<F>>::FieldPoint {
         // a^{q^6} = conjugate of a
         let f1 = self.conjugate(ctx, a);
-        let f2 = self.divide(ctx, &f1, a);
+        let f2 = self.divide_unsafe(ctx, &f1, a);
         let f3 = self.frobenius_map(ctx, &f2, 2);
         self.mul(ctx, &f3, &f2)
     }

halo2-ecc/src/ecc/ecdsa.rs

@@ -36,8 +36,8 @@ where
     let s_valid = scalar_chip.is_soft_nonzero(ctx, s);
 
     // compute u1 = m s^{-1} mod n and u2 = r s^{-1} mod n
-    let u1 = scalar_chip.divide(ctx, msghash, s);
-    let u2 = scalar_chip.divide(ctx, r, s);
+    let u1 = scalar_chip.divide_unsafe(ctx, msghash, s);
+    let u2 = scalar_chip.divide_unsafe(ctx, r, s);
 
     // compute u1 * G and u2 * pubkey
     let u1_mul = fixed_base::scalar_multiply::<F, _, _>(

halo2-ecc/src/ecc/mod.rs

@@ -73,7 +73,7 @@ pub fn ec_add_unequal<F: PrimeField, FC: FieldChip<F>>(
 
     let dx = chip.sub_no_carry(ctx, &Q.x, &P.x);
     let dy = chip.sub_no_carry(ctx, &Q.y, &P.y);
-    let lambda = chip.divide(ctx, &dy, &dx);
+    let lambda = chip.divide_unsafe(ctx, &dy, &dx);
 
     //  x_3 = lambda^2 - x_1 - x_2 (mod p)
     let lambda_sq = chip.mul_no_carry(ctx, &lambda, &lambda);
@@ -116,7 +116,7 @@ pub fn ec_sub_unequal<F: PrimeField, FC: FieldChip<F>>(
     let dx = chip.sub_no_carry(ctx, &Q.x, &P.x);
     let dy = chip.add_no_carry(ctx, &Q.y, &P.y);
 
-    let lambda = chip.neg_divide(ctx, &dy, &dx);
+    let lambda = chip.neg_divide_unsafe(ctx, &dy, &dx);
 
     // (x_2 - x_1) * lambda + y_2 + y_1 = 0 (mod p)
     let lambda_dx = chip.mul_no_carry(ctx, &lambda, &dx);
@@ -159,7 +159,7 @@ pub fn ec_double<F: PrimeField, FC: FieldChip<F>>(
     let two_y = chip.scalar_mul_no_carry(ctx, &P.y, 2);
     let three_x = chip.scalar_mul_no_carry(ctx, &P.x, 3);
     let three_x_sq = chip.mul_no_carry(ctx, &three_x, &P.x);
-    let lambda = chip.divide(ctx, &three_x_sq, &two_y);
+    let lambda = chip.divide_unsafe(ctx, &three_x_sq, &two_y);
 
     // x_3 = lambda^2 - 2 x % p
     let lambda_sq = chip.mul_no_carry(ctx, &lambda, &lambda);
@@ -200,7 +200,7 @@ pub fn ec_double_and_add_unequal<F: PrimeField, FC: FieldChip<F>>(
 
     let dx = chip.sub_no_carry(ctx, &Q.x, &P.x);
     let dy = chip.sub_no_carry(ctx, &Q.y, &P.y);
-    let lambda_0 = chip.divide(ctx, &dy, &dx);
+    let lambda_0 = chip.divide_unsafe(ctx, &dy, &dx);
 
     //  x_2 = lambda_0^2 - x_0 - x_1 (mod p)
     let lambda_0_sq = chip.mul_no_carry(ctx, &lambda_0, &lambda_0);
@@ -217,7 +217,7 @@ pub fn ec_double_and_add_unequal<F: PrimeField, FC: FieldChip<F>>(
     // lambda_1 = lambda_0 + 2 * y_0 / (x_2 - x_0)
     let two_y_0 = chip.scalar_mul_no_carry(ctx, &P.y, 2);
     let x_2_minus_x_0 = chip.sub_no_carry(ctx, &x_2, &P.x);
-    let lambda_1_minus_lambda_0 = chip.divide(ctx, &two_y_0, &x_2_minus_x_0);
+    let lambda_1_minus_lambda_0 = chip.divide_unsafe(ctx, &two_y_0, &x_2_minus_x_0);
     let lambda_1_no_carry = chip.add_no_carry(ctx, &lambda_0, &lambda_1_minus_lambda_0);
 
     // x_res = lambda_1^2 - x_0 - x_2

halo2-ecc/src/fields/fp.rs

@@ -330,6 +330,10 @@ impl<'range, F: PrimeField, Fp: PrimeField> FieldChip<F> for FpChip<'range, F, F
         // self.gate().and(ctx, is_zero, range_check)
     }
 
+    /// Given proper CRT integer `a`, returns 1 iff `a < modulus::<F>()` and `a != 0` as integers
+    ///
+    /// # Assumptions
+    /// * `a` is proper representation of BigUint
     fn is_soft_nonzero(&self, ctx: &mut Context<F>, a: &CRTInteger<F>) -> AssignedValue<F> {
         let is_zero = big_is_zero::crt::<F>(self.gate(), ctx, a);
         let is_nonzero = self.gate().not(ctx, is_zero);

halo2-ecc/src/fields/mod.rs

@@ -1,6 +1,6 @@
 use crate::halo2_proofs::arithmetic::Field;
 use halo2_base::{
-    gates::RangeInstructions,
+    gates::{GateInstructions, RangeInstructions},
     utils::{BigPrimeField, ScalarField},
     AssignedValue, Context,
 };
@@ -162,15 +162,31 @@ pub trait FieldChip<F: PrimeField>: Clone + Debug + Send + Sync {
         self.carry_mod(ctx, &no_carry)
     }
 
+    /// Constrains that `b` is nonzero as a field element and then returns `a / b`.
     fn divide(
         &self,
         ctx: &mut Context<F>,
         a: &Self::FieldPoint,
         b: &Self::FieldPoint,
+    ) -> Self::FieldPoint {
+        let b_is_zero = self.is_zero(ctx, b);
+        self.gate().assert_is_const(ctx, &b_is_zero, &F::zero());
+
+        self.divide_unsafe(ctx, a, b)
+    }
+
+    /// Returns `a / b` without constraining `b` to be nonzero.
+    ///
+    /// Warning: undefined behavior when `b` is zero.
+    fn divide_unsafe(
+        &self,
+        ctx: &mut Context<F>,
+        a: &Self::FieldPoint,
+        b: &Self::FieldPoint,
     ) -> Self::FieldPoint {
         let a_val = self.get_assigned_value(a);
         let b_val = self.get_assigned_value(b);
-        let b_inv = b_val.invert().unwrap();
+        let b_inv: Self::FieldType = Option::from(b_val.invert()).unwrap_or_default();
         let quot_val = a_val * b_inv;
 
         let quot = self.load_private(ctx, Self::fe_to_witness(&quot_val));
@@ -183,17 +199,30 @@ pub trait FieldChip<F: PrimeField>: Clone + Debug + Send + Sync {
         quot
     }
 
-    // constrain and output -a / b
-    // this is usually cheaper constraint-wise than computing -a and then (-a) / b separately
+    /// Constrains that `b` is nonzero as a field element and then returns `-a / b`.
     fn neg_divide(
         &self,
         ctx: &mut Context<F>,
         a: &Self::FieldPoint,
         b: &Self::FieldPoint,
+    ) -> Self::FieldPoint {
+        let b_is_zero = self.is_zero(ctx, b);
+        self.gate().assert_is_const(ctx, &b_is_zero, &F::zero());
+
+        self.neg_divide_unsafe(ctx, a, b)
+    }
+
+    // Returns `-a / b` without constraining `b` to be nonzero.
+    // this is usually cheaper constraint-wise than computing -a and then (-a) / b separately
+    fn neg_divide_unsafe(
+        &self,
+        ctx: &mut Context<F>,
+        a: &Self::FieldPoint,
+        b: &Self::FieldPoint,
     ) -> Self::FieldPoint {
         let a_val = self.get_assigned_value(a);
         let b_val = self.get_assigned_value(b);
-        let b_inv = b_val.invert().unwrap();
+        let b_inv: Self::FieldType = Option::from(b_val.invert()).unwrap_or_default();
         let quot_val = -a_val * b_inv;
 
         let quot = self.load_private(ctx, Self::fe_to_witness(&quot_val));