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