Nova/src/spartan/pp.rs
src/spartan/pp.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 compute_digest,
10 errors::NovaError,
11 r1cs::{R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
12 spartan::{
13 math::Math,
14 polynomial::{EqPolynomial, MultilinearPolynomial},
15 powers,
16 sumcheck::{CompressedUniPoly, SumcheckProof, UniPoly},
17 PolyEvalInstance, PolyEvalWitness, SparsePolynomial,
18 },
19 traits::{
20 circuit::StepCircuit,
21 commitment::{CommitmentEngineTrait, CommitmentTrait},
22 evaluation::EvaluationEngineTrait,
23 snark::RelaxedR1CSSNARKTrait,
24 Group, TranscriptEngineTrait, TranscriptReprTrait,
25 },
26 Commitment, CommitmentKey, CompressedCommitment,
27};
28use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError};
29use core::{cmp::max, marker::PhantomData};
30use ff::{Field, PrimeField};
31use itertools::concat;
32use rayon::prelude::*;
33use serde::{Deserialize, Serialize};
34
35fn vec_to_arr<T, const N: usize>(v: Vec<T>) -> [T; N] {
36 v.try_into()
37 .unwrap_or_else(|v: Vec<T>| panic!("Expected a Vec of length {} but it was {}", N, v.len()))
38}
39
40struct IdentityPolynomial<Scalar: PrimeField> {
41 ell: usize,
42 _p: PhantomData<Scalar>,
43}
44
45impl<Scalar: PrimeField> IdentityPolynomial<Scalar> {
46 pub fn new(ell: usize) -> Self {
47 IdentityPolynomial {
48 ell,
49 _p: Default::default(),
50 }
51 }
52
53 pub fn evaluate(&self, r: &[Scalar]) -> Scalar {
54 assert_eq!(self.ell, r.len());
55 (0..self.ell)
56 .map(|i| Scalar::from(2_usize.pow((self.ell - i - 1) as u32) as u64) * r[i])
57 .fold(Scalar::ZERO, |acc, item| acc + item)
58 }
59}
60
61/// A type that holds R1CSShape in a form amenable to memory checking
62#[derive(Clone, Serialize, Deserialize)]
63#[serde(bound = "")]
64pub struct R1CSShapeSparkRepr<G: Group> {
65 N: usize, // size of the vectors
66
67 // dense representation
68 row: Vec<G::Scalar>,
69 col: Vec<G::Scalar>,
70 val_A: Vec<G::Scalar>,
71 val_B: Vec<G::Scalar>,
72 val_C: Vec<G::Scalar>,
73
74 // timestamp polynomials
75 row_read_ts: Vec<G::Scalar>,
76 row_audit_ts: Vec<G::Scalar>,
77 col_read_ts: Vec<G::Scalar>,
78 col_audit_ts: Vec<G::Scalar>,
79}
80
81/// A type that holds a commitment to a sparse polynomial
82#[derive(Clone, Serialize, Deserialize)]
83#[serde(bound = "")]
84pub struct R1CSShapeSparkCommitment<G: Group> {
85 N: usize, // size of each vector
86
87 // commitments to the dense representation
88 comm_row: Commitment<G>,
89 comm_col: Commitment<G>,
90 comm_val_A: Commitment<G>,
91 comm_val_B: Commitment<G>,
92 comm_val_C: Commitment<G>,
93
94 // commitments to the timestamp polynomials
95 comm_row_read_ts: Commitment<G>,
96 comm_row_audit_ts: Commitment<G>,
97 comm_col_read_ts: Commitment<G>,
98 comm_col_audit_ts: Commitment<G>,
99}
100
101impl<G: Group> TranscriptReprTrait<G> for R1CSShapeSparkCommitment<G> {
102 fn to_transcript_bytes(&self) -> Vec<u8> {
103 [
104 self.comm_row,
105 self.comm_col,
106 self.comm_val_A,
107 self.comm_val_B,
108 self.comm_val_C,
109 self.comm_row_read_ts,
110 self.comm_row_audit_ts,
111 self.comm_col_read_ts,
112 self.comm_col_audit_ts,
113 ]
114 .as_slice()
115 .to_transcript_bytes()
116 }
117}
118
119impl<G: Group> R1CSShapeSparkRepr<G> {
120 /// represents R1CSShape in a Spark-friendly format amenable to memory checking
121 pub fn new(S: &R1CSShape<G>) -> R1CSShapeSparkRepr<G> {
122 let N = {
123 let total_nz = S.A.len() + S.B.len() + S.C.len();
124 max(total_nz, max(2 * S.num_vars, S.num_cons)).next_power_of_two()
125 };
126
127 let row = {
128 let mut r = S
129 .A
130 .iter()
131 .chain(S.B.iter())
132 .chain(S.C.iter())
133 .map(|(r, _, _)| *r)
134 .collect::<Vec<usize>>();
135 r.resize(N, 0usize);
136 r
137 };
138
139 let col = {
140 let mut c = S
141 .A
142 .iter()
143 .chain(S.B.iter())
144 .chain(S.C.iter())
145 .map(|(_, c, _)| *c)
146 .collect::<Vec<usize>>();
147 c.resize(N, 0usize);
148 c
149 };
150
151 let val_A = {
152 let mut val = S.A.iter().map(|(_, _, v)| *v).collect::<Vec<G::Scalar>>();
153 val.resize(N, G::Scalar::ZERO);
154 val
155 };
156
157 let val_B = {
158 // prepend zeros
159 let mut val = vec![G::Scalar::ZERO; S.A.len()];
160 val.extend(S.B.iter().map(|(_, _, v)| *v).collect::<Vec<G::Scalar>>());
161 // append zeros
162 val.resize(N, G::Scalar::ZERO);
163 val
164 };
165
166 let val_C = {
167 // prepend zeros
168 let mut val = vec![G::Scalar::ZERO; S.A.len() + S.B.len()];
169 val.extend(S.C.iter().map(|(_, _, v)| *v).collect::<Vec<G::Scalar>>());
170 // append zeros
171 val.resize(N, G::Scalar::ZERO);
172 val
173 };
174
175 // timestamp calculation routine
176 let timestamp_calc =
177 |num_ops: usize, num_cells: usize, addr_trace: &[usize]| -> (Vec<usize>, Vec<usize>) {
178 let mut read_ts = vec![0usize; num_ops];
179 let mut audit_ts = vec![0usize; num_cells];
180
181 assert!(num_ops >= addr_trace.len());
182 for i in 0..addr_trace.len() {
183 let addr = addr_trace[i];
184 assert!(addr < num_cells);
185 let r_ts = audit_ts[addr];
186 read_ts[i] = r_ts;
187
188 let w_ts = r_ts + 1;
189 audit_ts[addr] = w_ts;
190 }
191 (read_ts, audit_ts)
192 };
193
194 // timestamp polynomials for row
195 let (row_read_ts, row_audit_ts) = timestamp_calc(N, N, &row);
196 let (col_read_ts, col_audit_ts) = timestamp_calc(N, N, &col);
197
198 // a routine to turn a vector of usize into a vector scalars
199 let to_vec_scalar = |v: &[usize]| -> Vec<G::Scalar> {
200 (0..v.len())
201 .map(|i| G::Scalar::from(v[i] as u64))
202 .collect::<Vec<G::Scalar>>()
203 };
204
205 R1CSShapeSparkRepr {
206 N,
207
208 // dense representation
209 row: to_vec_scalar(&row),
210 col: to_vec_scalar(&col),
211 val_A,
212 val_B,
213 val_C,
214
215 // timestamp polynomials
216 row_read_ts: to_vec_scalar(&row_read_ts),
217 row_audit_ts: to_vec_scalar(&row_audit_ts),
218 col_read_ts: to_vec_scalar(&col_read_ts),
219 col_audit_ts: to_vec_scalar(&col_audit_ts),
220 }
221 }
222
223 fn commit(&self, ck: &CommitmentKey<G>) -> R1CSShapeSparkCommitment<G> {
224 let comm_vec: Vec<Commitment<G>> = [
225 &self.row,
226 &self.col,
227 &self.val_A,
228 &self.val_B,
229 &self.val_C,
230 &self.row_read_ts,
231 &self.row_audit_ts,
232 &self.col_read_ts,
233 &self.col_audit_ts,
234 ]
235 .par_iter()
236 .map(|v| G::CE::commit(ck, v))
237 .collect();
238
239 R1CSShapeSparkCommitment {
240 N: self.row.len(),
241 comm_row: comm_vec[0],
242 comm_col: comm_vec[1],
243 comm_val_A: comm_vec[2],
244 comm_val_B: comm_vec[3],
245 comm_val_C: comm_vec[4],
246 comm_row_read_ts: comm_vec[5],
247 comm_row_audit_ts: comm_vec[6],
248 comm_col_read_ts: comm_vec[7],
249 comm_col_audit_ts: comm_vec[8],
250 }
251 }
252
253 // computes evaluation oracles
254 fn evaluation_oracles(
255 &self,
256 S: &R1CSShape<G>,
257 r_x: &[G::Scalar],
258 z: &[G::Scalar],
259 ) -> (
260 Vec<G::Scalar>,
261 Vec<G::Scalar>,
262 Vec<G::Scalar>,
263 Vec<G::Scalar>,
264 ) {
265 let r_x_padded = {
266 let mut x = vec![G::Scalar::ZERO; self.N.log_2() - r_x.len()];
267 x.extend(r_x);
268 x
269 };
270
271 let mem_row = EqPolynomial::new(r_x_padded).evals();
272 let mem_col = {
273 let mut z = z.to_vec();
274 z.resize(self.N, G::Scalar::ZERO);
275 z
276 };
277
278 let mut E_row = S
279 .A
280 .iter()
281 .chain(S.B.iter())
282 .chain(S.C.iter())
283 .map(|(r, _, _)| mem_row[*r])
284 .collect::<Vec<G::Scalar>>();
285
286 let mut E_col = S
287 .A
288 .iter()
289 .chain(S.B.iter())
290 .chain(S.C.iter())
291 .map(|(_, c, _)| mem_col[*c])
292 .collect::<Vec<G::Scalar>>();
293
294 E_row.resize(self.N, mem_row[0]); // we place mem_row[0] since resized row is appended with 0s
295 E_col.resize(self.N, mem_col[0]);
296
297 (mem_row, mem_col, E_row, E_col)
298 }
299}
300
301/// Defines a trait for implementing sum-check in a generic manner
302pub trait SumcheckEngine<G: Group> {
303 /// returns the initial claims
304 fn initial_claims(&self) -> Vec<G::Scalar>;
305
306 /// degree of the sum-check polynomial
307 fn degree(&self) -> usize;
308
309 /// the size of the polynomials
310 fn size(&self) -> usize;
311
312 /// returns evaluation points at 0, 2, d-1 (where d is the degree of the sum-check polynomial)
313 fn evaluation_points(&self) -> Vec<Vec<G::Scalar>>;
314
315 /// bounds a variable in the constituent polynomials
316 fn bound(&mut self, r: &G::Scalar);
317
318 /// returns the final claims
319 fn final_claims(&self) -> Vec<Vec<G::Scalar>>;
320}
321
322struct ProductSumcheckInstance<G: Group> {
323 pub(crate) claims: Vec<G::Scalar>, // claimed products
324 pub(crate) comm_output_vec: Vec<Commitment<G>>,
325
326 input_vec: Vec<Vec<G::Scalar>>,
327 output_vec: Vec<Vec<G::Scalar>>,
328
329 poly_A: MultilinearPolynomial<G::Scalar>,
330 poly_B_vec: Vec<MultilinearPolynomial<G::Scalar>>,
331 poly_C_vec: Vec<MultilinearPolynomial<G::Scalar>>,
332 poly_D_vec: Vec<MultilinearPolynomial<G::Scalar>>,
333}
334
335impl<G: Group> ProductSumcheckInstance<G> {
336 pub fn new(
337 ck: &CommitmentKey<G>,
338 input_vec: Vec<Vec<G::Scalar>>, // list of input vectors
339 transcript: &mut G::TE,
340 ) -> Result<Self, NovaError> {
341 let compute_layer = |input: &[G::Scalar]| -> (Vec<G::Scalar>, Vec<G::Scalar>, Vec<G::Scalar>) {
342 let left = (0..input.len() / 2)
343 .map(|i| input[2 * i])
344 .collect::<Vec<G::Scalar>>();
345
346 let right = (0..input.len() / 2)
347 .map(|i| input[2 * i + 1])
348 .collect::<Vec<G::Scalar>>();
349
350 assert_eq!(left.len(), right.len());
351
352 let output = (0..left.len())
353 .map(|i| left[i] * right[i])
354 .collect::<Vec<G::Scalar>>();
355
356 (left, right, output)
357 };
358
359 // a closure that returns left, right, output, product
360 let prepare_inputs =
361 |input: &[G::Scalar]| -> (Vec<G::Scalar>, Vec<G::Scalar>, Vec<G::Scalar>, G::Scalar) {
362 let mut left: Vec<G::Scalar> = Vec::new();
363 let mut right: Vec<G::Scalar> = Vec::new();
364 let mut output: Vec<G::Scalar> = Vec::new();
365
366 let mut out = input.to_vec();
367 for _i in 0..input.len().log_2() {
368 let (l, r, o) = compute_layer(&out);
369 out = o.clone();
370
371 left.extend(l);
372 right.extend(r);
373 output.extend(o);
374 }
375
376 // add a dummy product operation to make the left.len() == right.len() == output.len() == input.len()
377 left.push(output[output.len() - 1]);
378 right.push(G::Scalar::ZERO);
379 output.push(G::Scalar::ZERO);
380
381 // output is stored at the last but one position
382 let product = output[output.len() - 2];
383
384 assert_eq!(left.len(), right.len());
385 assert_eq!(left.len(), output.len());
386 (left, right, output, product)
387 };
388
389 let mut left_vec = Vec::new();
390 let mut right_vec = Vec::new();
391 let mut output_vec = Vec::new();
392 let mut claims = Vec::new();
393 for input in input_vec.iter() {
394 let (l, r, o, p) = prepare_inputs(input);
395 left_vec.push(l);
396 right_vec.push(r);
397 output_vec.push(o);
398 claims.push(p);
399 }
400
401 // commit to the outputs
402 let comm_output_vec = (0..output_vec.len())
403 .into_par_iter()
404 .map(|i| G::CE::commit(ck, &output_vec[i]))
405 .collect::<Vec<_>>();
406
407 // absorb the output commitment and the claimed product
408 transcript.absorb(b"o", &comm_output_vec.as_slice());
409 transcript.absorb(b"c", &claims.as_slice());
410
411 // generate randomness for the eq polynomial
412 let num_rounds = output_vec[0].len().log_2();
413 let rand_eq = (0..num_rounds)
414 .map(|_i| transcript.squeeze(b"e"))
415 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
416
417 let poly_A = MultilinearPolynomial::new(EqPolynomial::new(rand_eq).evals());
418 let poly_B_vec = left_vec
419 .clone()
420 .into_par_iter()
421 .map(MultilinearPolynomial::new)
422 .collect::<Vec<_>>();
423 let poly_C_vec = right_vec
424 .clone()
425 .into_par_iter()
426 .map(MultilinearPolynomial::new)
427 .collect::<Vec<_>>();
428 let poly_D_vec = output_vec
429 .clone()
430 .into_par_iter()
431 .map(MultilinearPolynomial::new)
432 .collect::<Vec<_>>();
433
434 Ok(Self {
435 claims,
436 comm_output_vec,
437 input_vec,
438 output_vec,
439 poly_A,
440 poly_B_vec,
441 poly_C_vec,
442 poly_D_vec,
443 })
444 }
445}
446
447impl<G: Group> SumcheckEngine<G> for ProductSumcheckInstance<G> {
448 fn initial_claims(&self) -> Vec<G::Scalar> {
449 vec![G::Scalar::ZERO; 8]
450 }
451
452 fn degree(&self) -> usize {
453 3
454 }
455
456 fn size(&self) -> usize {
457 for poly_B in &self.poly_B_vec {
458 assert_eq!(poly_B.len(), self.poly_A.len());
459 }
460 for poly_C in &self.poly_C_vec {
461 assert_eq!(poly_C.len(), self.poly_A.len());
462 }
463 for poly_D in &self.poly_D_vec {
464 assert_eq!(poly_D.len(), self.poly_A.len());
465 }
466 self.poly_A.len()
467 }
468
469 fn evaluation_points(&self) -> Vec<Vec<G::Scalar>> {
470 let poly_A = &self.poly_A;
471
472 let comb_func =
473 |poly_A_comp: &G::Scalar,
474 poly_B_comp: &G::Scalar,
475 poly_C_comp: &G::Scalar,
476 poly_D_comp: &G::Scalar|
477 -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) };
478
479 self
480 .poly_B_vec
481 .iter()
482 .zip(self.poly_C_vec.iter())
483 .zip(self.poly_D_vec.iter())
484 .map(|((poly_B, poly_C), poly_D)| {
485 let len = poly_B.len() / 2;
486 // Make an iterator returning the contributions to the evaluations
487 let (eval_point_0, eval_point_2, eval_point_3) = (0..len)
488 .into_par_iter()
489 .map(|i| {
490 // eval 0: bound_func is A(low)
491 let eval_point_0 = comb_func(&poly_A[i], &poly_B[i], &poly_C[i], &poly_D[i]);
492
493 // eval 2: bound_func is -A(low) + 2*A(high)
494 let poly_A_bound_point = poly_A[len + i] + poly_A[len + i] - poly_A[i];
495 let poly_B_bound_point = poly_B[len + i] + poly_B[len + i] - poly_B[i];
496 let poly_C_bound_point = poly_C[len + i] + poly_C[len + i] - poly_C[i];
497 let poly_D_bound_point = poly_D[len + i] + poly_D[len + i] - poly_D[i];
498 let eval_point_2 = comb_func(
499 &poly_A_bound_point,
500 &poly_B_bound_point,
501 &poly_C_bound_point,
502 &poly_D_bound_point,
503 );
504
505 // eval 3: bound_func is -2A(low) + 3A(high); computed incrementally with bound_func applied to eval(2)
506 let poly_A_bound_point = poly_A_bound_point + poly_A[len + i] - poly_A[i];
507 let poly_B_bound_point = poly_B_bound_point + poly_B[len + i] - poly_B[i];
508 let poly_C_bound_point = poly_C_bound_point + poly_C[len + i] - poly_C[i];
509 let poly_D_bound_point = poly_D_bound_point + poly_D[len + i] - poly_D[i];
510 let eval_point_3 = comb_func(
511 &poly_A_bound_point,
512 &poly_B_bound_point,
513 &poly_C_bound_point,
514 &poly_D_bound_point,
515 );
516 (eval_point_0, eval_point_2, eval_point_3)
517 })
518 .reduce(
519 || (G::Scalar::ZERO, G::Scalar::ZERO, G::Scalar::ZERO),
520 |a, b| (a.0 + b.0, a.1 + b.1, a.2 + b.2),
521 );
522 vec![eval_point_0, eval_point_2, eval_point_3]
523 })
524 .collect::<Vec<Vec<G::Scalar>>>()
525 }
526
527 fn bound(&mut self, r: &G::Scalar) {
528 self.poly_A.bound_poly_var_top(r);
529 for ((poly_B, poly_C), poly_D) in self
530 .poly_B_vec
531 .iter_mut()
532 .zip(self.poly_C_vec.iter_mut())
533 .zip(self.poly_D_vec.iter_mut())
534 {
535 poly_B.bound_poly_var_top(r);
536 poly_C.bound_poly_var_top(r);
537 poly_D.bound_poly_var_top(r);
538 }
539 }
540 fn final_claims(&self) -> Vec<Vec<G::Scalar>> {
541 let poly_A_final = vec![self.poly_A[0]];
542 let poly_B_final = (0..self.poly_B_vec.len())
543 .map(|i| self.poly_B_vec[i][0])
544 .collect();
545 let poly_C_final = (0..self.poly_C_vec.len())
546 .map(|i| self.poly_C_vec[i][0])
547 .collect();
548 let poly_D_final = (0..self.poly_D_vec.len())
549 .map(|i| self.poly_D_vec[i][0])
550 .collect();
551
552 vec![poly_A_final, poly_B_final, poly_C_final, poly_D_final]
553 }
554}
555
556struct OuterSumcheckInstance<G: Group> {
557 poly_tau: MultilinearPolynomial<G::Scalar>,
558 poly_Az: MultilinearPolynomial<G::Scalar>,
559 poly_Bz: MultilinearPolynomial<G::Scalar>,
560 poly_uCz_E: MultilinearPolynomial<G::Scalar>,
561}
562
563impl<G: Group> SumcheckEngine<G> for OuterSumcheckInstance<G> {
564 fn initial_claims(&self) -> Vec<G::Scalar> {
565 vec![G::Scalar::ZERO]
566 }
567
568 fn degree(&self) -> usize {
569 3
570 }
571
572 fn size(&self) -> usize {
573 assert_eq!(self.poly_tau.len(), self.poly_Az.len());
574 assert_eq!(self.poly_tau.len(), self.poly_Bz.len());
575 assert_eq!(self.poly_tau.len(), self.poly_uCz_E.len());
576 self.poly_tau.len()
577 }
578
579 fn evaluation_points(&self) -> Vec<Vec<G::Scalar>> {
580 let (poly_A, poly_B, poly_C, poly_D) = (
581 &self.poly_tau,
582 &self.poly_Az,
583 &self.poly_Bz,
584 &self.poly_uCz_E,
585 );
586 let comb_func =
587 |poly_A_comp: &G::Scalar,
588 poly_B_comp: &G::Scalar,
589 poly_C_comp: &G::Scalar,
590 poly_D_comp: &G::Scalar|
591 -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) };
592 let len = poly_A.len() / 2;
593
594 // Make an iterator returning the contributions to the evaluations
595 let (eval_point_0, eval_point_2, eval_point_3) = (0..len)
596 .into_par_iter()
597 .map(|i| {
598 // eval 0: bound_func is A(low)
599 let eval_point_0 = comb_func(&poly_A[i], &poly_B[i], &poly_C[i], &poly_D[i]);
600
601 // eval 2: bound_func is -A(low) + 2*A(high)
602 let poly_A_bound_point = poly_A[len + i] + poly_A[len + i] - poly_A[i];
603 let poly_B_bound_point = poly_B[len + i] + poly_B[len + i] - poly_B[i];
604 let poly_C_bound_point = poly_C[len + i] + poly_C[len + i] - poly_C[i];
605 let poly_D_bound_point = poly_D[len + i] + poly_D[len + i] - poly_D[i];
606 let eval_point_2 = comb_func(
607 &poly_A_bound_point,
608 &poly_B_bound_point,
609 &poly_C_bound_point,
610 &poly_D_bound_point,
611 );
612
613 // eval 3: bound_func is -2A(low) + 3A(high); computed incrementally with bound_func applied to eval(2)
614 let poly_A_bound_point = poly_A_bound_point + poly_A[len + i] - poly_A[i];
615 let poly_B_bound_point = poly_B_bound_point + poly_B[len + i] - poly_B[i];
616 let poly_C_bound_point = poly_C_bound_point + poly_C[len + i] - poly_C[i];
617 let poly_D_bound_point = poly_D_bound_point + poly_D[len + i] - poly_D[i];
618 let eval_point_3 = comb_func(
619 &poly_A_bound_point,
620 &poly_B_bound_point,
621 &poly_C_bound_point,
622 &poly_D_bound_point,
623 );
624 (eval_point_0, eval_point_2, eval_point_3)
625 })
626 .reduce(
627 || (G::Scalar::ZERO, G::Scalar::ZERO, G::Scalar::ZERO),
628 |a, b| (a.0 + b.0, a.1 + b.1, a.2 + b.2),
629 );
630
631 vec![vec![eval_point_0, eval_point_2, eval_point_3]]
632 }
633
634 fn bound(&mut self, r: &G::Scalar) {
635 self.poly_tau.bound_poly_var_top(r);
636 self.poly_Az.bound_poly_var_top(r);
637 self.poly_Bz.bound_poly_var_top(r);
638 self.poly_uCz_E.bound_poly_var_top(r);
639 }
640
641 fn final_claims(&self) -> Vec<Vec<G::Scalar>> {
642 vec![vec![
643 self.poly_tau[0],
644 self.poly_Az[0],
645 self.poly_Bz[0],
646 self.poly_uCz_E[0],
647 ]]
648 }
649}
650
651struct InnerSumcheckInstance<G: Group> {
652 claim: G::Scalar,
653 poly_E_row: MultilinearPolynomial<G::Scalar>,
654 poly_E_col: MultilinearPolynomial<G::Scalar>,
655 poly_val: MultilinearPolynomial<G::Scalar>,
656}
657
658impl<G: Group> SumcheckEngine<G> for InnerSumcheckInstance<G> {
659 fn initial_claims(&self) -> Vec<G::Scalar> {
660 vec![self.claim]
661 }
662
663 fn degree(&self) -> usize {
664 3
665 }
666
667 fn size(&self) -> usize {
668 assert_eq!(self.poly_E_row.len(), self.poly_val.len());
669 assert_eq!(self.poly_E_row.len(), self.poly_E_col.len());
670 self.poly_E_row.len()
671 }
672
673 fn evaluation_points(&self) -> Vec<Vec<G::Scalar>> {
674 let (poly_A, poly_B, poly_C) = (&self.poly_E_row, &self.poly_E_col, &self.poly_val);
675 let comb_func = |poly_A_comp: &G::Scalar,
676 poly_B_comp: &G::Scalar,
677 poly_C_comp: &G::Scalar|
678 -> G::Scalar { *poly_A_comp * *poly_B_comp * *poly_C_comp };
679 let len = poly_A.len() / 2;
680
681 // Make an iterator returning the contributions to the evaluations
682 let (eval_point_0, eval_point_2, eval_point_3) = (0..len)
683 .into_par_iter()
684 .map(|i| {
685 // eval 0: bound_func is A(low)
686 let eval_point_0 = comb_func(&poly_A[i], &poly_B[i], &poly_C[i]);
687
688 // eval 2: bound_func is -A(low) + 2*A(high)
689 let poly_A_bound_point = poly_A[len + i] + poly_A[len + i] - poly_A[i];
690 let poly_B_bound_point = poly_B[len + i] + poly_B[len + i] - poly_B[i];
691 let poly_C_bound_point = poly_C[len + i] + poly_C[len + i] - poly_C[i];
692 let eval_point_2 = comb_func(
693 &poly_A_bound_point,
694 &poly_B_bound_point,
695 &poly_C_bound_point,
696 );
697
698 // eval 3: bound_func is -2A(low) + 3A(high); computed incrementally with bound_func applied to eval(2)
699 let poly_A_bound_point = poly_A_bound_point + poly_A[len + i] - poly_A[i];
700 let poly_B_bound_point = poly_B_bound_point + poly_B[len + i] - poly_B[i];
701 let poly_C_bound_point = poly_C_bound_point + poly_C[len + i] - poly_C[i];
702 let eval_point_3 = comb_func(
703 &poly_A_bound_point,
704 &poly_B_bound_point,
705 &poly_C_bound_point,
706 );
707 (eval_point_0, eval_point_2, eval_point_3)
708 })
709 .reduce(
710 || (G::Scalar::ZERO, G::Scalar::ZERO, G::Scalar::ZERO),
711 |a, b| (a.0 + b.0, a.1 + b.1, a.2 + b.2),
712 );
713
714 vec![vec![eval_point_0, eval_point_2, eval_point_3]]
715 }
716
717 fn bound(&mut self, r: &G::Scalar) {
718 self.poly_E_row.bound_poly_var_top(r);
719 self.poly_E_col.bound_poly_var_top(r);
720 self.poly_val.bound_poly_var_top(r);
721 }
722
723 fn final_claims(&self) -> Vec<Vec<G::Scalar>> {
724 vec![vec![
725 self.poly_E_row[0],
726 self.poly_E_col[0],
727 self.poly_val[0],
728 ]]
729 }
730}
731
732/// A type that represents the prover's key
733#[derive(Clone, Serialize, Deserialize)]
734#[serde(bound = "")]
735pub struct ProverKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
736 pk_ee: EE::ProverKey,
737 S: R1CSShape<G>,
738 S_repr: R1CSShapeSparkRepr<G>,
739 S_comm: R1CSShapeSparkCommitment<G>,
740 vk_digest: G::Scalar, // digest of verifier's key
741}
742
743/// A type that represents the verifier's key
744#[derive(Clone, Serialize, Deserialize)]
745#[serde(bound = "")]
746pub struct VerifierKey<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
747 num_cons: usize,
748 num_vars: usize,
749 vk_ee: EE::VerifierKey,
750 S_comm: R1CSShapeSparkCommitment<G>,
751 digest: G::Scalar,
752}
753
754/// A succinct proof of knowledge of a witness to a relaxed R1CS instance
755/// The proof is produced using Spartan's combination of the sum-check and
756/// the commitment to a vector viewed as a polynomial commitment
757#[derive(Clone, Serialize, Deserialize)]
758#[serde(bound = "")]
759pub struct RelaxedR1CSSNARK<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> {
760 // commitment to oracles
761 comm_Az: CompressedCommitment<G>,
762 comm_Bz: CompressedCommitment<G>,
763 comm_Cz: CompressedCommitment<G>,
764
765 // commitment to oracles for the inner sum-check
766 comm_E_row: CompressedCommitment<G>,
767 comm_E_col: CompressedCommitment<G>,
768
769 // initial claims
770 eval_Az_at_tau: G::Scalar,
771 eval_Bz_at_tau: G::Scalar,
772 eval_Cz_at_tau: G::Scalar,
773
774 comm_output_arr: [CompressedCommitment<G>; 8],
775 claims_product_arr: [G::Scalar; 8],
776
777 // satisfiability sum-check
778 sc_sat: SumcheckProof<G>,
779
780 // claims from the end of the sum-check
781 eval_Az: G::Scalar,
782 eval_Bz: G::Scalar,
783 eval_Cz: G::Scalar,
784 eval_E: G::Scalar,
785 eval_E_row: G::Scalar,
786 eval_E_col: G::Scalar,
787 eval_val_A: G::Scalar,
788 eval_val_B: G::Scalar,
789 eval_val_C: G::Scalar,
790 eval_left_arr: [G::Scalar; 8],
791 eval_right_arr: [G::Scalar; 8],
792 eval_output_arr: [G::Scalar; 8],
793 eval_input_arr: [G::Scalar; 8],
794 eval_output2_arr: [G::Scalar; 8],
795
796 eval_row: G::Scalar,
797 eval_row_read_ts: G::Scalar,
798 eval_E_row_at_r_prod: G::Scalar,
799 eval_row_audit_ts: G::Scalar,
800 eval_col: G::Scalar,
801 eval_col_read_ts: G::Scalar,
802 eval_E_col_at_r_prod: G::Scalar,
803 eval_col_audit_ts: G::Scalar,
804 eval_W: G::Scalar,
805
806 // batch openings of all multilinear polynomials
807 sc_proof_batch: SumcheckProof<G>,
808 evals_batch_arr: [G::Scalar; 7],
809 eval_arg: EE::EvaluationArgument,
810}
811
812impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARK<G, EE> {
813 fn prove_inner<T1, T2, T3>(
814 mem: &mut T1,
815 outer: &mut T2,
816 inner: &mut T3,
817 transcript: &mut G::TE,
818 ) -> Result<
819 (
820 SumcheckProof<G>,
821 Vec<G::Scalar>,
822 Vec<Vec<G::Scalar>>,
823 Vec<Vec<G::Scalar>>,
824 Vec<Vec<G::Scalar>>,
825 ),
826 NovaError,
827 >
828 where
829 T1: SumcheckEngine<G>,
830 T2: SumcheckEngine<G>,
831 T3: SumcheckEngine<G>,
832 {
833 // sanity checks
834 assert_eq!(mem.size(), outer.size());
835 assert_eq!(mem.size(), inner.size());
836 assert_eq!(mem.degree(), outer.degree());
837 assert_eq!(mem.degree(), inner.degree());
838
839 // these claims are already added to the transcript, so we do not need to add
840 let claims = {
841 let claims_mem = mem.initial_claims();
842 let claims_outer = outer.initial_claims();
843 let claims_inner = inner.initial_claims();
844 claims_mem
845 .into_iter()
846 .chain(claims_outer.into_iter())
847 .chain(claims_inner.into_iter())
848 .collect::<Vec<G::Scalar>>()
849 };
850
851 let num_claims = claims.len();
852 let coeffs = {
853 let s = transcript.squeeze(b"r")?;
854 let mut s_vec = vec![s];
855 for i in 1..num_claims {
856 s_vec.push(s_vec[i - 1] * s);
857 }
858 s_vec
859 };
860
861 // compute the joint claim
862 let claim = claims
863 .iter()
864 .zip(coeffs.iter())
865 .map(|(c_1, c_2)| *c_1 * c_2)
866 .fold(G::Scalar::ZERO, |acc, item| acc + item);
867
868 let mut e = claim;
869 let mut r: Vec<G::Scalar> = Vec::new();
870 let mut cubic_polys: Vec<CompressedUniPoly<G>> = Vec::new();
871 let num_rounds = mem.size().log_2();
872 for _i in 0..num_rounds {
873 let mut evals: Vec<Vec<G::Scalar>> = Vec::new();
874 evals.extend(mem.evaluation_points());
875 evals.extend(outer.evaluation_points());
876 evals.extend(inner.evaluation_points());
877 assert_eq!(evals.len(), num_claims);
878
879 let evals_combined_0 = (0..evals.len())
880 .map(|i| evals[i][0] * coeffs[i])
881 .fold(G::Scalar::ZERO, |acc, item| acc + item);
882 let evals_combined_2 = (0..evals.len())
883 .map(|i| evals[i][1] * coeffs[i])
884 .fold(G::Scalar::ZERO, |acc, item| acc + item);
885 let evals_combined_3 = (0..evals.len())
886 .map(|i| evals[i][2] * coeffs[i])
887 .fold(G::Scalar::ZERO, |acc, item| acc + item);
888
889 let evals = vec![
890 evals_combined_0,
891 e - evals_combined_0,
892 evals_combined_2,
893 evals_combined_3,
894 ];
895 let poly = UniPoly::from_evals(&evals);
896
897 // append the prover's message to the transcript
898 transcript.absorb(b"p", &poly);
899
900 // derive the verifier's challenge for the next round
901 let r_i = transcript.squeeze(b"c")?;
902 r.push(r_i);
903
904 mem.bound(&r_i);
905 outer.bound(&r_i);
906 inner.bound(&r_i);
907
908 e = poly.evaluate(&r_i);
909 cubic_polys.push(poly.compress());
910 }
911
912 let mem_claims = mem.final_claims();
913 let outer_claims = outer.final_claims();
914 let inner_claims = inner.final_claims();
915
916 Ok((
917 SumcheckProof::new(cubic_polys),
918 r,
919 mem_claims,
920 outer_claims,
921 inner_claims,
922 ))
923 }
924}
925
926impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G>
927 for RelaxedR1CSSNARK<G, EE>
928{
929 type ProverKey = ProverKey<G, EE>;
930 type VerifierKey = VerifierKey<G, EE>;
931
932 fn setup(
933 ck: &CommitmentKey<G>,
934 S: &R1CSShape<G>,
935 ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> {
936 let (pk_ee, vk_ee) = EE::setup(ck);
937
938 // pad the R1CS matrices
939 let S = S.pad();
940
941 let S_repr = R1CSShapeSparkRepr::new(&S);
942 let S_comm = S_repr.commit(ck);
943
944 let vk = {
945 let mut vk = VerifierKey {
946 num_cons: S.num_cons,
947 num_vars: S.num_vars,
948 S_comm: S_comm.clone(),
949 vk_ee,
950 digest: G::Scalar::ZERO,
951 };
952 vk.digest = compute_digest::<G, VerifierKey<G, EE>>(&vk);
953 vk
954 };
955
956 let pk = ProverKey {
957 pk_ee,
958 S,
959 S_repr,
960 S_comm,
961 vk_digest: vk.digest,
962 };
963
964 Ok((pk, vk))
965 }
966
967 /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
968 fn prove(
969 ck: &CommitmentKey<G>,
970 pk: &Self::ProverKey,
971 U: &RelaxedR1CSInstance<G>,
972 W: &RelaxedR1CSWitness<G>,
973 ) -> Result<Self, NovaError> {
974 let W = W.pad(&pk.S); // pad the witness
975 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
976
977 // a list of polynomial evaluation claims that will be batched
978 let mut w_u_vec = Vec::new();
979
980 // sanity check that R1CSShape has certain size characteristics
981 assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
982 assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
983 assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
984 assert!(pk.S.num_io < pk.S.num_vars);
985
986 // append the verifier key (which includes commitment to R1CS matrices) and the RelaxedR1CSInstance to the transcript
987 transcript.absorb(b"vk", &pk.vk_digest);
988 transcript.absorb(b"U", U);
989
990 // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
991 let z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
992
993 // compute Az, Bz, Cz
994 let (mut Az, mut Bz, mut Cz) = pk.S.multiply_vec(&z)?;
995
996 // commit to Az, Bz, Cz
997 let (comm_Az, (comm_Bz, comm_Cz)) = rayon::join(
998 || G::CE::commit(ck, &Az),
999 || rayon::join(|| G::CE::commit(ck, &Bz), || G::CE::commit(ck, &Cz)),
1000 );
1001
1002 transcript.absorb(b"c", &[comm_Az, comm_Bz, comm_Cz].as_slice());
1003
1004 // number of rounds of the satisfiability sum-check
1005 let num_rounds_sat = pk.S_repr.N.log_2();
1006 let tau = (0..num_rounds_sat)
1007 .map(|_| transcript.squeeze(b"t"))
1008 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1009
1010 // (1) send commitments to Az, Bz, and Cz along with their evaluations at tau
1011 let (Az, Bz, Cz, E) = {
1012 Az.resize(pk.S_repr.N, G::Scalar::ZERO);
1013 Bz.resize(pk.S_repr.N, G::Scalar::ZERO);
1014 Cz.resize(pk.S_repr.N, G::Scalar::ZERO);
1015
1016 let mut E = W.E.clone();
1017 E.resize(pk.S_repr.N, G::Scalar::ZERO);
1018
1019 (Az, Bz, Cz, E)
1020 };
1021 let (eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau) = {
1022 let evals_at_tau = [&Az, &Bz, &Cz]
1023 .into_par_iter()
1024 .map(|p| MultilinearPolynomial::evaluate_with(p, &tau))
1025 .collect::<Vec<G::Scalar>>();
1026 (evals_at_tau[0], evals_at_tau[1], evals_at_tau[2])
1027 };
1028
1029 // (2) send commitments to the following two oracles
1030 // E_row(i) = eq(tau, row(i)) for all i
1031 // E_col(i) = z(col(i)) for all i
1032 let (mem_row, mem_col, E_row, E_col) = pk.S_repr.evaluation_oracles(&pk.S, &tau, &z);
1033 let (comm_E_row, comm_E_col) =
1034 rayon::join(|| G::CE::commit(ck, &E_row), || G::CE::commit(ck, &E_col));
1035
1036 // absorb the claimed evaluations into the transcript
1037 transcript.absorb(
1038 b"e",
1039 &[eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau].as_slice(),
1040 );
1041 // absorb commitments to E_row and E_col in the transcript
1042 transcript.absorb(b"e", &vec![comm_E_row, comm_E_col].as_slice());
1043
1044 // add claims about Az, Bz, and Cz to be checked later
1045 // since all the three polynomials are opened at tau,
1046 // we can combine them into a single polynomial opened at tau
1047 let eval_vec = vec![eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau];
1048 let comm_vec = vec![comm_Az, comm_Bz, comm_Cz];
1049 let poly_vec = vec![&Az, &Bz, &Cz];
1050 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1051 let c = transcript.squeeze(b"c")?;
1052 let w = PolyEvalWitness::batch(&poly_vec, &c);
1053 let u = PolyEvalInstance::batch(&comm_vec, &tau, &eval_vec, &c);
1054 w_u_vec.push((w, u));
1055
1056 let c_inner = c;
1057
1058 // we now need to prove three claims
1059 // (1) 0 = \sum_x poly_tau(x) * (poly_Az(x) * poly_Bz(x) - poly_uCz_E(x))
1060 // (2) eval_Az_at_tau + r * eval_Bz_at_tau + r^2 * eval_Cz_at_tau = \sum_y E_row(y) * (val_A(y) + r * val_B(y) + r^2 * val_C(y)) * E_col(y)
1061 // (3) E_row(i) = eq(tau, row(i)) and E_col(i) = z(col(i))
1062
1063 // a sum-check instance to prove the first claim
1064 let mut outer_sc_inst = OuterSumcheckInstance {
1065 poly_tau: MultilinearPolynomial::new(EqPolynomial::new(tau).evals()),
1066 poly_Az: MultilinearPolynomial::new(Az.clone()),
1067 poly_Bz: MultilinearPolynomial::new(Bz.clone()),
1068 poly_uCz_E: {
1069 let uCz_E = (0..Cz.len())
1070 .map(|i| U.u * Cz[i] + E[i])
1071 .collect::<Vec<G::Scalar>>();
1072 MultilinearPolynomial::new(uCz_E)
1073 },
1074 };
1075
1076 // a sum-check instance to prove the second claim
1077 let val = pk
1078 .S_repr
1079 .val_A
1080 .iter()
1081 .zip(pk.S_repr.val_B.iter())
1082 .zip(pk.S_repr.val_C.iter())
1083 .map(|((v_a, v_b), v_c)| *v_a + c_inner * *v_b + c_inner * c_inner * *v_c)
1084 .collect::<Vec<G::Scalar>>();
1085 let mut inner_sc_inst = InnerSumcheckInstance {
1086 claim: eval_Az_at_tau + c_inner * eval_Bz_at_tau + c_inner * c_inner * eval_Cz_at_tau,
1087 poly_E_row: MultilinearPolynomial::new(E_row.clone()),
1088 poly_E_col: MultilinearPolynomial::new(E_col.clone()),
1089 poly_val: MultilinearPolynomial::new(val),
1090 };
1091
1092 // a third sum-check instance to prove the memory-related claim
1093 // we now need to prove that E_row and E_col are well-formed
1094 // we use memory checking: H(INIT) * H(WS) =? H(RS) * H(FINAL)
1095 let gamma_1 = transcript.squeeze(b"g1")?;
1096 let gamma_2 = transcript.squeeze(b"g2")?;
1097
1098 let gamma_1_sqr = gamma_1 * gamma_1;
1099 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
1100 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
1101 };
1102
1103 let init_row = (0..mem_row.len())
1104 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_row[i], &G::Scalar::ZERO))
1105 .collect::<Vec<G::Scalar>>();
1106 let read_row = (0..E_row.len())
1107 .map(|i| hash_func(&pk.S_repr.row[i], &E_row[i], &pk.S_repr.row_read_ts[i]))
1108 .collect::<Vec<G::Scalar>>();
1109 let write_row = (0..E_row.len())
1110 .map(|i| {
1111 hash_func(
1112 &pk.S_repr.row[i],
1113 &E_row[i],
1114 &(pk.S_repr.row_read_ts[i] + G::Scalar::ONE),
1115 )
1116 })
1117 .collect::<Vec<G::Scalar>>();
1118 let audit_row = (0..mem_row.len())
1119 .map(|i| {
1120 hash_func(
1121 &G::Scalar::from(i as u64),
1122 &mem_row[i],
1123 &pk.S_repr.row_audit_ts[i],
1124 )
1125 })
1126 .collect::<Vec<G::Scalar>>();
1127
1128 let init_col = (0..mem_col.len())
1129 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_col[i], &G::Scalar::ZERO))
1130 .collect::<Vec<G::Scalar>>();
1131 let read_col = (0..E_col.len())
1132 .map(|i| hash_func(&pk.S_repr.col[i], &E_col[i], &pk.S_repr.col_read_ts[i]))
1133 .collect::<Vec<G::Scalar>>();
1134 let write_col = (0..E_col.len())
1135 .map(|i| {
1136 hash_func(
1137 &pk.S_repr.col[i],
1138 &E_col[i],
1139 &(pk.S_repr.col_read_ts[i] + G::Scalar::ONE),
1140 )
1141 })
1142 .collect::<Vec<G::Scalar>>();
1143 let audit_col = (0..mem_col.len())
1144 .map(|i| {
1145 hash_func(
1146 &G::Scalar::from(i as u64),
1147 &mem_col[i],
1148 &pk.S_repr.col_audit_ts[i],
1149 )
1150 })
1151 .collect::<Vec<G::Scalar>>();
1152
1153 let mut mem_sc_inst = ProductSumcheckInstance::new(
1154 ck,
1155 vec![
1156 init_row, read_row, write_row, audit_row, init_col, read_col, write_col, audit_col,
1157 ],
1158 &mut transcript,
1159 )?;
1160
1161 let (sc_sat, r_sat, claims_mem, claims_outer, claims_inner) = Self::prove_inner(
1162 &mut mem_sc_inst,
1163 &mut outer_sc_inst,
1164 &mut inner_sc_inst,
1165 &mut transcript,
1166 )?;
1167
1168 // claims[0] is about the Eq polynomial, which the verifier computes directly
1169 // claims[1] =? weighed sum of left(rand)
1170 // claims[2] =? weighted sum of right(rand)
1171 // claims[3] =? weighted sum of output(rand), which is easy to verify by querying output
1172 // we also need to prove that output(output.len()-2) = claimed_product
1173 let eval_left_vec = claims_mem[1].clone();
1174 let eval_right_vec = claims_mem[2].clone();
1175 let eval_output_vec = claims_mem[3].clone();
1176
1177 // claims from the end of sum-check
1178 let (eval_Az, eval_Bz): (G::Scalar, G::Scalar) = (claims_outer[0][1], claims_outer[0][2]);
1179 let eval_Cz = MultilinearPolynomial::evaluate_with(&Cz, &r_sat);
1180 let eval_E = MultilinearPolynomial::evaluate_with(&E, &r_sat);
1181 let eval_E_row = claims_inner[0][0];
1182 let eval_E_col = claims_inner[0][1];
1183 let eval_val_A = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_A, &r_sat);
1184 let eval_val_B = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_B, &r_sat);
1185 let eval_val_C = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_C, &r_sat);
1186 let eval_vec = vec![
1187 eval_Az, eval_Bz, eval_Cz, eval_E, eval_E_row, eval_E_col, eval_val_A, eval_val_B, eval_val_C,
1188 ]
1189 .into_iter()
1190 .chain(eval_left_vec.clone().into_iter())
1191 .chain(eval_right_vec.clone().into_iter())
1192 .chain(eval_output_vec.clone().into_iter())
1193 .collect::<Vec<G::Scalar>>();
1194
1195 // absorb all the claimed evaluations
1196 transcript.absorb(b"e", &eval_vec.as_slice());
1197
1198 // we now combine eval_left = left(rand) and eval_right = right(rand)
1199 // into claims about input and output
1200 let c = transcript.squeeze(b"c")?;
1201
1202 // eval = (G::Scalar::ONE - c) * eval_left + c * eval_right
1203 // eval is claimed evaluation of input||output(r, c), which can be proven by proving input(r[1..], c) and output(r[1..], c)
1204 let rand_ext = {
1205 let mut r = r_sat.clone();
1206 r.extend(&[c]);
1207 r
1208 };
1209 let eval_input_vec = mem_sc_inst
1210 .input_vec
1211 .iter()
1212 .map(|i| MultilinearPolynomial::evaluate_with(i, &rand_ext[1..]))
1213 .collect::<Vec<G::Scalar>>();
1214
1215 let eval_output2_vec = mem_sc_inst
1216 .output_vec
1217 .iter()
1218 .map(|o| MultilinearPolynomial::evaluate_with(o, &rand_ext[1..]))
1219 .collect::<Vec<G::Scalar>>();
1220
1221 // add claimed evaluations to the transcript
1222 let evals = eval_input_vec
1223 .clone()
1224 .into_iter()
1225 .chain(eval_output2_vec.clone().into_iter())
1226 .collect::<Vec<G::Scalar>>();
1227 transcript.absorb(b"e", &evals.as_slice());
1228
1229 // squeeze a challenge to combine multiple claims into one
1230 let powers_of_rho = {
1231 let s = transcript.squeeze(b"r")?;
1232 let mut s_vec = vec![s];
1233 for i in 1..mem_sc_inst.initial_claims().len() {
1234 s_vec.push(s_vec[i - 1] * s);
1235 }
1236 s_vec
1237 };
1238
1239 // take weighted sum of input, output, and their commitments
1240 let product = mem_sc_inst
1241 .claims
1242 .iter()
1243 .zip(powers_of_rho.iter())
1244 .map(|(e, p)| *e * p)
1245 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1246
1247 let eval_output = eval_output_vec
1248 .iter()
1249 .zip(powers_of_rho.iter())
1250 .map(|(e, p)| *e * p)
1251 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1252
1253 let comm_output = mem_sc_inst
1254 .comm_output_vec
1255 .iter()
1256 .zip(powers_of_rho.iter())
1257 .map(|(c, r_i)| *c * *r_i)
1258 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1259
1260 let weighted_sum = |W: &[Vec<G::Scalar>], s: &[G::Scalar]| -> Vec<G::Scalar> {
1261 assert_eq!(W.len(), s.len());
1262 let mut p = vec![G::Scalar::ZERO; W[0].len()];
1263 for i in 0..W.len() {
1264 for (j, item) in W[i].iter().enumerate().take(W[i].len()) {
1265 p[j] += *item * s[i]
1266 }
1267 }
1268 p
1269 };
1270
1271 let poly_output = weighted_sum(&mem_sc_inst.output_vec, &powers_of_rho);
1272
1273 let eval_output2 = eval_output2_vec
1274 .iter()
1275 .zip(powers_of_rho.iter())
1276 .map(|(e, p)| *e * p)
1277 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1278
1279 // eval_output = output(r_sat)
1280 w_u_vec.push((
1281 PolyEvalWitness {
1282 p: poly_output.clone(),
1283 },
1284 PolyEvalInstance {
1285 c: comm_output,
1286 x: r_sat.clone(),
1287 e: eval_output,
1288 },
1289 ));
1290
1291 // claimed_product = output(1, ..., 1, 0)
1292 let x = {
1293 let mut x = vec![G::Scalar::ONE; r_sat.len()];
1294 x[r_sat.len() - 1] = G::Scalar::ZERO;
1295 x
1296 };
1297 w_u_vec.push((
1298 PolyEvalWitness {
1299 p: poly_output.clone(),
1300 },
1301 PolyEvalInstance {
1302 c: comm_output,
1303 x,
1304 e: product,
1305 },
1306 ));
1307
1308 // eval_output2 = output(rand_ext[1..])
1309 w_u_vec.push((
1310 PolyEvalWitness { p: poly_output },
1311 PolyEvalInstance {
1312 c: comm_output,
1313 x: rand_ext[1..].to_vec(),
1314 e: eval_output2,
1315 },
1316 ));
1317
1318 let r_prod = rand_ext[1..].to_vec();
1319 // row-related and col-related claims of polynomial evaluations to aid the final check of the sum-check
1320 let evals = [
1321 &pk.S_repr.row,
1322 &pk.S_repr.row_read_ts,
1323 &E_row,
1324 &pk.S_repr.row_audit_ts,
1325 &pk.S_repr.col,
1326 &pk.S_repr.col_read_ts,
1327 &E_col,
1328 &pk.S_repr.col_audit_ts,
1329 ]
1330 .into_par_iter()
1331 .map(|p| MultilinearPolynomial::evaluate_with(p, &r_prod))
1332 .collect::<Vec<G::Scalar>>();
1333
1334 let eval_row = evals[0];
1335 let eval_row_read_ts = evals[1];
1336 let eval_E_row_at_r_prod = evals[2];
1337 let eval_row_audit_ts = evals[3];
1338 let eval_col = evals[4];
1339 let eval_col_read_ts = evals[5];
1340 let eval_E_col_at_r_prod = evals[6];
1341 let eval_col_audit_ts = evals[7];
1342
1343 // 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..]).
1344 // r_prod was padded, so we now remove the padding
1345 let r_prod_unpad = {
1346 let l = pk.S_repr.N.log_2() - (2 * pk.S.num_vars).log_2();
1347 r_prod[l..].to_vec()
1348 };
1349
1350 let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_prod_unpad[1..]);
1351
1352 // we can batch all the claims
1353 transcript.absorb(
1354 b"e",
1355 &[
1356 eval_row,
1357 eval_row_read_ts,
1358 eval_E_row_at_r_prod,
1359 eval_row_audit_ts,
1360 eval_col,
1361 eval_col_read_ts,
1362 eval_E_col_at_r_prod,
1363 eval_col_audit_ts,
1364 eval_W, // this will not be batched below as it is evaluated at r_prod[1..]
1365 ]
1366 .as_slice(),
1367 );
1368
1369 let c = transcript.squeeze(b"c")?;
1370 let eval_vec = [
1371 eval_row,
1372 eval_row_read_ts,
1373 eval_E_row_at_r_prod,
1374 eval_row_audit_ts,
1375 eval_col,
1376 eval_col_read_ts,
1377 eval_E_col_at_r_prod,
1378 eval_col_audit_ts,
1379 ];
1380 let comm_vec = [
1381 pk.S_comm.comm_row,
1382 pk.S_comm.comm_row_read_ts,
1383 comm_E_row,
1384 pk.S_comm.comm_row_audit_ts,
1385 pk.S_comm.comm_col,
1386 pk.S_comm.comm_col_read_ts,
1387 comm_E_col,
1388 pk.S_comm.comm_col_audit_ts,
1389 ];
1390 let poly_vec = [
1391 &pk.S_repr.row,
1392 &pk.S_repr.row_read_ts,
1393 &E_row,
1394 &pk.S_repr.row_audit_ts,
1395 &pk.S_repr.col,
1396 &pk.S_repr.col_read_ts,
1397 &E_col,
1398 &pk.S_repr.col_audit_ts,
1399 ];
1400 let w = PolyEvalWitness::batch(&poly_vec, &c);
1401 let u = PolyEvalInstance::batch(&comm_vec, &r_prod, &eval_vec, &c);
1402
1403 // add the claim to prove for later
1404 w_u_vec.push((w, u));
1405
1406 w_u_vec.push((
1407 PolyEvalWitness { p: W.W },
1408 PolyEvalInstance {
1409 c: U.comm_W,
1410 x: r_prod_unpad[1..].to_vec(),
1411 e: eval_W,
1412 },
1413 ));
1414
1415 // all nine evaluations are at r_sat, we can fold them into one; they were added to the transcript earlier
1416 let eval_vec = [
1417 eval_Az, eval_Bz, eval_Cz, eval_E, eval_E_row, eval_E_col, eval_val_A, eval_val_B, eval_val_C,
1418 ];
1419 let comm_vec = [
1420 comm_Az,
1421 comm_Bz,
1422 comm_Cz,
1423 U.comm_E,
1424 comm_E_row,
1425 comm_E_col,
1426 pk.S_comm.comm_val_A,
1427 pk.S_comm.comm_val_B,
1428 pk.S_comm.comm_val_C,
1429 ];
1430 let poly_vec = [
1431 &Az,
1432 &Bz,
1433 &Cz,
1434 &E,
1435 &E_row,
1436 &E_col,
1437 &pk.S_repr.val_A,
1438 &pk.S_repr.val_B,
1439 &pk.S_repr.val_C,
1440 ];
1441 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1442 let c = transcript.squeeze(b"c")?;
1443 let w = PolyEvalWitness::batch(&poly_vec, &c);
1444 let u = PolyEvalInstance::batch(&comm_vec, &r_sat, &eval_vec, &c);
1445 w_u_vec.push((w, u));
1446
1447 // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point.
1448 // For example, eval_W =? W(r_y[1..]) and eval_W =? E(r_x) into
1449 // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz)
1450 // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz),
1451 // where gamma is a public challenge
1452 // Since commitments to W and E are homomorphic, the verifier can compute a commitment
1453 // to the batched polynomial.
1454 assert!(w_u_vec.len() >= 2);
1455
1456 let (w_vec, u_vec): (Vec<PolyEvalWitness<G>>, Vec<PolyEvalInstance<G>>) =
1457 w_u_vec.into_iter().unzip();
1458 let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size
1459 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1460
1461 // generate a challenge
1462 let rho = transcript.squeeze(b"r")?;
1463 let num_claims = w_vec_padded.len();
1464 let powers_of_rho = powers::<G>(&rho, num_claims);
1465 let claim_batch_joint = u_vec_padded
1466 .iter()
1467 .zip(powers_of_rho.iter())
1468 .map(|(u, p)| u.e * p)
1469 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1470
1471 let mut polys_left: Vec<MultilinearPolynomial<G::Scalar>> = w_vec_padded
1472 .iter()
1473 .map(|w| MultilinearPolynomial::new(w.p.clone()))
1474 .collect();
1475 let mut polys_right: Vec<MultilinearPolynomial<G::Scalar>> = u_vec_padded
1476 .iter()
1477 .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals()))
1478 .collect();
1479
1480 let num_rounds_z = u_vec_padded[0].x.len();
1481 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
1482 *poly_A_comp * *poly_B_comp
1483 };
1484 let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch(
1485 &claim_batch_joint,
1486 num_rounds_z,
1487 &mut polys_left,
1488 &mut polys_right,
1489 &powers_of_rho,
1490 comb_func,
1491 &mut transcript,
1492 )?;
1493
1494 let (claims_batch_left, _): (Vec<G::Scalar>, Vec<G::Scalar>) = claims_batch;
1495
1496 transcript.absorb(b"l", &claims_batch_left.as_slice());
1497
1498 // we now combine evaluation claims at the same point rz into one
1499 let gamma = transcript.squeeze(b"g")?;
1500 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
1501 let comm_joint = u_vec_padded
1502 .iter()
1503 .zip(powers_of_gamma.iter())
1504 .map(|(u, g_i)| u.c * *g_i)
1505 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1506 let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma);
1507 let eval_joint = claims_batch_left
1508 .iter()
1509 .zip(powers_of_gamma.iter())
1510 .map(|(e, g_i)| *e * *g_i)
1511 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1512
1513 let eval_arg = EE::prove(
1514 ck,
1515 &pk.pk_ee,
1516 &mut transcript,
1517 &comm_joint,
1518 &poly_joint.p,
1519 &r_z,
1520 &eval_joint,
1521 )?;
1522
1523 Ok(RelaxedR1CSSNARK {
1524 comm_Az: comm_Az.compress(),
1525 comm_Bz: comm_Bz.compress(),
1526 comm_Cz: comm_Cz.compress(),
1527 comm_E_row: comm_E_row.compress(),
1528 comm_E_col: comm_E_col.compress(),
1529 eval_Az_at_tau,
1530 eval_Bz_at_tau,
1531 eval_Cz_at_tau,
1532 comm_output_arr: vec_to_arr(
1533 mem_sc_inst
1534 .comm_output_vec
1535 .iter()
1536 .map(|c| c.compress())
1537 .collect::<Vec<CompressedCommitment<G>>>(),
1538 ),
1539 claims_product_arr: vec_to_arr(mem_sc_inst.claims.clone()),
1540
1541 sc_sat,
1542
1543 eval_Az,
1544 eval_Bz,
1545 eval_Cz,
1546 eval_E,
1547 eval_E_row,
1548 eval_E_col,
1549 eval_val_A,
1550 eval_val_B,
1551 eval_val_C,
1552
1553 eval_left_arr: vec_to_arr(eval_left_vec),
1554 eval_right_arr: vec_to_arr(eval_right_vec),
1555 eval_output_arr: vec_to_arr(eval_output_vec),
1556 eval_input_arr: vec_to_arr(eval_input_vec),
1557 eval_output2_arr: vec_to_arr(eval_output2_vec),
1558
1559 eval_row,
1560 eval_row_read_ts,
1561 eval_E_row_at_r_prod,
1562 eval_row_audit_ts,
1563 eval_col,
1564 eval_col_read_ts,
1565 eval_E_col_at_r_prod,
1566 eval_col_audit_ts,
1567 eval_W,
1568
1569 sc_proof_batch,
1570 evals_batch_arr: vec_to_arr(claims_batch_left),
1571 eval_arg,
1572 })
1573 }
1574
1575 /// verifies a proof of satisfiability of a RelaxedR1CS instance
1576 fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
1577 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
1578 let mut u_vec: Vec<PolyEvalInstance<G>> = Vec::new();
1579
1580 // append the verifier key (including commitment to R1CS matrices) and the RelaxedR1CSInstance to the transcript
1581 transcript.absorb(b"vk", &vk.digest);
1582 transcript.absorb(b"U", U);
1583
1584 let comm_Az = Commitment::<G>::decompress(&self.comm_Az)?;
1585 let comm_Bz = Commitment::<G>::decompress(&self.comm_Bz)?;
1586 let comm_Cz = Commitment::<G>::decompress(&self.comm_Cz)?;
1587 let comm_E_row = Commitment::<G>::decompress(&self.comm_E_row)?;
1588 let comm_E_col = Commitment::<G>::decompress(&self.comm_E_col)?;
1589
1590 transcript.absorb(b"c", &[comm_Az, comm_Bz, comm_Cz].as_slice());
1591
1592 let num_rounds_sat = vk.S_comm.N.log_2();
1593 let tau = (0..num_rounds_sat)
1594 .map(|_i| transcript.squeeze(b"t"))
1595 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1596
1597 transcript.absorb(
1598 b"e",
1599 &[
1600 self.eval_Az_at_tau,
1601 self.eval_Bz_at_tau,
1602 self.eval_Cz_at_tau,
1603 ]
1604 .as_slice(),
1605 );
1606
1607 transcript.absorb(b"e", &vec![comm_E_row, comm_E_col].as_slice());
1608
1609 // add claims about Az, Bz, and Cz to be checked later
1610 // since all the three polynomials are opened at tau,
1611 // we can combine them into a single polynomial opened at tau
1612 let eval_vec = vec![
1613 self.eval_Az_at_tau,
1614 self.eval_Bz_at_tau,
1615 self.eval_Cz_at_tau,
1616 ];
1617 let comm_vec = vec![comm_Az, comm_Bz, comm_Cz];
1618 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1619 let c = transcript.squeeze(b"c")?;
1620 let u = PolyEvalInstance::batch(&comm_vec, &tau, &eval_vec, &c);
1621 let claim_inner = u.e;
1622 let c_inner = c;
1623 u_vec.push(u);
1624
1625 let gamma_1 = transcript.squeeze(b"g1")?;
1626 let gamma_2 = transcript.squeeze(b"g2")?;
1627
1628 // hash function
1629 let gamma_1_sqr = gamma_1 * gamma_1;
1630 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
1631 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
1632 };
1633
1634 // check the required multiset relationship
1635 // row
1636 if self.claims_product_arr[0] * self.claims_product_arr[2]
1637 != self.claims_product_arr[1] * self.claims_product_arr[3]
1638 {
1639 return Err(NovaError::InvalidMultisetProof);
1640 }
1641 // col
1642 if self.claims_product_arr[4] * self.claims_product_arr[6]
1643 != self.claims_product_arr[5] * self.claims_product_arr[7]
1644 {
1645 return Err(NovaError::InvalidMultisetProof);
1646 }
1647
1648 let comm_output_vec = self
1649 .comm_output_arr
1650 .iter()
1651 .map(|c| Commitment::<G>::decompress(c))
1652 .collect::<Result<Vec<Commitment<G>>, NovaError>>()?;
1653
1654 transcript.absorb(b"o", &comm_output_vec.as_slice());
1655 transcript.absorb(b"c", &self.claims_product_arr.as_slice());
1656
1657 let num_rounds = vk.S_comm.N.log_2();
1658 let rand_eq = (0..num_rounds)
1659 .map(|_i| transcript.squeeze(b"e"))
1660 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1661
1662 let num_claims = 10;
1663 let coeffs = {
1664 let s = transcript.squeeze(b"r")?;
1665 let mut s_vec = vec![s];
1666 for i in 1..num_claims {
1667 s_vec.push(s_vec[i - 1] * s);
1668 }
1669 s_vec
1670 };
1671
1672 let claim = coeffs[9] * claim_inner; // rest are zeros
1673 let (claim_sat_final, r_sat) = self
1674 .sc_sat
1675 .verify(claim, num_rounds_sat, 3, &mut transcript)?;
1676
1677 // verify claim_sat_final
1678 let taus_bound_r_sat = EqPolynomial::new(tau.clone()).evaluate(&r_sat);
1679 let rand_eq_bound_r_sat = EqPolynomial::new(rand_eq).evaluate(&r_sat);
1680 let claim_mem_final_expected = (0..8)
1681 .map(|i| {
1682 coeffs[i]
1683 * rand_eq_bound_r_sat
1684 * (self.eval_left_arr[i] * self.eval_right_arr[i] - self.eval_output_arr[i])
1685 })
1686 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1687 let claim_outer_final_expected = coeffs[8]
1688 * taus_bound_r_sat
1689 * (self.eval_Az * self.eval_Bz - U.u * self.eval_Cz - self.eval_E);
1690 let claim_inner_final_expected = coeffs[9]
1691 * self.eval_E_row
1692 * self.eval_E_col
1693 * (self.eval_val_A + c_inner * self.eval_val_B + c_inner * c_inner * self.eval_val_C);
1694
1695 if claim_mem_final_expected + claim_outer_final_expected + claim_inner_final_expected
1696 != claim_sat_final
1697 {
1698 return Err(NovaError::InvalidSumcheckProof);
1699 }
1700
1701 // claims from the end of the sum-check
1702 let eval_vec = [
1703 self.eval_Az,
1704 self.eval_Bz,
1705 self.eval_Cz,
1706 self.eval_E,
1707 self.eval_E_row,
1708 self.eval_E_col,
1709 self.eval_val_A,
1710 self.eval_val_B,
1711 self.eval_val_C,
1712 ]
1713 .into_iter()
1714 .chain(self.eval_left_arr.into_iter())
1715 .chain(self.eval_right_arr.into_iter())
1716 .chain(self.eval_output_arr.into_iter())
1717 .collect::<Vec<G::Scalar>>();
1718
1719 transcript.absorb(b"e", &eval_vec.as_slice());
1720 // we now combine eval_left = left(rand) and eval_right = right(rand)
1721 // into claims about input and output
1722 let c = transcript.squeeze(b"c")?;
1723
1724 // eval = (G::Scalar::ONE - c) * eval_left + c * eval_right
1725 // eval is claimed evaluation of input||output(r, c), which can be proven by proving input(r[1..], c) and output(r[1..], c)
1726 let rand_ext = {
1727 let mut r = r_sat.clone();
1728 r.extend(&[c]);
1729 r
1730 };
1731
1732 // add claimed evaluations to the transcript
1733 let evals = self
1734 .eval_input_arr
1735 .into_iter()
1736 .chain(self.eval_output2_arr.into_iter())
1737 .collect::<Vec<G::Scalar>>();
1738 transcript.absorb(b"e", &evals.as_slice());
1739
1740 // squeeze a challenge to combine multiple claims into one
1741 let powers_of_rho = {
1742 let s = transcript.squeeze(b"r")?;
1743 let mut s_vec = vec![s];
1744 for i in 1..num_claims {
1745 s_vec.push(s_vec[i - 1] * s);
1746 }
1747 s_vec
1748 };
1749
1750 // take weighted sum of input, output, and their commitments
1751 let product = self
1752 .claims_product_arr
1753 .iter()
1754 .zip(powers_of_rho.iter())
1755 .map(|(e, p)| *e * p)
1756 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1757
1758 let eval_output = self
1759 .eval_output_arr
1760 .iter()
1761 .zip(powers_of_rho.iter())
1762 .map(|(e, p)| *e * p)
1763 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1764
1765 let comm_output = comm_output_vec
1766 .iter()
1767 .zip(powers_of_rho.iter())
1768 .map(|(c, r_i)| *c * *r_i)
1769 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1770
1771 let eval_output2 = self
1772 .eval_output2_arr
1773 .iter()
1774 .zip(powers_of_rho.iter())
1775 .map(|(e, p)| *e * p)
1776 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1777
1778 // eval_output = output(r_sat)
1779 u_vec.push(PolyEvalInstance {
1780 c: comm_output,
1781 x: r_sat.clone(),
1782 e: eval_output,
1783 });
1784
1785 // claimed_product = output(1, ..., 1, 0)
1786 let x = {
1787 let mut x = vec![G::Scalar::ONE; r_sat.len()];
1788 x[r_sat.len() - 1] = G::Scalar::ZERO;
1789 x
1790 };
1791 u_vec.push(PolyEvalInstance {
1792 c: comm_output,
1793 x,
1794 e: product,
1795 });
1796
1797 // eval_output2 = output(rand_ext[1..])
1798 u_vec.push(PolyEvalInstance {
1799 c: comm_output,
1800 x: rand_ext[1..].to_vec(),
1801 e: eval_output2,
1802 });
1803
1804 let r_prod = rand_ext[1..].to_vec();
1805 // row-related and col-related claims of polynomial evaluations to aid the final check of the sum-check
1806 // we can batch all the claims
1807 transcript.absorb(
1808 b"e",
1809 &[
1810 self.eval_row,
1811 self.eval_row_read_ts,
1812 self.eval_E_row_at_r_prod,
1813 self.eval_row_audit_ts,
1814 self.eval_col,
1815 self.eval_col_read_ts,
1816 self.eval_E_col_at_r_prod,
1817 self.eval_col_audit_ts,
1818 self.eval_W,
1819 ]
1820 .as_slice(),
1821 );
1822 let c = transcript.squeeze(b"c")?;
1823 let eval_vec = [
1824 self.eval_row,
1825 self.eval_row_read_ts,
1826 self.eval_E_row_at_r_prod,
1827 self.eval_row_audit_ts,
1828 self.eval_col,
1829 self.eval_col_read_ts,
1830 self.eval_E_col_at_r_prod,
1831 self.eval_col_audit_ts,
1832 ];
1833 let comm_vec = [
1834 vk.S_comm.comm_row,
1835 vk.S_comm.comm_row_read_ts,
1836 comm_E_row,
1837 vk.S_comm.comm_row_audit_ts,
1838 vk.S_comm.comm_col,
1839 vk.S_comm.comm_col_read_ts,
1840 comm_E_col,
1841 vk.S_comm.comm_col_audit_ts,
1842 ];
1843 let u = PolyEvalInstance::batch(&comm_vec, &r_prod, &eval_vec, &c);
1844
1845 // add the claim to prove for later
1846 u_vec.push(u);
1847
1848 // compute eval_Z
1849 let (eval_Z, r_prod_unpad) = {
1850 // r_prod was padded, so we now remove the padding
1851 let (factor, r_prod_unpad) = {
1852 let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2();
1853
1854 let mut factor = G::Scalar::ONE;
1855 for r_p in r_prod.iter().take(l) {
1856 factor *= G::Scalar::ONE - r_p
1857 }
1858
1859 let r_prod_unpad = {
1860 let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2();
1861 r_prod[l..].to_vec()
1862 };
1863
1864 (factor, r_prod_unpad)
1865 };
1866
1867 let eval_X = {
1868 // constant term
1869 let mut poly_X = vec![(0, U.u)];
1870 //remaining inputs
1871 poly_X.extend(
1872 (0..U.X.len())
1873 .map(|i| (i + 1, U.X[i]))
1874 .collect::<Vec<(usize, G::Scalar)>>(),
1875 );
1876 SparsePolynomial::new((vk.num_vars as f64).log2() as usize, poly_X)
1877 .evaluate(&r_prod_unpad[1..])
1878 };
1879 let eval_Z =
1880 factor * ((G::Scalar::ONE - r_prod_unpad[0]) * self.eval_W + r_prod_unpad[0] * eval_X);
1881
1882 (eval_Z, r_prod_unpad)
1883 };
1884
1885 u_vec.push(PolyEvalInstance {
1886 c: U.comm_W,
1887 x: r_prod_unpad[1..].to_vec(),
1888 e: self.eval_W,
1889 });
1890
1891 // finish the final step of the sum-check
1892 let (claim_init_expected_row, claim_audit_expected_row) = {
1893 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
1894 let val = EqPolynomial::new(tau.to_vec()).evaluate(&r_prod);
1895 (
1896 hash_func(&addr, &val, &G::Scalar::ZERO),
1897 hash_func(&addr, &val, &self.eval_row_audit_ts),
1898 )
1899 };
1900
1901 let (claim_read_expected_row, claim_write_expected_row) = {
1902 (
1903 hash_func(
1904 &self.eval_row,
1905 &self.eval_E_row_at_r_prod,
1906 &self.eval_row_read_ts,
1907 ),
1908 hash_func(
1909 &self.eval_row,
1910 &self.eval_E_row_at_r_prod,
1911 &(self.eval_row_read_ts + G::Scalar::ONE),
1912 ),
1913 )
1914 };
1915
1916 // multiset check for the row
1917 if claim_init_expected_row != self.eval_input_arr[0]
1918 || claim_read_expected_row != self.eval_input_arr[1]
1919 || claim_write_expected_row != self.eval_input_arr[2]
1920 || claim_audit_expected_row != self.eval_input_arr[3]
1921 {
1922 return Err(NovaError::InvalidSumcheckProof);
1923 }
1924
1925 let (claim_init_expected_col, claim_audit_expected_col) = {
1926 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
1927 let val = eval_Z;
1928 (
1929 hash_func(&addr, &val, &G::Scalar::ZERO),
1930 hash_func(&addr, &val, &self.eval_col_audit_ts),
1931 )
1932 };
1933
1934 let (claim_read_expected_col, claim_write_expected_col) = {
1935 (
1936 hash_func(
1937 &self.eval_col,
1938 &self.eval_E_col_at_r_prod,
1939 &self.eval_col_read_ts,
1940 ),
1941 hash_func(
1942 &self.eval_col,
1943 &self.eval_E_col_at_r_prod,
1944 &(self.eval_col_read_ts + G::Scalar::ONE),
1945 ),
1946 )
1947 };
1948
1949 // multiset check for the col
1950 if claim_init_expected_col != self.eval_input_arr[4]
1951 || claim_read_expected_col != self.eval_input_arr[5]
1952 || claim_write_expected_col != self.eval_input_arr[6]
1953 || claim_audit_expected_col != self.eval_input_arr[7]
1954 {
1955 return Err(NovaError::InvalidSumcheckProof);
1956 }
1957
1958 // since all the nine polynomials are opened at r_sat,
1959 // we can combine them into a single polynomial opened at r_sat
1960 let eval_vec = [
1961 self.eval_Az,
1962 self.eval_Bz,
1963 self.eval_Cz,
1964 self.eval_E,
1965 self.eval_E_row,
1966 self.eval_E_col,
1967 self.eval_val_A,
1968 self.eval_val_B,
1969 self.eval_val_C,
1970 ];
1971 let comm_vec = [
1972 comm_Az,
1973 comm_Bz,
1974 comm_Cz,
1975 U.comm_E,
1976 comm_E_row,
1977 comm_E_col,
1978 vk.S_comm.comm_val_A,
1979 vk.S_comm.comm_val_B,
1980 vk.S_comm.comm_val_C,
1981 ];
1982 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1983 let c = transcript.squeeze(b"c")?;
1984 let u = PolyEvalInstance::batch(&comm_vec, &r_sat, &eval_vec, &c);
1985 u_vec.push(u);
1986
1987 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1988
1989 // generate a challenge
1990 let rho = transcript.squeeze(b"r")?;
1991 let num_claims = u_vec.len();
1992 let powers_of_rho = powers::<G>(&rho, num_claims);
1993 let claim_batch_joint = u_vec_padded
1994 .iter()
1995 .zip(powers_of_rho.iter())
1996 .map(|(u, p)| u.e * p)
1997 .fold(G::Scalar::ZERO, |acc, item| acc + item);
1998
1999 let num_rounds_z = u_vec_padded[0].x.len();
2000 let (claim_batch_final, r_z) =
2001 self
2002 .sc_proof_batch
2003 .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?;
2004
2005 let claim_batch_final_expected = {
2006 let poly_rz = EqPolynomial::new(r_z.clone());
2007 let evals = u_vec_padded
2008 .iter()
2009 .map(|u| poly_rz.evaluate(&u.x))
2010 .collect::<Vec<G::Scalar>>();
2011
2012 evals
2013 .iter()
2014 .zip(self.evals_batch_arr.iter())
2015 .zip(powers_of_rho.iter())
2016 .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i)
2017 .fold(G::Scalar::ZERO, |acc, item| acc + item)
2018 };
2019
2020 if claim_batch_final != claim_batch_final_expected {
2021 return Err(NovaError::InvalidSumcheckProof);
2022 }
2023
2024 transcript.absorb(b"l", &self.evals_batch_arr.as_slice());
2025
2026 // we now combine evaluation claims at the same point rz into one
2027 let gamma = transcript.squeeze(b"g")?;
2028 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
2029 let comm_joint = u_vec_padded
2030 .iter()
2031 .zip(powers_of_gamma.iter())
2032 .map(|(u, g_i)| u.c * *g_i)
2033 .fold(Commitment::<G>::default(), |acc, item| acc + item);
2034 let eval_joint = self
2035 .evals_batch_arr
2036 .iter()
2037 .zip(powers_of_gamma.iter())
2038 .map(|(e, g_i)| *e * *g_i)
2039 .fold(G::Scalar::ZERO, |acc, item| acc + item);
2040
2041 // verify
2042 EE::verify(
2043 &vk.vk_ee,
2044 &mut transcript,
2045 &comm_joint,
2046 &r_z,
2047 &eval_joint,
2048 &self.eval_arg,
2049 )?;
2050
2051 Ok(())
2052 }
2053}
2054
2055// provides direct interfaces to call the SNARK implemented in this module
2056struct SpartanCircuit<G: Group, SC: StepCircuit<G::Scalar>> {
2057 z_i: Option<Vec<G::Scalar>>, // inputs to the circuit
2058 sc: SC, // step circuit to be executed
2059}
2060
2061impl<G: Group, SC: StepCircuit<G::Scalar>> Circuit<G::Scalar> for SpartanCircuit<G, SC> {
2062 fn synthesize<CS: ConstraintSystem<G::Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
2063 // obtain the arity information
2064 let arity = self.sc.arity();
2065
2066 // Allocate zi. If inputs.zi is not provided, allocate default value 0
2067 let zero = vec![G::Scalar::ZERO; arity];
2068 let z_i = (0..arity)
2069 .map(|i| {
2070 AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || {
2071 Ok(self.z_i.as_ref().unwrap_or(&zero)[i])
2072 })
2073 })
2074 .collect::<Result<Vec<AllocatedNum<G::Scalar>>, _>>()?;
2075
2076 let z_i_plus_one = self.sc.synthesize(&mut cs.namespace(|| "F"), &z_i)?;
2077
2078 // inputize both z_i and z_i_plus_one
2079 for (j, input) in z_i.iter().enumerate().take(arity) {
2080 let _ = input.inputize(cs.namespace(|| format!("input {j}")));
2081 }
2082 for (j, output) in z_i_plus_one.iter().enumerate().take(arity) {
2083 let _ = output.inputize(cs.namespace(|| format!("output {j}")));
2084 }
2085
2086 Ok(())
2087 }
2088}
2089
2090/// A type that holds Spartan's prover key
2091#[derive(Clone, Serialize, Deserialize)]
2092#[serde(bound = "")]
2093pub struct SpartanProverKey<G, EE>
2094where
2095 G: Group,
2096 EE: EvaluationEngineTrait<G, CE = G::CE>,
2097{
2098 S: R1CSShape<G>,
2099 ck: CommitmentKey<G>,
2100 pk: ProverKey<G, EE>,
2101}
2102
2103/// A type that holds Spartan's verifier key
2104#[derive(Clone, Serialize, Deserialize)]
2105#[serde(bound = "")]
2106pub struct SpartanVerifierKey<G, EE>
2107where
2108 G: Group,
2109 EE: EvaluationEngineTrait<G, CE = G::CE>,
2110{
2111 vk: VerifierKey<G, EE>,
2112}
2113
2114/// A direct SNARK proving a step circuit
2115#[derive(Clone, Serialize, Deserialize)]
2116#[serde(bound = "")]
2117pub struct SpartanSNARK<G, EE, C>
2118where
2119 G: Group,
2120 EE: EvaluationEngineTrait<G, CE = G::CE>,
2121 C: StepCircuit<G::Scalar>,
2122{
2123 comm_W: Commitment<G>, // commitment to the witness
2124 snark: RelaxedR1CSSNARK<G, EE>, // snark proving the witness is satisfying
2125 _p: PhantomData<C>,
2126}
2127
2128impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>, C: StepCircuit<G::Scalar>>
2129 SpartanSNARK<G, EE, C>
2130{
2131 /// Produces prover and verifier keys for Spartan
2132 pub fn setup(sc: C) -> Result<(SpartanProverKey<G, EE>, SpartanVerifierKey<G, EE>), NovaError> {
2133 // construct a circuit that can be synthesized
2134 let circuit: SpartanCircuit<G, C> = SpartanCircuit { z_i: None, sc };
2135
2136 let mut cs: ShapeCS<G> = ShapeCS::new();
2137 let _ = circuit.synthesize(&mut cs);
2138 let (S, ck) = cs.r1cs_shape();
2139
2140 let (pk, vk) = RelaxedR1CSSNARK::setup(&ck, &S)?;
2141
2142 let pk = SpartanProverKey { S, ck, pk };
2143
2144 let vk = SpartanVerifierKey { vk };
2145
2146 Ok((pk, vk))
2147 }
2148
2149 /// Produces a proof of satisfiability of the provided circuit
2150 pub fn prove(pk: &SpartanProverKey<G, EE>, sc: C, z_i: &[G::Scalar]) -> Result<Self, NovaError> {
2151 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
2152
2153 let circuit: SpartanCircuit<G, C> = SpartanCircuit {
2154 z_i: Some(z_i.to_vec()),
2155 sc,
2156 };
2157
2158 let _ = circuit.synthesize(&mut cs);
2159 let (u, w) = cs
2160 .r1cs_instance_and_witness(&pk.S, &pk.ck)
2161 .map_err(|_e| NovaError::UnSat)?;
2162
2163 // convert the instance and witness to relaxed form
2164 let (u_relaxed, w_relaxed) = (
2165 RelaxedR1CSInstance::from_r1cs_instance_unchecked(&u.comm_W, &u.X),
2166 RelaxedR1CSWitness::from_r1cs_witness(&pk.S, &w),
2167 );
2168
2169 // prove the instance using Spartan
2170 let snark = RelaxedR1CSSNARK::prove(&pk.ck, &pk.pk, &u_relaxed, &w_relaxed)?;
2171
2172 Ok(SpartanSNARK {
2173 comm_W: u.comm_W,
2174 snark,
2175 _p: Default::default(),
2176 })
2177 }
2178
2179 /// Verifies a proof of satisfiability
2180 pub fn verify(&self, vk: &SpartanVerifierKey<G, EE>, io: &[G::Scalar]) -> Result<(), NovaError> {
2181 // construct an instance using the provided commitment to the witness and z_i and z_{i+1}
2182 let u_relaxed = RelaxedR1CSInstance::from_r1cs_instance_unchecked(&self.comm_W, io);
2183
2184 // verify the snark using the constructed instance
2185 self.snark.verify(&vk.vk, &u_relaxed)?;
2186
2187 Ok(())
2188 }
2189}
2190
2191#[cfg(test)]
2192mod tests {
2193 use super::*;
2194 use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
2195 use core::marker::PhantomData;
2196 use ff::PrimeField;
2197
2198 #[derive(Clone, Debug, Default)]
2199 struct CubicCircuit<F: PrimeField> {
2200 _p: PhantomData<F>,
2201 }
2202
2203 impl<F> StepCircuit<F> for CubicCircuit<F>
2204 where
2205 F: PrimeField,
2206 {
2207 fn arity(&self) -> usize {
2208 1
2209 }
2210
2211 fn synthesize<CS: ConstraintSystem<F>>(
2212 &self,
2213 cs: &mut CS,
2214 z: &[AllocatedNum<F>],
2215 ) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
2216 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
2217 let x = &z[0];
2218 let x_sq = x.square(cs.namespace(|| "x_sq"))?;
2219 let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), x)?;
2220 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
2221 Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
2222 })?;
2223
2224 cs.enforce(
2225 || "y = x^3 + x + 5",
2226 |lc| {
2227 lc + x_cu.get_variable()
2228 + x.get_variable()
2229 + CS::one()
2230 + CS::one()
2231 + CS::one()
2232 + CS::one()
2233 + CS::one()
2234 },
2235 |lc| lc + CS::one(),
2236 |lc| lc + y.get_variable(),
2237 );
2238
2239 Ok(vec![y])
2240 }
2241
2242 fn output(&self, z: &[F]) -> Vec<F> {
2243 vec![z[0] * z[0] * z[0] + z[0] + F::from(5u64)]
2244 }
2245 }
2246
2247 #[test]
2248 fn test_spartan_snark() {
2249 type G = pasta_curves::pallas::Point;
2250 type EE = crate::provider::ipa_pc::EvaluationEngine<G>;
2251
2252 test_spartan_snark_with::<G, EE>();
2253 }
2254
2255 fn test_spartan_snark_with<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>>() {
2256 let circuit = CubicCircuit::default();
2257
2258 // produce keys
2259 let (pk, vk) =
2260 SpartanSNARK::<G, EE, CubicCircuit<<G as Group>::Scalar>>::setup(circuit.clone()).unwrap();
2261
2262 let num_steps = 3;
2263
2264 // setup inputs
2265 let z0 = vec![<G as Group>::Scalar::ZERO];
2266 let mut z_i = z0;
2267
2268 for _i in 0..num_steps {
2269 // produce a SNARK
2270 let res = SpartanSNARK::prove(&pk, circuit.clone(), &z_i);
2271 assert!(res.is_ok());
2272
2273 let z_i_plus_one = circuit.output(&z_i);
2274
2275 let snark = res.unwrap();
2276
2277 // verify the SNARK
2278 let io = z_i
2279 .clone()
2280 .into_iter()
2281 .chain(z_i_plus_one.clone().into_iter())
2282 .collect::<Vec<_>>();
2283 let res = snark.verify(&vk, &io);
2284 assert!(res.is_ok());
2285
2286 // set input to the next step
2287 z_i = z_i_plus_one.clone();
2288 }
2289
2290 // sanity: check the claimed output with a direct computation of the same
2291 assert_eq!(z_i, vec![<G as Group>::Scalar::from(2460515u64)]);
2292 }
2293}