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