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