diff options
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | src/Curves/Curve25519.v | 32 | ||||
| -rw-r--r-- | src/Galois/GaloisField.v (renamed from src/GaloisField.v) | 25 | ||||
| -rw-r--r-- | src/Galois/GaloisFieldTheory.v (renamed from src/GaloisFieldTheory.v) | 9 |
5 files changed, 48 insertions, 31 deletions
@@ -10,13 +10,13 @@ include .make/coq.mk FAST_TARGETS += check_fiat clean .DEFAULT_GOAL = all -.PHONY: all clean coquille +.PHONY: all deps objects clean coquille -all: $(SOURCES) - @echo "done!" +all: objects -coquille: - vim -c "execute coquille#Launch($(COQLIBS))" . +deps: $(SOURCES:%=%.d) + +objects: deps $(SOURCES:%=%o) clean: $(RM) $(foreach f,$(SOURCES),$(call coq-generated,$(basename $f))) diff --git a/_CoqProject b/_CoqProject index 89404292d..fac637589 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,3 +1,6 @@ -R src Crypto -R fiat/src Fiat +src/Galois/GaloisField.v +src/Galois/GaloisFieldTheory.v src/Curves/Curve25519.v +src/Assembly/Assembly.v diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index 8bc3d6e20..df0b2ce06 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -1,13 +1,23 @@ -Require Import ZModulo. -(** - * The relevant module is ZModulo: - * the constructor you want is of_pos - * the operations you want are in zmod_ops - * the tactics you want are somewhere between Field and CyclicType: - * probs you want to be converting to/from Z pretty frequently - * - * Coq Reference page: - * https://coq.inria.fr/library/Coq.Numbers.Cyclic.ZModulo.ZModulo.html - *) +Require Import Zpower ZArith Znumtheory. +Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. + +Definition prime25519 : Prime. + exists ((two_p 255) - 19). + (* <http://safecurves.cr.yp.to/proof/57896044618658097711785492504343953926634992332820282019728792003956564819949.html> *) +Admitted. + +Module Modulus25519 <: Modulus. + Definition modulus := prime25519. +End Modulus25519. + +Declare Module GaloisField25519 : GaloisField Modulus25519. + +Declare Module GaloisTheory25519 : GaloisFieldTheory Modulus25519 GaloisField25519. + +Module Curve25519. + Import Modulus25519 GaloisField25519 GaloisTheory25519. + + (* Prove some theorems! *) +End Curve25519. diff --git a/src/GaloisField.v b/src/Galois/GaloisField.v index 928eaf702..dfae63312 100644 --- a/src/GaloisField.v +++ b/src/Galois/GaloisField.v @@ -2,19 +2,12 @@ Require Import BinInt BinNat ZArith Znumtheory. Require Import ProofIrrelevance Epsilon. -Definition Prime := {x: Z | prime x}. +Section GaloisPreliminaries. + Definition Prime := {x: Z | prime x}. -Module Type GaloisField. - - Parameter modulus: Prime. - - (* Data type definitions *) Definition primeToZ(x: Prime) := proj1_sig x. Coercion primeToZ: Prime >-> Z. - Definition GF := {x: Z | exists y, x = y mod modulus}. - Definition GFToZ(x: GF) := proj1_sig x. - Theorem exist_eq: forall (x y: Z) P e1 e2, x = y <-> exist P x e1 = exist P y e2. intros. split. intro H. apply subset_eq_compat; trivial. @@ -23,13 +16,23 @@ Module Type GaloisField. rewrite H. trivial. simpl in H0. rewrite H0. trivial. Qed. +End GaloisPreliminaries. + +Module Type Modulus. + Parameter modulus: Prime. +End Modulus. + +Module Type GaloisField (M: Modulus). + Import M. + + Definition GF := {x: Z | exists y, x = y mod modulus}. + Definition GFToZ(x: GF) := proj1_sig x. + Coercion GFToZ: GF >-> Z. Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y. intros x y. destruct x, y. split; apply exist_eq. Qed. - Coercion GFToZ: GF >-> Z. - (* Elementary operations *) Definition GFzero: GF. exists 0. exists 0. trivial. diff --git a/src/GaloisFieldTheory.v b/src/Galois/GaloisFieldTheory.v index 1a749b027..1a478e088 100644 --- a/src/GaloisFieldTheory.v +++ b/src/Galois/GaloisFieldTheory.v @@ -1,13 +1,14 @@ Require Import BinInt BinNat ZArith Znumtheory. -Require Export Morphisms Setoid Ring_theory Field_theory Field_tac. -Require Export GaloisField. +Require Export Coq.Classes.Morphisms Setoid. +Require Export Ring_theory Field_theory Field_tac. +Require Export Crypto.Galois.GaloisField. Set Implicit Arguments. Unset Strict Implicits. -Module Type GaloisFieldTheory. - Declare Module Field: GaloisField. +Module Type GaloisFieldTheory (M: Modulus) (Field: GaloisField M). + Import M. Import Field. (* Notations *) |