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 pk.S.check_regular_shape();
971
972 // append the verifier key (which includes commitment to R1CS matrices) and the RelaxedR1CSInstance to the transcript
973 transcript.absorb(b"vk", &pk.vk_digest);
974 transcript.absorb(b"U", U);
975
976 // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
977 let z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
978
979 // compute Az, Bz, Cz
980 let (mut Az, mut Bz, mut Cz) = pk.S.multiply_vec(&z)?;
981
982 // commit to Az, Bz, Cz
983 let (comm_Az, (comm_Bz, comm_Cz)) = rayon::join(
984 || G::CE::commit(ck, &Az),
985 || rayon::join(|| G::CE::commit(ck, &Bz), || G::CE::commit(ck, &Cz)),
986 );
987
988 transcript.absorb(b"c", &[comm_Az, comm_Bz, comm_Cz].as_slice());
989
990 // number of rounds of the satisfiability sum-check
991 let num_rounds_sat = pk.S_repr.N.log_2();
992 let tau = (0..num_rounds_sat)
993 .map(|_| transcript.squeeze(b"t"))
994 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
995
996 // (1) send commitments to Az, Bz, and Cz along with their evaluations at tau
997 let (Az, Bz, Cz, E) = {
998 Az.resize(pk.S_repr.N, G::Scalar::ZERO);
999 Bz.resize(pk.S_repr.N, G::Scalar::ZERO);
1000 Cz.resize(pk.S_repr.N, G::Scalar::ZERO);
1001
1002 let mut E = W.E.clone();
1003 E.resize(pk.S_repr.N, G::Scalar::ZERO);
1004
1005 (Az, Bz, Cz, E)
1006 };
1007 let (eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau) = {
1008 let evals_at_tau = [&Az, &Bz, &Cz]
1009 .into_par_iter()
1010 .map(|p| MultilinearPolynomial::evaluate_with(p, &tau))
1011 .collect::<Vec<G::Scalar>>();
1012 (evals_at_tau[0], evals_at_tau[1], evals_at_tau[2])
1013 };
1014
1015 // (2) send commitments to the following two oracles
1016 // E_row(i) = eq(tau, row(i)) for all i
1017 // E_col(i) = z(col(i)) for all i
1018 let (mem_row, mem_col, E_row, E_col) = pk.S_repr.evaluation_oracles(&pk.S, &tau, &z);
1019 let (comm_E_row, comm_E_col) =
1020 rayon::join(|| G::CE::commit(ck, &E_row), || G::CE::commit(ck, &E_col));
1021
1022 // absorb the claimed evaluations into the transcript
1023 transcript.absorb(
1024 b"e",
1025 &[eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau].as_slice(),
1026 );
1027 // absorb commitments to E_row and E_col in the transcript
1028 transcript.absorb(b"e", &vec![comm_E_row, comm_E_col].as_slice());
1029
1030 // add claims about Az, Bz, and Cz to be checked later
1031 // since all the three polynomials are opened at tau,
1032 // we can combine them into a single polynomial opened at tau
1033 let eval_vec = vec![eval_Az_at_tau, eval_Bz_at_tau, eval_Cz_at_tau];
1034 let comm_vec = vec![comm_Az, comm_Bz, comm_Cz];
1035 let poly_vec = vec![&Az, &Bz, &Cz];
1036 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1037 let c = transcript.squeeze(b"c")?;
1038 let w = PolyEvalWitness::batch(&poly_vec, &c);
1039 let u = PolyEvalInstance::batch(&comm_vec, &tau, &eval_vec, &c);
1040 w_u_vec.push((w, u));
1041
1042 let c_inner = c;
1043
1044 // we now need to prove three claims
1045 // (1) 0 = \sum_x poly_tau(x) * (poly_Az(x) * poly_Bz(x) - poly_uCz_E(x))
1046 // (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)
1047 // (3) E_row(i) = eq(tau, row(i)) and E_col(i) = z(col(i))
1048
1049 // a sum-check instance to prove the first claim
1050 let mut outer_sc_inst = OuterSumcheckInstance {
1051 poly_tau: MultilinearPolynomial::new(EqPolynomial::new(tau).evals()),
1052 poly_Az: MultilinearPolynomial::new(Az.clone()),
1053 poly_Bz: MultilinearPolynomial::new(Bz.clone()),
1054 poly_uCz_E: {
1055 let uCz_E = (0..Cz.len())
1056 .map(|i| U.u * Cz[i] + E[i])
1057 .collect::<Vec<G::Scalar>>();
1058 MultilinearPolynomial::new(uCz_E)
1059 },
1060 };
1061
1062 // a sum-check instance to prove the second claim
1063 let val = pk
1064 .S_repr
1065 .val_A
1066 .iter()
1067 .zip(pk.S_repr.val_B.iter())
1068 .zip(pk.S_repr.val_C.iter())
1069 .map(|((v_a, v_b), v_c)| *v_a + c_inner * *v_b + c_inner * c_inner * *v_c)
1070 .collect::<Vec<G::Scalar>>();
1071 let mut inner_sc_inst = InnerSumcheckInstance {
1072 claim: eval_Az_at_tau + c_inner * eval_Bz_at_tau + c_inner * c_inner * eval_Cz_at_tau,
1073 poly_E_row: MultilinearPolynomial::new(E_row.clone()),
1074 poly_E_col: MultilinearPolynomial::new(E_col.clone()),
1075 poly_val: MultilinearPolynomial::new(val),
1076 };
1077
1078 // a third sum-check instance to prove the memory-related claim
1079 // we now need to prove that E_row and E_col are well-formed
1080 // we use memory checking: H(INIT) * H(WS) =? H(RS) * H(FINAL)
1081 let gamma_1 = transcript.squeeze(b"g1")?;
1082 let gamma_2 = transcript.squeeze(b"g2")?;
1083
1084 let gamma_1_sqr = gamma_1 * gamma_1;
1085 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
1086 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
1087 };
1088
1089 let init_row = (0..mem_row.len())
1090 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_row[i], &G::Scalar::ZERO))
1091 .collect::<Vec<G::Scalar>>();
1092 let read_row = (0..E_row.len())
1093 .map(|i| hash_func(&pk.S_repr.row[i], &E_row[i], &pk.S_repr.row_read_ts[i]))
1094 .collect::<Vec<G::Scalar>>();
1095 let write_row = (0..E_row.len())
1096 .map(|i| {
1097 hash_func(
1098 &pk.S_repr.row[i],
1099 &E_row[i],
1100 &(pk.S_repr.row_read_ts[i] + G::Scalar::ONE),
1101 )
1102 })
1103 .collect::<Vec<G::Scalar>>();
1104 let audit_row = (0..mem_row.len())
1105 .map(|i| {
1106 hash_func(
1107 &G::Scalar::from(i as u64),
1108 &mem_row[i],
1109 &pk.S_repr.row_audit_ts[i],
1110 )
1111 })
1112 .collect::<Vec<G::Scalar>>();
1113
1114 let init_col = (0..mem_col.len())
1115 .map(|i| hash_func(&G::Scalar::from(i as u64), &mem_col[i], &G::Scalar::ZERO))
1116 .collect::<Vec<G::Scalar>>();
1117 let read_col = (0..E_col.len())
1118 .map(|i| hash_func(&pk.S_repr.col[i], &E_col[i], &pk.S_repr.col_read_ts[i]))
1119 .collect::<Vec<G::Scalar>>();
1120 let write_col = (0..E_col.len())
1121 .map(|i| {
1122 hash_func(
1123 &pk.S_repr.col[i],
1124 &E_col[i],
1125 &(pk.S_repr.col_read_ts[i] + G::Scalar::ONE),
1126 )
1127 })
1128 .collect::<Vec<G::Scalar>>();
1129 let audit_col = (0..mem_col.len())
1130 .map(|i| {
1131 hash_func(
1132 &G::Scalar::from(i as u64),
1133 &mem_col[i],
1134 &pk.S_repr.col_audit_ts[i],
1135 )
1136 })
1137 .collect::<Vec<G::Scalar>>();
1138
1139 let mut mem_sc_inst = ProductSumcheckInstance::new(
1140 ck,
1141 vec![
1142 init_row, read_row, write_row, audit_row, init_col, read_col, write_col, audit_col,
1143 ],
1144 &mut transcript,
1145 )?;
1146
1147 let (sc_sat, r_sat, claims_mem, claims_outer, claims_inner) = Self::prove_inner(
1148 &mut mem_sc_inst,
1149 &mut outer_sc_inst,
1150 &mut inner_sc_inst,
1151 &mut transcript,
1152 )?;
1153
1154 // claims[0] is about the Eq polynomial, which the verifier computes directly
1155 // claims[1] =? weighed sum of left(rand)
1156 // claims[2] =? weighted sum of right(rand)
1157 // claims[3] =? weighted sum of output(rand), which is easy to verify by querying output
1158 // we also need to prove that output(output.len()-2) = claimed_product
1159 let eval_left_vec = claims_mem[1].clone();
1160 let eval_right_vec = claims_mem[2].clone();
1161 let eval_output_vec = claims_mem[3].clone();
1162
1163 // claims from the end of sum-check
1164 let (eval_Az, eval_Bz): (G::Scalar, G::Scalar) = (claims_outer[0][1], claims_outer[0][2]);
1165 let eval_Cz = MultilinearPolynomial::evaluate_with(&Cz, &r_sat);
1166 let eval_E = MultilinearPolynomial::evaluate_with(&E, &r_sat);
1167 let eval_E_row = claims_inner[0][0];
1168 let eval_E_col = claims_inner[0][1];
1169 let eval_val_A = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_A, &r_sat);
1170 let eval_val_B = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_B, &r_sat);
1171 let eval_val_C = MultilinearPolynomial::evaluate_with(&pk.S_repr.val_C, &r_sat);
1172 let eval_vec = vec![
1173 eval_Az, eval_Bz, eval_Cz, eval_E, eval_E_row, eval_E_col, eval_val_A, eval_val_B, eval_val_C,
1174 ]
1175 .into_iter()
1176 .chain(eval_left_vec.clone())
1177 .chain(eval_right_vec.clone())
1178 .chain(eval_output_vec.clone())
1179 .collect::<Vec<G::Scalar>>();
1180
1181 // absorb all the claimed evaluations
1182 transcript.absorb(b"e", &eval_vec.as_slice());
1183
1184 // we now combine eval_left = left(rand) and eval_right = right(rand)
1185 // into claims about input and output
1186 let c = transcript.squeeze(b"c")?;
1187
1188 // eval = (G::Scalar::ONE - c) * eval_left + c * eval_right
1189 // eval is claimed evaluation of input||output(r, c), which can be proven by proving input(r[1..], c) and output(r[1..], c)
1190 let rand_ext = {
1191 let mut r = r_sat.clone();
1192 r.extend(&[c]);
1193 r
1194 };
1195 let eval_input_vec = mem_sc_inst
1196 .input_vec
1197 .iter()
1198 .map(|i| MultilinearPolynomial::evaluate_with(i, &rand_ext[1..]))
1199 .collect::<Vec<G::Scalar>>();
1200
1201 let eval_output2_vec = mem_sc_inst
1202 .output_vec
1203 .iter()
1204 .map(|o| MultilinearPolynomial::evaluate_with(o, &rand_ext[1..]))
1205 .collect::<Vec<G::Scalar>>();
1206
1207 // add claimed evaluations to the transcript
1208 let evals = eval_input_vec
1209 .clone()
1210 .into_iter()
1211 .chain(eval_output2_vec.clone())
1212 .collect::<Vec<G::Scalar>>();
1213 transcript.absorb(b"e", &evals.as_slice());
1214
1215 // squeeze a challenge to combine multiple claims into one
1216 let powers_of_rho = {
1217 let s = transcript.squeeze(b"r")?;
1218 let mut s_vec = vec![s];
1219 for i in 1..mem_sc_inst.initial_claims().len() {
1220 s_vec.push(s_vec[i - 1] * s);
1221 }
1222 s_vec
1223 };
1224
1225 // take weighted sum of input, output, and their commitments
1226 let product = mem_sc_inst
1227 .claims
1228 .iter()
1229 .zip(powers_of_rho.iter())
1230 .map(|(e, p)| *e * p)
1231 .sum();
1232
1233 let eval_output = eval_output_vec
1234 .iter()
1235 .zip(powers_of_rho.iter())
1236 .map(|(e, p)| *e * p)
1237 .sum();
1238
1239 let comm_output = mem_sc_inst
1240 .comm_output_vec
1241 .iter()
1242 .zip(powers_of_rho.iter())
1243 .map(|(c, r_i)| *c * *r_i)
1244 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1245
1246 let weighted_sum = |W: &[Vec<G::Scalar>], s: &[G::Scalar]| -> Vec<G::Scalar> {
1247 assert_eq!(W.len(), s.len());
1248 let mut p = vec![G::Scalar::ZERO; W[0].len()];
1249 for i in 0..W.len() {
1250 for (j, item) in W[i].iter().enumerate().take(W[i].len()) {
1251 p[j] += *item * s[i]
1252 }
1253 }
1254 p
1255 };
1256
1257 let poly_output = weighted_sum(&mem_sc_inst.output_vec, &powers_of_rho);
1258
1259 let eval_output2 = eval_output2_vec
1260 .iter()
1261 .zip(powers_of_rho.iter())
1262 .map(|(e, p)| *e * p)
1263 .sum();
1264
1265 // eval_output = output(r_sat)
1266 w_u_vec.push((
1267 PolyEvalWitness {
1268 p: poly_output.clone(),
1269 },
1270 PolyEvalInstance {
1271 c: comm_output,
1272 x: r_sat.clone(),
1273 e: eval_output,
1274 },
1275 ));
1276
1277 // claimed_product = output(1, ..., 1, 0)
1278 let x = {
1279 let mut x = vec![G::Scalar::ONE; r_sat.len()];
1280 x[r_sat.len() - 1] = G::Scalar::ZERO;
1281 x
1282 };
1283 w_u_vec.push((
1284 PolyEvalWitness {
1285 p: poly_output.clone(),
1286 },
1287 PolyEvalInstance {
1288 c: comm_output,
1289 x,
1290 e: product,
1291 },
1292 ));
1293
1294 // eval_output2 = output(rand_ext[1..])
1295 w_u_vec.push((
1296 PolyEvalWitness { p: poly_output },
1297 PolyEvalInstance {
1298 c: comm_output,
1299 x: rand_ext[1..].to_vec(),
1300 e: eval_output2,
1301 },
1302 ));
1303
1304 let r_prod = rand_ext[1..].to_vec();
1305 // row-related and col-related claims of polynomial evaluations to aid the final check of the sum-check
1306 let evals = [
1307 &pk.S_repr.row,
1308 &pk.S_repr.row_read_ts,
1309 &E_row,
1310 &pk.S_repr.row_audit_ts,
1311 &pk.S_repr.col,
1312 &pk.S_repr.col_read_ts,
1313 &E_col,
1314 &pk.S_repr.col_audit_ts,
1315 ]
1316 .into_par_iter()
1317 .map(|p| MultilinearPolynomial::evaluate_with(p, &r_prod))
1318 .collect::<Vec<G::Scalar>>();
1319
1320 let eval_row = evals[0];
1321 let eval_row_read_ts = evals[1];
1322 let eval_E_row_at_r_prod = evals[2];
1323 let eval_row_audit_ts = evals[3];
1324 let eval_col = evals[4];
1325 let eval_col_read_ts = evals[5];
1326 let eval_E_col_at_r_prod = evals[6];
1327 let eval_col_audit_ts = evals[7];
1328
1329 // 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..]).
1330 // r_prod was padded, so we now remove the padding
1331 let r_prod_unpad = {
1332 let l = pk.S_repr.N.log_2() - (2 * pk.S.num_vars).log_2();
1333 r_prod[l..].to_vec()
1334 };
1335
1336 let eval_W = MultilinearPolynomial::evaluate_with(&W.W, &r_prod_unpad[1..]);
1337
1338 // we can batch all the claims
1339 transcript.absorb(
1340 b"e",
1341 &[
1342 eval_row,
1343 eval_row_read_ts,
1344 eval_E_row_at_r_prod,
1345 eval_row_audit_ts,
1346 eval_col,
1347 eval_col_read_ts,
1348 eval_E_col_at_r_prod,
1349 eval_col_audit_ts,
1350 eval_W, // this will not be batched below as it is evaluated at r_prod[1..]
1351 ]
1352 .as_slice(),
1353 );
1354
1355 let c = transcript.squeeze(b"c")?;
1356 let eval_vec = [
1357 eval_row,
1358 eval_row_read_ts,
1359 eval_E_row_at_r_prod,
1360 eval_row_audit_ts,
1361 eval_col,
1362 eval_col_read_ts,
1363 eval_E_col_at_r_prod,
1364 eval_col_audit_ts,
1365 ];
1366 let comm_vec = [
1367 pk.S_comm.comm_row,
1368 pk.S_comm.comm_row_read_ts,
1369 comm_E_row,
1370 pk.S_comm.comm_row_audit_ts,
1371 pk.S_comm.comm_col,
1372 pk.S_comm.comm_col_read_ts,
1373 comm_E_col,
1374 pk.S_comm.comm_col_audit_ts,
1375 ];
1376 let poly_vec = [
1377 &pk.S_repr.row,
1378 &pk.S_repr.row_read_ts,
1379 &E_row,
1380 &pk.S_repr.row_audit_ts,
1381 &pk.S_repr.col,
1382 &pk.S_repr.col_read_ts,
1383 &E_col,
1384 &pk.S_repr.col_audit_ts,
1385 ];
1386 let w = PolyEvalWitness::batch(&poly_vec, &c);
1387 let u = PolyEvalInstance::batch(&comm_vec, &r_prod, &eval_vec, &c);
1388
1389 // add the claim to prove for later
1390 w_u_vec.push((w, u));
1391
1392 w_u_vec.push((
1393 PolyEvalWitness { p: W.W },
1394 PolyEvalInstance {
1395 c: U.comm_W,
1396 x: r_prod_unpad[1..].to_vec(),
1397 e: eval_W,
1398 },
1399 ));
1400
1401 // all nine evaluations are at r_sat, we can fold them into one; they were added to the transcript earlier
1402 let eval_vec = [
1403 eval_Az, eval_Bz, eval_Cz, eval_E, eval_E_row, eval_E_col, eval_val_A, eval_val_B, eval_val_C,
1404 ];
1405 let comm_vec = [
1406 comm_Az,
1407 comm_Bz,
1408 comm_Cz,
1409 U.comm_E,
1410 comm_E_row,
1411 comm_E_col,
1412 pk.S_comm.comm_val_A,
1413 pk.S_comm.comm_val_B,
1414 pk.S_comm.comm_val_C,
1415 ];
1416 let poly_vec = [
1417 &Az,
1418 &Bz,
1419 &Cz,
1420 &E,
1421 &E_row,
1422 &E_col,
1423 &pk.S_repr.val_A,
1424 &pk.S_repr.val_B,
1425 &pk.S_repr.val_C,
1426 ];
1427 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1428 let c = transcript.squeeze(b"c")?;
1429 let w = PolyEvalWitness::batch(&poly_vec, &c);
1430 let u = PolyEvalInstance::batch(&comm_vec, &r_sat, &eval_vec, &c);
1431 w_u_vec.push((w, u));
1432
1433 // We will now reduce a vector of claims of evaluations at different points into claims about them at the same point.
1434 // For example, eval_W =? W(r_y[1..]) and eval_W =? E(r_x) into
1435 // two claims: eval_W_prime =? W(rz) and eval_E_prime =? E(rz)
1436 // We can them combine the two into one: eval_W_prime + gamma * eval_E_prime =? (W + gamma*E)(rz),
1437 // where gamma is a public challenge
1438 // Since commitments to W and E are homomorphic, the verifier can compute a commitment
1439 // to the batched polynomial.
1440 assert!(w_u_vec.len() >= 2);
1441
1442 let (w_vec, u_vec): (Vec<PolyEvalWitness<G>>, Vec<PolyEvalInstance<G>>) =
1443 w_u_vec.into_iter().unzip();
1444 let w_vec_padded = PolyEvalWitness::pad(&w_vec); // pad the polynomials to be of the same size
1445 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1446
1447 // generate a challenge
1448 let rho = transcript.squeeze(b"r")?;
1449 let num_claims = w_vec_padded.len();
1450 let powers_of_rho = powers::<G>(&rho, num_claims);
1451 let claim_batch_joint = u_vec_padded
1452 .iter()
1453 .zip(powers_of_rho.iter())
1454 .map(|(u, p)| u.e * p)
1455 .sum();
1456
1457 let mut polys_left: Vec<MultilinearPolynomial<G::Scalar>> = w_vec_padded
1458 .iter()
1459 .map(|w| MultilinearPolynomial::new(w.p.clone()))
1460 .collect();
1461 let mut polys_right: Vec<MultilinearPolynomial<G::Scalar>> = u_vec_padded
1462 .iter()
1463 .map(|u| MultilinearPolynomial::new(EqPolynomial::new(u.x.clone()).evals()))
1464 .collect();
1465
1466 let num_rounds_z = u_vec_padded[0].x.len();
1467 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
1468 *poly_A_comp * *poly_B_comp
1469 };
1470 let (sc_proof_batch, r_z, claims_batch) = SumcheckProof::prove_quad_batch(
1471 &claim_batch_joint,
1472 num_rounds_z,
1473 &mut polys_left,
1474 &mut polys_right,
1475 &powers_of_rho,
1476 comb_func,
1477 &mut transcript,
1478 )?;
1479
1480 let (claims_batch_left, _): (Vec<G::Scalar>, Vec<G::Scalar>) = claims_batch;
1481
1482 transcript.absorb(b"l", &claims_batch_left.as_slice());
1483
1484 // we now combine evaluation claims at the same point rz into one
1485 let gamma = transcript.squeeze(b"g")?;
1486 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
1487 let comm_joint = u_vec_padded
1488 .iter()
1489 .zip(powers_of_gamma.iter())
1490 .map(|(u, g_i)| u.c * *g_i)
1491 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1492 let poly_joint = PolyEvalWitness::weighted_sum(&w_vec_padded, &powers_of_gamma);
1493 let eval_joint = claims_batch_left
1494 .iter()
1495 .zip(powers_of_gamma.iter())
1496 .map(|(e, g_i)| *e * *g_i)
1497 .sum();
1498
1499 let eval_arg = EE::prove(
1500 ck,
1501 &pk.pk_ee,
1502 &mut transcript,
1503 &comm_joint,
1504 &poly_joint.p,
1505 &r_z,
1506 &eval_joint,
1507 )?;
1508
1509 Ok(RelaxedR1CSSNARK {
1510 comm_Az: comm_Az.compress(),
1511 comm_Bz: comm_Bz.compress(),
1512 comm_Cz: comm_Cz.compress(),
1513 comm_E_row: comm_E_row.compress(),
1514 comm_E_col: comm_E_col.compress(),
1515 eval_Az_at_tau,
1516 eval_Bz_at_tau,
1517 eval_Cz_at_tau,
1518 comm_output_arr: vec_to_arr(
1519 mem_sc_inst
1520 .comm_output_vec
1521 .iter()
1522 .map(|c| c.compress())
1523 .collect::<Vec<CompressedCommitment<G>>>(),
1524 ),
1525 claims_product_arr: vec_to_arr(mem_sc_inst.claims.clone()),
1526
1527 sc_sat,
1528
1529 eval_Az,
1530 eval_Bz,
1531 eval_Cz,
1532 eval_E,
1533 eval_E_row,
1534 eval_E_col,
1535 eval_val_A,
1536 eval_val_B,
1537 eval_val_C,
1538
1539 eval_left_arr: vec_to_arr(eval_left_vec),
1540 eval_right_arr: vec_to_arr(eval_right_vec),
1541 eval_output_arr: vec_to_arr(eval_output_vec),
1542 eval_input_arr: vec_to_arr(eval_input_vec),
1543 eval_output2_arr: vec_to_arr(eval_output2_vec),
1544
1545 eval_row,
1546 eval_row_read_ts,
1547 eval_E_row_at_r_prod,
1548 eval_row_audit_ts,
1549 eval_col,
1550 eval_col_read_ts,
1551 eval_E_col_at_r_prod,
1552 eval_col_audit_ts,
1553 eval_W,
1554
1555 sc_proof_batch,
1556 evals_batch_arr: vec_to_arr(claims_batch_left),
1557 eval_arg,
1558 })
1559 }
1560
1561 /// verifies a proof of satisfiability of a RelaxedR1CS instance
1562 fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
1563 let mut transcript = G::TE::new(b"RelaxedR1CSSNARK");
1564 let mut u_vec: Vec<PolyEvalInstance<G>> = Vec::new();
1565
1566 // append the verifier key (including commitment to R1CS matrices) and the RelaxedR1CSInstance to the transcript
1567 transcript.absorb(b"vk", &vk.digest);
1568 transcript.absorb(b"U", U);
1569
1570 let comm_Az = Commitment::<G>::decompress(&self.comm_Az)?;
1571 let comm_Bz = Commitment::<G>::decompress(&self.comm_Bz)?;
1572 let comm_Cz = Commitment::<G>::decompress(&self.comm_Cz)?;
1573 let comm_E_row = Commitment::<G>::decompress(&self.comm_E_row)?;
1574 let comm_E_col = Commitment::<G>::decompress(&self.comm_E_col)?;
1575
1576 transcript.absorb(b"c", &[comm_Az, comm_Bz, comm_Cz].as_slice());
1577
1578 let num_rounds_sat = vk.S_comm.N.log_2();
1579 let tau = (0..num_rounds_sat)
1580 .map(|_i| transcript.squeeze(b"t"))
1581 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1582
1583 transcript.absorb(
1584 b"e",
1585 &[
1586 self.eval_Az_at_tau,
1587 self.eval_Bz_at_tau,
1588 self.eval_Cz_at_tau,
1589 ]
1590 .as_slice(),
1591 );
1592
1593 transcript.absorb(b"e", &vec![comm_E_row, comm_E_col].as_slice());
1594
1595 // add claims about Az, Bz, and Cz to be checked later
1596 // since all the three polynomials are opened at tau,
1597 // we can combine them into a single polynomial opened at tau
1598 let eval_vec = vec![
1599 self.eval_Az_at_tau,
1600 self.eval_Bz_at_tau,
1601 self.eval_Cz_at_tau,
1602 ];
1603 let comm_vec = vec![comm_Az, comm_Bz, comm_Cz];
1604 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1605 let c = transcript.squeeze(b"c")?;
1606 let u = PolyEvalInstance::batch(&comm_vec, &tau, &eval_vec, &c);
1607 let claim_inner = u.e;
1608 let c_inner = c;
1609 u_vec.push(u);
1610
1611 let gamma_1 = transcript.squeeze(b"g1")?;
1612 let gamma_2 = transcript.squeeze(b"g2")?;
1613
1614 // hash function
1615 let gamma_1_sqr = gamma_1 * gamma_1;
1616 let hash_func = |addr: &G::Scalar, val: &G::Scalar, ts: &G::Scalar| -> G::Scalar {
1617 (*ts * gamma_1_sqr + *val * gamma_1 + *addr) - gamma_2
1618 };
1619
1620 // check the required multiset relationship
1621 // row
1622 if self.claims_product_arr[0] * self.claims_product_arr[2]
1623 != self.claims_product_arr[1] * self.claims_product_arr[3]
1624 {
1625 return Err(NovaError::InvalidMultisetProof);
1626 }
1627 // col
1628 if self.claims_product_arr[4] * self.claims_product_arr[6]
1629 != self.claims_product_arr[5] * self.claims_product_arr[7]
1630 {
1631 return Err(NovaError::InvalidMultisetProof);
1632 }
1633
1634 let comm_output_vec = self
1635 .comm_output_arr
1636 .iter()
1637 .map(|c| Commitment::<G>::decompress(c))
1638 .collect::<Result<Vec<Commitment<G>>, NovaError>>()?;
1639
1640 transcript.absorb(b"o", &comm_output_vec.as_slice());
1641 transcript.absorb(b"c", &self.claims_product_arr.as_slice());
1642
1643 let num_rounds = vk.S_comm.N.log_2();
1644 let rand_eq = (0..num_rounds)
1645 .map(|_i| transcript.squeeze(b"e"))
1646 .collect::<Result<Vec<G::Scalar>, NovaError>>()?;
1647
1648 let num_claims = 10;
1649 let coeffs = {
1650 let s = transcript.squeeze(b"r")?;
1651 let mut s_vec = vec![s];
1652 for i in 1..num_claims {
1653 s_vec.push(s_vec[i - 1] * s);
1654 }
1655 s_vec
1656 };
1657
1658 let claim = coeffs[9] * claim_inner; // rest are zeros
1659 let (claim_sat_final, r_sat) = self
1660 .sc_sat
1661 .verify(claim, num_rounds_sat, 3, &mut transcript)?;
1662
1663 // verify claim_sat_final
1664 let taus_bound_r_sat = EqPolynomial::new(tau.clone()).evaluate(&r_sat);
1665 let rand_eq_bound_r_sat = EqPolynomial::new(rand_eq).evaluate(&r_sat);
1666 let claim_mem_final_expected: G::Scalar = (0..8)
1667 .map(|i| {
1668 coeffs[i]
1669 * rand_eq_bound_r_sat
1670 * (self.eval_left_arr[i] * self.eval_right_arr[i] - self.eval_output_arr[i])
1671 })
1672 .sum();
1673 let claim_outer_final_expected = coeffs[8]
1674 * taus_bound_r_sat
1675 * (self.eval_Az * self.eval_Bz - U.u * self.eval_Cz - self.eval_E);
1676 let claim_inner_final_expected = coeffs[9]
1677 * self.eval_E_row
1678 * self.eval_E_col
1679 * (self.eval_val_A + c_inner * self.eval_val_B + c_inner * c_inner * self.eval_val_C);
1680
1681 if claim_mem_final_expected + claim_outer_final_expected + claim_inner_final_expected
1682 != claim_sat_final
1683 {
1684 return Err(NovaError::InvalidSumcheckProof);
1685 }
1686
1687 // claims from the end of the sum-check
1688 let eval_vec = [
1689 self.eval_Az,
1690 self.eval_Bz,
1691 self.eval_Cz,
1692 self.eval_E,
1693 self.eval_E_row,
1694 self.eval_E_col,
1695 self.eval_val_A,
1696 self.eval_val_B,
1697 self.eval_val_C,
1698 ]
1699 .into_iter()
1700 .chain(self.eval_left_arr)
1701 .chain(self.eval_right_arr)
1702 .chain(self.eval_output_arr)
1703 .collect::<Vec<G::Scalar>>();
1704
1705 transcript.absorb(b"e", &eval_vec.as_slice());
1706 // we now combine eval_left = left(rand) and eval_right = right(rand)
1707 // into claims about input and output
1708 let c = transcript.squeeze(b"c")?;
1709
1710 // eval = (G::Scalar::ONE - c) * eval_left + c * eval_right
1711 // eval is claimed evaluation of input||output(r, c), which can be proven by proving input(r[1..], c) and output(r[1..], c)
1712 let rand_ext = {
1713 let mut r = r_sat.clone();
1714 r.extend(&[c]);
1715 r
1716 };
1717
1718 // add claimed evaluations to the transcript
1719 let evals = self
1720 .eval_input_arr
1721 .into_iter()
1722 .chain(self.eval_output2_arr)
1723 .collect::<Vec<G::Scalar>>();
1724 transcript.absorb(b"e", &evals.as_slice());
1725
1726 // squeeze a challenge to combine multiple claims into one
1727 let powers_of_rho = {
1728 let s = transcript.squeeze(b"r")?;
1729 let mut s_vec = vec![s];
1730 for i in 1..num_claims {
1731 s_vec.push(s_vec[i - 1] * s);
1732 }
1733 s_vec
1734 };
1735
1736 // take weighted sum of input, output, and their commitments
1737 let product = self
1738 .claims_product_arr
1739 .iter()
1740 .zip(powers_of_rho.iter())
1741 .map(|(e, p)| *e * p)
1742 .sum();
1743
1744 let eval_output = self
1745 .eval_output_arr
1746 .iter()
1747 .zip(powers_of_rho.iter())
1748 .map(|(e, p)| *e * p)
1749 .sum();
1750
1751 let comm_output = comm_output_vec
1752 .iter()
1753 .zip(powers_of_rho.iter())
1754 .map(|(c, r_i)| *c * *r_i)
1755 .fold(Commitment::<G>::default(), |acc, item| acc + item);
1756
1757 let eval_output2 = self
1758 .eval_output2_arr
1759 .iter()
1760 .zip(powers_of_rho.iter())
1761 .map(|(e, p)| *e * p)
1762 .sum();
1763
1764 // eval_output = output(r_sat)
1765 u_vec.push(PolyEvalInstance {
1766 c: comm_output,
1767 x: r_sat.clone(),
1768 e: eval_output,
1769 });
1770
1771 // claimed_product = output(1, ..., 1, 0)
1772 let x = {
1773 let mut x = vec![G::Scalar::ONE; r_sat.len()];
1774 x[r_sat.len() - 1] = G::Scalar::ZERO;
1775 x
1776 };
1777 u_vec.push(PolyEvalInstance {
1778 c: comm_output,
1779 x,
1780 e: product,
1781 });
1782
1783 // eval_output2 = output(rand_ext[1..])
1784 u_vec.push(PolyEvalInstance {
1785 c: comm_output,
1786 x: rand_ext[1..].to_vec(),
1787 e: eval_output2,
1788 });
1789
1790 let r_prod = rand_ext[1..].to_vec();
1791 // row-related and col-related claims of polynomial evaluations to aid the final check of the sum-check
1792 // we can batch all the claims
1793 transcript.absorb(
1794 b"e",
1795 &[
1796 self.eval_row,
1797 self.eval_row_read_ts,
1798 self.eval_E_row_at_r_prod,
1799 self.eval_row_audit_ts,
1800 self.eval_col,
1801 self.eval_col_read_ts,
1802 self.eval_E_col_at_r_prod,
1803 self.eval_col_audit_ts,
1804 self.eval_W,
1805 ]
1806 .as_slice(),
1807 );
1808 let c = transcript.squeeze(b"c")?;
1809 let eval_vec = [
1810 self.eval_row,
1811 self.eval_row_read_ts,
1812 self.eval_E_row_at_r_prod,
1813 self.eval_row_audit_ts,
1814 self.eval_col,
1815 self.eval_col_read_ts,
1816 self.eval_E_col_at_r_prod,
1817 self.eval_col_audit_ts,
1818 ];
1819 let comm_vec = [
1820 vk.S_comm.comm_row,
1821 vk.S_comm.comm_row_read_ts,
1822 comm_E_row,
1823 vk.S_comm.comm_row_audit_ts,
1824 vk.S_comm.comm_col,
1825 vk.S_comm.comm_col_read_ts,
1826 comm_E_col,
1827 vk.S_comm.comm_col_audit_ts,
1828 ];
1829 let u = PolyEvalInstance::batch(&comm_vec, &r_prod, &eval_vec, &c);
1830
1831 // add the claim to prove for later
1832 u_vec.push(u);
1833
1834 // compute eval_Z
1835 let (eval_Z, r_prod_unpad) = {
1836 // r_prod was padded, so we now remove the padding
1837 let (factor, r_prod_unpad) = {
1838 let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2();
1839
1840 let mut factor = G::Scalar::ONE;
1841 for r_p in r_prod.iter().take(l) {
1842 factor *= G::Scalar::ONE - r_p
1843 }
1844
1845 let r_prod_unpad = {
1846 let l = vk.S_comm.N.log_2() - (2 * vk.num_vars).log_2();
1847 r_prod[l..].to_vec()
1848 };
1849
1850 (factor, r_prod_unpad)
1851 };
1852
1853 let eval_X = {
1854 // constant term
1855 let mut poly_X = vec![(0, U.u)];
1856 //remaining inputs
1857 poly_X.extend(
1858 (0..U.X.len())
1859 .map(|i| (i + 1, U.X[i]))
1860 .collect::<Vec<(usize, G::Scalar)>>(),
1861 );
1862 SparsePolynomial::new((vk.num_vars as f64).log2() as usize, poly_X)
1863 .evaluate(&r_prod_unpad[1..])
1864 };
1865 let eval_Z =
1866 factor * ((G::Scalar::ONE - r_prod_unpad[0]) * self.eval_W + r_prod_unpad[0] * eval_X);
1867
1868 (eval_Z, r_prod_unpad)
1869 };
1870
1871 u_vec.push(PolyEvalInstance {
1872 c: U.comm_W,
1873 x: r_prod_unpad[1..].to_vec(),
1874 e: self.eval_W,
1875 });
1876
1877 // finish the final step of the sum-check
1878 let (claim_init_expected_row, claim_audit_expected_row) = {
1879 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
1880 let val = EqPolynomial::new(tau.to_vec()).evaluate(&r_prod);
1881 (
1882 hash_func(&addr, &val, &G::Scalar::ZERO),
1883 hash_func(&addr, &val, &self.eval_row_audit_ts),
1884 )
1885 };
1886
1887 let (claim_read_expected_row, claim_write_expected_row) = {
1888 (
1889 hash_func(
1890 &self.eval_row,
1891 &self.eval_E_row_at_r_prod,
1892 &self.eval_row_read_ts,
1893 ),
1894 hash_func(
1895 &self.eval_row,
1896 &self.eval_E_row_at_r_prod,
1897 &(self.eval_row_read_ts + G::Scalar::ONE),
1898 ),
1899 )
1900 };
1901
1902 // multiset check for the row
1903 if claim_init_expected_row != self.eval_input_arr[0]
1904 || claim_read_expected_row != self.eval_input_arr[1]
1905 || claim_write_expected_row != self.eval_input_arr[2]
1906 || claim_audit_expected_row != self.eval_input_arr[3]
1907 {
1908 return Err(NovaError::InvalidSumcheckProof);
1909 }
1910
1911 let (claim_init_expected_col, claim_audit_expected_col) = {
1912 let addr = IdentityPolynomial::new(r_prod.len()).evaluate(&r_prod);
1913 let val = eval_Z;
1914 (
1915 hash_func(&addr, &val, &G::Scalar::ZERO),
1916 hash_func(&addr, &val, &self.eval_col_audit_ts),
1917 )
1918 };
1919
1920 let (claim_read_expected_col, claim_write_expected_col) = {
1921 (
1922 hash_func(
1923 &self.eval_col,
1924 &self.eval_E_col_at_r_prod,
1925 &self.eval_col_read_ts,
1926 ),
1927 hash_func(
1928 &self.eval_col,
1929 &self.eval_E_col_at_r_prod,
1930 &(self.eval_col_read_ts + G::Scalar::ONE),
1931 ),
1932 )
1933 };
1934
1935 // multiset check for the col
1936 if claim_init_expected_col != self.eval_input_arr[4]
1937 || claim_read_expected_col != self.eval_input_arr[5]
1938 || claim_write_expected_col != self.eval_input_arr[6]
1939 || claim_audit_expected_col != self.eval_input_arr[7]
1940 {
1941 return Err(NovaError::InvalidSumcheckProof);
1942 }
1943
1944 // since all the nine polynomials are opened at r_sat,
1945 // we can combine them into a single polynomial opened at r_sat
1946 let eval_vec = [
1947 self.eval_Az,
1948 self.eval_Bz,
1949 self.eval_Cz,
1950 self.eval_E,
1951 self.eval_E_row,
1952 self.eval_E_col,
1953 self.eval_val_A,
1954 self.eval_val_B,
1955 self.eval_val_C,
1956 ];
1957 let comm_vec = [
1958 comm_Az,
1959 comm_Bz,
1960 comm_Cz,
1961 U.comm_E,
1962 comm_E_row,
1963 comm_E_col,
1964 vk.S_comm.comm_val_A,
1965 vk.S_comm.comm_val_B,
1966 vk.S_comm.comm_val_C,
1967 ];
1968 transcript.absorb(b"e", &eval_vec.as_slice()); // c_vec is already in the transcript
1969 let c = transcript.squeeze(b"c")?;
1970 let u = PolyEvalInstance::batch(&comm_vec, &r_sat, &eval_vec, &c);
1971 u_vec.push(u);
1972
1973 let u_vec_padded = PolyEvalInstance::pad(&u_vec); // pad the evaluation points
1974
1975 // generate a challenge
1976 let rho = transcript.squeeze(b"r")?;
1977 let num_claims = u_vec.len();
1978 let powers_of_rho = powers::<G>(&rho, num_claims);
1979 let claim_batch_joint = u_vec_padded
1980 .iter()
1981 .zip(powers_of_rho.iter())
1982 .map(|(u, p)| u.e * p)
1983 .sum();
1984
1985 let num_rounds_z = u_vec_padded[0].x.len();
1986 let (claim_batch_final, r_z) =
1987 self
1988 .sc_proof_batch
1989 .verify(claim_batch_joint, num_rounds_z, 2, &mut transcript)?;
1990
1991 let claim_batch_final_expected = {
1992 let poly_rz = EqPolynomial::new(r_z.clone());
1993 let evals = u_vec_padded
1994 .iter()
1995 .map(|u| poly_rz.evaluate(&u.x))
1996 .collect::<Vec<G::Scalar>>();
1997
1998 evals
1999 .iter()
2000 .zip(self.evals_batch_arr.iter())
2001 .zip(powers_of_rho.iter())
2002 .map(|((e_i, p_i), rho_i)| *e_i * *p_i * rho_i)
2003 .sum()
2004 };
2005
2006 if claim_batch_final != claim_batch_final_expected {
2007 return Err(NovaError::InvalidSumcheckProof);
2008 }
2009
2010 transcript.absorb(b"l", &self.evals_batch_arr.as_slice());
2011
2012 // we now combine evaluation claims at the same point rz into one
2013 let gamma = transcript.squeeze(b"g")?;
2014 let powers_of_gamma: Vec<G::Scalar> = powers::<G>(&gamma, num_claims);
2015 let comm_joint = u_vec_padded
2016 .iter()
2017 .zip(powers_of_gamma.iter())
2018 .map(|(u, g_i)| u.c * *g_i)
2019 .fold(Commitment::<G>::default(), |acc, item| acc + item);
2020 let eval_joint = self
2021 .evals_batch_arr
2022 .iter()
2023 .zip(powers_of_gamma.iter())
2024 .map(|(e, g_i)| *e * *g_i)
2025 .sum();
2026
2027 // verify
2028 EE::verify(
2029 &vk.vk_ee,
2030 &mut transcript,
2031 &comm_joint,
2032 &r_z,
2033 &eval_joint,
2034 &self.eval_arg,
2035 )?;
2036
2037 Ok(())
2038 }
2039}