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