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 .sum();
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()).map(|i| evals[i][0] * coeffs[i]).sum();
880 let evals_combined_2 = (0..evals.len()).map(|i| evals[i][1] * coeffs[i]).sum();
881 let evals_combined_3 = (0..evals.len()).map(|i| evals[i][2] * coeffs[i]).sum();
882
883 let evals = vec![
884 evals_combined_0,
885 e - evals_combined_0,
886 evals_combined_2,
887 evals_combined_3,
888 ];
889 let poly = UniPoly::from_evals(&evals);
890
891 // append the prover's message to the transcript
892 transcript.absorb(b"p", &poly);
893
894 // derive the verifier's challenge for the next round
895 let r_i = transcript.squeeze(b"c")?;
896 r.push(r_i);
897
898 mem.bound(&r_i);
899 outer.bound(&r_i);
900 inner.bound(&r_i);
901
902 e = poly.evaluate(&r_i);
903 cubic_polys.push(poly.compress());
904 }
905
906 let mem_claims = mem.final_claims();
907 let outer_claims = outer.final_claims();
908 let inner_claims = inner.final_claims();
909
910 Ok((
911 SumcheckProof::new(cubic_polys),
912 r,
913 mem_claims,
914 outer_claims,
915 inner_claims,
916 ))
917 }
918}
919
920impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>> RelaxedR1CSSNARKTrait<G>
921 for RelaxedR1CSSNARK<G, EE>
922{
923 type ProverKey = ProverKey<G, EE>;
924 type VerifierKey = VerifierKey<G, EE>;
925
926 fn setup(
927 ck: &CommitmentKey<G>,
928 S: &R1CSShape<G>,
929 ) -> Result<(Self::ProverKey, Self::VerifierKey), NovaError> {
930 let (pk_ee, vk_ee) = EE::setup(ck);
931
932 // pad the R1CS matrices
933 let S = S.pad();
934
935 let S_repr = R1CSShapeSparkRepr::new(&S);
936 let S_comm = S_repr.commit(ck);
937
938 let vk = {
939 let mut vk = VerifierKey {
940 num_cons: S.num_cons,
941 num_vars: S.num_vars,
942 S_comm: S_comm.clone(),
943 vk_ee,
944 digest: G::Scalar::ZERO,
945 };
946 vk.digest = compute_digest::<G, VerifierKey<G, EE>>(&vk);
947 vk
948 };
949
950 let pk = ProverKey {
951 pk_ee,
952 S,
953 S_repr,
954 S_comm,
955 vk_digest: vk.digest,
956 };
957
958 Ok((pk, vk))
959 }
960
961 /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
962 fn prove(
963 ck: &CommitmentKey<G>,
964 pk: &Self::ProverKey,
965 U: &RelaxedR1CSInstance<G>,
966 W: &RelaxedR1CSWitness<G>,
967 ) -> Result<Self, NovaError> {
968 let W = W.pad(&pk.S); // pad the witness
969 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
970
971 // a list of polynomial evaluation claims that will be batched
972 let mut w_u_vec = Vec::new();
973
974 // sanity check that R1CSShape has certain size characteristics
975 assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
976 assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
977 assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
978 assert!(pk.S.num_io < pk.S.num_vars);
979
980 // append the verifier key (which includes commitment to R1CS matrices) and the RelaxedR1CSInstance to the transcript
981 transcript.absorb(b"vk", &pk.vk_digest);
982 transcript.absorb(b"U", U);
983
984 // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
985 let z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
986
987 // compute Az, Bz, Cz
988 let (mut Az, mut Bz, mut Cz) = pk.S.multiply_vec(&z)?;
989
990 // commit to Az, Bz, Cz
991 let (comm_Az, (comm_Bz, comm_Cz)) = rayon::join(
992 || G::CE::commit(ck, &Az),
993 || rayon::join(|| G::CE::commit(ck, &Bz), || G::CE::commit(ck, &Cz)),
994 );
995
996 transcript.absorb(b"c", &[comm_Az, comm_Bz, comm_Cz].as_slice());
997
998 // number of rounds of the satisfiability sum-check
999 let num_rounds_sat = pk.S_repr.N.log_2();
1000 let tau = (0..num_rounds_sat)
1001 .map(|_| transcript.squeeze(b"t"))
1002 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1003
1004 // (1) send commitments to Az, Bz, and Cz along with their evaluations at tau
1005 let (Az, Bz, Cz, E) = {
1006 Az.resize(pk.S_repr.N, G::Scalar::ZERO);
1007 Bz.resize(pk.S_repr.N, G::Scalar::ZERO);
1008 Cz.resize(pk.S_repr.N, G::Scalar::ZERO);
1009
1010 let mut E = W.E.clone();
1011 E.resize(pk.S_repr.N, G::Scalar::ZERO);
1012
1013 (Az, Bz, Cz, E)
1014 };
1015 let (eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau) = {
1016 let evals_at_tau = [&Az, &Bz, &Cz]
1017 .into_par_iter()
1018 .map(|p| MultilinearPolynomial::evaluate_with(p, &tau))
1019 .collect::<Vec<G::Scalar>>();
1020 (evals_at_tau[0], evals_at_tau[1], evals_at_tau[2])
1021 };
1022
1023 // (2) send commitments to the following two oracles
1024 // E_row(i) = eq(tau, row(i)) for all i
1025 // E_col(i) = z(col(i)) for all i
1026 let (mem_row, mem_col, E_row, E_col) = pk.S_repr.evaluation_oracles(&pk.S, &tau, &z);
1027 let (comm_E_row, comm_E_col) =
1028 rayon::join(|| G::CE::commit(ck, &E_row), || G::CE::commit(ck, &E_col));
1029
1030 // absorb the claimed evaluations into the transcript
1031 transcript.absorb(
1032 b"e",
1033 &[eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau].as_slice(),
1034 );
1035 // absorb commitments to E_row and E_col in the transcript
1036 transcript.absorb(b"e", &vec![comm_E_row, comm_E_col].as_slice());
1037
1038 // add claims about Az, Bz, and Cz to be checked later
1039 // since all the three polynomials are opened at tau,
1040 // we can combine them into a single polynomial opened at tau
1041 let eval_vec = vec![eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau];
1042 let comm_vec = vec![comm_Az, comm_Bz, comm_Cz];
1043 let poly_vec = vec![&Az, &Bz, &Cz];
1044 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1045 let c = transcript.squeeze(b"c")?;
1046 let w = PolyEvalWitness::batch(&poly_vec, &c);
1047 let u = PolyEvalInstance::batch(&comm_vec, &tau, &eval_vec, &c);
1048 w_u_vec.push((w, u));
1049
1050 let c_inner = c;
1051
1052 // we now need to prove three claims
1053 // (1) 0 = \sum_x poly_tau(x) * (poly_Az(x) * poly_Bz(x) - poly_uCz_E(x))
1054 // (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)
1055 // (3) E_row(i) = eq(tau, row(i)) and E_col(i) = z(col(i))
1056
1057 // a sum-check instance to prove the first claim
1058 let mut outer_sc_inst = OuterSumcheckInstance {
1059 poly_tau: MultilinearPolynomial::new(EqPolynomial::new(tau).evals()),
1060 poly_Az: MultilinearPolynomial::new(Az.clone()),
1061 poly_Bz: MultilinearPolynomial::new(Bz.clone()),
1062 poly_uCz_E: {
1063 let uCz_E = (0..Cz.len())
1064 .map(|i| U.u * Cz[i] + E[i])
1065 .collect::<Vec<G::Scalar>>();
1066 MultilinearPolynomial::new(uCz_E)
1067 },
1068 };
1069
1070 // a sum-check instance to prove the second claim
1071 let val = pk
1072 .S_repr
1073 .val_A
1074 .iter()
1075 .zip(pk.S_repr.val_B.iter())
1076 .zip(pk.S_repr.val_C.iter())
1077 .map(|((v_a, v_b), v_c)| *v_a + c_inner * *v_b + c_inner * c_inner * *v_c)
1078 .collect::<Vec<G::Scalar>>();
1079 let mut inner_sc_inst = InnerSumcheckInstance {
1080 claim: eval_Az_at_tau + c_inner * eval_Bz_at_tau + c_inner * c_inner * eval_Cz_at_tau,
1081 poly_E_row: MultilinearPolynomial::new(E_row.clone()),
1082 poly_E_col: MultilinearPolynomial::new(E_col.clone()),
1083 poly_val: MultilinearPolynomial::new(val),
1084 };
1085
1086 // a third sum-check instance to prove the memory-related claim
1087 // we now need to prove that E_row and E_col are well-formed
1088 // we use memory checking: H(INIT) * H(WS) =? H(RS) * H(FINAL)
1089 let gamma_1 = transcript.squeeze(b"g1")?;
1090 let gamma_2 = transcript.squeeze(b"g2")?;
1091
1092 let gamma_1_sqr = gamma_1 * gamma_1;
1093 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
1094 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
1095 };
1096
1097 let init_row = (0..mem_row.len())
1098 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_row[i], &G::Scalar::ZERO))
1099 .collect::<Vec<G::Scalar>>();
1100 let read_row = (0..E_row.len())
1101 .map(|i| hash_func(&pk.S_repr.row[i], &E_row[i], &pk.S_repr.row_read_ts[i]))
1102 .collect::<Vec<G::Scalar>>();
1103 let write_row = (0..E_row.len())
1104 .map(|i| {
1105 hash_func(
1106 &pk.S_repr.row[i],
1107 &E_row[i],
1108 &(pk.S_repr.row_read_ts[i] + G::Scalar::ONE),
1109 )
1110 })
1111 .collect::<Vec<G::Scalar>>();
1112 let audit_row = (0..mem_row.len())
1113 .map(|i| {
1114 hash_func(
1115 &G::Scalar::from(i as u64),
1116 &mem_row[i],
1117 &pk.S_repr.row_audit_ts[i],
1118 )
1119 })
1120 .collect::<Vec<G::Scalar>>();
1121
1122 let init_col = (0..mem_col.len())
1123 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_col[i], &G::Scalar::ZERO))
1124 .collect::<Vec<G::Scalar>>();
1125 let read_col = (0..E_col.len())
1126 .map(|i| hash_func(&pk.S_repr.col[i], &E_col[i], &pk.S_repr.col_read_ts[i]))
1127 .collect::<Vec<G::Scalar>>();
1128 let write_col = (0..E_col.len())
1129 .map(|i| {
1130 hash_func(
1131 &pk.S_repr.col[i],
1132 &E_col[i],
1133 &(pk.S_repr.col_read_ts[i] + G::Scalar::ONE),
1134 )
1135 })
1136 .collect::<Vec<G::Scalar>>();
1137 let audit_col = (0..mem_col.len())
1138 .map(|i| {
1139 hash_func(
1140 &G::Scalar::from(i as u64),
1141 &mem_col[i],
1142 &pk.S_repr.col_audit_ts[i],
1143 )
1144 })
1145 .collect::<Vec<G::Scalar>>();
1146
1147 let mut mem_sc_inst = ProductSumcheckInstance::new(
1148 ck,
1149 vec![
1150 init_row, read_row, write_row, audit_row, init_col, read_col, write_col, audit_col,
1151 ],
1152 &mut transcript,
1153 )?;
1154
1155 let (sc_sat, r_sat, claims_mem, claims_outer, claims_inner) = Self::prove_inner(
1156 &mut mem_sc_inst,
1157 &mut outer_sc_inst,
1158 &mut inner_sc_inst,
1159 &mut transcript,
1160 )?;
1161
1162 // claims[0] is about the Eq polynomial, which the verifier computes directly
1163 // claims[1] =? weighed sum of left(rand)
1164 // claims[2] =? weighted sum of right(rand)
1165 // claims[3] =? weighted sum of output(rand), which is easy to verify by querying output
1166 // we also need to prove that output(output.len()-2) = claimed_product
1167 let eval_left_vec = claims_mem[1].clone();
1168 let eval_right_vec = claims_mem[2].clone();
1169 let eval_output_vec = claims_mem[3].clone();
1170
1171 // claims from the end of sum-check
1172 let (eval_Az, eval_Bz): (G::Scalar, G::Scalar) = (claims_outer[0][1], claims_outer[0][2]);
1173 let eval_Cz = MultilinearPolynomial::evaluate_with(&Cz, &r_sat);
1174 let eval_E = MultilinearPolynomial::evaluate_with(&E, &r_sat);
1175 let eval_E_row = claims_inner[0][0];
1176 let eval_E_col = claims_inner[0][1];
1177 let eval_val_A = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_A, &r_sat);
1178 let eval_val_B = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_B, &r_sat);
1179 let eval_val_C = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_C, &r_sat);
1180 let eval_vec = vec![
1181 eval_Az, eval_Bz, eval_Cz, eval_E, eval_E_row, eval_E_col, eval_val_A, eval_val_B, eval_val_C,
1182 ]
1183 .into_iter()
1184 .chain(eval_left_vec.clone().into_iter())
1185 .chain(eval_right_vec.clone().into_iter())
1186 .chain(eval_output_vec.clone().into_iter())
1187 .collect::<Vec<G::Scalar>>();
1188
1189 // absorb all the claimed evaluations
1190 transcript.absorb(b"e", &eval_vec.as_slice());
1191
1192 // we now combine eval_left = left(rand) and eval_right = right(rand)
1193 // into claims about input and output
1194 let c = transcript.squeeze(b"c")?;
1195
1196 // eval = (G::Scalar::ONE - c) * eval_left + c * eval_right
1197 // eval is claimed evaluation of input||output(r, c), which can be proven by proving input(r[1..], c) and output(r[1..], c)
1198 let rand_ext = {
1199 let mut r = r_sat.clone();
1200 r.extend(&[c]);
1201 r
1202 };
1203 let eval_input_vec = mem_sc_inst
1204 .input_vec
1205 .iter()
1206 .map(|i| MultilinearPolynomial::evaluate_with(i, &rand_ext[1..]))
1207 .collect::<Vec<G::Scalar>>();
1208
1209 let eval_output2_vec = mem_sc_inst
1210 .output_vec
1211 .iter()
1212 .map(|o| MultilinearPolynomial::evaluate_with(o, &rand_ext[1..]))
1213 .collect::<Vec<G::Scalar>>();
1214
1215 // add claimed evaluations to the transcript
1216 let evals = eval_input_vec
1217 .clone()
1218 .into_iter()
1219 .chain(eval_output2_vec.clone().into_iter())
1220 .collect::<Vec<G::Scalar>>();
1221 transcript.absorb(b"e", &evals.as_slice());
1222
1223 // squeeze a challenge to combine multiple claims into one
1224 let powers_of_rho = {
1225 let s = transcript.squeeze(b"r")?;
1226 let mut s_vec = vec![s];
1227 for i in 1..mem_sc_inst.initial_claims().len() {
1228 s_vec.push(s_vec[i - 1] * s);
1229 }
1230 s_vec
1231 };
1232
1233 // take weighted sum of input, output, and their commitments
1234 let product = mem_sc_inst
1235 .claims
1236 .iter()
1237 .zip(powers_of_rho.iter())
1238 .map(|(e, p)| *e * p)
1239 .sum();
1240
1241 let eval_output = eval_output_vec
1242 .iter()
1243 .zip(powers_of_rho.iter())
1244 .map(|(e, p)| *e * p)
1245 .sum();
1246
1247 let comm_output = mem_sc_inst
1248 .comm_output_vec
1249 .iter()
1250 .zip(powers_of_rho.iter())
1251 .map(|(c, r_i)| *c * *r_i)
1252 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1253
1254 let weighted_sum = |W: &[Vec<G::Scalar>], s: &[G::Scalar]| -> Vec<G::Scalar> {
1255 assert_eq!(W.len(), s.len());
1256 let mut p = vec![G::Scalar::ZERO; W[0].len()];
1257 for i in 0..W.len() {
1258 for (j, item) in W[i].iter().enumerate().take(W[i].len()) {
1259 p[j] += *item * s[i]
1260 }
1261 }
1262 p
1263 };
1264
1265 let poly_output = weighted_sum(&mem_sc_inst.output_vec, &powers_of_rho);
1266
1267 let eval_output2 = eval_output2_vec
1268 .iter()
1269 .zip(powers_of_rho.iter())
1270 .map(|(e, p)| *e * p)
1271 .sum();
1272
1273 // eval_output = output(r_sat)
1274 w_u_vec.push((
1275 PolyEvalWitness {
1276 p: poly_output.clone(),
1277 },
1278 PolyEvalInstance {
1279 c: comm_output,
1280 x: r_sat.clone(),
1281 e: eval_output,
1282 },
1283 ));
1284
1285 // claimed_product = output(1, ..., 1, 0)
1286 let x = {
1287 let mut x = vec![G::Scalar::ONE; r_sat.len()];
1288 x[r_sat.len() - 1] = G::Scalar::ZERO;
1289 x
1290 };
1291 w_u_vec.push((
1292 PolyEvalWitness {
1293 p: poly_output.clone(),
1294 },
1295 PolyEvalInstance {
1296 c: comm_output,
1297 x,
1298 e: product,
1299 },
1300 ));
1301
1302 // eval_output2 = output(rand_ext[1..])
1303 w_u_vec.push((
1304 PolyEvalWitness { p: poly_output },
1305 PolyEvalInstance {
1306 c: comm_output,
1307 x: rand_ext[1..].to_vec(),
1308 e: eval_output2,
1309 },
1310 ));
1311
1312 let r_prod = rand_ext[1..].to_vec();
1313 // row-related and col-related claims of polynomial evaluations to aid the final check of the sum-check
1314 let evals = [
1315 &pk.S_repr.row,
1316 &pk.S_repr.row_read_ts,
1317 &E_row,
1318 &pk.S_repr.row_audit_ts,
1319 &pk.S_repr.col,
1320 &pk.S_repr.col_read_ts,
1321 &E_col,
1322 &pk.S_repr.col_audit_ts,
1323 ]
1324 .into_par_iter()
1325 .map(|p| MultilinearPolynomial::evaluate_with(p, &r_prod))
1326 .collect::<Vec<G::Scalar>>();
1327
1328 let eval_row = evals[0];
1329 let eval_row_read_ts = evals[1];
1330 let eval_E_row_at_r_prod = evals[2];
1331 let eval_row_audit_ts = evals[3];
1332 let eval_col = evals[4];
1333 let eval_col_read_ts = evals[5];
1334 let eval_E_col_at_r_prod = evals[6];
1335 let eval_col_audit_ts = evals[7];
1336
1337 // 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..]).
1338 // r_prod was padded, so we now remove the padding
1339 let r_prod_unpad = {
1340 let l = pk.S_repr.N.log_2() - (2 * pk.S.num_vars).log_2();
1341 r_prod[l..].to_vec()
1342 };
1343
1344 let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_prod_unpad[1..]);
1345
1346 // we can batch all the claims
1347 transcript.absorb(
1348 b"e",
1349 &[
1350 eval_row,
1351 eval_row_read_ts,
1352 eval_E_row_at_r_prod,
1353 eval_row_audit_ts,
1354 eval_col,
1355 eval_col_read_ts,
1356 eval_E_col_at_r_prod,
1357 eval_col_audit_ts,
1358 eval_W, // this will not be batched below as it is evaluated at r_prod[1..]
1359 ]
1360 .as_slice(),
1361 );
1362
1363 let c = transcript.squeeze(b"c")?;
1364 let eval_vec = [
1365 eval_row,
1366 eval_row_read_ts,
1367 eval_E_row_at_r_prod,
1368 eval_row_audit_ts,
1369 eval_col,
1370 eval_col_read_ts,
1371 eval_E_col_at_r_prod,
1372 eval_col_audit_ts,
1373 ];
1374 let comm_vec = [
1375 pk.S_comm.comm_row,
1376 pk.S_comm.comm_row_read_ts,
1377 comm_E_row,
1378 pk.S_comm.comm_row_audit_ts,
1379 pk.S_comm.comm_col,
1380 pk.S_comm.comm_col_read_ts,
1381 comm_E_col,
1382 pk.S_comm.comm_col_audit_ts,
1383 ];
1384 let poly_vec = [
1385 &pk.S_repr.row,
1386 &pk.S_repr.row_read_ts,
1387 &E_row,
1388 &pk.S_repr.row_audit_ts,
1389 &pk.S_repr.col,
1390 &pk.S_repr.col_read_ts,
1391 &E_col,
1392 &pk.S_repr.col_audit_ts,
1393 ];
1394 let w = PolyEvalWitness::batch(&poly_vec, &c);
1395 let u = PolyEvalInstance::batch(&comm_vec, &r_prod, &eval_vec, &c);
1396
1397 // add the claim to prove for later
1398 w_u_vec.push((w, u));
1399
1400 w_u_vec.push((
1401 PolyEvalWitness { p: W.W },
1402 PolyEvalInstance {
1403 c: U.comm_W,
1404 x: r_prod_unpad[1..].to_vec(),
1405 e: eval_W,
1406 },
1407 ));
1408
1409 // all nine evaluations are at r_sat, we can fold them into one; they were added to the transcript earlier
1410 let eval_vec = [
1411 eval_Az, eval_Bz, eval_Cz, eval_E, eval_E_row, eval_E_col, eval_val_A, eval_val_B, eval_val_C,
1412 ];
1413 let comm_vec = [
1414 comm_Az,
1415 comm_Bz,
1416 comm_Cz,
1417 U.comm_E,
1418 comm_E_row,
1419 comm_E_col,
1420 pk.S_comm.comm_val_A,
1421 pk.S_comm.comm_val_B,
1422 pk.S_comm.comm_val_C,
1423 ];
1424 let poly_vec = [
1425 &Az,
1426 &Bz,
1427 &Cz,
1428 &E,
1429 &E_row,
1430 &E_col,
1431 &pk.S_repr.val_A,
1432 &pk.S_repr.val_B,
1433 &pk.S_repr.val_C,
1434 ];
1435 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1436 let c = transcript.squeeze(b"c")?;
1437 let w = PolyEvalWitness::batch(&poly_vec, &c);
1438 let u = PolyEvalInstance::batch(&comm_vec, &r_sat, &eval_vec, &c);
1439 w_u_vec.push((w, u));
1440
1441 // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point.
1442 // For example, eval_W =? W(r_y[1..]) and eval_W =? E(r_x) into
1443 // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz)
1444 // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz),
1445 // where gamma is a public challenge
1446 // Since commitments to W and E are homomorphic, the verifier can compute a commitment
1447 // to the batched polynomial.
1448 assert!(w_u_vec.len() >= 2);
1449
1450 let (w_vec, u_vec): (Vec<PolyEvalWitness<G>>, Vec<PolyEvalInstance<G>>) =
1451 w_u_vec.into_iter().unzip();
1452 let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size
1453 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1454
1455 // generate a challenge
1456 let rho = transcript.squeeze(b"r")?;
1457 let num_claims = w_vec_padded.len();
1458 let powers_of_rho = powers::<G>(&rho, num_claims);
1459 let claim_batch_joint = u_vec_padded
1460 .iter()
1461 .zip(powers_of_rho.iter())
1462 .map(|(u, p)| u.e * p)
1463 .sum();
1464
1465 let mut polys_left: Vec<MultilinearPolynomial<G::Scalar>> = w_vec_padded
1466 .iter()
1467 .map(|w| MultilinearPolynomial::new(w.p.clone()))
1468 .collect();
1469 let mut polys_right: Vec<MultilinearPolynomial<G::Scalar>> = u_vec_padded
1470 .iter()
1471 .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals()))
1472 .collect();
1473
1474 let num_rounds_z = u_vec_padded[0].x.len();
1475 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
1476 *poly_A_comp * *poly_B_comp
1477 };
1478 let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch(
1479 &claim_batch_joint,
1480 num_rounds_z,
1481 &mut polys_left,
1482 &mut polys_right,
1483 &powers_of_rho,
1484 comb_func,
1485 &mut transcript,
1486 )?;
1487
1488 let (claims_batch_left, _): (Vec<G::Scalar>, Vec<G::Scalar>) = claims_batch;
1489
1490 transcript.absorb(b"l", &claims_batch_left.as_slice());
1491
1492 // we now combine evaluation claims at the same point rz into one
1493 let gamma = transcript.squeeze(b"g")?;
1494 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
1495 let comm_joint = u_vec_padded
1496 .iter()
1497 .zip(powers_of_gamma.iter())
1498 .map(|(u, g_i)| u.c * *g_i)
1499 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1500 let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma);
1501 let eval_joint = claims_batch_left
1502 .iter()
1503 .zip(powers_of_gamma.iter())
1504 .map(|(e, g_i)| *e * *g_i)
1505 .sum();
1506
1507 let eval_arg = EE::prove(
1508 ck,
1509 &pk.pk_ee,
1510 &mut transcript,
1511 &comm_joint,
1512 &poly_joint.p,
1513 &r_z,
1514 &eval_joint,
1515 )?;
1516
1517 Ok(RelaxedR1CSSNARK {
1518 comm_Az: comm_Az.compress(),
1519 comm_Bz: comm_Bz.compress(),
1520 comm_Cz: comm_Cz.compress(),
1521 comm_E_row: comm_E_row.compress(),
1522 comm_E_col: comm_E_col.compress(),
1523 eval_Az_at_tau,
1524 eval_Bz_at_tau,
1525 eval_Cz_at_tau,
1526 comm_output_arr: vec_to_arr(
1527 mem_sc_inst
1528 .comm_output_vec
1529 .iter()
1530 .map(|c| c.compress())
1531 .collect::<Vec<CompressedCommitment<G>>>(),
1532 ),
1533 claims_product_arr: vec_to_arr(mem_sc_inst.claims.clone()),
1534
1535 sc_sat,
1536
1537 eval_Az,
1538 eval_Bz,
1539 eval_Cz,
1540 eval_E,
1541 eval_E_row,
1542 eval_E_col,
1543 eval_val_A,
1544 eval_val_B,
1545 eval_val_C,
1546
1547 eval_left_arr: vec_to_arr(eval_left_vec),
1548 eval_right_arr: vec_to_arr(eval_right_vec),
1549 eval_output_arr: vec_to_arr(eval_output_vec),
1550 eval_input_arr: vec_to_arr(eval_input_vec),
1551 eval_output2_arr: vec_to_arr(eval_output2_vec),
1552
1553 eval_row,
1554 eval_row_read_ts,
1555 eval_E_row_at_r_prod,
1556 eval_row_audit_ts,
1557 eval_col,
1558 eval_col_read_ts,
1559 eval_E_col_at_r_prod,
1560 eval_col_audit_ts,
1561 eval_W,
1562
1563 sc_proof_batch,
1564 evals_batch_arr: vec_to_arr(claims_batch_left),
1565 eval_arg,
1566 })
1567 }
1568
1569 /// verifies a proof of satisfiability of a RelaxedR1CS instance
1570 fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
1571 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
1572 let mut u_vec: Vec<PolyEvalInstance<G>> = Vec::new();
1573
1574 // append the verifier key (including commitment to R1CS matrices) and the RelaxedR1CSInstance to the transcript
1575 transcript.absorb(b"vk", &vk.digest);
1576 transcript.absorb(b"U", U);
1577
1578 let comm_Az = Commitment::<G>::decompress(&self.comm_Az)?;
1579 let comm_Bz = Commitment::<G>::decompress(&self.comm_Bz)?;
1580 let comm_Cz = Commitment::<G>::decompress(&self.comm_Cz)?;
1581 let comm_E_row = Commitment::<G>::decompress(&self.comm_E_row)?;
1582 let comm_E_col = Commitment::<G>::decompress(&self.comm_E_col)?;
1583
1584 transcript.absorb(b"c", &[comm_Az, comm_Bz, comm_Cz].as_slice());
1585
1586 let num_rounds_sat = vk.S_comm.N.log_2();
1587 let tau = (0..num_rounds_sat)
1588 .map(|_i| transcript.squeeze(b"t"))
1589 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1590
1591 transcript.absorb(
1592 b"e",
1593 &[
1594 self.eval_Az_at_tau,
1595 self.eval_Bz_at_tau,
1596 self.eval_Cz_at_tau,
1597 ]
1598 .as_slice(),
1599 );
1600
1601 transcript.absorb(b"e", &vec![comm_E_row, comm_E_col].as_slice());
1602
1603 // add claims about Az, Bz, and Cz to be checked later
1604 // since all the three polynomials are opened at tau,
1605 // we can combine them into a single polynomial opened at tau
1606 let eval_vec = vec![
1607 self.eval_Az_at_tau,
1608 self.eval_Bz_at_tau,
1609 self.eval_Cz_at_tau,
1610 ];
1611 let comm_vec = vec![comm_Az, comm_Bz, comm_Cz];
1612 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1613 let c = transcript.squeeze(b"c")?;
1614 let u = PolyEvalInstance::batch(&comm_vec, &tau, &eval_vec, &c);
1615 let claim_inner = u.e;
1616 let c_inner = c;
1617 u_vec.push(u);
1618
1619 let gamma_1 = transcript.squeeze(b"g1")?;
1620 let gamma_2 = transcript.squeeze(b"g2")?;
1621
1622 // hash function
1623 let gamma_1_sqr = gamma_1 * gamma_1;
1624 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
1625 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
1626 };
1627
1628 // check the required multiset relationship
1629 // row
1630 if self.claims_product_arr[0] * self.claims_product_arr[2]
1631 != self.claims_product_arr[1] * self.claims_product_arr[3]
1632 {
1633 return Err(NovaError::InvalidMultisetProof);
1634 }
1635 // col
1636 if self.claims_product_arr[4] * self.claims_product_arr[6]
1637 != self.claims_product_arr[5] * self.claims_product_arr[7]
1638 {
1639 return Err(NovaError::InvalidMultisetProof);
1640 }
1641
1642 let comm_output_vec = self
1643 .comm_output_arr
1644 .iter()
1645 .map(|c| Commitment::<G>::decompress(c))
1646 .collect::<Result<Vec<Commitment<G>>, NovaError>>()?;
1647
1648 transcript.absorb(b"o", &comm_output_vec.as_slice());
1649 transcript.absorb(b"c", &self.claims_product_arr.as_slice());
1650
1651 let num_rounds = vk.S_comm.N.log_2();
1652 let rand_eq = (0..num_rounds)
1653 .map(|_i| transcript.squeeze(b"e"))
1654 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1655
1656 let num_claims = 10;
1657 let coeffs = {
1658 let s = transcript.squeeze(b"r")?;
1659 let mut s_vec = vec![s];
1660 for i in 1..num_claims {
1661 s_vec.push(s_vec[i - 1] * s);
1662 }
1663 s_vec
1664 };
1665
1666 let claim = coeffs[9] * claim_inner; // rest are zeros
1667 let (claim_sat_final, r_sat) = self
1668 .sc_sat
1669 .verify(claim, num_rounds_sat, 3, &mut transcript)?;
1670
1671 // verify claim_sat_final
1672 let taus_bound_r_sat = EqPolynomial::new(tau.clone()).evaluate(&r_sat);
1673 let rand_eq_bound_r_sat = EqPolynomial::new(rand_eq).evaluate(&r_sat);
1674 let claim_mem_final_expected: G::Scalar = (0..8)
1675 .map(|i| {
1676 coeffs[i]
1677 * rand_eq_bound_r_sat
1678 * (self.eval_left_arr[i] * self.eval_right_arr[i] - self.eval_output_arr[i])
1679 })
1680 .sum();
1681 let claim_outer_final_expected = coeffs[8]
1682 * taus_bound_r_sat
1683 * (self.eval_Az * self.eval_Bz - U.u * self.eval_Cz - self.eval_E);
1684 let claim_inner_final_expected = coeffs[9]
1685 * self.eval_E_row
1686 * self.eval_E_col
1687 * (self.eval_val_A + c_inner * self.eval_val_B + c_inner * c_inner * self.eval_val_C);
1688
1689 if claim_mem_final_expected + claim_outer_final_expected + claim_inner_final_expected
1690 != claim_sat_final
1691 {
1692 return Err(NovaError::InvalidSumcheckProof);
1693 }
1694
1695 // claims from the end of the sum-check
1696 let eval_vec = [
1697 self.eval_Az,
1698 self.eval_Bz,
1699 self.eval_Cz,
1700 self.eval_E,
1701 self.eval_E_row,
1702 self.eval_E_col,
1703 self.eval_val_A,
1704 self.eval_val_B,
1705 self.eval_val_C,
1706 ]
1707 .into_iter()
1708 .chain(self.eval_left_arr.into_iter())
1709 .chain(self.eval_right_arr.into_iter())
1710 .chain(self.eval_output_arr.into_iter())
1711 .collect::<Vec<G::Scalar>>();
1712
1713 transcript.absorb(b"e", &eval_vec.as_slice());
1714 // we now combine eval_left = left(rand) and eval_right = right(rand)
1715 // into claims about input and output
1716 let c = transcript.squeeze(b"c")?;
1717
1718 // eval = (G::Scalar::ONE - c) * eval_left + c * eval_right
1719 // eval is claimed evaluation of input||output(r, c), which can be proven by proving input(r[1..], c) and output(r[1..], c)
1720 let rand_ext = {
1721 let mut r = r_sat.clone();
1722 r.extend(&[c]);
1723 r
1724 };
1725
1726 // add claimed evaluations to the transcript
1727 let evals = self
1728 .eval_input_arr
1729 .into_iter()
1730 .chain(self.eval_output2_arr.into_iter())
1731 .collect::<Vec<G::Scalar>>();
1732 transcript.absorb(b"e", &evals.as_slice());
1733
1734 // squeeze a challenge to combine multiple claims into one
1735 let powers_of_rho = {
1736 let s = transcript.squeeze(b"r")?;
1737 let mut s_vec = vec![s];
1738 for i in 1..num_claims {
1739 s_vec.push(s_vec[i - 1] * s);
1740 }
1741 s_vec
1742 };
1743
1744 // take weighted sum of input, output, and their commitments
1745 let product = self
1746 .claims_product_arr
1747 .iter()
1748 .zip(powers_of_rho.iter())
1749 .map(|(e, p)| *e * p)
1750 .sum();
1751
1752 let eval_output = self
1753 .eval_output_arr
1754 .iter()
1755 .zip(powers_of_rho.iter())
1756 .map(|(e, p)| *e * p)
1757 .sum();
1758
1759 let comm_output = comm_output_vec
1760 .iter()
1761 .zip(powers_of_rho.iter())
1762 .map(|(c, r_i)| *c * *r_i)
1763 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1764
1765 let eval_output2 = self
1766 .eval_output2_arr
1767 .iter()
1768 .zip(powers_of_rho.iter())
1769 .map(|(e, p)| *e * p)
1770 .sum();
1771
1772 // eval_output = output(r_sat)
1773 u_vec.push(PolyEvalInstance {
1774 c: comm_output,
1775 x: r_sat.clone(),
1776 e: eval_output,
1777 });
1778
1779 // claimed_product = output(1, ..., 1, 0)
1780 let x = {
1781 let mut x = vec![G::Scalar::ONE; r_sat.len()];
1782 x[r_sat.len() - 1] = G::Scalar::ZERO;
1783 x
1784 };
1785 u_vec.push(PolyEvalInstance {
1786 c: comm_output,
1787 x,
1788 e: product,
1789 });
1790
1791 // eval_output2 = output(rand_ext[1..])
1792 u_vec.push(PolyEvalInstance {
1793 c: comm_output,
1794 x: rand_ext[1..].to_vec(),
1795 e: eval_output2,
1796 });
1797
1798 let r_prod = rand_ext[1..].to_vec();
1799 // row-related and col-related claims of polynomial evaluations to aid the final check of the sum-check
1800 // we can batch all the claims
1801 transcript.absorb(
1802 b"e",
1803 &[
1804 self.eval_row,
1805 self.eval_row_read_ts,
1806 self.eval_E_row_at_r_prod,
1807 self.eval_row_audit_ts,
1808 self.eval_col,
1809 self.eval_col_read_ts,
1810 self.eval_E_col_at_r_prod,
1811 self.eval_col_audit_ts,
1812 self.eval_W,
1813 ]
1814 .as_slice(),
1815 );
1816 let c = transcript.squeeze(b"c")?;
1817 let eval_vec = [
1818 self.eval_row,
1819 self.eval_row_read_ts,
1820 self.eval_E_row_at_r_prod,
1821 self.eval_row_audit_ts,
1822 self.eval_col,
1823 self.eval_col_read_ts,
1824 self.eval_E_col_at_r_prod,
1825 self.eval_col_audit_ts,
1826 ];
1827 let comm_vec = [
1828 vk.S_comm.comm_row,
1829 vk.S_comm.comm_row_read_ts,
1830 comm_E_row,
1831 vk.S_comm.comm_row_audit_ts,
1832 vk.S_comm.comm_col,
1833 vk.S_comm.comm_col_read_ts,
1834 comm_E_col,
1835 vk.S_comm.comm_col_audit_ts,
1836 ];
1837 let u = PolyEvalInstance::batch(&comm_vec, &r_prod, &eval_vec, &c);
1838
1839 // add the claim to prove for later
1840 u_vec.push(u);
1841
1842 // compute eval_Z
1843 let (eval_Z, r_prod_unpad) = {
1844 // r_prod was padded, so we now remove the padding
1845 let (factor, r_prod_unpad) = {
1846 let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2();
1847
1848 let mut factor = G::Scalar::ONE;
1849 for r_p in r_prod.iter().take(l) {
1850 factor *= G::Scalar::ONE - r_p
1851 }
1852
1853 let r_prod_unpad = {
1854 let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2();
1855 r_prod[l..].to_vec()
1856 };
1857
1858 (factor, r_prod_unpad)
1859 };
1860
1861 let eval_X = {
1862 // constant term
1863 let mut poly_X = vec![(0, U.u)];
1864 //remaining inputs
1865 poly_X.extend(
1866 (0..U.X.len())
1867 .map(|i| (i + 1, U.X[i]))
1868 .collect::<Vec<(usize, G::Scalar)>>(),
1869 );
1870 SparsePolynomial::new((vk.num_vars as f64).log2() as usize, poly_X)
1871 .evaluate(&r_prod_unpad[1..])
1872 };
1873 let eval_Z =
1874 factor * ((G::Scalar::ONE - r_prod_unpad[0]) * self.eval_W + r_prod_unpad[0] * eval_X);
1875
1876 (eval_Z, r_prod_unpad)
1877 };
1878
1879 u_vec.push(PolyEvalInstance {
1880 c: U.comm_W,
1881 x: r_prod_unpad[1..].to_vec(),
1882 e: self.eval_W,
1883 });
1884
1885 // finish the final step of the sum-check
1886 let (claim_init_expected_row, claim_audit_expected_row) = {
1887 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
1888 let val = EqPolynomial::new(tau.to_vec()).evaluate(&r_prod);
1889 (
1890 hash_func(&addr, &val, &G::Scalar::ZERO),
1891 hash_func(&addr, &val, &self.eval_row_audit_ts),
1892 )
1893 };
1894
1895 let (claim_read_expected_row, claim_write_expected_row) = {
1896 (
1897 hash_func(
1898 &self.eval_row,
1899 &self.eval_E_row_at_r_prod,
1900 &self.eval_row_read_ts,
1901 ),
1902 hash_func(
1903 &self.eval_row,
1904 &self.eval_E_row_at_r_prod,
1905 &(self.eval_row_read_ts + G::Scalar::ONE),
1906 ),
1907 )
1908 };
1909
1910 // multiset check for the row
1911 if claim_init_expected_row != self.eval_input_arr[0]
1912 || claim_read_expected_row != self.eval_input_arr[1]
1913 || claim_write_expected_row != self.eval_input_arr[2]
1914 || claim_audit_expected_row != self.eval_input_arr[3]
1915 {
1916 return Err(NovaError::InvalidSumcheckProof);
1917 }
1918
1919 let (claim_init_expected_col, claim_audit_expected_col) = {
1920 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
1921 let val = eval_Z;
1922 (
1923 hash_func(&addr, &val, &G::Scalar::ZERO),
1924 hash_func(&addr, &val, &self.eval_col_audit_ts),
1925 )
1926 };
1927
1928 let (claim_read_expected_col, claim_write_expected_col) = {
1929 (
1930 hash_func(
1931 &self.eval_col,
1932 &self.eval_E_col_at_r_prod,
1933 &self.eval_col_read_ts,
1934 ),
1935 hash_func(
1936 &self.eval_col,
1937 &self.eval_E_col_at_r_prod,
1938 &(self.eval_col_read_ts + G::Scalar::ONE),
1939 ),
1940 )
1941 };
1942
1943 // multiset check for the col
1944 if claim_init_expected_col != self.eval_input_arr[4]
1945 || claim_read_expected_col != self.eval_input_arr[5]
1946 || claim_write_expected_col != self.eval_input_arr[6]
1947 || claim_audit_expected_col != self.eval_input_arr[7]
1948 {
1949 return Err(NovaError::InvalidSumcheckProof);
1950 }
1951
1952 // since all the nine polynomials are opened at r_sat,
1953 // we can combine them into a single polynomial opened at r_sat
1954 let eval_vec = [
1955 self.eval_Az,
1956 self.eval_Bz,
1957 self.eval_Cz,
1958 self.eval_E,
1959 self.eval_E_row,
1960 self.eval_E_col,
1961 self.eval_val_A,
1962 self.eval_val_B,
1963 self.eval_val_C,
1964 ];
1965 let comm_vec = [
1966 comm_Az,
1967 comm_Bz,
1968 comm_Cz,
1969 U.comm_E,
1970 comm_E_row,
1971 comm_E_col,
1972 vk.S_comm.comm_val_A,
1973 vk.S_comm.comm_val_B,
1974 vk.S_comm.comm_val_C,
1975 ];
1976 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1977 let c = transcript.squeeze(b"c")?;
1978 let u = PolyEvalInstance::batch(&comm_vec, &r_sat, &eval_vec, &c);
1979 u_vec.push(u);
1980
1981 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1982
1983 // generate a challenge
1984 let rho = transcript.squeeze(b"r")?;
1985 let num_claims = u_vec.len();
1986 let powers_of_rho = powers::<G>(&rho, num_claims);
1987 let claim_batch_joint = u_vec_padded
1988 .iter()
1989 .zip(powers_of_rho.iter())
1990 .map(|(u, p)| u.e * p)
1991 .sum();
1992
1993 let num_rounds_z = u_vec_padded[0].x.len();
1994 let (claim_batch_final, r_z) =
1995 self
1996 .sc_proof_batch
1997 .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?;
1998
1999 let claim_batch_final_expected = {
2000 let poly_rz = EqPolynomial::new(r_z.clone());
2001 let evals = u_vec_padded
2002 .iter()
2003 .map(|u| poly_rz.evaluate(&u.x))
2004 .collect::<Vec<G::Scalar>>();
2005
2006 evals
2007 .iter()
2008 .zip(self.evals_batch_arr.iter())
2009 .zip(powers_of_rho.iter())
2010 .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i)
2011 .sum()
2012 };
2013
2014 if claim_batch_final != claim_batch_final_expected {
2015 return Err(NovaError::InvalidSumcheckProof);
2016 }
2017
2018 transcript.absorb(b"l", &self.evals_batch_arr.as_slice());
2019
2020 // we now combine evaluation claims at the same point rz into one
2021 let gamma = transcript.squeeze(b"g")?;
2022 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
2023 let comm_joint = u_vec_padded
2024 .iter()
2025 .zip(powers_of_gamma.iter())
2026 .map(|(u, g_i)| u.c * *g_i)
2027 .fold(Commitment::<G>::default(), |acc, item| acc + item);
2028 let eval_joint = self
2029 .evals_batch_arr
2030 .iter()
2031 .zip(powers_of_gamma.iter())
2032 .map(|(e, g_i)| *e * *g_i)
2033 .sum();
2034
2035 // verify
2036 EE::verify(
2037 &vk.vk_ee,
2038 &mut transcript,
2039 &comm_joint,
2040 &r_z,
2041 &eval_joint,
2042 &self.eval_arg,
2043 )?;
2044
2045 Ok(())
2046 }
2047}
2048
2049// provides direct interfaces to call the SNARK implemented in this module
2050struct SpartanCircuit<G: Group, SC: StepCircuit<G::Scalar>> {
2051 z_i: Option<Vec<G::Scalar>>, // inputs to the circuit
2052 sc: SC, // step circuit to be executed
2053}
2054
2055impl<G: Group, SC: StepCircuit<G::Scalar>> Circuit<G::Scalar> for SpartanCircuit<G, SC> {
2056 fn synthesize<CS: ConstraintSystem<G::Scalar>>(self, cs: &mut CS) -> Result<(), SynthesisError> {
2057 // obtain the arity information
2058 let arity = self.sc.arity();
2059
2060 // Allocate zi. If inputs.zi is not provided, allocate default value 0
2061 let zero = vec![G::Scalar::ZERO; arity];
2062 let z_i = (0..arity)
2063 .map(|i| {
2064 AllocatedNum::alloc(cs.namespace(|| format!("zi_{i}")), || {
2065 Ok(self.z_i.as_ref().unwrap_or(&zero)[i])
2066 })
2067 })
2068 .collect::<Result<Vec<AllocatedNum<G::Scalar>>, _>>()?;
2069
2070 let z_i_plus_one = self.sc.synthesize(&mut cs.namespace(|| "F"), &z_i)?;
2071
2072 // inputize both z_i and z_i_plus_one
2073 for (j, input) in z_i.iter().enumerate().take(arity) {
2074 let _ = input.inputize(cs.namespace(|| format!("input {j}")));
2075 }
2076 for (j, output) in z_i_plus_one.iter().enumerate().take(arity) {
2077 let _ = output.inputize(cs.namespace(|| format!("output {j}")));
2078 }
2079
2080 Ok(())
2081 }
2082}
2083
2084/// A type that holds Spartan's prover key
2085#[derive(Clone, Serialize, Deserialize)]
2086#[serde(bound = "")]
2087pub struct SpartanProverKey<G, EE>
2088where
2089 G: Group,
2090 EE: EvaluationEngineTrait<G, CE = G::CE>,
2091{
2092 S: R1CSShape<G>,
2093 ck: CommitmentKey<G>,
2094 pk: ProverKey<G, EE>,
2095}
2096
2097/// A type that holds Spartan's verifier key
2098#[derive(Clone, Serialize, Deserialize)]
2099#[serde(bound = "")]
2100pub struct SpartanVerifierKey<G, EE>
2101where
2102 G: Group,
2103 EE: EvaluationEngineTrait<G, CE = G::CE>,
2104{
2105 vk: VerifierKey<G, EE>,
2106}
2107
2108/// A direct SNARK proving a step circuit
2109#[derive(Clone, Serialize, Deserialize)]
2110#[serde(bound = "")]
2111pub struct SpartanSNARK<G, EE, C>
2112where
2113 G: Group,
2114 EE: EvaluationEngineTrait<G, CE = G::CE>,
2115 C: StepCircuit<G::Scalar>,
2116{
2117 comm_W: Commitment<G>, // commitment to the witness
2118 snark: RelaxedR1CSSNARK<G, EE>, // snark proving the witness is satisfying
2119 _p: PhantomData<C>,
2120}
2121
2122impl<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>, C: StepCircuit<G::Scalar>>
2123 SpartanSNARK<G, EE, C>
2124{
2125 /// Produces prover and verifier keys for Spartan
2126 pub fn setup(sc: C) -> Result<(SpartanProverKey<G, EE>, SpartanVerifierKey<G, EE>), NovaError> {
2127 // construct a circuit that can be synthesized
2128 let circuit: SpartanCircuit<G, C> = SpartanCircuit { z_i: None, sc };
2129
2130 let mut cs: ShapeCS<G> = ShapeCS::new();
2131 let _ = circuit.synthesize(&mut cs);
2132 let (S, ck) = cs.r1cs_shape();
2133
2134 let (pk, vk) = RelaxedR1CSSNARK::setup(&ck, &S)?;
2135
2136 let pk = SpartanProverKey { S, ck, pk };
2137
2138 let vk = SpartanVerifierKey { vk };
2139
2140 Ok((pk, vk))
2141 }
2142
2143 /// Produces a proof of satisfiability of the provided circuit
2144 pub fn prove(pk: &SpartanProverKey<G, EE>, sc: C, z_i: &[G::Scalar]) -> Result<Self, NovaError> {
2145 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
2146
2147 let circuit: SpartanCircuit<G, C> = SpartanCircuit {
2148 z_i: Some(z_i.to_vec()),
2149 sc,
2150 };
2151
2152 let _ = circuit.synthesize(&mut cs);
2153 let (u, w) = cs
2154 .r1cs_instance_and_witness(&pk.S, &pk.ck)
2155 .map_err(|_e| NovaError::UnSat)?;
2156
2157 // convert the instance and witness to relaxed form
2158 let (u_relaxed, w_relaxed) = (
2159 RelaxedR1CSInstance::from_r1cs_instance_unchecked(&u.comm_W, &u.X),
2160 RelaxedR1CSWitness::from_r1cs_witness(&pk.S, &w),
2161 );
2162
2163 // prove the instance using Spartan
2164 let snark = RelaxedR1CSSNARK::prove(&pk.ck, &pk.pk, &u_relaxed, &w_relaxed)?;
2165
2166 Ok(SpartanSNARK {
2167 comm_W: u.comm_W,
2168 snark,
2169 _p: Default::default(),
2170 })
2171 }
2172
2173 /// Verifies a proof of satisfiability
2174 pub fn verify(&self, vk: &SpartanVerifierKey<G, EE>, io: &[G::Scalar]) -> Result<(), NovaError> {
2175 // construct an instance using the provided commitment to the witness and z_i and z_{i+1}
2176 let u_relaxed = RelaxedR1CSInstance::from_r1cs_instance_unchecked(&self.comm_W, io);
2177
2178 // verify the snark using the constructed instance
2179 self.snark.verify(&vk.vk, &u_relaxed)?;
2180
2181 Ok(())
2182 }
2183}
2184
2185#[cfg(test)]
2186mod tests {
2187 use super::*;
2188 use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
2189 use core::marker::PhantomData;
2190 use ff::PrimeField;
2191
2192 #[derive(Clone, Debug, Default)]
2193 struct CubicCircuit<F: PrimeField> {
2194 _p: PhantomData<F>,
2195 }
2196
2197 impl<F> StepCircuit<F> for CubicCircuit<F>
2198 where
2199 F: PrimeField,
2200 {
2201 fn arity(&self) -> usize {
2202 1
2203 }
2204
2205 fn synthesize<CS: ConstraintSystem<F>>(
2206 &self,
2207 cs: &mut CS,
2208 z: &[AllocatedNum<F>],
2209 ) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
2210 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
2211 let x = &z[0];
2212 let x_sq = x.square(cs.namespace(|| "x_sq"))?;
2213 let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), x)?;
2214 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
2215 Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
2216 })?;
2217
2218 cs.enforce(
2219 || "y = x^3 + x + 5",
2220 |lc| {
2221 lc + x_cu.get_variable()
2222 + x.get_variable()
2223 + CS::one()
2224 + CS::one()
2225 + CS::one()
2226 + CS::one()
2227 + CS::one()
2228 },
2229 |lc| lc + CS::one(),
2230 |lc| lc + y.get_variable(),
2231 );
2232
2233 Ok(vec![y])
2234 }
2235
2236 fn output(&self, z: &[F]) -> Vec<F> {
2237 vec![z[0] * z[0] * z[0] + z[0] + F::from(5u64)]
2238 }
2239 }
2240
2241 #[test]
2242 fn test_spartan_snark() {
2243 type G = pasta_curves::pallas::Point;
2244 type EE = crate::provider::ipa_pc::EvaluationEngine<G>;
2245
2246 test_spartan_snark_with::<G, EE>();
2247 }
2248
2249 fn test_spartan_snark_with<G: Group, EE: EvaluationEngineTrait<G, CE = G::CE>>() {
2250 let circuit = CubicCircuit::default();
2251
2252 // produce keys
2253 let (pk, vk) =
2254 SpartanSNARK::<G, EE, CubicCircuit<<G as Group>::Scalar>>::setup(circuit.clone()).unwrap();
2255
2256 let num_steps = 3;
2257
2258 // setup inputs
2259 let z0 = vec![<G as Group>::Scalar::ZERO];
2260 let mut z_i = z0;
2261
2262 for _i in 0..num_steps {
2263 // produce a SNARK
2264 let res = SpartanSNARK::prove(&pk, circuit.clone(), &z_i);
2265 assert!(res.is_ok());
2266
2267 let z_i_plus_one = circuit.output(&z_i);
2268
2269 let snark = res.unwrap();
2270
2271 // verify the SNARK
2272 let io = z_i
2273 .clone()
2274 .into_iter()
2275 .chain(z_i_plus_one.clone().into_iter())
2276 .collect::<Vec<_>>();
2277 let res = snark.verify(&vk, &io);
2278 assert!(res.is_ok());
2279
2280 // set input to the next step
2281 z_i = z_i_plus_one.clone();
2282 }
2283
2284 // sanity: check the claimed output with a direct computation of the same
2285 assert_eq!(z_i, vec![<G as Group>::Scalar::from(2460515u64)]);
2286 }
2287}