From 5f79b9630e7ab42f19feff1e26d11ba758462d1c Mon Sep 17 00:00:00 2001 From: Daniel Lubarov Date: Wed, 28 Jul 2021 18:06:32 -0700 Subject: [PATCH] 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 | 11 +++++++---- src/gadgets/interpolation.rs | 2 +- src/plonk_common.rs | 4 ++++ src/vanishing_poly.rs | 5 ++++- 4 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/fri/recursive_verifier.rs b/src/fri/recursive_verifier.rs index 0c256ae8..f80f156c 100644 --- a/src/fri/recursive_verifier.rs +++ b/src/fri/recursive_verifier.rs @@ -194,6 +194,8 @@ impl, const D: usize> CircuitBuilder { 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, const D: usize> CircuitBuilder { 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, const D: usize> CircuitBuilder { 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); diff --git a/src/gadgets/interpolation.rs b/src/gadgets/interpolation.rs index 5de2c651..72119354 100644 --- a/src/gadgets/interpolation.rs +++ b/src/gadgets/interpolation.rs @@ -19,7 +19,7 @@ impl, const D: usize> CircuitBuilder { 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) } diff --git a/src/plonk_common.rs b/src/plonk_common.rs index 595fed91..9caf3746 100644 --- a/src/plonk_common.rs +++ b/src/plonk_common.rs @@ -119,6 +119,10 @@ pub(crate) fn eval_l_1(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, const D: usize>( builder: &mut CircuitBuilder, n: usize, diff --git a/src/vanishing_poly.rs b/src/vanishing_poly.rs index 6101a9fb..8e6d50d5 100644 --- a/src/vanishing_poly.rs +++ b/src/vanishing_poly.rs @@ -253,6 +253,9 @@ pub fn evaluate_gate_constraints_recursively, 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, const D: usize>( builder: &mut CircuitBuilder, common_data: &CommonCircuitData, @@ -314,7 +317,7 @@ pub(crate) fn eval_vanishing_poly_recursively, const D: usize>( }) .collect::>(); 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::>(); // The partial products considered for this iteration of `i`.