@@ -1,6 +1,6 @@
 [package]
 name = "nova-snark"
-version = "0.15.0"
+version = "0.16.0"
 authors = ["Srinath Setty <srinath@microsoft.com>"]
 edition = "2021"
 description = "Recursive zkSNARKs without trusted setup"

@@ -11,7 +11,7 @@ AppendToTranscriptTrait, ChallengeTrait, Group, TranscriptEngineTrait,
   },
   Commitment, CommitmentGens, CompressedCommitment, CE,
 };
-use core::{cmp::max, iter};
+use core::iter;
 use ff::Field;
 use rayon::prelude::*;
 use serde::{Deserialize, Serialize};
@@ -29,7 +29,6 @@ /// Provides an implementation of a polynomial evaluation argument
 #[derive(Clone, Debug, Serialize, Deserialize)]
 #[serde(bound = "")]
 pub struct EvaluationArgument<G: Group> {
-  nifs: Vec<NIFSForInnerProduct<G>>,
   ipa: InnerProductArgument<G>,
 }
 
@@ -55,89 +54,38 @@ gens_s: CommitmentGens::<G>::new(b"ipa", 1),
     }
   }
 
-  fn prove_batch(
+  fn prove(
     gens: &Self::EvaluationGens,
     transcript: &mut G::TE,
-    comms: &[Commitment<G>],
-    polys: &[Vec<G::Scalar>],
-    points: &[Vec<G::Scalar>],
-    evals: &[G::Scalar],
+    comm: &Commitment<G>,
+    poly: &[G::Scalar],
+    point: &[G::Scalar],
+    eval: &G::Scalar,
   ) -> Result<Self::EvaluationArgument, NovaError> {
-    // sanity checks (these should never fail)
-    assert!(polys.len() >= 2);
-    assert_eq!(comms.len(), polys.len());
-    assert_eq!(comms.len(), points.len());
-    assert_eq!(comms.len(), evals.len());
+    let u = InnerProductInstance::new(comm, &EqPolynomial::new(point.to_vec()).evals(), eval);
+    let w = InnerProductWitness::new(poly);
 
-    let mut r_U = InnerProductInstance::new(
-      &comms[0],
-      &EqPolynomial::new(points[0].clone()).evals(),
-      &evals[0],
-    );
-    let mut r_W = InnerProductWitness::new(&polys[0]);
-    let mut nifs = Vec::new();
-
-    for i in 1..polys.len() {
-      let (n, u, w) = NIFSForInnerProduct::prove(
-        &r_U,
-        &r_W,
-        &InnerProductInstance::new(
-          &comms[i],
-          &EqPolynomial::new(points[i].clone()).evals(),
-          &evals[i],
-        ),
-        &InnerProductWitness::new(&polys[i]),
-        transcript,
-      )?;
-      nifs.push(n);
-      r_U = u;
-      r_W = w;
-    }
-
-    let ipa = InnerProductArgument::prove(&gens.gens_v, &gens.gens_s, &r_U, &r_W, transcript)?;
-
-    Ok(EvaluationArgument { nifs, ipa })
+    Ok(EvaluationArgument {
+      ipa: InnerProductArgument::prove(&gens.gens_v, &gens.gens_s, &u, &w, transcript)?,
+    })
   }
 
   /// A method to verify purported evaluations of a batch of polynomials
-  fn verify_batch(
+  fn verify(
     gens: &Self::EvaluationGens,
     transcript: &mut G::TE,
-    comms: &[Commitment<G>],
-    points: &[Vec<G::Scalar>],
-    evals: &[G::Scalar],
+    comm: &Commitment<G>,
+    point: &[G::Scalar],
+    eval: &G::Scalar,
     arg: &Self::EvaluationArgument,
   ) -> Result<(), NovaError> {
-    // sanity checks (these should never fail)
-    assert!(comms.len() >= 2);
-    assert_eq!(comms.len(), points.len());
-    assert_eq!(comms.len(), evals.len());
-
-    let mut r_U = InnerProductInstance::new(
-      &comms[0],
-      &EqPolynomial::new(points[0].clone()).evals(),
-      &evals[0],
-    );
-    let mut num_vars = points[0].len();
-    for i in 1..comms.len() {
-      let u = arg.nifs[i - 1].verify(
-        &r_U,
-        &InnerProductInstance::new(
-          &comms[i],
-          &EqPolynomial::new(points[i].clone()).evals(),
-          &evals[i],
-        ),
-        transcript,
-      )?;
-      r_U = u;
-      num_vars = max(num_vars, points[i].len());
-    }
+    let u = InnerProductInstance::new(comm, &EqPolynomial::new(point.to_vec()).evals(), eval);
 
     arg.ipa.verify(
       &gens.gens_v,
       &gens.gens_s,
-      (2_usize).pow(num_vars as u32),
-      &r_U,
+      (2_usize).pow(point.len() as u32),
+      &u,
       transcript,
     )?;
 
@@ -172,16 +120,6 @@ b_vec: b_vec.to_vec(),
       c: *c,
     }
   }
-
-  fn pad(&self, n: usize) -> InnerProductInstance<G> {
-    let mut b_vec = self.b_vec.clone();
-    b_vec.resize(n, G::Scalar::zero());
-    InnerProductInstance {
-      comm_a_vec: self.comm_a_vec,
-      b_vec,
-      c: self.c,
-    }
-  }
 }
 
 struct InnerProductWitness<G: Group> {
@@ -193,134 +131,6 @@ fn new(a_vec: &[G::Scalar]) -> Self {
     InnerProductWitness {
       a_vec: a_vec.to_vec(),
     }
-  }
-
-  fn pad(&self, n: usize) -> InnerProductWitness<G> {
-    let mut a_vec = self.a_vec.clone();
-    a_vec.resize(n, G::Scalar::zero());
-    InnerProductWitness { a_vec }
-  }
-}
-
-/// A non-interactive folding scheme (NIFS) for inner product relations
-#[derive(Clone, Debug, Serialize, Deserialize)]
-pub struct NIFSForInnerProduct<G: Group> {
-  cross_term: G::Scalar,
-}
-
-impl<G: Group> NIFSForInnerProduct<G> {
-  fn protocol_name() -> &'static [u8] {
-    b"NIFSForInnerProduct"
-  }
-
-  fn prove(
-    U1: &InnerProductInstance<G>,
-    W1: &InnerProductWitness<G>,
-    U2: &InnerProductInstance<G>,
-    W2: &InnerProductWitness<G>,
-    transcript: &mut G::TE,
-  ) -> Result<(Self, InnerProductInstance<G>, InnerProductWitness<G>), NovaError> {
-    transcript.absorb_bytes(b"protocol-name", Self::protocol_name());
-
-    // pad the instances and witness so they are of the same length
-    let U1 = U1.pad(max(U1.b_vec.len(), U2.b_vec.len()));
-    let U2 = U2.pad(max(U1.b_vec.len(), U2.b_vec.len()));
-    let W1 = W1.pad(max(U1.b_vec.len(), U2.b_vec.len()));
-    let W2 = W2.pad(max(U1.b_vec.len(), U2.b_vec.len()));
-
-    // add the two commitments and two public vectors to the transcript
-    // we do not need to add public vectors as their compressed versions were
-    // read from the transcript
-    U1.comm_a_vec
-      .append_to_transcript(b"U1_comm_a_vec", transcript);
-    U2.comm_a_vec
-      .append_to_transcript(b"U2_comm_a_vec", transcript);
-
-    // compute the cross-term
-    let cross_term = inner_product(&W1.a_vec, &U2.b_vec) + inner_product(&W2.a_vec, &U1.b_vec);
-
-    // add the cross-term to the transcript
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &cross_term,
-      b"cross_term",
-      transcript,
-    );
-
-    // obtain a random challenge
-    let r = G::Scalar::challenge(b"r", transcript)?;
-
-    // fold the vectors and their inner product
-    let a_vec = W1
-      .a_vec
-      .par_iter()
-      .zip(W2.a_vec.par_iter())
-      .map(|(x1, x2)| *x1 + r * x2)
-      .collect::<Vec<G::Scalar>>();
-    let b_vec = U1
-      .b_vec
-      .par_iter()
-      .zip(U2.b_vec.par_iter())
-      .map(|(a1, a2)| *a1 + r * a2)
-      .collect::<Vec<G::Scalar>>();
-
-    let c = U1.c + r * r * U2.c + r * cross_term;
-    let comm_a_vec = U1.comm_a_vec + U2.comm_a_vec * r;
-
-    let W = InnerProductWitness { a_vec };
-    let U = InnerProductInstance {
-      comm_a_vec,
-      b_vec,
-      c,
-    };
-
-    Ok((NIFSForInnerProduct { cross_term }, U, W))
-  }
-
-  fn verify(
-    &self,
-    U1: &InnerProductInstance<G>,
-    U2: &InnerProductInstance<G>,
-    transcript: &mut G::TE,
-  ) -> Result<InnerProductInstance<G>, NovaError> {
-    transcript.absorb_bytes(b"protocol-name", Self::protocol_name());
-
-    // pad the instances so they are of the same length
-    let U1 = U1.pad(max(U1.b_vec.len(), U2.b_vec.len()));
-    let U2 = U2.pad(max(U1.b_vec.len(), U2.b_vec.len()));
-
-    // add the two commitments and two public vectors to the transcript
-    // we do not need to add public vectors as their compressed representation
-    // were derived from the transcript
-    U1.comm_a_vec
-      .append_to_transcript(b"U1_comm_a_vec", transcript);
-    U2.comm_a_vec
-      .append_to_transcript(b"U2_comm_a_vec", transcript);
-
-    // add the cross-term to the transcript
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &self.cross_term,
-      b"cross_term",
-      transcript,
-    );
-
-    // obtain a random challenge
-    let r = G::Scalar::challenge(b"r", transcript)?;
-
-    // fold the vectors and their inner product
-    let b_vec = U1
-      .b_vec
-      .par_iter()
-      .zip(U2.b_vec.par_iter())
-      .map(|(a1, a2)| *a1 + r * a2)
-      .collect::<Vec<G::Scalar>>();
-    let c = U1.c + r * r * U2.c + r * self.cross_term;
-    let comm_a_vec = U1.comm_a_vec + U2.comm_a_vec * r;
-
-    Ok(InnerProductInstance {
-      comm_a_vec,
-      b_vec,
-      c,
-    })
   }
 }
 

