Reorganize various Spartan SNARKs and make the direct interface more generic (#195)

* reorganize different variants of spartan and make direct snark more generic

* cargo fmt

benches/compressed-snark.rs

@@ -17,8 +17,8 @@ type G1 = pasta_curves::pallas::Point;
 type G2 = pasta_curves::vesta::Point;
 type EE1 = nova_snark::provider::ipa_pc::EvaluationEngine<G1>;
 type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine<G2>;
-type S1 = nova_snark::spartan::RelaxedR1CSSNARK<G1, EE1>;
+type S1 = nova_snark::spartan::snark::RelaxedR1CSSNARK<G1, EE1>;
-type S2 = nova_snark::spartan::RelaxedR1CSSNARK<G2, EE2>;
+type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK<G2, EE2>;
 type C1 = NonTrivialTestCircuit<<G1 as Group>::Scalar>;
 type C2 = TrivialTestCircuit<<G2 as Group>::Scalar>;
 

examples/minroot.rs

@@ -262,8 +262,8 @@ fn main() {
     let start = Instant::now();
     type EE1 = nova_snark::provider::ipa_pc::EvaluationEngine<G1>;
     type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine<G2>;
-    type S1 = nova_snark::spartan::RelaxedR1CSSNARK<G1, EE1>;
+    type S1 = nova_snark::spartan::snark::RelaxedR1CSSNARK<G1, EE1>;
-    type S2 = nova_snark::spartan::RelaxedR1CSSNARK<G2, EE2>;
+    type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK<G2, EE2>;
 
     let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &pk, &recursive_snark);
     println!(

src/lib.rs

@@ -799,10 +799,10 @@ mod tests {
   use super::*;
   type EE1<G1> = provider::ipa_pc::EvaluationEngine<G1>;
   type EE2<G2> = provider::ipa_pc::EvaluationEngine<G2>;
-  type S1<G1> = spartan::RelaxedR1CSSNARK<G1, EE1<G1>>;
+  type S1<G1> = spartan::snark::RelaxedR1CSSNARK<G1, EE1<G1>>;
-  type S2<G2> = spartan::RelaxedR1CSSNARK<G2, EE2<G2>>;
+  type S2<G2> = spartan::snark::RelaxedR1CSSNARK<G2, EE2<G2>>;
-  type S1Prime<G1> = spartan::pp::RelaxedR1CSSNARK<G1, EE1<G1>>;
+  type S1Prime<G1> = spartan::ppsnark::RelaxedR1CSSNARK<G1, EE1<G1>>;
-  type S2Prime<G2> = spartan::pp::RelaxedR1CSSNARK<G2, EE2<G2>>;
+  type S2Prime<G2> = spartan::ppsnark::RelaxedR1CSSNARK<G2, EE2<G2>>;
 
   use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
   use core::marker::PhantomData;

src/spartan/direct.rs

@@ -0,0 +1,265 @@
+//! This module provides interfaces to directly prove a step circuit by using Spartan SNARK.
+//! In particular, it supports any SNARK that implements RelaxedR1CSSNARK trait
+//! (e.g., with the SNARKs implemented in ppsnark.rs or snark.rs).
+use crate::{
+  bellperson::{
+    r1cs::{NovaShape, NovaWitness},
+    shape_cs::ShapeCS,
+    solver::SatisfyingAssignment,
+  },
+  errors::NovaError,
+  r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
+  traits::{circuit::StepCircuit, snark::RelaxedR1CSSNARKTrait, Group},
+  Commitment, CommitmentKey,
+};
+use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError};
+use core::marker::PhantomData;
+use ff::Field;
+use serde::{Deserialize, Serialize};
+
+struct DirectCircuit<G: Group, SC: StepCircuit<G::Scalar>> {
+  z_i: Option<Vec<G::Scalar>>, // inputs to the circuit
+  sc: SC,                      // step circuit to be executed
+}
+
+impl<G: Group, SC: StepCircuit<G::Scalar>> Circuit<G::Scalar> for DirectCircuit<G, SC> {
+  fn synthesize<CS: ConstraintSystem<G::Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
+    // obtain the arity information
+    let arity = self.sc.arity();
+
+    // Allocate zi. If inputs.zi is not provided, allocate default value 0
+    let zero = vec![G::Scalar::ZERO; arity];
+    let z_i = (0..arity)
+      .map(|i| {
+        AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || {
+          Ok(self.z_i.as_ref().unwrap_or(&zero)[i])
+        })
+      })
+      .collect::<Result<Vec<AllocatedNum<G::Scalar>>, _>>()?;
+
+    let z_i_plus_one = self.sc.synthesize(&mut cs.namespace(|| "F"), &z_i)?;
+
+    // inputize both z_i and z_i_plus_one
+    for (j, input) in z_i.iter().enumerate().take(arity) {
+      let _ = input.inputize(cs.namespace(|| format!("input {j}")));
+    }
+    for (j, output) in z_i_plus_one.iter().enumerate().take(arity) {
+      let _ = output.inputize(cs.namespace(|| format!("output {j}")));
+    }
+
+    Ok(())
+  }
+}
+
+/// A type that holds the prover key
+#[derive(Clone, Serialize, Deserialize)]
+#[serde(bound = "")]
+pub struct ProverKey<G, S>
+where
+  G: Group,
+  S: RelaxedR1CSSNARKTrait<G>,
+{
+  S: R1CSShape<G>,
+  ck: CommitmentKey<G>,
+  pk: S::ProverKey,
+}
+
+/// A type that holds the verifier key
+#[derive(Clone, Serialize, Deserialize)]
+#[serde(bound = "")]
+pub struct VerifierKey<G, S>
+where
+  G: Group,
+  S: RelaxedR1CSSNARKTrait<G>,
+{
+  vk: S::VerifierKey,
+}
+
+/// A direct SNARK proving a step circuit
+#[derive(Clone, Serialize, Deserialize)]
+#[serde(bound = "")]
+pub struct DirectSNARK<G, S, C>
+where
+  G: Group,
+  S: RelaxedR1CSSNARKTrait<G>,
+  C: StepCircuit<G::Scalar>,
+{
+  comm_W: Commitment<G>, // commitment to the witness
+  snark: S,              // snark proving the witness is satisfying
+  _p: PhantomData<C>,
+}
+
+impl<G: Group, S: RelaxedR1CSSNARKTrait<G>, C: StepCircuit<G::Scalar>> DirectSNARK<G, S, C> {
+  /// Produces prover and verifier keys for the direct SNARK
+  pub fn setup(sc: C) -> Result<(ProverKey<G, S>, VerifierKey<G, S>), NovaError> {
+    // construct a circuit that can be synthesized
+    let circuit: DirectCircuit<G, C> = DirectCircuit { z_i: None, sc };
+
+    let mut cs: ShapeCS<G> = ShapeCS::new();
+    let _ = circuit.synthesize(&mut cs);
+    let (shape, ck) = cs.r1cs_shape();
+
+    let (pk, vk) = S::setup(&ck, &shape)?;
+
+    let pk = ProverKey { S: shape, ck, pk };
+
+    let vk = VerifierKey { vk };
+
+    Ok((pk, vk))
+  }
+
+  /// Produces a proof of satisfiability of the provided circuit
+  pub fn prove(pk: &ProverKey<G, S>, sc: C, z_i: &[G::Scalar]) -> Result<Self, NovaError> {
+    let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
+
+    let circuit: DirectCircuit<G, C> = DirectCircuit {
+      z_i: Some(z_i.to_vec()),
+      sc,
+    };
+
+    let _ = circuit.synthesize(&mut cs);
+    let (u, w) = cs
+      .r1cs_instance_and_witness(&pk.S, &pk.ck)
+      .map_err(|_e| NovaError::UnSat)?;
+
+    // convert the instance and witness to relaxed form
+    let (u_relaxed, w_relaxed) = (
+      RelaxedR1CSInstance::from_r1cs_instance_unchecked(&u.comm_W, &u.X),
+      RelaxedR1CSWitness::from_r1cs_witness(&pk.S, &w),
+    );
+
+    // prove the instance using Spartan
+    let snark = S::prove(&pk.ck, &pk.pk, &u_relaxed, &w_relaxed)?;
+
+    Ok(DirectSNARK {
+      comm_W: u.comm_W,
+      snark,
+      _p: Default::default(),
+    })
+  }
+
+  /// Verifies a proof of satisfiability
+  pub fn verify(&self, vk: &VerifierKey<G, S>, io: &[G::Scalar]) -> Result<(), NovaError> {
+    // construct an instance using the provided commitment to the witness and z_i and z_{i+1}
+    let u_relaxed = RelaxedR1CSInstance::from_r1cs_instance_unchecked(&self.comm_W, io);
+
+    // verify the snark using the constructed instance
+    self.snark.verify(&vk.vk, &u_relaxed)?;
+
+    Ok(())
+  }
+}
+
+#[cfg(test)]
+mod tests {
+  use super::*;
+  use crate::provider::bn256_grumpkin::bn256;
+  use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
+  use core::marker::PhantomData;
+  use ff::PrimeField;
+
+  #[derive(Clone, Debug, Default)]
+  struct CubicCircuit<F: PrimeField> {
+    _p: PhantomData<F>,
+  }
+
+  impl<F> StepCircuit<F> for CubicCircuit<F>
+  where
+    F: PrimeField,
+  {
+    fn arity(&self) -> usize {
+      1
+    }
+
+    fn synthesize<CS: ConstraintSystem<F>>(
+      &self,
+      cs: &mut CS,
+      z: &[AllocatedNum<F>],
+    ) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
+      // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
+      let x = &z[0];
+      let x_sq = x.square(cs.namespace(|| "x_sq"))?;
+      let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), x)?;
+      let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
+        Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
+      })?;
+
+      cs.enforce(
+        || "y = x^3 + x + 5",
+        |lc| {
+          lc + x_cu.get_variable()
+            + x.get_variable()
+            + CS::one()
+            + CS::one()
+            + CS::one()
+            + CS::one()
+            + CS::one()
+        },
+        |lc| lc + CS::one(),
+        |lc| lc + y.get_variable(),
+      );
+
+      Ok(vec![y])
+    }
+
+    fn output(&self, z: &[F]) -> Vec<F> {
+      vec![z[0] * z[0] * z[0] + z[0] + F::from(5u64)]
+    }
+  }
+
+  #[test]
+  fn test_direct_snark() {
+    type G = pasta_curves::pallas::Point;
+    type EE = crate::provider::ipa_pc::EvaluationEngine<G>;
+    type S = crate::spartan::snark::RelaxedR1CSSNARK<G, EE>;
+    type Spp = crate::spartan::ppsnark::RelaxedR1CSSNARK<G, EE>;
+    test_direct_snark_with::<G, S>();
+    test_direct_snark_with::<G, Spp>();
+
+    type G2 = bn256::Point;
+    type EE2 = crate::provider::ipa_pc::EvaluationEngine<G2>;
+    type S2 = crate::spartan::snark::RelaxedR1CSSNARK<G2, EE2>;
+    type S2pp = crate::spartan::ppsnark::RelaxedR1CSSNARK<G2, EE2>;
+    test_direct_snark_with::<G2, S2>();
+    test_direct_snark_with::<G2, S2pp>();
+  }
+
+  fn test_direct_snark_with<G: Group, S: RelaxedR1CSSNARKTrait<G>>() {
+    let circuit = CubicCircuit::default();
+
+    // produce keys
+    let (pk, vk) =
+      DirectSNARK::<G, S, CubicCircuit<<G as Group>::Scalar>>::setup(circuit.clone()).unwrap();
+
+    let num_steps = 3;
+
+    // setup inputs
+    let z0 = vec![<G as Group>::Scalar::ZERO];
+    let mut z_i = z0;
+
+    for _i in 0..num_steps {
+      // produce a SNARK
+      let res = DirectSNARK::prove(&pk, circuit.clone(), &z_i);
+      assert!(res.is_ok());
+
+      let z_i_plus_one = circuit.output(&z_i);
+
+      let snark = res.unwrap();
+
+      // verify the SNARK
+      let io = z_i
+        .clone()
+        .into_iter()
+        .chain(z_i_plus_one.clone().into_iter())
+        .collect::<Vec<_>>();
+      let res = snark.verify(&vk, &io);
+      assert!(res.is_ok());
+
+      // set input to the next step
+      z_i = z_i_plus_one.clone();
+    }
+
+    // sanity: check the claimed output with a direct computation of the same
+    assert_eq!(z_i, vec![<G as Group>::Scalar::from(2460515u64)]);
+  }
+}

