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 constants;
10mod nifs;
11mod r1cs;
12
13// public modules
14pub mod errors;
15pub mod gadgets;
16pub mod provider;
17pub mod spartan;
18pub mod traits;
19
20use crate::bellperson::{
21 r1cs::{NovaShape, NovaWitness},
22 shape_cs::ShapeCS,
23 solver::SatisfyingAssignment,
24};
25use ::bellperson::{Circuit, ConstraintSystem};
26use circuit::{NovaAugmentedCircuit, NovaAugmentedCircuitInputs, NovaAugmentedCircuitParams};
27use constants::{BN_LIMB_WIDTH, BN_N_LIMBS, NUM_FE_WITHOUT_IO_FOR_CRHF, NUM_HASH_BITS};
28use core::marker::PhantomData;
29use errors::NovaError;
30use ff::Field;
31use gadgets::utils::scalar_as_base;
32use nifs::NIFS;
33use r1cs::{
34 R1CSGens, R1CSInstance, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness,
35};
36use serde::{Deserialize, Serialize};
37use traits::{
38 circuit::StepCircuit,
39 commitment::{CommitmentEngineTrait, CompressedCommitmentTrait},
40 snark::RelaxedR1CSSNARKTrait,
41 AbsorbInROTrait, Group, ROConstants, 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
720type CommitmentGens<G> = <<G as traits::Group>::CE as CommitmentEngineTrait<G>>::CommitmentGens;
721type Commitment<G> = <<G as Group>::CE as CommitmentEngineTrait<G>>::Commitment;
722type CompressedCommitment<G> = <<G as Group>::CE as CommitmentEngineTrait<G>>::CompressedCommitment;
723type CE<G> = <G as Group>::CE;
724
725#[cfg(test)]
726mod tests {
727 use super::*;
728 type G1 = pasta_curves::pallas::Point;
729 type G2 = pasta_curves::vesta::Point;
730 type EE1 = provider::ipa_pc::EvaluationEngine<G1>;
731 type EE2 = provider::ipa_pc::EvaluationEngine<G2>;
732 type S1 = spartan::RelaxedR1CSSNARK<G1, EE1>;
733 type S2 = spartan::RelaxedR1CSSNARK<G2, EE2>;
734 use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
735 use core::marker::PhantomData;
736 use ff::PrimeField;
737 use traits::circuit::TrivialTestCircuit;
738
739 #[derive(Clone, Debug, Default)]
740 struct CubicCircuit<F: PrimeField> {
741 _p: PhantomData<F>,
742 }
743
744 impl<F> StepCircuit<F> for CubicCircuit<F>
745 where
746 F: PrimeField,
747 {
748 fn arity(&self) -> usize {
749 1
750 }
751
752 fn synthesize<CS: ConstraintSystem<F>>(
753 &self,
754 cs: &mut CS,
755 z: &[AllocatedNum<F>],
756 ) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
757 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
758 let x = &z[0];
759 let x_sq = x.square(cs.namespace(|| "x_sq"))?;
760 let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), x)?;
761 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
762 Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + F::from(5u64))
763 })?;
764
765 cs.enforce(
766 || "y = x^3 + x + 5",
767 |lc| {
768 lc + x_cu.get_variable()
769 + x.get_variable()
770 + CS::one()
771 + CS::one()
772 + CS::one()
773 + CS::one()
774 + CS::one()
775 },
776 |lc| lc + CS::one(),
777 |lc| lc + y.get_variable(),
778 );
779
780 Ok(vec![y])
781 }
782
783 fn output(&self, z: &[F]) -> Vec<F> {
784 vec![z[0] * z[0] * z[0] + z[0] + F::from(5u64)]
785 }
786 }
787
788 #[test]
789 fn test_ivc_trivial() {
790 // produce public parameters
791 let pp = PublicParams::<
792 G1,
793 G2,
794 TrivialTestCircuit<<G1 as Group>::Scalar>,
795 TrivialTestCircuit<<G2 as Group>::Scalar>,
796 >::setup(TrivialTestCircuit::default(), TrivialTestCircuit::default());
797
798 let num_steps = 1;
799
800 // produce a recursive SNARK
801 let res = RecursiveSNARK::prove_step(
802 &pp,
803 None,
804 TrivialTestCircuit::default(),
805 TrivialTestCircuit::default(),
806 vec![<G1 as Group>::Scalar::zero()],
807 vec![<G2 as Group>::Scalar::zero()],
808 );
809 assert!(res.is_ok());
810 let recursive_snark = res.unwrap();
811
812 // verify the recursive SNARK
813 let res = recursive_snark.verify(
814 &pp,
815 num_steps,
816 vec![<G1 as Group>::Scalar::zero()],
817 vec![<G2 as Group>::Scalar::zero()],
818 );
819 assert!(res.is_ok());
820 }
821
822 #[test]
823 fn test_ivc_nontrivial() {
824 let circuit_primary = TrivialTestCircuit::default();
825 let circuit_secondary = CubicCircuit::default();
826
827 // produce public parameters
828 let pp = PublicParams::<
829 G1,
830 G2,
831 TrivialTestCircuit<<G1 as Group>::Scalar>,
832 CubicCircuit<<G2 as Group>::Scalar>,
833 >::setup(circuit_primary.clone(), circuit_secondary.clone());
834
835 let num_steps = 3;
836
837 // produce a recursive SNARK
838 let mut recursive_snark: Option<
839 RecursiveSNARK<
840 G1,
841 G2,
842 TrivialTestCircuit<<G1 as Group>::Scalar>,
843 CubicCircuit<<G2 as Group>::Scalar>,
844 >,
845 > = None;
846
847 for i in 0..num_steps {
848 let res = RecursiveSNARK::prove_step(
849 &pp,
850 recursive_snark,
851 circuit_primary.clone(),
852 circuit_secondary.clone(),
853 vec![<G1 as Group>::Scalar::one()],
854 vec![<G2 as Group>::Scalar::zero()],
855 );
856 assert!(res.is_ok());
857 let recursive_snark_unwrapped = res.unwrap();
858
859 // verify the recursive snark at each step of recursion
860 let res = recursive_snark_unwrapped.verify(
861 &pp,
862 i + 1,
863 vec![<G1 as Group>::Scalar::one()],
864 vec![<G2 as Group>::Scalar::zero()],
865 );
866 assert!(res.is_ok());
867
868 // set the running variable for the next iteration
869 recursive_snark = Some(recursive_snark_unwrapped);
870 }
871
872 assert!(recursive_snark.is_some());
873 let recursive_snark = recursive_snark.unwrap();
874
875 // verify the recursive SNARK
876 let res = recursive_snark.verify(
877 &pp,
878 num_steps,
879 vec![<G1 as Group>::Scalar::one()],
880 vec![<G2 as Group>::Scalar::zero()],
881 );
882 assert!(res.is_ok());
883
884 let (zn_primary, zn_secondary) = res.unwrap();
885
886 // sanity: check the claimed output with a direct computation of the same
887 assert_eq!(zn_primary, vec![<G1 as Group>::Scalar::one()]);
888 let mut zn_secondary_direct = vec![<G2 as Group>::Scalar::zero()];
889 for _i in 0..num_steps {
890 zn_secondary_direct = CubicCircuit::default().output(&zn_secondary_direct);
891 }
892 assert_eq!(zn_secondary, zn_secondary_direct);
893 assert_eq!(zn_secondary, vec![<G2 as Group>::Scalar::from(2460515u64)]);
894 }
895
896 #[test]
897 fn test_ivc_nontrivial_with_compression() {
898 let circuit_primary = TrivialTestCircuit::default();
899 let circuit_secondary = CubicCircuit::default();
900
901 // produce public parameters
902 let pp = PublicParams::<
903 G1,
904 G2,
905 TrivialTestCircuit<<G1 as Group>::Scalar>,
906 CubicCircuit<<G2 as Group>::Scalar>,
907 >::setup(circuit_primary.clone(), circuit_secondary.clone());
908
909 let num_steps = 3;
910
911 // produce a recursive SNARK
912 let mut recursive_snark: Option<
913 RecursiveSNARK<
914 G1,
915 G2,
916 TrivialTestCircuit<<G1 as Group>::Scalar>,
917 CubicCircuit<<G2 as Group>::Scalar>,
918 >,
919 > = None;
920
921 for _i in 0..num_steps {
922 let res = RecursiveSNARK::prove_step(
923 &pp,
924 recursive_snark,
925 circuit_primary.clone(),
926 circuit_secondary.clone(),
927 vec![<G1 as Group>::Scalar::one()],
928 vec![<G2 as Group>::Scalar::zero()],
929 );
930 assert!(res.is_ok());
931 recursive_snark = Some(res.unwrap());
932 }
933
934 assert!(recursive_snark.is_some());
935 let recursive_snark = recursive_snark.unwrap();
936
937 // verify the recursive SNARK
938 let res = recursive_snark.verify(
939 &pp,
940 num_steps,
941 vec![<G1 as Group>::Scalar::one()],
942 vec![<G2 as Group>::Scalar::zero()],
943 );
944 assert!(res.is_ok());
945
946 let (zn_primary, zn_secondary) = res.unwrap();
947
948 // sanity: check the claimed output with a direct computation of the same
949 assert_eq!(zn_primary, vec![<G1 as Group>::Scalar::one()]);
950 let mut zn_secondary_direct = vec![<G2 as Group>::Scalar::zero()];
951 for _i in 0..num_steps {
952 zn_secondary_direct = CubicCircuit::default().output(&zn_secondary_direct);
953 }
954 assert_eq!(zn_secondary, zn_secondary_direct);
955 assert_eq!(zn_secondary, vec![<G2 as Group>::Scalar::from(2460515u64)]);
956
957 // produce a compressed SNARK
958 let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &recursive_snark);
959 assert!(res.is_ok());
960 let compressed_snark = res.unwrap();
961
962 // verify the compressed SNARK
963 let res = compressed_snark.verify(
964 &pp,
965 num_steps,
966 vec![<G1 as Group>::Scalar::one()],
967 vec![<G2 as Group>::Scalar::zero()],
968 );
969 assert!(res.is_ok());
970 }
971
972 #[test]
973 fn test_ivc_nondet_with_compression() {
974 // y is a non-deterministic advice representing the fifth root of the input at a step.
975 #[derive(Clone, Debug)]
976 struct FifthRootCheckingCircuit<F: PrimeField> {
977 y: F,
978 }
979
980 impl<F> FifthRootCheckingCircuit<F>
981 where
982 F: PrimeField,
983 {
984 fn new(num_steps: usize) -> (Vec<F>, Vec<Self>) {
985 let mut powers = Vec::new();
986 let rng = &mut rand::rngs::OsRng;
987 let mut seed = F::random(rng);
988 for _i in 0..num_steps + 1 {
989 let mut power = seed;
990 power = power.square();
991 power = power.square();
992 power *= seed;
993
994 powers.push(Self { y: power });
995
996 seed = power;
997 }
998
999 // reverse the powers to get roots
1000 let roots = powers.into_iter().rev().collect::<Vec<Self>>();
1001 (vec![roots[0].y], roots[1..].to_vec())
1002 }
1003 }
1004
1005 impl<F> StepCircuit<F> for FifthRootCheckingCircuit<F>
1006 where
1007 F: PrimeField,
1008 {
1009 fn arity(&self) -> usize {
1010 1
1011 }
1012
1013 fn synthesize<CS: ConstraintSystem<F>>(
1014 &self,
1015 cs: &mut CS,
1016 z: &[AllocatedNum<F>],
1017 ) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
1018 let x = &z[0];
1019
1020 // we allocate a variable and set it to the provided non-derministic advice.
1021 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || Ok(self.y))?;
1022
1023 // We now check if y = x^{1/5} by checking if y^5 = x
1024 let y_sq = y.square(cs.namespace(|| "y_sq"))?;
1025 let y_quad = y_sq.square(cs.namespace(|| "y_quad"))?;
1026 let y_pow_5 = y_quad.mul(cs.namespace(|| "y_fifth"), &y)?;
1027
1028 cs.enforce(
1029 || "y^5 = x",
1030 |lc| lc + y_pow_5.get_variable(),
1031 |lc| lc + CS::one(),
1032 |lc| lc + x.get_variable(),
1033 );
1034
1035 Ok(vec![y])
1036 }
1037
1038 fn output(&self, z: &[F]) -> Vec<F> {
1039 // sanity check
1040 let x = z[0];
1041 let y_pow_5 = {
1042 let y = self.y;
1043 let y_sq = y.square();
1044 let y_quad = y_sq.square();
1045 y_quad * self.y
1046 };
1047 assert_eq!(x, y_pow_5);
1048
1049 // return non-deterministic advice
1050 // as the output of the step
1051 vec![self.y]
1052 }
1053 }
1054
1055 let circuit_primary = FifthRootCheckingCircuit {
1056 y: <G1 as Group>::Scalar::zero(),
1057 };
1058
1059 let circuit_secondary = TrivialTestCircuit::default();
1060
1061 // produce public parameters
1062 let pp = PublicParams::<
1063 G1,
1064 G2,
1065 FifthRootCheckingCircuit<<G1 as Group>::Scalar>,
1066 TrivialTestCircuit<<G2 as Group>::Scalar>,
1067 >::setup(circuit_primary, circuit_secondary.clone());
1068
1069 let num_steps = 3;
1070
1071 // produce non-deterministic advice
1072 let (z0_primary, roots) = FifthRootCheckingCircuit::new(num_steps);
1073 let z0_secondary = vec![<G2 as Group>::Scalar::zero()];
1074
1075 // produce a recursive SNARK
1076 let mut recursive_snark: Option<
1077 RecursiveSNARK<
1078 G1,
1079 G2,
1080 FifthRootCheckingCircuit<<G1 as Group>::Scalar>,
1081 TrivialTestCircuit<<G2 as Group>::Scalar>,
1082 >,
1083 > = None;
1084
1085 for circuit_primary in roots.iter().take(num_steps) {
1086 let res = RecursiveSNARK::prove_step(
1087 &pp,
1088 recursive_snark,
1089 circuit_primary.clone(),
1090 circuit_secondary.clone(),
1091 z0_primary.clone(),
1092 z0_secondary.clone(),
1093 );
1094 assert!(res.is_ok());
1095 recursive_snark = Some(res.unwrap());
1096 }
1097
1098 assert!(recursive_snark.is_some());
1099 let recursive_snark = recursive_snark.unwrap();
1100
1101 // verify the recursive SNARK
1102 let res = recursive_snark.verify(&pp, num_steps, z0_primary.clone(), z0_secondary.clone());
1103 assert!(res.is_ok());
1104
1105 // produce a compressed SNARK
1106 let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &recursive_snark);
1107 assert!(res.is_ok());
1108 let compressed_snark = res.unwrap();
1109
1110 // verify the compressed SNARK
1111 let res = compressed_snark.verify(&pp, num_steps, z0_primary, z0_secondary);
1112 assert!(res.is_ok());
1113 }
1114
1115 #[test]
1116 fn test_ivc_base() {
1117 // produce public parameters
1118 let pp = PublicParams::<
1119 G1,
1120 G2,
1121 TrivialTestCircuit<<G1 as Group>::Scalar>,
1122 CubicCircuit<<G2 as Group>::Scalar>,
1123 >::setup(TrivialTestCircuit::default(), CubicCircuit::default());
1124
1125 let num_steps = 1;
1126
1127 // produce a recursive SNARK
1128 let res = RecursiveSNARK::prove_step(
1129 &pp,
1130 None,
1131 TrivialTestCircuit::default(),
1132 CubicCircuit::default(),
1133 vec![<G1 as Group>::Scalar::one()],
1134 vec![<G2 as Group>::Scalar::zero()],
1135 );
1136 assert!(res.is_ok());
1137 let recursive_snark = res.unwrap();
1138
1139 // verify the recursive SNARK
1140 let res = recursive_snark.verify(
1141 &pp,
1142 num_steps,
1143 vec![<G1 as Group>::Scalar::one()],
1144 vec![<G2 as Group>::Scalar::zero()],
1145 );
1146 assert!(res.is_ok());
1147
1148 let (zn_primary, zn_secondary) = res.unwrap();
1149
1150 assert_eq!(zn_primary, vec![<G1 as Group>::Scalar::one()]);
1151 assert_eq!(zn_secondary, vec![<G2 as Group>::Scalar::from(5u64)]);
1152 }
1153}