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