src/spartan/mod.rs

@@ -1,25 +1,18 @@
 //! This module implements RelaxedR1CSSNARKTrait using Spartan that is generic
 //! over the polynomial commitment and evaluation argument (i.e., a PCS)
+//! We provide two implementations, one in snark.rs (which does not use any preprocessing)
+//! and another in ppsnark.rs (which uses preprocessing to keep the verifier's state small if the PCS scheme provides a succinct verifier)
+//! We also provide direct.rs that allows proving a step circuit directly with either of the two SNARKs.
+pub mod direct;
 mod math;
 pub(crate) mod polynomial;
-pub mod pp;
+pub mod ppsnark;
+pub mod snark;
 mod sumcheck;
 
-use crate::{
+use crate::{traits::Group, Commitment};
-  compute_digest,
-  errors::NovaError,
-  r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
-  traits::{
-    evaluation::EvaluationEngineTrait, snark::RelaxedR1CSSNARKTrait, Group, TranscriptEngineTrait,
-  },
-  Commitment, CommitmentKey,
-};
 use ff::Field;
-use itertools::concat;
+use polynomial::SparsePolynomial;
-use polynomial::{EqPolynomial, MultilinearPolynomial, SparsePolynomial};
-use rayon::prelude::*;
-use serde::{Deserialize, Serialize};
-use sumcheck::SumcheckProof;
 
 fn powers<G: Group>(s: &G::Scalar, n: usize) -> Vec<G::Scalar> {
   assert!(n >= 1);
@@ -123,510 +116,3 @@ impl<G: Group> PolyEvalInstance<G> {
     }
   }
 }
