diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | .make/cc.mk | 20 | ||||
| -rw-r--r-- | .make/coq.mk | 28 | ||||
| -rw-r--r-- | Makefile | 30 | ||||
| -rw-r--r-- | _CoqProject | 22 | ||||
| -rw-r--r-- | src/Curves/Curve25519.v | 14 | ||||
| -rw-r--r-- | src/Curves/PointFormats.v | 6 | ||||
| -rw-r--r-- | src/Galois/AbstractGaloisField.v | 14 | ||||
| -rw-r--r-- | src/Galois/ComputationalGaloisField.v | 52 | ||||
| -rw-r--r-- | src/Galois/EdDSA.v | 13 | ||||
| -rw-r--r-- | src/Galois/Galois.v | 54 | ||||
| -rw-r--r-- | src/Galois/GaloisField.v (renamed from src/Galois/ZGaloisField.v) | 38 | ||||
| -rw-r--r-- | src/Galois/GaloisRep.v | 3 | ||||
| -rw-r--r-- | src/Galois/GaloisTheory.v | 57 | ||||
| -rw-r--r-- | src/Galois/GaloisTutorial.v (renamed from src/Galois/GaloisExamples.v) | 44 | ||||
| -rw-r--r-- | src/Galois/ModularBaseSystem.v | 15 | ||||
| -rw-r--r-- | src/Rep/BinGF.v | 139 | ||||
| -rw-r--r-- | src/Rep/ECRep.v | 12 | ||||
| -rw-r--r-- | src/Rep/GaloisRep.v | 8 | ||||
| -rw-r--r-- | src/Specific/EdDSA25519.v | 12 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
21 files changed, 216 insertions, 370 deletions
diff --git a/.gitignore b/.gitignore index cec91e9a6..ff148cbf2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,6 @@ bedrock fiat *~ +*.vo +*.d +Makefile.coq diff --git a/.make/cc.mk b/.make/cc.mk deleted file mode 100644 index 58724089a..000000000 --- a/.make/cc.mk +++ /dev/null @@ -1,20 +0,0 @@ -# © 2012–2015 the Massachusetts Institute of Technology -# @author bbaren - -CC = clang -CXX = clang++ - -CPPFLAGS = \ - -Wall \ - -D_FORTIFY_SOURCE=2 - -CXXFLAGS = \ - -std=c++11 \ - -ftrapv \ - -fstack-protector-strong --param=ssp-buffer-size=4 \ - -fPIC \ - -O2 -g \ - -ffunction-sections -fdata-sections \ - -Weverything -Wno-c++98-compat - -LDFLAGS = -fPIE -pie diff --git a/.make/coq.mk b/.make/coq.mk deleted file mode 100644 index bab225be7..000000000 --- a/.make/coq.mk +++ /dev/null @@ -1,28 +0,0 @@ -# © 2012–2015 the Massachusetts Institute of Technology -# @author bbaren + rsloan - -COQC = coqc -COQDEP = coqdep - -COMPILE.v = $(COQC) -q $(COQLIBS) - -.PHONY: check_fiat check_bedrock - -check_fiat: - @perl -e \ - 'if(! -d "./fiat") { print("you need to link fiat to ./fiat\n"); exit(1) }' - -check_bedrock: - @perl -e \ - 'if(! -d "./bedrock") { print("you need to link bedrock to ./bedrock\n"); exit(1) }' - -%.vo %.glob: %.v.d - $(COMPILE.v) $* - -%.v.d: %.v - @$(COQDEP) -I . $(COQLIBS) "$<" >"$@" \ - || (RV=$$?; rm -f "$@"; exit $${RV}) - -define coq-generated -$1.vo $1.v.d $1.glob -endef @@ -1,19 +1,25 @@ -# © 2015 the Massachusetts Institute of Technology -# @author bbaren + rsloan +COQ_ARGS := -R fiat/src Fiat -R bedrock/Bedrock Bedrock +MOD_NAME := Crypto +SRC_DIR := src +MODULES := Curves Galois Rep Specific Tactics Util -SOURCES := $(shell grep -v '^-' _CoqProject | tr '\n' ' ') -COQLIBS := $(shell grep '^-' _CoqProject | tr '\n' ' ') +VS := $(MODULES:%=src/%/*.v) -include .make/cc.mk -include .make/coq.mk +.PHONY: coq clean install +.DEFAULT_GOAL: coq -FAST_TARGETS += check_fiat check_bedrock clean +coq: Makefile.coq + $(MAKE) -f Makefile.coq -.DEFAULT_GOAL = all -.PHONY: clean coquille +Makefile.coq: Makefile $(VS) + coq_makefile -R $(SRC_DIR) $(MOD_NAME) $(COQ_ARGS) $(VS) -o Makefile.coq -all: check_fiat check_bedrock $(SOURCES:%=%o) +clean: Makefile.coq + $(MAKE) -f Makefile.coq clean + rm -f Makefile.coq -clean: - $(RM) $(foreach f,$(SOURCES),$(call coq-generated,$(basename $f))) +install: coq + ln -sfL $(shell pwd)/src $(shell coqtop -where)/user-contrib/Crypto + ln -sfL $(shell pwd)/fiat/src $(shell coqtop -where)/user-contrib/Fiat + ln -sfL $(shell pwd)/bedrock/Bedrock $(shell coqtop -where)/user-contrib/Bedrock diff --git a/_CoqProject b/_CoqProject deleted file mode 100644 index a99d9a3f7..000000000 --- a/_CoqProject +++ /dev/null @@ -1,22 +0,0 @@ --R src Crypto --R fiat/src Fiat --R bedrock/Bedrock Bedrock -src/Tactics/VerdiTactics.v -src/Util/CaseUtil.v -src/Util/ListUtil.v -src/Util/NatUtil.v -src/Util/ZUtil.v -src/Util/NumTheoryUtil.v -src/Galois/Galois.v -src/Galois/GaloisTheory.v -src/Galois/ZGaloisField.v -src/Galois/GaloisExamples.v -src/Galois/AbstractGaloisField.v -src/Galois/ComputationalGaloisField.v -src/Galois/BaseSystem.v -src/Galois/ModularBaseSystem.v -src/Curves/PointFormats.v -src/Galois/EdDSA.v -src/Assembly/WordBounds.v -src/Curves/Curve25519.v -src/Specific/GF25519.v diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index 8bb2148db..38aed1924 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -1,5 +1,5 @@ Require Import Zpower ZArith Znumtheory. -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. +Require Import Crypto.Galois.GaloisField. Require Import Crypto.Curves.PointFormats. Definition two_255_19 := 2^255 - 19. (* <http://safecurves.cr.yp.to/primeproofs.html> *) @@ -9,9 +9,8 @@ Module Modulus25519 <: Modulus. End Modulus25519. Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519. - Module Import GFDefs := GaloisDefs Modulus25519. + Module Import GFDefs := GaloisField Modulus25519. Local Open Scope GF_scope. - Coercion inject : Z >-> GF. Definition a : GF := -1. Definition d : GF := -121665 / 121666. @@ -21,10 +20,10 @@ Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Mod discriminate. Qed. - Lemma a_square : exists x, x * x = a. + Definition sqrt_a: GF := 19681161376707505956807079304988542015446066515923890162744021073123829784752. + + Lemma a_square : sqrt_a^2 = a. Proof. - unfold a. - exists 19681161376707505956807079304988542015446066515923890162744021073123829784752. (* vm_compute runs out of memory. *) Admitted. @@ -48,6 +47,9 @@ Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Mod *) Definition basepointY := 4 / 5. + + Definition char_gt_2: (1+1) <> 0. + Admitted. End Curve25519Params. Module Edwards25519 := CompleteTwistedEdwardsCurve Modulus25519 Curve25519Params. diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 7e1fd0f81..1d9a19780 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -1,10 +1,10 @@ -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ZGaloisField. +Require Import Crypto.Galois.GaloisTheory Crypto.Galois.GaloisField. Require Import Tactics.VerdiTactics. Require Import Logic.Eqdep_dec. Require Import BinNums NArith. Module Type TwistedEdwardsParams (M : Modulus). - Module Export GFDefs := ZGaloisField M. + Module Export GFDefs := GaloisField M. Local Open Scope GF_scope. Axiom char_gt_2 : (1+1) <> 0. Parameter a : GF. @@ -538,7 +538,7 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. - Module Export GFDefs := ZGaloisField M. + Module Export GFDefs := GaloisField M. Local Open Scope GF_scope. Axiom char_gt_2 : (1+1) <> 0. Definition a := inject (- 1). diff --git a/src/Galois/AbstractGaloisField.v b/src/Galois/AbstractGaloisField.v deleted file mode 100644 index 12a9af80d..000000000 --- a/src/Galois/AbstractGaloisField.v +++ /dev/null @@ -1,14 +0,0 @@ - -Require Import BinInt BinNat ZArith Znumtheory. -Require Import Eqdep_dec. -Require Import Tactics.VerdiTactics. -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. - -Module AbstractGaloisField (M: Modulus). - Module G := Galois M. - Module T := GaloisTheory M. - Export M G T. - - Add Field GFfield_computational : GFfield_theory - (power_tac GFpower_theory [GFexp_tac]). -End AbstractGaloisField. diff --git a/src/Galois/ComputationalGaloisField.v b/src/Galois/ComputationalGaloisField.v deleted file mode 100644 index e83e22fea..000000000 --- a/src/Galois/ComputationalGaloisField.v +++ /dev/null @@ -1,52 +0,0 @@ - -Require Import BinInt BinNat ZArith Znumtheory. -Require Import Eqdep_dec. -Require Import Tactics.VerdiTactics. -Require Import Galois GaloisTheory. - -Module ComputationalGaloisField (M: Modulus). - Module G := Galois M. - Module T := GaloisTheory M. - Export M G T. - - Ltac isModulusConstant := - let hnfModulus := eval hnf in (proj1_sig modulus) - in match (isZcst hnfModulus) with - | NotConstant => NotConstant - | _ => match hnfModulus with - | Z.pos _ => true - | _ => false - end - end. - - Ltac isGFconstant t := - match t with - | GFzero => true - | GFone => true - | ZToGF _ => isModulusConstant - | exist _ ?z _ => match (isZcst z) with - | NotConstant => NotConstant - | _ => isModulusConstant - end - | _ => NotConstant - end. - - Ltac GFconstants t := - match isGFconstant t with - | NotConstant => NotConstant - | _ => t - end. - - Add Ring GFring_computational : GFring_theory - (decidable GFdecidable, - constants [GFconstants], - div GFdiv_theory, - power_tac GFpower_theory [GFexp_tac]). - - Add Field GFfield_computational : GFfield_theory - (decidable GFdecidable, - completeness GFcomplete, - constants [GFconstants], - div GFdiv_theory, - power_tac GFpower_theory [GFexp_tac]). -End ComputationalGaloisField. diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index af4f892ca..68b8867b8 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.GaloisField. 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 := GaloisField Modulus_q. Local Open Scope GF_scope. (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit @@ -66,8 +66,9 @@ Module Type EdDSAParams. * on average to determine an EdDSA secret key from an EdDSA public key *) Parameter a : GF. + Parameter sqrt_a : GF. Axiom a_nonzero : a <> 0%GF. - Axiom a_square : exists x, x * x = a. + Axiom a_square : sqrt_a^2 = a. (* The usual recommendation for best performance is a = −1 if q mod 4 = 1, * and a = 1 if q mod 4 = 3. * The original specification of EdDSA did not include this parameter: @@ -81,11 +82,17 @@ Module Type EdDSAParams. (* E = {(x, y) \in Fq x Fq : ax^2 + y^2 = 1 + dx^2y^2}. * This set forms a group with neutral element 0 = (0, 1) under the * twisted Edwards addition law. *) + + (* We have an odd prime *) + Axiom char_gt_2: 1+1 <> 0. + Module CurveParameters <: TwistedEdwardsParams Modulus_q. Module GFDefs := GFDefs. Definition a : GF := a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. + Definition char_gt_2 := char_gt_2. + Definition sqrt_a := sqrt_a. Definition d := d. Definition d_nonsquare := d_nonsquare. End CurveParameters. diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v index 4fd151d36..86ce7f05e 100644 --- a/src/Galois/Galois.v +++ b/src/Galois/Galois.v @@ -3,24 +3,59 @@ Require Import BinInt BinNat ZArith Znumtheory. Require Import Eqdep_dec. Require Import Tactics.VerdiTactics. +(* This file is for the high-level type definitions of + * GF, Primes, Moduli, etc. and their notations and essential + * operations. + * + * The lemmas required for the ring and field theories are + * in GaloisTheory.v and the actual tactic implementations + * for the field are in GaloisField.v. An introduction to the + * use of our implementation of the Galois field is in + * GaloisTutorial.v + *) + Section GaloisPreliminaries. + (* The core prime modulus type, relying on Znumtheory's prime *) Definition Prime := {x: Z | prime x}. + (* Automagically coerce primes to Z *) Definition primeToZ(x: Prime) := proj1_sig x. Coercion primeToZ: Prime >-> Z. End GaloisPreliminaries. +(* A module to hold the field's modulus, which will be an argument to + * all of our Galois modules. + *) Module Type Modulus. Parameter modulus: Prime. End Modulus. +(* The core Galois Field model *) Module Galois (M: Modulus). Import M. + (* The sigma definition of an element of the field: we have + * an element corresponding to the values in Z which can be + * produced by a 'mod' operation. + *) Definition GF := {x: Z | x = x mod modulus}. + + Delimit Scope GF_scope with GF. + Local Open Scope GF_scope. + + (* Automagically convert GF to Z when needed *) Definition GFToZ(x: GF) := proj1_sig x. Coercion GFToZ: GF >-> Z. + (* Automagically convert Z to GF when needed *) + Definition inject(x: Z): GF. + exists (x mod modulus). + abstract (rewrite Zmod_mod; trivial). + Defined. + + Coercion inject : Z >-> GF. + + (* Convert Z to GF without a mod operation, for when the modulus is opaque *) Definition ZToGF (x: Z) : if ((0 <=? x) && (x <? modulus))%bool then GF else True. break_if; [|trivial]. exists x. @@ -31,6 +66,7 @@ Module Galois (M: Modulus). - rewrite <- Z.ltb_lt; auto. Defined. + (* Core lemma: equality in GF implies equality in Z *) Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y. Proof. destruct x, y; intuition; simpl in *; try congruence. @@ -40,7 +76,7 @@ Module Galois (M: Modulus). apply Z.eq_dec. Qed. - (* Elementary operations *) + (* Core values: One and Zero *) Definition GFzero: GF. exists 0. abstract trivial. @@ -60,6 +96,7 @@ Module Galois (M: Modulus). Qed. Hint Resolve GFone_nonzero. + (* Elementary operations: +, -, * *) Definition GFplus(x y: GF): GF. exists ((x + y) mod modulus); abstract (rewrite Zmod_mod; trivial). @@ -77,7 +114,7 @@ Module Galois (M: Modulus). Definition GFopp(x: GF): GF := GFminus GFzero x. - (* Totient Preliminaries *) + (* Modular exponentiation *) Fixpoint GFexp' (x: GF) (power: positive) := match power with | xH => x @@ -91,12 +128,13 @@ Module Galois (M: Modulus). | Npos power' => GFexp' x power' end. - (* Inverses + division derived from the existence of a totient *) + (* Preliminaries to inversion in a prime field *) Definition isTotient(e: N) := N.gt e 0 /\ forall g: GF, g <> GFzero -> GFexp g e = GFone. Definition Totient := {e: N | isTotient e}. + (* Get a totient via Fermat's little theorem *) Theorem fermat_little_theorem: isTotient (N.pred (Z.to_N modulus)). Admitted. @@ -108,8 +146,18 @@ Module Galois (M: Modulus). Definition totientToN(x: Totient) := proj1_sig x. Coercion totientToN: Totient >-> N. + (* Define inversion and division *) Definition GFinv(x: GF): GF := GFexp x (N.pred totient). Definition GFdiv(x y: GF): GF := GFmult x (GFinv y). + (* Notations for all of the operations we just made *) + Notation "1" := GFone : GF_scope. + Notation "0" := GFzero : GF_scope. + Infix "+" := GFplus : GF_scope. + Infix "-" := GFminus : GF_scope. + Infix "*" := GFmult : GF_scope. + Infix "/" := GFdiv : GF_scope. + Infix "^" := GFexp : GF_scope. + End Galois. diff --git a/src/Galois/ZGaloisField.v b/src/Galois/GaloisField.v index a554e826a..d87e35dc4 100644 --- a/src/Galois/ZGaloisField.v +++ b/src/Galois/GaloisField.v @@ -1,13 +1,27 @@ Require Import BinInt BinNat ZArith Znumtheory. Require Import BoolEq Field_theory. -Require Import Galois GaloisTheory. -Require Import Tactics.VerdiTactics. +Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory. +Require Import Crypto.Tactics.VerdiTactics. -Module ZGaloisField (M: Modulus). +(* This file is for the actual field tactics and some specialized + * morphisms that help field operate. + * + * When you want a Galois Field, this is the /only module/ you + * should import, because it automatically pulls in everything + * from Galois and the Modulus. + *) +Module GaloisField (M: Modulus). Module G := Galois M. Module T := GaloisTheory M. Export M G T. + (* Define a "ring morphism" between GF and Z, i.e. an equivalence + * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'. + * + * Doing this allows us to do our coefficient manipulations in Z + * rather than GF, because we know it's equivalent to inject the + * result afterward. + *) Lemma GFring_morph: ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool @@ -26,6 +40,7 @@ Module ZGaloisField (M: Modulus). symmetry; apply Zeq_bool_eq; trivial. Qed. + (* Redefine our division theory under the ring morphism *) Lemma GFmorph_div_theory: div_theory eq Zplus Zmult inject Z.quotrem. Proof. @@ -38,6 +53,7 @@ Module ZGaloisField (M: Modulus). destruct a; simpl; trivial. Qed. + (* Some simple utility lemmas *) Lemma injectZeroIsGFZero : GFzero = inject 0. Proof. @@ -57,10 +73,18 @@ Module ZGaloisField (M: Modulus). intuition; solve_by_inversion. Qed. + (* Change all GFones to (inject 1) and GFzeros to (inject 0) so that + * we can use our ring morphism to simplify them + *) Ltac GFpreprocess := repeat rewrite injectZeroIsGFZero; repeat rewrite injectOneIsGFOne. + (* Split up the equation (because field likes /\, then + * change back all of our GFones and GFzeros. + * + * TODO (adamc): what causes it to generate these subproofs? + *) Ltac GFpostprocess := repeat split; repeat match goal with [ |- context[exist ?a ?b (inject_subproof ?x)] ] => @@ -69,18 +93,21 @@ Module ZGaloisField (M: Modulus). repeat rewrite <- injectZeroIsGFZero; repeat rewrite <- injectOneIsGFOne. + (* Tactic to passively convert from GF to Z in special circumstances *) Ltac GFconstant t := match t with | inject ?x => x | _ => NotConstant end. + (* Add our ring with all the fixin's *) Add Ring GFring_Z : GFring_theory (morphism GFring_morph, constants [GFconstant], div GFmorph_div_theory, - power_tac GFpower_theory [GFexp_tac]). + power_tac GFpower_theory [GFexp_tac]). + (* Add our field with all the fixin's *) Add Field GFfield_Z : GFfield_theory (morphism GFring_morph, preprocess [GFpreprocess], @@ -88,4 +115,5 @@ Module ZGaloisField (M: Modulus). constants [GFconstant], div GFmorph_div_theory, power_tac GFpower_theory [GFexp_tac]). -End ZGaloisField. + +End GaloisField. diff --git a/src/Galois/GaloisRep.v b/src/Galois/GaloisRep.v index 027d0d27e..4f4dce486 100644 --- a/src/Galois/GaloisRep.v +++ b/src/Galois/GaloisRep.v @@ -1,5 +1,6 @@ -Module Type GaloisRep (). +Module Type GaloisRep . End GaloisRep. + diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v index 3cfa0323c..bef7fbe03 100644 --- a/src/Galois/GaloisTheory.v +++ b/src/Galois/GaloisTheory.v @@ -8,21 +8,14 @@ Require Export Crypto.Galois.Galois. Set Implicit Arguments. Unset Strict Implicits. +(* This file is for all the lemmas we need to construct a ring, + * field, power, and division theory on a Galois Field. + *) Module GaloisTheory (M: Modulus). Module G := Galois M. Export M G. - (* Notations *) - Delimit Scope GF_scope with GF. - Notation "1" := GFone : GF_scope. - Notation "0" := GFzero : GF_scope. - Infix "+" := GFplus : GF_scope. - Infix "-" := GFminus : GF_scope. - Infix "*" := GFmult : GF_scope. - Infix "/" := GFdiv : GF_scope. - Infix "^" := GFexp : GF_scope. - - (* Basic Properties *) + (***** Preliminary Tactics *****) (* Fails iff the input term does some arithmetic with mod'd values. *) Ltac notFancy E := @@ -76,6 +69,7 @@ Module GaloisTheory (M: Modulus). end; simpl in *; autorewrite with core; intuition; demod; try solve [ f_equal; intuition ]. + (* Automatically unfold the definition of Z *) Lemma modmatch_eta : forall n, match n with | 0 => 0 @@ -88,10 +82,11 @@ Module GaloisTheory (M: Modulus). Hint Rewrite Zmod_mod modmatch_eta. - (* Ring Theory*) - + (* Substitution to prove all Compats *) Ltac compat := repeat intro; subst; trivial. + (***** Ring Theory *****) + Instance GFplus_compat : Proper (eq==>eq==>eq) GFplus. Proof. compat. @@ -117,10 +112,11 @@ Module GaloisTheory (M: Modulus). constructor; galois. Qed. - (* Power theory *) + (***** Power theory *****) Local Open Scope GF_scope. + (* Separate two of the same base *) Lemma GFexp'_doubling : forall q r0, GFexp' (r0 * r0) q = GFexp' r0 q * GFexp' r0 q. Proof. induction q; simpl; intuition. @@ -129,6 +125,7 @@ Module GaloisTheory (M: Modulus). apply Zmod_eq; ring. Qed. + (* Equivalence with pow_pos for subroutine of GFexp *) Lemma GFexp'_correct : forall r p, GFexp' r p = pow_pos GFmult r p. Proof. induction p; simpl; intuition; @@ -137,12 +134,14 @@ Module GaloisTheory (M: Modulus). Hint Immediate GFexp'_correct. + (* Equivalence with pow_pos for GFexp *) Lemma GFexp_correct : forall r n, r^n = pow_N 1 GFmult r n. Proof. induction n; simpl; intuition. Qed. + (* Equivalence with pow_pos for GFexp with identity (a utility lemma) *) Lemma GFexp_correct' : forall r n, r^id n = pow_N 1 GFmult r n. Proof. @@ -156,10 +155,11 @@ Module GaloisTheory (M: Modulus). constructor; auto. Qed. - (* Ring properties *) + (***** Additional tricks for Ring *****) Ltac GFexp_tac t := Ncst t. + (* Decideability *) Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y. Proof. intros; galois. @@ -167,6 +167,7 @@ Module GaloisTheory (M: Modulus). trivial. Qed. + (* Completeness *) Lemma GFcomplete : forall (x y: GF), x = y -> Zeq_bool x y = true. Proof. intros. @@ -174,40 +175,45 @@ Module GaloisTheory (M: Modulus). galois. Qed. - (* Division Theory *) - Definition inject(x: Z): GF. - exists (x mod modulus). - abstract (demod; trivial). - Defined. + (***** Division Theory *****) + (* Compatibility between inject and addition *) Lemma inject_distr_add : forall (m n : Z), inject (m + n) = inject m + inject n. Proof. galois. Qed. + (* Compatibility between inject and subtraction *) Lemma inject_distr_sub : forall (m n : Z), inject (m - n) = inject m - inject n. Proof. galois. Qed. + (* Compatibility between inject and multiplication *) Lemma inject_distr_mul : forall (m n : Z), inject (m * n) = inject m * inject n. Proof. galois. Qed. + (* Compatibility between inject and GFtoZ *) Lemma inject_eq : forall (x : GF), inject x = x. Proof. galois. Qed. + (* Compatibility between inject and mod *) Lemma inject_mod_eq : forall x, inject x = inject (x mod modulus). Proof. galois. Qed. + (* The main division theory: + * equivalence between division and quotrem (euclidean division) + *) + Definition GFquotrem(a b: GF): GF * GF := match (Z.quotrem a b) with | (q, r) => (inject q, inject r) @@ -225,13 +231,13 @@ Module GaloisTheory (M: Modulus). destruct a; simpl; trivial. Qed. - (* Now add the ring with all modifiers *) + (***** Field Theory *****) + (* First, add the modifiers to our ring *) Add Ring GFring0 : GFring_theory (power_tac GFpower_theory [GFexp_tac]). - (* Field Theory*) - + (* Utility lemmas for multiplicative inverses *) Lemma GFexp'_pred' : forall x p, GFexp' p (Pos.succ x) = GFexp' p x * p. Proof. @@ -258,6 +264,7 @@ Module GaloisTheory (M: Modulus). destruct p0; intuition. Qed. + (* Show that GFinv actually defines multiplicative inverses *) Lemma GF_multiplicative_inverse : forall p, p <> 0 -> GFinv p * p = 1. @@ -269,11 +276,13 @@ Module GaloisTheory (M: Modulus). eapply N.lt_irrefl; eauto using N.gt_lt. Qed. + (* Compatibility of inverses and equality *) Instance GFinv_compat : Proper (eq==>eq) GFinv. Proof. compat. Qed. + (* Compatibility of division and equality *) Instance GFdiv_compat : Proper (eq==>eq==>eq) GFdiv. Proof. compat. @@ -283,9 +292,11 @@ Module GaloisTheory (M: Modulus). Local Hint Extern 1 False => discriminate. + (* Add an abstract field (without modifiers) *) Definition GFfield_theory : field_theory GFzero GFone GFplus GFmult GFminus GFopp GFdiv GFinv eq. Proof. constructor; auto. Qed. + End GaloisTheory. diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisTutorial.v index 12bcfa2c8..4bab0b829 100644 --- a/src/Galois/GaloisExamples.v +++ b/src/Galois/GaloisTutorial.v @@ -1,16 +1,20 @@ Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.ZGaloisField. +Require Import Crypto.Galois.GaloisField. +(* First, we define our prime in Z*) Definition two_5_1 := (two_p 5) - 1. +Definition two_127_1 := (two_p 127) - 1. + +(* Then proofs of their primality *) Lemma two_5_1_prime : prime two_5_1. Admitted. -Definition two_127_1 := (two_p 127) - 1. Lemma two_127_1_prime : prime two_127_1. Admitted. +(* And use those to make modulus modules *) Module Modulus31 <: Modulus. Definition modulus := exist _ two_5_1 two_5_1_prime. End Modulus31. @@ -20,38 +24,40 @@ Module Modulus127_1 <: Modulus. End Modulus127_1. Module Example31. - Module Theory := ZGaloisField Modulus31. - Import Theory. + (* Then we can construct a field with that modulus *) + Module Field := GaloisField Modulus31. + Import Field. + + (* And pull in the appropriate notations *) Local Open Scope GF_scope. - Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2). + (* First, let's solve a ring example*) + Lemma ring_example: forall x: GF, x * 2 = x + x. Proof. - intros; simpl. - field; trivial. + intros. + ring. Qed. - Lemma example2: forall x: GF, x * (inject 2) = x + x. + (* Then a field example (we have to know we can't divide by zero!) *) + Lemma field_example: forall x y z: GF, z <> 0 -> + x * (y / z) / z = x * y / (z ^ 2). Proof. intros; simpl. - field. + field; trivial. Qed. - Lemma example3: forall x: GF, x ^ 2 + (inject 2) * x + (inject 1) = (x + (inject 1)) ^ 2. + (* Then an example with exponentiation *) + Lemma exp_example: forall x: GF, x ^ 2 + 2 * x + 1 = (x + 1) ^ 2. Proof. intros; simpl. field; trivial. Qed. - Lemma example4: forall x: GF, x/(inject 1) = x. - Proof. - intros; field. - discriminate. - Qed. - End Example31. +(* Notice that the field tactics work whether we know what the modulus is *) Module TimesZeroTransparentTestModule. - Module Theory := ZGaloisField Modulus127_1. + Module Theory := GaloisField Modulus127_1. Import Theory. Local Open Scope GF_scope. @@ -61,8 +67,9 @@ Module TimesZeroTransparentTestModule. Qed. End TimesZeroTransparentTestModule. +(* Or if we don't (i.e. it's opaque) *) Module TimesZeroParametricTestModule (M: Modulus). - Module Theory := ZGaloisField M. + Module Theory := GaloisField M. Import Theory. Local Open Scope GF_scope. @@ -71,3 +78,4 @@ Module TimesZeroParametricTestModule (M: Modulus). field. Qed. End TimesZeroParametricTestModule. + diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v index 5a97d67c9..7df44ba7b 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/Galois/ModularBaseSystem.v @@ -1,6 +1,6 @@ Require Import Zpower ZArith. Require Import List. -Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. +Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisField. Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import VerdiTactics. Local Open Scope Z_scope. @@ -35,8 +35,9 @@ Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus). End PseudoMersenneBaseParams. Module Type GFrep (Import M:Modulus). - Module Import GF := GaloisTheory M. - (* TODO: could GF notation be in Galois, not GaloisTheory *) + Module Field := GaloisField M. + Import Field. + Parameter T : Type. Parameter fromGF : GF -> T. Parameter toGF : T -> GF. @@ -58,7 +59,9 @@ Module Type GFrep (Import M:Modulus). End GFrep. Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBaseParams BC M) <: GFrep M. - Module Import GF := GaloisTheory M. + Module Field := GaloisField M. + Import Field. + Module EC <: BaseCoefs. Definition base := BC.base ++ (map (Z.mul (2^(P.k))) BC.base). @@ -211,7 +214,7 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara Definition T := B.digits. Local Hint Unfold T. - Definition toGF (us : T) : GF := GF.inject (B.decode us). + Definition toGF (us : T) : GF := inject (B.decode us). Local Hint Unfold toGF. Definition rep (us : T) (x : GF) := (length us <= length BC.base)%nat /\ toGF us = x. Local Notation "u '~=' x" := (rep u x) (at level 70). @@ -233,7 +236,7 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara } { unfold toGF. rewrite B.encode_rep. - rewrite GF.inject_eq; auto. + rewrite inject_eq; auto. } Qed. diff --git a/src/Rep/BinGF.v b/src/Rep/BinGF.v deleted file mode 100644 index 138277870..000000000 --- a/src/Rep/BinGF.v +++ /dev/null @@ -1,139 +0,0 @@ - -Require Import ZArith. -Require Import Bedrock.Word. -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.ZGaloisField. -Require Import Eqdep_dec. - -Module Type BitSpec. - Parameter wordSize: nat. - Parameter numWords: nat. - - Axiom wordSize_pos : (wordSize > 0)%nat. -End BitSpec. - -Module GFBits (M: Modulus) (Spec: BitSpec). - Module Field := ZGaloisField M. - Import Field Spec. - Local Open Scope GF_scope. - Local Open Scope list. - - Definition bits {k} (x: word k) := k. - - Definition BinGF := {lst: list (word wordSize) | length lst = numWords}. - - Definition splitGt {n m} {H : (n > m)%nat} (w : word n) : word m * word (n - m). - Proof. - refine (let w' := match _ : (n = m + (n - m))%nat in _ = N return word N with - | eq_refl => w - end in - (split1 m (n - m) w', split2 m (n - m) w')); - abstract omega. - Defined. - - Fixpoint copies {A} (x : A) (n : nat) : list A := - match n with - | O => nil - | S n' => x :: copies x n' - end. - - Definition splitWords' : forall (len : nat) {sz: nat} (x: word sz), list (word wordSize). - Proof. - refine (fix splitWords' (len : nat) {sz : nat} (w : word sz) {struct len} : list (word wordSize) := - match len with - | O => nil - | S len' => - if gt_dec sz wordSize - then let (w1, w2) := splitGt w in - w1 :: splitWords' len' w2 - else match _ in _ = N return list (word N) with - | eq_refl => zext w (wordSize - sz) :: copies (wzero _) len' - end - end)%nat; clear splitWords'; abstract omega. - Defined. - - Lemma length_cast : forall A (F : A -> Type) x1 x2 (pf : x1 = x2) x xs, - length (match pf in _ = X return list (F X) with - | eq_refl => x :: xs - end) = S (length xs). - Proof. - destruct pf; auto. - Qed. - - Lemma length_copies : forall A (x : A) n, length (copies x n) = n. - Proof. - induction n; simpl; auto. - Qed. - - Hint Rewrite length_cast length_copies. - - Lemma length_splitWords' : forall len sz (w : word sz), length (splitWords' len w) = len. - Proof. - induction len; simpl; intuition; - match goal with - | [ |- context[match ?E with _ => _ end] ] => destruct E - end; simpl; try rewrite IHlen; autorewrite with core; reflexivity. - Qed. - - Definition splitWords {sz} (len: nat) (x: word sz): - {x: list (word wordSize) | length x = len}. - Proof. - exists (splitWords' len x); apply length_splitWords'. - Defined. - - Definition splitGF (x: GF) := - splitWords numWords (NToWord (numWords * wordSize)%nat (Z.to_N (proj1_sig x))). - - Fixpoint combineAll' (b: list (word wordSize)): word (wordSize * (length b)). - induction b. - - - simpl. - replace (wordSize * 0)%nat with 0%nat; intuition. - exact (natToWord 0 0). - - - replace (wordSize * length (a :: b))%nat - with (wordSize + wordSize * length b)%nat. - + exact (combine a IHb). - + simpl; rewrite mult_succ_r; intuition. - Defined. - - Definition combineAll (b: BinGF): GF := - inject (Z.of_N (wordToN (combineAll' (proj1_sig b)))). - - Definition binEquiv a b := combineAll a = combineAll b. - - Lemma combine_split: - forall (x: GF) (len: nat), - combineAll (splitGF x) = x. - Admitted. - - Record unaryOp: Set := mkUnary { - f : GF -> GF; - binF : BinGF -> BinGF; - - unaryCompat : forall (a b: GF), - a = b -> f a = f b; - - unaryBinCompat : forall (a b: BinGF), - binEquiv a b -> binEquiv (binF a) (binF b); - - unaryCorrect: forall (a: GF), - f a = combineAll (binF (splitGF a)) - }. - - Record binaryOp: Set := mkBinary { - g : GF -> GF -> GF; - binG : BinGF -> BinGF -> BinGF; - - binaryCompat : forall (a b c d: GF), - a = b -> c = d -> g a c = g b d; - - binaryBinCompat : forall (a b c d: BinGF), - binEquiv a b -> binEquiv c d -> - binEquiv (binG a c) (binG b d); - - binaryCorrect: forall (a b: GF), - g a b = combineAll (binG (splitGF a) (splitGF b)) - }. - -End GFBits. diff --git a/src/Rep/ECRep.v b/src/Rep/ECRep.v index b42e1e067..60481fe72 100644 --- a/src/Rep/ECRep.v +++ b/src/Rep/ECRep.v @@ -1,18 +1,16 @@ -Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.AbstractGaloisField. +Require Export Crypto.Galois.GaloisField. Module ECRep (M: Modulus). - Module G := Galois M. - Module F := AbstractGaloisField M. - Import M G F. + Module F := GaloisField M. + Import F. Local Open Scope GF_scope. - Definition ECSig : ADTSig := + (* Definition ECSig : ADTSig := ADTsignature { Constructor "FromTwistedXY" : GF x GF -> rep, Method "Add" : rep x rep -> rep, - }. + }.*) End ECRep. diff --git a/src/Rep/GaloisRep.v b/src/Rep/GaloisRep.v index 02844ea7c..bfd09acfd 100644 --- a/src/Rep/GaloisRep.v +++ b/src/Rep/GaloisRep.v @@ -1,14 +1,14 @@ Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.AbstractGaloisField. +Require Import Crypto.Galois.GaloisField. Module GaloisRep (M: Modulus). Module G := Galois M. - Module F := AbstractGaloisField M. + Module F := GaloisField M. Import M G F. Local Open Scope GF_scope. - Definition GFSig : ADTSig := + (* Definition GFSig : ADTSig := ADTsignature { Constructor "FromGF" : GF -> rep, @@ -22,5 +22,5 @@ Module GaloisRep (M: Modulus). : rep x rep -> rep, Method "Div" : rep x rep -> rep - }. + }. *) End GaloisRep. diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index 26c45a713..32ae4dde7 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -1,6 +1,6 @@ Require Import ZArith.ZArith Zpower ZArith Znumtheory. Require Import NPeano. -Require Import Galois.EdDSA Galois GaloisTheory. +Require Import Crypto.Galois.EdDSA Crypto.Galois.GaloisField. Require Import Crypto.Curves.PointFormats. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. @@ -65,7 +65,8 @@ Module EdDSA25519_Params <: EdDSAParams. unfold n, b; omega. Qed. - Module Import GFDefs := GaloisDefs Modulus_q. + Module GFDefs := GaloisField Modulus_q. + Import GFDefs. Local Open Scope GF_scope. Definition a := GFopp 1%GF. @@ -105,7 +106,7 @@ Module EdDSA25519_Params <: EdDSAParams. rewrite H1; reflexivity. Qed. - Lemma a_square : exists x, (x * x = a)%GF. + Lemma a_square_old : exists x, (x * x = a)%GF. Proof. intros. pose proof (minus1_square_1mod4 q (proj2_sig q) q_1mod4). @@ -119,15 +120,20 @@ Module EdDSA25519_Params <: EdDSAParams. (* TODO *) Parameter d : GF. + Parameter sqrt_a : GF. Axiom d_nonsquare : forall x, x^2 <> d. + Axiom a_square: (sqrt_a^2 = a)%GF. + Axiom char_gt_2: (1+1 <> 0)%GF. Module CurveParameters <: TwistedEdwardsParams Modulus_q. Module GFDefs := GFDefs. Definition a : GF := a. + Definition sqrt_a := sqrt_a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. Definition d := d. Definition d_nonsquare := d_nonsquare. + Definition char_gt_2 := char_gt_2. End CurveParameters. Module Facts := CompleteTwistedEdwardsFacts Modulus_q CurveParameters. Module Import Curve := Facts.Curve. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 51f1b14c8..4b06e5230 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -139,7 +139,7 @@ end. Section GF25519Base25Point5Formula. Import GF25519Base25Point5. - Import GF. + Import Field. Hint Rewrite Z.mul_0_l |