From ff68b66bbbeec48e770e9d75503f9252429281d1 Mon Sep 17 00:00:00 2001
From: wborgeaud <williamborgeaud@gmail.com>
Date: Mon, 9 Aug 2021 13:46:20 +0200
Subject: [PATCH] Add `div_add`

---
 src/fri/recursive_verifier.rs       |  8 +++-----
 src/gadgets/arithmetic_extension.rs | 24 ++++++++++++++++++++++++
 2 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/src/fri/recursive_verifier.rs b/src/fri/recursive_verifier.rs
index a0937554..a179cf2b 100644
--- a/src/fri/recursive_verifier.rs
+++ b/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
     }
diff --git a/src/gadgets/arithmetic_extension.rs b/src/gadgets/arithmetic_extension.rs
index 3a494cbc..608a412c 100644
--- a/src/gadgets/arithmetic_extension.rs
+++ b/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();