You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

324 lines
9.5 KiB

  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 execute a configurable number of iterations of the MinRoot function per step of Nova's recursion.
  4. type G1 = pasta_curves::pallas::Point;
  5. type G2 = pasta_curves::vesta::Point;
  6. use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
  7. use ff::PrimeField;
  8. use generic_array::typenum::U2;
  9. use neptune::{
  10. circuit::poseidon_hash,
  11. poseidon::{Poseidon, PoseidonConstants},
  12. Strength,
  13. };
  14. use nova_snark::{
  15. traits::{Group, StepCircuit},
  16. CompressedSNARK, PublicParams, RecursiveSNARK,
  17. };
  18. use num_bigint::BigUint;
  19. use std::marker::PhantomData;
  20. use std::time::Instant;
  21. #[derive(Clone, Debug)]
  22. struct MinRootIteration<F: PrimeField> {
  23. x_i: F,
  24. y_i: F,
  25. x_i_plus_1: F,
  26. y_i_plus_1: F,
  27. }
  28. impl<F: PrimeField> MinRootIteration<F> {
  29. // produces a sample non-deterministic advice, executing one invocation of MinRoot per step
  30. fn new(num_iters: usize, x_0: &F, y_0: &F, pc: &PoseidonConstants<F, U2>) -> (F, Vec<Self>) {
  31. // although this code is written generically, it is tailored to Pallas' scalar field
  32. // (p - 3 / 5)
  33. let exp = BigUint::parse_bytes(
  34. b"23158417847463239084714197001737581570690445185553317903743794198714690358477",
  35. 10,
  36. )
  37. .unwrap();
  38. let mut res = Vec::new();
  39. let mut x_i = *x_0;
  40. let mut y_i = *y_0;
  41. for _i in 0..num_iters {
  42. let x_i_plus_1 = (x_i + y_i).pow_vartime(exp.to_u64_digits()); // computes the fifth root of x_i + y_i
  43. // sanity check
  44. let sq = x_i_plus_1 * x_i_plus_1;
  45. let quad = sq * sq;
  46. let fifth = quad * x_i_plus_1;
  47. debug_assert_eq!(fifth, x_i + y_i);
  48. let y_i_plus_1 = x_i;
  49. res.push(Self {
  50. x_i,
  51. y_i,
  52. x_i_plus_1,
  53. y_i_plus_1,
  54. });
  55. x_i = x_i_plus_1;
  56. y_i = y_i_plus_1;
  57. }
  58. let z0 = Poseidon::<F, U2>::new_with_preimage(&[*x_0, *y_0], pc).hash();
  59. (z0, res)
  60. }
  61. }
  62. #[derive(Clone, Debug)]
  63. struct MinRootCircuit<F: PrimeField> {
  64. seq: Vec<MinRootIteration<F>>,
  65. pc: PoseidonConstants<F, U2>,
  66. }
  67. impl<F> StepCircuit<F> for MinRootCircuit<F>
  68. where
  69. F: PrimeField,
  70. {
  71. fn synthesize<CS: ConstraintSystem<F>>(
  72. &self,
  73. cs: &mut CS,
  74. z: AllocatedNum<F>,
  75. ) -> Result<AllocatedNum<F>, SynthesisError> {
  76. let mut z_out: Result<AllocatedNum<F>, SynthesisError> = Err(SynthesisError::AssignmentMissing);
  77. for i in 0..self.seq.len() {
  78. // Allocate four variables for holding non-deterministic advice: x_i, y_i, x_i_plus_1, y_i_plus_1
  79. let x_i = AllocatedNum::alloc(cs.namespace(|| format!("x_i_iter_{}", i)), || {
  80. Ok(self.seq[i].x_i)
  81. })?;
  82. let y_i = AllocatedNum::alloc(cs.namespace(|| format!("y_i_iter_{}", i)), || {
  83. Ok(self.seq[i].y_i)
  84. })?;
  85. let x_i_plus_1 =
  86. AllocatedNum::alloc(cs.namespace(|| format!("x_i_plus_1_iter_{}", i)), || {
  87. Ok(self.seq[i].x_i_plus_1)
  88. })?;
  89. // check that z = hash(x_i, y_i), where z is an output from the prior step
  90. if i == 0 {
  91. let z_hash = poseidon_hash(
  92. cs.namespace(|| "input hash"),
  93. vec![x_i.clone(), y_i.clone()],
  94. &self.pc,
  95. )?;
  96. cs.enforce(
  97. || "z =? z_hash",
  98. |lc| lc + z_hash.get_variable(),
  99. |lc| lc + CS::one(),
  100. |lc| lc + z.get_variable(),
  101. );
  102. }
  103. // check the following conditions hold:
  104. // (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
  105. // (ii) y_i_plus_1 = x_i
  106. // (1) constraints for condition (i) are below
  107. // (2) constraints for condition (ii) is avoided because we just used x_i wherever y_i_plus_1 is used
  108. let x_i_plus_1_sq =
  109. x_i_plus_1.square(cs.namespace(|| format!("x_i_plus_1_sq_iter_{}", i)))?;
  110. let x_i_plus_1_quad =
  111. x_i_plus_1_sq.square(cs.namespace(|| format!("x_i_plus_1_quad_{}", i)))?;
  112. let x_i_plus_1_pow_5 = x_i_plus_1_quad.mul(
  113. cs.namespace(|| format!("x_i_plus_1_pow_5_{}", i)),
  114. &x_i_plus_1,
  115. )?;
  116. cs.enforce(
  117. || format!("x_i_plus_1_pow_5 = x_i + y_i_iter_{}", i),
  118. |lc| lc + x_i_plus_1_pow_5.get_variable(),
  119. |lc| lc + CS::one(),
  120. |lc| lc + x_i.get_variable() + y_i.get_variable(),
  121. );
  122. // return hash(x_i_plus_1, y_i_plus_1) since Nova circuits expect a single output
  123. if i == self.seq.len() - 1 {
  124. z_out = poseidon_hash(
  125. cs.namespace(|| "output hash"),
  126. vec![x_i_plus_1, x_i.clone()],
  127. &self.pc,
  128. );
  129. }
  130. }
  131. z_out
  132. }
  133. fn compute(&self, z: &F) -> F {
  134. // sanity check
  135. let z_hash =
  136. Poseidon::<F, U2>::new_with_preimage(&[self.seq[0].x_i, self.seq[0].y_i], &self.pc).hash();
  137. debug_assert_eq!(z, &z_hash);
  138. // compute output hash using advice
  139. let iters = self.seq.len();
  140. Poseidon::<F, U2>::new_with_preimage(
  141. &[
  142. self.seq[iters - 1].x_i_plus_1,
  143. self.seq[iters - 1].y_i_plus_1,
  144. ],
  145. &self.pc,
  146. )
  147. .hash()
  148. }
  149. }
  150. fn main() {
  151. let num_steps = 10;
  152. let num_iters_per_step = 10; // number of iterations of MinRoot per Nova's recursive step
  153. let pc = PoseidonConstants::<<G1 as Group>::Scalar, U2>::new_with_strength(Strength::Standard);
  154. let circuit_primary = MinRootCircuit {
  155. seq: vec![
  156. MinRootIteration {
  157. x_i: <G1 as Group>::Scalar::zero(),
  158. y_i: <G1 as Group>::Scalar::zero(),
  159. x_i_plus_1: <G1 as Group>::Scalar::zero(),
  160. y_i_plus_1: <G1 as Group>::Scalar::zero(),
  161. };
  162. num_iters_per_step
  163. ],
  164. pc: pc.clone(),
  165. };
  166. let circuit_secondary = TrivialTestCircuit {
  167. _p: Default::default(),
  168. };
  169. println!("Nova-based VDF with MinRoot delay function");
  170. println!("==========================================");
  171. println!(
  172. "Proving {} iterations of MinRoot per step",
  173. num_iters_per_step
  174. );
  175. // produce public parameters
  176. println!("Producing public parameters...");
  177. let pp = PublicParams::<
  178. G1,
  179. G2,
  180. MinRootCircuit<<G1 as Group>::Scalar>,
  181. TrivialTestCircuit<<G2 as Group>::Scalar>,
  182. >::setup(circuit_primary, circuit_secondary.clone());
  183. println!(
  184. "Number of constraints per step (primary circuit): {}",
  185. pp.num_constraints().0
  186. );
  187. println!(
  188. "Number of constraints per step (secondary circuit): {}",
  189. pp.num_constraints().1
  190. );
  191. // produce non-deterministic advice
  192. let (z0_primary, minroot_iterations) = MinRootIteration::new(
  193. num_iters_per_step * num_steps,
  194. &<G1 as Group>::Scalar::zero(),
  195. &<G1 as Group>::Scalar::one(),
  196. &pc,
  197. );
  198. let minroot_circuits = (0..num_steps)
  199. .map(|i| MinRootCircuit {
  200. seq: (0..num_iters_per_step)
  201. .map(|j| MinRootIteration {
  202. x_i: minroot_iterations[i * num_iters_per_step + j].x_i,
  203. y_i: minroot_iterations[i * num_iters_per_step + j].y_i,
  204. x_i_plus_1: minroot_iterations[i * num_iters_per_step + j].x_i_plus_1,
  205. y_i_plus_1: minroot_iterations[i * num_iters_per_step + j].y_i_plus_1,
  206. })
  207. .collect::<Vec<_>>(),
  208. pc: pc.clone(),
  209. })
  210. .collect::<Vec<_>>();
  211. let z0_secondary = <G2 as Group>::Scalar::zero();
  212. type C1 = MinRootCircuit<<G1 as Group>::Scalar>;
  213. type C2 = TrivialTestCircuit<<G2 as Group>::Scalar>;
  214. // produce a recursive SNARK
  215. println!("Generating a RecursiveSNARK...");
  216. let mut recursive_snark: Option<RecursiveSNARK<G1, G2, C1, C2>> = None;
  217. for (i, circuit_primary) in minroot_circuits.iter().take(num_steps).enumerate() {
  218. let start = Instant::now();
  219. let res = RecursiveSNARK::prove_step(
  220. &pp,
  221. recursive_snark,
  222. circuit_primary.clone(),
  223. circuit_secondary.clone(),
  224. z0_primary,
  225. z0_secondary,
  226. );
  227. assert!(res.is_ok());
  228. println!(
  229. "RecursiveSNARK::prove_step {}: {:?}, took {:?} ",
  230. i,
  231. res.is_ok(),
  232. start.elapsed()
  233. );
  234. recursive_snark = Some(res.unwrap());
  235. }
  236. assert!(recursive_snark.is_some());
  237. let recursive_snark = recursive_snark.unwrap();
  238. // verify the recursive SNARK
  239. println!("Verifying a RecursiveSNARK...");
  240. let start = Instant::now();
  241. let res = recursive_snark.verify(&pp, num_steps, z0_primary, z0_secondary);
  242. println!(
  243. "RecursiveSNARK::verify: {:?}, took {:?}",
  244. res.is_ok(),
  245. start.elapsed()
  246. );
  247. assert!(res.is_ok());
  248. // produce a compressed SNARK
  249. println!("Generating a CompressedSNARK using Spartan with IPA-PC...");
  250. let start = Instant::now();
  251. type S1 = nova_snark::spartan_with_ipa_pc::RelaxedR1CSSNARK<G1>;
  252. type S2 = nova_snark::spartan_with_ipa_pc::RelaxedR1CSSNARK<G2>;
  253. let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &recursive_snark);
  254. println!(
  255. "CompressedSNARK::prove: {:?}, took {:?}",
  256. res.is_ok(),
  257. start.elapsed()
  258. );
  259. assert!(res.is_ok());
  260. let compressed_snark = res.unwrap();
  261. // verify the compressed SNARK
  262. println!("Verifying a CompressedSNARK...");
  263. let start = Instant::now();
  264. let res = compressed_snark.verify(&pp, num_steps, z0_primary, z0_secondary);
  265. println!(
  266. "CompressedSNARK::verify: {:?}, took {:?}",
  267. res.is_ok(),
  268. start.elapsed()
  269. );
  270. assert!(res.is_ok());
  271. }
  272. // A trivial test circuit that we use on the secondary curve
  273. #[derive(Clone, Debug)]
  274. struct TrivialTestCircuit<F: PrimeField> {
  275. _p: PhantomData<F>,
  276. }
  277. impl<F> StepCircuit<F> for TrivialTestCircuit<F>
  278. where
  279. F: PrimeField,
  280. {
  281. fn synthesize<CS: ConstraintSystem<F>>(
  282. &self,
  283. _cs: &mut CS,
  284. z: AllocatedNum<F>,
  285. ) -> Result<AllocatedNum<F>, SynthesisError> {
  286. Ok(z)
  287. }
  288. fn compute(&self, z: &F) -> F {
  289. *z
  290. }
  291. }