Nova/src/spartan/pp/mod.rs
src/spartan/pp/mod.rsRaw
1//! This module implements RelaxedR1CSSNARK traits using a spark-based approach to prove evaluations of
2//! sparse multilinear polynomials involved in Spartan's sum-check protocol, thereby providing a preprocessing SNARK
3use crate::{
4 bellperson::{
5 r1cs::{NovaShape, NovaWitness},
6 shape_cs::ShapeCS,
7 solver::SatisfyingAssignment,
8 },
9 errors::NovaError,
10 r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
11 spartan::{
12 math::Math,
13 polynomial::{EqPolynomial, MultilinearPolynomial, SparsePolynomial},
14 sumcheck::SumcheckProof,
15 PolyEvalInstance, PolyEvalWitness,
16 },
17 traits::{
18 circuit::StepCircuit, commitment::CommitmentEngineTrait, evaluation::EvaluationEngineTrait,
19 snark::RelaxedR1CSSNARKTrait, Group, TranscriptEngineTrait, TranscriptReprTrait,
20 },
21 Commitment, CommitmentKey,
22};
23use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError};
24use core::{cmp::max, marker::PhantomData};
25use ff::Field;
26use itertools::concat;
27use rayon::prelude::*;
28use serde::{Deserialize, Serialize};
29
30mod product;
31
32use product::{IdentityPolynomial, ProductArgument};
33
34/// A type that holds R1CSShape in a form amenable to memory checking
35#[derive(Clone, Serialize, Deserialize)]
36#[serde(bound = "")]
37pub struct R1CSShapeSparkRepr<G: Group> {
38 N: usize, // size of the vectors
39
40 // dense representation
41 row: Vec<G::Scalar>,
42 col: Vec<G::Scalar>,
43 val_A: Vec<G::Scalar>,
44 val_B: Vec<G::Scalar>,
45 val_C: Vec<G::Scalar>,
46
47 // timestamp polynomials
48 row_read_ts: Vec<G::Scalar>,
49 row_audit_ts: Vec<G::Scalar>,
50 col_read_ts: Vec<G::Scalar>,
51 col_audit_ts: Vec<G::Scalar>,
52}
53
54/// A type that holds a commitment to a sparse polynomial
55#[derive(Clone, Serialize, Deserialize)]
56#[serde(bound = "")]
57pub struct R1CSShapeSparkCommitment<G: Group> {
58 N: usize, // size of each vector
59
60 // commitments to the dense representation
61 comm_row: Commitment<G>,
62 comm_col: Commitment<G>,
63 comm_val_A: Commitment<G>,
64 comm_val_B: Commitment<G>,
65 comm_val_C: Commitment<G>,
66
67 // commitments to the timestamp polynomials
68 comm_row_read_ts: Commitment<G>,
69 comm_row_audit_ts: Commitment<G>,
70 comm_col_read_ts: Commitment<G>,
71 comm_col_audit_ts: Commitment<G>,
72}
73
74impl<G: Group> TranscriptReprTrait<G> for R1CSShapeSparkCommitment<G> {
75 fn to_transcript_bytes(&self) -> Vec<u8> {
76 [
77 self.comm_row,
78 self.comm_col,
79 self.comm_val_A,
80 self.comm_val_B,
81 self.comm_val_C,
82 self.comm_row_read_ts,
83 self.comm_row_audit_ts,
84 self.comm_col_read_ts,
85 self.comm_col_audit_ts,
86 ]
87 .as_slice()
88 .to_transcript_bytes()
89 }
90}
91
92impl<G: Group> R1CSShapeSparkRepr<G> {
93 /// represents R1CSShape in a Spark-friendly format amenable to memory checking
94 pub fn new(S: &R1CSShape<G>) -> R1CSShapeSparkRepr<G> {
95 let N = {
96 let total_nz = S.A.len() + S.B.len() + S.C.len();
97 max(total_nz, max(2 * S.num_vars, S.num_cons)).next_power_of_two()
98 };
99
100 let row = {
101 let mut r = S
102 .A
103 .iter()
104 .chain(S.B.iter())
105 .chain(S.C.iter())
106 .map(|(r, _, _)| *r)
107 .collect::<Vec<usize>>();
108 r.resize(N, 0usize);
109 r
110 };
111
112 let col = {
113 let mut c = S
114 .A
115 .iter()
116 .chain(S.B.iter())
117 .chain(S.C.iter())
118 .map(|(_, c, _)| *c)
119 .collect::<Vec<usize>>();
120 c.resize(N, 0usize);
121 c
122 };
123
124 let val_A = {
125 let mut val = S.A.iter().map(|(_, _, v)| *v).collect::<Vec<G::Scalar>>();
126 val.resize(N, G::Scalar::zero());
127 val
128 };
129
130 let val_B = {
131 // prepend zeros
132 let mut val = vec![G::Scalar::zero(); S.A.len()];
133 val.extend(S.B.iter().map(|(_, _, v)| *v).collect::<Vec<G::Scalar>>());
134 // append zeros
135 val.resize(N, G::Scalar::zero());
136 val
137 };
138
139 let val_C = {
140 // prepend zeros
141 let mut val = vec![G::Scalar::zero(); S.A.len() + S.B.len()];
142 val.extend(S.C.iter().map(|(_, _, v)| *v).collect::<Vec<G::Scalar>>());
143 // append zeros
144 val.resize(N, G::Scalar::zero());
145 val
146 };
147
148 // timestamp calculation routine
149 let timestamp_calc =
150 |num_ops: usize, num_cells: usize, addr_trace: &[usize]| -> (Vec<usize>, Vec<usize>) {
151 let mut read_ts = vec![0usize; num_ops];
152 let mut audit_ts = vec![0usize; num_cells];
153
154 assert!(num_ops >= addr_trace.len());
155 for i in 0..addr_trace.len() {
156 let addr = addr_trace[i];
157 assert!(addr < num_cells);
158 let r_ts = audit_ts[addr];
159 read_ts[i] = r_ts;
160
161 let w_ts = r_ts + 1;
162 audit_ts[addr] = w_ts;
163 }
164 (read_ts, audit_ts)
165 };
166
167 // timestamp polynomials for row
168 let (row_read_ts, row_audit_ts) = timestamp_calc(N, N, &row);
169 let (col_read_ts, col_audit_ts) = timestamp_calc(N, N, &col);
170
171 // a routine to turn a vector of usize into a vector scalars
172 let to_vec_scalar = |v: &[usize]| -> Vec<G::Scalar> {
173 (0..v.len())
174 .map(|i| G::Scalar::from(v[i] as u64))
175 .collect::<Vec<G::Scalar>>()
176 };
177
178 R1CSShapeSparkRepr {
179 N,
180
181 // dense representation
182 row: to_vec_scalar(&row),
183 col: to_vec_scalar(&col),
184 val_A,
185 val_B,
186 val_C,
187
188 // timestamp polynomials
189 row_read_ts: to_vec_scalar(&row_read_ts),
190 row_audit_ts: to_vec_scalar(&row_audit_ts),
191 col_read_ts: to_vec_scalar(&col_read_ts),
192 col_audit_ts: to_vec_scalar(&col_audit_ts),
193 }
194 }
195
196 fn commit(&self, ck: &CommitmentKey<G>) -> R1CSShapeSparkCommitment<G> {
197 let comm_vec: Vec<Commitment<G>> = [
198 &self.row,
199 &self.col,
200 &self.val_A,
201 &self.val_B,
202 &self.val_C,
203 &self.row_read_ts,
204 &self.row_audit_ts,
205 &self.col_read_ts,
206 &self.col_audit_ts,
207 ]
208 .par_iter()
209 .map(|v| G::CE::commit(ck, v))
210 .collect();
211
212 R1CSShapeSparkCommitment {
213 N: self.row.len(),
214 comm_row: comm_vec[0],
215 comm_col: comm_vec[1],
216 comm_val_A: comm_vec[2],
217 comm_val_B: comm_vec[3],
218 comm_val_C: comm_vec[4],
219 comm_row_read_ts: comm_vec[5],
220 comm_row_audit_ts: comm_vec[6],
221 comm_col_read_ts: comm_vec[7],
222 comm_col_audit_ts: comm_vec[8],
223 }
224 }
225
226 /// evaluates the the provided R1CSShape at (r_x, r_y)
227 pub fn multi_evaluate(
228 M_vec: &[&[(usize, usize, G::Scalar)]],
229 r_x: &[G::Scalar],
230 r_y: &[G::Scalar],
231 ) -> Vec<G::Scalar> {
232 let evaluate_with_table =
233 |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar {
234 (0..M.len())
235 .collect::<Vec<usize>>()
236 .par_iter()
237 .map(|&i| {
238 let (row, col, val) = M[i];
239 T_x[row] * T_y[col] * val
240 })
241 .reduce(G::Scalar::zero, |acc, x| acc + x)
242 };
243
244 let (T_x, T_y) = rayon::join(
245 || EqPolynomial::new(r_x.to_vec()).evals(),
246 || EqPolynomial::new(r_y.to_vec()).evals(),
247 );
248
249 (0..M_vec.len())
250 .collect::<Vec<usize>>()
251 .par_iter()
252 .map(|&i| evaluate_with_table(M_vec[i], &T_x, &T_y))
253 .collect()
254 }
255
256 // computes evaluation oracles
257 fn evaluation_oracles(
258 &self,
259 S: &R1CSShape<G>,
260 r_x: &[G::Scalar],
261 z: &[G::Scalar],
262 ) -> (
263 Vec<G::Scalar>,
264 Vec<G::Scalar>,
265 Vec<G::Scalar>,
266 Vec<G::Scalar>,
267 ) {
268 let r_x_padded = {
269 let mut x = vec![G::Scalar::zero(); self.N.log_2() - r_x.len()];
270 x.extend(r_x);
271 x
272 };
273
274 let mem_row = EqPolynomial::new(r_x_padded).evals();
275 let mem_col = {
276 let mut z = z.to_vec();
277 z.resize(self.N, G::Scalar::zero());
278 z
279 };
280
281 let mut E_row = S
282 .A
283 .iter()
284 .chain(S.B.iter())
285 .chain(S.C.iter())
286 .map(|(r, _, _)| mem_row[*r])
287 .collect::<Vec<G::Scalar>>();
288
289 let mut E_col = S
290 .A
291 .iter()
292 .chain(S.B.iter())
293 .chain(S.C.iter())
294 .map(|(_, c, _)| mem_col[*c])
295 .collect::<Vec<G::Scalar>>();
296
297 E_row.resize(self.N, mem_row[0]); // we place mem_row[0] since resized row is appended with 0s
298 E_col.resize(self.N, mem_col[0]);
299
300 (mem_row, mem_col, E_row, E_col)
301 }
302}
303
304/// A type that represents the memory-checking argument
305#[derive(Clone, Serialize, Deserialize)]
306#[serde(bound = "")]
307pub struct MemcheckProof<G: Group> {
308 sc_prod: ProductArgument<G>,
309
310 eval_init_row: G::Scalar,
311 eval_read_row: G::Scalar,
312 eval_write_row: G::Scalar,
313 eval_audit_row: G::Scalar,
314 eval_init_col: G::Scalar,
315 eval_read_col: G::Scalar,
316 eval_write_col: G::Scalar,
317 eval_audit_col: G::Scalar,
318
319 eval_row: G::Scalar,
320 eval_row_read_ts: G::Scalar,
321 eval_E_row: G::Scalar,
322 eval_row_audit_ts: G::Scalar,
323 eval_col: G::Scalar,
324 eval_col_read_ts: G::Scalar,
325 eval_E_col: G::Scalar,
326 eval_col_audit_ts: G::Scalar,
327 eval_z: G::Scalar,
328}
329
330impl<G: Group> MemcheckProof<G> {
331 #[allow(clippy::too_many_arguments)]
332 /// proves a memory-checking relation
333 fn prove(
334 ck: &CommitmentKey<G>,
335 S_repr: &R1CSShapeSparkRepr<G>,
336 S_comm: &R1CSShapeSparkCommitment<G>,
337 mem_row: &[G::Scalar],
338 comm_E_row: &Commitment<G>,
339 E_row: &[G::Scalar],
340 mem_col: &[G::Scalar],
341 comm_E_col: &Commitment<G>,
342 E_col: &[G::Scalar],
343 transcript: &mut G::TE,
344 ) -> Result<
345 (
346 MemcheckProof<G>,
347 Vec<(PolyEvalWitness<G>, PolyEvalInstance<G>)>,
348 G::Scalar,
349 Vec<G::Scalar>,
350 ),
351 NovaError,
352 > {
353 // we now need to prove that E_row and E_col are well-formed
354 // we use memory checking: H(INIT) * H(WS) =? H(RS) * H(FINAL)
355 let gamma_1 = transcript.squeeze(b"g1")?;
356 let gamma_2 = transcript.squeeze(b"g2")?;
357
358 let gamma_1_sqr = gamma_1 * gamma_1;
359 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
360 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
361 };
362
363 let init_row = (0..mem_row.len())
364 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_row[i], &G::Scalar::zero()))
365 .collect::<Vec<G::Scalar>>();
366 let read_row = (0..E_row.len())
367 .map(|i| hash_func(&S_repr.row[i], &E_row[i], &S_repr.row_read_ts[i]))
368 .collect::<Vec<G::Scalar>>();
369 let write_row = (0..E_row.len())
370 .map(|i| {
371 hash_func(
372 &S_repr.row[i],
373 &E_row[i],
374 &(S_repr.row_read_ts[i] + G::Scalar::one()),
375 )
376 })
377 .collect::<Vec<G::Scalar>>();
378 let audit_row = (0..mem_row.len())
379 .map(|i| {
380 hash_func(
381 &G::Scalar::from(i as u64),
382 &mem_row[i],
383 &S_repr.row_audit_ts[i],
384 )
385 })
386 .collect::<Vec<G::Scalar>>();
387
388 let init_col = (0..mem_col.len())
389 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_col[i], &G::Scalar::zero()))
390 .collect::<Vec<G::Scalar>>();
391 let read_col = (0..E_col.len())
392 .map(|i| hash_func(&S_repr.col[i], &E_col[i], &S_repr.col_read_ts[i]))
393 .collect::<Vec<G::Scalar>>();
394 let write_col = (0..E_col.len())
395 .map(|i| {
396 hash_func(
397 &S_repr.col[i],
398 &E_col[i],
399 &(S_repr.col_read_ts[i] + G::Scalar::one()),
400 )
401 })
402 .collect::<Vec<G::Scalar>>();
403 let audit_col = (0..mem_col.len())
404 .map(|i| {
405 hash_func(
406 &G::Scalar::from(i as u64),
407 &mem_col[i],
408 &S_repr.col_audit_ts[i],
409 )
410 })
411 .collect::<Vec<G::Scalar>>();
412
413 let (sc_prod, evals_prod, r_prod, _evals_input_vec, mut w_u_vec) = ProductArgument::prove(
414 ck,
415 &[
416 init_row, read_row, write_row, audit_row, init_col, read_col, write_col, audit_col,
417 ],
418 transcript,
419 )?;
420
421 // row-related and col-related claims of polynomial evaluations to aid the final check of the sum-check
422 let evals = [
423 &S_repr.row,
424 &S_repr.row_read_ts,
425 E_row,
426 &S_repr.row_audit_ts,
427 &S_repr.col,
428 &S_repr.col_read_ts,
429 E_col,
430 &S_repr.col_audit_ts,
431 mem_col,
432 ]
433 .into_par_iter()
434 .map(|p| MultilinearPolynomial::evaluate_with(p, &r_prod))
435 .collect::<Vec<G::Scalar>>();
436
437 let eval_row = evals[0];
438 let eval_row_read_ts = evals[1];
439 let eval_E_row = evals[2];
440 let eval_row_audit_ts = evals[3];
441 let eval_col = evals[4];
442 let eval_col_read_ts = evals[5];
443 let eval_E_col = evals[6];
444 let eval_col_audit_ts = evals[7];
445 let eval_z = evals[8];
446
447 // we can batch all the claims
448 transcript.absorb(
449 b"e",
450 &[
451 eval_row,
452 eval_row_read_ts,
453 eval_E_row,
454 eval_row_audit_ts,
455 eval_col,
456 eval_col_read_ts,
457 eval_E_col,
458 eval_col_audit_ts,
459 ]
460 .as_slice(),
461 );
462 let c = transcript.squeeze(b"c")?;
463 let eval_joint = eval_row
464 + c * eval_row_read_ts
465 + c * c * eval_E_row
466 + c * c * c * eval_row_audit_ts
467 + c * c * c * c * eval_col
468 + c * c * c * c * c * eval_col_read_ts
469 + c * c * c * c * c * c * eval_E_col
470 + c * c * c * c * c * c * c * eval_col_audit_ts;
471 let comm_joint = S_comm.comm_row
472 + S_comm.comm_row_read_ts * c
473 + *comm_E_row * c * c
474 + S_comm.comm_row_audit_ts * c * c * c
475 + S_comm.comm_col * c * c * c * c
476 + S_comm.comm_col_read_ts * c * c * c * c * c
477 + *comm_E_col * c * c * c * c * c * c
478 + S_comm.comm_col_audit_ts * c * c * c * c * c * c * c;
479 let poly_joint = S_repr
480 .row
481 .iter()
482 .zip(S_repr.row_read_ts.iter())
483 .zip(E_row.iter())
484 .zip(S_repr.row_audit_ts.iter())
485 .zip(S_repr.col.iter())
486 .zip(S_repr.col_read_ts.iter())
487 .zip(E_col.iter())
488 .zip(S_repr.col_audit_ts.iter())
489 .map(|(((((((x, y), z), m), n), q), s), t)| {
490 *x + c * y
491 + c * c * z
492 + c * c * c * m
493 + c * c * c * c * n
494 + c * c * c * c * c * q
495 + c * c * c * c * c * c * s
496 + c * c * c * c * c * c * c * t
497 })
498 .collect::<Vec<_>>();
499
500 // add the claim to prove for later
501 w_u_vec.push((
502 PolyEvalWitness { p: poly_joint },
503 PolyEvalInstance {
504 c: comm_joint,
505 x: r_prod.clone(),
506 e: eval_joint,
507 },
508 ));
509
510 let eval_arg = Self {
511 eval_init_row: evals_prod[0],
512 eval_read_row: evals_prod[1],
513 eval_write_row: evals_prod[2],
514 eval_audit_row: evals_prod[3],
515 eval_init_col: evals_prod[4],
516 eval_read_col: evals_prod[5],
517 eval_write_col: evals_prod[6],
518 eval_audit_col: evals_prod[7],
519 sc_prod,
520
521 eval_row,
522 eval_row_read_ts,
523 eval_E_row,
524 eval_row_audit_ts,
525 eval_col,
526 eval_col_read_ts,
527 eval_E_col,
528 eval_col_audit_ts,
529 eval_z,
530 };
531
532 Ok((eval_arg, w_u_vec, eval_z, r_prod))
533 }
534
535 /// verifies a memory-checking relation
536 fn verify(
537 &self,
538 S_comm: &R1CSShapeSparkCommitment<G>,
539 comm_E_row: &Commitment<G>,
540 comm_E_col: &Commitment<G>,
541 r_x: &[G::Scalar],
542 transcript: &mut G::TE,
543 ) -> Result<(Vec<PolyEvalInstance<G>>, G::Scalar, Vec<G::Scalar>), NovaError> {
544 let r_x_padded = {
545 let mut x = vec![G::Scalar::zero(); S_comm.N.log_2() - r_x.len()];
546 x.extend(r_x);
547 x
548 };
549
550 // verify if E_row and E_col are well formed
551 let gamma_1 = transcript.squeeze(b"g1")?;
552 let gamma_2 = transcript.squeeze(b"g2")?;
553
554 // hash function
555 let gamma_1_sqr = gamma_1 * gamma_1;
556 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
557 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
558 };
559
560 // check the required multiset relationship
561 // row
562 if self.eval_init_row * self.eval_write_row != self.eval_read_row * self.eval_audit_row {
563 return Err(NovaError::InvalidMultisetProof);
564 }
565 // col
566 if self.eval_init_col * self.eval_write_col != self.eval_read_col * self.eval_audit_col {
567 return Err(NovaError::InvalidMultisetProof);
568 }
569
570 // verify the product proofs
571 let (claims_final, r_prod, mut u_vec) = self.sc_prod.verify(
572 &[
573 self.eval_init_row,
574 self.eval_read_row,
575 self.eval_write_row,
576 self.eval_audit_row,
577 self.eval_init_col,
578 self.eval_read_col,
579 self.eval_write_col,
580 self.eval_audit_col,
581 ],
582 S_comm.N,
583 transcript,
584 )?;
585
586 // finish the final step of the sum-check
587 let (claim_init_expected_row, claim_audit_expected_row) = {
588 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
589 let val = EqPolynomial::new(r_x_padded.to_vec()).evaluate(&r_prod);
590 (
591 hash_func(&addr, &val, &G::Scalar::zero()),
592 hash_func(&addr, &val, &self.eval_row_audit_ts),
593 )
594 };
595
596 let (claim_read_expected_row, claim_write_expected_row) = {
597 (
598 hash_func(&self.eval_row, &self.eval_E_row, &self.eval_row_read_ts),
599 hash_func(
600 &self.eval_row,
601 &self.eval_E_row,
602 &(self.eval_row_read_ts + G::Scalar::one()),
603 ),
604 )
605 };
606
607 // multiset check for the row
608 if claim_init_expected_row != claims_final[0]
609 || claim_read_expected_row != claims_final[1]
610 || claim_write_expected_row != claims_final[2]
611 || claim_audit_expected_row != claims_final[3]
612 {
613 return Err(NovaError::InvalidSumcheckProof);
614 }
615
616 let (claim_init_expected_col, claim_audit_expected_col) = {
617 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
618 let val = self.eval_z; // this value is later checked against U.comm_W and u.X
619 (
620 hash_func(&addr, &val, &G::Scalar::zero()),
621 hash_func(&addr, &val, &self.eval_col_audit_ts),
622 )
623 };
624
625 let (claim_read_expected_col, claim_write_expected_col) = {
626 (
627 hash_func(&self.eval_col, &self.eval_E_col, &self.eval_col_read_ts),
628 hash_func(
629 &self.eval_col,
630 &self.eval_E_col,
631 &(self.eval_col_read_ts + G::Scalar::one()),
632 ),
633 )
634 };
635
636 // multiset check for the col
637 if claim_init_expected_col != claims_final[4]
638 || claim_read_expected_col != claims_final[5]
639 || claim_write_expected_col != claims_final[6]
640 || claim_audit_expected_col != claims_final[7]
641 {
642 return Err(NovaError::InvalidSumcheckProof);
643 }
644
645 transcript.absorb(
646 b"e",
647 &[
648 self.eval_row,
649 self.eval_row_read_ts,
650 self.eval_E_row,
651 self.eval_row_audit_ts,
652 self.eval_col,
653 self.eval_col_read_ts,
654 self.eval_E_col,
655 self.eval_col_audit_ts,
656 ]
657 .as_slice(),
658 );
659 let c = transcript.squeeze(b"c")?;
660 let eval_joint = self.eval_row
661 + c * self.eval_row_read_ts
662 + c * c * self.eval_E_row
663 + c * c * c * self.eval_row_audit_ts
664 + c * c * c * c * self.eval_col
665 + c * c * c * c * c * self.eval_col_read_ts
666 + c * c * c * c * c * c * self.eval_E_col
667 + c * c * c * c * c * c * c * self.eval_col_audit_ts;
668 let comm_joint = S_comm.comm_row
669 + S_comm.comm_row_read_ts * c
670 + *comm_E_row * c * c
671 + S_comm.comm_row_audit_ts * c * c * c
672 + S_comm.comm_col * c * c * c * c
673 + S_comm.comm_col_read_ts * c * c * c * c * c
674 + *comm_E_col * c * c * c * c * c * c
675 + S_comm.comm_col_audit_ts * c * c * c * c * c * c * c;
676
677 u_vec.push(PolyEvalInstance {
678 c: comm_joint,
679 x: r_prod.clone(),
680 e: eval_joint,
681 });
682
683 Ok((u_vec, self.eval_z, r_prod))
684 }
685}
686
687/// A type that represents the prover's key
688#[derive(Clone, Serialize, Deserialize)]
689#[serde(bound = "")]
690pub struct ProverKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
691 pk_ee: EE::ProverKey,
692 S: R1CSShape<G>,
693 S_repr: R1CSShapeSparkRepr<G>,
694 S_comm: R1CSShapeSparkCommitment<G>,
695}
696
697/// A type that represents the verifier's key
698#[derive(Clone, Serialize, Deserialize)]
699#[serde(bound = "")]
700pub struct VerifierKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
701 num_cons: usize,
702 num_vars: usize,
703 vk_ee: EE::VerifierKey,
704 S_comm: R1CSShapeSparkCommitment<G>,
705}
706
707/// A succinct proof of knowledge of a witness to a relaxed R1CS instance
708/// The proof is produced using Spartan's combination of the sum-check and
709/// the commitment to a vector viewed as a polynomial commitment
710#[derive(Clone, Serialize, Deserialize)]
711#[serde(bound = "")]
712pub struct RelaxedR1CSSNARK<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
713 // outer sum-check
714 sc_proof_outer: SumcheckProof<G>,
715
716 // claims from the end of the outer sum-check
717 eval_Az: G::Scalar,
718 eval_Bz: G::Scalar,
719 eval_Cz: G::Scalar,
720 eval_E: G::Scalar,
721
722 // commitment to oracles for the inner sum-check
723 comm_E_row: Commitment<G>,
724 comm_E_col: Commitment<G>,
725
726 // inner sum-check
727 sc_proof_inner: SumcheckProof<G>,
728
729 // claims from the end of inner sum-check
730 eval_E_row: G::Scalar,
731 eval_E_col: G::Scalar,
732 eval_val_A: G::Scalar,
733 eval_val_B: G::Scalar,
734 eval_val_C: G::Scalar,
735
736 // memory-checking proof
737 mc_proof: MemcheckProof<G>,
738
739 // claim about W evaluation
740 eval_W: G::Scalar,
741
742 // batch openings of all multilinear polynomials
743 sc_proof_batch: SumcheckProof<G>,
744 evals_batch: Vec<G::Scalar>,
745 eval_arg: EE::EvaluationArgument,
746}
747
748impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G>
749 for RelaxedR1CSSNARK<G, EE>
750{
751 type ProverKey = ProverKey<G, EE>;
752 type VerifierKey = VerifierKey<G, EE>;
753
754 fn setup(
755 ck: &CommitmentKey<G>,
756 S: &R1CSShape<G>,
757 ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> {
758 let (pk_ee, vk_ee) = EE::setup(ck);
759
760 // pad the R1CS matrices
761 let S = S.pad();
762
763 let S_repr = R1CSShapeSparkRepr::new(&S);
764 let S_comm = S_repr.commit(ck);
765
766 let vk = VerifierKey {
767 num_cons: S.num_cons,
768 num_vars: S.num_vars,
769 S_comm: S_comm.clone(),
770 vk_ee,
771 };
772
773 let pk = ProverKey {
774 pk_ee,
775 S,
776 S_repr,
777 S_comm,
778 };
779
780 Ok((pk, vk))
781 }
782
783 /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
784 fn prove(
785 ck: &CommitmentKey<G>,
786 pk: &Self::ProverKey,
787 U: &RelaxedR1CSInstance<G>,
788 W: &RelaxedR1CSWitness<G>,
789 ) -> Result<Self, NovaError> {
790 let W = W.pad(&pk.S); // pad the witness
791 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
792
793 // a list of polynomial evaluation claims that will be batched
794 let mut w_u_vec = Vec::new();
795
796 // sanity check that R1CSShape has certain size characteristics
797 assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
798 assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
799 assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
800 assert!(pk.S.num_io < pk.S.num_vars);
801
802 // append the commitment to R1CS matrices and the RelaxedR1CSInstance to the transcript
803 transcript.absorb(b"C", &pk.S_comm);
804 transcript.absorb(b"U", U);
805
806 // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
807 let z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
808
809 let (num_rounds_x, _num_rounds_y) = (
810 (pk.S.num_cons as f64).log2() as usize,
811 ((pk.S.num_vars as f64).log2() as usize + 1),
812 );
813
814 // outer sum-check
815 let tau = (0..num_rounds_x)
816 .map(|_i| transcript.squeeze(b"t"))
817 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
818
819 let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals());
820 let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = {
821 let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?;
822 let poly_uCz_E = (0..pk.S.num_cons)
823 .map(|i| U.u * poly_Cz[i] + W.E[i])
824 .collect::<Vec<G::Scalar>>();
825 (
826 MultilinearPolynomial::new(poly_Az),
827 MultilinearPolynomial::new(poly_Bz),
828 MultilinearPolynomial::new(poly_Cz),
829 MultilinearPolynomial::new(poly_uCz_E),
830 )
831 };
832
833 let comb_func_outer =
834 |poly_A_comp: &G::Scalar,
835 poly_B_comp: &G::Scalar,
836 poly_C_comp: &G::Scalar,
837 poly_D_comp: &G::Scalar|
838 -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) };
839 let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term(
840 &G::Scalar::zero(), // claim is zero
841 num_rounds_x,
842 &mut poly_tau,
843 &mut poly_Az,
844 &mut poly_Bz,
845 &mut poly_uCz_E,
846 comb_func_outer,
847 &mut transcript,
848 )?;
849
850 // claims from the end of sum-check
851 let (eval_Az, eval_Bz): (G::Scalar, G::Scalar) = (claims_outer[1], claims_outer[2]);
852 let eval_Cz = poly_Cz.evaluate(&r_x);
853 let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x);
854 transcript.absorb(b"o", &[eval_Az, eval_Bz, eval_Cz, eval_E].as_slice());
855
856 // add claim about eval_E to be proven
857 w_u_vec.push((
858 PolyEvalWitness { p: W.E.clone() },
859 PolyEvalInstance {
860 c: U.comm_E,
861 x: r_x.clone(),
862 e: eval_E,
863 },
864 ));
865
866 // send oracles to aid the inner sum-check
867 // E_row(i) = eq(r_x, row(i)) for all i
868 // E_col(i) = z(col(i)) for all i
869 let (mem_row, z, E_row, E_col) = pk.S_repr.evaluation_oracles(&pk.S, &r_x, &z);
870 let (comm_E_row, comm_E_col) =
871 rayon::join(|| G::CE::commit(ck, &E_row), || G::CE::commit(ck, &E_col));
872
873 // add E_row and E_col to transcript
874 transcript.absorb(b"e", &vec![comm_E_row, comm_E_col].as_slice());
875
876 let r = transcript.squeeze(b"r")?;
877 let val = pk
878 .S_repr
879 .val_A
880 .iter()
881 .zip(pk.S_repr.val_B.iter())
882 .zip(pk.S_repr.val_C.iter())
883 .map(|((a, b), c)| *a + r * *b + r * r * *c)
884 .collect::<Vec<G::Scalar>>();
885
886 // inner sum-check
887 let claim_inner_joint = eval_Az + r * eval_Bz + r * r * eval_Cz;
888 let num_rounds_y = pk.S_repr.N.log_2();
889 let comb_func = |poly_A_comp: &G::Scalar,
890 poly_B_comp: &G::Scalar,
891 poly_C_comp: &G::Scalar|
892 -> G::Scalar { *poly_A_comp * *poly_B_comp * *poly_C_comp };
893
894 debug_assert_eq!(
895 E_row
896 .iter()
897 .zip(val.iter())
898 .zip(E_col.iter())
899 .map(|((a, b), c)| *a * *b * *c)
900 .fold(G::Scalar::zero(), |acc, item| acc + item),
901 claim_inner_joint
902 );
903
904 let (sc_proof_inner, r_y, claims_inner) = SumcheckProof::prove_cubic(
905 &claim_inner_joint,
906 num_rounds_y,
907 &mut MultilinearPolynomial::new(E_row.clone()),
908 &mut MultilinearPolynomial::new(E_col.clone()),
909 &mut MultilinearPolynomial::new(val),
910 comb_func,
911 &mut transcript,
912 )?;
913
914 let eval_E_row = claims_inner[0];
915 let eval_E_col = claims_inner[1];
916 let eval_val_A = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_A, &r_y);
917 let eval_val_B = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_B, &r_y);
918 let eval_val_C = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_C, &r_y);
919
920 // since all the five polynomials are opened at r_y,
921 // we can combine them into a single polynomial opened at r_y
922 transcript.absorb(
923 b"e",
924 &[eval_E_row, eval_E_col, eval_val_A, eval_val_B, eval_val_C].as_slice(),
925 );
926 let c = transcript.squeeze(b"c")?;
927 let eval_sc_inner = eval_E_row
928 + c * eval_E_col
929 + c * c * eval_val_A
930 + c * c * c * eval_val_B
931 + c * c * c * c * eval_val_C;
932 let comm_sc_inner = comm_E_row
933 + comm_E_col * c
934 + pk.S_comm.comm_val_A * c * c
935 + pk.S_comm.comm_val_B * c * c * c
936 + pk.S_comm.comm_val_C * c * c * c * c;
937 let poly_sc_inner = E_row
938 .iter()
939 .zip(E_col.iter())
940 .zip(pk.S_repr.val_A.iter())
941 .zip(pk.S_repr.val_B.iter())
942 .zip(pk.S_repr.val_C.iter())
943 .map(|((((x, y), z), m), n)| *x + c * y + c * c * z + c * c * c * m + c * c * c * c * n)
944 .collect::<Vec<_>>();
945
946 w_u_vec.push((
947 PolyEvalWitness { p: poly_sc_inner },
948 PolyEvalInstance {
949 c: comm_sc_inner,
950 x: r_y,
951 e: eval_sc_inner,
952 },
953 ));
954
955 // we need to prove that E_row and E_col are well-formed
956 let (mc_proof, w_u_vec_mem, _eval_z, r_prod) = MemcheckProof::prove(
957 ck,
958 &pk.S_repr,
959 &pk.S_comm,
960 &mem_row,
961 &comm_E_row,
962 &E_row,
963 &z,
964 &comm_E_col,
965 &E_col,
966 &mut transcript,
967 )?;
968
969 // add claims from memory-checking
970 w_u_vec.extend(w_u_vec_mem);
971
972 // we need to prove that eval_z = z(r_prod) = (1-r_prod[0]) * W.w(r_prod[1..]) + r_prod[0] * U.x(r_prod[1..]).
973 // r_prod was padded, so we now remove the padding
974 let r_prod_unpad = {
975 let l = pk.S_repr.N.log_2() - (2 * pk.S.num_vars).log_2();
976 r_prod[l..].to_vec()
977 };
978
979 let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_prod_unpad[1..]);
980 w_u_vec.push((
981 PolyEvalWitness { p: W.W },
982 PolyEvalInstance {
983 c: U.comm_W,
984 x: r_prod_unpad[1..].to_vec(),
985 e: eval_W,
986 },
987 ));
988
989 // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point.
990 // For example, eval_W =? W(r_y[1..]) and eval_W =? E(r_x) into
991 // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz)
992 // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz),
993 // where gamma is a public challenge
994 // Since commitments to W and E are homomorphic, the verifier can compute a commitment
995 // to the batched polynomial.
996 assert!(w_u_vec.len() >= 2);
997
998 let (w_vec, u_vec): (Vec<PolyEvalWitness<G>>, Vec<PolyEvalInstance<G>>) =
999 w_u_vec.into_iter().unzip();
1000 let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size
1001 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1002
1003 let powers = |s: &G::Scalar, n: usize| -> Vec<G::Scalar> {
1004 assert!(n >= 1);
1005 let mut powers = Vec::new();
1006 powers.push(G::Scalar::one());
1007 for i in 1..n {
1008 powers.push(powers[i - 1] * s);
1009 }
1010 powers
1011 };
1012
1013 // generate a challenge
1014 let rho = transcript.squeeze(b"r")?;
1015 let num_claims = w_vec_padded.len();
1016 let powers_of_rho = powers(&rho, num_claims);
1017 let claim_batch_joint = u_vec_padded
1018 .iter()
1019 .zip(powers_of_rho.iter())
1020 .map(|(u, p)| u.e * p)
1021 .fold(G::Scalar::zero(), |acc, item| acc + item);
1022
1023 let mut polys_left: Vec<MultilinearPolynomial<G::Scalar>> = w_vec_padded
1024 .iter()
1025 .map(|w| MultilinearPolynomial::new(w.p.clone()))
1026 .collect();
1027 let mut polys_right: Vec<MultilinearPolynomial<G::Scalar>> = u_vec_padded
1028 .iter()
1029 .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals()))
1030 .collect();
1031
1032 let num_rounds_z = u_vec_padded[0].x.len();
1033 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
1034 *poly_A_comp * *poly_B_comp
1035 };
1036 let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch(
1037 &claim_batch_joint,
1038 num_rounds_z,
1039 &mut polys_left,
1040 &mut polys_right,
1041 &powers_of_rho,
1042 comb_func,
1043 &mut transcript,
1044 )?;
1045
1046 let (claims_batch_left, _): (Vec<G::Scalar>, Vec<G::Scalar>) = claims_batch;
1047
1048 transcript.absorb(b"l", &claims_batch_left.as_slice());
1049
1050 // we now combine evaluation claims at the same point rz into one
1051 let gamma = transcript.squeeze(b"g")?;
1052 let powers_of_gamma: Vec<G::Scalar> = powers(&gamma, num_claims);
1053 let comm_joint = u_vec_padded
1054 .iter()
1055 .zip(powers_of_gamma.iter())
1056 .map(|(u, g_i)| u.c * *g_i)
1057 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1058 let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma);
1059 let eval_joint = claims_batch_left
1060 .iter()
1061 .zip(powers_of_gamma.iter())
1062 .map(|(e, g_i)| *e * *g_i)
1063 .fold(G::Scalar::zero(), |acc, item| acc + item);
1064
1065 let eval_arg = EE::prove(
1066 ck,
1067 &pk.pk_ee,
1068 &mut transcript,
1069 &comm_joint,
1070 &poly_joint.p,
1071 &r_z,
1072 &eval_joint,
1073 )?;
1074
1075 Ok(RelaxedR1CSSNARK {
1076 sc_proof_outer,
1077 eval_Az,
1078 eval_Bz,
1079 eval_Cz,
1080 eval_E,
1081 comm_E_row,
1082 comm_E_col,
1083 sc_proof_inner,
1084 eval_E_row,
1085 eval_val_A,
1086 eval_val_B,
1087 eval_val_C,
1088 eval_E_col,
1089
1090 mc_proof,
1091
1092 eval_W,
1093
1094 sc_proof_batch,
1095 evals_batch: claims_batch_left,
1096 eval_arg,
1097 })
1098 }
1099
1100 /// verifies a proof of satisfiability of a RelaxedR1CS instance
1101 fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
1102 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
1103 let mut u_vec: Vec<PolyEvalInstance<G>> = Vec::new();
1104
1105 // append the commitment to R1CS matrices and the RelaxedR1CSInstance to the transcript
1106 transcript.absorb(b"C", &vk.S_comm);
1107 transcript.absorb(b"U", U);
1108
1109 let num_rounds_x = (vk.num_cons as f64).log2() as usize;
1110
1111 // outer sum-check
1112 let tau = (0..num_rounds_x)
1113 .map(|_i| transcript.squeeze(b"t"))
1114 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1115
1116 let (claim_outer_final, r_x) =
1117 self
1118 .sc_proof_outer
1119 .verify(G::Scalar::zero(), num_rounds_x, 3, &mut transcript)?;
1120
1121 // verify claim_outer_final
1122 let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x);
1123 let claim_outer_final_expected =
1124 taus_bound_rx * (self.eval_Az * self.eval_Bz - U.u * self.eval_Cz - self.eval_E);
1125 if claim_outer_final != claim_outer_final_expected {
1126 return Err(NovaError::InvalidSumcheckProof);
1127 }
1128
1129 // absorb the claim about eval_E to be checked later
1130 u_vec.push(PolyEvalInstance {
1131 c: U.comm_E,
1132 x: r_x.clone(),
1133 e: self.eval_E,
1134 });
1135
1136 transcript.absorb(
1137 b"o",
1138 &[self.eval_Az, self.eval_Bz, self.eval_Cz, self.eval_E].as_slice(),
1139 );
1140
1141 // add claimed oracles
1142 transcript.absorb(b"e", &vec![self.comm_E_row, self.comm_E_col].as_slice());
1143
1144 // inner sum-check
1145 let r = transcript.squeeze(b"r")?;
1146 let claim_inner_joint = self.eval_Az + r * self.eval_Bz + r * r * self.eval_Cz;
1147 let num_rounds_y = vk.S_comm.N.log_2();
1148
1149 let (claim_inner_final, r_y) =
1150 self
1151 .sc_proof_inner
1152 .verify(claim_inner_joint, num_rounds_y, 3, &mut transcript)?;
1153
1154 // verify claim_inner_final
1155 let claim_inner_final_expected = self.eval_E_row
1156 * self.eval_E_col
1157 * (self.eval_val_A + r * self.eval_val_B + r * r * self.eval_val_C);
1158 if claim_inner_final != claim_inner_final_expected {
1159 return Err(NovaError::InvalidSumcheckProof);
1160 }
1161
1162 // add claims about five polynomials used at the end of the inner sum-check
1163 // since they are all evaluated at r_y, we can batch them into one
1164 transcript.absorb(
1165 b"e",
1166 &[
1167 self.eval_E_row,
1168 self.eval_E_col,
1169 self.eval_val_A,
1170 self.eval_val_B,
1171 self.eval_val_C,
1172 ]
1173 .as_slice(),
1174 );
1175 let c = transcript.squeeze(b"c")?;
1176 let eval_sc_inner = self.eval_E_row
1177 + c * self.eval_E_col
1178 + c * c * self.eval_val_A
1179 + c * c * c * self.eval_val_B
1180 + c * c * c * c * self.eval_val_C;
1181 let comm_sc_inner = self.comm_E_row
1182 + self.comm_E_col * c
1183 + vk.S_comm.comm_val_A * c * c
1184 + vk.S_comm.comm_val_B * c * c * c
1185 + vk.S_comm.comm_val_C * c * c * c * c;
1186
1187 u_vec.push(PolyEvalInstance {
1188 c: comm_sc_inner,
1189 x: r_y,
1190 e: eval_sc_inner,
1191 });
1192
1193 let (u_vec_mem, eval_Z, r_prod) = self.mc_proof.verify(
1194 &vk.S_comm,
1195 &self.comm_E_row,
1196 &self.comm_E_col,
1197 &r_x,
1198 &mut transcript,
1199 )?;
1200
1201 u_vec.extend(u_vec_mem);
1202
1203 // we verify that eval_z = z(r_prod) = (1-r_prod[0]) * W.w(r_prod[1..]) + r_prod[0] * U.x(r_prod[1..]).
1204 let (eval_Z_expected, r_prod_unpad) = {
1205 // r_prod was padded, so we now remove the padding
1206 let (factor, r_prod_unpad) = {
1207 let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2();
1208
1209 let mut factor = G::Scalar::one();
1210 for r_p in r_prod.iter().take(l) {
1211 factor *= G::Scalar::one() - r_p
1212 }
1213
1214 (factor, r_prod[l..].to_vec())
1215 };
1216
1217 let eval_X = {
1218 // constant term
1219 let mut poly_X = vec![(0, U.u)];
1220 //remaining inputs
1221 poly_X.extend(
1222 (0..U.X.len())
1223 .map(|i| (i + 1, U.X[i]))
1224 .collect::<Vec<(usize, G::Scalar)>>(),
1225 );
1226 SparsePolynomial::new((vk.num_vars as f64).log2() as usize, poly_X)
1227 .evaluate(&r_prod_unpad[1..])
1228 };
1229 let eval_Z =
1230 factor * ((G::Scalar::one() - r_prod_unpad[0]) * self.eval_W + r_prod_unpad[0] * eval_X);
1231
1232 (eval_Z, r_prod_unpad)
1233 };
1234
1235 if eval_Z != eval_Z_expected {
1236 return Err(NovaError::IncorrectWitness);
1237 }
1238
1239 u_vec.push(PolyEvalInstance {
1240 c: U.comm_W,
1241 x: r_prod_unpad[1..].to_vec(),
1242 e: self.eval_W,
1243 });
1244
1245 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1246
1247 let powers = |s: &G::Scalar, n: usize| -> Vec<G::Scalar> {
1248 assert!(n >= 1);
1249 let mut powers = Vec::new();
1250 powers.push(G::Scalar::one());
1251 for i in 1..n {
1252 powers.push(powers[i - 1] * s);
1253 }
1254 powers
1255 };
1256
1257 // generate a challenge
1258 let rho = transcript.squeeze(b"r")?;
1259 let num_claims = u_vec.len();
1260 let powers_of_rho = powers(&rho, num_claims);
1261 let claim_batch_joint = u_vec
1262 .iter()
1263 .zip(powers_of_rho.iter())
1264 .map(|(u, p)| u.e * p)
1265 .fold(G::Scalar::zero(), |acc, item| acc + item);
1266
1267 let num_rounds_z = u_vec_padded[0].x.len();
1268 let (claim_batch_final, r_z) =
1269 self
1270 .sc_proof_batch
1271 .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?;
1272
1273 let claim_batch_final_expected = {
1274 let poly_rz = EqPolynomial::new(r_z.clone());
1275 let evals = u_vec_padded
1276 .iter()
1277 .map(|u| poly_rz.evaluate(&u.x))
1278 .collect::<Vec<G::Scalar>>();
1279
1280 evals
1281 .iter()
1282 .zip(self.evals_batch.iter())
1283 .zip(powers_of_rho.iter())
1284 .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i)
1285 .fold(G::Scalar::zero(), |acc, item| acc + item)
1286 };
1287
1288 if claim_batch_final != claim_batch_final_expected {
1289 return Err(NovaError::InvalidSumcheckProof);
1290 }
1291
1292 transcript.absorb(b"l", &self.evals_batch.as_slice());
1293
1294 // we now combine evaluation claims at the same point rz into one
1295 let gamma = transcript.squeeze(b"g")?;
1296 let powers_of_gamma: Vec<G::Scalar> = powers(&gamma, num_claims);
1297 let comm_joint = u_vec_padded
1298 .iter()
1299 .zip(powers_of_gamma.iter())
1300 .map(|(u, g_i)| u.c * *g_i)
1301 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1302 let eval_joint = self
1303 .evals_batch
1304 .iter()
1305 .zip(powers_of_gamma.iter())
1306 .map(|(e, g_i)| *e * *g_i)
1307 .fold(G::Scalar::zero(), |acc, item| acc + item);
1308
1309 // verify
1310 EE::verify(
1311 &vk.vk_ee,
1312 &mut transcript,
1313 &comm_joint,
1314 &r_z,
1315 &eval_joint,
1316 &self.eval_arg,
1317 )?;
1318
1319 Ok(())
1320 }
1321}
1322
1323// provides direct interfaces to call the SNARK implemented in this module
1324struct SpartanCircuit<G: Group, SC: StepCircuit<G::Scalar>> {
1325 z_i: Option<Vec<G::Scalar>>, // inputs to the circuit
1326 sc: SC, // step circuit to be executed
1327}
1328
1329impl<G: Group, SC: StepCircuit<G::Scalar>> Circuit<G::Scalar> for SpartanCircuit<G, SC> {
1330 fn synthesize<CS: ConstraintSystem<G::Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
1331 // obtain the arity information
1332 let arity = self.sc.arity();
1333
1334 // Allocate zi. If inputs.zi is not provided, allocate default value 0
1335 let zero = vec![G::Scalar::zero(); arity];
1336 let z_i = (0..arity)
1337 .map(|i| {
1338 AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || {
1339 Ok(self.z_i.as_ref().unwrap_or(&zero)[i])
1340 })
1341 })
1342 .collect::<Result<Vec<AllocatedNum<G::Scalar>>, _>>()?;
1343
1344 let z_i_plus_one = self.sc.synthesize(&mut cs.namespace(|| "F"), &z_i)?;
1345
1346 // inputize both z_i and z_i_plus_one
1347 for (j, input) in z_i.iter().enumerate().take(arity) {
1348 let _ = input.inputize(cs.namespace(|| format!("input {j}")));
1349 }
1350 for (j, output) in z_i_plus_one.iter().enumerate().take(arity) {
1351 let _ = output.inputize(cs.namespace(|| format!("output {j}")));
1352 }
1353
1354 Ok(())
1355 }
1356}
1357
1358/// A type that holds Spartan's prover key
1359#[derive(Clone, Serialize, Deserialize)]
1360#[serde(bound = "")]
1361pub struct SpartanProverKey<G, EE>
1362where
1363 G: Group,
1364 EE: EvaluationEngineTrait<G, CE = G::CE>,
1365{
1366 F_arity: usize,
1367 S: R1CSShape<G>,
1368 ck: CommitmentKey<G>,
1369 pk: ProverKey<G, EE>,
1370}
1371
1372/// A type that holds Spartan's verifier key
1373#[derive(Clone, Serialize, Deserialize)]
1374#[serde(bound = "")]
1375pub struct SpartanVerifierKey<G, EE>
1376where
1377 G: Group,
1378 EE: EvaluationEngineTrait<G, CE = G::CE>,
1379{
1380 F_arity: usize,
1381 vk: VerifierKey<G, EE>,
1382}
1383
1384/// A direct SNARK proving a step circuit
1385#[derive(Clone, Serialize, Deserialize)]
1386#[serde(bound = "")]
1387pub struct SpartanSNARK<G, EE, C>
1388where
1389 G: Group,
1390 EE: EvaluationEngineTrait<G, CE = G::CE>,
1391 C: StepCircuit<G::Scalar>,
1392{
1393 comm_W: Commitment<G>, // commitment to the witness
1394 snark: RelaxedR1CSSNARK<G, EE>, // snark proving the witness is satisfying
1395 _p: PhantomData<C>,
1396}
1397
1398impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>, C: StepCircuit<G::Scalar>>
1399 SpartanSNARK<G, EE, C>
1400{
1401 /// Produces prover and verifier keys for Spartan
1402 pub fn setup(sc: C) -> Result<(SpartanProverKey<G, EE>, SpartanVerifierKey<G, EE>), NovaError> {
1403 let F_arity = sc.arity();
1404
1405 // construct a circuit that can be synthesized
1406 let circuit: SpartanCircuit<G, C> = SpartanCircuit { z_i: None, sc };
1407
1408 let mut cs: ShapeCS<G> = ShapeCS::new();
1409 let _ = circuit.synthesize(&mut cs);
1410 let (S, ck) = cs.r1cs_shape();
1411
1412 let (pk, vk) = RelaxedR1CSSNARK::setup(&ck, &S)?;
1413
1414 let pk = SpartanProverKey { F_arity, S, ck, pk };
1415
1416 let vk = SpartanVerifierKey { F_arity, vk };
1417
1418 Ok((pk, vk))
1419 }
1420
1421 /// Produces a proof of satisfiability of the provided circuit
1422 pub fn prove(
1423 pk: &SpartanProverKey<G, EE>,
1424 sc: C,
1425 z_i: Vec<G::Scalar>,
1426 ) -> Result<Self, NovaError> {
1427 if z_i.len() != pk.F_arity || sc.output(&z_i).len() != pk.F_arity {
1428 return Err(NovaError::InvalidInitialInputLength);
1429 }
1430
1431 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
1432
1433 let circuit: SpartanCircuit<G, C> = SpartanCircuit { z_i: Some(z_i), sc };
1434
1435 let _ = circuit.synthesize(&mut cs);
1436 let (u, w) = cs
1437 .r1cs_instance_and_witness(&pk.S, &pk.ck)
1438 .map_err(|_e| NovaError::UnSat)?;
1439
1440 // convert the instance and witness to relaxed form
1441 let (u_relaxed, w_relaxed) = (
1442 RelaxedR1CSInstance::from_r1cs_instance_unchecked(&u.comm_W, &u.X),
1443 RelaxedR1CSWitness::from_r1cs_witness(&pk.S, &w),
1444 );
1445
1446 // prove the instance using Spartan
1447 let snark = RelaxedR1CSSNARK::prove(&pk.ck, &pk.pk, &u_relaxed, &w_relaxed)?;
1448
1449 Ok(SpartanSNARK {
1450 comm_W: u.comm_W,
1451 snark,
1452 _p: Default::default(),
1453 })
1454 }
1455
1456 /// Verifies a proof of satisfiability
1457 pub fn verify(
1458 &self,
1459 vk: &SpartanVerifierKey<G, EE>,
1460 z_i: Vec<G::Scalar>,
1461 z_i_plus_one: Vec<G::Scalar>,
1462 ) -> Result<(), NovaError> {
1463 // check if z_i and z_i_plus_one have lengths according to the provided arity
1464 if z_i.len() != vk.F_arity || z_i_plus_one.len() != vk.F_arity {
1465 return Err(NovaError::InvalidInitialInputLength);
1466 }
1467
1468 // construct an instance using the provided commitment to the witness and z_i and z_{i+1}
1469 let u_relaxed = RelaxedR1CSInstance::from_r1cs_instance_unchecked(
1470 &self.comm_W,
1471 &z_i
1472 .into_iter()
1473 .chain(z_i_plus_one.into_iter())
1474 .collect::<Vec<G::Scalar>>(),
1475 );
1476
1477 // verify the snark using the constructed instance
1478 self.snark.verify(&vk.vk, &u_relaxed)?;
1479
1480 Ok(())
1481 }
1482}
1483
1484#[cfg(test)]
1485mod tests {
1486 use super::*;
1487 type G = pasta_curves::pallas::Point;
1488 type EE = crate::provider::ipa_pc::EvaluationEngine<G>;
1489 use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
1490 use core::marker::PhantomData;
1491 use ff::PrimeField;
1492
1493 #[derive(Clone, Debug, Default)]
1494 struct CubicCircuit<F: PrimeField> {
1495 _p: PhantomData<F>,
1496 }
1497
1498 impl<F> StepCircuit<F> for CubicCircuit<F>
1499 where
1500 F: PrimeField,
1501 {
1502 fn arity(&self) -> usize {
1503 1
1504 }
1505
1506 fn synthesize<CS: ConstraintSystem<F>>(
1507 &self,
1508 cs: &mut CS,
1509 z: &[AllocatedNum<F>],
1510 ) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
1511 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
1512 let x = &z[0];
1513 let x_sq = x.square(cs.namespace(|| "x_sq"))?;
1514 let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), x)?;
1515 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
1516 Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
1517 })?;
1518
1519 cs.enforce(
1520 || "y = x^3 + x + 5",
1521 |lc| {
1522 lc + x_cu.get_variable()
1523 + x.get_variable()
1524 + CS::one()
1525 + CS::one()
1526 + CS::one()
1527 + CS::one()
1528 + CS::one()
1529 },
1530 |lc| lc + CS::one(),
1531 |lc| lc + y.get_variable(),
1532 );
1533
1534 Ok(vec![y])
1535 }
1536
1537 fn output(&self, z: &[F]) -> Vec<F> {
1538 vec![z[0] * z[0] * z[0] + z[0] + F::from(5u64)]
1539 }
1540 }
1541
1542 #[test]
1543 fn test_spartan_snark() {
1544 let circuit = CubicCircuit::default();
1545
1546 // produce keys
1547 let (pk, vk) =
1548 SpartanSNARK::<G, EE, CubicCircuit<<G as Group>::Scalar>>::setup(circuit.clone()).unwrap();
1549
1550 let num_steps = 3;
1551
1552 // setup inputs
1553 let z0 = vec![<G as Group>::Scalar::zero()];
1554 let mut z_i = z0;
1555
1556 for _i in 0..num_steps {
1557 // produce a SNARK
1558 let res = SpartanSNARK::prove(&pk, circuit.clone(), z_i.clone());
1559 assert!(res.is_ok());
1560
1561 let z_i_plus_one = circuit.output(&z_i);
1562
1563 let snark = res.unwrap();
1564
1565 // verify the SNARK
1566 let res = snark.verify(&vk, z_i.clone(), z_i_plus_one.clone());
1567 assert!(res.is_ok());
1568
1569 // set input to the next step
1570 z_i = z_i_plus_one.clone();
1571 }
1572
1573 // sanity: check the claimed output with a direct computation of the same
1574 assert_eq!(z_i, vec![<G as Group>::Scalar::from(2460515u64)]);
1575 }
1576}