Nova/src/spartan_with_ipa_pc/mod.rs
src/spartan_with_ipa_pc/mod.rsRaw
1//! This module implements RelaxedR1CSSNARKTrait using a Spartan variant
2//! instantiated with an IPA-based polynomial commitment scheme
3mod ipa;
4mod polynomial;
5mod sumcheck;
6
7use super::{
8 commitments::CommitGens,
9 errors::NovaError,
10 r1cs::{R1CSGens, R1CSShape, RelaxedR1CSInstance, RelaxedR1CSWitness},
11 snark::{ProverKeyTrait, RelaxedR1CSSNARKTrait, VerifierKeyTrait},
12 traits::{AppendToTranscriptTrait, ChallengeTrait, Group},
13};
14use core::cmp::max;
15use ff::Field;
16use ipa::{InnerProductArgument, InnerProductInstance, InnerProductWitness, NIFSForInnerProduct};
17use itertools::concat;
18use merlin::Transcript;
19use polynomial::{EqPolynomial, MultilinearPolynomial, SparsePolynomial};
20use rayon::prelude::*;
21use sumcheck::SumcheckProof;
22
23/// A type that represents the prover's key
24pub struct ProverKey<G: Group> {
25 gens_r1cs: R1CSGens<G>,
26 gens_ipa: CommitGens<G>,
27 S: R1CSShape<G>,
28}
29
30impl<G: Group> ProverKeyTrait<G> for ProverKey<G> {
31 fn new(gens: &R1CSGens<G>, S: &R1CSShape<G>) -> Self {
32 ProverKey {
33 gens_r1cs: gens.clone(),
34 gens_ipa: CommitGens::new(b"ipa", 1),
35 S: S.clone(),
36 }
37 }
38}
39
40/// A type that represents the verifier's key
41pub struct VerifierKey<G: Group> {
42 gens_r1cs: R1CSGens<G>,
43 gens_ipa: CommitGens<G>,
44 S: R1CSShape<G>,
45}
46
47impl<G: Group> VerifierKeyTrait<G> for VerifierKey<G> {
48 fn new(gens: &R1CSGens<G>, S: &R1CSShape<G>) -> Self {
49 VerifierKey {
50 gens_r1cs: gens.clone(),
51 gens_ipa: CommitGens::new(b"ipa", 1),
52 S: S.clone(),
53 }
54 }
55}
56
57/// A succinct proof of knowledge of a witness to a relaxed R1CS instance
58/// The proof is produced using Spartan's combination of the sum-check and
59/// the commitment to a vector viewed as a polynomial commitment
60pub struct RelaxedR1CSSNARK<G: Group> {
61 sc_proof_outer: SumcheckProof<G>,
62 claims_outer: (G::Scalar, G::Scalar, G::Scalar),
63 sc_proof_inner: SumcheckProof<G>,
64 eval_E: G::Scalar,
65 eval_W: G::Scalar,
66 nifs_ip: NIFSForInnerProduct<G>,
67 ipa: InnerProductArgument<G>,
68}
69
70impl<G: Group> RelaxedR1CSSNARKTrait<G> for RelaxedR1CSSNARK<G> {
71 type ProverKey = ProverKey<G>;
72 type VerifierKey = VerifierKey<G>;
73
74 /// produces a succinct proof of satisfiability of a RelaxedR1CS instance
75 fn prove(
76 pk: &Self::ProverKey,
77 U: &RelaxedR1CSInstance<G>,
78 W: &RelaxedR1CSWitness<G>,
79 ) -> Result<Self, NovaError> {
80 let mut transcript = Transcript::new(b"RelaxedR1CSSNARK");
81
82 debug_assert!(pk.S.is_sat_relaxed(&pk.gens_r1cs, U, W).is_ok());
83
84 // sanity check that R1CSShape has certain size characteristics
85 assert_eq!(pk.S.num_cons.next_power_of_two(), pk.S.num_cons);
86 assert_eq!(pk.S.num_vars.next_power_of_two(), pk.S.num_vars);
87 assert_eq!(pk.S.num_io.next_power_of_two(), pk.S.num_io);
88 assert!(pk.S.num_io < pk.S.num_vars);
89
90 // append the R1CSShape and RelaxedR1CSInstance to the transcript
91 pk.S.append_to_transcript(b"S", &mut transcript);
92 U.append_to_transcript(b"U", &mut transcript);
93
94 // compute the full satisfying assignment by concatenating W.W, U.u, and U.X
95 let mut z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
96
97 let (num_rounds_x, num_rounds_y) = (
98 (pk.S.num_cons as f64).log2() as usize,
99 ((pk.S.num_vars as f64).log2() as usize + 1) as usize,
100 );
101
102 // outer sum-check
103 let tau = (0..num_rounds_x)
104 .map(|_i| G::Scalar::challenge(b"challenge_tau", &mut transcript))
105 .collect();
106
107 let mut poly_tau = MultilinearPolynomial::new(EqPolynomial::new(tau).evals());
108 let (mut poly_Az, mut poly_Bz, poly_Cz, mut poly_uCz_E) = {
109 let (poly_Az, poly_Bz, poly_Cz) = pk.S.multiply_vec(&z)?;
110 let poly_uCz_E = (0..pk.S.num_cons)
111 .map(|i| U.u * poly_Cz[i] + W.E[i])
112 .collect::<Vec<G::Scalar>>();
113 (
114 MultilinearPolynomial::new(poly_Az),
115 MultilinearPolynomial::new(poly_Bz),
116 MultilinearPolynomial::new(poly_Cz),
117 MultilinearPolynomial::new(poly_uCz_E),
118 )
119 };
120
121 let comb_func_outer =
122 |poly_A_comp: &G::Scalar,
123 poly_B_comp: &G::Scalar,
124 poly_C_comp: &G::Scalar,
125 poly_D_comp: &G::Scalar|
126 -> G::Scalar { *poly_A_comp * (*poly_B_comp * *poly_C_comp - *poly_D_comp) };
127 let (sc_proof_outer, r_x, claims_outer) = SumcheckProof::prove_cubic_with_additive_term(
128 &G::Scalar::zero(), // claim is zero
129 num_rounds_x,
130 &mut poly_tau,
131 &mut poly_Az,
132 &mut poly_Bz,
133 &mut poly_uCz_E,
134 comb_func_outer,
135 &mut transcript,
136 );
137
138 // claims from the end of sum-check
139 let (claim_Az, claim_Bz): (G::Scalar, G::Scalar) = (claims_outer[1], claims_outer[2]);
140
141 claim_Az.append_to_transcript(b"claim_Az", &mut transcript);
142 claim_Bz.append_to_transcript(b"claim_Bz", &mut transcript);
143 let claim_Cz = poly_Cz.evaluate(&r_x);
144 let eval_E = MultilinearPolynomial::new(W.E.clone()).evaluate(&r_x);
145 claim_Cz.append_to_transcript(b"claim_Cz", &mut transcript);
146 eval_E.append_to_transcript(b"eval_E", &mut transcript);
147
148 // inner sum-check
149 let r_A = G::Scalar::challenge(b"challenge_rA", &mut transcript);
150 let r_B = G::Scalar::challenge(b"challenge_rB", &mut transcript);
151 let r_C = G::Scalar::challenge(b"challenge_rC", &mut transcript);
152 let claim_inner_joint = r_A * claim_Az + r_B * claim_Bz + r_C * claim_Cz;
153
154 let poly_ABC = {
155 // compute the initial evaluation table for R(\tau, x)
156 let evals_rx = EqPolynomial::new(r_x.clone()).evals();
157
158 // Bounds "row" variables of (A, B, C) matrices viewed as 2d multilinear polynomials
159 let compute_eval_table_sparse =
160 |S: &R1CSShape<G>, rx: &[G::Scalar]| -> (Vec<G::Scalar>, Vec<G::Scalar>, Vec<G::Scalar>) {
161 assert_eq!(rx.len(), S.num_cons);
162
163 let inner = |M: &Vec<(usize, usize, G::Scalar)>, M_evals: &mut Vec<G::Scalar>| {
164 for (row, col, val) in M {
165 M_evals[*col] += rx[*row] * val;
166 }
167 };
168
169 let (A_evals, (B_evals, C_evals)) = rayon::join(
170 || {
171 let mut A_evals: Vec<G::Scalar> = vec![G::Scalar::zero(); 2 * S.num_vars];
172 inner(&S.A, &mut A_evals);
173 A_evals
174 },
175 || {
176 rayon::join(
177 || {
178 let mut B_evals: Vec<G::Scalar> = vec![G::Scalar::zero(); 2 * S.num_vars];
179 inner(&S.B, &mut B_evals);
180 B_evals
181 },
182 || {
183 let mut C_evals: Vec<G::Scalar> = vec![G::Scalar::zero(); 2 * S.num_vars];
184 inner(&S.C, &mut C_evals);
185 C_evals
186 },
187 )
188 },
189 );
190
191 (A_evals, B_evals, C_evals)
192 };
193
194 let (evals_A, evals_B, evals_C) = compute_eval_table_sparse(&pk.S, &evals_rx);
195
196 assert_eq!(evals_A.len(), evals_B.len());
197 assert_eq!(evals_A.len(), evals_C.len());
198 (0..evals_A.len())
199 .into_par_iter()
200 .map(|i| r_A * evals_A[i] + r_B * evals_B[i] + r_C * evals_C[i])
201 .collect::<Vec<G::Scalar>>()
202 };
203
204 let poly_z = {
205 z.resize(pk.S.num_vars * 2, G::Scalar::zero());
206 z
207 };
208
209 let comb_func = |poly_A_comp: &G::Scalar, poly_B_comp: &G::Scalar| -> G::Scalar {
210 *poly_A_comp * *poly_B_comp
211 };
212 let (sc_proof_inner, r_y, _claims_inner) = SumcheckProof::prove_quad(
213 &claim_inner_joint,
214 num_rounds_y,
215 &mut MultilinearPolynomial::new(poly_ABC),
216 &mut MultilinearPolynomial::new(poly_z),
217 comb_func,
218 &mut transcript,
219 );
220
221 let eval_W = MultilinearPolynomial::new(W.W.clone()).evaluate(&r_y[1..]);
222 eval_W.append_to_transcript(b"eval_W", &mut transcript);
223
224 let (nifs_ip, r_U, r_W) = NIFSForInnerProduct::prove(
225 &InnerProductInstance::new(&U.comm_E, &EqPolynomial::new(r_x).evals(), &eval_E),
226 &InnerProductWitness::new(&W.E),
227 &InnerProductInstance::new(
228 &U.comm_W,
229 &EqPolynomial::new(r_y[1..].to_vec()).evals(),
230 &eval_W,
231 ),
232 &InnerProductWitness::new(&W.W),
233 &mut transcript,
234 );
235
236 let ipa = InnerProductArgument::prove(
237 &pk.gens_r1cs.gens,
238 &pk.gens_ipa,
239 &r_U,
240 &r_W,
241 &mut transcript,
242 )?;
243
244 Ok(RelaxedR1CSSNARK {
245 sc_proof_outer,
246 claims_outer: (claim_Az, claim_Bz, claim_Cz),
247 sc_proof_inner,
248 eval_W,
249 eval_E,
250 nifs_ip,
251 ipa,
252 })
253 }
254
255 /// verifies a proof of satisfiability of a RelaxedR1CS instance
256 fn verify(&self, vk: &Self::VerifierKey, U: &RelaxedR1CSInstance<G>) -> Result<(), NovaError> {
257 let mut transcript = Transcript::new(b"RelaxedR1CSSNARK");
258
259 // append the R1CSShape and RelaxedR1CSInstance to the transcript
260 vk.S.append_to_transcript(b"S", &mut transcript);
261 U.append_to_transcript(b"U", &mut transcript);
262
263 let (num_rounds_x, num_rounds_y) = (
264 (vk.S.num_cons as f64).log2() as usize,
265 ((vk.S.num_vars as f64).log2() as usize + 1) as usize,
266 );
267
268 // outer sum-check
269 let tau = (0..num_rounds_x)
270 .map(|_i| G::Scalar::challenge(b"challenge_tau", &mut transcript))
271 .collect::<Vec<G::Scalar>>();
272
273 let (claim_outer_final, r_x) =
274 self
275 .sc_proof_outer
276 .verify(G::Scalar::zero(), num_rounds_x, 3, &mut transcript)?;
277
278 // verify claim_outer_final
279 let (claim_Az, claim_Bz, claim_Cz) = self.claims_outer;
280 let taus_bound_rx = EqPolynomial::new(tau).evaluate(&r_x);
281 let claim_outer_final_expected =
282 taus_bound_rx * (claim_Az * claim_Bz - U.u * claim_Cz - self.eval_E);
283 if claim_outer_final != claim_outer_final_expected {
284 return Err(NovaError::InvalidSumcheckProof);
285 }
286
287 self
288 .claims_outer
289 .0
290 .append_to_transcript(b"claim_Az", &mut transcript);
291 self
292 .claims_outer
293 .1
294 .append_to_transcript(b"claim_Bz", &mut transcript);
295 self
296 .claims_outer
297 .2
298 .append_to_transcript(b"claim_Cz", &mut transcript);
299 self.eval_E.append_to_transcript(b"eval_E", &mut transcript);
300
301 // inner sum-check
302 let r_A = G::Scalar::challenge(b"challenge_rA", &mut transcript);
303 let r_B = G::Scalar::challenge(b"challenge_rB", &mut transcript);
304 let r_C = G::Scalar::challenge(b"challenge_rC", &mut transcript);
305 let claim_inner_joint =
306 r_A * self.claims_outer.0 + r_B * self.claims_outer.1 + r_C * self.claims_outer.2;
307
308 let (claim_inner_final, r_y) =
309 self
310 .sc_proof_inner
311 .verify(claim_inner_joint, num_rounds_y, 2, &mut transcript)?;
312
313 // verify claim_inner_final
314 let eval_Z = {
315 let eval_X = {
316 // constant term
317 let mut poly_X = vec![(0, U.u)];
318 //remaining inputs
319 poly_X.extend(
320 (0..U.X.len())
321 .map(|i| (i + 1, U.X[i]))
322 .collect::<Vec<(usize, G::Scalar)>>(),
323 );
324 SparsePolynomial::new((vk.S.num_vars as f64).log2() as usize, poly_X)
325 .evaluate(&r_y[1..].to_vec())
326 };
327 (G::Scalar::one() - r_y[0]) * self.eval_W + r_y[0] * eval_X
328 };
329
330 let evaluate_as_sparse_polynomial = |S: &R1CSShape<G>,
331 r_x: &[G::Scalar],
332 r_y: &[G::Scalar]|
333 -> (G::Scalar, G::Scalar, G::Scalar) {
334 let evaluate_with_table =
335 |M: &[(usize, usize, G::Scalar)], T_x: &[G::Scalar], T_y: &[G::Scalar]| -> G::Scalar {
336 (0..M.len())
337 .map(|i| {
338 let (row, col, val) = M[i];
339 T_x[row] * T_y[col] * val
340 })
341 .fold(G::Scalar::zero(), |acc, x| acc + x)
342 };
343
344 let T_x = EqPolynomial::new(r_x.to_vec()).evals();
345 let T_y = EqPolynomial::new(r_y.to_vec()).evals();
346 let eval_A_r = evaluate_with_table(&S.A, &T_x, &T_y);
347 let eval_B_r = evaluate_with_table(&S.B, &T_x, &T_y);
348 let eval_C_r = evaluate_with_table(&S.C, &T_x, &T_y);
349 (eval_A_r, eval_B_r, eval_C_r)
350 };
351
352 let (eval_A_r, eval_B_r, eval_C_r) = evaluate_as_sparse_polynomial(&vk.S, &r_x, &r_y);
353 let claim_inner_final_expected = (r_A * eval_A_r + r_B * eval_B_r + r_C * eval_C_r) * eval_Z;
354 if claim_inner_final != claim_inner_final_expected {
355 return Err(NovaError::InvalidSumcheckProof);
356 }
357
358 // verify eval_W and eval_E
359 self.eval_W.append_to_transcript(b"eval_W", &mut transcript); //eval_E is already in the transcript
360
361 let r_U = self.nifs_ip.verify(
362 &InnerProductInstance::new(&U.comm_E, &EqPolynomial::new(r_x).evals(), &self.eval_E),
363 &InnerProductInstance::new(
364 &U.comm_W,
365 &EqPolynomial::new(r_y[1..].to_vec()).evals(),
366 &self.eval_W,
367 ),
368 &mut transcript,
369 );
370
371 self.ipa.verify(
372 &vk.gens_r1cs.gens,
373 &vk.gens_ipa,
374 max(vk.S.num_vars, vk.S.num_cons),
375 &r_U,
376 &mut transcript,
377 )?;
378
379 Ok(())
380 }
381}