Nova/src/spartan/snark.rs
src/spartan/snark.rsRaw
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 compute_digest,
9 errors::NovaError,
10 r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
11 spartan::{
12 polynomial::{EqPolynomial, MultilinearPolynomial, SparsePolynomial},
13 powers,
14 sumcheck::SumcheckProof,
15 PolyEvalInstance, PolyEvalWitness,
16 },
17 traits::{
18 evaluation::EvaluationEngineTrait, snark::RelaxedR1CSSNARKTrait, Group, TranscriptEngineTrait,
19 },
20 Commitment, CommitmentKey,
21};
22use ff::Field;
23use itertools::concat;
24use rayon::prelude::*;
25use serde::{Deserialize, Serialize};
26
27/// A type that represents the prover's key
28#[derive(Serialize, Deserialize)]
29#[serde(bound = "")]
30pub struct ProverKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
31 pk_ee: EE::ProverKey,
32 S: R1CSShape<G>,
33 vk_digest: G::Scalar, // digest of the verifier's key
34}
35
36/// A type that represents the verifier's key
37#[derive(Serialize, Deserialize)]
38#[serde(bound = "")]
39pub struct VerifierKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
40 vk_ee: EE::VerifierKey,
41 S: R1CSShape<G>,
42 digest: G::Scalar,
43}
44
45/// A succinct proof of knowledge of a witness to a relaxed R1CS instance
46/// The proof is produced using Spartan's combination of the sum-check and
47/// the commitment to a vector viewed as a polynomial commitment
48#[derive(Serialize, Deserialize)]
49#[serde(bound = "")]
50pub struct RelaxedR1CSSNARK<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
51 sc_proof_outer: SumcheckProof<G>,
52 claims_outer: (G::Scalar, G::Scalar, G::Scalar),
53 eval_E: G::Scalar,
54 sc_proof_inner: SumcheckProof<G>,
55 eval_W: G::Scalar,
56 sc_proof_batch: SumcheckProof<G>,
57 evals_batch: Vec<G::Scalar>,
58 eval_arg: EE::EvaluationArgument,
59}
60
61impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G>
62 for RelaxedR1CSSNARK<G, EE>
63{
64 type ProverKey = ProverKey<G, EE>;
65 type VerifierKey = VerifierKey<G, EE>;
66
67 fn setup(
68 ck: &CommitmentKey<G>,
69 S: &R1CSShape<G>,
70 ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> {
71 let (pk_ee, vk_ee) = EE::setup(ck);
72
73 let S = S.pad();
74
75 let vk = {
76 let mut vk = VerifierKey {
77 vk_ee,
78 S: S.clone(),
79 digest: G::Scalar::ZERO,
80 };
81 vk.digest = compute_digest::<G, VerifierKey<G, EE>>(&vk);
82 vk
83 };
84
85 let pk = ProverKey {
86 pk_ee,
87 S,
88 vk_digest: vk.digest,
89 };
90
91 Ok((pk, vk))
92 }
93
94 /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
95 fn prove(
96 ck: &CommitmentKey<G>,
97 pk: &Self::ProverKey,
98 U: &RelaxedR1CSInstance<G>,
99 W: &RelaxedR1CSWitness<G>,
100 ) -> Result<Self, NovaError> {
101 let W = W.pad(&pk.S); // pad the witness
102 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
103
104 // sanity check that R1CSShape has certain size characteristics
105 assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
106 assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
107 assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
108 assert!(pk.S.num_io < pk.S.num_vars);
109
110 // append the digest of vk (which includes R1CS matrices) and the RelaxedR1CSInstance to the transcript
111 transcript.absorb(b"vk", &pk.vk_digest);
112 transcript.absorb(b"U", U);
113
114 // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
115 let mut z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
116
117 let (num_rounds_x, num_rounds_y) = (
118 (pk.S.num_cons as f64).log2() as usize,
119 ((pk.S.num_vars as f64).log2() as usize + 1),
120 );
121
122 // outer sum-check
123 let tau = (0..num_rounds_x)
124 .map(|_i| transcript.squeeze(b"t"))
125 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
126
127 let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals());
128 let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = {
129 let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?;
130 let poly_uCz_E = (0..pk.S.num_cons)
131 .map(|i| U.u * poly_Cz[i] + W.E[i])
132 .collect::<Vec<G::Scalar>>();
133 (
134 MultilinearPolynomial::new(poly_Az),
135 MultilinearPolynomial::new(poly_Bz),
136 MultilinearPolynomial::new(poly_Cz),
137 MultilinearPolynomial::new(poly_uCz_E),
138 )
139 };
140
141 let comb_func_outer =
142 |poly_A_comp: &G::Scalar,
143 poly_B_comp: &G::Scalar,
144 poly_C_comp: &G::Scalar,
145 poly_D_comp: &G::Scalar|
146 -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) };
147 let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term(
148 &G::Scalar::ZERO, // claim is zero
149 num_rounds_x,
150 &mut poly_tau,
151 &mut poly_Az,
152 &mut poly_Bz,
153 &mut poly_uCz_E,
154 comb_func_outer,
155 &mut transcript,
156 )?;
157
158 // claims from the end of sum-check
159 let (claim_Az, claim_Bz): (G::Scalar, G::Scalar) = (claims_outer[1], claims_outer[2]);
160 let claim_Cz = poly_Cz.evaluate(&r_x);
161 let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x);
162 transcript.absorb(
163 b"claims_outer",
164 &[claim_Az, claim_Bz, claim_Cz, eval_E].as_slice(),
165 );
166
167 // inner sum-check
168 let r = transcript.squeeze(b"r")?;
169 let claim_inner_joint = claim_Az + r * claim_Bz + r * r * claim_Cz;
170
171 let poly_ABC = {
172 // compute the initial evaluation table for R(\tau, x)
173 let evals_rx = EqPolynomial::new(r_x.clone()).evals();
174
175 // Bounds "row" variables of (A, B, C) matrices viewed as 2d multilinear polynomials
176 let compute_eval_table_sparse =
177 |S: &R1CSShape<G>, rx: &[G::Scalar]| -> (Vec<G::Scalar>, Vec<G::Scalar>, Vec<G::Scalar>) {
178 assert_eq!(rx.len(), S.num_cons);
179
180 let inner = |M: &Vec<(usize, usize, G::Scalar)>, M_evals: &mut Vec<G::Scalar>| {
181 for (row, col, val) in M {
182 M_evals[*col] += rx[*row] * val;
183 }
184 };
185
186 let (A_evals, (B_evals, C_evals)) = rayon::join(
187 || {
188 let mut A_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
189 inner(&S.A, &mut A_evals);
190 A_evals
191 },
192 || {
193 rayon::join(
194 || {
195 let mut B_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
196 inner(&S.B, &mut B_evals);
197 B_evals
198 },
199 || {
200 let mut C_evals: Vec<G::Scalar> = vec![G::Scalar::ZERO; 2 * S.num_vars];
201 inner(&S.C, &mut C_evals);
202 C_evals
203 },
204 )
205 },
206 );
207
208 (A_evals, B_evals, C_evals)
209 };
210
211 let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&pk.S, &evals_rx);
212
213 assert_eq!(evals_A.len(), evals_B.len());
214 assert_eq!(evals_A.len(), evals_C.len());
215 (0..evals_A.len())
216 .into_par_iter()
217 .map(|i| evals_A[i] + r * evals_B[i] + r * r * evals_C[i])
218 .collect::<Vec<G::Scalar>>()
219 };
220
221 let poly_z = {
222 z.resize(pk.S.num_vars * 2, G::Scalar::ZERO);
223 z
224 };
225
226 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
227 *poly_A_comp * *poly_B_comp
228 };
229 let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad(
230 &claim_inner_joint,
231 num_rounds_y,
232 &mut MultilinearPolynomial::new(poly_ABC),
233 &mut MultilinearPolynomial::new(poly_z),
234 comb_func,
235 &mut transcript,
236 )?;
237
238 // add additional claims about W and E polynomials to the list from CC
239 let mut w_u_vec = Vec::new();
240 let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_y[1..]);
241 w_u_vec.push((
242 PolyEvalWitness { p: W.W.clone() },
243 PolyEvalInstance {
244 c: U.comm_W,
245 x: r_y[1..].to_vec(),
246 e: eval_W,
247 },
248 ));
249
250 w_u_vec.push((
251 PolyEvalWitness { p: W.E },
252 PolyEvalInstance {
253 c: U.comm_E,
254 x: r_x,
255 e: eval_E,
256 },
257 ));
258
259 // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point.
260 // For example, eval_W =? W(r_y[1..]) and eval_E =? E(r_x) into
261 // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz)
262 // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz),
263 // where gamma is a public challenge
264 // Since commitments to W and E are homomorphic, the verifier can compute a commitment
265 // to the batched polynomial.
266 assert!(w_u_vec.len() >= 2);
267
268 let (w_vec, u_vec): (Vec<PolyEvalWitness<G>>, Vec<PolyEvalInstance<G>>) =
269 w_u_vec.into_iter().unzip();
270 let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size
271 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
272
273 // generate a challenge
274 let rho = transcript.squeeze(b"r")?;
275 let num_claims = w_vec_padded.len();
276 let powers_of_rho = powers::<G>(&rho, num_claims);
277 let claim_batch_joint = u_vec_padded
278 .iter()
279 .zip(powers_of_rho.iter())
280 .map(|(u, p)| u.e * p)
281 .sum();
282
283 let mut polys_left: Vec<MultilinearPolynomial<G::Scalar>> = w_vec_padded
284 .iter()
285 .map(|w| MultilinearPolynomial::new(w.p.clone()))
286 .collect();
287 let mut polys_right: Vec<MultilinearPolynomial<G::Scalar>> = u_vec_padded
288 .iter()
289 .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals()))
290 .collect();
291
292 let num_rounds_z = u_vec_padded[0].x.len();
293 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
294 *poly_A_comp * *poly_B_comp
295 };
296 let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch(
297 &claim_batch_joint,
298 num_rounds_z,
299 &mut polys_left,
300 &mut polys_right,
301 &powers_of_rho,
302 comb_func,
303 &mut transcript,
304 )?;
305
306 let (claims_batch_left, _): (Vec<G::Scalar>, Vec<G::Scalar>) = claims_batch;
307
308 transcript.absorb(b"l", &claims_batch_left.as_slice());
309
310 // we now combine evaluation claims at the same point rz into one
311 let gamma = transcript.squeeze(b"g")?;
312 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
313 let comm_joint = u_vec_padded
314 .iter()
315 .zip(powers_of_gamma.iter())
316 .map(|(u, g_i)| u.c * *g_i)
317 .fold(Commitment::<G>::default(), |acc, item| acc + item);
318 let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma);
319 let eval_joint = claims_batch_left
320 .iter()
321 .zip(powers_of_gamma.iter())
322 .map(|(e, g_i)| *e * *g_i)
323 .sum();
324
325 let eval_arg = EE::prove(
326 ck,
327 &pk.pk_ee,
328 &mut transcript,
329 &comm_joint,
330 &poly_joint.p,
331 &r_z,
332 &eval_joint,
333 )?;
334
335 Ok(RelaxedR1CSSNARK {
336 sc_proof_outer,
337 claims_outer: (claim_Az, claim_Bz, claim_Cz),
338 eval_E,
339 sc_proof_inner,
340 eval_W,
341 sc_proof_batch,
342 evals_batch: claims_batch_left,
343 eval_arg,
344 })
345 }
346
347 /// verifies a proof of satisfiability of a RelaxedR1CS instance
348 fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
349 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
350
351 // append the digest of R1CS matrices and the RelaxedR1CSInstance to the transcript
352 transcript.absorb(b"vk", &vk.digest);
353 transcript.absorb(b"U", U);
354
355 let (num_rounds_x, num_rounds_y) = (
356 (vk.S.num_cons as f64).log2() as usize,
357 ((vk.S.num_vars as f64).log2() as usize + 1),
358 );
359
360 // outer sum-check
361 let tau = (0..num_rounds_x)
362 .map(|_i| transcript.squeeze(b"t"))
363 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
364
365 let (claim_outer_final, r_x) =
366 self
367 .sc_proof_outer
368 .verify(G::Scalar::ZERO, num_rounds_x, 3, &mut transcript)?;
369
370 // verify claim_outer_final
371 let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer;
372 let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x);
373 let claim_outer_final_expected =
374 taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E);
375 if claim_outer_final != claim_outer_final_expected {
376 return Err(NovaError::InvalidSumcheckProof);
377 }
378
379 transcript.absorb(
380 b"claims_outer",
381 &[
382 self.claims_outer.0,
383 self.claims_outer.1,
384 self.claims_outer.2,
385 self.eval_E,
386 ]
387 .as_slice(),
388 );
389
390 // inner sum-check
391 let r = transcript.squeeze(b"r")?;
392 let claim_inner_joint =
393 self.claims_outer.0 + r * self.claims_outer.1 + r * r * self.claims_outer.2;
394
395 let (claim_inner_final, r_y) =
396 self
397 .sc_proof_inner
398 .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?;
399
400 // verify claim_inner_final
401 let eval_Z = {
402 let eval_X = {
403 // constant term
404 let mut poly_X = vec![(0, U.u)];
405 //remaining inputs
406 poly_X.extend(
407 (0..U.X.len())
408 .map(|i| (i + 1, U.X[i]))
409 .collect::<Vec<(usize, G::Scalar)>>(),
410 );
411 SparsePolynomial::new((vk.S.num_vars as f64).log2() as usize, poly_X).evaluate(&r_y[1..])
412 };
413 (G::Scalar::ONE - r_y[0]) * self.eval_W + r_y[0] * eval_X
414 };
415
416 // compute evaluations of R1CS matrices
417 let multi_evaluate = |M_vec: &[&[(usize, usize, G::Scalar)]],
418 r_x: &[G::Scalar],
419 r_y: &[G::Scalar]|
420 -> Vec<G::Scalar> {
421 let evaluate_with_table =
422 |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar {
423 (0..M.len())
424 .collect::<Vec<usize>>()
425 .par_iter()
426 .map(|&i| {
427 let (row, col, val) = M[i];
428 T_x[row] * T_y[col] * val
429 })
430 .reduce(|| G::Scalar::ZERO, |acc, x| acc + x)
431 };
432
433 let (T_x, T_y) = rayon::join(
434 || EqPolynomial::new(r_x.to_vec()).evals(),
435 || EqPolynomial::new(r_y.to_vec()).evals(),
436 );
437
438 (0..M_vec.len())
439 .collect::<Vec<usize>>()
440 .par_iter()
441 .map(|&i| evaluate_with_table(M_vec[i], &T_x, &T_y))
442 .collect()
443 };
444
445 let evals = multi_evaluate(&[&vk.S.A, &vk.S.B, &vk.S.C], &r_x, &r_y);
446
447 let claim_inner_final_expected = (evals[0] + r * evals[1] + r * r * evals[2]) * eval_Z;
448 if claim_inner_final != claim_inner_final_expected {
449 return Err(NovaError::InvalidSumcheckProof);
450 }
451
452 // add claims about W and E polynomials
453 let u_vec: Vec<PolyEvalInstance<G>> = vec![
454 PolyEvalInstance {
455 c: U.comm_W,
456 x: r_y[1..].to_vec(),
457 e: self.eval_W,
458 },
459 PolyEvalInstance {
460 c: U.comm_E,
461 x: r_x,
462 e: self.eval_E,
463 },
464 ];
465
466 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
467
468 // generate a challenge
469 let rho = transcript.squeeze(b"r")?;
470 let num_claims = u_vec.len();
471 let powers_of_rho = powers::<G>(&rho, num_claims);
472 let claim_batch_joint = u_vec
473 .iter()
474 .zip(powers_of_rho.iter())
475 .map(|(u, p)| u.e * p)
476 .sum();
477
478 let num_rounds_z = u_vec_padded[0].x.len();
479 let (claim_batch_final, r_z) =
480 self
481 .sc_proof_batch
482 .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?;
483
484 let claim_batch_final_expected = {
485 let poly_rz = EqPolynomial::new(r_z.clone());
486 let evals = u_vec_padded
487 .iter()
488 .map(|u| poly_rz.evaluate(&u.x))
489 .collect::<Vec<G::Scalar>>();
490
491 evals
492 .iter()
493 .zip(self.evals_batch.iter())
494 .zip(powers_of_rho.iter())
495 .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i)
496 .sum()
497 };
498
499 if claim_batch_final != claim_batch_final_expected {
500 return Err(NovaError::InvalidSumcheckProof);
501 }
502
503 transcript.absorb(b"l", &self.evals_batch.as_slice());
504
505 // we now combine evaluation claims at the same point rz into one
506 let gamma = transcript.squeeze(b"g")?;
507 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
508 let comm_joint = u_vec_padded
509 .iter()
510 .zip(powers_of_gamma.iter())
511 .map(|(u, g_i)| u.c * *g_i)
512 .fold(Commitment::<G>::default(), |acc, item| acc + item);
513 let eval_joint = self
514 .evals_batch
515 .iter()
516 .zip(powers_of_gamma.iter())
517 .map(|(e, g_i)| *e * *g_i)
518 .sum();
519
520 // verify
521 EE::verify(
522 &vk.vk_ee,
523 &mut transcript,
524 &comm_joint,
525 &r_z,
526 &eval_joint,
527 &self.eval_arg,
528 )?;
529
530 Ok(())
531 }
532}