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