| Description | Pasta curve is extensively used in Zk-SNARK, specificially in Halo2, to compose recursive proof. The goal of this project to implement Pasta curve in Coq, Lean, or Dafny and prove the correctness properties, e.g., the prime modulus of Pallas is the group order of Vesta curve. Zcash has published a Rust implementation [1]; also, there is Haskell implementation [2].
[1] https://github.com/zcash/pasta_curves
[2] https://hackage.haskell.org/package/pasta-curves-0.0.1.0/docs/PastaCurves.html |
|---|