Update division calls (#132)

We have two division methods: one "unsafe" one, which permits 0/0 = anything, and one "safe" one, for which 0/0 results in an unsatisfiable instance. The latter is slightly more expensive.

I switched a few calls over to safe division, where unsafe division didn't seem sound (or at least it wasn't obvious). For calls where unsafe division did seem sound, I added comments explaining why.

Closes #97.

src/fri/recursive_verifier.rs

@@ -194,6 +194,8 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         let config = self.config.clone();
         let degree_log = proof.evals_proofs[0].1.siblings.len() - config.rate_bits;
         let subgroup_x = self.convert_to_ext(subgroup_x);
+        let vanish_zeta = self.sub_extension(subgroup_x, zeta);
+        let vanish_zeta_right = self.sub_extension(subgroup_x, zeta_right);
         let mut alpha = ReducingFactorTarget::new(alpha);
         let mut sum = self.zero_extension();
 
@@ -218,8 +220,9 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         let single_composition_eval = alpha.reduce_base(&single_evals, self);
         let single_numerator =
             self.sub_extension(single_composition_eval, precomputed_reduced_evals.single);
-        let single_denominator = self.sub_extension(subgroup_x, zeta);
-        let quotient = self.div_unsafe_extension(single_numerator, single_denominator);
+        // This division is safe because the denominator will be nonzero unless zeta is in the
+        // codeword domain, which occurs with negligible probability given a large extension field.
+        let quotient = self.div_unsafe_extension(single_numerator, vanish_zeta);
         sum = self.add_extension(sum, quotient);
         alpha.reset();
 
@@ -242,9 +245,9 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
             subgroup_x,
         );
         let zs_numerator = self.sub_extension(zs_composition_eval, interpol_val);
-        let vanish_zeta = self.sub_extension(subgroup_x, zeta);
-        let vanish_zeta_right = self.sub_extension(subgroup_x, zeta_right);
         let zs_denominator = self.mul_extension(vanish_zeta, vanish_zeta_right);
+        // This division is safe because the denominator will be nonzero unless zeta is in the
+        // codeword domain, which occurs with negligible probability given a large extension field.
         let zs_quotient = self.div_unsafe_extension(zs_numerator, zs_denominator);
         sum = alpha.shift(sum, self);
         sum = self.add_extension(sum, zs_quotient);

src/gadgets/interpolation.rs

@@ -19,7 +19,7 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         let x_m_a0 = self.sub_extension(evaluation_point, interpolation_points[0].0);
         let b1_m_a1 = self.sub_extension(interpolation_points[1].1, interpolation_points[0].1);
         let b0_m_a0 = self.sub_extension(interpolation_points[1].0, interpolation_points[0].0);
-        let quotient = self.div_unsafe_extension(b1_m_a1, b0_m_a0);
+        let quotient = self.div_extension(b1_m_a1, b0_m_a0);
 
         self.mul_add_extension(x_m_a0, quotient, interpolation_points[0].1)
     }

src/plonk_common.rs

@@ -119,6 +119,10 @@ pub(crate) fn eval_l_1<F: Field>(n: usize, x: F) -> F {
     eval_zero_poly(n, x) / (F::from_canonical_usize(n) * (x - F::ONE))
 }
 
+/// Evaluates the Lagrange basis L_1(x), which has L_1(1) = 1 and vanishes at all other points in
+/// the order-`n` subgroup.
+///
+/// Assumes `x != 1`; if `x` could be 1 then this is unsound.
 pub(crate) fn eval_l_1_recursively<F: Extendable<D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
     n: usize,

src/vanishing_poly.rs

@@ -253,6 +253,9 @@ pub fn evaluate_gate_constraints_recursively<F: Extendable<D>, const D: usize>(
 /// Evaluate the vanishing polynomial at `x`. In this context, the vanishing polynomial is a random
 /// linear combination of gate constraints, plus some other terms relating to the permutation
 /// argument. All such terms should vanish on `H`.
+///
+/// Assumes `x != 1`; if `x` could be 1 then this is unsound. This is fine if `x` is a random
+/// variable drawn from a sufficiently large domain.
 pub(crate) fn eval_vanishing_poly_recursively<F: Extendable<D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
     common_data: &CommonCircuitData<F, D>,
@@ -314,7 +317,7 @@ pub(crate) fn eval_vanishing_poly_recursively<F: Extendable<D>, const D: usize>(
             })
             .collect::<Vec<_>>();
         let quotient_values = (0..common_data.config.num_routed_wires)
-            .map(|j| builder.div_unsafe_extension(numerator_values[j], denominator_values[j]))
+            .map(|j| builder.div_extension(numerator_values[j], denominator_values[j]))
             .collect::<Vec<_>>();
 
         // The partial products considered for this iteration of `i`.