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