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