first version of PST

src/constraints.rs

@@ -18,10 +18,15 @@ use ark_groth16::{
   Groth16, PreparedVerifyingKey, Proof as GrothProof,
 };
 
+use ark_poly_commit::multilinear_pc::{
+  data_structures::{Commitment, Proof, VerifierKey},
+  MultilinearPC,
+};
 use ark_r1cs_std::{
   alloc::{AllocVar, AllocationMode},
   fields::fp::FpVar,
   prelude::{Boolean, EqGadget, FieldVar},
+  R1CSVar,
 };
 use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
 use ark_sponge::{
@@ -248,6 +253,8 @@ pub struct R1CSVerificationCircuit {
   pub eval_vars_at_ry: Fr,
   pub sc_phase1: SumcheckVerificationCircuit,
   pub sc_phase2: SumcheckVerificationCircuit,
+  // The point on which the polynomial was evaluated by the prover.
+  pub claimed_ry: Vec<Scalar>,
 }
 
 impl R1CSVerificationCircuit {
@@ -268,6 +275,7 @@ impl R1CSVerificationCircuit {
       sc_phase2: SumcheckVerificationCircuit {
         polys: config.polys_sc2.clone(),
       },
+      claimed_ry: config.ry.clone(),
     }
   }
 }
@@ -294,7 +302,13 @@ impl ConstraintSynthesizer<Fr> for R1CSVerificationCircuit {
     let input_vars = self
       .input
       .iter()
-      .map(|i| FpVar::<Fr>::new_input(cs.clone(), || Ok(i)).unwrap())
+      .map(|i| FpVar::<Fr>::new_variable(cs.clone(), || Ok(i), AllocationMode::Witness).unwrap())
+      .collect::<Vec<FpVar<Fr>>>();
+
+    let claimed_ry_vars = self
+      .claimed_ry
+      .iter()
+      .map(|r| FpVar::<Fr>::new_variable(cs.clone(), || Ok(r), AllocationMode::Input).unwrap())
       .collect::<Vec<FpVar<Fr>>>();
 
     transcript_var.append_vector(&input_vars)?;
@@ -344,6 +358,17 @@ impl ConstraintSynthesizer<Fr> for R1CSVerificationCircuit {
         .sc_phase2
         .verifiy_sumcheck(&poly_sc2_vars, &claim_phase2_var, &mut transcript_var)?;
 
+    //  Because the verifier checks the commitment opening on point ry outside
+    //  the circuit, the prover needs to send ry to the verifier (making the
+    //  proof size O(log n)). As this point is normally obtained by the verifier
+    //  from the second round of sumcheck, the circuit needs to ensure the
+    //  claimed point, coming from the prover, is actually the point derived
+    //  inside the circuit. These additional checks will be removed
+    //  when the commitment verification is done inside the circuit.
+    for (i, r) in claimed_ry_vars.iter().enumerate() {
+      ry_var[i].enforce_equal(r)?;
+    }
+
     let input_as_sparse_poly_var = SparsePolynomialVar::new_variable(
       cs.clone(),
       || Ok(&self.input_as_sparse_poly),
@@ -366,7 +391,6 @@ impl ConstraintSynthesizer<Fr> for R1CSVerificationCircuit {
     let scalar_var = &r_A_var * &eval_A_r_var + &r_B_var * &eval_B_r_var + &r_C_var * &eval_C_r_var;
 
     let expected_claim_post_phase2_var = eval_Z_at_ry_var * scalar_var;
-
     claim_post_phase2_var.enforce_equal(&expected_claim_post_phase2_var)?;
 
     Ok(())
@@ -386,15 +410,16 @@ pub struct VerifierConfig {
   pub eval_vars_at_ry: Fr,
   pub polys_sc1: Vec<UniPoly>,
   pub polys_sc2: Vec<UniPoly>,
+  pub ry: Vec<Scalar>,
 }
 #[derive(Clone)]
 pub struct VerifierCircuit {
   pub inner_circuit: R1CSVerificationCircuit,
   pub inner_proof: GrothProof<I>,
   pub inner_vk: PreparedVerifyingKey<I>,
-  pub evals_var_at_ry: Fr,
+  pub eval_vars_at_ry: Fr,
   pub claims_phase2: (Fr, Fr, Fr, Fr),
-  pub input: Vec<Fr>,
+  pub ry: Vec<Fr>,
 }
 
 impl VerifierCircuit {
@@ -410,9 +435,9 @@ impl VerifierCircuit {
       inner_circuit,
       inner_proof: proof,
       inner_vk: pvk,
-      evals_var_at_ry: config.eval_vars_at_ry,
+      eval_vars_at_ry: config.eval_vars_at_ry,
       claims_phase2: config.claims_phase2,
-      input: config.input.clone(),
+      ry: config.ry.clone(),
     })
   }
 }
@@ -421,8 +446,10 @@ impl ConstraintSynthesizer<Fq> for VerifierCircuit {
   fn generate_constraints(self, cs: ConstraintSystemRef<Fq>) -> ark_relations::r1cs::Result<()> {
     let proof_var = ProofVar::<I, IV>::new_witness(cs.clone(), || Ok(self.inner_proof.clone()))?;
     let (v_A, v_B, v_C, v_AB) = self.claims_phase2;
-    let mut pubs = self.input.clone();
-    pubs.extend(vec![v_A, v_B, v_C, v_AB, self.evals_var_at_ry]);
+    let mut pubs = vec![];
+    pubs.extend(self.ry);
+    pubs.extend(vec![v_A, v_B, v_C, v_AB]);
+    pubs.extend(vec![self.eval_vars_at_ry]);
     let bits = pubs
       .iter()
       .map(|c| {

src/dense_mlpoly.rs

@@ -1,4 +1,5 @@
 #![allow(clippy::too_many_arguments)]
+use crate::group::Fr;
 use crate::poseidon_transcript::{AppendToPoseidon, PoseidonTranscript};
 
 use super::commitments::{Commitments, MultiCommitGens};
@@ -12,32 +13,198 @@ use super::nizk::{DotProductProofGens, DotProductProofLog};
 use super::random::RandomTape;
 use super::scalar::Scalar;
 use super::transcript::{AppendToTranscript, ProofTranscript};
-use ark_ff::{One, Zero};
+use ark_bls12_377::Bls12_377 as I;
+use ark_ff::{One, UniformRand, Zero};
+use ark_poly::{DenseMultilinearExtension, MultilinearExtension};
+use ark_poly_commit::multilinear_pc::data_structures::{
+  CommitterKey, UniversalParams, VerifierKey,
+};
+use ark_poly_commit::multilinear_pc::MultilinearPC;
 use ark_serialize::*;
 use core::ops::Index;
 use merlin::Transcript;
+use std::ops::{Add, AddAssign, Neg, Sub, SubAssign};
+use std::process::abort;
 
 #[cfg(feature = "multicore")]
 use rayon::prelude::*;
 
-#[derive(Debug)]
+// TODO: integrate the DenseMultilinearExtension(and Sparse) https://github.com/arkworks-rs/algebra/tree/master/poly/src/evaluations/multivariate/multilinear from arkworks into Spartan. This requires moving the specific Spartan functionalities in separate traits.
+#[derive(Debug, Clone, Eq, PartialEq, Hash, CanonicalDeserialize, CanonicalSerialize)]
 pub struct DensePolynomial {
   num_vars: usize, // the number of variables in the multilinear polynomial
   len: usize,
   Z: Vec<Scalar>, // evaluations of the polynomial in all the 2^num_vars Boolean inputs
 }
 
+impl MultilinearExtension<Scalar> for DensePolynomial {
+  fn num_vars(&self) -> usize {
+    self.get_num_vars()
+  }
+
+  fn evaluate(&self, point: &[Scalar]) -> Option<Scalar> {
+    if point.len() == self.num_vars {
+      Some(self.evaluate(&point))
+    } else {
+      None
+    }
+  }
+
+  fn rand<R: rand::Rng>(num_vars: usize, rng: &mut R) -> Self {
+    let evals = (0..(1 << num_vars)).map(|_| Scalar::rand(rng)).collect();
+    Self {
+      num_vars: num_vars,
+      len: 1 << num_vars,
+      Z: evals,
+    }
+  }
+
+  fn relabel(&self, a: usize, b: usize, k: usize) -> Self {
+    unimplemented!()
+  }
+
+  fn fix_variables(&self, partial_point: &[Scalar]) -> Self {
+    unimplemented!()
+  }
+
+  fn to_evaluations(&self) -> Vec<Scalar> {
+    self.Z.to_vec()
+  }
+}
+
+impl Zero for DensePolynomial {
+  fn zero() -> Self {
+    Self {
+      num_vars: 0,
+      len: 1,
+      Z: vec![Scalar::zero()],
+    }
+  }
+
+  fn is_zero(&self) -> bool {
+    self.num_vars == 0 && self.len == 1 && self.Z[0].is_zero()
+  }
+}
+
+impl Add for DensePolynomial {
+  type Output = DensePolynomial;
+  fn add(self, other: Self) -> Self {
+    &self + &other
+  }
+}
+
+// function needed because the result might have a different lifetime than the
+// operands
+impl<'a, 'b> Add<&'a DensePolynomial> for &'b DensePolynomial {
+  type Output = DensePolynomial;
+
+  fn add(self, other: &'a DensePolynomial) -> Self::Output {
+    if other.is_zero() {
+      return self.clone();
+    }
+    if self.is_zero() {
+      return other.clone();
+    }
+    assert_eq!(self.num_vars, other.num_vars);
+
+    let res: Vec<Scalar> = self
+      .Z
+      .iter()
+      .zip(other.Z.iter())
+      .map(|(a, b)| *a + *b)
+      .collect();
+    Self::Output {
+      num_vars: self.num_vars,
+      len: self.len,
+      Z: res,
+    }
+  }
+}
+
+impl AddAssign for DensePolynomial {
+  fn add_assign(&mut self, other: Self) {
+    *self = &*self + &other;
+  }
+}
+
+impl<'a, 'b> AddAssign<&'a DensePolynomial> for DensePolynomial {
+  fn add_assign(&mut self, other: &'a DensePolynomial) {
+    *self = &*self + other;
+  }
+}
+
+impl<'a, 'b> AddAssign<(Scalar, &'a DensePolynomial)> for DensePolynomial {
+  fn add_assign(&mut self, (scalar, other): (Scalar, &'a DensePolynomial)) {
+    let other = Self {
+      num_vars: other.num_vars,
+      len: 1 << other.num_vars,
+      Z: other.Z.iter().map(|x| scalar * x).collect(),
+    };
+    *self = &*self + &other;
+  }
+}
+
+impl Neg for DensePolynomial {
+  type Output = DensePolynomial;
+
+  fn neg(self) -> Self::Output {
+    Self::Output {
+      num_vars: self.num_vars,
+      len: self.len,
+      Z: self.Z.iter().map(|x| -*x).collect(),
+    }
+  }
+}
+
+impl Sub for DensePolynomial {
+  type Output = DensePolynomial;
+
+  fn sub(self, other: Self) -> Self::Output {
+    &self - &other
+  }
+}
+
+impl<'a, 'b> Sub<&'a DensePolynomial> for &'b DensePolynomial {
+  type Output = DensePolynomial;
+
+  fn sub(self, other: &'a DensePolynomial) -> Self::Output {
+    self + &other.clone().neg()
+  }
+}
+
+impl SubAssign for DensePolynomial {
+  fn sub_assign(&mut self, other: Self) {
+    *self = &*self - &other;
+  }
+}
+
+impl<'a, 'b> SubAssign<&'a DensePolynomial> for DensePolynomial {
+  fn sub_assign(&mut self, other: &'a DensePolynomial) {
+    *self = &*self - other;
+  }
+}
+
 #[derive(Clone)]
 pub struct PolyCommitmentGens {
   pub gens: DotProductProofGens,
+  pub ck: CommitterKey<I>,
+  pub vk: VerifierKey<I>,
 }
 
 impl PolyCommitmentGens {
-  // the number of variables in the multilinear polynomial
+  // num vars is the number of variables in the multilinear polynomial
+  // this gives the maximum degree bound
   pub fn new(num_vars: usize, label: &'static [u8]) -> PolyCommitmentGens {
     let (_left, right) = EqPolynomial::compute_factored_lens(num_vars);
     let gens = DotProductProofGens::new(right.pow2(), label);
-    PolyCommitmentGens { gens }
+
+    // Generates the SRS and trims it based on the number of variables in the
+    // multilinear polynomial.
+    let mut rng = ark_std::test_rng();
+    let pst_gens = MultilinearPC::<I>::setup(num_vars, &mut rng);
+    let (ck, vk) = MultilinearPC::<I>::trim(&pst_gens, num_vars);
+
+    PolyCommitmentGens { gens, ck, vk }
   }
 }
 
@@ -79,6 +246,9 @@ impl EqPolynomial {
     for j in 0..ell {
       // in each iteration, we double the size of chis
       size *= 2;
+      // TODO: this reverse causes inconsistent evaluation in comparison to the
+      //evaluation function in ark-poly-commit, we should look into this to
+      // avoid the extra constraints in the circuit
       for i in (0..size).rev().step_by(2) {
         // copy each element from the prior iteration twice
         let scalar = evals[i / 2];

src/lib.rs

@@ -328,6 +328,8 @@ pub struct SNARK {
   r1cs_sat_proof: R1CSProof,
   inst_evals: (Scalar, Scalar, Scalar),
   r1cs_eval_proof: R1CSEvalProof,
+  rx: Vec<Scalar>,
+  ry: Vec<Scalar>,
 }
 
 impl SNARK {
@@ -385,7 +387,7 @@ impl SNARK {
           &inst.inst,
           padded_vars.assignment,
           &inputs.assignment,
-          // &gens.gens_r1cs_sat,
+          &gens.gens_r1cs_sat,
           transcript,
           // &mut random_tape,
         )
@@ -432,6 +434,8 @@ impl SNARK {
       r1cs_sat_proof,
       inst_evals,
       r1cs_eval_proof,
+      rx,
+      ry,
     }
   }
 
@@ -441,9 +445,9 @@ impl SNARK {
     comm: &ComputationCommitment,
     input: &InputsAssignment,
     transcript: &mut PoseidonTranscript,
-    _gens: &SNARKGens,
-  ) -> Result<(), ProofVerifyError> {
-    let _timer_verify = Timer::new("SNARK::verify");
+    gens: &SNARKGens,
+  ) -> Result<(u128, u128, u128), ProofVerifyError> {
+    let timer_verify = Timer::new("SNARK::verify");
     // transcript.append_protocol_name(SNARK::protocol_name());
 
     // append a commitment to the computation to the transcript
@@ -452,35 +456,36 @@ impl SNARK {
     let timer_sat_proof = Timer::new("verify_sat_proof");
     assert_eq!(input.assignment.len(), comm.comm.get_num_inputs());
     // let (rx, ry) =
-    self.r1cs_sat_proof.circuit_size(
+    let res = self.r1cs_sat_proof.verify_groth16(
       comm.comm.get_num_vars(),
       comm.comm.get_num_cons(),
       &input.assignment,
       &self.inst_evals,
       transcript,
-      // &gens.gens_r1cs_sat,
+      &gens.gens_r1cs_sat,
     )?;
     timer_sat_proof.stop();
 
     // let timer_eval_proof = Timer::new("verify_eval_proof");
-    // let (Ar, Br, Cr) = &self.inst_evals;
-    // // Ar.append_to_transcript(b"Ar_claim", transcript);
-    // // Br.append_to_transcript(b"Br_claim", transcript);
-    // // Cr.append_to_transcript(b"Cr_claim", transcript);
-    // transcript.append_scalar(&Ar);
-    // transcript.append_scalar(&Br);
-    // transcript.append_scalar(&Cr);
+
+    let (Ar, Br, Cr) = &self.inst_evals;
+    transcript.append_scalar(&Ar);
+    transcript.append_scalar(&Br);
+    transcript.append_scalar(&Cr);
+
+    // TODO: debug this
+    // https://github.com/maramihali/Spartan/issues/6
     // self.r1cs_eval_proof.verify(
     //   &comm.comm,
-    //   &rx,
-    //   &ry,
+    //   &self.rx,
+    //   &self.ry,
     //   &self.inst_evals,
     //   &gens.gens_r1cs_eval,
     //   transcript,
     // )?;
     // timer_eval_proof.stop();
-    // timer_verify.stop();
-    Ok(())
+    timer_verify.stop();
+    Ok(res)
   }
 }
 
@@ -523,7 +528,7 @@ impl NIZK {
     inst: &Instance,
     vars: VarsAssignment,
     input: &InputsAssignment,
-    // gens: &NIZKGens,
+    gens: &NIZKGens,
     transcript: &mut PoseidonTranscript,
   ) -> Self {
     let timer_prove = Timer::new("NIZK::prove");
@@ -550,7 +555,7 @@ impl NIZK {
         &inst.inst,
         padded_vars.assignment,
         &input.assignment,
-        // &gens.gens_r1cs_sat,
+        &gens.gens_r1cs_sat,
         transcript,
         // &mut random_tape,
       );
@@ -573,7 +578,7 @@ impl NIZK {
     inst: &Instance,
     input: &InputsAssignment,
     transcript: &mut PoseidonTranscript,
-    // gens: &NIZKGens,
+    gens: &NIZKGens,
   ) -> Result<usize, ProofVerifyError> {
     let timer_verify = Timer::new("NIZK::verify");
 
@@ -595,7 +600,7 @@ impl NIZK {
       &input.assignment,
       &inst_evals,
       transcript,
-      // &gens.gens_r1cs_sat,
+      &gens.gens_r1cs_sat,
     )?;
 
     // verify if claimed rx and ry are correct
@@ -613,6 +618,7 @@ impl NIZK {
     inst: &Instance,
     input: &InputsAssignment,
     transcript: &mut PoseidonTranscript,
+    gens: &NIZKGens,
   ) -> Result<(u128, u128, u128), ProofVerifyError> {
     let timer_verify = Timer::new("NIZK::verify");
 
@@ -635,7 +641,7 @@ impl NIZK {
       &input.assignment,
       &inst_evals,
       transcript,
-      // &gens.gens_r1cs_sat,
+      &gens.gens_r1cs_sat,
     )?;
 
     // verify if claimed rx and ry are correct
@@ -805,7 +811,7 @@ mod tests {
       .is_ok());
 
     // NIZK public params
-    let _gens = NIZKGens::new(num_cons, num_vars, num_inputs);
+    let gens = NIZKGens::new(num_cons, num_vars, num_inputs);
 
     let params = poseidon_params();
 
@@ -815,14 +821,14 @@ mod tests {
       &inst,
       assignment_vars,
       &assignment_inputs,
-      // &gens,
+      &gens,
       &mut prover_transcript,
     );
 
     // verify the NIZK
     let mut verifier_transcript = PoseidonTranscript::new(&params);
     assert!(proof
-      .verify(&inst, &assignment_inputs, &mut verifier_transcript)
+      .verify_groth16(&inst, &assignment_inputs, &mut verifier_transcript, &gens)
       .is_ok());
   }
 }

src/poseidon_transcript.rs

@@ -1,7 +1,9 @@
 use crate::group::{CompressedGroup, Fr};
 
 use super::scalar::Scalar;
-
+use ark_bls12_377::Bls12_377 as I;
+use ark_poly_commit::multilinear_pc::data_structures::Commitment;
+use ark_serialize::CanonicalSerialize;
 // use ark_r1cs_std::prelude::*;
 use ark_sponge::{
   poseidon::{PoseidonParameters, PoseidonSponge},
@@ -70,3 +72,11 @@ impl AppendToPoseidon for CompressedGroup {
     transcript.append_point(self);
   }
 }
+
+impl AppendToPoseidon for Commitment<I> {
+  fn append_to_poseidon(&self, transcript: &mut PoseidonTranscript) {
+    let mut bytes = Vec::new();
+    self.serialize(&mut bytes).unwrap();
+    transcript.append_bytes(&bytes);
+  }
+}

src/r1csproof.rs

@@ -3,10 +3,13 @@ use crate::constraints::{VerifierCircuit, VerifierConfig};
 use crate::group::{Fq, Fr};
 use crate::math::Math;
 use crate::parameters::poseidon_params;
-use crate::poseidon_transcript::PoseidonTranscript;
+use crate::poseidon_transcript::{AppendToPoseidon, PoseidonTranscript};
 use crate::sumcheck::SumcheckInstanceProof;
-
+use ark_bls12_377::Bls12_377 as I;
 use ark_bw6_761::BW6_761 as P;
+use ark_poly::MultilinearExtension;
+use ark_poly_commit::multilinear_pc::data_structures::{Commitment, Proof};
+use ark_poly_commit::multilinear_pc::MultilinearPC;
 
 use super::commitments::MultiCommitGens;
 use super::dense_mlpoly::{DensePolynomial, EqPolynomial, PolyCommitmentGens};
@@ -28,14 +31,15 @@ use std::time::Instant;
 
 #[derive(CanonicalSerialize, CanonicalDeserialize, Debug)]
 pub struct R1CSProof {
+  // The PST commitment to the multilinear extension of the witness.
+  comm: Commitment<I>,
   sc_proof_phase1: SumcheckInstanceProof,
   claims_phase2: (Scalar, Scalar, Scalar, Scalar),
-  // pok_claims_phase2: (KnowledgeProof, ProductProof),
-  // proof_eq_sc_phase1: EqualityProof,
   sc_proof_phase2: SumcheckInstanceProof,
   eval_vars_at_ry: Scalar,
-  // proof_eval_vars_at_ry: PolyEvalProof,
-  // proof_eq_sc_phase2: EqualityProof,
+  proof_eval_vars_at_ry: Proof<I>,
+  rx: Vec<Scalar>,
+  ry: Vec<Scalar>,
 }
 #[derive(Clone)]
 pub struct R1CSSumcheckGens {
@@ -128,19 +132,27 @@ impl R1CSProof {
     inst: &R1CSInstance,
     vars: Vec<Scalar>,
     input: &[Scalar],
+    gens: &R1CSGens,
     transcript: &mut PoseidonTranscript,
   ) -> (R1CSProof, Vec<Scalar>, Vec<Scalar>) {
     let timer_prove = Timer::new("R1CSProof::prove");
     // we currently require the number of |inputs| + 1 to be at most number of vars
     assert!(input.len() < vars.len());
 
+    // create the multilinear witness polynomial from the satisfying assiment
+    let poly_vars = DensePolynomial::new(vars.clone());
+
+    let timer_commit = Timer::new("polycommit");
+    // commitment to the satisfying witness polynomial
+    let comm = MultilinearPC::<I>::commit(&gens.gens_pc.ck, &poly_vars);
+    comm.append_to_poseidon(transcript);
+    timer_commit.stop();
+
     let c = transcript.challenge_scalar();
     transcript.new_from_state(&c);
 
     transcript.append_scalar_vector(input);
 
-    let poly_vars = DensePolynomial::new(vars.clone());
-
     let timer_sc_proof_phase1 = Timer::new("prove_sc_phase_one");
 
     // append input to variables to create a single vector z
@@ -214,6 +226,19 @@ impl R1CSProof {
     );
     timer_sc_proof_phase2.stop();
 
+    // TODO: modify the polynomial evaluation in Spartan to be consistent
+    // with the evaluation in ark-poly-commit so that reversing is not needed
+    // anymore
+    let timmer_opening = Timer::new("polyopening");
+    let mut dummy = ry[1..].to_vec().clone();
+    dummy.reverse();
+    let proof_eval_vars_at_ry = MultilinearPC::<I>::open(&gens.gens_pc.ck, &poly_vars, &dummy);
+    println!(
+      "proof size (no of quotients): {:?}",
+      proof_eval_vars_at_ry.proofs.len()
+    );
+    timmer_opening.stop();
+
     let timer_polyeval = Timer::new("polyeval");
     let eval_vars_at_ry = poly_vars.evaluate(&ry[1..]);
     timer_polyeval.stop();
@@ -222,10 +247,14 @@ impl R1CSProof {
 
     (
       R1CSProof {
+        comm,
         sc_proof_phase1,
         claims_phase2: (*Az_claim, *Bz_claim, *Cz_claim, prod_Az_Bz_claims),
         sc_proof_phase2,
         eval_vars_at_ry,
+        proof_eval_vars_at_ry,
+        rx: rx.clone(),
+        ry: ry.clone(),
       },
       rx,
       ry,
@@ -239,7 +268,10 @@ impl R1CSProof {
     input: &[Scalar],
     evals: &(Scalar, Scalar, Scalar),
     transcript: &mut PoseidonTranscript,
+    gens: &R1CSGens,
   ) -> Result<(u128, u128, u128), ProofVerifyError> {
+    self.comm.append_to_poseidon(transcript);
+
     let c = transcript.challenge_scalar();
 
     let mut input_as_sparse_poly_entries = vec![SparsePolyEntry::new(0, Scalar::one())];
@@ -266,30 +298,58 @@ impl R1CSProof {
       polys_sc2: self.sc_proof_phase2.polys.clone(),
       eval_vars_at_ry: self.eval_vars_at_ry,
       input_as_sparse_poly,
+      // rx: self.rx.clone(),
+      ry: self.ry.clone(),
     };
 
     let mut rng = ark_std::test_rng();
 
+    let prove_inner = Timer::new("proveinnercircuit");
     let start = Instant::now();
     let circuit = VerifierCircuit::new(&config, &mut rng).unwrap();
     let dp1 = start.elapsed().as_millis();
+    prove_inner.stop();
 
     let start = Instant::now();
     let (pk, vk) = Groth16::<P>::setup(circuit.clone(), &mut rng).unwrap();
     let ds = start.elapsed().as_millis();
 
+    let prove_outer = Timer::new("proveoutercircuit");
     let start = Instant::now();
     let proof = Groth16::<P>::prove(&pk, circuit, &mut rng).unwrap();
     let dp2 = start.elapsed().as_millis();
+    prove_outer.stop();
 
     let start = Instant::now();
     let is_verified = Groth16::<P>::verify(&vk, &[], &proof).unwrap();
-    let dv = start.elapsed().as_millis();
     assert!(is_verified);
 
+    let timer_verification = Timer::new("commitverification");
+    let mut dummy = self.ry[1..].to_vec();
+    // TODO: ensure ark-poly-commit and Spartan produce consistent results
+    // when evaluating a polynomial at a given point so this reverse is not
+    // needed.
+    dummy.reverse();
+
+    // Verifies the proof of opening against the result of evaluating the
+    // witness polynomial at point ry.
+    let res = MultilinearPC::<I>::check(
+      &gens.gens_pc.vk,
+      &self.comm,
+      &dummy,
+      self.eval_vars_at_ry,
+      &self.proof_eval_vars_at_ry,
+    );
+
+    timer_verification.stop();
+    assert!(res == true);
+    let dv = start.elapsed().as_millis();
+
     Ok((ds, dp1 + dp2, dv))
   }
 
+  // Helper function to find the number of constraint in the circuit which
+  // requires executing it.
   pub fn circuit_size(
     &self,
     num_vars: usize,
@@ -297,7 +357,10 @@ impl R1CSProof {
     input: &[Scalar],
     evals: &(Scalar, Scalar, Scalar),
     transcript: &mut PoseidonTranscript,
+    gens: &R1CSGens,
   ) -> Result<usize, ProofVerifyError> {
+    self.comm.append_to_poseidon(transcript);
+
     let c = transcript.challenge_scalar();
 
     let mut input_as_sparse_poly_entries = vec![SparsePolyEntry::new(0, Scalar::one())];
@@ -324,6 +387,8 @@ impl R1CSProof {
       polys_sc2: self.sc_proof_phase2.polys.clone(),
       eval_vars_at_ry: self.eval_vars_at_ry,
       input_as_sparse_poly,
+      // rx: self.rx.clone(),
+      ry: self.ry.clone(),
     };
 
     let mut rng = ark_std::test_rng();
@@ -439,13 +504,13 @@ mod tests {
     let num_inputs = 10;
     let (inst, vars, input) = R1CSInstance::produce_synthetic_r1cs(num_cons, num_vars, num_inputs);
 
-    // let gens = R1CSGens::new(b"test-m", num_cons, num_vars);
+    let gens = R1CSGens::new(b"test-m", num_cons, num_vars);
 
     let params = poseidon_params();
     // let mut random_tape = RandomTape::new(b"proof");
 
     let mut prover_transcript = PoseidonTranscript::new(&params);
-    let (proof, rx, ry) = R1CSProof::prove(&inst, vars, &input, &mut prover_transcript);
+    let (proof, rx, ry) = R1CSProof::prove(&inst, vars, &input, &gens, &mut prover_transcript);
 
     let inst_evals = inst.evaluate(&rx, &ry);
 
@@ -461,6 +526,7 @@ mod tests {
         &input,
         &inst_evals,
         &mut verifier_transcript,
+        &gens,
       )
       .is_ok());
   }