-
-/// A type that represents the prover's key
-#[derive(Serialize, Deserialize)]
-#[serde(bound = "")]
-pub struct ProverKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
-  pk_ee: EE::ProverKey,
-  S: R1CSShape<G>,
-  vk_digest: G::Scalar, // digest of the verifier's key
-}
-
-/// A type that represents the verifier's key
-#[derive(Serialize, Deserialize)]
-#[serde(bound = "")]
-pub struct VerifierKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
-  vk_ee: EE::VerifierKey,
-  S: R1CSShape<G>,
-  digest: G::Scalar,
-}
-
-/// A succinct proof of knowledge of a witness to a relaxed R1CS instance
-/// The proof is produced using Spartan's combination of the sum-check and
-/// the commitment to a vector viewed as a polynomial commitment
-#[derive(Serialize, Deserialize)]
-#[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),
-  eval_E: G::Scalar,
-  sc_proof_inner: SumcheckProof<G>,
-  eval_W: G::Scalar,
-  sc_proof_batch: SumcheckProof<G>,
-  evals_batch: Vec<G::Scalar>,
-  eval_arg: EE::EvaluationArgument,
-}
-
-impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G>
-  for RelaxedR1CSSNARK<G, EE>
-{
-  type ProverKey = ProverKey<G, EE>;
-  type VerifierKey = VerifierKey<G, EE>;
-
-  fn setup(
-    ck: &CommitmentKey<G>,
-    S: &R1CSShape<G>,
-  ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> {
-    let (pk_ee, vk_ee) = EE::setup(ck);
-
-    let S = S.pad();
-
-    let vk = {
-      let mut vk = VerifierKey {
-        vk_ee,
-        S: S.clone(),
-        digest: G::Scalar::ZERO,
-      };
-      vk.digest = compute_digest::<G, VerifierKey<G, EE>>(&vk);
-      vk
-    };
-
-    let pk = ProverKey {
-      pk_ee,
-      S,
-      vk_digest: vk.digest,
-    };
-
-    Ok((pk, vk))
-  }
-
-  /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
-  fn prove(
-    ck: &CommitmentKey<G>,
-    pk: &Self::ProverKey,
-    U: &RelaxedR1CSInstance<G>,
-    W: &RelaxedR1CSWitness<G>,
-  ) -> Result<Self, NovaError> {
-    let W = W.pad(&pk.S); // pad the witness
-    let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
-
-    // sanity check that R1CSShape has certain size characteristics
-    assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
-    assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
-    assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
-    assert!(pk.S.num_io < pk.S.num_vars);
-
-    // append the digest of vk (which includes R1CS matrices) and the RelaxedR1CSInstance to the transcript
-    transcript.absorb(b"vk", &pk.vk_digest);
-    transcript.absorb(b"U", U);
-
-    // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
-    let mut z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
-
-    let (num_rounds_x, num_rounds_y) = (
-      (pk.S.num_cons as f64).log2() as usize,
-      ((pk.S.num_vars as f64).log2() as usize + 1),
-    );
-
-    // outer sum-check
-    let tau = (0..num_rounds_x)
-      .map(|_i| transcript.squeeze(b"t"))
-      .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
-
-    let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals());
-    let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = {
-      let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?;
-      let poly_uCz_E = (0..pk.S.num_cons)
-        .map(|i| U.u * poly_Cz[i] + W.E[i])
-        .collect::<Vec<G::Scalar>>();
-      (
-        MultilinearPolynomial::new(poly_Az),
-        MultilinearPolynomial::new(poly_Bz),
-        MultilinearPolynomial::new(poly_Cz),
-        MultilinearPolynomial::new(poly_uCz_E),
-      )
-    };
-
-    let comb_func_outer =
-      |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 * *poly_C_comp - *poly_D_comp) };
-    let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term(
-      &G::Scalar::ZERO, // claim is zero
-      num_rounds_x,
-      &mut poly_tau,
-      &mut poly_Az,
-      &mut poly_Bz,
-      &mut poly_uCz_E,
-      comb_func_outer,
-      &mut transcript,
-    )?;
-
-    // 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);
-    transcript.absorb(
-      b"claims_outer",
-      &[claim_Az, claim_Bz, claim_Cz, eval_E].as_slice(),
-    );
-
-    // inner sum-check
-    let r = transcript.squeeze(b"r")?;
-    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)
-      let evals_rx = EqPolynomial::new(r_x.clone()).evals();
-
-      // Bounds "row" variables of (A, B, C) matrices viewed as 2d multilinear polynomials
-      let compute_eval_table_sparse =
-        |S: &R1CSShape<G>, rx: &[G::Scalar]| -> (Vec<G::Scalar>, Vec<G::Scalar>, Vec<G::Scalar>) {
-          assert_eq!(rx.len(), S.num_cons);
-
-          let inner = |M: &Vec<(usize, usize, G::Scalar)>, M_evals: &mut Vec<G::Scalar>| {
-            for (row, col, val) in M {
-              M_evals[*col] += rx[*row] * val;
-            }
-          };
-
-          let (A_evals, (B_evals, C_evals)) = rayon::join(
-            || {
-              let mut A_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
-              inner(&S.A, &mut A_evals);
-              A_evals
-            },
-            || {
-              rayon::join(
-                || {
-                  let mut B_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
-                  inner(&S.B, &mut B_evals);
-                  B_evals
-                },
-                || {
-                  let mut C_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
-                  inner(&S.C, &mut C_evals);
-                  C_evals
-                },
-              )
-            },
-          );
-
-          (A_evals, B_evals, C_evals)
-        };
-
-      let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&pk.S, &evals_rx);
-
-      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| evals_A[i] + r * evals_B[i] + r * r * evals_C[i])
-        .collect::<Vec<G::Scalar>>()
-    };
-
-    let poly_z = {
-      z.resize(pk.S.num_vars * 2, G::Scalar::ZERO);
-      z
-    };
-
-    let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
-      *poly_A_comp * *poly_B_comp
-    };
-    let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad(
-      &claim_inner_joint,
-      num_rounds_y,
-      &mut MultilinearPolynomial::new(poly_ABC),
-      &mut MultilinearPolynomial::new(poly_z),
-      comb_func,
-      &mut transcript,
-    )?;
-
-    // add additional claims about W and E polynomials to the list from CC
-    let mut w_u_vec = Vec::new();
-    let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_y[1..]);
-    w_u_vec.push((
-      PolyEvalWitness { p: W.W.clone() },
-      PolyEvalInstance {
-        c: U.comm_W,
-        x: r_y[1..].to_vec(),
-        e: eval_W,
-      },
-    ));
-
-    w_u_vec.push((
-      PolyEvalWitness { p: W.E },
-      PolyEvalInstance {
-        c: U.comm_E,
-        x: r_x,
-        e: eval_E,
-      },
-    ));
-
-    // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point.
-    // For example, eval_W =? W(r_y[1..]) and eval_E =? 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.
-    assert!(w_u_vec.len() >= 2);
-
-    let (w_vec, u_vec): (Vec<PolyEvalWitness<G>>, Vec<PolyEvalInstance<G>>) =
-      w_u_vec.into_iter().unzip();
-    let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size
-    let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
-
-    // generate a challenge
-    let rho = transcript.squeeze(b"r")?;
-    let num_claims = w_vec_padded.len();
-    let powers_of_rho = powers::<G>(&rho, num_claims);
-    let claim_batch_joint = u_vec_padded
-      .iter()
-      .zip(powers_of_rho.iter())
-      .map(|(u, p)| u.e * p)
-      .sum();
-
-    let mut polys_left: Vec<MultilinearPolynomial<G::Scalar>> = w_vec_padded
-      .iter()
-      .map(|w| MultilinearPolynomial::new(w.p.clone()))
-      .collect();
-    let mut polys_right: Vec<MultilinearPolynomial<G::Scalar>> = u_vec_padded
-      .iter()
-      .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals()))
-      .collect();
-
-    let num_rounds_z = u_vec_padded[0].x.len();
-    let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
-      *poly_A_comp * *poly_B_comp
-    };
-    let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch(
-      &claim_batch_joint,
-      num_rounds_z,
-      &mut polys_left,
-      &mut polys_right,
-      &powers_of_rho,
-      comb_func,
-      &mut transcript,
-    )?;
-
-    let (claims_batch_left, _): (Vec<G::Scalar>, Vec<G::Scalar>) = claims_batch;
-
-    transcript.absorb(b"l", &claims_batch_left.as_slice());
-
-    // we now combine evaluation claims at the same point rz into one
-    let gamma = transcript.squeeze(b"g")?;
-    let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
-    let comm_joint = u_vec_padded
-      .iter()
-      .zip(powers_of_gamma.iter())
-      .map(|(u, g_i)| u.c * *g_i)
-      .fold(Commitment::<G>::default(), |acc, item| acc + item);
-    let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma);
-    let eval_joint = claims_batch_left
-      .iter()
-      .zip(powers_of_gamma.iter())
-      .map(|(e, g_i)| *e * *g_i)
-      .sum();
-
-    let eval_arg = EE::prove(
-      ck,
-      &pk.pk_ee,
-      &mut transcript,
-      &comm_joint,
-      &poly_joint.p,
-      &r_z,
-      &eval_joint,
-    )?;
-
-    Ok(RelaxedR1CSSNARK {
-      sc_proof_outer,
-      claims_outer: (claim_Az, claim_Bz, claim_Cz),
-      eval_E,
-      sc_proof_inner,
-      eval_W,
-      sc_proof_batch,
-      evals_batch: claims_batch_left,
-      eval_arg,
-    })
-  }
-
-  /// verifies a proof of satisfiability of a RelaxedR1CS instance
-  fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
-    let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
-
-    // append the digest of R1CS matrices and the RelaxedR1CSInstance to the transcript
-    transcript.absorb(b"vk", &vk.digest);
-    transcript.absorb(b"U", U);
-
-    let (num_rounds_x, num_rounds_y) = (
-      (vk.S.num_cons as f64).log2() as usize,
-      ((vk.S.num_vars as f64).log2() as usize + 1),
-    );
-
-    // outer sum-check
-    let tau = (0..num_rounds_x)
-      .map(|_i| transcript.squeeze(b"t"))
-      .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
-
-    let (claim_outer_final, r_x) =
-      self
-        .sc_proof_outer
-        .verify(G::Scalar::ZERO, num_rounds_x, 3, &mut transcript)?;
-
-    // verify claim_outer_final
-    let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer;
-    let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x);
-    let claim_outer_final_expected =
-      taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E);
-    if claim_outer_final != claim_outer_final_expected {
-      return Err(NovaError::InvalidSumcheckProof);
-    }
-
-    transcript.absorb(
-      b"claims_outer",
-      &[
-        self.claims_outer.0,
-        self.claims_outer.1,
-        self.claims_outer.2,
-        self.eval_E,
-      ]
-      .as_slice(),
-    );
-
-    // inner sum-check
-    let r = transcript.squeeze(b"r")?;
-    let claim_inner_joint =
-      self.claims_outer.0 + r * self.claims_outer.1 + r * r * self.claims_outer.2;
-
-    let (claim_inner_final, r_y) =
-      self
-        .sc_proof_inner
-        .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?;
-
-    // verify claim_inner_final
-    let eval_Z = {
-      let eval_X = {
-        // constant term
-        let mut poly_X = vec![(0, U.u)];
-        //remaining inputs
-        poly_X.extend(
-          (0..U.X.len())
-            .map(|i| (i + 1, U.X[i]))
-            .collect::<Vec<(usize, G::Scalar)>>(),
-        );
-        SparsePolynomial::new((vk.S.num_vars as f64).log2() as usize, poly_X).evaluate(&r_y[1..])
-      };
-      (G::Scalar::ONE - r_y[0]) * self.eval_W + r_y[0] * eval_X
-    };
-
-    // compute evaluations of R1CS matrices
-    let multi_evaluate = |M_vec: &[&[(usize, usize, G::Scalar)]],
-                          r_x: &[G::Scalar],
-                          r_y: &[G::Scalar]|
-     -> Vec<G::Scalar> {
-      let evaluate_with_table =
-        |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar {
-          (0..M.len())
-            .collect::<Vec<usize>>()
-            .par_iter()
-            .map(|&i| {
-              let (row, col, val) = M[i];
-              T_x[row] * T_y[col] * val
-            })
-            .reduce(|| G::Scalar::ZERO, |acc, x| acc + x)
-        };
-
-      let (T_x, T_y) = rayon::join(
-        || EqPolynomial::new(r_x.to_vec()).evals(),
-        || EqPolynomial::new(r_y.to_vec()).evals(),
-      );
-
-      (0..M_vec.len())
-        .collect::<Vec<usize>>()
-        .par_iter()
-        .map(|&i| evaluate_with_table(M_vec[i], &T_x, &T_y))
-        .collect()
-    };
-
-    let evals = multi_evaluate(&[&vk.S.A, &vk.S.B, &vk.S.C], &r_x, &r_y);
-
-    let claim_inner_final_expected = (evals[0] + r * evals[1] + r * r * evals[2]) * eval_Z;
-    if claim_inner_final != claim_inner_final_expected {
-      return Err(NovaError::InvalidSumcheckProof);
-    }
-
-    // add claims about W and E polynomials
-    let u_vec: Vec<PolyEvalInstance<G>> = vec![
-      PolyEvalInstance {
-        c: U.comm_W,
-        x: r_y[1..].to_vec(),
-        e: self.eval_W,
-      },
-      PolyEvalInstance {
-        c: U.comm_E,
-        x: r_x,
-        e: self.eval_E,
-      },
-    ];
-
-    let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
-
-    // generate a challenge
-    let rho = transcript.squeeze(b"r")?;
-    let num_claims = u_vec.len();
-    let powers_of_rho = powers::<G>(&rho, num_claims);
-    let claim_batch_joint = u_vec
-      .iter()
-      .zip(powers_of_rho.iter())
-      .map(|(u, p)| u.e * p)
-      .sum();
-
-    let num_rounds_z = u_vec_padded[0].x.len();
-    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 evals = u_vec_padded
-        .iter()
-        .map(|u| poly_rz.evaluate(&u.x))
-        .collect::<Vec<G::Scalar>>();
-
-      evals
-        .iter()
-        .zip(self.evals_batch.iter())
-        .zip(powers_of_rho.iter())
-        .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i)
-        .sum()
-    };
-
-    if claim_batch_final != claim_batch_final_expected {
-      return Err(NovaError::InvalidSumcheckProof);
-    }
-
-    transcript.absorb(b"l", &self.evals_batch.as_slice());
-
-    // we now combine evaluation claims at the same point rz into one
-    let gamma = transcript.squeeze(b"g")?;
-    let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
-    let comm_joint = u_vec_padded
-      .iter()
-      .zip(powers_of_gamma.iter())
-      .map(|(u, g_i)| u.c * *g_i)
-      .fold(Commitment::<G>::default(), |acc, item| acc + item);
-    let eval_joint = self
-      .evals_batch
-      .iter()
-      .zip(powers_of_gamma.iter())
-      .map(|(e, g_i)| *e * *g_i)
-      .sum();
-
-    // verify
-    EE::verify(
-      &vk.vk_ee,
-      &mut transcript,
-      &comm_joint,
-      &r_z,
-      &eval_joint,
-      &self.eval_arg,
-    )?;
-
-    Ok(())
-  }
-}

