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