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