Merge pull request #33 from cryptonetlab/benchmarks

update benchmarks and add missing constraints to circuit

Author: maramihali

src/constraints.rs

@@ -229,6 +229,7 @@ pub struct R1CSVerificationCircuit<F: PrimeField> {
   pub sc_phase1: SumcheckVerificationCircuit<F>,
   pub sc_phase2: SumcheckVerificationCircuit<F>,
   // The point on which the polynomial was evaluated by the prover.
+  pub claimed_rx: Vec<F>,
   pub claimed_ry: Vec<F>,
   pub claimed_transcript_sat_state: F,
 }
@@ -251,6 +252,7 @@ impl<F: PrimeField> R1CSVerificationCircuit<F> {
       sc_phase2: SumcheckVerificationCircuit {
         polys: config.polys_sc2.clone(),
       },
+      claimed_rx: config.rx.clone(),
       claimed_ry: config.ry.clone(),
       claimed_transcript_sat_state: config.transcript_sat_state,
     }
@@ -284,6 +286,12 @@ impl<F: PrimeField> ConstraintSynthesizer<F> for R1CSVerificationCircuit<F> {
       .map(|i| FpVar::<F>::new_variable(cs.clone(), || Ok(i), AllocationMode::Input).unwrap())
       .collect::<Vec<FpVar<F>>>();
 
+    let claimed_rx_vars = self
+      .claimed_rx
+      .iter()
+      .map(|r| FpVar::<F>::new_variable(cs.clone(), || Ok(r), AllocationMode::Input).unwrap())
+      .collect::<Vec<FpVar<F>>>();
+
     let claimed_ry_vars = self
       .claimed_ry
       .iter()
@@ -304,6 +312,13 @@ impl<F: PrimeField> ConstraintSynthesizer<F> for R1CSVerificationCircuit<F> {
         .sc_phase1
         .verifiy_sumcheck(&poly_sc1_vars, &claim_phase1_var, &mut transcript_var)?;
 
+    // The prover sends (rx, ry) to the verifier for the evaluation proof so
+    // the constraints need to ensure it is indeed the result from the first
+    // round of sumcheck verification.
+    for (i, r) in claimed_rx_vars.iter().enumerate() {
+      rx_var[i].enforce_equal(r)?;
+    }
+
     let (Az_claim, Bz_claim, Cz_claim, prod_Az_Bz_claims) = &self.claims_phase2;
 
     let Az_claim_var = FpVar::<F>::new_witness(cs.clone(), || Ok(Az_claim))?;
@@ -344,6 +359,7 @@ impl<F: PrimeField> ConstraintSynthesizer<F> for R1CSVerificationCircuit<F> {
     //  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.
+    //  Moreover, (rx, ry) will be used in the evaluation proof.
     for (i, r) in claimed_ry_vars.iter().enumerate() {
       ry_var[i].enforce_equal(r)?;
     }
@@ -401,6 +417,7 @@ pub struct VerifierConfig<E: Pairing> {
   pub eval_vars_at_ry: E::ScalarField,
   pub polys_sc1: Vec<UniPoly<E::ScalarField>>,
   pub polys_sc2: Vec<UniPoly<E::ScalarField>>,
+  pub rx: Vec<E::ScalarField>,
   pub ry: Vec<E::ScalarField>,
   pub transcript_sat_state: E::ScalarField,
 }

src/r1csproof.rs

@@ -58,7 +58,6 @@ pub struct R1CSVerifierProof<E: Pairing> {
   initial_state: E::ScalarField,
   transcript_sat_state: E::ScalarField,
   eval_vars_at_ry: E::ScalarField,
-  ry: Vec<E::ScalarField>,
   proof_eval_vars_at_ry: Proof<E>,
   t: E::TargetField,
   mipp_proof: MippProof<E>,
@@ -138,6 +137,9 @@ where
       sc_phase2: SumcheckVerificationCircuit {
         polys: uni_polys_round2,
       },
+      claimed_rx: (0..num_cons.log_2())
+        .map(|_i| E::ScalarField::rand(&mut rng))
+        .collect_vec(),
       claimed_ry: (0..num_vars.log_2() + 1)
         .map(|_i| E::ScalarField::rand(&mut rng))
         .collect_vec(),
@@ -407,6 +409,7 @@ where
       eval_vars_at_ry: self.eval_vars_at_ry,
       input_as_sparse_poly,
       comm: self.comm.clone(),
+      rx: self.rx.clone(),
       ry: self.ry.clone(),
       transcript_sat_state: self.transcript_sat_state,
     };
@@ -423,7 +426,6 @@ where
       initial_state: self.initial_state,
       transcript_sat_state: self.transcript_sat_state,
       eval_vars_at_ry: self.eval_vars_at_ry,
-      ry: self.ry.clone(),
       proof_eval_vars_at_ry: self.proof_eval_vars_at_ry.clone(),
       t: self.t,
       mipp_proof: self.mipp_proof.clone(),
@@ -439,15 +441,18 @@ where
   // commitment opening.
   pub fn verify(
     &self,
+    r: (Vec<E::ScalarField>, Vec<E::ScalarField>),
     input: &[E::ScalarField],
     evals: &(E::ScalarField, E::ScalarField, E::ScalarField),
     transcript: &mut PoseidonTranscript<E::ScalarField>,
     gens: &R1CSGens<E>,
   ) -> Result<bool, ProofVerifyError> {
+    let (rx, ry) = &r;
     let (Ar, Br, Cr) = evals;
     let mut pubs = vec![self.initial_state];
     pubs.extend(input.clone());
-    pubs.extend(self.ry.clone());
+    pubs.extend(rx.clone());
+    pubs.extend(ry.clone());
     pubs.extend(vec![
       self.eval_vars_at_ry,
       *Ar,
@@ -466,7 +471,7 @@ where
         transcript,
         &gens.gens_pc.vk,
         &self.comm,
-        &self.ry[1..],
+        &ry[1..],
         self.eval_vars_at_ry,
         &self.proof_eval_vars_at_ry,
         &self.mipp_proof,
@@ -616,7 +621,13 @@ mod tests {
 
     let mut verifier_transcript = PoseidonTranscript::new(&params.clone());
     assert!(verifer_proof
-      .verify(&input, &inst_evals, &mut verifier_transcript, &gens)
+      .verify(
+        (rx, ry),
+        &input,
+        &inst_evals,
+        &mut verifier_transcript,
+        &gens
+      )
       .is_ok());
   }
 }

src/testudo_nizk.rs

@@ -126,7 +126,7 @@ where
 
   // Verifies the satisfiability proof for the R1CS instance. In NIZK mode, the
   // verifier evaluates matrices A, B and C themselves, which is a linear
-  // operation and hence this is not a SNARK. 
+  // operation and hence this is not a SNARK.
   // However, for highly structured circuits this operation is fast.
   pub fn verify(
     &self,
@@ -141,6 +141,7 @@ where
     let inst_evals = inst.inst.evaluate(claimed_rx, claimed_ry);
 
     let sat_verified = self.r1cs_verifier_proof.verify(
+      (claimed_rx.clone(), claimed_ry.clone()),
       &input.assignment,
       &inst_evals,
       transcript,

src/testudo_snark.rs

@@ -202,8 +202,11 @@ where
     transcript: &mut PoseidonTranscript<E::ScalarField>,
     _poseidon: PoseidonConfig<E::ScalarField>,
   ) -> Result<bool, ProofVerifyError> {
+    let (rx, ry) = &self.r;
+
     let timer_sat_verification = Timer::new("r1cs_sat_verification");
     let sat_verified = self.r1cs_verifier_proof.verify(
+      (rx.clone(), ry.clone()),
       &input.assignment,
       &self.inst_evals,
       transcript,
@@ -217,7 +220,6 @@ where
     transcript.append_scalar(b"", Br);
     transcript.append_scalar(b"", Cr);
 
-    let (rx, ry) = &self.r;
     let timer_eval_verification = Timer::new("r1cs_eval_verification");
     let eval_verified = self.r1cs_eval_proof.verify(
       &comm.comm,