src/spartan/ppsnark.rs

@@ -1,11 +1,8 @@
 //! This module implements RelaxedR1CSSNARK traits using a spark-based approach to prove evaluations of
 //! sparse multilinear polynomials involved in Spartan's sum-check protocol, thereby providing a preprocessing SNARK
+//! The verifier in this preprocessing SNARK maintains a commitment to R1CS matrices. This is beneficial when using a
+//! polynomial commitment scheme in which the verifier's costs is succinct.
 use crate::{
-  bellperson::{
-    r1cs::{NovaShape, NovaWitness},
-    shape_cs::ShapeCS,
-    solver::SatisfyingAssignment,
-  },
   compute_digest,
   errors::NovaError,
   r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
@@ -17,7 +14,6 @@ use crate::{
     PolyEvalInstance, PolyEvalWitness, SparsePolynomial,
   },
   traits::{
-    circuit::StepCircuit,
     commitment::{CommitmentEngineTrait, CommitmentTrait},
     evaluation::EvaluationEngineTrait,
     snark::RelaxedR1CSSNARKTrait,
@@ -25,7 +21,6 @@ use crate::{
   },
   Commitment, CommitmentKey, CompressedCommitment,
 };
-use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError};
 use core::{cmp::max, marker::PhantomData};
 use ff::{Field, PrimeField};
 use itertools::concat;