@@ -63,9 +63,12 @@ #[serde(bound = "")]
 pub struct RelaxedR1CSSNARK<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
   sc_proof_outer: SumcheckProof<G>,
   claims_outer: (G::Scalar, G::Scalar, G::Scalar),
-  sc_proof_inner: SumcheckProof<G>,
   eval_E: G::Scalar,
+  sc_proof_inner: SumcheckProof<G>,
   eval_W: G::Scalar,
+  sc_proof_batch: SumcheckProof<G>,
+  eval_E_prime: G::Scalar,
+  eval_W_prime: G::Scalar,
   eval_arg: EE::EvaluationArgument,
 }
 
@@ -103,7 +106,7 @@ );
 
     // outer sum-check
     let tau = (0..num_rounds_x)
-      .map(|_i| G::Scalar::challenge(b"challenge_tau", &mut transcript))
+      .map(|_i| G::Scalar::challenge(b"tau", &mut transcript))
       .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
 
     let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals());
@@ -140,35 +143,17 @@
     // claims from the end of sum-check
     let (claim_Az, claim_Bz): (G::Scalar, G::Scalar) = (claims_outer[1], claims_outer[2]);
     let claim_Cz = poly_Cz.evaluate(&r_x);
+    let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x);
 
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &claim_Az,
-      b"claim_Az",
-      &mut transcript,
-    );
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &claim_Bz,
-      b"claim_Bz",
-      &mut transcript,
-    );
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &claim_Cz,
-      b"claim_Cz",
-      &mut transcript,
-    );
-
-    let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x);
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &eval_E,
-      b"eval_E",
+    <[G::Scalar] as AppendToTranscriptTrait<G>>::append_to_transcript(
+      &[claim_Az, claim_Bz, claim_Cz, eval_E],
+      b"claims_outer",
       &mut transcript,
     );
 
     // inner sum-check
