Add div_add

src/fri/recursive_verifier.rs

@@ -233,8 +233,7 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
             self.sub_extension(single_composition_eval, precomputed_reduced_evals.single);
         // 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);
+        sum = self.div_unsafe_add_extension(single_numerator, vanish_zeta, sum);
         alpha.reset();
 
         // Polynomials opened at `x` and `g x`, i.e., the Zs polynomials.
@@ -268,11 +267,10 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         let zs_numerator = tmp.0;
         let vanish_zeta_right = tmp.1;
         let zs_denominator = self.mul_extension(vanish_zeta, vanish_zeta_right);
+        sum = alpha.shift(sum, self);
         // 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);
+        sum = self.div_unsafe_add_extension(zs_numerator, zs_denominator, sum);
 
         sum
     }

src/gadgets/arithmetic_extension.rs

@@ -575,6 +575,30 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
         quotient
     }
 
+    /// Computes ` x / y + z`.
+    pub fn div_unsafe_add_extension(
+        &mut self,
+        x: ExtensionTarget<D>,
+        y: ExtensionTarget<D>,
+        z: ExtensionTarget<D>,
+    ) -> ExtensionTarget<D> {
+        let zero = self.zero_extension();
+        let one = self.one_extension();
+        let quotient = self.add_virtual_extension_target();
+        self.add_generator(QuotientGeneratorExtension {
+            numerator: x,
+            denominator: y,
+            quotient,
+        });
+
+        // Enforce that q y = x.
+        let (q_y, res) =
+            self.double_arithmetic_extension(F::ONE, F::ONE, quotient, y, zero, one, quotient, z);
+        self.assert_equal_extension(q_y, x);
+
+        res
+    }
+
     /// Computes `1 / x`. Results in an unsatisfiable instance if `x = 0`.
     pub fn inverse_extension(&mut self, x: ExtensionTarget<D>) -> ExtensionTarget<D> {
         let inv = self.add_virtual_extension_target();