aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore3
-rw-r--r--.make/cc.mk20
-rw-r--r--.make/coq.mk28
-rw-r--r--Makefile30
-rw-r--r--_CoqProject23
-rw-r--r--src/Curves/Curve25519.v33
-rw-r--r--src/Curves/PointFormats.v156
-rw-r--r--src/Galois/AbstractGaloisField.v14
-rw-r--r--src/Galois/ComputationalGaloisField.v52
-rw-r--r--src/Galois/EdDSA.v15
-rw-r--r--src/Galois/Galois.v54
-rw-r--r--src/Galois/GaloisExamples.v73
-rw-r--r--src/Galois/GaloisField.v (renamed from src/Galois/ZGaloisField.v)38
-rw-r--r--src/Galois/GaloisRep.v3
-rw-r--r--src/Galois/GaloisTheory.v57
-rw-r--r--src/Galois/GaloisTutorial.v106
-rw-r--r--src/Galois/ModularBaseSystem.v17
-rw-r--r--src/Rep/BinGF.v139
-rw-r--r--src/Rep/ECRep.v12
-rw-r--r--src/Rep/GaloisRep.v8
-rw-r--r--src/Specific/EdDSA25519.v12
-rw-r--r--src/Specific/GF25519.v2
22 files changed, 433 insertions, 462 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
diff --git a/Makefile b/Makefile
index 1940c4b2e..21c43fc28 100644
--- a/Makefile
+++ b/Makefile
@@ -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 d5e2c1c89..000000000
--- a/_CoqProject
+++ /dev/null
@@ -1,23 +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
-src/Specific/EdDSA25519.v
diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index 4162d4c1c..248e0af6e 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -1,6 +1,5 @@
Require Import Zpower ZArith Znumtheory.
-Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
-Require Import Crypto.Galois.ZGaloisField.
+Require Import Crypto.Galois.GaloisField.
Require Import Crypto.Curves.PointFormats.
Definition two_255_19 := 2^255 - 19. (* <http://safecurves.cr.yp.to/primeproofs.html> *)
@@ -10,13 +9,9 @@ Module Modulus25519 <: Modulus.
End Modulus25519.
Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519.
- Module Import GFDefs := ZGaloisField Modulus25519.
-
- Lemma char_gt_2 : inject 2 <> 0%GF.
- Admitted.
+ Module Import GFDefs := GaloisField Modulus25519.
Local Open Scope GF_scope.
- Coercion inject : Z >-> GF.
Definition a : GF := -1.
Definition d : GF := -121665 / 121666.
@@ -26,14 +21,24 @@ 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. *)
+ (* An example of how to use ring properly *)
+ replace (sqrt_a ^ 2) with (sqrt_a * sqrt_a) by ring.
+ assert ((inject ((GFToZ sqrt_a) * (GFToZ sqrt_a)))%Z = a).
+
+ - apply gf_eq.
+ (* vm_compute runs out of memory. *)
+ admit.
+
+ - rewrite inject_distr_mul in H.
+ intuition.
+
Admitted.
- Lemma d_nonsquare : forall x, x * x <> d.
+ Lemma d_nonsquare : forall x, x * x <> d.
(* <https://en.wikipedia.org/wiki/Euler%27s_criterion> *)
Admitted.
@@ -53,6 +58,10 @@ Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Mod
*)
Definition basepointY := 4 / 5.
+
+ (* True iff this prime is odd *)
+ 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 32e6acdd0..cd27a2033 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -1,15 +1,16 @@
-Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ZGaloisField.
-Require Import Tactics.VerdiTactics.
-Require Import Logic.Eqdep_dec.
-Require Import BinNums NArith.
+Require Import Crypto.Galois.GaloisTheory Crypto.Galois.GaloisField.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Logic Logic.Eqdep_dec.
+Require Import BinNums NArith Nnat ZArith.
Module Type TwistedEdwardsParams (M : Modulus).
- Module Export GFDefs := ZGaloisField M.
+ Module Export GFDefs := GaloisField M.
Local Open Scope GF_scope.
- Axiom char_gt_2 : inject 2 <> 0.
+ Axiom char_gt_2 : (1+1) <> 0.
Parameter a : GF.
Axiom a_nonzero : a <> 0.
- Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
+ Parameter sqrt_a : GF.
+ Axiom a_square : sqrt_a^2 = a.
Parameter d : GF.
Axiom d_nonsquare : forall x, x * x <> d.
End TwistedEdwardsParams.
@@ -104,7 +105,7 @@ Qed.
Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M).
Local Open Scope GF_scope.
- (** Twisted Ewdwards curves with complete addition laws. References:
+ (** Twisted Edwards curves with complete addition laws. References:
* <https://eprint.iacr.org/2008/013.pdf>
* <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
* <https://eprint.iacr.org/2015/677.pdf>
@@ -133,22 +134,104 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
(* https://eprint.iacr.org/2007/286.pdf Theorem 3.3 *)
(* c=1 and an extra a in front of x^2 *)
- Lemma root_zero : forall x p, x^p = 0 -> x = 0.
- Admitted.
- Lemma root_nonzero : forall x p, x^p <> 0 -> x <> 0.
- Admitted.
+ (* NOTE: these should serve as an example for using field *)
+
Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
- Admitted.
+ intros; intuition; subst.
+ assert (0 * b = 0) by field; intuition.
+ Qed.
+
Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
- Admitted.
- Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
- Admitted.
- Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
- Admitted.
+ intros; intuition; subst.
+ assert (a0 * 0 = 0) by field; intuition.
+ Qed.
+
Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
- Admitted.
+ intros.
+ assert (H := Z.eq_dec (inject x) (inject y)).
+
+ destruct H.
+
+ - left; galois; intuition.
+
+ - right; intuition.
+ rewrite H in n.
+ assert (y = y); intuition.
+ Qed.
+
+ Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
+ intros.
+ assert (Z := GF_eq_dec a0 0); destruct Z.
+
+ - left; intuition.
+
+ - assert (a0 * b / a0 = 0) by
+ ( rewrite H; field; intuition ).
+
+ field_simplify in H0.
+ replace (b/1) with b in H0 by (field; intuition).
+ right; intuition.
+ apply n in H0; intuition.
+ Qed.
+
+ Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
+ intros; intuition; subst.
+ apply mul_zero_why in H1.
+ destruct H1; subst; intuition.
+ Qed.
Hint Resolve mul_nonzero_nonzero.
+ Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0.
+ intros.
+
+ induction p; inversion H.
+
+ revert H H1; generalize x; induction p; intros.
+
+ - simpl in H; apply mul_zero_why in H; destruct H; intuition.
+
+ + subst; intuition.
+
+ + apply IHp in H.
+ rewrite H1.
+ simpl in H1.
+ apply mul_zero_why in H1; destruct H1; intuition.
+ rewrite H0 in H.
+ apply mul_zero_why in H; destruct H; intuition.
+
+ simpl; intuition.
+
+ - simpl in H1; apply IHp in H1; simpl; intuition.
+ simpl in H; rewrite H in H1; rewrite H.
+ apply mul_zero_why in H1; destruct H1; intuition.
+
+ - simpl in H; subst; intuition.
+
+ Qed.
+
+ Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0.
+ intros; intuition.
+
+ induction p.
+
+ - apply H; intuition.
+
+ - apply H.
+ rewrite H1 in *.
+ induction p.
+
+ + simpl.
+ field.
+
+ + simpl in *.
+ replace (0 * 0) with 0 in * by field.
+ apply IHp; intuition.
+ induction p; inversion H2.
+
+ + simpl; intuition.
+
+ Qed.
+
Ltac whatsNotZero :=
repeat match goal with
| [H: ?lhs = ?rhs |- _ ] =>
@@ -159,7 +242,10 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
assert (rhs <> 0) by (rewrite H; auto)
| [H: (?a^?p)%GF <> 0 |- _ ] =>
match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
- assert (a <> 0) by (eapply root_nonzero; eauto)
+ let Y:=fresh in let Z:=fresh in try (
+ assert (p <> 0%N) as Z by (intro Y; inversion Y);
+ assert (a <> 0) by (eapply root_nonzero; eauto);
+ clear Z)
| [H: (?a*?b)%GF <> 0 |- _ ] =>
match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
assert (a <> 0) by (eapply mul_nonzero_l; eauto)
@@ -173,11 +259,14 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
onCurve (x2, y2) ->
(d*x1*x2*y1*y2)^2 <> 1.
Proof.
+ (* TODO: this proof was made inconsistent by an actually
+ correct version of root_nonzero. This adds the necessary
+ hypothesis*)
unfold onCurve; intuition; whatsNotZero.
pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero.
destruct a_square as [sqrt_a a_square].
- rewrite <- a_square in *.
+ rewrite a_square in Ha_nonzero.
(* Furthermore... *)
pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
@@ -206,13 +295,18 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
end.
assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
+
+ rewrite a_square in *.
replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field.
(* contradiction: product of nonzero things is zero *)
- destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition];
- destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero; field.
+ destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition].
+ destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero.
+
+ + replace (inject 2%Z) with (1+1) in Hccc by field; intuition.
+
+ + rewrite <- a_square; simpl; rewrite Hccc; field.
Qed.
-
Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
onCurve (x1,y1) ->
onCurve (x2, y2) ->
@@ -239,8 +333,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
Definition projX (P:point) := fst (proj1_sig P).
Definition projY (P:point) := snd (proj1_sig P).
- Definition checkOnCurve x y : if Zbool.Zeq_bool (a*x^2 + y^2) (1 + d*x^2*y^2) then point else True.
- break_if. exists (x, y). exact (GFdecidable _ _ Heqb). trivial.
+ Definition checkOnCurve (x y: GF) : if Zbool.Zeq_bool (a*x^2 + y^2)%GF (1 + d*x^2*y^2)%GF then point else True.
+ break_if; trivial. exists (x, y). apply GFdecidable. exact Heqb.
Defined.
Hint Unfold onCurve mkPoint.
@@ -259,6 +353,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
Proof.
(* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
* c=1 and an extra a in front of x^2 *)
+
unfold unifiedAdd', onCurve in *; injection H; clear H; intros.
Ltac t x1 y1 x2 y2 :=
@@ -281,7 +376,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/
((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto.
- - rewrite <-HT1, <-HT2; field; rewrite HT1;
+ - rewrite <-HT1, <-HT2; field; rewrite HT1.
replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
by field; simpl; auto.
@@ -507,12 +602,13 @@ 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 : inject 2 <> 0.
+ Axiom char_gt_2 : (1+1) <> 0.
Definition a := inject (- 1).
Axiom a_nonzero : a <> 0.
- Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
+ Parameter sqrt_a : GF.
+ Axiom a_square : sqrt_a^2 = a.
Parameter d : GF.
Axiom d_nonsquare : forall x, x * x <> d.
End Minus1Params.
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 de26c678c..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.ZGaloisField 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 := ZGaloisField 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,13 +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 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.
+ 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/GaloisExamples.v b/src/Galois/GaloisExamples.v
deleted file mode 100644
index 12bcfa2c8..000000000
--- a/src/Galois/GaloisExamples.v
+++ /dev/null
@@ -1,73 +0,0 @@
-
-Require Import Zpower ZArith Znumtheory.
-Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
-Require Import Crypto.Galois.ZGaloisField.
-
-Definition two_5_1 := (two_p 5) - 1.
-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.
-
-Module Modulus31 <: Modulus.
- Definition modulus := exist _ two_5_1 two_5_1_prime.
-End Modulus31.
-
-Module Modulus127_1 <: Modulus.
- Definition modulus := exist _ two_127_1 two_127_1_prime.
-End Modulus127_1.
-
-Module Example31.
- Module Theory := ZGaloisField Modulus31.
- Import Theory.
- Local Open Scope GF_scope.
-
- Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2).
- Proof.
- intros; simpl.
- field; trivial.
- Qed.
-
- Lemma example2: forall x: GF, x * (inject 2) = x + x.
- Proof.
- intros; simpl.
- field.
- Qed.
-
- Lemma example3: forall x: GF, x ^ 2 + (inject 2) * x + (inject 1) = (x + (inject 1)) ^ 2.
- Proof.
- intros; simpl.
- field; trivial.
- Qed.
-
- Lemma example4: forall x: GF, x/(inject 1) = x.
- Proof.
- intros; field.
- discriminate.
- Qed.
-
-End Example31.
-
-Module TimesZeroTransparentTestModule.
- Module Theory := ZGaloisField Modulus127_1.
- Import Theory.
- Local Open Scope GF_scope.
-
- Lemma timesZero : forall a, a*0 = 0.
- intros.
- field.
- Qed.
-End TimesZeroTransparentTestModule.
-
-Module TimesZeroParametricTestModule (M: Modulus).
- Module Theory := ZGaloisField M.
- Import Theory.
- Local Open Scope GF_scope.
-
- Lemma timesZero : forall a, a*0 = 0.
- intros.
- field.
- Qed.
-End TimesZeroParametricTestModule.
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/GaloisTutorial.v b/src/Galois/GaloisTutorial.v
new file mode 100644
index 000000000..5ef0e4cf5
--- /dev/null
+++ b/src/Galois/GaloisTutorial.v
@@ -0,0 +1,106 @@
+
+Require Import Zpower ZArith Znumtheory.
+Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
+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.
+
+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.
+
+Module Modulus127_1 <: Modulus.
+ Definition modulus := exist _ two_127_1 two_127_1_prime.
+End Modulus127_1.
+
+Module Example31.
+ (* 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.
+
+ (* First, let's solve a ring example*)
+ Lemma ring_example: forall x: GF, x * 2 = x + x.
+ Proof.
+ intros.
+ ring.
+ Qed.
+
+ (* 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; trivial.
+ Qed.
+
+ (* 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.
+
+ (* In general, the rule I've been using is:
+
+ - If our goal looks like x = y:
+
+ + If we need to use assumptions to prove the goal, then before
+ we apply field,
+
+ * Perform all relevant substitutions (especially subst)
+
+ * If we have something more complex, we're probably going
+ to have to performe some sequence of "replace X with Y"
+ and solve out the subgoals manually before we can use
+ field.
+
+ + Else, just use field directly
+
+ - If we just want to simplify terms and put them into a canonical
+ form, then field_simplify or ring_simplify should do the trick.
+ Note, however, that the canonical form has lots of annoying "/1"s
+
+ - Otherwise, do a "replace X with Y" to generate an equality
+ so that we can use field in the above case
+
+ *)
+
+End Example31.
+
+(* Notice that the field tactics work whether we know what the modulus is *)
+Module TimesZeroTransparentTestModule.
+ Module Theory := GaloisField Modulus127_1.
+ Import Theory.
+ Local Open Scope GF_scope.
+
+ Lemma timesZero : forall a, a*0 = 0.
+ intros.
+ field.
+ Qed.
+End TimesZeroTransparentTestModule.
+
+(* Or if we don't (i.e. it's opaque) *)
+Module TimesZeroParametricTestModule (M: Modulus).
+ Module Theory := GaloisField M.
+ Import Theory.
+ Local Open Scope GF_scope.
+
+ Lemma timesZero : forall a, a*0 = 0.
+ intros.
+ field.
+ Qed.
+End TimesZeroParametricTestModule.
+
diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v
index 5a97d67c9..138eabd3f 100644
--- a/src/Galois/ModularBaseSystem.v
+++ b/src/Galois/ModularBaseSystem.v
@@ -1,7 +1,7 @@
Require Import Zpower ZArith.
Require Import List.
-Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory.
-Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
+Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisField.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.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 f5546f3c8..194f94385 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.
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:07:58 +0000