diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-10-22 00:34:18 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-10-22 00:37:11 -0400 |
| commit | 200dbd2af724fb331c210e7282c862e142df16ab (patch) | |
| tree | a554b9cc6fa8d17161f33a85f0357143eb9d09e3 /src/Curves | |
| parent | 06c3554e3ce698d30c2fd1588c5014d1b58fb02b (diff) | |
disable Curve25519 until PointFormats is parametric or we give up and retry
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Curve25519.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index fc6cbb104..8b7c32b5f 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -2,6 +2,8 @@ Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. Require Import Crypto.Curves.PointFormats. +(* +(* FIXME: re-enable when modulus-parametric point formats work *) Definition two_255_19 := (two_p 255) - 19. Lemma two_255_19_prime : prime two_255_19. (* <http://safecurves.cr.yp.to/proof/57896044618658097711785492504343953926634992332820282019728792003956564819949.html>, @@ -16,8 +18,11 @@ Module Modulus25519 <: Modulus. End Modulus25519. Module Curve25519. - Module PointFormats25519 := PointFormats Modulus25519. - Import Modulus25519 PointFormats25519 PointFormats25519.Theory PointFormats25519.Field. + Module PointFormats25519 := PointFormats. + (* Import Modulus25519 PointFormats25519 PointFormats25519.Theory PointFormats25519.Field. *) + Import PointFormats PointFormats.Theory PointFormats.Field. + Import PointFormats.CompleteTwistedEdwardsSpec. + Local Open Scope GF_scope. Definition A : GF := ZToGF 486662. @@ -38,3 +43,4 @@ Module Curve25519. (* TODO(andreser): implement (in PointFormats) recoverX from <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) End Curve25519. +*) |