redo module structure + init curve25519

1 files changed, 21 insertions, 11 deletions

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index 8bc3d6e20..df0b2ce06 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -1,13 +1,23 @@
 
-Require Import ZModulo.
-(**
- * The relevant module is ZModulo:
- *   the constructor you want is of_pos
- *   the operations you want are in zmod_ops
- *   the tactics you want are somewhere between Field and CyclicType:
- *     probs you want to be converting to/from Z pretty frequently
- *
- * Coq Reference page:
- *    https://coq.inria.fr/library/Coq.Numbers.Cyclic.ZModulo.ZModulo.html
- *)
+Require Import Zpower ZArith Znumtheory.
+Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory.
+
+Definition prime25519 : Prime.
+  exists ((two_p 255) - 19).
+  (* <http://safecurves.cr.yp.to/proof/57896044618658097711785492504343953926634992332820282019728792003956564819949.html> *)
+Admitted.
+
+Module Modulus25519 <: Modulus.
+  Definition modulus := prime25519.
+End Modulus25519.
+
+Declare Module GaloisField25519 : GaloisField Modulus25519.
+
+Declare Module GaloisTheory25519 : GaloisFieldTheory Modulus25519 GaloisField25519.
+
+Module Curve25519.
+  Import Modulus25519 GaloisField25519 GaloisTheory25519.
+
+  (* Prove some theorems! *)
+End Curve25519.