diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
| commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
| tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Spec/Ed25519.v | |
| parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) | |
rename-everything
Diffstat (limited to 'src/Spec/Ed25519.v')
| -rw-r--r-- | src/Spec/Ed25519.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 2a2847a31..b8526bb0e 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -2,7 +2,8 @@ Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Spec.EdDSA. -Require ModularArithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *) +Require Crypto.Arithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *) +Require Crypto.Curves.Edwards.AffineProofs. (* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q. @@ -83,7 +84,7 @@ Section Ed25519. Definition ed25519 (l_order_B: E.eq(F:=Fq)(Fone:=F.one) (mul (BinInt.Z.to_nat l) B)%E zero) : EdDSA (E:=E) (Eadd:=add) (Ezero:=zero) (EscalarMult:=mul) (B:=B) - (Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *) + (Eopp:=Crypto.Curves.Edwards.AffineProofs.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *) (Eeq:=E.eq) (* TODO: move defn *) (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512). |