diff options
| -rw-r--r-- | .make/coq.mk | 10 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Galois/GaloisExamples.v | 14 | ||||
| -rw-r--r-- | src/Galois/GaloisField.v | 216 | ||||
| -rw-r--r-- | src/Galois/GaloisFieldTheory.v | 310 |
6 files changed, 17 insertions, 536 deletions
diff --git a/.make/coq.mk b/.make/coq.mk index b05c7e59d..b077a5b08 100644 --- a/.make/coq.mk +++ b/.make/coq.mk @@ -6,16 +6,20 @@ COQDEP = coqdep COMPILE.v = $(COQC) -q $(COQLIBS) -.PHONY: check_fiat +.PHONY: check_fiat check_bedrock check_fiat: @perl -e \ 'if(! -d "./fiat") { print("you need to link fiat to ./fiat\n"); exit(1) }' -%.vo %.glob: check_fiat %.v +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: check_fiat %.v +%.v.d: check_fiat check_bedrock %.v @$(COQDEP) -I . $(COQLIBS) "$<" >"$@" \ || (RV=$$?; rm -f "$@"; exit $${RV}) @@ -7,7 +7,7 @@ COQLIBS := $(shell grep '^-' _CoqProject | tr '\n' ' ') include .make/cc.mk include .make/coq.mk -FAST_TARGETS += check_fiat clean +FAST_TARGETS += check_fiat check_bedrock clean .DEFAULT_GOAL = all .PHONY: all deps objects clean coquille diff --git a/_CoqProject b/_CoqProject index afcbc907e..feb0ebf9c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,5 +1,6 @@ -R src Crypto -R fiat/src Fiat +-R bedrock/Bedrock Bedrock src/Tactics/VerdiTactics.v src/Galois/GaloisField.v src/Galois/GaloisFieldTheory.v diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v index 527acd547..35faf3f03 100644 --- a/src/Galois/GaloisExamples.v +++ b/src/Galois/GaloisExamples.v @@ -1,6 +1,8 @@ Require Import Zpower ZArith Znumtheory. -Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. +Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. +Require Import Crypto.Galois.ComputationalGaloisField. +Require Import Crypto.Galois.AbstractGaloisField. Definition two_5_1 := (two_p 5) - 1. Lemma two_5_1_prime : prime two_5_1. @@ -18,10 +20,10 @@ Module Modulus127_1 <: Modulus. Definition modulus := exist _ two_127_1 two_127_1_prime. End Modulus127_1. - Module Example31. - Module Theory := GaloisFieldTheory Modulus31. - Import Modulus31 Theory Theory.Field. + Module Field := Galois Modulus31. + Module Theory := ComputationalGaloisField Modulus31. + Import Modulus31 Theory Field. Local Open Scope GF_scope. Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2). @@ -45,7 +47,7 @@ Module Example31. End Example31. Module TimesZeroTransparentTestModule. - Module Theory := GaloisFieldTheory Modulus127_1. + Module Theory := ComputationalGaloisField Modulus127_1. Import Modulus127_1 Theory Theory.Field. Local Open Scope GF_scope. @@ -56,7 +58,7 @@ Module TimesZeroTransparentTestModule. End TimesZeroTransparentTestModule. Module TimesZeroParametricTestModule (M: Modulus). - Module Theory := GaloisFieldTheory M. + Module Theory := AbstractGaloisField M. Import M Theory Theory.Field. Local Open Scope GF_scope. diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v deleted file mode 100644 index 2e79453ec..000000000 --- a/src/Galois/GaloisField.v +++ /dev/null @@ -1,216 +0,0 @@ - -Require Import BinInt BinNat ZArith Znumtheory. -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 primeToZ(x: Prime) := proj1_sig x. - Coercion primeToZ: Prime >-> Z. -End GaloisPreliminaries. - -Module Type Modulus. - Parameter modulus: Prime. -End Modulus. - -Module GaloisField (M: Modulus). - Import M. - - Definition GF := {x: Z | x = x mod modulus}. - Definition GFToZ(x: GF) := proj1_sig x. - Coercion GFToZ: GF >-> Z. - - Definition ZToGF (x: Z) : if ((0 <=? x) && (x <? modulus))%bool then GF else True. - break_if; [|trivial]. - exists x. - destruct (Bool.andb_true_eq _ _ (eq_sym Heqb)); clear Heqb. - erewrite Zmod_small; [trivial|]. - intuition. - - rewrite <- Z.leb_le; auto. - - 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. - subst x. - f_equal. - apply UIP_dec. - 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. - abstract trivial. - Defined. - - Definition GFone: GF. - exists 1. - 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. - 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. - exists ((x - y) mod modulus). - abstract (rewrite Zmod_mod; trivial). - Defined. - - Definition GFmult(x y: GF): GF. - exists ((x * y) mod modulus). - abstract (rewrite Zmod_mod; trivial). - Defined. - - Definition GFopp(x: GF): GF := GFminus GFzero x. - - (* Totient Preliminaries *) - Fixpoint GFexp' (x: GF) (power: positive) := - match power with - | xH => x - | xO power' => GFexp' (GFmult x x) power' - | xI power' => GFmult x (GFexp' (GFmult x x) power') - end. - - Definition GFexp (x: GF) (power: N): GF := - match power with - | N0 => GFone - | Npos power' => GFexp' x power' - end. - - (* Inverses + division derived from the existence of a totient *) - Definition isTotient(e: N) := N.gt e 0 /\ forall g: GF, g <> GFzero -> - GFexp g e = GFone. - - Definition Totient := {e: N | isTotient e}. - - Theorem fermat_little_theorem: isTotient (N.pred (Z.to_N modulus)). - Admitted. - - Definition totient : Totient. - exists (N.pred (Z.to_N modulus)). - exact fermat_little_theorem. - Defined. - - Definition totientToN(x: Totient) := proj1_sig x. - Coercion totientToN: Totient >-> N. - - Definition GFinv(x: GF): GF := GFexp x (N.pred totient). - - Definition GFdiv(x y: GF): GF := GFmult x (GFinv y). - -End GaloisField. diff --git a/src/Galois/GaloisFieldTheory.v b/src/Galois/GaloisFieldTheory.v deleted file mode 100644 index bf96ce098..000000000 --- a/src/Galois/GaloisFieldTheory.v +++ /dev/null @@ -1,310 +0,0 @@ - -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. - -Set Implicit Arguments. -Unset Strict Implicits. - -Module GaloisFieldTheory (M: Modulus). - Module Field := GaloisField M. - Export M Field. - - (* 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 *) - - (* Fails iff the input term does some arithmetic with mod'd values. *) - Ltac notFancy E := - match E with - | - (_ mod _) => idtac - | context[_ mod _] => fail 1 - | _ => idtac - end. - - Lemma Zplus_neg : forall n m, n + -m = n - m. - Proof. - auto. - Qed. - - Lemma Zmod_eq : forall a b n, a = b -> a mod n = b mod n. - Proof. - intros; rewrite H; trivial. - Qed. - - (* Remove redundant [mod] operations from the conclusion. *) - Ltac demod := - repeat match goal with - | [ |- context[(?x mod _ + _) mod _] ] => - notFancy x; rewrite (Zplus_mod_idemp_l x) - | [ |- context[(_ + ?y mod _) mod _] ] => - notFancy y; rewrite (Zplus_mod_idemp_r y) - | [ |- context[(?x mod _ - _) mod _] ] => - notFancy x; rewrite (Zminus_mod_idemp_l x) - | [ |- context[(_ - ?y mod _) mod _] ] => - notFancy y; rewrite (Zminus_mod_idemp_r _ y) - | [ |- context[(?x mod _ * _) mod _] ] => - 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 - | [ x : GF |- _ ] => destruct x - end; simpl in *; autorewrite with core; - intuition; demod; try solve [ f_equal; intuition ]. - - Lemma modmatch_eta : forall n, - match n with - | 0 => 0 - | Z.pos y' => Z.pos y' - | Z.neg y' => Z.neg y' - end = n. - Proof. - destruct n; auto. - Qed. - - Hint Rewrite Zmod_mod modmatch_eta. - - (* Ring Theory*) - - Ltac compat := repeat intro; subst; trivial. - - Instance GFplus_compat : Proper (eq==>eq==>eq) GFplus. - Proof. - compat. - Qed. - - Instance GFminus_compat : Proper (eq==>eq==>eq) GFminus. - Proof. - compat. - Qed. - - Instance GFmult_compat : Proper (eq==>eq==>eq) GFmult. - Proof. - compat. - Qed. - - Instance GFopp_compat : Proper (eq==>eq) GFopp. - Proof. - compat. - Qed. - - Definition GFring_theory : ring_theory GFzero GFone GFplus GFmult GFminus GFopp eq. - Proof. - constructor; galois. - Qed. - - (* Power theory *) - - Local Open Scope GF_scope. - - Lemma GFexp'_doubling : forall q r0, GFexp' (r0 * r0) q = GFexp' r0 q * GFexp' r0 q. - Proof. - induction q; simpl; intuition. - rewrite (IHq (r0 * r0)); generalize (GFexp' (r0 * r0) q); intro. - galois. - apply Zmod_eq; ring. - Qed. - - Lemma GFexp'_correct : forall r p, GFexp' r p = pow_pos GFmult r p. - Proof. - induction p; simpl; intuition; - rewrite GFexp'_doubling; congruence. - Qed. - - Hint Immediate GFexp'_correct. - - Lemma GFexp_correct : forall r n, - r^n = pow_N 1 GFmult r n. - Proof. - induction n; simpl; intuition. - Qed. - - Lemma GFexp_correct' : forall r n, - r^id n = pow_N 1 GFmult r n. - Proof. - apply GFexp_correct. - Qed. - - Hint Immediate GFexp_correct'. - - Lemma GFpower_theory : power_theory GFone GFmult eq id GFexp. - Proof. - constructor; auto. - Qed. - - (* 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 _ => isModulusConstant - | exist _ ?z _ => match (isZcst z) with - | NotConstant => NotConstant - | _ => isModulusConstant - end - | _ => NotConstant - end. - - Ltac GFconstants t := - match isGFconstant t with - | NotConstant => NotConstant - | _ => t - end. - - Ltac GFexp_tac t := - match t with - | Z0 => N0 - | Zpos ?n => Ncst (Npos n) - | Z_of_N ?n => Ncst n - | NtoZ ?n => Ncst n - | _ => NotConstant - end. - - Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y. - Proof. - intros; galois. - apply Zeq_is_eq_bool. - trivial. - Qed. - - Lemma GFcomplete : forall (x y: GF), x = y -> Zeq_bool x y = true. - Proof. - intros. - apply Zeq_is_eq_bool. - 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*) - - Lemma GFexp'_pred' : forall x p, - GFexp' p (Pos.succ x) = GFexp' p x * p. - Proof. - induction x; simpl; intuition; try ring. - rewrite IHx; ring. - Qed. - - Lemma GFexp'_pred : forall x p, - p <> 0 - -> x <> 1%positive - -> GFexp' p x = GFexp' p (Pos.pred x) * p. - Proof. - intros; rewrite <- (Pos.succ_pred x) at 1; auto using GFexp'_pred'. - Qed. - - Lemma GFexp_pred : forall p x, - p <> 0 - -> x <> 0%N - -> p^x = p^N.pred x * p. - Proof. - destruct x; simpl; intuition. - destruct (Pos.eq_dec p0 1); subst; simpl; try ring. - rewrite GFexp'_pred by auto. - destruct p0; intuition. - Qed. - - Lemma GF_multiplicative_inverse : forall p, - p <> 0 - -> GFinv p * p = 1. - Proof. - unfold GFinv; destruct totient as [ ? [ ] ]; simpl. - intros. - rewrite <- GFexp_pred; auto using N.gt_lt, N.lt_neq. - intro; subst. - eapply N.lt_irrefl; eauto using N.gt_lt. - Qed. - - Instance GFinv_compat : Proper (eq==>eq) GFinv. - Proof. - compat. - Qed. - - Instance GFdiv_compat : Proper (eq==>eq==>eq) GFdiv. - Proof. - compat. - Qed. - - Hint Immediate GF_multiplicative_inverse GFring_theory. - - Local Hint Extern 1 False => discriminate. - - Definition GFfield_theory : field_theory GFzero GFone GFplus GFmult GFminus GFopp GFdiv GFinv eq. - Proof. - constructor; auto. - Qed. - - (* 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. |