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