-    let r_A = G::Scalar::challenge(b"challenge_rA", &mut transcript)?;
-    let r_B = G::Scalar::challenge(b"challenge_rB", &mut transcript)?;
-    let r_C = G::Scalar::challenge(b"challenge_rC", &mut transcript)?;
-    let claim_inner_joint = r_A * claim_Az + r_B * claim_Bz + r_C * claim_Cz;
+    let r = G::Scalar::challenge(b"r", &mut transcript)?;
+    let claim_inner_joint = claim_Az + r * claim_Bz + r * r * claim_Cz;
 
     let poly_ABC = {
       // compute the initial evaluation table for R(\tau, x)
@@ -216,7 +201,7 @@ assert_eq!(evals_A.len(), evals_B.len());
       assert_eq!(evals_A.len(), evals_C.len());
       (0..evals_A.len())
         .into_par_iter()
-        .map(|i| r_A * evals_A[i] + r_B * evals_B[i] + r_C * evals_C[i])
+        .map(|i| evals_A[i] + r * evals_B[i] + r * r * evals_C[i])
         .collect::<Vec<G::Scalar>>()
     };
 
@@ -244,21 +229,63 @@ b"eval_W",
       &mut transcript,
     );
 
-    let eval_arg = EE::prove_batch(
-      &pk.gens,
+    // We will now reduce eval_W =? W(r_y[1..]) and eval_W =? E(r_x) into
+    // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz)
+    // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz),
+    // where gamma is a public challenge
+    // Since commitments to W and E are homomorphic, the verifier can compute a commitment
+    // to the batched polynomial.
+    let rho = G::Scalar::challenge(b"rho", &mut transcript)?;
+
+    let claim_batch_joint = eval_E + rho * eval_W;
+    let num_rounds_z = num_rounds_x;
+    let comb_func =
+      |poly_A_comp: &G::Scalar,
+       poly_B_comp: &G::Scalar,
+       poly_C_comp: &G::Scalar,
+       poly_D_comp: &G::Scalar|
+       -> G::Scalar { *poly_A_comp * *poly_B_comp + rho * *poly_C_comp * *poly_D_comp };
+    let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_sum(
+      &claim_batch_joint,
+      num_rounds_z,
+      &mut MultilinearPolynomial::new(EqPolynomial::new(r_x).evals()),
+      &mut MultilinearPolynomial::new(W.E.clone()),
+      &mut MultilinearPolynomial::new(EqPolynomial::new(r_y[1..].to_vec()).evals()),
+      &mut MultilinearPolynomial::new(W.W.clone()),
+      comb_func,
       &mut transcript,
-      &[U.comm_E, U.comm_W],
-      &[W.E.clone(), W.W.clone()],
-      &[r_x, r_y[1..].to_vec()],
-      &[eval_E, eval_W],
     )?;
+
+    let eval_E_prime = claims_batch[1];
+    let eval_W_prime = claims_batch[3];
+    <[G::Scalar] as AppendToTranscriptTrait<G>>::append_to_transcript(
+      &[eval_E_prime, eval_W_prime],
+      b"claims_batch",
+      &mut transcript,
+    );
+
+    // we now combine evaluation claims at the same point rz into one
+    let gamma = G::Scalar::challenge(b"gamma", &mut transcript)?;
+    let comm = U.comm_E + U.comm_W * gamma;
+    let poly = W
+      .E
+      .iter()
+      .zip(W.W.iter())
+      .map(|(e, w)| *e + gamma * w)
+      .collect::<Vec<G::Scalar>>();
+    let eval = eval_E_prime + gamma * eval_W_prime;
+
+    let eval_arg = EE::prove(&pk.gens, &mut transcript, &comm, &poly, &r_z, &eval)?;
 
     Ok(RelaxedR1CSSNARK {
       sc_proof_outer,
       claims_outer: (claim_Az, claim_Bz, claim_Cz),
+      eval_E,
       sc_proof_inner,
       eval_W,
-      eval_E,
+      sc_proof_batch,
+      eval_E_prime,
+      eval_W_prime,
       eval_arg,
     })
   }
