Nova/examples/minroot.rs
examples/minroot.rsRaw
1//! Demonstrates how to use Nova to produce a recursive proof of the correct execution of
2//! iterations of the MinRoot function, thereby realizing a Nova-based verifiable delay function (VDF).
3//! We currently execute a single iteration of the MinRoot function per step of Nova's recursion.
4type G1 = pasta_curves::pallas::Point;
5type G2 = pasta_curves::vesta::Point;
6type S1 = nova_snark::spartan_with_ipa_pc::RelaxedR1CSSNARK<G1>;
7type S2 = nova_snark::spartan_with_ipa_pc::RelaxedR1CSSNARK<G2>;
8use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
9use ff::PrimeField;
10use generic_array::typenum::U2;
11use neptune::{
12 circuit::poseidon_hash,
13 poseidon::{Poseidon, PoseidonConstants},
14 Strength,
15};
16use nova_snark::{
17 traits::{Group, StepCircuit},
18 CompressedSNARK, PublicParams, RecursiveSNARK,
19};
20use num_bigint::BigUint;
21use std::marker::PhantomData;
22
23// A trivial test circuit that we will use on the secondary curve
24#[derive(Clone, Debug)]
25struct TrivialTestCircuit<F: PrimeField> {
26 _p: PhantomData<F>,
27}
28
29impl<F> StepCircuit<F> for TrivialTestCircuit<F>
30where
31 F: PrimeField,
32{
33 fn synthesize<CS: ConstraintSystem<F>>(
34 &self,
35 _cs: &mut CS,
36 z: AllocatedNum<F>,
37 ) -> Result<AllocatedNum<F>, SynthesisError> {
38 Ok(z)
39 }
40
41 fn compute(&self, z: &F) -> F {
42 *z
43 }
44}
45
46#[derive(Clone, Debug)]
47struct MinRootCircuit<F: PrimeField> {
48 x_i: F,
49 y_i: F,
50 x_i_plus_1: F,
51 y_i_plus_1: F,
52 pc: PoseidonConstants<F, U2>,
53}
54
55impl<F: PrimeField> MinRootCircuit<F> {
56 // produces a sample non-deterministic advice, executing one invocation of MinRoot per step
57 fn new(num_steps: usize, x_0: &F, y_0: &F, pc: &PoseidonConstants<F, U2>) -> (F, Vec<Self>) {
58 // although this code is written generically, it is tailored to Pallas' scalar field
59 // (p - 3 / 5)
60 let exp = BigUint::parse_bytes(
61 b"23158417847463239084714197001737581570690445185553317903743794198714690358477",
62 10,
63 )
64 .unwrap();
65
66 let mut res = Vec::new();
67 let mut x_i = *x_0;
68 let mut y_i = *y_0;
69 for _i in 0..num_steps {
70 let x_i_plus_1 = (x_i + y_i).pow_vartime(exp.to_u64_digits()); // computes the fifth root of x_i + y_i
71
72 // sanity check
73 let sq = x_i_plus_1 * x_i_plus_1;
74 let quad = sq * sq;
75 let fifth = quad * x_i_plus_1;
76 debug_assert_eq!(fifth, x_i + y_i);
77
78 let y_i_plus_1 = x_i;
79
80 res.push(Self {
81 x_i,
82 y_i,
83 x_i_plus_1,
84 y_i_plus_1,
85 pc: pc.clone(),
86 });
87
88 x_i = x_i_plus_1;
89 y_i = y_i_plus_1;
90 }
91
92 let z0 = Poseidon::<F, U2>::new_with_preimage(&[*x_0, *y_0], pc).hash();
93
94 (z0, res)
95 }
96}
97
98impl<F> StepCircuit<F> for MinRootCircuit<F>
99where
100 F: PrimeField,
101{
102 fn synthesize<CS: ConstraintSystem<F>>(
103 &self,
104 cs: &mut CS,
105 z: AllocatedNum<F>,
106 ) -> Result<AllocatedNum<F>, SynthesisError> {
107 // Allocate four variables for holding non-deterministic advice: x_i, y_i, x_i_plus_1, y_i_plus_1
108 let x_i = AllocatedNum::alloc(cs.namespace(|| "x_i"), || Ok(self.x_i))?;
109 let y_i = AllocatedNum::alloc(cs.namespace(|| "y_i"), || Ok(self.y_i))?;
110 let x_i_plus_1 = AllocatedNum::alloc(cs.namespace(|| "x_i_plus_1"), || Ok(self.x_i_plus_1))?;
111
112 // check that z = hash(x_i, y_i), where z is an output from the prior step
113 let z_hash = poseidon_hash(
114 cs.namespace(|| "input hash"),
115 vec![x_i.clone(), y_i.clone()],
116 &self.pc,
117 )?;
118 cs.enforce(
119 || "z =? z_hash",
120 |lc| lc + z_hash.get_variable(),
121 |lc| lc + CS::one(),
122 |lc| lc + z.get_variable(),
123 );
124
125 // check the following conditions hold:
126 // (i) x_i_plus_1 = (x_i + y_i)^{1/5}, which can be more easily checked with x_i_plus_1^5 = x_i + y_i
127 // (ii) y_i_plus_1 = x_i
128 // (1) constraints for condition (i) are below
129 // (2) constraints for condition (ii) is avoided because we just used x_i wherever y_i_plus_1 is used
130 let x_i_plus_1_sq = x_i_plus_1.square(cs.namespace(|| "x_i_plus_1_sq"))?;
131 let x_i_plus_1_quad = x_i_plus_1_sq.square(cs.namespace(|| "x_i_plus_1_quad"))?;
132 let x_i_plus_1_pow_5 = x_i_plus_1_quad.mul(cs.namespace(|| "x_i_plus_1_pow_5"), &x_i_plus_1)?;
133 cs.enforce(
134 || "x_i_plus_1_pow_5 = x_i + y_i",
135 |lc| lc + x_i_plus_1_pow_5.get_variable(),
136 |lc| lc + CS::one(),
137 |lc| lc + x_i.get_variable() + y_i.get_variable(),
138 );
139
140 // return hash(x_i_plus_1, y_i_plus_1) since Nova circuits expect a single output
141 poseidon_hash(
142 cs.namespace(|| "output hash"),
143 vec![x_i_plus_1, x_i.clone()],
144 &self.pc,
145 )
146 }
147
148 fn compute(&self, z: &F) -> F {
149 // sanity check
150 let z_hash = Poseidon::<F, U2>::new_with_preimage(&[self.x_i, self.y_i], &self.pc).hash();
151 debug_assert_eq!(z, &z_hash);
152
153 // compute output hash using advice
154 Poseidon::<F, U2>::new_with_preimage(&[self.x_i_plus_1, self.y_i_plus_1], &self.pc).hash()
155 }
156}
157
158fn main() {
159 let pc = PoseidonConstants::<<G1 as Group>::Scalar, U2>::new_with_strength(Strength::Standard);
160
161 let circuit_primary = MinRootCircuit {
162 x_i: <G1 as Group>::Scalar::zero(),
163 y_i: <G1 as Group>::Scalar::zero(),
164 x_i_plus_1: <G1 as Group>::Scalar::zero(),
165 y_i_plus_1: <G1 as Group>::Scalar::zero(),
166 pc: pc.clone(),
167 };
168
169 let circuit_secondary = TrivialTestCircuit {
170 _p: Default::default(),
171 };
172
173 // produce public parameters
174 let pp = PublicParams::<
175 G1,
176 G2,
177 MinRootCircuit<<G1 as Group>::Scalar>,
178 TrivialTestCircuit<<G2 as Group>::Scalar>,
179 >::setup(circuit_primary, circuit_secondary.clone());
180
181 // produce non-deterministic advice
182 let num_steps = 3;
183 let (z0_primary, minroot_circuits) = MinRootCircuit::new(
184 num_steps,
185 &<G1 as Group>::Scalar::zero(),
186 &<G1 as Group>::Scalar::one(),
187 &pc,
188 );
189 let z0_secondary = <G2 as Group>::Scalar::zero();
190
191 type C1 = MinRootCircuit<<G1 as Group>::Scalar>;
192 type C2 = TrivialTestCircuit<<G2 as Group>::Scalar>;
193 // produce a recursive SNARK
194 println!("Generating a RecursiveSNARK...");
195 let mut recursive_snark: Option<RecursiveSNARK<G1, G2, C1, C2>> = None;
196
197 for (i, circuit_primary) in minroot_circuits.iter().take(num_steps).enumerate() {
198 let res = RecursiveSNARK::prove_step(
199 &pp,
200 recursive_snark,
201 circuit_primary.clone(),
202 circuit_secondary.clone(),
203 z0_primary,
204 z0_secondary,
205 );
206 assert!(res.is_ok());
207 println!("RecursiveSNARK::prove_step {}: {:?}", i, res.is_ok());
208 recursive_snark = Some(res.unwrap());
209 }
210
211 assert!(recursive_snark.is_some());
212 let recursive_snark = recursive_snark.unwrap();
213
214 // verify the recursive SNARK
215 println!("Verifying a RecursiveSNARK...");
216 let res = recursive_snark.verify(&pp, num_steps, z0_primary, z0_secondary);
217 println!("RecursiveSNARK::verify: {:?}", res.is_ok());
218 assert!(res.is_ok());
219
220 // produce a compressed SNARK
221 println!("Generating a CompressedSNARK...");
222 let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &recursive_snark);
223 println!("CompressedSNARK::prove: {:?}", res.is_ok());
224 assert!(res.is_ok());
225 let compressed_snark = res.unwrap();
226
227 // verify the compressed SNARK
228 println!("Verifying a CompressedSNARK...");
229 let res = compressed_snark.verify(&pp, num_steps, z0_primary, z0_secondary);
230 println!("CompressedSNARK::verify: {:?}", res.is_ok());
231 assert!(res.is_ok());
232}