M .github/workflows/testudo.yml → .github/workflows/testudo.yml

@@ -21,8 +21,8 @@ - name: Install
         run: rustup default nightly
       - name: Install rustfmt Components
         run: rustup component add rustfmt
-      - name: Install clippy
-        run: rustup component add clippy
+      # - name: Install clippy
+      #   run: rustup component add clippy
       - name: Build
         run: cargo build --verbose
       - name: Run tests
@@ -32,6 +32,6 @@ run: cargo build --examples --verbose
       - name: Check Rustfmt Code Style
         run: cargo fmt --all -- --check
       # cargo clippy uses cargo check which returns an error when asm is emitted
-      # we want to emit asm for ff operations so we avoid using clippy for now
+      # we want to emit asm for ark-ff operations so we avoid using clippy for # now
       # - name: Check clippy warnings
       #   run: cargo clippy --all-targets --all-features

M src/constraints.rs → src/constraints.rs

@@ -255,6 +255,7 @@ pub sc_phase1: SumcheckVerificationCircuit,
   pub sc_phase2: SumcheckVerificationCircuit,
   // The point on which the polynomial was evaluated by the prover.
   pub claimed_ry: Vec<Scalar>,
+  pub claimed_transcript_sat_state: Scalar,
 }
 
 impl R1CSVerificationCircuit {
@@ -276,6 +277,7 @@ sc_phase2: SumcheckVerificationCircuit {
         polys: config.polys_sc2.clone(),
       },
       claimed_ry: config.ry.clone(),
+      claimed_transcript_sat_state: config.transcript_sat_state,
     }
   }
 }
@@ -386,13 +388,21 @@ let (eval_A_r, eval_B_r, eval_C_r) = self.evals;
 
     let eval_A_r_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(eval_A_r))?;
     let eval_B_r_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(eval_B_r))?;
-    let eval_C_r_var = FpVar::<Fr>::new_witness(cs, || Ok(eval_C_r))?;
+    let eval_C_r_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(eval_C_r))?;
 
     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)?;
 
+    let expected_transcript_state_var = transcript_var.challenge()?;
+    let claimed_transcript_state_var =
+      FpVar::<Fr>::new_input(cs, || Ok(self.claimed_transcript_sat_state))?;
+
+    // Ensure that the prover and verifier transcipt views are consistent at
+    // the end of the satisfiability proof.
+    expected_transcript_state_var.enforce_equal(&claimed_transcript_state_var)?;
+
     Ok(())
   }
 }
@@ -411,6 +421,7 @@ pub eval_vars_at_ry: Fr,
   pub polys_sc1: Vec<UniPoly>,
   pub polys_sc2: Vec<UniPoly>,
   pub ry: Vec<Scalar>,
+  pub transcript_sat_state: Scalar,
 }
 #[derive(Clone)]
 pub struct VerifierCircuit {
@@ -420,6 +431,7 @@ pub inner_vk: PreparedVerifyingKey<I>,
   pub eval_vars_at_ry: Fr,
   pub claims_phase2: (Fr, Fr, Fr, Fr),
   pub ry: Vec<Fr>,
+  pub transcript_sat_state: Scalar,
 }
 
 impl VerifierCircuit {
@@ -438,6 +450,7 @@ inner_vk: pvk,
       eval_vars_at_ry: config.eval_vars_at_ry,
       claims_phase2: config.claims_phase2,
       ry: config.ry.clone(),
+      transcript_sat_state: config.transcript_sat_state,
     })
   }
 }
@@ -449,7 +462,8 @@ let (v_A, v_B, v_C, v_AB) = self.claims_phase2;
     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]);
+    pubs.extend(vec![self.eval_vars_at_ry, self.transcript_sat_state]);
+
     let bits = pubs
       .iter()
       .map(|c| {

M src/lib.rs → src/lib.rs

@@ -42,6 +42,7 @@ mod constraints;
 pub mod poseidon_transcript;
 
 use ark_ff::Field;
+use ark_relations::r1cs;
 use ark_serialize::*;
 use ark_std::Zero;
 use core::cmp::max;
@@ -400,6 +401,13 @@
       (proof, rx, ry)
     };
 
+    // We need to reset the transcript state before starting the evaluation
+    // proof and share this state with the verifier because, on the verifier's
+    // side all the previous updates are done on the transcript
+    // circuit variable and the transcript outside the circuit will be
+    // inconsistent wrt to the prover's.
+    transcript.new_from_state(&r1cs_sat_proof.transcript_sat_state);
+
     // We send evaluations of A, B, C at r = (rx, ry) as claims
     // to enable the verifier complete the first sum-check
     let timer_eval = Timer::new("eval_sparse_polys");
@@ -466,24 +474,27 @@ &gens.gens_r1cs_sat,
     )?;
     timer_sat_proof.stop();
 
-    // let timer_eval_proof = Timer::new("verify_eval_proof");
+    let timer_eval_proof = Timer::new("verify_eval_proof");
+    // Reset the transcript using the state sent by the prover.
+    // TODO: find a way to retrieve this state from the circuit. Currently
+    // the API for generating constraints doesn't support returning values
+    // computed inside the circuit.
+    transcript.new_from_state(&self.r1cs_sat_proof.transcript_sat_state);
 
     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,
-    //   &self.rx,
-    //   &self.ry,
-    //   &self.inst_evals,
-    //   &gens.gens_r1cs_eval,
-    //   transcript,
-    // )?;
-    // timer_eval_proof.stop();
+    self.r1cs_eval_proof.verify(
+      &comm.comm,
+      &self.rx,
+      &self.ry,
+      &self.inst_evals,
+      &gens.gens_r1cs_eval,
+      transcript,
+    )?;
+    timer_eval_proof.stop();
     timer_verify.stop();
     Ok(res)
   }

M src/r1csproof.rs → src/r1csproof.rs

@@ -40,6 +40,8 @@ eval_vars_at_ry: Scalar,
   proof_eval_vars_at_ry: Proof<I>,
   rx: Vec<Scalar>,
   ry: Vec<Scalar>,
+  // The transcript state after the satisfiability proof was computed.
+  pub transcript_sat_state: Scalar,
 }
 #[derive(Clone)]
 pub struct R1CSSumcheckGens {
@@ -245,6 +247,8 @@ timer_polyeval.stop();
 
     timer_prove.stop();
 
+    let c = transcript.challenge_scalar();
+
     (
       R1CSProof {
         comm,
@@ -255,6 +259,7 @@ eval_vars_at_ry,
         proof_eval_vars_at_ry,
         rx: rx.clone(),
         ry: ry.clone(),
+        transcript_sat_state: c,
       },
       rx,
       ry,
@@ -300,6 +305,7 @@ eval_vars_at_ry: self.eval_vars_at_ry,
       input_as_sparse_poly,
       // rx: self.rx.clone(),
       ry: self.ry.clone(),
+      transcript_sat_state: self.transcript_sat_state,
     };
 
     let mut rng = ark_std::test_rng();
@@ -389,6 +395,7 @@ eval_vars_at_ry: self.eval_vars_at_ry,
       input_as_sparse_poly,
       // rx: self.rx.clone(),
       ry: self.ry.clone(),
+      transcript_sat_state: self.transcript_sat_state,
     };
 
     let mut rng = ark_std::test_rng();