@@ -278,7 +305,7 @@ );
 
     // outer sum-check
     let tau = (0..num_rounds_x)
-      .map(|_i| G::Scalar::challenge(b"challenge_tau", &mut transcript))
+      .map(|_i| G::Scalar::challenge(b"tau", &mut transcript))
       .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
 
     let (claim_outer_final, r_x) =
@@ -295,33 +322,21 @@ if claim_outer_final != claim_outer_final_expected {
       return Err(NovaError::InvalidSumcheckProof);
     }
 
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &self.claims_outer.0,
-      b"claim_Az",
-      &mut transcript,
-    );
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &self.claims_outer.1,
-      b"claim_Bz",
-      &mut transcript,
-    );
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &self.claims_outer.2,
-      b"claim_Cz",
-      &mut transcript,
-    );
-    <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
-      &self.eval_E,
-      b"eval_E",
+    <[G::Scalar] as AppendToTranscriptTrait<G>>::append_to_transcript(
+      &[
+        self.claims_outer.0,
+        self.claims_outer.1,
+        self.claims_outer.2,
+        self.eval_E,
+      ],
+      b"claims_outer",
       &mut transcript,
     );
 
     // inner sum-check
-    let r_A = G::Scalar::challenge(b"challenge_rA", &mut transcript)?;
-    let r_B = G::Scalar::challenge(b"challenge_rB", &mut transcript)?;
-    let r_C = G::Scalar::challenge(b"challenge_rC", &mut transcript)?;
+    let r = G::Scalar::challenge(b"r", &mut transcript)?;
     let claim_inner_joint =
