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