@@ -2045,245 +2040,3 @@ impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G
     Ok(())
   }
 }
-
-// provides direct interfaces to call the SNARK implemented in this module
-struct SpartanCircuit<G: Group, SC: StepCircuit<G::Scalar>> {
-  z_i: Option<Vec<G::Scalar>>, // inputs to the circuit
-  sc: SC,                      // step circuit to be executed
-}
-
-impl<G: Group, SC: StepCircuit<G::Scalar>> Circuit<G::Scalar> for SpartanCircuit<G, SC> {
-  fn synthesize<CS: ConstraintSystem<G::Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
-    // obtain the arity information
-    let arity = self.sc.arity();
-
-    // Allocate zi. If inputs.zi is not provided, allocate default value 0
-    let zero = vec![G::Scalar::ZERO; arity];
-    let z_i = (0..arity)
-      .map(|i| {
-        AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || {
-          Ok(self.z_i.as_ref().unwrap_or(&zero)[i])
-        })
-      })
-      .collect::<Result<Vec<AllocatedNum<G::Scalar>>, _>>()?;
-
-    let z_i_plus_one = self.sc.synthesize(&mut cs.namespace(|| "F"), &z_i)?;
-
-    // inputize both z_i and z_i_plus_one
-    for (j, input) in z_i.iter().enumerate().take(arity) {
-      let _ = input.inputize(cs.namespace(|| format!("input {j}")));
-    }
-    for (j, output) in z_i_plus_one.iter().enumerate().take(arity) {
-      let _ = output.inputize(cs.namespace(|| format!("output {j}")));
-    }
-
-    Ok(())
-  }
-}
-
-/// A type that holds Spartan's prover key
-#[derive(Clone, Serialize, Deserialize)]
-#[serde(bound = "")]
-pub struct SpartanProverKey<G, EE>
-where
-  G: Group,
-  EE: EvaluationEngineTrait<G, CE = G::CE>,
-{
-  S: R1CSShape<G>,
-  ck: CommitmentKey<G>,
-  pk: ProverKey<G, EE>,
-}
-
-/// A type that holds Spartan's verifier key
-#[derive(Clone, Serialize, Deserialize)]
-#[serde(bound = "")]
-pub struct SpartanVerifierKey<G, EE>
-where
-  G: Group,
-  EE: EvaluationEngineTrait<G, CE = G::CE>,
-{
-  vk: VerifierKey<G, EE>,
-}
-
-/// A direct SNARK proving a step circuit
-#[derive(Clone, Serialize, Deserialize)]
-#[serde(bound = "")]
-pub struct SpartanSNARK<G, EE, C>
-where
-  G: Group,
-  EE: EvaluationEngineTrait<G, CE = G::CE>,
-  C: StepCircuit<G::Scalar>,
-{
-  comm_W: Commitment<G>,          // commitment to the witness
-  snark: RelaxedR1CSSNARK<G, EE>, // snark proving the witness is satisfying
-  _p: PhantomData<C>,
-}
-
-impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>, C: StepCircuit<G::Scalar>>
-  SpartanSNARK<G, EE, C>
-{
-  /// Produces prover and verifier keys for Spartan
-  pub fn setup(sc: C) -> Result<(SpartanProverKey<G, EE>, SpartanVerifierKey<G, EE>), NovaError> {
-    // construct a circuit that can be synthesized
-    let circuit: SpartanCircuit<G, C> = SpartanCircuit { z_i: None, sc };
-
-    let mut cs: ShapeCS<G> = ShapeCS::new();
-    let _ = circuit.synthesize(&mut cs);
-    let (S, ck) = cs.r1cs_shape();
-
-    let (pk, vk) = RelaxedR1CSSNARK::setup(&ck, &S)?;
-
-    let pk = SpartanProverKey { S, ck, pk };
-
-    let vk = SpartanVerifierKey { vk };
-
-    Ok((pk, vk))
-  }
-
-  /// Produces a proof of satisfiability of the provided circuit
-  pub fn prove(pk: &SpartanProverKey<G, EE>, sc: C, z_i: &[G::Scalar]) -> Result<Self, NovaError> {
-    let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
-
-    let circuit: SpartanCircuit<G, C> = SpartanCircuit {
-      z_i: Some(z_i.to_vec()),
-      sc,
-    };
-
-    let _ = circuit.synthesize(&mut cs);
-    let (u, w) = cs
-      .r1cs_instance_and_witness(&pk.S, &pk.ck)
-      .map_err(|_e| NovaError::UnSat)?;
-
-    // convert the instance and witness to relaxed form
-    let (u_relaxed, w_relaxed) = (
-      RelaxedR1CSInstance::from_r1cs_instance_unchecked(&u.comm_W, &u.X),
-      RelaxedR1CSWitness::from_r1cs_witness(&pk.S, &w),
-    );
-
-    // prove the instance using Spartan
-    let snark = RelaxedR1CSSNARK::prove(&pk.ck, &pk.pk, &u_relaxed, &w_relaxed)?;
-
-    Ok(SpartanSNARK {
-      comm_W: u.comm_W,
-      snark,
-      _p: Default::default(),
-    })
-  }
-
-  /// Verifies a proof of satisfiability
-  pub fn verify(&self, vk: &SpartanVerifierKey<G, EE>, io: &[G::Scalar]) -> Result<(), NovaError> {
-    // construct an instance using the provided commitment to the witness and z_i and z_{i+1}
-    let u_relaxed = RelaxedR1CSInstance::from_r1cs_instance_unchecked(&self.comm_W, io);
-
-    // verify the snark using the constructed instance
-    self.snark.verify(&vk.vk, &u_relaxed)?;
-
-    Ok(())
-  }
-}
-
-#[cfg(test)]
-mod tests {
-  use super::*;
-  use crate::provider::bn256_grumpkin::bn256;
-  use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
-  use core::marker::PhantomData;
-  use ff::PrimeField;
-
-  #[derive(Clone, Debug, Default)]
-  struct CubicCircuit<F: PrimeField> {
-    _p: PhantomData<F>,
-  }
-
-  impl<F> StepCircuit<F> for CubicCircuit<F>
-  where
-    F: PrimeField,
-  {
-    fn arity(&self) -> usize {
-      1
-    }
-
-    fn synthesize<CS: ConstraintSystem<F>>(
-      &self,
-      cs: &mut CS,
-      z: &[AllocatedNum<F>],
-    ) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
-      // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
-      let x = &z[0];
-      let x_sq = x.square(cs.namespace(|| "x_sq"))?;
-      let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), x)?;
-      let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
-        Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
-      })?;
-
-      cs.enforce(
-        || "y = x^3 + x + 5",
-        |lc| {
-          lc + x_cu.get_variable()
-            + x.get_variable()
-            + CS::one()
-            + CS::one()
-            + CS::one()
-            + CS::one()
-            + CS::one()
-        },
-        |lc| lc + CS::one(),
-        |lc| lc + y.get_variable(),
-      );
-
-      Ok(vec![y])
-    }
-
-    fn output(&self, z: &[F]) -> Vec<F> {
-      vec![z[0] * z[0] * z[0] + z[0] + F::from(5u64)]
-    }
-  }
-
-  #[test]
-  fn test_spartan_snark() {
-    type G = pasta_curves::pallas::Point;
-    type EE = crate::provider::ipa_pc::EvaluationEngine<G>;
-
-    test_spartan_snark_with::<G, EE>();
-    test_spartan_snark_with::<_, crate::provider::ipa_pc::EvaluationEngine<bn256::Point>>();
-  }
-
-  fn test_spartan_snark_with<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>>() {
-    let circuit = CubicCircuit::default();
-
-    // produce keys
-    let (pk, vk) =
-      SpartanSNARK::<G, EE, CubicCircuit<<G as Group>::Scalar>>::setup(circuit.clone()).unwrap();
-
-    let num_steps = 3;
-
-    // setup inputs
-    let z0 = vec![<G as Group>::Scalar::ZERO];
-    let mut z_i = z0;
-
-    for _i in 0..num_steps {
-      // produce a SNARK
-      let res = SpartanSNARK::prove(&pk, circuit.clone(), &z_i);
-      assert!(res.is_ok());
-
-      let z_i_plus_one = circuit.output(&z_i);
-
-      let snark = res.unwrap();
-
-      // verify the SNARK
-      let io = z_i
-        .clone()
-        .into_iter()
-        .chain(z_i_plus_one.clone().into_iter())
-        .collect::<Vec<_>>();
-      let res = snark.verify(&vk, &io);
-      assert!(res.is_ok());
-
-      // set input to the next step
-      z_i = z_i_plus_one.clone();
-    }
-
-    // sanity: check the claimed output with a direct computation of the same
-    assert_eq!(z_i, vec![<G as Group>::Scalar::from(2460515u64)]);
-  }
-}