-      r_A * self.claims_outer.0 + r_B * self.claims_outer.1 + r_C * self.claims_outer.2;
+      self.claims_outer.0 + r * self.claims_outer.1 + r * r * self.claims_outer.2;
 
     let (claim_inner_final, r_y) =
       self
@@ -351,11 +366,13 @@ -> (G::Scalar, G::Scalar, G::Scalar) {
       let evaluate_with_table =
         |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar {
           (0..M.len())
-            .map(|i| {
+            .collect::<Vec<usize>>()
+            .par_iter()
+            .map(|&i| {
               let (row, col, val) = M[i];
               T_x[row] * T_y[col] * val
             })
-            .fold(G::Scalar::zero(), |acc, x| acc + x)
+            .reduce(G::Scalar::zero, |acc, x| acc + x)
         };
 
       let T_x = EqPolynomial::new(r_x.to_vec()).evals();
@@ -367,24 +384,55 @@ (eval_A_r, eval_B_r, eval_C_r)
     };
 
     let (eval_A_r, eval_B_r, eval_C_r) = evaluate_as_sparse_polynomial(&vk.S, &r_x, &r_y);
-    let claim_inner_final_expected = (r_A * eval_A_r + r_B * eval_B_r + r_C * eval_C_r) * eval_Z;
+    let claim_inner_final_expected = (eval_A_r + r * eval_B_r + r * r * eval_C_r) * eval_Z;
     if claim_inner_final != claim_inner_final_expected {
       return Err(NovaError::InvalidSumcheckProof);
     }
 
-    // verify eval_W and eval_E
+    // batch sum-check
     <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
       &self.eval_W,
       b"eval_W",
       &mut transcript,
-    ); //eval_E is already in the transcript
+    );
+
+    let rho = G::Scalar::challenge(b"rho", &mut transcript)?;
+    let claim_batch_joint = self.eval_E + rho * self.eval_W;
+    let num_rounds_z = num_rounds_x;
+    let (claim_batch_final, r_z) =
+      self
+        .sc_proof_batch
+        .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?;
+
+    let claim_batch_final_expected = {
+      let poly_rz = EqPolynomial::new(r_z.clone());
+      let rz_rx = poly_rz.evaluate(&r_x);
+      let rz_ry = poly_rz.evaluate(&r_y[1..]);
+      rz_rx * self.eval_E_prime + rho * rz_ry * self.eval_W_prime
+    };
+
+    if claim_batch_final != claim_batch_final_expected {
+      return Err(NovaError::InvalidSumcheckProof);
+    }
+
+    <[G::Scalar] as AppendToTranscriptTrait<G>>::append_to_transcript(
+      &[self.eval_E_prime, self.eval_W_prime],
+      b"claims_batch",
+      &mut transcript,
+    );
 
