From f4425e8a1de9cff978f794e4783eff1bcfede412 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 8 Jan 2016 20:09:52 -0500 Subject: cleanup --- src/Galois/EdDSA.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/Galois/EdDSA.v') 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. -- cgit v1.2.3