diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Assembly/Assembly.v | 3 | ||||
| -rw-r--r-- | src/Galois/GaloisExamples.v | 37 | ||||
| -rw-r--r-- | src/Galois/GaloisField.v | 123 | ||||
| -rw-r--r-- | src/Galois/GaloisFieldTheory.v | 63 | ||||
| -rw-r--r-- | src/Galois/GaloisTest.v | 35 |
6 files changed, 204 insertions, 58 deletions
diff --git a/_CoqProject b/_CoqProject index e5fbba08a..afcbc907e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6,4 +6,3 @@ src/Galois/GaloisFieldTheory.v src/Galois/GaloisExamples.v src/Curves/PointFormats.v src/Curves/Curve25519.v -src/Assembly/Assembly.v diff --git a/src/Assembly/Assembly.v b/src/Assembly/Assembly.v deleted file mode 100644 index 14ba480ea..000000000 --- a/src/Assembly/Assembly.v +++ /dev/null @@ -1,3 +0,0 @@ - -Require Import Fiat.Common Fiat.Computation. -Require Import Fiat.ADTNotation Fiat.ADTRefinement. diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v index 969ee2d4a..527acd547 100644 --- a/src/Galois/GaloisExamples.v +++ b/src/Galois/GaloisExamples.v @@ -6,17 +6,22 @@ Definition two_5_1 := (two_p 5) - 1. Lemma two_5_1_prime : prime two_5_1. Admitted. -Definition prime31 := exist _ two_5_1 two_5_1_prime. -Local Notation p := two_5_1. +Definition two_127_1 := (two_p 127) - 1. +Lemma two_127_1_prime : prime two_127_1. +Admitted. Module Modulus31 <: Modulus. - Definition modulus := prime31. + Definition modulus := exist _ two_5_1 two_5_1_prime. End Modulus31. -Module Theory31 := GaloisFieldTheory Modulus31. +Module Modulus127_1 <: Modulus. + Definition modulus := exist _ two_127_1 two_127_1_prime. +End Modulus127_1. + Module Example31. - Import Modulus31 Theory31 Theory31.Field. + Module Theory := GaloisFieldTheory Modulus31. + Import Modulus31 Theory Theory.Field. Local Open Scope GF_scope. Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2). @@ -39,3 +44,25 @@ Module Example31. End Example31. +Module TimesZeroTransparentTestModule. + Module Theory := GaloisFieldTheory Modulus127_1. + Import Modulus127_1 Theory Theory.Field. + Local Open Scope GF_scope. + + Lemma timesZero : forall a, a*0 = 0. + intros. + field. + Qed. +End TimesZeroTransparentTestModule. + +Module TimesZeroParametricTestModule (M: Modulus). + Module Theory := GaloisFieldTheory M. + Import M Theory Theory.Field. + Local Open Scope GF_scope. + + Lemma timesZero : forall a, a*0 = 0. + intros. + field. + ring. (* field doesn't work but ring does :) *) + Qed. +End TimesZeroParametricTestModule. diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v index 860e830b9..2e79453ec 100644 --- a/src/Galois/GaloisField.v +++ b/src/Galois/GaloisField.v @@ -4,7 +4,10 @@ Require Import Eqdep_dec. Require Import Tactics.VerdiTactics. Section GaloisPreliminaries. - Definition Prime := {x: Z | prime x}. + Definition SMALL_THRESH: Z := 128. + Definition MIN_PRIME: Z := SMALL_THRESH * SMALL_THRESH. + + Definition Prime := {x: Z | prime x /\ x > MIN_PRIME}. Definition primeToZ(x: Prime) := proj1_sig x. Coercion primeToZ: Prime >-> Z. @@ -31,7 +34,6 @@ Module GaloisField (M: Modulus). - rewrite <- Z.ltb_lt; auto. Defined. - Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y. Proof. destruct x, y; intuition; simpl in *; try congruence. @@ -41,6 +43,98 @@ Module GaloisField (M: Modulus). apply Z.eq_dec. Qed. + (* Useful small-number lemmas *) + Definition isSmall (x: Z) := x <? SMALL_THRESH. + + Lemma small_prop: forall x: Z, isSmall x = true <-> x < SMALL_THRESH. + Proof. + intros; unfold isSmall; apply (Z.ltb_lt x SMALL_THRESH). + Qed. + + Lemma small_neg_prop: forall x: Z, isSmall x = false <-> SMALL_THRESH <= x. + Proof. + intros; unfold isSmall; apply (Z.ltb_ge x SMALL_THRESH). + Qed. + + Lemma small_dec: forall x: Z, {isSmall x = true} + {isSmall x = false}. + Proof. + intros; induction (isSmall x); intuition. + Qed. + + Lemma double_small_dec: forall x y: Z, + {isSmall x = true /\ isSmall y = true} + + {isSmall x = false \/ isSmall y = false}. + Proof. + intros; destruct (small_dec x), (small_dec y). + - left; intuition. + - right; intuition. + - right; intuition. + - right; intuition. + Qed. + + Lemma GF_ge_zero: forall x: GF, x >= 0. + Proof. + intros; destruct x; simpl; rewrite e. + assert (modulus > 0); + destruct modulus; destruct a; + assert (Z := prime_ge_2 x0); simpl; intuition. + assert (A := Z_mod_lt x x0). + intuition. + Qed. + + Lemma small_plus: forall x y: GF, + isSmall x = true -> isSmall y = true -> + x + y = (x + y) mod modulus. + Proof. + intros. rewrite Zmod_small; trivial. + rewrite small_prop in H, H0. + assert (Hx := GF_ge_zero x). + assert (Hy := GF_ge_zero y). + split; try intuition. + + destruct modulus; simpl in *. + destruct a. + assert (x0 > SMALL_THRESH * SMALL_THRESH); intuition. + assert (SMALL_THRESH * SMALL_THRESH > SMALL_THRESH + SMALL_THRESH); + simpl; intuition. + Qed. + + Lemma small_minus: forall x y: GF, + isSmall x = true -> isSmall y = true -> x >= y -> + x - y = (x - y) mod modulus. + Proof. + intros. rewrite Zmod_small; trivial. + rewrite small_prop in H, H0. + assert (Hx := GF_ge_zero x). + assert (Hy := GF_ge_zero y). + split; try intuition. + + destruct modulus; simpl in *. + destruct a. + assert (x0 > SMALL_THRESH * SMALL_THRESH); intuition. + assert (SMALL_THRESH * SMALL_THRESH > SMALL_THRESH + SMALL_THRESH); + simpl; intuition. + Qed. + + Lemma small_mult: forall x y: GF, + isSmall x = true -> isSmall y = true -> + x * y = (x * y) mod modulus. + Proof. + intros. rewrite Zmod_small; trivial. + rewrite small_prop in H, H0. + assert (Hx := GF_ge_zero x). + assert (Hy := GF_ge_zero y). + split; try intuition. + + destruct x, y; simpl in *. + destruct modulus; simpl in *. + destruct a. + assert (x1 > SMALL_THRESH * SMALL_THRESH); intuition. + assert (x * x0 <= SMALL_THRESH * SMALL_THRESH); intuition. + left. + + Qed. + (* Elementary operations *) Definition GFzero: GF. exists 0. @@ -49,13 +143,27 @@ Module GaloisField (M: Modulus). Definition GFone: GF. exists 1. - abstract (symmetry; apply Zmod_small; intuition; destruct modulus; simpl; - apply prime_ge_2 in p; intuition). + abstract (symmetry; apply Zmod_small; intuition; + destruct modulus; simpl; destruct a; + apply prime_ge_2 in H; intuition). Defined. Definition GFplus(x y: GF): GF. - exists ((x + y) mod modulus). - abstract (rewrite Zmod_mod; trivial). + destruct (double_small_dec x y). + + exists (x + y). + rewrite Zmod_small; trivial. + destruct modulus. + destruct a. + assert (0 <= x + y). + auto with arith. + assert (x + y < SMALL_THRESH + SMALL_THRESH). + unfold isSmall, SMALL_THRESH in *. + intuition. + + exists ((x + y) mod modulus); + abstract (rewrite Zmod_mod; trivial). + Defined. Definition GFminus(x y: GF): GF. @@ -85,7 +193,8 @@ Module GaloisField (M: Modulus). end. (* Inverses + division derived from the existence of a totient *) - Definition isTotient(e: N) := N.gt e 0 /\ forall g, GFexp g e = GFone. + Definition isTotient(e: N) := N.gt e 0 /\ forall g: GF, g <> GFzero -> + GFexp g e = GFone. Definition Totient := {e: N | isTotient e}. diff --git a/src/Galois/GaloisFieldTheory.v b/src/Galois/GaloisFieldTheory.v index ab9889cb6..bf96ce098 100644 --- a/src/Galois/GaloisFieldTheory.v +++ b/src/Galois/GaloisFieldTheory.v @@ -1,5 +1,6 @@ Require Import BinInt BinNat ZArith Znumtheory NArith. +Require Import Eqdep_dec. Require Export Coq.Classes.Morphisms Setoid. Require Export Ring_theory Field_theory Field_tac. Require Export Crypto.Galois.GaloisField. @@ -56,9 +57,18 @@ Module GaloisFieldTheory (M: Modulus). notFancy x; rewrite (Zmult_mod_idemp_l x) | [ |- context[(_ * (?y mod _)) mod _] ] => notFancy y; rewrite (Zmult_mod_idemp_r y) + | [ |- context[(?x mod _) mod _] ] => + notFancy x; rewrite (Zmod_mod x) | _ => rewrite Zplus_neg in * || rewrite Z.sub_diag in * end. + (* Remove exists under equals: we do this a lot *) + Ltac eq_remove_proofs := match goal with + | [ |- ?a = ?b ] => + assert (Q := gf_eq a b); + simpl in *; apply Q; clear Q + end. + (* General big hammer for proving Galois arithmetic facts *) Ltac galois := intros; apply gf_eq; simpl; repeat match goal with @@ -148,19 +158,32 @@ Module GaloisFieldTheory (M: Modulus). (* Ring properties *) + 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 _ => true - | exist _ ?z _ => isZcst z - | _ => false + | ZToGF _ => isModulusConstant + | exist _ ?z _ => match (isZcst z) with + | NotConstant => NotConstant + | _ => isModulusConstant + end + | _ => NotConstant end. Ltac GFconstants t := match isGFconstant t with - | true => t - | _ => NotConstant + | NotConstant => NotConstant + | _ => t end. Ltac GFexp_tac t := @@ -186,11 +209,35 @@ Module GaloisFieldTheory (M: Modulus). galois. Qed. + (* Division Theory *) + Definition inject(x: Z): GF. + exists (x mod modulus). + abstract (demod; trivial). + Defined. + + Definition GFquotrem(a b: GF): GF * GF := + match (Z.quotrem a b) with + | (q, r) => (inject q, inject r) + end. + + Lemma GFdiv_theory : div_theory eq GFplus GFmult (@id _) GFquotrem. + Proof. + constructor; intros; unfold GFquotrem. + + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + + eq_remove_proofs; demod; + rewrite <- (Z.quot_rem' a b); + destruct a; simpl; trivial. + Qed. + (* Now add the ring with all modifiers *) Add Ring GFring : GFring_theory (decidable GFdecidable, constants [GFconstants], + div GFdiv_theory, power_tac GFpower_theory [GFexp_tac]). (* Field Theory*) @@ -251,11 +298,13 @@ Module GaloisFieldTheory (M: Modulus). constructor; auto. Qed. - Add Field GFfield : GFfield_theory + (* Add Scoped field declarations *) + + Add Field GFfield_computational : GFfield_theory (decidable GFdecidable, completeness GFcomplete, constants [GFconstants], + div GFdiv_theory, power_tac GFpower_theory [GFexp_tac]). End GaloisFieldTheory. - diff --git a/src/Galois/GaloisTest.v b/src/Galois/GaloisTest.v deleted file mode 100644 index 807224020..000000000 --- a/src/Galois/GaloisTest.v +++ /dev/null @@ -1,35 +0,0 @@ -Require Import Zpower ZArith Znumtheory. -Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. - - -Definition two_127_1 := (two_p 127) - 1. -Lemma two_127_1_prime : prime two_127_1. -Admitted. - -Module Modulus127_1 <: Modulus. - Definition modulus := exist _ two_127_1 two_127_1_prime. -End Modulus127_1. - -Module TimesZeroTransparentTestModule. - Module Theory := GaloisFieldTheory Modulus127_1. - Import Modulus127_1 Theory Theory.Field. - Local Open Scope GF_scope. - - Lemma timesZero : forall a, a*0 = 0. - intros. - field. - Qed. -End TimesZeroTransparentTestModule. - -Module TimesZeroParametricTestModule (M: Modulus). - Module Theory := GaloisFieldTheory M. - Import M Theory Theory.Field. - Local Open Scope GF_scope. - - Lemma timesZero : forall a, a*0 = 0. - intros. - (* - field. (*not a valid field equation*) - *) - Abort. -End TimesZeroParametricTestModule . |