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