-    EE::verify_batch(
+    // we now combine evaluation claims at the same point rz into one
+    let gamma = G::Scalar::challenge(b"gamma", &mut transcript)?;
+    let comm = U.comm_E + U.comm_W * gamma;
+    let eval = self.eval_E_prime + gamma * self.eval_W_prime;
+
+    // verify eval_W and eval_E
+    EE::verify(
       &vk.gens,
       &mut transcript,
-      &[U.comm_E, U.comm_W],
-      &[r_x, r_y[1..].to_vec()],
-      &[self.eval_E, self.eval_W],
+      &comm,
+      &r_z,
+      &eval,
       &self.eval_arg,
     )?;
 

@@ -46,7 +46,7 @@ // append the prover's message to the transcript
       poly.append_to_transcript(b"poly", transcript);
 
       //derive the verifier's challenge for the next round
-      let r_i = G::Scalar::challenge(b"challenge_nextround", transcript)?;
+      let r_i = G::Scalar::challenge(b"challenge", transcript)?;
 
       r.push(r_i);
 
@@ -101,7 +101,7 @@ // append the prover's message to the transcript
       poly.append_to_transcript(b"poly", transcript);
 
       //derive the verifier's challenge for the next round
-      let r_i = G::Scalar::challenge(b"challenge_nextround", transcript)?;
+      let r_i = G::Scalar::challenge(b"challenge", transcript)?;
       r.push(r_i);
       polys.push(poly.compress());
 
@@ -122,6 +122,82 @@ vec![poly_A[0], poly_B[0]],
     ))
   }
 
