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 sc_proof_inner: SumcheckProof<G>,
67 eval_E: G::Scalar,
68 eval_W: G::Scalar,
69 eval_arg: EE::EvaluationArgument,
70}
71
72impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G>
73 for RelaxedR1CSSNARK<G, EE>
74{
75 type ProverKey = ProverKey<G, EE>;
76 type VerifierKey = VerifierKey<G, EE>;
77
78 /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
79 fn prove(
80 pk: &Self::ProverKey,
81 U: &RelaxedR1CSInstance<G>,
82 W: &RelaxedR1CSWitness<G>,
83 ) -> Result<Self, NovaError> {
84 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
85
86 // sanity check that R1CSShape has certain size characteristics
87 assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
88 assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
89 assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
90 assert!(pk.S.num_io < pk.S.num_vars);
91
92 // append the R1CSShape and RelaxedR1CSInstance to the transcript
93 pk.S.append_to_transcript(b"S", &mut transcript);
94 U.append_to_transcript(b"U", &mut transcript);
95
96 // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
97 let mut z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
98
99 let (num_rounds_x, num_rounds_y) = (
100 (pk.S.num_cons as f64).log2() as usize,
101 ((pk.S.num_vars as f64).log2() as usize + 1),
102 );
103
104 // outer sum-check
105 let tau = (0..num_rounds_x)
106 .map(|_i| G::Scalar::challenge(b"challenge_tau", &mut transcript))
107 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
108
109 let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals());
110 let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = {
111 let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?;
112 let poly_uCz_E = (0..pk.S.num_cons)
113 .map(|i| U.u * poly_Cz[i] + W.E[i])
114 .collect::<Vec<G::Scalar>>();
115 (
116 MultilinearPolynomial::new(poly_Az),
117 MultilinearPolynomial::new(poly_Bz),
118 MultilinearPolynomial::new(poly_Cz),
119 MultilinearPolynomial::new(poly_uCz_E),
120 )
121 };
122
123 let comb_func_outer =
124 |poly_A_comp: &G::Scalar,
125 poly_B_comp: &G::Scalar,
126 poly_C_comp: &G::Scalar,
127 poly_D_comp: &G::Scalar|
128 -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) };
129 let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term(
130 &G::Scalar::zero(), // claim is zero
131 num_rounds_x,
132 &mut poly_tau,
133 &mut poly_Az,
134 &mut poly_Bz,
135 &mut poly_uCz_E,
136 comb_func_outer,
137 &mut transcript,
138 )?;
139
140 // claims from the end of sum-check
141 let (claim_Az, claim_Bz): (G::Scalar, G::Scalar) = (claims_outer[1], claims_outer[2]);
142 let claim_Cz = poly_Cz.evaluate(&r_x);
143
144 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
145 &claim_Az,
146 b"claim_Az",
147 &mut transcript,
148 );
149 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
150 &claim_Bz,
151 b"claim_Bz",
152 &mut transcript,
153 );
154 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
155 &claim_Cz,
156 b"claim_Cz",
157 &mut transcript,
158 );
159
160 let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x);
161 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
162 &eval_E,
163 b"eval_E",
164 &mut transcript,
165 );
166
167 // inner sum-check
168 let r_A = G::Scalar::challenge(b"challenge_rA", &mut transcript)?;
169 let r_B = G::Scalar::challenge(b"challenge_rB", &mut transcript)?;
170 let r_C = G::Scalar::challenge(b"challenge_rC", &mut transcript)?;
171 let claim_inner_joint = r_A * claim_Az + r_B * claim_Bz + r_C * claim_Cz;
172
173 let poly_ABC = {
174 // compute the initial evaluation table for R(\tau, x)
175 let evals_rx = EqPolynomial::new(r_x.clone()).evals();
176
177 // Bounds "row" variables of (A, B, C) matrices viewed as 2d multilinear polynomials
178 let compute_eval_table_sparse =
179 |S: &R1CSShape<G>, rx: &[G::Scalar]| -> (Vec<G::Scalar>, Vec<G::Scalar>, Vec<G::Scalar>) {
180 assert_eq!(rx.len(), S.num_cons);
181
182 let inner = |M: &Vec<(usize, usize, G::Scalar)>, M_evals: &mut Vec<G::Scalar>| {
183 for (row, col, val) in M {
184 M_evals[*col] += rx[*row] * val;
185 }
186 };
187
188 let (A_evals, (B_evals, C_evals)) = rayon::join(
189 || {
190 let mut A_evals: Vec<G::Scalar> = vec![G::Scalar::zero(); 2 * S.num_vars];
191 inner(&S.A, &mut A_evals);
192 A_evals
193 },
194 || {
195 rayon::join(
196 || {
197 let mut B_evals: Vec<G::Scalar> = vec![G::Scalar::zero(); 2 * S.num_vars];
198 inner(&S.B, &mut B_evals);
199 B_evals
200 },
201 || {
202 let mut C_evals: Vec<G::Scalar> = vec![G::Scalar::zero(); 2 * S.num_vars];
203 inner(&S.C, &mut C_evals);
204 C_evals
205 },
206 )
207 },
208 );
209
210 (A_evals, B_evals, C_evals)
211 };
212
213 let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&pk.S, &evals_rx);
214
215 assert_eq!(evals_A.len(), evals_B.len());
216 assert_eq!(evals_A.len(), evals_C.len());
217 (0..evals_A.len())
218 .into_par_iter()
219 .map(|i| r_A * evals_A[i] + r_B * evals_B[i] + r_C * evals_C[i])
220 .collect::<Vec<G::Scalar>>()
221 };
222
223 let poly_z = {
224 z.resize(pk.S.num_vars * 2, G::Scalar::zero());
225 z
226 };
227
228 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
229 *poly_A_comp * *poly_B_comp
230 };
231 let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad(
232 &claim_inner_joint,
233 num_rounds_y,
234 &mut MultilinearPolynomial::new(poly_ABC),
235 &mut MultilinearPolynomial::new(poly_z),
236 comb_func,
237 &mut transcript,
238 )?;
239
240 let eval_W = MultilinearPolynomial::new(W.W.clone()).evaluate(&r_y[1..]);
241 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
242 &eval_W,
243 b"eval_W",
244 &mut transcript,
245 );
246
247 let eval_arg = EE::prove_batch(
248 &pk.gens,
249 &mut transcript,
250 &[U.comm_E, U.comm_W],
251 &[W.E.clone(), W.W.clone()],
252 &[r_x, r_y[1..].to_vec()],
253 &[eval_E, eval_W],
254 )?;
255
256 Ok(RelaxedR1CSSNARK {
257 sc_proof_outer,
258 claims_outer: (claim_Az, claim_Bz, claim_Cz),
259 sc_proof_inner,
260 eval_W,
261 eval_E,
262 eval_arg,
263 })
264 }
265
266 /// verifies a proof of satisfiability of a RelaxedR1CS instance
267 fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
268 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
269
270 // append the R1CSShape and RelaxedR1CSInstance to the transcript
271 vk.S.append_to_transcript(b"S", &mut transcript);
272 U.append_to_transcript(b"U", &mut transcript);
273
274 let (num_rounds_x, num_rounds_y) = (
275 (vk.S.num_cons as f64).log2() as usize,
276 ((vk.S.num_vars as f64).log2() as usize + 1),
277 );
278
279 // outer sum-check
280 let tau = (0..num_rounds_x)
281 .map(|_i| G::Scalar::challenge(b"challenge_tau", &mut transcript))
282 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
283
284 let (claim_outer_final, r_x) =
285 self
286 .sc_proof_outer
287 .verify(G::Scalar::zero(), num_rounds_x, 3, &mut transcript)?;
288
289 // verify claim_outer_final
290 let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer;
291 let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x);
292 let claim_outer_final_expected =
293 taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E);
294 if claim_outer_final != claim_outer_final_expected {
295 return Err(NovaError::InvalidSumcheckProof);
296 }
297
298 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
299 &self.claims_outer.0,
300 b"claim_Az",
301 &mut transcript,
302 );
303 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
304 &self.claims_outer.1,
305 b"claim_Bz",
306 &mut transcript,
307 );
308 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
309 &self.claims_outer.2,
310 b"claim_Cz",
311 &mut transcript,
312 );
313 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
314 &self.eval_E,
315 b"eval_E",
316 &mut transcript,
317 );
318
319 // inner sum-check
320 let r_A = G::Scalar::challenge(b"challenge_rA", &mut transcript)?;
321 let r_B = G::Scalar::challenge(b"challenge_rB", &mut transcript)?;
322 let r_C = G::Scalar::challenge(b"challenge_rC", &mut transcript)?;
323 let claim_inner_joint =
324 r_A * self.claims_outer.0 + r_B * self.claims_outer.1 + r_C * self.claims_outer.2;
325
326 let (claim_inner_final, r_y) =
327 self
328 .sc_proof_inner
329 .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?;
330
331 // verify claim_inner_final
332 let eval_Z = {
333 let eval_X = {
334 // constant term
335 let mut poly_X = vec![(0, U.u)];
336 //remaining inputs
337 poly_X.extend(
338 (0..U.X.len())
339 .map(|i| (i + 1, U.X[i]))
340 .collect::<Vec<(usize, G::Scalar)>>(),
341 );
342 SparsePolynomial::new((vk.S.num_vars as f64).log2() as usize, poly_X).evaluate(&r_y[1..])
343 };
344 (G::Scalar::one() - r_y[0]) * self.eval_W + r_y[0] * eval_X
345 };
346
347 let evaluate_as_sparse_polynomial = |S: &R1CSShape<G>,
348 r_x: &[G::Scalar],
349 r_y: &[G::Scalar]|
350 -> (G::Scalar, G::Scalar, G::Scalar) {
351 let evaluate_with_table =
352 |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar {
353 (0..M.len())
354 .map(|i| {
355 let (row, col, val) = M[i];
356 T_x[row] * T_y[col] * val
357 })
358 .fold(G::Scalar::zero(), |acc, x| acc + x)
359 };
360
361 let T_x = EqPolynomial::new(r_x.to_vec()).evals();
362 let T_y = EqPolynomial::new(r_y.to_vec()).evals();
363 let eval_A_r = evaluate_with_table(&S.A, &T_x, &T_y);
364 let eval_B_r = evaluate_with_table(&S.B, &T_x, &T_y);
365 let eval_C_r = evaluate_with_table(&S.C, &T_x, &T_y);
366 (eval_A_r, eval_B_r, eval_C_r)
367 };
368
369 let (eval_A_r, eval_B_r, eval_C_r) = evaluate_as_sparse_polynomial(&vk.S, &r_x, &r_y);
370 let claim_inner_final_expected = (r_A * eval_A_r + r_B * eval_B_r + r_C * eval_C_r) * eval_Z;
371 if claim_inner_final != claim_inner_final_expected {
372 return Err(NovaError::InvalidSumcheckProof);
373 }
374
375 // verify eval_W and eval_E
376 <G::Scalar as AppendToTranscriptTrait<G>>::append_to_transcript(
377 &self.eval_W,
378 b"eval_W",
379 &mut transcript,
380 ); //eval_E is already in the transcript
381
382 EE::verify_batch(
383 &vk.gens,
384 &mut transcript,
385 &[U.comm_E, U.comm_W],
386 &[r_x, r_y[1..].to_vec()],
387 &[self.eval_E, self.eval_W],
388 &self.eval_arg,
389 )?;
390
391 Ok(())
392 }
393}