src/spartan/snark.rs

@@ -0,0 +1,532 @@
+//! This module implements RelaxedR1CSSNARKTrait using Spartan that is generic
+//! over the polynomial commitment and evaluation argument (i.e., a PCS)
+//! This version of Spartan does not use preprocessing so the verifier keeps the entire
+//! description of R1CS matrices. This is essentially optimal for the verifier when using
+//! an IPA-based polynomial commitment scheme.
+
+use crate::{
+  compute_digest,
+  errors::NovaError,
+  r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
+  spartan::{
+    polynomial::{EqPolynomial, MultilinearPolynomial, SparsePolynomial},
+    powers,
+    sumcheck::SumcheckProof,
+    PolyEvalInstance, PolyEvalWitness,
+  },
+  traits::{
+    evaluation::EvaluationEngineTrait, snark::RelaxedR1CSSNARKTrait, Group, TranscriptEngineTrait,
+  },
+  Commitment, CommitmentKey,
+};
+use ff::Field;
+use itertools::concat;
+use rayon::prelude::*;
+use serde::{Deserialize, Serialize};
+
+/// A type that represents the prover's key
+#[derive(Serialize, Deserialize)]
+#[serde(bound = "")]
+pub struct ProverKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
+  pk_ee: EE::ProverKey,
+  S: R1CSShape<G>,
+  vk_digest: G::Scalar, // digest of the verifier's key
+}
+
+/// A type that represents the verifier's key
+#[derive(Serialize, Deserialize)]
+#[serde(bound = "")]
+pub struct VerifierKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
+  vk_ee: EE::VerifierKey,
+  S: R1CSShape<G>,
+  digest: G::Scalar,
+}
+
+/// A succinct proof of knowledge of a witness to a relaxed R1CS instance
+/// The proof is produced using Spartan's combination of the sum-check and
+/// the commitment to a vector viewed as a polynomial commitment
+#[derive(Serialize, Deserialize)]
+#[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),
+  eval_E: G::Scalar,
+  sc_proof_inner: SumcheckProof<G>,
+  eval_W: G::Scalar,
+  sc_proof_batch: SumcheckProof<G>,
+  evals_batch: Vec<G::Scalar>,
+  eval_arg: EE::EvaluationArgument,
+}
+
+impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G>
+  for RelaxedR1CSSNARK<G, EE>
+{
+  type ProverKey = ProverKey<G, EE>;
+  type VerifierKey = VerifierKey<G, EE>;
+
+  fn setup(
+    ck: &CommitmentKey<G>,
+    S: &R1CSShape<G>,
+  ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> {
+    let (pk_ee, vk_ee) = EE::setup(ck);
+
+    let S = S.pad();
+
+    let vk = {
+      let mut vk = VerifierKey {
+        vk_ee,
+        S: S.clone(),
+        digest: G::Scalar::ZERO,
+      };
+      vk.digest = compute_digest::<G, VerifierKey<G, EE>>(&vk);
+      vk
+    };
+
+    let pk = ProverKey {
+      pk_ee,
+      S,
+      vk_digest: vk.digest,
+    };
+
+    Ok((pk, vk))
+  }
+
+  /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
+  fn prove(
+    ck: &CommitmentKey<G>,
+    pk: &Self::ProverKey,
+    U: &RelaxedR1CSInstance<G>,
+    W: &RelaxedR1CSWitness<G>,
+  ) -> Result<Self, NovaError> {
+    let W = W.pad(&pk.S); // pad the witness
+    let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
+
+    // sanity check that R1CSShape has certain size characteristics
+    assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
+    assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
+    assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
+    assert!(pk.S.num_io < pk.S.num_vars);
+
+    // append the digest of vk (which includes R1CS matrices) and the RelaxedR1CSInstance to the transcript
+    transcript.absorb(b"vk", &pk.vk_digest);
+    transcript.absorb(b"U", U);
+
+    // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
+    let mut z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
+
+    let (num_rounds_x, num_rounds_y) = (
+      (pk.S.num_cons as f64).log2() as usize,
+      ((pk.S.num_vars as f64).log2() as usize + 1),
+    );
+
+    // outer sum-check
+    let tau = (0..num_rounds_x)
+      .map(|_i| transcript.squeeze(b"t"))
+      .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
+
+    let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals());
+    let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = {
+      let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?;
+      let poly_uCz_E = (0..pk.S.num_cons)
+        .map(|i| U.u * poly_Cz[i] + W.E[i])
+        .collect::<Vec<G::Scalar>>();
+      (
+        MultilinearPolynomial::new(poly_Az),
+        MultilinearPolynomial::new(poly_Bz),
+        MultilinearPolynomial::new(poly_Cz),
+        MultilinearPolynomial::new(poly_uCz_E),
+      )
+    };
+
+    let comb_func_outer =
+      |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 * *poly_C_comp - *poly_D_comp) };
+    let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term(
+      &G::Scalar::ZERO, // claim is zero
+      num_rounds_x,
+      &mut poly_tau,
+      &mut poly_Az,
+      &mut poly_Bz,
+      &mut poly_uCz_E,
+      comb_func_outer,
+      &mut transcript,
+    )?;
+
+    // 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);
+    transcript.absorb(
+      b"claims_outer",
+      &[claim_Az, claim_Bz, claim_Cz, eval_E].as_slice(),
+    );
+
+    // inner sum-check
+    let r = transcript.squeeze(b"r")?;
+    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)
+      let evals_rx = EqPolynomial::new(r_x.clone()).evals();
+
+      // Bounds "row" variables of (A, B, C) matrices viewed as 2d multilinear polynomials
+      let compute_eval_table_sparse =
+        |S: &R1CSShape<G>, rx: &[G::Scalar]| -> (Vec<G::Scalar>, Vec<G::Scalar>, Vec<G::Scalar>) {
+          assert_eq!(rx.len(), S.num_cons);
+
+          let inner = |M: &Vec<(usize, usize, G::Scalar)>, M_evals: &mut Vec<G::Scalar>| {
+            for (row, col, val) in M {
+              M_evals[*col] += rx[*row] * val;
+            }
+          };
+
+          let (A_evals, (B_evals, C_evals)) = rayon::join(
+            || {
+              let mut A_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
+              inner(&S.A, &mut A_evals);
+              A_evals
+            },
+            || {
+              rayon::join(
+                || {
+                  let mut B_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
+                  inner(&S.B, &mut B_evals);
+                  B_evals
+                },
+                || {
+                  let mut C_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
+                  inner(&S.C, &mut C_evals);
+                  C_evals
+                },
+              )
+            },
+          );
+
+          (A_evals, B_evals, C_evals)
+        };
+
+      let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&pk.S, &evals_rx);
+
+      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| evals_A[i] + r * evals_B[i] + r * r * evals_C[i])
+        .collect::<Vec<G::Scalar>>()
+    };
+
+    let poly_z = {
+      z.resize(pk.S.num_vars * 2, G::Scalar::ZERO);
+      z
+    };
+
+    let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
+      *poly_A_comp * *poly_B_comp
+    };
+    let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad(
+      &claim_inner_joint,
+      num_rounds_y,
+      &mut MultilinearPolynomial::new(poly_ABC),
+      &mut MultilinearPolynomial::new(poly_z),
+      comb_func,
+      &mut transcript,
+    )?;
+
+    // add additional claims about W and E polynomials to the list from CC
+    let mut w_u_vec = Vec::new();
+    let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_y[1..]);
+    w_u_vec.push((
+      PolyEvalWitness { p: W.W.clone() },
+      PolyEvalInstance {
+        c: U.comm_W,
+        x: r_y[1..].to_vec(),
+        e: eval_W,
+      },
+    ));
+
+    w_u_vec.push((
+      PolyEvalWitness { p: W.E },
+      PolyEvalInstance {
+        c: U.comm_E,
+        x: r_x,
+        e: eval_E,
+      },
+    ));
+
+    // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point.
+    // For example, eval_W =? W(r_y[1..]) and eval_E =? 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.
+    assert!(w_u_vec.len() >= 2);
+
+    let (w_vec, u_vec): (Vec<PolyEvalWitness<G>>, Vec<PolyEvalInstance<G>>) =
+      w_u_vec.into_iter().unzip();
+    let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size
+    let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
+
+    // generate a challenge
+    let rho = transcript.squeeze(b"r")?;
+    let num_claims = w_vec_padded.len();
+    let powers_of_rho = powers::<G>(&rho, num_claims);
+    let claim_batch_joint = u_vec_padded
+      .iter()
+      .zip(powers_of_rho.iter())
+      .map(|(u, p)| u.e * p)
+      .sum();
+
+    let mut polys_left: Vec<MultilinearPolynomial<G::Scalar>> = w_vec_padded
+      .iter()
+      .map(|w| MultilinearPolynomial::new(w.p.clone()))
+      .collect();
+    let mut polys_right: Vec<MultilinearPolynomial<G::Scalar>> = u_vec_padded
+      .iter()
+      .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals()))
+      .collect();
+
+    let num_rounds_z = u_vec_padded[0].x.len();
+    let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
+      *poly_A_comp * *poly_B_comp
+    };
+    let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch(
+      &claim_batch_joint,
+      num_rounds_z,
+      &mut polys_left,
+      &mut polys_right,
+      &powers_of_rho,
+      comb_func,
+      &mut transcript,
+    )?;
+
+    let (claims_batch_left, _): (Vec<G::Scalar>, Vec<G::Scalar>) = claims_batch;
+
+    transcript.absorb(b"l", &claims_batch_left.as_slice());
+
+    // we now combine evaluation claims at the same point rz into one
+    let gamma = transcript.squeeze(b"g")?;
+    let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
+    let comm_joint = u_vec_padded
+      .iter()
+      .zip(powers_of_gamma.iter())
+      .map(|(u, g_i)| u.c * *g_i)
+      .fold(Commitment::<G>::default(), |acc, item| acc + item);
+    let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma);
+    let eval_joint = claims_batch_left
+      .iter()
+      .zip(powers_of_gamma.iter())
+      .map(|(e, g_i)| *e * *g_i)
+      .sum();
+
+    let eval_arg = EE::prove(
+      ck,
+      &pk.pk_ee,
+      &mut transcript,
+      &comm_joint,
+      &poly_joint.p,
+      &r_z,
+      &eval_joint,
+    )?;
+
+    Ok(RelaxedR1CSSNARK {
+      sc_proof_outer,
+      claims_outer: (claim_Az, claim_Bz, claim_Cz),
+      eval_E,
+      sc_proof_inner,
+      eval_W,
+      sc_proof_batch,
+      evals_batch: claims_batch_left,
+      eval_arg,
+    })
+  }
+
+  /// verifies a proof of satisfiability of a RelaxedR1CS instance
+  fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
+    let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
+
+    // append the digest of R1CS matrices and the RelaxedR1CSInstance to the transcript
+    transcript.absorb(b"vk", &vk.digest);
+    transcript.absorb(b"U", U);
+
+    let (num_rounds_x, num_rounds_y) = (
+      (vk.S.num_cons as f64).log2() as usize,
+      ((vk.S.num_vars as f64).log2() as usize + 1),
+    );
+
+    // outer sum-check
+    let tau = (0..num_rounds_x)
+      .map(|_i| transcript.squeeze(b"t"))
+      .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
+
+    let (claim_outer_final, r_x) =
+      self
+        .sc_proof_outer
+        .verify(G::Scalar::ZERO, num_rounds_x, 3, &mut transcript)?;
+
+    // verify claim_outer_final
+    let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer;
+    let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x);
+    let claim_outer_final_expected =
+      taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E);
+    if claim_outer_final != claim_outer_final_expected {
+      return Err(NovaError::InvalidSumcheckProof);
+    }
+
+    transcript.absorb(
+      b"claims_outer",
+      &[
+        self.claims_outer.0,
+        self.claims_outer.1,
+        self.claims_outer.2,
+        self.eval_E,
+      ]
+      .as_slice(),
+    );
+
+    // inner sum-check
+    let r = transcript.squeeze(b"r")?;
+    let claim_inner_joint =
+      self.claims_outer.0 + r * self.claims_outer.1 + r * r * self.claims_outer.2;
+
+    let (claim_inner_final, r_y) =
+      self
+        .sc_proof_inner
+        .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?;
+
+    // verify claim_inner_final
+    let eval_Z = {
+      let eval_X = {
+        // constant term
+        let mut poly_X = vec![(0, U.u)];
+        //remaining inputs
+        poly_X.extend(
+          (0..U.X.len())
+            .map(|i| (i + 1, U.X[i]))
+            .collect::<Vec<(usize, G::Scalar)>>(),
+        );
+        SparsePolynomial::new((vk.S.num_vars as f64).log2() as usize, poly_X).evaluate(&r_y[1..])
+      };
+      (G::Scalar::ONE - r_y[0]) * self.eval_W + r_y[0] * eval_X
+    };
+
+    // compute evaluations of R1CS matrices
+    let multi_evaluate = |M_vec: &[&[(usize, usize, G::Scalar)]],
+                          r_x: &[G::Scalar],
+                          r_y: &[G::Scalar]|
+     -> Vec<G::Scalar> {
+      let evaluate_with_table =
+        |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar {
+          (0..M.len())
+            .collect::<Vec<usize>>()
+            .par_iter()
+            .map(|&i| {
+              let (row, col, val) = M[i];
+              T_x[row] * T_y[col] * val
+            })
+            .reduce(|| G::Scalar::ZERO, |acc, x| acc + x)
+        };
+
+      let (T_x, T_y) = rayon::join(
+        || EqPolynomial::new(r_x.to_vec()).evals(),
+        || EqPolynomial::new(r_y.to_vec()).evals(),
+      );
+
+      (0..M_vec.len())
+        .collect::<Vec<usize>>()
+        .par_iter()
+        .map(|&i| evaluate_with_table(M_vec[i], &T_x, &T_y))
+        .collect()
+    };
+
+    let evals = multi_evaluate(&[&vk.S.A, &vk.S.B, &vk.S.C], &r_x, &r_y);
+
+    let claim_inner_final_expected = (evals[0] + r * evals[1] + r * r * evals[2]) * eval_Z;
+    if claim_inner_final != claim_inner_final_expected {
+      return Err(NovaError::InvalidSumcheckProof);
+    }
+
+    // add claims about W and E polynomials
+    let u_vec: Vec<PolyEvalInstance<G>> = vec![
+      PolyEvalInstance {
+        c: U.comm_W,
+        x: r_y[1..].to_vec(),
+        e: self.eval_W,
+      },
+      PolyEvalInstance {
+        c: U.comm_E,
+        x: r_x,
+        e: self.eval_E,
+      },
+    ];
+
+    let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
+
+    // generate a challenge
+    let rho = transcript.squeeze(b"r")?;
+    let num_claims = u_vec.len();
+    let powers_of_rho = powers::<G>(&rho, num_claims);
+    let claim_batch_joint = u_vec
+      .iter()
+      .zip(powers_of_rho.iter())
+      .map(|(u, p)| u.e * p)
+      .sum();
+
+    let num_rounds_z = u_vec_padded[0].x.len();
+    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 evals = u_vec_padded
+        .iter()
+        .map(|u| poly_rz.evaluate(&u.x))
+        .collect::<Vec<G::Scalar>>();
+
+      evals
+        .iter()
+        .zip(self.evals_batch.iter())
+        .zip(powers_of_rho.iter())
+        .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i)
+        .sum()
+    };
+
+    if claim_batch_final != claim_batch_final_expected {
+      return Err(NovaError::InvalidSumcheckProof);
+    }
+
+    transcript.absorb(b"l", &self.evals_batch.as_slice());
+
+    // we now combine evaluation claims at the same point rz into one
+    let gamma = transcript.squeeze(b"g")?;
+    let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
+    let comm_joint = u_vec_padded
+      .iter()
+      .zip(powers_of_gamma.iter())
+      .map(|(u, g_i)| u.c * *g_i)
+      .fold(Commitment::<G>::default(), |acc, item| acc + item);
+    let eval_joint = self
+      .evals_batch
+      .iter()
+      .zip(powers_of_gamma.iter())
+      .map(|(e, g_i)| *e * *g_i)
+      .sum();
+
+    // verify
+    EE::verify(
+      &vk.vk_ee,
+      &mut transcript,
+      &comm_joint,
+      &r_z,
+      &eval_joint,
+      &self.eval_arg,
+    )?;
+
+    Ok(())
+  }
+}