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