+  pub fn prove_quad_sum<F>(
+    claim: &G::Scalar,
+    num_rounds: usize,
+    poly_A: &mut MultilinearPolynomial<G::Scalar>,
+    poly_B: &mut MultilinearPolynomial<G::Scalar>,
+    poly_C: &mut MultilinearPolynomial<G::Scalar>,
+    poly_D: &mut MultilinearPolynomial<G::Scalar>,
+    comb_func: F,
+    transcript: &mut G::TE,
+  ) -> Result<(Self, Vec<G::Scalar>, Vec<G::Scalar>), NovaError>
+  where
+    F: Fn(&G::Scalar, &G::Scalar, &G::Scalar, &G::Scalar) -> G::Scalar + Sync,
+  {
+    let mut r: Vec<G::Scalar> = Vec::new();
+    let mut polys: Vec<CompressedUniPoly<G>> = Vec::new();
+    let mut claim_per_round = *claim;
+    for _ in 0..num_rounds {
+      let poly = {
+        let len = poly_A.len() / 2;
+
+        // Make an iterator returning the contributions to the evaluations
+        let (eval_point_0, eval_point_2) = (0..len)
+          .into_par_iter()
+          .map(|i| {
+            // eval 0: bound_func is A(low)
+            let eval_point_0 = comb_func(&poly_A[i], &poly_B[i], &poly_C[i], &poly_D[i]);
+
+            // eval 2: bound_func is -A(low) + 2*A(high)
+            let poly_A_bound_point = poly_A[len + i] + poly_A[len + i] - poly_A[i];
+            let poly_B_bound_point = poly_B[len + i] + poly_B[len + i] - poly_B[i];
+            let poly_C_bound_point = poly_C[len + i] + poly_C[len + i] - poly_C[i];
+            let poly_D_bound_point = poly_D[len + i] + poly_D[len + i] - poly_D[i];
+            let eval_point_2 = comb_func(
+              &poly_A_bound_point,
+              &poly_B_bound_point,
+              &poly_C_bound_point,
+              &poly_D_bound_point,
+            );
+            (eval_point_0, eval_point_2)
+          })
+          .reduce(
+            || (G::Scalar::zero(), G::Scalar::zero()),
+            |a, b| (a.0 + b.0, a.1 + b.1),
+          );
+
+        let evals = vec![eval_point_0, claim_per_round - eval_point_0, eval_point_2];
+        UniPoly::from_evals(&evals)
+      };
+
+      // append the prover's message to the transcript
+      poly.append_to_transcript(b"poly", transcript);
+
+      //derive the verifier's challenge for the next round
+      let r_i = G::Scalar::challenge(b"challenge", transcript)?;
+      r.push(r_i);
+      polys.push(poly.compress());
+
+      // Set up next round
+      claim_per_round = poly.evaluate(&r_i);
+
+      // bound all tables to the verifier's challenege
+      poly_A.bound_poly_var_top(&r_i);
+      poly_B.bound_poly_var_top(&r_i);
+      poly_C.bound_poly_var_top(&r_i);
+      poly_D.bound_poly_var_top(&r_i);
+    }
+
+    Ok((
+      SumcheckProof {
+        compressed_polys: polys,
+      },
+      r,
+      vec![poly_A[0], poly_B[0], poly_C[0], poly_D[0]],
+    ))
+  }
+
   pub fn prove_cubic_with_additive_term<F>(
     claim: &G::Scalar,
     num_rounds: usize,
@@ -193,7 +269,7 @@ // append the prover's message to the transcript
       poly.append_to_transcript(b"poly", transcript);
 
       //derive the verifier's challenge for the next round
-      let r_i = G::Scalar::challenge(b"challenge_nextround", transcript)?;
+      let r_i = G::Scalar::challenge(b"challenge", transcript)?;
       r.push(r_i);
       polys.push(poly.compress());
 

@@ -23,23 +23,23 @@
   /// A method to perform any additional setup needed to produce proofs of evaluations
   fn setup(gens: &<Self::CE as CommitmentEngineTrait<G>>::CommitmentGens) -> Self::EvaluationGens;
 
-  /// A method to prove evaluations of a batch of polynomials
-  fn prove_batch(
+  /// A method to prove the evaluation of a multilinear polynomial
+  fn prove(
     gens: &Self::EvaluationGens,
     transcript: &mut G::TE,
-    comm: &[<Self::CE as CommitmentEngineTrait<G>>::Commitment],
-    polys: &[Vec<G::Scalar>],
-    points: &[Vec<G::Scalar>],
-    evals: &[G::Scalar],
+    comm: &<Self::CE as CommitmentEngineTrait<G>>::Commitment,
+    poly: &[G::Scalar],
+    point: &[G::Scalar],
+    eval: &G::Scalar,
   ) -> Result<Self::EvaluationArgument, NovaError>;
 
-  /// A method to verify purported evaluations of a batch of polynomials
-  fn verify_batch(
+  /// A method to verify the purported evaluation of a multilinear polynomials
+  fn verify(
     gens: &Self::EvaluationGens,
     transcript: &mut G::TE,
-    comm: &[<Self::CE as CommitmentEngineTrait<G>>::Commitment],
-    points: &[Vec<G::Scalar>],
-    evals: &[G::Scalar],
+    comm: &<Self::CE as CommitmentEngineTrait<G>>::Commitment,
+    point: &[G::Scalar],
+    eval: &G::Scalar,
     arg: &Self::EvaluationArgument,
   ) -> Result<(), NovaError>;
 }