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