Skip to main content

nova_snark/spartan/
snark.rs

1//! This module implements `RelaxedR1CSSNARKTrait` using Spartan that is generic
2//! over the polynomial commitment and evaluation argument (i.e., a PCS)
3//! This version of Spartan does not use preprocessing so the verifier keeps the entire
4//! description of R1CS matrices. This is essentially optimal for the verifier when using
5//! an IPA-based polynomial commitment scheme.
6
7use crate::{
8  digest::{DigestComputer, SimpleDigestible},
9  errors::NovaError,
10  r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness, SparseMatrix},
11  spartan::{
12    compute_eval_table_sparse,
13    math::Math,
14    polys::{eq::EqPolynomial, multilinear::MultilinearPolynomial, multilinear::SparsePolynomial},
15    sumcheck::SumcheckProof,
16    PolyEvalInstance, PolyEvalWitness,
17  },
18  traits::{
19    evaluation::EvaluationEngineTrait,
20    snark::{DigestHelperTrait, RelaxedR1CSSNARKTrait},
21    Engine, TranscriptEngineTrait,
22  },
23  CommitmentKey,
24};
25use ff::Field;
26use once_cell::sync::OnceCell;
27use rayon::prelude::*;
28use serde::{Deserialize, Serialize};
29
30/// A type that represents the prover's key
31#[derive(Serialize, Deserialize)]
32#[serde(bound = "")]
33pub struct ProverKey<E: Engine, EE: EvaluationEngineTrait<E>> {
34  pk_ee: EE::ProverKey,
35  vk_digest: E::Scalar, // digest of the verifier's key
36}
37
38/// A type that represents the verifier's key
39#[derive(Serialize, Deserialize)]
40#[serde(bound = "")]
41pub struct VerifierKey<E: Engine, EE: EvaluationEngineTrait<E>> {
42  vk_ee: EE::VerifierKey,
43  S: R1CSShape<E>,
44  #[serde(skip, default = "OnceCell::new")]
45  digest: OnceCell<E::Scalar>,
46}
47
48impl<E: Engine, EE: EvaluationEngineTrait<E>> SimpleDigestible for VerifierKey<E, EE> {}
49
50impl<E: Engine, EE: EvaluationEngineTrait<E>> VerifierKey<E, EE> {
51  fn new(shape: R1CSShape<E>, vk_ee: EE::VerifierKey) -> Self {
52    VerifierKey {
53      vk_ee,
54      S: shape,
55      digest: OnceCell::new(),
56    }
57  }
58}
59
60impl<E: Engine, EE: EvaluationEngineTrait<E>> DigestHelperTrait<E> for VerifierKey<E, EE> {
61  /// Returns the digest of the verifier's key.
62  fn digest(&self) -> E::Scalar {
63    self
64      .digest
65      .get_or_try_init(|| {
66        let dc = DigestComputer::<E::Scalar, _>::new(self);
67        dc.digest()
68      })
69      .cloned()
70      .expect("Failure to retrieve digest!")
71  }
72}
73
74/// A succinct proof of knowledge of a witness to a relaxed R1CS instance
75/// The proof is produced using Spartan's combination of the sum-check and
76/// the commitment to a vector viewed as a polynomial commitment
77#[derive(Debug, Serialize, Deserialize)]
78#[serde(bound = "")]
79pub struct RelaxedR1CSSNARK<E: Engine, EE: EvaluationEngineTrait<E>> {
80  sc_proof_outer: SumcheckProof<E>,
81  claims_outer: (E::Scalar, E::Scalar, E::Scalar),
82  eval_E: E::Scalar,
83  sc_proof_inner: SumcheckProof<E>,
84  eval_W: E::Scalar,
85  sc_proof_batch: SumcheckProof<E>,
86  evals_batch: Vec<E::Scalar>,
87  eval_arg: EE::EvaluationArgument,
88}
89
90impl<E: Engine, EE: EvaluationEngineTrait<E>> RelaxedR1CSSNARKTrait<E> for RelaxedR1CSSNARK<E, EE> {
91  type ProverKey = ProverKey<E, EE>;
92  type VerifierKey = VerifierKey<E, EE>;
93
94  fn setup(
95    ck: &CommitmentKey<E>,
96    S: &R1CSShape<E>,
97  ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> {
98    let (pk_ee, vk_ee) = EE::setup(ck)?;
99
100    let S = S.pad();
101
102    let vk: VerifierKey<E, EE> = VerifierKey::new(S, vk_ee);
103
104    let pk = ProverKey {
105      pk_ee,
106      vk_digest: vk.digest(),
107    };
108
109    Ok((pk, vk))
110  }
111
112  /// produces a succinct proof of satisfiability of a `RelaxedR1CS` instance
113  fn prove(
114    ck: &CommitmentKey<E>,
115    pk: &Self::ProverKey,
116    S: &R1CSShape<E>,
117    U: &RelaxedR1CSInstance<E>,
118    W: &RelaxedR1CSWitness<E>,
119  ) -> Result<Self, NovaError> {
120    // pad the R1CSShape
121    let S = S.pad();
122    // sanity check that R1CSShape has all required size characteristics
123    assert!(S.is_regular_shape());
124
125    let W = W.pad(&S); // pad the witness
126    let mut transcript = E::TE::new(b"RelaxedR1CSSNARK");
127
128    // append the digest of vk (which includes R1CS matrices) and the RelaxedR1CSInstance to the transcript
129    transcript.absorb(b"vk", &pk.vk_digest);
130    transcript.absorb(b"U", U);
131
132    // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
133    let mut z = [W.W.clone(), vec![U.u], U.X.clone()].concat();
134
135    let (num_rounds_x, num_rounds_y) = (
136      usize::try_from(S.num_cons.ilog2()).unwrap(),
137      (usize::try_from(S.num_vars.ilog2()).unwrap() + 1),
138    );
139
140    // outer sum-check
141    let tau = (0..num_rounds_x)
142      .map(|_i| transcript.squeeze(b"t"))
143      .collect::<Result<Vec<_>, NovaError>>()?;
144
145    let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = {
146      let (poly_Az, poly_Bz, poly_Cz) = S.multiply_vec(&z)?;
147      let poly_uCz_E = (0..S.num_cons)
148        .map(|i| U.u * poly_Cz[i] + W.E[i])
149        .collect::<Vec<E::Scalar>>();
150      (
151        MultilinearPolynomial::new(poly_Az),
152        MultilinearPolynomial::new(poly_Bz),
153        MultilinearPolynomial::new(poly_Cz),
154        MultilinearPolynomial::new(poly_uCz_E),
155      )
156    };
157
158    let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_three_inputs(
159      &E::Scalar::ZERO, // claim is zero
160      tau,
161      &mut poly_Az,
162      &mut poly_Bz,
163      &mut poly_uCz_E,
164      &mut transcript,
165    )?;
166
167    // claims from the end of sum-check
168    let (claim_Az, claim_Bz): (E::Scalar, E::Scalar) = (claims_outer[0], claims_outer[1]);
169    let claim_Cz = poly_Cz.evaluate(&r_x);
170    let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x);
171    transcript.absorb(
172      b"claims_outer",
173      &[claim_Az, claim_Bz, claim_Cz, eval_E].as_slice(),
174    );
175
176    // inner sum-check
177    let r = transcript.squeeze(b"r")?;
178    let claim_inner_joint = claim_Az + r * claim_Bz + r * r * claim_Cz;
179
180    let poly_ABC = {
181      // compute the initial evaluation table for R(\tau, x)
182      let evals_rx = EqPolynomial::evals_from_points(&r_x.clone());
183
184      let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&S, &evals_rx);
185
186      assert_eq!(evals_A.len(), evals_B.len());
187      assert_eq!(evals_A.len(), evals_C.len());
188      (0..evals_A.len())
189        .into_par_iter()
190        .map(|i| evals_A[i] + r * evals_B[i] + r * r * evals_C[i])
191        .collect::<Vec<E::Scalar>>()
192    };
193
194    let poly_z = {
195      z.resize(S.num_vars * 2, E::Scalar::ZERO);
196      z
197    };
198
199    let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad_prod(
200      &claim_inner_joint,
201      num_rounds_y,
202      &mut MultilinearPolynomial::new(poly_ABC),
203      &mut MultilinearPolynomial::new(poly_z),
204      &mut transcript,
205    )?;
206
207    // Add additional claims about W and E polynomials to the list from CC
208    // We will reduce a vector of claims of evaluations at different points into claims about them at the same point.
209    // For example, eval_W =? W(r_y[1..]) and eval_E =? E(r_x) into
210    // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz)
211    // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz),
212    // where gamma is a public challenge
213    // Since commitments to W and E are homomorphic, the verifier can compute a commitment
214    // to the batched polynomial.
215    let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_y[1..]);
216
217    let w_vec = vec![PolyEvalWitness { p: W.W }, PolyEvalWitness { p: W.E }];
218    let u_vec = vec![
219      PolyEvalInstance {
220        c: U.comm_W,
221        x: r_y[1..].to_vec(),
222        e: eval_W,
223      },
224      PolyEvalInstance {
225        c: U.comm_E,
226        x: r_x,
227        e: eval_E,
228      },
229    ];
230
231    let (batched_u, batched_w, _chal, sc_proof_batch, claims_batch_left) =
232      super::batch_eval_reduce(u_vec, w_vec, &mut transcript)?;
233
234    let eval_arg = EE::prove(
235      ck,
236      &pk.pk_ee,
237      &mut transcript,
238      &batched_u.c,
239      &batched_w.p,
240      &batched_u.x,
241      &batched_u.e,
242    )?;
243
244    Ok(RelaxedR1CSSNARK {
245      sc_proof_outer,
246      claims_outer: (claim_Az, claim_Bz, claim_Cz),
247      eval_E,
248      sc_proof_inner,
249      eval_W,
250      sc_proof_batch,
251      evals_batch: claims_batch_left,
252      eval_arg,
253    })
254  }
255
256  /// verifies a proof of satisfiability of a `RelaxedR1CS` instance
257  fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<E>) -> Result<(), NovaError> {
258    let mut transcript = E::TE::new(b"RelaxedR1CSSNARK");
259
260    // append the digest of R1CS matrices and the RelaxedR1CSInstance to the transcript
261    transcript.absorb(b"vk", &vk.digest());
262    transcript.absorb(b"U", U);
263
264    let (num_rounds_x, num_rounds_y) = (
265      usize::try_from(vk.S.num_cons.ilog2()).unwrap(),
266      (usize::try_from(vk.S.num_vars.ilog2()).unwrap() + 1),
267    );
268
269    // outer sum-check
270    let tau = (0..num_rounds_x)
271      .map(|_i| transcript.squeeze(b"t"))
272      .collect::<Result<EqPolynomial<_>, NovaError>>()?;
273
274    let (claim_outer_final, r_x) =
275      self
276        .sc_proof_outer
277        .verify(E::Scalar::ZERO, num_rounds_x, 3, &mut transcript)?;
278
279    // verify claim_outer_final
280    let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer;
281    let taus_bound_rx = tau.evaluate(&r_x);
282    let claim_outer_final_expected =
283      taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E);
284    if claim_outer_final != claim_outer_final_expected {
285      return Err(NovaError::InvalidSumcheckProof);
286    }
287
288    transcript.absorb(
289      b"claims_outer",
290      &[
291        self.claims_outer.0,
292        self.claims_outer.1,
293        self.claims_outer.2,
294        self.eval_E,
295      ]
296      .as_slice(),
297    );
298
299    // inner sum-check
300    let r = transcript.squeeze(b"r")?;
301    let claim_inner_joint =
302      self.claims_outer.0 + r * self.claims_outer.1 + r * r * self.claims_outer.2;
303
304    let (claim_inner_final, r_y) =
305      self
306        .sc_proof_inner
307        .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?;
308
309    // verify claim_inner_final
310    let eval_Z = {
311      let eval_X = {
312        // public IO is (u, X)
313        let X = vec![U.u]
314          .into_iter()
315          .chain(U.X.iter().cloned())
316          .collect::<Vec<E::Scalar>>();
317        SparsePolynomial::new(vk.S.num_vars.log_2(), X).evaluate(&r_y[1..])
318      };
319      (E::Scalar::ONE - r_y[0]) * self.eval_W + r_y[0] * eval_X
320    };
321
322    // compute evaluations of R1CS matrices
323    let multi_evaluate = |M_vec: &[&SparseMatrix<E::Scalar>],
324                          r_x: &[E::Scalar],
325                          r_y: &[E::Scalar]|
326     -> Vec<E::Scalar> {
327      let evaluate_with_table =
328        |M: &SparseMatrix<E::Scalar>, T_x: &[E::Scalar], T_y: &[E::Scalar]| -> E::Scalar {
329          M.indptr
330            .par_windows(2)
331            .enumerate()
332            .map(|(row_idx, ptrs)| {
333              M.get_row_unchecked(ptrs.try_into().unwrap())
334                .map(|(val, col_idx)| T_x[row_idx] * T_y[*col_idx] * val)
335                .sum::<E::Scalar>()
336            })
337            .sum()
338        };
339
340      let (T_x, T_y) = rayon::join(
341        || EqPolynomial::evals_from_points(r_x),
342        || EqPolynomial::evals_from_points(r_y),
343      );
344
345      (0..M_vec.len())
346        .into_par_iter()
347        .map(|i| evaluate_with_table(M_vec[i], &T_x, &T_y))
348        .collect()
349    };
350
351    let evals = multi_evaluate(&[&vk.S.A, &vk.S.B, &vk.S.C], &r_x, &r_y);
352
353    let claim_inner_final_expected = (evals[0] + r * evals[1] + r * r * evals[2]) * eval_Z;
354    if claim_inner_final != claim_inner_final_expected {
355      return Err(NovaError::InvalidSumcheckProof);
356    }
357
358    // add claims about W and E polynomials
359    let u_vec: Vec<PolyEvalInstance<E>> = vec![
360      PolyEvalInstance {
361        c: U.comm_W,
362        x: r_y[1..].to_vec(),
363        e: self.eval_W,
364      },
365      PolyEvalInstance {
366        c: U.comm_E,
367        x: r_x,
368        e: self.eval_E,
369      },
370    ];
371
372    let (batched_u, _chal) = super::batch_eval_verify(
373      u_vec,
374      &mut transcript,
375      &self.sc_proof_batch,
376      &self.evals_batch,
377    )?;
378
379    // verify
380    EE::verify(
381      &vk.vk_ee,
382      &mut transcript,
383      &batched_u.c,
384      &batched_u.x,
385      &batched_u.e,
386      &self.eval_arg,
387    )?;
388
389    Ok(())
390  }
391}