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 spartan_with_ipa_pc;
20pub mod traits;
21
22use crate::bellperson::{
23 r1cs::{NovaShape, NovaWitness},
24 shape_cs::ShapeCS,
25 solver::SatisfyingAssignment,
26};
27use ::bellperson::{Circuit, ConstraintSystem};
28use circuit::{NovaAugmentedCircuit, NovaAugmentedCircuitInputs, NovaAugmentedCircuitParams};
29use constants::{BN_LIMB_WIDTH, BN_N_LIMBS};
30use core::marker::PhantomData;
31use errors::NovaError;
32use ff::Field;
33use gadgets::utils::scalar_as_base;
34use nifs::NIFS;
35use r1cs::{
36 R1CSGens, R1CSInstance, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness,
37};
38use traits::{
39 circuit::StepCircuit, snark::RelaxedR1CSSNARKTrait, AbsorbInROTrait, Group, HashFuncConstants,
40 HashFuncConstantsCircuit, HashFuncConstantsTrait, HashFuncTrait,
41};
42
43/// A type that holds public parameters of Nova
44pub struct PublicParams<G1, G2, C1, C2>
45where
46 G1: Group<Base = <G2 as Group>::Scalar>,
47 G2: Group<Base = <G1 as Group>::Scalar>,
48 C1: StepCircuit<G1::Scalar>,
49 C2: StepCircuit<G2::Scalar>,
50{
51 ro_consts_primary: HashFuncConstants<G1>,
52 ro_consts_circuit_primary: HashFuncConstantsCircuit<G2>,
53 r1cs_gens_primary: R1CSGens<G1>,
54 r1cs_shape_primary: R1CSShape<G1>,
55 r1cs_shape_padded_primary: R1CSShape<G1>,
56 ro_consts_secondary: HashFuncConstants<G2>,
57 ro_consts_circuit_secondary: HashFuncConstantsCircuit<G1>,
58 r1cs_gens_secondary: R1CSGens<G2>,
59 r1cs_shape_secondary: R1CSShape<G2>,
60 r1cs_shape_padded_secondary: R1CSShape<G2>,
61 augmented_circuit_params_primary: NovaAugmentedCircuitParams,
62 augmented_circuit_params_secondary: NovaAugmentedCircuitParams,
63 _p_c1: PhantomData<C1>,
64 _p_c2: PhantomData<C2>,
65}
66
67impl<G1, G2, C1, C2> PublicParams<G1, G2, C1, C2>
68where
69 G1: Group<Base = <G2 as Group>::Scalar>,
70 G2: Group<Base = <G1 as Group>::Scalar>,
71 C1: StepCircuit<G1::Scalar>,
72 C2: StepCircuit<G2::Scalar>,
73{
74 /// Create a new `PublicParams`
75 pub fn setup(c_primary: C1, c_secondary: C2) -> Self {
76 let augmented_circuit_params_primary =
77 NovaAugmentedCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
78 let augmented_circuit_params_secondary =
79 NovaAugmentedCircuitParams::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: NovaAugmentedCircuit<G2, C1> = NovaAugmentedCircuit::new(
92 augmented_circuit_params_primary.clone(),
93 None,
94 c_primary,
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: NovaAugmentedCircuit<G1, C2> = NovaAugmentedCircuit::new(
104 augmented_circuit_params_secondary.clone(),
105 None,
106 c_secondary,
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 augmented_circuit_params_primary,
126 augmented_circuit_params_secondary,
127 _p_c1: Default::default(),
128 _p_c2: Default::default(),
129 }
130 }
131
132 /// Returns the number of constraints in the primary and secondary circuits
133 pub fn num_constraints(&self) -> (usize, usize) {
134 (
135 self.r1cs_shape_primary.num_cons,
136 self.r1cs_shape_secondary.num_cons,
137 )
138 }
139}
140
141/// A SNARK that proves the correct execution of an incremental computation
142#[derive(Clone, Debug)]
143pub struct RecursiveSNARK<G1, G2, C1, C2>
144where
145 G1: Group<Base = <G2 as Group>::Scalar>,
146 G2: Group<Base = <G1 as Group>::Scalar>,
147 C1: StepCircuit<G1::Scalar>,
148 C2: StepCircuit<G2::Scalar>,
149{
150 r_W_primary: RelaxedR1CSWitness<G1>,
151 r_U_primary: RelaxedR1CSInstance<G1>,
152 l_w_primary: R1CSWitness<G1>,
153 l_u_primary: R1CSInstance<G1>,
154 r_W_secondary: RelaxedR1CSWitness<G2>,
155 r_U_secondary: RelaxedR1CSInstance<G2>,
156 l_w_secondary: R1CSWitness<G2>,
157 l_u_secondary: R1CSInstance<G2>,
158 i: usize,
159 zi_primary: G1::Scalar,
160 zi_secondary: G2::Scalar,
161 _p_c1: PhantomData<C1>,
162 _p_c2: PhantomData<C2>,
163}
164
165impl<G1, G2, C1, C2> RecursiveSNARK<G1, G2, C1, C2>
166where
167 G1: Group<Base = <G2 as Group>::Scalar>,
168 G2: Group<Base = <G1 as Group>::Scalar>,
169 C1: StepCircuit<G1::Scalar>,
170 C2: StepCircuit<G2::Scalar>,
171{
172 /// Create a new `RecursiveSNARK` (or updates the provided `RecursiveSNARK`)
173 /// by executing a step of the incremental computation
174 pub fn prove_step(
175 pp: &PublicParams<G1, G2, C1, C2>,
176 recursive_snark: Option<Self>,
177 c_primary: C1,
178 c_secondary: C2,
179 z0_primary: G1::Scalar,
180 z0_secondary: G2::Scalar,
181 ) -> Result<Self, NovaError> {
182 match recursive_snark {
183 None => {
184 // base case for the primary
185 let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
186 let inputs_primary: NovaAugmentedCircuitInputs<G2> = NovaAugmentedCircuitInputs::new(
187 pp.r1cs_shape_secondary.get_digest(),
188 G1::Scalar::zero(),
189 z0_primary,
190 None,
191 None,
192 None,
193 None,
194 );
195
196 let circuit_primary: NovaAugmentedCircuit<G2, C1> = NovaAugmentedCircuit::new(
197 pp.augmented_circuit_params_primary.clone(),
198 Some(inputs_primary),
199 c_primary.clone(),
200 pp.ro_consts_circuit_primary.clone(),
201 );
202 let _ = circuit_primary.synthesize(&mut cs_primary);
203 let (u_primary, w_primary) = cs_primary
204 .r1cs_instance_and_witness(&pp.r1cs_shape_primary, &pp.r1cs_gens_primary)
205 .map_err(|_e| NovaError::UnSat)?;
206
207 // base case for the secondary
208 let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
209 let inputs_secondary: NovaAugmentedCircuitInputs<G1> = NovaAugmentedCircuitInputs::new(
210 pp.r1cs_shape_primary.get_digest(),
211 G2::Scalar::zero(),
212 z0_secondary,
213 None,
214 None,
215 Some(u_primary.clone()),
216 None,
217 );
218 let circuit_secondary: NovaAugmentedCircuit<G1, C2> = NovaAugmentedCircuit::new(
219 pp.augmented_circuit_params_secondary.clone(),
220 Some(inputs_secondary),
221 c_secondary.clone(),
222 pp.ro_consts_circuit_secondary.clone(),
223 );
224 let _ = circuit_secondary.synthesize(&mut cs_secondary);
225 let (u_secondary, w_secondary) = cs_secondary
226 .r1cs_instance_and_witness(&pp.r1cs_shape_secondary, &pp.r1cs_gens_secondary)
227 .map_err(|_e| NovaError::UnSat)?;
228
229 // IVC proof for the primary circuit
230 let l_w_primary = w_primary;
231 let l_u_primary = u_primary;
232 let r_W_primary =
233 RelaxedR1CSWitness::from_r1cs_witness(&pp.r1cs_shape_primary, &l_w_primary);
234 let r_U_primary = RelaxedR1CSInstance::from_r1cs_instance(
235 &pp.r1cs_gens_primary,
236 &pp.r1cs_shape_primary,
237 &l_u_primary,
238 );
239
240 // IVC proof of the secondary circuit
241 let l_w_secondary = w_secondary;
242 let l_u_secondary = u_secondary;
243 let r_W_secondary = RelaxedR1CSWitness::<G2>::default(&pp.r1cs_shape_secondary);
244 let r_U_secondary =
245 RelaxedR1CSInstance::<G2>::default(&pp.r1cs_gens_secondary, &pp.r1cs_shape_secondary);
246
247 // Outputs of the two circuits thus far
248 let zi_primary = c_primary.compute(&z0_primary);
249 let zi_secondary = c_secondary.compute(&z0_secondary);
250
251 Ok(Self {
252 r_W_primary,
253 r_U_primary,
254 l_w_primary,
255 l_u_primary,
256 r_W_secondary,
257 r_U_secondary,
258 l_w_secondary,
259 l_u_secondary,
260 i: 1_usize,
261 zi_primary,
262 zi_secondary,
263 _p_c1: Default::default(),
264 _p_c2: Default::default(),
265 })
266 }
267 Some(r_snark) => {
268 // fold the secondary circuit's instance
269 let (nifs_secondary, (r_U_secondary, r_W_secondary)) = NIFS::prove(
270 &pp.r1cs_gens_secondary,
271 &pp.ro_consts_secondary,
272 &pp.r1cs_shape_secondary,
273 &r_snark.r_U_secondary,
274 &r_snark.r_W_secondary,
275 &r_snark.l_u_secondary,
276 &r_snark.l_w_secondary,
277 )?;
278
279 let mut cs_primary: SatisfyingAssignment<G1> = SatisfyingAssignment::new();
280 let inputs_primary: NovaAugmentedCircuitInputs<G2> = NovaAugmentedCircuitInputs::new(
281 pp.r1cs_shape_secondary.get_digest(),
282 G1::Scalar::from(r_snark.i as u64),
283 z0_primary,
284 Some(r_snark.zi_primary),
285 Some(r_snark.r_U_secondary.clone()),
286 Some(r_snark.l_u_secondary.clone()),
287 Some(nifs_secondary.comm_T.decompress()?),
288 );
289
290 let circuit_primary: NovaAugmentedCircuit<G2, C1> = NovaAugmentedCircuit::new(
291 pp.augmented_circuit_params_primary.clone(),
292 Some(inputs_primary),
293 c_primary.clone(),
294 pp.ro_consts_circuit_primary.clone(),
295 );
296 let _ = circuit_primary.synthesize(&mut cs_primary);
297
298 let (l_u_primary, l_w_primary) = cs_primary
299 .r1cs_instance_and_witness(&pp.r1cs_shape_primary, &pp.r1cs_gens_primary)
300 .map_err(|_e| NovaError::UnSat)?;
301
302 // fold the primary circuit's instance
303 let (nifs_primary, (r_U_primary, r_W_primary)) = NIFS::prove(
304 &pp.r1cs_gens_primary,
305 &pp.ro_consts_primary,
306 &pp.r1cs_shape_primary,
307 &r_snark.r_U_primary,
308 &r_snark.r_W_primary,
309 &l_u_primary,
310 &l_w_primary,
311 )?;
312
313 let mut cs_secondary: SatisfyingAssignment<G2> = SatisfyingAssignment::new();
314 let inputs_secondary: NovaAugmentedCircuitInputs<G1> = NovaAugmentedCircuitInputs::new(
315 pp.r1cs_shape_primary.get_digest(),
316 G2::Scalar::from(r_snark.i as u64),
317 z0_secondary,
318 Some(r_snark.zi_secondary),
319 Some(r_snark.r_U_primary.clone()),
320 Some(l_u_primary.clone()),
321 Some(nifs_primary.comm_T.decompress()?),
322 );
323
324 let circuit_secondary: NovaAugmentedCircuit<G1, C2> = NovaAugmentedCircuit::new(
325 pp.augmented_circuit_params_secondary.clone(),
326 Some(inputs_secondary),
327 c_secondary.clone(),
328 pp.ro_consts_circuit_secondary.clone(),
329 );
330 let _ = circuit_secondary.synthesize(&mut cs_secondary);
331
332 let (l_u_secondary, l_w_secondary) = cs_secondary
333 .r1cs_instance_and_witness(&pp.r1cs_shape_secondary, &pp.r1cs_gens_secondary)
334 .map_err(|_e| NovaError::UnSat)?;
335
336 // update the running instances and witnesses
337 let zi_primary = c_primary.compute(&r_snark.zi_primary);
338 let zi_secondary = c_secondary.compute(&r_snark.zi_secondary);
339
340 Ok(Self {
341 r_W_primary,
342 r_U_primary,
343 l_w_primary,
344 l_u_primary,
345 r_W_secondary,
346 r_U_secondary,
347 l_w_secondary,
348 l_u_secondary,
349 i: r_snark.i + 1,
350 zi_primary,
351 zi_secondary,
352 _p_c1: Default::default(),
353 _p_c2: Default::default(),
354 })
355 }
356 }
357 }
358
359 /// Verify the correctness of the `RecursiveSNARK`
360 pub fn verify(
361 &self,
362 pp: &PublicParams<G1, G2, C1, C2>,
363 num_steps: usize,
364 z0_primary: G1::Scalar,
365 z0_secondary: G2::Scalar,
366 ) -> Result<(G1::Scalar, G2::Scalar), NovaError> {
367 // number of steps cannot be zero
368 if num_steps == 0 {
369 return Err(NovaError::ProofVerifyError);
370 }
371
372 // check if the provided proof has executed num_steps
373 if self.i != num_steps {
374 return Err(NovaError::ProofVerifyError);
375 }
376
377 // check if the (relaxed) R1CS instances have two public outputs
378 if self.l_u_primary.X.len() != 2
379 || self.l_u_secondary.X.len() != 2
380 || self.r_U_primary.X.len() != 2
381 || self.r_U_secondary.X.len() != 2
382 {
383 return Err(NovaError::ProofVerifyError);
384 }
385
386 // check if the output hashes in R1CS instances point to the right running instances
387 let (hash_primary, hash_secondary) = {
388 let mut hasher = <G2 as Group>::HashFunc::new(pp.ro_consts_secondary.clone());
389 hasher.absorb(scalar_as_base::<G2>(pp.r1cs_shape_secondary.get_digest()));
390 hasher.absorb(G1::Scalar::from(num_steps as u64));
391 hasher.absorb(z0_primary);
392 hasher.absorb(self.zi_primary);
393 self.r_U_secondary.absorb_in_ro(&mut hasher);
394
395 let mut hasher2 = <G1 as Group>::HashFunc::new(pp.ro_consts_primary.clone());
396 hasher2.absorb(scalar_as_base::<G1>(pp.r1cs_shape_primary.get_digest()));
397 hasher2.absorb(G2::Scalar::from(num_steps as u64));
398 hasher2.absorb(z0_secondary);
399 hasher2.absorb(self.zi_secondary);
400 self.r_U_primary.absorb_in_ro(&mut hasher2);
401
402 (hasher.get_hash(), hasher2.get_hash())
403 };
404
405 if hash_primary != scalar_as_base::<G1>(self.l_u_primary.X[1])
406 || hash_secondary != scalar_as_base::<G2>(self.l_u_secondary.X[1])
407 {
408 return Err(NovaError::ProofVerifyError);
409 }
410
411 // check the satisfiability of the provided instances
412 let ((res_r_primary, res_l_primary), (res_r_secondary, res_l_secondary)) = rayon::join(
413 || {
414 rayon::join(
415 || {
416 pp.r1cs_shape_primary.is_sat_relaxed(
417 &pp.r1cs_gens_primary,
418 &self.r_U_primary,
419 &self.r_W_primary,
420 )
421 },
422 || {
423 pp.r1cs_shape_primary.is_sat(
424 &pp.r1cs_gens_primary,
425 &self.l_u_primary,
426 &self.l_w_primary,
427 )
428 },
429 )
430 },
431 || {
432 rayon::join(
433 || {
434 pp.r1cs_shape_secondary.is_sat_relaxed(
435 &pp.r1cs_gens_secondary,
436 &self.r_U_secondary,
437 &self.r_W_secondary,
438 )
439 },
440 || {
441 pp.r1cs_shape_secondary.is_sat(
442 &pp.r1cs_gens_secondary,
443 &self.l_u_secondary,
444 &self.l_w_secondary,
445 )
446 },
447 )
448 },
449 );
450
451 // check the returned res objects
452 res_r_primary?;
453 res_l_primary?;
454 res_r_secondary?;
455 res_l_secondary?;
456
457 Ok((self.zi_primary, self.zi_secondary))
458 }
459}
460
461/// A SNARK that proves the knowledge of a valid `RecursiveSNARK`
462#[derive(Clone, Debug)]
463pub struct CompressedSNARK<G1, G2, C1, C2, S1, S2>
464where
465 G1: Group<Base = <G2 as Group>::Scalar>,
466 G2: Group<Base = <G1 as Group>::Scalar>,
467 C1: StepCircuit<G1::Scalar>,
468 C2: StepCircuit<G2::Scalar>,
469 S1: RelaxedR1CSSNARKTrait<G1>,
470 S2: RelaxedR1CSSNARKTrait<G2>,
471{
472 r_U_primary: RelaxedR1CSInstance<G1>,
473 l_u_primary: R1CSInstance<G1>,
474 nifs_primary: NIFS<G1>,
475 f_W_snark_primary: S1,
476
477 r_U_secondary: RelaxedR1CSInstance<G2>,
478 l_u_secondary: R1CSInstance<G2>,
479 nifs_secondary: NIFS<G2>,
480 f_W_snark_secondary: S2,
481
482 zn_primary: G1::Scalar,
483 zn_secondary: G2::Scalar,
484
485 _p_c1: PhantomData<C1>,
486 _p_c2: PhantomData<C2>,
487}
488
489impl<G1, G2, C1, C2, S1, S2> CompressedSNARK<G1, G2, C1, C2, S1, S2>
490where
491 G1: Group<Base = <G2 as Group>::Scalar>,
492 G2: Group<Base = <G1 as Group>::Scalar>,
493 C1: StepCircuit<G1::Scalar>,
494 C2: StepCircuit<G2::Scalar>,
495 S1: RelaxedR1CSSNARKTrait<G1>,
496 S2: RelaxedR1CSSNARKTrait<G2>,
497{
498 /// Create a new `CompressedSNARK`
499 pub fn prove(
500 pp: &PublicParams<G1, G2, C1, C2>,
501 recursive_snark: &RecursiveSNARK<G1, G2, C1, C2>,
502 ) -> Result<Self, NovaError> {
503 let (res_primary, res_secondary) = rayon::join(
504 // fold the primary circuit's instance
505 || {
506 NIFS::prove(
507 &pp.r1cs_gens_primary,
508 &pp.ro_consts_primary,
509 &pp.r1cs_shape_primary,
510 &recursive_snark.r_U_primary,
511 &recursive_snark.r_W_primary,
512 &recursive_snark.l_u_primary,
513 &recursive_snark.l_w_primary,
514 )
515 },
516 || {
517 // fold the secondary circuit's instance
518 NIFS::prove(
519 &pp.r1cs_gens_secondary,
520 &pp.ro_consts_secondary,
521 &pp.r1cs_shape_secondary,
522 &recursive_snark.r_U_secondary,
523 &recursive_snark.r_W_secondary,
524 &recursive_snark.l_u_secondary,
525 &recursive_snark.l_w_secondary,
526 )
527 },
528 );
529
530 let (nifs_primary, (f_U_primary, f_W_primary)) = res_primary?;
531 let (nifs_secondary, (f_U_secondary, f_W_secondary)) = res_secondary?;
532
533 // produce a prover key for the SNARK
534 let (pk_primary, pk_secondary) = rayon::join(
535 || S1::prover_key(&pp.r1cs_gens_primary, &pp.r1cs_shape_padded_primary),
536 || S2::prover_key(&pp.r1cs_gens_secondary, &pp.r1cs_shape_padded_secondary),
537 );
538
539 // create SNARKs proving the knowledge of f_W_primary and f_W_secondary
540 let (f_W_snark_primary, f_W_snark_secondary) = rayon::join(
541 || {
542 S1::prove(
543 &pk_primary,
544 &f_U_primary,
545 &f_W_primary.pad(&pp.r1cs_shape_padded_primary), // pad the witness since shape was padded
546 )
547 },
548 || {
549 S2::prove(
550 &pk_secondary,
551 &f_U_secondary,
552 &f_W_secondary.pad(&pp.r1cs_shape_padded_secondary), // pad the witness since the shape was padded
553 )
554 },
555 );
556
557 Ok(Self {
558 r_U_primary: recursive_snark.r_U_primary.clone(),
559 l_u_primary: recursive_snark.l_u_primary.clone(),
560 nifs_primary,
561 f_W_snark_primary: f_W_snark_primary?,
562
563 r_U_secondary: recursive_snark.r_U_secondary.clone(),
564 l_u_secondary: recursive_snark.l_u_secondary.clone(),
565 nifs_secondary,
566 f_W_snark_secondary: f_W_snark_secondary?,
567
568 zn_primary: recursive_snark.zi_primary,
569 zn_secondary: recursive_snark.zi_secondary,
570
571 _p_c1: Default::default(),
572 _p_c2: Default::default(),
573 })
574 }
575
576 /// Verify the correctness of the `CompressedSNARK`
577 pub fn verify(
578 &self,
579 pp: &PublicParams<G1, G2, C1, C2>,
580 num_steps: usize,
581 z0_primary: G1::Scalar,
582 z0_secondary: G2::Scalar,
583 ) -> Result<(G1::Scalar, G2::Scalar), NovaError> {
584 // number of steps cannot be zero
585 if num_steps == 0 {
586 return Err(NovaError::ProofVerifyError);
587 }
588
589 // check if the (relaxed) R1CS instances have two public outputs
590 if self.l_u_primary.X.len() != 2
591 || self.l_u_secondary.X.len() != 2
592 || self.r_U_primary.X.len() != 2
593 || self.r_U_secondary.X.len() != 2
594 {
595 return Err(NovaError::ProofVerifyError);
596 }
597
598 // check if the output hashes in R1CS instances point to the right running instances
599 let (hash_primary, hash_secondary) = {
600 let mut hasher = <G2 as Group>::HashFunc::new(pp.ro_consts_secondary.clone());
601 hasher.absorb(scalar_as_base::<G2>(pp.r1cs_shape_secondary.get_digest()));
602 hasher.absorb(G1::Scalar::from(num_steps as u64));
603 hasher.absorb(z0_primary);
604 hasher.absorb(self.zn_primary);
605 self.r_U_secondary.absorb_in_ro(&mut hasher);
606
607 let mut hasher2 = <G1 as Group>::HashFunc::new(pp.ro_consts_primary.clone());
608 hasher2.absorb(scalar_as_base::<G1>(pp.r1cs_shape_primary.get_digest()));
609 hasher2.absorb(G2::Scalar::from(num_steps as u64));
610 hasher2.absorb(z0_secondary);
611 hasher2.absorb(self.zn_secondary);
612 self.r_U_primary.absorb_in_ro(&mut hasher2);
613
614 (hasher.get_hash(), hasher2.get_hash())
615 };
616
617 if hash_primary != scalar_as_base::<G1>(self.l_u_primary.X[1])
618 || hash_secondary != scalar_as_base::<G2>(self.l_u_secondary.X[1])
619 {
620 return Err(NovaError::ProofVerifyError);
621 }
622
623 // fold the running instance and last instance to get a folded instance
624 let f_U_primary = self.nifs_primary.verify(
625 &pp.ro_consts_primary,
626 &pp.r1cs_shape_primary,
627 &self.r_U_primary,
628 &self.l_u_primary,
629 )?;
630 let f_U_secondary = self.nifs_secondary.verify(
631 &pp.ro_consts_secondary,
632 &pp.r1cs_shape_secondary,
633 &self.r_U_secondary,
634 &self.l_u_secondary,
635 )?;
636
637 // produce a verifier key for the SNARK
638 let (vk_primary, vk_secondary) = rayon::join(
639 || S1::verifier_key(&pp.r1cs_gens_primary, &pp.r1cs_shape_padded_primary),
640 || S2::verifier_key(&pp.r1cs_gens_secondary, &pp.r1cs_shape_padded_secondary),
641 );
642
643 // check the satisfiability of the folded instances using SNARKs proving the knowledge of their satisfying witnesses
644 let (res_primary, res_secondary) = rayon::join(
645 || self.f_W_snark_primary.verify(&vk_primary, &f_U_primary),
646 || {
647 self
648 .f_W_snark_secondary
649 .verify(&vk_secondary, &f_U_secondary)
650 },
651 );
652
653 res_primary?;
654 res_secondary?;
655
656 Ok((self.zn_primary, self.zn_secondary))
657 }
658}
659
660#[cfg(test)]
661mod tests {
662 use super::*;
663 type G1 = pasta_curves::pallas::Point;
664 type G2 = pasta_curves::vesta::Point;
665 type S1 = spartan_with_ipa_pc::RelaxedR1CSSNARK<G1>;
666 type S2 = spartan_with_ipa_pc::RelaxedR1CSSNARK<G2>;
667 use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
668 use core::marker::PhantomData;
669 use ff::PrimeField;
670 use traits::circuit::TrivialTestCircuit;
671
672 #[derive(Clone, Debug, Default)]
673 struct CubicCircuit<F: PrimeField> {
674 _p: PhantomData<F>,
675 }
676
677 impl<F> StepCircuit<F> for CubicCircuit<F>
678 where
679 F: PrimeField,
680 {
681 fn synthesize<CS: ConstraintSystem<F>>(
682 &self,
683 cs: &mut CS,
684 z: AllocatedNum<F>,
685 ) -> Result<AllocatedNum<F>, SynthesisError> {
686 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
687 let x = z;
688 let x_sq = x.square(cs.namespace(|| "x_sq"))?;
689 let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), &x)?;
690 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
691 Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
692 })?;
693
694 cs.enforce(
695 || "y = x^3 + x + 5",
696 |lc| {
697 lc + x_cu.get_variable()
698 + x.get_variable()
699 + CS::one()
700 + CS::one()
701 + CS::one()
702 + CS::one()
703 + CS::one()
704 },
705 |lc| lc + CS::one(),
706 |lc| lc + y.get_variable(),
707 );
708
709 Ok(y)
710 }
711
712 fn compute(&self, z: &F) -> F {
713 *z * *z * *z + z + F::from(5u64)
714 }
715 }
716
717 #[test]
718 fn test_ivc_trivial() {
719 // produce public parameters
720 let pp = PublicParams::<
721 G1,
722 G2,
723 TrivialTestCircuit<<G1 as Group>::Scalar>,
724 TrivialTestCircuit<<G2 as Group>::Scalar>,
725 >::setup(TrivialTestCircuit::default(), TrivialTestCircuit::default());
726
727 let num_steps = 1;
728
729 // produce a recursive SNARK
730 let res = RecursiveSNARK::prove_step(
731 &pp,
732 None,
733 TrivialTestCircuit::default(),
734 TrivialTestCircuit::default(),
735 <G1 as Group>::Scalar::zero(),
736 <G2 as Group>::Scalar::zero(),
737 );
738 assert!(res.is_ok());
739 let recursive_snark = res.unwrap();
740
741 // verify the recursive SNARK
742 let res = recursive_snark.verify(
743 &pp,
744 num_steps,
745 <G1 as Group>::Scalar::zero(),
746 <G2 as Group>::Scalar::zero(),
747 );
748 assert!(res.is_ok());
749 }
750
751 #[test]
752 fn test_ivc_nontrivial() {
753 let circuit_primary = TrivialTestCircuit::default();
754 let circuit_secondary = CubicCircuit::default();
755
756 // produce public parameters
757 let pp = PublicParams::<
758 G1,
759 G2,
760 TrivialTestCircuit<<G1 as Group>::Scalar>,
761 CubicCircuit<<G2 as Group>::Scalar>,
762 >::setup(circuit_primary.clone(), circuit_secondary.clone());
763
764 let num_steps = 3;
765
766 // produce a recursive SNARK
767 let mut recursive_snark: Option<
768 RecursiveSNARK<
769 G1,
770 G2,
771 TrivialTestCircuit<<G1 as Group>::Scalar>,
772 CubicCircuit<<G2 as Group>::Scalar>,
773 >,
774 > = None;
775
776 for i in 0..num_steps {
777 let res = RecursiveSNARK::prove_step(
778 &pp,
779 recursive_snark,
780 circuit_primary.clone(),
781 circuit_secondary.clone(),
782 <G1 as Group>::Scalar::one(),
783 <G2 as Group>::Scalar::zero(),
784 );
785 assert!(res.is_ok());
786 let recursive_snark_unwrapped = res.unwrap();
787
788 // verify the recursive snark at each step of recursion
789 let res = recursive_snark_unwrapped.verify(
790 &pp,
791 i + 1,
792 <G1 as Group>::Scalar::one(),
793 <G2 as Group>::Scalar::zero(),
794 );
795 assert!(res.is_ok());
796
797 // set the running variable for the next iteration
798 recursive_snark = Some(recursive_snark_unwrapped);
799 }
800
801 assert!(recursive_snark.is_some());
802 let recursive_snark = recursive_snark.unwrap();
803
804 // verify the recursive SNARK
805 let res = recursive_snark.verify(
806 &pp,
807 num_steps,
808 <G1 as Group>::Scalar::one(),
809 <G2 as Group>::Scalar::zero(),
810 );
811 assert!(res.is_ok());
812
813 let (zn_primary, zn_secondary) = res.unwrap();
814
815 // sanity: check the claimed output with a direct computation of the same
816 assert_eq!(zn_primary, <G1 as Group>::Scalar::one());
817 let mut zn_secondary_direct = <G2 as Group>::Scalar::zero();
818 for _i in 0..num_steps {
819 zn_secondary_direct = CubicCircuit::default().compute(&zn_secondary_direct);
820 }
821 assert_eq!(zn_secondary, zn_secondary_direct);
822 assert_eq!(zn_secondary, <G2 as Group>::Scalar::from(2460515u64));
823 }
824
825 #[test]
826 fn test_ivc_nontrivial_with_compression() {
827 let circuit_primary = TrivialTestCircuit::default();
828 let circuit_secondary = CubicCircuit::default();
829
830 // produce public parameters
831 let pp = PublicParams::<
832 G1,
833 G2,
834 TrivialTestCircuit<<G1 as Group>::Scalar>,
835 CubicCircuit<<G2 as Group>::Scalar>,
836 >::setup(circuit_primary.clone(), circuit_secondary.clone());
837
838 let num_steps = 3;
839
840 // produce a recursive SNARK
841 let mut recursive_snark: Option<
842 RecursiveSNARK<
843 G1,
844 G2,
845 TrivialTestCircuit<<G1 as Group>::Scalar>,
846 CubicCircuit<<G2 as Group>::Scalar>,
847 >,
848 > = None;
849
850 for _i in 0..num_steps {
851 let res = RecursiveSNARK::prove_step(
852 &pp,
853 recursive_snark,
854 circuit_primary.clone(),
855 circuit_secondary.clone(),
856 <G1 as Group>::Scalar::one(),
857 <G2 as Group>::Scalar::zero(),
858 );
859 assert!(res.is_ok());
860 recursive_snark = Some(res.unwrap());
861 }
862
863 assert!(recursive_snark.is_some());
864 let recursive_snark = recursive_snark.unwrap();
865
866 // verify the recursive SNARK
867 let res = recursive_snark.verify(
868 &pp,
869 num_steps,
870 <G1 as Group>::Scalar::one(),
871 <G2 as Group>::Scalar::zero(),
872 );
873 assert!(res.is_ok());
874
875 let (zn_primary, zn_secondary) = res.unwrap();
876
877 // sanity: check the claimed output with a direct computation of the same
878 assert_eq!(zn_primary, <G1 as Group>::Scalar::one());
879 let mut zn_secondary_direct = <G2 as Group>::Scalar::zero();
880 for _i in 0..num_steps {
881 zn_secondary_direct = CubicCircuit::default().compute(&zn_secondary_direct);
882 }
883 assert_eq!(zn_secondary, zn_secondary_direct);
884 assert_eq!(zn_secondary, <G2 as Group>::Scalar::from(2460515u64));
885
886 // produce a compressed SNARK
887 let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &recursive_snark);
888 assert!(res.is_ok());
889 let compressed_snark = res.unwrap();
890
891 // verify the compressed SNARK
892 let res = compressed_snark.verify(
893 &pp,
894 num_steps,
895 <G1 as Group>::Scalar::one(),
896 <G2 as Group>::Scalar::zero(),
897 );
898 assert!(res.is_ok());
899 }
900
901 #[test]
902 fn test_ivc_nondet_with_compression() {
903 // y is a non-deterministic advice representing the fifth root of the input at a step.
904 #[derive(Clone, Debug)]
905 struct FifthRootCheckingCircuit<F: PrimeField> {
906 y: F,
907 }
908
909 impl<F> FifthRootCheckingCircuit<F>
910 where
911 F: PrimeField,
912 {
913 fn new(num_steps: usize) -> (F, Vec<Self>) {
914 let mut powers = Vec::new();
915 let rng = &mut rand::rngs::OsRng;
916 let mut seed = F::random(rng);
917 for _i in 0..num_steps + 1 {
918 let mut power = seed;
919 power = power.square();
920 power = power.square();
921 power *= seed;
922
923 powers.push(Self { y: power });
924
925 seed = power;
926 }
927
928 // reverse the powers to get roots
929 let roots = powers.into_iter().rev().collect::<Vec<Self>>();
930 (roots[0].y, roots[1..].to_vec())
931 }
932 }
933
934 impl<F> StepCircuit<F> for FifthRootCheckingCircuit<F>
935 where
936 F: PrimeField,
937 {
938 fn synthesize<CS: ConstraintSystem<F>>(
939 &self,
940 cs: &mut CS,
941 z: AllocatedNum<F>,
942 ) -> Result<AllocatedNum<F>, SynthesisError> {
943 let x = z;
944
945 // we allocate a variable and set it to the provided non-derministic advice.
946 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || Ok(self.y))?;
947
948 // We now check if y = x^{1/5} by checking if y^5 = x
949 let y_sq = y.square(cs.namespace(|| "y_sq"))?;
950 let y_quad = y_sq.square(cs.namespace(|| "y_quad"))?;
951 let y_pow_5 = y_quad.mul(cs.namespace(|| "y_fifth"), &y)?;
952
953 cs.enforce(
954 || "y^5 = x",
955 |lc| lc + y_pow_5.get_variable(),
956 |lc| lc + CS::one(),
957 |lc| lc + x.get_variable(),
958 );
959
960 Ok(y)
961 }
962
963 fn compute(&self, z: &F) -> F {
964 // sanity check
965 let x = *z;
966 let y_pow_5 = {
967 let y = self.y;
968 let y_sq = y.square();
969 let y_quad = y_sq.square();
970 y_quad * self.y
971 };
972 assert_eq!(x, y_pow_5);
973
974 // return non-deterministic advice
975 // as the output of the step
976 self.y
977 }
978 }
979
980 let circuit_primary = FifthRootCheckingCircuit {
981 y: <G1 as Group>::Scalar::zero(),
982 };
983
984 let circuit_secondary = TrivialTestCircuit::default();
985
986 // produce public parameters
987 let pp = PublicParams::<
988 G1,
989 G2,
990 FifthRootCheckingCircuit<<G1 as Group>::Scalar>,
991 TrivialTestCircuit<<G2 as Group>::Scalar>,
992 >::setup(circuit_primary, circuit_secondary.clone());
993
994 let num_steps = 3;
995
996 // produce non-deterministic advice
997 let (z0_primary, roots) = FifthRootCheckingCircuit::new(num_steps);
998 let z0_secondary = <G2 as Group>::Scalar::zero();
999
1000 // produce a recursive SNARK
1001 let mut recursive_snark: Option<
1002 RecursiveSNARK<
1003 G1,
1004 G2,
1005 FifthRootCheckingCircuit<<G1 as Group>::Scalar>,
1006 TrivialTestCircuit<<G2 as Group>::Scalar>,
1007 >,
1008 > = None;
1009
1010 for circuit_primary in roots.iter().take(num_steps) {
1011 let res = RecursiveSNARK::prove_step(
1012 &pp,
1013 recursive_snark,
1014 circuit_primary.clone(),
1015 circuit_secondary.clone(),
1016 z0_primary,
1017 z0_secondary,
1018 );
1019 assert!(res.is_ok());
1020 recursive_snark = Some(res.unwrap());
1021 }
1022
1023 assert!(recursive_snark.is_some());
1024 let recursive_snark = recursive_snark.unwrap();
1025
1026 // verify the recursive SNARK
1027 let res = recursive_snark.verify(&pp, num_steps, z0_primary, z0_secondary);
1028 assert!(res.is_ok());
1029
1030 // produce a compressed SNARK
1031 let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &recursive_snark);
1032 assert!(res.is_ok());
1033 let compressed_snark = res.unwrap();
1034
1035 // verify the compressed SNARK
1036 let res = compressed_snark.verify(&pp, num_steps, z0_primary, z0_secondary);
1037 assert!(res.is_ok());
1038 }
1039
1040 #[test]
1041 fn test_ivc_base() {
1042 // produce public parameters
1043 let pp = PublicParams::<
1044 G1,
1045 G2,
1046 TrivialTestCircuit<<G1 as Group>::Scalar>,
1047 CubicCircuit<<G2 as Group>::Scalar>,
1048 >::setup(TrivialTestCircuit::default(), CubicCircuit::default());
1049
1050 let num_steps = 1;
1051
1052 // produce a recursive SNARK
1053 let res = RecursiveSNARK::prove_step(
1054 &pp,
1055 None,
1056 TrivialTestCircuit::default(),
1057 CubicCircuit::default(),
1058 <G1 as Group>::Scalar::one(),
1059 <G2 as Group>::Scalar::zero(),
1060 );
1061 assert!(res.is_ok());
1062 let recursive_snark = res.unwrap();
1063
1064 // verify the recursive SNARK
1065 let res = recursive_snark.verify(
1066 &pp,
1067 num_steps,
1068 <G1 as Group>::Scalar::one(),
1069 <G2 as Group>::Scalar::zero(),
1070 );
1071 assert!(res.is_ok());
1072
1073 let (zn_primary, zn_secondary) = res.unwrap();
1074
1075 assert_eq!(zn_primary, <G1 as Group>::Scalar::one());
1076 assert_eq!(zn_secondary, <G2 as Group>::Scalar::from(5u64));
1077 }
1078}