Nova/src/lib.rs
src/lib.rsRaw
1//! This library implements Nova, a high-speed recursive SNARK.
2#![allow(non_snake_case)]
3#![allow(clippy::type_complexity)]
4#![deny(missing_docs)]
5
6// private modules
7mod bellperson;
8mod circuit;
9mod commitments;
10mod constants;
11mod nifs;
12mod poseidon;
13mod r1cs;
14
15// public modules
16pub mod errors;
17pub mod gadgets;
18pub mod pasta;
19pub mod snark;
20pub mod spartan_with_ipa_pc;
21pub mod traits;
22
23use crate::bellperson::{
24 r1cs::{NovaShape, NovaWitness},
25 shape_cs::ShapeCS,
26 solver::SatisfyingAssignment,
27};
28use ::bellperson::{Circuit, ConstraintSystem};
29use circuit::{NIFSVerifierCircuit, NIFSVerifierCircuitInputs, NIFSVerifierCircuitParams};
30use constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
31use core::marker::PhantomData;
32use errors::NovaError;
33use ff::Field;
34use gadgets::utils::scalar_as_base;
35use nifs::NIFS;
36use r1cs::{
37 R1CSGens, R1CSInstance, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness,
38};
39use snark::RelaxedR1CSSNARKTrait;
40use traits::{
41 AbsorbInROTrait, Group, HashFuncConstants, HashFuncConstantsCircuit, HashFuncConstantsTrait,
42 HashFuncTrait, StepCircuit,
43};
44
45/// A type that holds public parameters of Nova
46pub struct PublicParams<G1, G2, C1, C2>
47where
48 G1: Group<Base = <G2 as Group>::Scalar>,
49 G2: Group<Base = <G1 as Group>::Scalar>,
50 C1: StepCircuit<G1::Scalar>,
51 C2: StepCircuit<G2::Scalar>,
52{
53 ro_consts_primary: HashFuncConstants<G1>,
54 ro_consts_circuit_primary: HashFuncConstantsCircuit<G2>,
55 r1cs_gens_primary: R1CSGens<G1>,
56 r1cs_shape_primary: R1CSShape<G1>,
57 r1cs_shape_padded_primary: R1CSShape<G1>,
58 ro_consts_secondary: HashFuncConstants<G2>,
59 ro_consts_circuit_secondary: HashFuncConstantsCircuit<G1>,
60 r1cs_gens_secondary: R1CSGens<G2>,
61 r1cs_shape_secondary: R1CSShape<G2>,
62 r1cs_shape_padded_secondary: R1CSShape<G2>,
63 c_primary: C1,
64 c_secondary: C2,
65 params_primary: NIFSVerifierCircuitParams,
66 params_secondary: NIFSVerifierCircuitParams,
67}
68
69impl<G1, G2, C1, C2> PublicParams<G1, G2, C1, C2>
70where
71 G1: Group<Base = <G2 as Group>::Scalar>,
72 G2: Group<Base = <G1 as Group>::Scalar>,
73 C1: StepCircuit<G1::Scalar>,
74 C2: StepCircuit<G2::Scalar>,
75{
76 /// Create a new `PublicParams`
77 pub fn setup(c_primary: C1, c_secondary: C2) -> Self {
78 let params_primary = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
79 let params_secondary = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false);
80
81 let ro_consts_primary: HashFuncConstants<G1> = HashFuncConstants::<G1>::new();
82 let ro_consts_secondary: HashFuncConstants<G2> = HashFuncConstants::<G2>::new();
83
84 // ro_consts_circuit_primart are parameterized by G2 because the type alias uses G2::Base = G1::Scalar
85 let ro_consts_circuit_primary: HashFuncConstantsCircuit<G2> =
86 HashFuncConstantsCircuit::<G2>::new();
87 let ro_consts_circuit_secondary: HashFuncConstantsCircuit<G1> =
88 HashFuncConstantsCircuit::<G1>::new();
89
90 // Initialize gens for the primary
91 let circuit_primary: NIFSVerifierCircuit<G2, C1> = NIFSVerifierCircuit::new(
92 params_primary.clone(),
93 None,
94 c_primary.clone(),
95 ro_consts_circuit_primary.clone(),
96 );
97 let mut cs: ShapeCS<G1> = ShapeCS::new();
98 let _ = circuit_primary.synthesize(&mut cs);
99 let (r1cs_shape_primary, r1cs_gens_primary) = (cs.r1cs_shape(), cs.r1cs_gens());
100 let r1cs_shape_padded_primary = r1cs_shape_primary.pad();
101
102 // Initialize gens for the secondary
103 let circuit_secondary: NIFSVerifierCircuit<G1, C2> = NIFSVerifierCircuit::new(
104 params_secondary.clone(),
105 None,
106 c_secondary.clone(),
107 ro_consts_circuit_secondary.clone(),
108 );
109 let mut cs: ShapeCS<G2> = ShapeCS::new();
110 let _ = circuit_secondary.synthesize(&mut cs);
111 let (r1cs_shape_secondary, r1cs_gens_secondary) = (cs.r1cs_shape(), cs.r1cs_gens());
112 let r1cs_shape_padded_secondary = r1cs_shape_secondary.pad();
113
114 Self {
115 ro_consts_primary,
116 ro_consts_circuit_primary,
117 r1cs_gens_primary,
118 r1cs_shape_primary,
119 r1cs_shape_padded_primary,
120 ro_consts_secondary,
121 ro_consts_circuit_secondary,
122 r1cs_gens_secondary,
123 r1cs_shape_secondary,
124 r1cs_shape_padded_secondary,
125 c_primary,
126 c_secondary,
127 params_primary,
128 params_secondary,
129 }
130 }
131}
132
133/// A SNARK that proves the correct execution of an incremental computation
134pub struct RecursiveSNARK<G1, G2, C1, C2>
135where
136 G1: Group<Base = <G2 as Group>::Scalar>,
137 G2: Group<Base = <G1 as Group>::Scalar>,
138 C1: StepCircuit<G1::Scalar>,
139 C2: StepCircuit<G2::Scalar>,
140{
141 r_W_primary: RelaxedR1CSWitness<G1>,
142 r_U_primary: RelaxedR1CSInstance<G1>,
143 l_w_primary: R1CSWitness<G1>,
144 l_u_primary: R1CSInstance<G1>,
145 r_W_secondary: RelaxedR1CSWitness<G2>,
146 r_U_secondary: RelaxedR1CSInstance<G2>,
147 l_w_secondary: R1CSWitness<G2>,
148 l_u_secondary: R1CSInstance<G2>,
149 zn_primary: G1::Scalar,
150 zn_secondary: G2::Scalar,
151 _p_c1: PhantomData<C1>,
152 _p_c2: PhantomData<C2>,
153}
154
155impl<G1, G2, C1, C2> RecursiveSNARK<G1, G2, C1, C2>
156where
157 G1: Group<Base = <G2 as Group>::Scalar>,
158 G2: Group<Base = <G1 as Group>::Scalar>,
159 C1: StepCircuit<G1::Scalar>,
160 C2: StepCircuit<G2::Scalar>,
161{
162 /// Create a new `RecursiveSNARK`
163 pub fn prove(
164 pp: &PublicParams<G1, G2, C1, C2>,
165 num_steps: usize,
166 z0_primary: G1::Scalar,
167 z0_secondary: G2::Scalar,
168 ) -> Result<Self, NovaError> {
169 if num_steps == 0 {
170 return Err(NovaError::InvalidNumSteps);
171 }
172
173 // Execute the base case for the primary
174 let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
175 let inputs_primary: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
176 pp.r1cs_shape_secondary.get_digest(),
177 G1::Scalar::zero(),
178 z0_primary,
179 None,
180 None,
181 None,
182 None,
183 );
184 let circuit_primary: NIFSVerifierCircuit<G2, C1> = NIFSVerifierCircuit::new(
185 pp.params_primary.clone(),
186 Some(inputs_primary),
187 pp.c_primary.clone(),
188 pp.ro_consts_circuit_primary.clone(),
189 );
190 let _ = circuit_primary.synthesize(&mut cs_primary);
191 let (u_primary, w_primary) = cs_primary
192 .r1cs_instance_and_witness(&pp.r1cs_shape_primary, &pp.r1cs_gens_primary)
193 .map_err(|_e| NovaError::UnSat)?;
194
195 // Execute the base case for the secondary
196 let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
197 let inputs_secondary: NIFSVerifierCircuitInputs<G1> = NIFSVerifierCircuitInputs::new(
198 pp.r1cs_shape_primary.get_digest(),
199 G2::Scalar::zero(),
200 z0_secondary,
201 None,
202 None,
203 Some(u_primary.clone()),
204 None,
205 );
206 let circuit_secondary: NIFSVerifierCircuit<G1, C2> = NIFSVerifierCircuit::new(
207 pp.params_secondary.clone(),
208 Some(inputs_secondary),
209 pp.c_secondary.clone(),
210 pp.ro_consts_circuit_secondary.clone(),
211 );
212 let _ = circuit_secondary.synthesize(&mut cs_secondary);
213 let (u_secondary, w_secondary) = cs_secondary
214 .r1cs_instance_and_witness(&pp.r1cs_shape_secondary, &pp.r1cs_gens_secondary)
215 .map_err(|_e| NovaError::UnSat)?;
216
217 // execute the remaining steps, alternating between G1 and G2
218 let mut l_w_primary = w_primary;
219 let mut l_u_primary = u_primary;
220 let mut r_W_primary =
221 RelaxedR1CSWitness::from_r1cs_witness(&pp.r1cs_shape_primary, &l_w_primary);
222 let mut r_U_primary = RelaxedR1CSInstance::from_r1cs_instance(
223 &pp.r1cs_gens_primary,
224 &pp.r1cs_shape_primary,
225 &l_u_primary,
226 );
227
228 let mut r_W_secondary = RelaxedR1CSWitness::<G2>::default(&pp.r1cs_shape_secondary);
229 let mut r_U_secondary =
230 RelaxedR1CSInstance::<G2>::default(&pp.r1cs_gens_secondary, &pp.r1cs_shape_secondary);
231 let mut l_w_secondary = w_secondary;
232 let mut l_u_secondary = u_secondary;
233
234 let mut z_next_primary = z0_primary;
235 let mut z_next_secondary = z0_secondary;
236 z_next_primary = pp.c_primary.compute(&z_next_primary);
237 z_next_secondary = pp.c_secondary.compute(&z_next_secondary);
238
239 for i in 1..num_steps {
240 // fold the secondary circuit's instance
241 let (nifs_secondary, (r_U_next_secondary, r_W_next_secondary)) = NIFS::prove(
242 &pp.r1cs_gens_secondary,
243 &pp.ro_consts_secondary,
244 &pp.r1cs_shape_secondary,
245 &r_U_secondary,
246 &r_W_secondary,
247 &l_u_secondary,
248 &l_w_secondary,
249 )?;
250
251 let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
252 let inputs_primary: NIFSVerifierCircuitInputs<G2> = NIFSVerifierCircuitInputs::new(
253 pp.r1cs_shape_secondary.get_digest(),
254 G1::Scalar::from(i as u64),
255 z0_primary,
256 Some(z_next_primary),
257 Some(r_U_secondary),
258 Some(l_u_secondary),
259 Some(nifs_secondary.comm_T.decompress()?),
260 );
261
262 let circuit_primary: NIFSVerifierCircuit<G2, C1> = NIFSVerifierCircuit::new(
263 pp.params_primary.clone(),
264 Some(inputs_primary),
265 pp.c_primary.clone(),
266 pp.ro_consts_circuit_primary.clone(),
267 );
268 let _ = circuit_primary.synthesize(&mut cs_primary);
269
270 (l_u_primary, l_w_primary) = cs_primary
271 .r1cs_instance_and_witness(&pp.r1cs_shape_primary, &pp.r1cs_gens_primary)
272 .map_err(|_e| NovaError::UnSat)?;
273
274 // fold the primary circuit's instance
275 let (nifs_primary, (r_U_next_primary, r_W_next_primary)) = NIFS::prove(
276 &pp.r1cs_gens_primary,
277 &pp.ro_consts_primary,
278 &pp.r1cs_shape_primary,
279 &r_U_primary.clone(),
280 &r_W_primary.clone(),
281 &l_u_primary.clone(),
282 &l_w_primary.clone(),
283 )?;
284
285 let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
286 let inputs_secondary: NIFSVerifierCircuitInputs<G1> = NIFSVerifierCircuitInputs::new(
287 pp.r1cs_shape_primary.get_digest(),
288 G2::Scalar::from(i as u64),
289 z0_secondary,
290 Some(z_next_secondary),
291 Some(r_U_primary.clone()),
292 Some(l_u_primary.clone()),
293 Some(nifs_primary.comm_T.decompress()?),
294 );
295
296 let circuit_secondary: NIFSVerifierCircuit<G1, C2> = NIFSVerifierCircuit::new(
297 pp.params_secondary.clone(),
298 Some(inputs_secondary),
299 pp.c_secondary.clone(),
300 pp.ro_consts_circuit_secondary.clone(),
301 );
302 let _ = circuit_secondary.synthesize(&mut cs_secondary);
303
304 (l_u_secondary, l_w_secondary) = cs_secondary
305 .r1cs_instance_and_witness(&pp.r1cs_shape_secondary, &pp.r1cs_gens_secondary)
306 .map_err(|_e| NovaError::UnSat)?;
307
308 // update the running instances and witnesses
309 r_U_secondary = r_U_next_secondary;
310 r_W_secondary = r_W_next_secondary;
311 r_U_primary = r_U_next_primary;
312 r_W_primary = r_W_next_primary;
313 z_next_primary = pp.c_primary.compute(&z_next_primary);
314 z_next_secondary = pp.c_secondary.compute(&z_next_secondary);
315 }
316
317 Ok(Self {
318 r_W_primary,
319 r_U_primary,
320 l_w_primary,
321 l_u_primary,
322 r_W_secondary,
323 r_U_secondary,
324 l_w_secondary,
325 l_u_secondary,
326 zn_primary: z_next_primary,
327 zn_secondary: z_next_secondary,
328 _p_c1: Default::default(),
329 _p_c2: Default::default(),
330 })
331 }
332
333 /// Verify the correctness of the `RecursiveSNARK`
334 pub fn verify(
335 &self,
336 pp: &PublicParams<G1, G2, C1, C2>,
337 num_steps: usize,
338 z0_primary: G1::Scalar,
339 z0_secondary: G2::Scalar,
340 ) -> Result<(G1::Scalar, G2::Scalar), NovaError> {
341 // number of steps cannot be zero
342 if num_steps == 0 {
343 return Err(NovaError::ProofVerifyError);
344 }
345
346 // check if the (relaxed) R1CS instances have two public outputs
347 if self.l_u_primary.X.len() != 2
348 || self.l_u_secondary.X.len() != 2
349 || self.r_U_primary.X.len() != 2
350 || self.r_U_secondary.X.len() != 2
351 {
352 return Err(NovaError::ProofVerifyError);
353 }
354
355 // check if the output hashes in R1CS instances point to the right running instances
356 let (hash_primary, hash_secondary) = {
357 let mut hasher = <G2 as Group>::HashFunc::new(pp.ro_consts_secondary.clone());
358 hasher.absorb(scalar_as_base::<G2>(pp.r1cs_shape_secondary.get_digest()));
359 hasher.absorb(G1::Scalar::from(num_steps as u64));
360 hasher.absorb(z0_primary);
361 hasher.absorb(self.zn_primary);
362 self.r_U_secondary.absorb_in_ro(&mut hasher);
363
364 let mut hasher2 = <G1 as Group>::HashFunc::new(pp.ro_consts_primary.clone());
365 hasher2.absorb(scalar_as_base::<G1>(pp.r1cs_shape_primary.get_digest()));
366 hasher2.absorb(G2::Scalar::from(num_steps as u64));
367 hasher2.absorb(z0_secondary);
368 hasher2.absorb(self.zn_secondary);
369 self.r_U_primary.absorb_in_ro(&mut hasher2);
370
371 (hasher.get_hash(), hasher2.get_hash())
372 };
373
374 if hash_primary != scalar_as_base::<G1>(self.l_u_primary.X[1])
375 || hash_secondary != scalar_as_base::<G2>(self.l_u_secondary.X[1])
376 {
377 return Err(NovaError::ProofVerifyError);
378 }
379
380 // check the satisfiability of the provided instances
381 let ((res_r_primary, res_l_primary), (res_r_secondary, res_l_secondary)) = rayon::join(
382 || {
383 rayon::join(
384 || {
385 pp.r1cs_shape_primary.is_sat_relaxed(
386 &pp.r1cs_gens_primary,
387 &self.r_U_primary,
388 &self.r_W_primary,
389 )
390 },
391 || {
392 pp.r1cs_shape_primary.is_sat(
393 &pp.r1cs_gens_primary,
394 &self.l_u_primary,
395 &self.l_w_primary,
396 )
397 },
398 )
399 },
400 || {
401 rayon::join(
402 || {
403 pp.r1cs_shape_secondary.is_sat_relaxed(
404 &pp.r1cs_gens_secondary,
405 &self.r_U_secondary,
406 &self.r_W_secondary,
407 )
408 },
409 || {
410 pp.r1cs_shape_secondary.is_sat(
411 &pp.r1cs_gens_secondary,
412 &self.l_u_secondary,
413 &self.l_w_secondary,
414 )
415 },
416 )
417 },
418 );
419
420 // check the returned res objects
421 res_r_primary?;
422 res_l_primary?;
423 res_r_secondary?;
424 res_l_secondary?;
425
426 Ok((self.zn_primary, self.zn_secondary))
427 }
428}
429
430/// A SNARK that proves the knowledge of a valid `RecursiveSNARK`
431pub struct CompressedSNARK<G1, G2, C1, C2, S1, S2>
432where
433 G1: Group<Base = <G2 as Group>::Scalar>,
434 G2: Group<Base = <G1 as Group>::Scalar>,
435 C1: StepCircuit<G1::Scalar>,
436 C2: StepCircuit<G2::Scalar>,
437 S1: RelaxedR1CSSNARKTrait<G1>,
438 S2: RelaxedR1CSSNARKTrait<G2>,
439{
440 r_U_primary: RelaxedR1CSInstance<G1>,
441 l_u_primary: R1CSInstance<G1>,
442 nifs_primary: NIFS<G1>,
443 f_W_snark_primary: S1,
444
445 r_U_secondary: RelaxedR1CSInstance<G2>,
446 l_u_secondary: R1CSInstance<G2>,
447 nifs_secondary: NIFS<G2>,
448 f_W_snark_secondary: S2,
449
450 zn_primary: G1::Scalar,
451 zn_secondary: G2::Scalar,
452
453 _p_c1: PhantomData<C1>,
454 _p_c2: PhantomData<C2>,
455}
456
457impl<G1, G2, C1, C2, S1, S2> CompressedSNARK<G1, G2, C1, C2, S1, S2>
458where
459 G1: Group<Base = <G2 as Group>::Scalar>,
460 G2: Group<Base = <G1 as Group>::Scalar>,
461 C1: StepCircuit<G1::Scalar>,
462 C2: StepCircuit<G2::Scalar>,
463 S1: RelaxedR1CSSNARKTrait<G1>,
464 S2: RelaxedR1CSSNARKTrait<G2>,
465{
466 /// Create a new `CompressedSNARK`
467 pub fn prove(
468 pp: &PublicParams<G1, G2, C1, C2>,
469 recursive_snark: &RecursiveSNARK<G1, G2, C1, C2>,
470 ) -> Result<Self, NovaError> {
471 let (res_primary, res_secondary) = rayon::join(
472 // fold the primary circuit's instance
473 || {
474 NIFS::prove(
475 &pp.r1cs_gens_primary,
476 &pp.ro_consts_primary,
477 &pp.r1cs_shape_primary,
478 &recursive_snark.r_U_primary,
479 &recursive_snark.r_W_primary,
480 &recursive_snark.l_u_primary,
481 &recursive_snark.l_w_primary,
482 )
483 },
484 || {
485 // fold the secondary circuit's instance
486 NIFS::prove(
487 &pp.r1cs_gens_secondary,
488 &pp.ro_consts_secondary,
489 &pp.r1cs_shape_secondary,
490 &recursive_snark.r_U_secondary,
491 &recursive_snark.r_W_secondary,
492 &recursive_snark.l_u_secondary,
493 &recursive_snark.l_w_secondary,
494 )
495 },
496 );
497
498 let (nifs_primary, (f_U_primary, f_W_primary)) = res_primary?;
499 let (nifs_secondary, (f_U_secondary, f_W_secondary)) = res_secondary?;
500
501 // produce a prover key for the SNARK
502 let (pk_primary, pk_secondary) = rayon::join(
503 || S1::prover_key(&pp.r1cs_gens_primary, &pp.r1cs_shape_padded_primary),
504 || S2::prover_key(&pp.r1cs_gens_secondary, &pp.r1cs_shape_padded_secondary),
505 );
506
507 // create SNARKs proving the knowledge of f_W_primary and f_W_secondary
508 let (f_W_snark_primary, f_W_snark_secondary) = rayon::join(
509 || {
510 S1::prove(
511 &pk_primary,
512 &f_U_primary,
513 &f_W_primary.pad(&pp.r1cs_shape_padded_primary), // pad the witness since shape was padded
514 )
515 },
516 || {
517 S2::prove(
518 &pk_secondary,
519 &f_U_secondary,
520 &f_W_secondary.pad(&pp.r1cs_shape_padded_secondary), // pad the witness since the shape was padded
521 )
522 },
523 );
524
525 Ok(Self {
526 r_U_primary: recursive_snark.r_U_primary.clone(),
527 l_u_primary: recursive_snark.l_u_primary.clone(),
528 nifs_primary,
529 f_W_snark_primary: f_W_snark_primary?,
530
531 r_U_secondary: recursive_snark.r_U_secondary.clone(),
532 l_u_secondary: recursive_snark.l_u_secondary.clone(),
533 nifs_secondary,
534 f_W_snark_secondary: f_W_snark_secondary?,
535
536 zn_primary: recursive_snark.zn_primary,
537 zn_secondary: recursive_snark.zn_secondary,
538
539 _p_c1: Default::default(),
540 _p_c2: Default::default(),
541 })
542 }
543
544 /// Verify the correctness of the `CompressedSNARK`
545 pub fn verify(
546 &self,
547 pp: &PublicParams<G1, G2, C1, C2>,
548 num_steps: usize,
549 z0_primary: G1::Scalar,
550 z0_secondary: G2::Scalar,
551 ) -> Result<(G1::Scalar, G2::Scalar), NovaError> {
552 // number of steps cannot be zero
553 if num_steps == 0 {
554 return Err(NovaError::ProofVerifyError);
555 }
556
557 // check if the (relaxed) R1CS instances have two public outputs
558 if self.l_u_primary.X.len() != 2
559 || self.l_u_secondary.X.len() != 2
560 || self.r_U_primary.X.len() != 2
561 || self.r_U_secondary.X.len() != 2
562 {
563 return Err(NovaError::ProofVerifyError);
564 }
565
566 // check if the output hashes in R1CS instances point to the right running instances
567 let (hash_primary, hash_secondary) = {
568 let mut hasher = <G2 as Group>::HashFunc::new(pp.ro_consts_secondary.clone());
569 hasher.absorb(scalar_as_base::<G2>(pp.r1cs_shape_secondary.get_digest()));
570 hasher.absorb(G1::Scalar::from(num_steps as u64));
571 hasher.absorb(z0_primary);
572 hasher.absorb(self.zn_primary);
573 self.r_U_secondary.absorb_in_ro(&mut hasher);
574
575 let mut hasher2 = <G1 as Group>::HashFunc::new(pp.ro_consts_primary.clone());
576 hasher2.absorb(scalar_as_base::<G1>(pp.r1cs_shape_primary.get_digest()));
577 hasher2.absorb(G2::Scalar::from(num_steps as u64));
578 hasher2.absorb(z0_secondary);
579 hasher2.absorb(self.zn_secondary);
580 self.r_U_primary.absorb_in_ro(&mut hasher2);
581
582 (hasher.get_hash(), hasher2.get_hash())
583 };
584
585 if hash_primary != scalar_as_base::<G1>(self.l_u_primary.X[1])
586 || hash_secondary != scalar_as_base::<G2>(self.l_u_secondary.X[1])
587 {
588 return Err(NovaError::ProofVerifyError);
589 }
590
591 // fold the running instance and last instance to get a folded instance
592 let f_U_primary = self.nifs_primary.verify(
593 &pp.ro_consts_primary,
594 &pp.r1cs_shape_primary,
595 &self.r_U_primary,
596 &self.l_u_primary,
597 )?;
598 let f_U_secondary = self.nifs_secondary.verify(
599 &pp.ro_consts_secondary,
600 &pp.r1cs_shape_secondary,
601 &self.r_U_secondary,
602 &self.l_u_secondary,
603 )?;
604
605 // produce a verifier key for the SNARK
606 let (vk_primary, vk_secondary) = rayon::join(
607 || S1::verifier_key(&pp.r1cs_gens_primary, &pp.r1cs_shape_padded_primary),
608 || S2::verifier_key(&pp.r1cs_gens_secondary, &pp.r1cs_shape_padded_secondary),
609 );
610
611 // check the satisfiability of the folded instances using SNARKs proving the knowledge of their satisfying witnesses
612 let (res_primary, res_secondary) = rayon::join(
613 || self.f_W_snark_primary.verify(&vk_primary, &f_U_primary),
614 || {
615 self
616 .f_W_snark_secondary
617 .verify(&vk_secondary, &f_U_secondary)
618 },
619 );
620
621 res_primary?;
622 res_secondary?;
623
624 Ok((self.zn_primary, self.zn_secondary))
625 }
626}
627
628#[cfg(test)]
629mod tests {
630 use super::*;
631 type G1 = pasta_curves::pallas::Point;
632 type G2 = pasta_curves::vesta::Point;
633 type S1 = spartan_with_ipa_pc::RelaxedR1CSSNARK<G1>;
634 type S2 = spartan_with_ipa_pc::RelaxedR1CSSNARK<G2>;
635 use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
636 use ff::PrimeField;
637 use std::marker::PhantomData;
638
639 #[derive(Clone, Debug)]
640 struct TrivialTestCircuit<F: PrimeField> {
641 _p: PhantomData<F>,
642 }
643
644 impl<F> StepCircuit<F> for TrivialTestCircuit<F>
645 where
646 F: PrimeField,
647 {
648 fn synthesize<CS: ConstraintSystem<F>>(
649 &self,
650 _cs: &mut CS,
651 z: AllocatedNum<F>,
652 ) -> Result<AllocatedNum<F>, SynthesisError> {
653 Ok(z)
654 }
655
656 fn compute(&self, z: &F) -> F {
657 *z
658 }
659 }
660
661 #[derive(Clone, Debug)]
662 struct CubicCircuit<F: PrimeField> {
663 _p: PhantomData<F>,
664 }
665
666 impl<F> StepCircuit<F> for CubicCircuit<F>
667 where
668 F: PrimeField,
669 {
670 fn synthesize<CS: ConstraintSystem<F>>(
671 &self,
672 cs: &mut CS,
673 z: AllocatedNum<F>,
674 ) -> Result<AllocatedNum<F>, SynthesisError> {
675 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
676 let x = z;
677 let x_sq = x.square(cs.namespace(|| "x_sq"))?;
678 let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), &x)?;
679 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
680 Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
681 })?;
682
683 cs.enforce(
684 || "y = x^3 + x + 5",
685 |lc| {
686 lc + x_cu.get_variable()
687 + x.get_variable()
688 + CS::one()
689 + CS::one()
690 + CS::one()
691 + CS::one()
692 + CS::one()
693 },
694 |lc| lc + CS::one(),
695 |lc| lc + y.get_variable(),
696 );
697
698 Ok(y)
699 }
700
701 fn compute(&self, z: &F) -> F {
702 *z * *z * *z + z + F::from(5u64)
703 }
704 }
705
706 #[test]
707 fn test_ivc_trivial() {
708 // produce public parameters
709 let pp = PublicParams::<
710 G1,
711 G2,
712 TrivialTestCircuit<<G1 as Group>::Scalar>,
713 TrivialTestCircuit<<G2 as Group>::Scalar>,
714 >::setup(
715 TrivialTestCircuit {
716 _p: Default::default(),
717 },
718 TrivialTestCircuit {
719 _p: Default::default(),
720 },
721 );
722
723 // produce a recursive SNARK
724 let res = RecursiveSNARK::prove(
725 &pp,
726 3,
727 <G1 as Group>::Scalar::zero(),
728 <G2 as Group>::Scalar::zero(),
729 );
730 assert!(res.is_ok());
731 let recursive_snark = res.unwrap();
732
733 // verify the recursive SNARK
734 let res = recursive_snark.verify(
735 &pp,
736 3,
737 <G1 as Group>::Scalar::zero(),
738 <G2 as Group>::Scalar::zero(),
739 );
740 assert!(res.is_ok());
741 }
742
743 #[test]
744 fn test_ivc_nontrivial() {
745 // produce public parameters
746 let pp = PublicParams::<
747 G1,
748 G2,
749 TrivialTestCircuit<<G1 as Group>::Scalar>,
750 CubicCircuit<<G2 as Group>::Scalar>,
751 >::setup(
752 TrivialTestCircuit {
753 _p: Default::default(),
754 },
755 CubicCircuit {
756 _p: Default::default(),
757 },
758 );
759
760 let num_steps = 3;
761
762 // produce a recursive SNARK
763 let res = RecursiveSNARK::prove(
764 &pp,
765 num_steps,
766 <G1 as Group>::Scalar::one(),
767 <G2 as Group>::Scalar::zero(),
768 );
769 assert!(res.is_ok());
770 let recursive_snark = res.unwrap();
771
772 // verify the recursive SNARK
773 let res = recursive_snark.verify(
774 &pp,
775 num_steps,
776 <G1 as Group>::Scalar::one(),
777 <G2 as Group>::Scalar::zero(),
778 );
779 assert!(res.is_ok());
780
781 let (zn_primary, zn_secondary) = res.unwrap();
782
783 // sanity: check the claimed output with a direct computation of the same
784 assert_eq!(zn_primary, <G1 as Group>::Scalar::one());
785 let mut zn_secondary_direct = <G2 as Group>::Scalar::zero();
786 for _i in 0..num_steps {
787 zn_secondary_direct = CubicCircuit {
788 _p: Default::default(),
789 }
790 .compute(&zn_secondary_direct);
791 }
792 assert_eq!(zn_secondary, zn_secondary_direct);
793 assert_eq!(zn_secondary, <G2 as Group>::Scalar::from(2460515u64));
794 }
795
796 #[test]
797 fn test_ivc_nontrivial_with_compression() {
798 // produce public parameters
799 let pp = PublicParams::<
800 G1,
801 G2,
802 TrivialTestCircuit<<G1 as Group>::Scalar>,
803 CubicCircuit<<G2 as Group>::Scalar>,
804 >::setup(
805 TrivialTestCircuit {
806 _p: Default::default(),
807 },
808 CubicCircuit {
809 _p: Default::default(),
810 },
811 );
812
813 let num_steps = 3;
814
815 // produce a recursive SNARK
816 let res = RecursiveSNARK::prove(
817 &pp,
818 num_steps,
819 <G1 as Group>::Scalar::one(),
820 <G2 as Group>::Scalar::zero(),
821 );
822 assert!(res.is_ok());
823 let recursive_snark = res.unwrap();
824
825 // verify the recursive SNARK
826 let res = recursive_snark.verify(
827 &pp,
828 num_steps,
829 <G1 as Group>::Scalar::one(),
830 <G2 as Group>::Scalar::zero(),
831 );
832 assert!(res.is_ok());
833
834 let (zn_primary, zn_secondary) = res.unwrap();
835
836 // sanity: check the claimed output with a direct computation of the same
837 assert_eq!(zn_primary, <G1 as Group>::Scalar::one());
838 let mut zn_secondary_direct = <G2 as Group>::Scalar::zero();
839 for _i in 0..num_steps {
840 zn_secondary_direct = CubicCircuit {
841 _p: Default::default(),
842 }
843 .compute(&zn_secondary_direct);
844 }
845 assert_eq!(zn_secondary, zn_secondary_direct);
846 assert_eq!(zn_secondary, <G2 as Group>::Scalar::from(2460515u64));
847
848 // produce a compressed SNARK
849 let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &recursive_snark);
850 assert!(res.is_ok());
851 let compressed_snark = res.unwrap();
852
853 // verify the compressed SNARK
854 let res = compressed_snark.verify(
855 &pp,
856 num_steps,
857 <G1 as Group>::Scalar::one(),
858 <G2 as Group>::Scalar::zero(),
859 );
860 assert!(res.is_ok());
861 }
862
863 #[test]
864 fn test_ivc_base() {
865 // produce public parameters
866 let pp = PublicParams::<
867 G1,
868 G2,
869 TrivialTestCircuit<<G1 as Group>::Scalar>,
870 CubicCircuit<<G2 as Group>::Scalar>,
871 >::setup(
872 TrivialTestCircuit {
873 _p: Default::default(),
874 },
875 CubicCircuit {
876 _p: Default::default(),
877 },
878 );
879
880 let num_steps = 1;
881
882 // produce a recursive SNARK
883 let res = RecursiveSNARK::prove(
884 &pp,
885 num_steps,
886 <G1 as Group>::Scalar::one(),
887 <G2 as Group>::Scalar::zero(),
888 );
889 assert!(res.is_ok());
890 let recursive_snark = res.unwrap();
891
892 // verify the recursive SNARK
893 let res = recursive_snark.verify(
894 &pp,
895 num_steps,
896 <G1 as Group>::Scalar::one(),
897 <G2 as Group>::Scalar::zero(),
898 );
899 assert!(res.is_ok());
900
901 let (zn_primary, zn_secondary) = res.unwrap();
902
903 assert_eq!(zn_primary, <G1 as Group>::Scalar::one());
904 assert_eq!(zn_secondary, <G2 as Group>::Scalar::from(5u64));
905 }
906}