From bc53758da02d15498f5fb6fc2bb821f4a009cad5 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Wed, 9 Dec 2015 23:20:09 -0500 Subject: More refacoring PointFormats. --- src/Curves/PointFormats.v | 39 ++++++++++++++++----------------------- 1 file changed, 16 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 6ec9aba68..5bc0ecd85 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -2,19 +2,21 @@ Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Tactics.VerdiTactics. -Module Type TwistedEdwardsParams (Import M : Modulus). - Module Export GT := GaloisTheory M. - Open Scope GF_scope. - Definition twistedA := { a : GF | a <> 0 /\ exists sqrt_a, sqrt_a^2 = a }. - Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }. - - Parameter a : twistedA. - Parameter d : twistedD. - - Definition twistedAToGF (a : twistedA) := proj1_sig a. - Coercion twistedAToGF : twistedA >-> GF. - Definition twistedDToGF (d : twistedD) := proj1_sig d. - Coercion twistedDToGF : twistedD >-> GF. +Module TwistedEdwardsDefs (Import M : Modulus). + Module Export GT := GaloisTheory M. + Open Scope GF_scope. + Definition twistedA := { a : GF | a <> 0 /\ exists sqrt_a, sqrt_a^2 = a }. + Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }. + Definition twistedAToGF (a : twistedA) := proj1_sig a. + Coercion twistedAToGF : twistedA >-> GF. + Definition twistedDToGF (d : twistedD) := proj1_sig d. + Coercion twistedDToGF : twistedD >-> GF. +End TwistedEdwardsDefs. + +Module Type TwistedEdwardsParams (M : Modulus). + Module Export D := TwistedEdwardsDefs M. + Parameter a : twistedA. + Parameter d : twistedD. End TwistedEdwardsParams. Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M). @@ -111,21 +113,12 @@ End CompleteTwistedEdwardsFacts. Module Minus1Twisted (Import M : Modulus). Module Minus1Params <: TwistedEdwardsParams M. - Module Export GT := GaloisTheory M. - Open Scope GF_scope. + Module Export D := TwistedEdwardsDefs M. Definition isSquareAndNonzero (a : GF) := a <> 0 /\ exists sqrt_a, sqrt_a^2 = a. - Definition twistedA := { a : GF | isSquareAndNonzero a }. - Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }. - Axiom minusOneIsSquareAndNonzero : isSquareAndNonzero (0 - 1). Definition a : twistedA := exist _ _ minusOneIsSquareAndNonzero. Parameter d : twistedD. - - Definition twistedAToGF (a : twistedA) := proj1_sig a. - Coercion twistedAToGF : twistedA >-> GF. - Definition twistedDToGF (d : twistedD) := proj1_sig d. - Coercion twistedDToGF : twistedD >-> GF. End Minus1Params. Import Minus1Params. -- cgit v1.2.3