arnaucube
arnaucube/NovaPublic Self-hosted repository
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 poseidon::ROConstantsCircuit; // TODO: make this a trait so we can use it without the concrete implementation
 37use r1cs::{
 38  R1CSGens, R1CSInstance, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness,
 39};
 40use snark::RelaxedR1CSSNARKTrait;
 41use traits::{AbsorbInROTrait, Group, HashFuncConstantsTrait, HashFuncTrait, StepCircuit};
 42
 43type ROConstants<G> =
 44  <<G as Group>::HashFunc as HashFuncTrait<<G as Group>::Base, <G as Group>::Scalar>>::Constants;
 45
 46/// A type that holds public parameters of Nova
 47pub struct PublicParams<G1, G2, C1, C2>
 48where
 49  G1: Group<Base = <G2 as Group>::Scalar>,
 50  G2: Group<Base = <G1 as Group>::Scalar>,
 51  C1: StepCircuit<G1::Scalar> + Clone,
 52  C2: StepCircuit<G2::Scalar> + Clone,
 53{
 54  ro_consts_primary: ROConstants<G1>,
 55  ro_consts_circuit_primary: ROConstantsCircuit<<G2 as Group>::Base>,
 56  r1cs_gens_primary: R1CSGens<G1>,
 57  r1cs_shape_primary: R1CSShape<G1>,
 58  r1cs_shape_padded_primary: R1CSShape<G1>,
 59  ro_consts_secondary: ROConstants<G2>,
 60  ro_consts_circuit_secondary: ROConstantsCircuit<<G1 as Group>::Base>,
 61  r1cs_gens_secondary: R1CSGens<G2>,
 62  r1cs_shape_secondary: R1CSShape<G2>,
 63  r1cs_shape_padded_secondary: R1CSShape<G2>,
 64  c_primary: C1,
 65  c_secondary: C2,
 66  params_primary: NIFSVerifierCircuitParams,
 67  params_secondary: NIFSVerifierCircuitParams,
 68}
 69
 70impl<G1, G2, C1, C2> PublicParams<G1, G2, C1, C2>
 71where
 72  G1: Group<Base = <G2 as Group>::Scalar>,
 73  G2: Group<Base = <G1 as Group>::Scalar>,
 74  C1: StepCircuit<G1::Scalar> + Clone,
 75  C2: StepCircuit<G2::Scalar> + Clone,
 76{
 77  /// Create a new `PublicParams`
 78  pub fn setup(c_primary: C1, c_secondary: C2) -> Self {
 79    let params_primary = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, true);
 80    let params_secondary = NIFSVerifierCircuitParams::new(BN_LIMB_WIDTH, BN_N_LIMBS, false);
 81
 82    let ro_consts_primary: ROConstants<G1> = ROConstants::<G1>::new();
 83    let ro_consts_secondary: ROConstants<G2> = ROConstants::<G2>::new();
 84
 85    let ro_consts_circuit_primary: ROConstantsCircuit<<G2 as Group>::Base> =
 86      ROConstantsCircuit::new();
 87    let ro_consts_circuit_secondary: ROConstantsCircuit<<G1 as Group>::Base> =
 88      ROConstantsCircuit::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> + Clone,
139  C2: StepCircuit<G2::Scalar> + Clone,
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> + Clone,
160  C2: StepCircuit<G2::Scalar> + Clone,
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}