diff options
| -rw-r--r-- | .make/coq.mk | 2 | ||||
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | _CoqProject | 7 | ||||
| -rw-r--r-- | src/Curves/Curve25519.v | 26 | ||||
| -rw-r--r-- | src/Curves/PointFormats.v | 7 | ||||
| -rw-r--r-- | src/Galois/AbstractGaloisField.v | 6 | ||||
| -rw-r--r-- | src/Galois/ComputationalGaloisField.v | 6 | ||||
| -rw-r--r-- | src/Galois/Galois.v | 11 | ||||
| -rw-r--r-- | src/Galois/GaloisTheory.v | 7 | ||||
| -rw-r--r-- | src/Rep/WordEquivalence.v | 18 |
10 files changed, 39 insertions, 59 deletions
diff --git a/.make/coq.mk b/.make/coq.mk index b077a5b08..bab225be7 100644 --- a/.make/coq.mk +++ b/.make/coq.mk @@ -19,7 +19,7 @@ check_bedrock: %.vo %.glob: %.v.d $(COMPILE.v) $* -%.v.d: check_fiat check_bedrock %.v +%.v.d: %.v @$(COQDEP) -I . $(COQLIBS) "$<" >"$@" \ || (RV=$$?; rm -f "$@"; exit $${RV}) @@ -10,13 +10,9 @@ include .make/coq.mk FAST_TARGETS += check_fiat check_bedrock clean .DEFAULT_GOAL = all -.PHONY: all deps objects clean coquille +.PHONY: clean coquille -all: objects - -deps: $(SOURCES:%=%.d) - -objects: deps $(SOURCES:%=%o) +all: check_fiat check_bedrock $(SOURCES:%=%o) clean: $(RM) $(foreach f,$(SOURCES),$(call coq-generated,$(basename $f))) diff --git a/_CoqProject b/_CoqProject index feb0ebf9c..037a9be62 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,8 +2,9 @@ -R fiat/src Fiat -R bedrock/Bedrock Bedrock src/Tactics/VerdiTactics.v -src/Galois/GaloisField.v -src/Galois/GaloisFieldTheory.v -src/Galois/GaloisExamples.v +src/Galois/Galois.v +src/Galois/GaloisTheory.v +src/Galois/AbstractGaloisField.v +src/Galois/ComputationalGaloisField.v src/Curves/PointFormats.v src/Curves/Curve25519.v diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index fc6cbb104..fc40d9136 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -1,39 +1,29 @@ Require Import Zpower ZArith Znumtheory. -Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. +Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Crypto.Curves.PointFormats. -Definition two_255_19 := (two_p 255) - 19. -Lemma two_255_19_prime : prime two_255_19. - (* <http://safecurves.cr.yp.to/proof/57896044618658097711785492504343953926634992332820282019728792003956564819949.html>, - * <https://github.com/sipa/Coin25519/blob/master/spec/primeCerts/prime57896044618658097711785492504343953926634992332820282019728792003956564819949.v#L16> *) -Admitted. - -Definition prime25519 := exist _ two_255_19 two_255_19_prime. -Local Notation p := two_255_19. - -Module Modulus25519 <: Modulus. - Definition modulus := prime25519. -End Modulus25519. - Module Curve25519. - Module PointFormats25519 := PointFormats Modulus25519. - Import Modulus25519 PointFormats25519 PointFormats25519.Theory PointFormats25519.Field. + Module PF := PointFormats. + Import PF. Local Open Scope GF_scope. Definition A : GF := ZToGF 486662. Definition d : GF := ((0 -ZToGF 121665) / (ZToGF 121666))%GF. - Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A. + + (* Module-izing Twisted was a breaking change Definition m1TwistedOnCurve25519 := twistedOnCurve (0 -1) d. Definition identityTwisted : twisted := mkTwisted 0 1. Lemma identityTwistedOnCurve : m1TwistedOnCurve25519 identityTwisted. - unfold m1TwistedOnCurve25519, twistedOnCurve, identityTwisted. + unfold m1TwistedOnCurve25519, twistedOnCurve. simpl; field. Qed. + *) + Definition basepointY := ZToGF 4 / ZToGF 5. (* TODO(andreser): implement (in PointFormats) recoverX from <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) End Curve25519. diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index a72d5d5e0..3962e1d90 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -1,5 +1,5 @@ -Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. +Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. Require Import Tactics.VerdiTactics. (* FIXME: remove after [field] with modulus as a parameter (34d9f8a6e6a4be439d1c56a8b999d2c21ee12a46) is fixed *) @@ -15,9 +15,8 @@ End M. (** Theory of elliptic curves over prime fields for cryptographic applications, with focus on the curves in <https://tools.ietf.org/html/draft-ladd-safecurves-04> *) Module PointFormats. - Module Field := GaloisField M. - Module Theory := GaloisFieldTheory M. - Import M Field Theory. + Module F := ComputationalGaloisField M. + Export M F F.T. Local Open Scope GF_scope. Local Notation "2" := (1+1). Local Notation "3" := (1+1+1). diff --git a/src/Galois/AbstractGaloisField.v b/src/Galois/AbstractGaloisField.v index a196c7bf8..12a9af80d 100644 --- a/src/Galois/AbstractGaloisField.v +++ b/src/Galois/AbstractGaloisField.v @@ -2,7 +2,7 @@ Require Import BinInt BinNat ZArith Znumtheory. Require Import Eqdep_dec. Require Import Tactics.VerdiTactics. -Require Import Galois GaloisTheory. +Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. Module AbstractGaloisField (M: Modulus). Module G := Galois M. @@ -10,7 +10,5 @@ Module AbstractGaloisField (M: Modulus). Export M G T. Add Field GFfield_computational : GFfield_theory - (completeness GFcomplete, - div GFdiv_theory, - power_tac GFpower_theory [GFexp_tac]). + (power_tac GFpower_theory [GFexp_tac]). End AbstractGaloisField. diff --git a/src/Galois/ComputationalGaloisField.v b/src/Galois/ComputationalGaloisField.v index a17783475..e83e22fea 100644 --- a/src/Galois/ComputationalGaloisField.v +++ b/src/Galois/ComputationalGaloisField.v @@ -37,6 +37,12 @@ Module ComputationalGaloisField (M: Modulus). | _ => 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, diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v index 439b4735c..3ee86e4e4 100644 --- a/src/Galois/Galois.v +++ b/src/Galois/Galois.v @@ -4,10 +4,7 @@ Require Import Eqdep_dec. Require Import Tactics.VerdiTactics. Section GaloisPreliminaries. - Definition SMALL_THRESH: Z := 128. - Definition MIN_PRIME: Z := SMALL_THRESH * SMALL_THRESH. - - Definition Prime := {x: Z | prime x /\ x > MIN_PRIME}. + Definition Prime := {x: Z | prime x}. Definition primeToZ(x: Prime) := proj1_sig x. Coercion primeToZ: Prime >-> Z. @@ -51,9 +48,9 @@ Module Galois (M: Modulus). Definition GFone: GF. exists 1. - abstract (symmetry; apply Zmod_small; intuition; - destruct modulus; simpl; destruct a; - apply prime_ge_2 in H; intuition). + abstract( symmetry; apply Zmod_small; intuition; + destruct modulus; simpl; + apply prime_ge_2 in p; intuition). Defined. Definition GFplus(x y: GF): GF. diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v index 9b1637bf3..e95eed864 100644 --- a/src/Galois/GaloisTheory.v +++ b/src/Galois/GaloisTheory.v @@ -206,10 +206,8 @@ Module GaloisTheory (M: Modulus). (* Now add the ring with all modifiers *) - Add Ring GFring : GFring_theory - (decidable GFdecidable, - div GFdiv_theory, - power_tac GFpower_theory [GFexp_tac]). + Add Ring GFring0 : GFring_theory + (power_tac GFpower_theory [GFexp_tac]). (* Field Theory*) @@ -269,3 +267,4 @@ Module GaloisTheory (M: Modulus). constructor; auto. Qed. End GaloisTheory. + diff --git a/src/Rep/WordEquivalence.v b/src/Rep/WordEquivalence.v index 6c625db60..4005adc2a 100644 --- a/src/Rep/WordEquivalence.v +++ b/src/Rep/WordEquivalence.v @@ -22,9 +22,9 @@ Module GFBits (M: Modulus). match len with | O => [] | S len' => - if(sz - wordSize > 0) + if(sz - wordSize >? 0) then Cons (split1 wordSize (sz - wordSize) x) - (words len' (split2 wordSize (sz - wordSize) x)) + (splitWords len' (split2 wordSize (sz - wordSize) x)) else zext x wordSize end. @@ -34,22 +34,16 @@ Module GFBits (M: Modulus). | Cons x xs => combine x (combineAll xs) end. + wordEq a b := wordToN (combineAll a) = wordToN (combineAll b) + Definition toZ (b: BinGF) := Z.of_N (wordToN (combineAll b)). Definition toGF (b: BinGF) := ZToGF ((toZ b) mod modulus) Definition fromZ (x: Z) := splitWords numWords (NToWord (Z.to_N x)) Definition fromGF (x: GF) := fromZ (proj1_sig x). - Inductive BinEquiv (x: GF) (y: BinGF) := - | EquivGF : forall x, BinEquiv x (fromGF x) - | EquivBin : forall y, BinEquiv (toGF y) y - | EquivPlus : forall x1 y1 x2 y2, - BinEquiv x1 y1 -> binEquiv x2 y2 -> BinEquiv (x1 + x2) (y1 ^+ y2)%word - | EquivMinus : forall x1 y1 x2 y2, - BinEquiv x1 y1 -> binEquiv x2 y2 -> BinEquiv (x1 - x2) (y1 ^- y2)%word - | EquivMult : forall x1 y1 x2 y2, - BinEquiv x1 y1 -> binEquiv x2 y2 -> BinEquiv (x1 * x2) (y1 ^* y2)%word. - + toZ a + toZ b = toZ (a ^+ b) + Lemma equivalent_GF : BinEquiv x y <-> x = toGF y. Admitted. |