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