diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-01-08 20:09:52 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-01-08 20:09:52 -0500 |
| commit | f4425e8a1de9cff978f794e4783eff1bcfede412 (patch) | |
| tree | e250b5c13cd4610a8c4411465c7c9b5e33309c12 /src/Galois/EdDSA.v | |
| parent | bb4c8e7d281279eb9aeb44c5d0de5be1d022028c (diff) | |
cleanup
Diffstat (limited to 'src/Galois/EdDSA.v')
| -rw-r--r-- | src/Galois/EdDSA.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index af4f892ca..de26c678c 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -1,7 +1,7 @@ Require Import ZArith NPeano. Require Import Bedrock.Word. Require Import Crypto.Curves.PointFormats. -Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. +Require Import Crypto.Galois.BaseSystem Crypto.Galois.ZGaloisField Crypto.Galois.GaloisTheory. Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import VerdiTactics. @@ -54,7 +54,7 @@ Module Type EdDSAParams. Axiom n_ge_c : n >= c. Axiom n_le_b : n <= b. - Module Import GFDefs := GaloisDefs Modulus_q. + Module Import GFDefs := ZGaloisField Modulus_q. Local Open Scope GF_scope. (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit @@ -83,6 +83,8 @@ Module Type EdDSAParams. * twisted Edwards addition law. *) Module CurveParameters <: TwistedEdwardsParams Modulus_q. Module GFDefs := GFDefs. + Definition char_gt_2 : inject 2 <> 0. + Admitted. (* follows from q_odd *) Definition a : GF := a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. |