diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Assembly/ConstrainedComputation.v | 6 | ||||
| -rw-r--r-- | src/Galois/GaloisExamples.v | 21 | ||||
| -rw-r--r-- | src/Galois/GaloisTheory.v | 9 | ||||
| -rw-r--r-- | src/Galois/ZGaloisField.v | 50 | ||||
| -rw-r--r-- | src/Rep/WordEquivalence.v | 4 |
6 files changed, 64 insertions, 27 deletions
diff --git a/_CoqProject b/_CoqProject index 9c07ea0dd..538b6efc9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,6 +4,7 @@ src/Tactics/VerdiTactics.v src/Galois/Galois.v src/Galois/GaloisTheory.v +src/Galois/GaloisExamples.v src/Galois/AbstractGaloisField.v src/Galois/ComputationalGaloisField.v src/Galois/ZGaloisField.v diff --git a/src/Assembly/ConstrainedComputation.v b/src/Assembly/ConstrainedComputation.v index f36b75187..aa5702506 100644 --- a/src/Assembly/ConstrainedComputation.v +++ b/src/Assembly/ConstrainedComputation.v @@ -1,12 +1,11 @@ Require Import Bedrock.Word. +(* Expression *) (* THEORY: if we permit operations on joined types, we can represent * vector operations without searching *) Inductive CType: Set := - | Int32: CType - | Int64: CType - | Join: CType -> CType -> CType . + | Words | list word Definition cTypeToWord(type: CType): Type := match type with @@ -44,6 +43,7 @@ Inductive CExpr (type: CType) := Inductive Sub (inType: CType) (outType: CType) := | CRet : Expr outType -> Sub inType outType + (* | Repeat *) | CCompose : forall medType, (Sub inType medType) -> (Sub medType outType) diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v index 35faf3f03..f649701b7 100644 --- a/src/Galois/GaloisExamples.v +++ b/src/Galois/GaloisExamples.v @@ -1,8 +1,7 @@ Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.ComputationalGaloisField. -Require Import Crypto.Galois.AbstractGaloisField. +Require Import Crypto.Galois.ZGaloisField. Definition two_5_1 := (two_p 5) - 1. Lemma two_5_1_prime : prime two_5_1. @@ -21,9 +20,8 @@ Module Modulus127_1 <: Modulus. End Modulus127_1. Module Example31. - Module Field := Galois Modulus31. - Module Theory := ComputationalGaloisField Modulus31. - Import Modulus31 Theory Field. + 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). @@ -32,13 +30,13 @@ Module Example31. field; trivial. Qed. - Lemma example2: forall x: GF, x * (ZToGF 2) = x + x. + Lemma example2: forall x: GF, x * (inject 2) = x + x. Proof. intros; simpl. field. Qed. - Lemma example3: forall x: GF, x ^ 2 + (ZToGF 2) * x + (ZToGF 1) = (x + (ZToGF 1)) ^ 2. + Lemma example3: forall x: GF, x ^ 2 + (inject 2) * x + (inject 1) = (x + (inject 1)) ^ 2. Proof. intros; simpl. field; trivial. @@ -47,8 +45,8 @@ Module Example31. End Example31. Module TimesZeroTransparentTestModule. - Module Theory := ComputationalGaloisField Modulus127_1. - Import Modulus127_1 Theory Theory.Field. + Module Theory := ZGaloisField Modulus127_1. + Import Theory. Local Open Scope GF_scope. Lemma timesZero : forall a, a*0 = 0. @@ -58,13 +56,12 @@ Module TimesZeroTransparentTestModule. End TimesZeroTransparentTestModule. Module TimesZeroParametricTestModule (M: Modulus). - Module Theory := AbstractGaloisField M. - Import M Theory Theory.Field. + Module Theory := ZGaloisField M. + Import Theory. 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/GaloisTheory.v b/src/Galois/GaloisTheory.v index e95eed864..8fa1b4113 100644 --- a/src/Galois/GaloisTheory.v +++ b/src/Galois/GaloisTheory.v @@ -158,14 +158,7 @@ Module GaloisTheory (M: Modulus). (* Ring properties *) - 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. + Ltac GFexp_tac t := Ncst t. Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y. Proof. diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v index 23b1c8dd8..bf9efa964 100644 --- a/src/Galois/ZGaloisField.v +++ b/src/Galois/ZGaloisField.v @@ -1,6 +1,6 @@ Require Import BinInt BinNat ZArith Znumtheory. -Require Import BoolEq. +Require Import BoolEq Field_theory. Require Import Galois GaloisTheory. Module ZGaloisField (M: Modulus). @@ -26,13 +26,59 @@ Module ZGaloisField (M: Modulus). symmetry; apply Zeq_bool_eq; trivial. Qed. + Lemma GFmorph_div_theory: + div_theory eq Zplus Zmult inject Z.quotrem. + Proof. + constructor; intros; intuition. + 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. + + Lemma injectZeroIsGFZero : + GFzero = inject 0. + Proof. + apply gf_eq; simpl; trivial. + Qed. + + Lemma injectOneIsGFOne : + GFone = inject 1. + Proof. + apply gf_eq; simpl; intuition. + symmetry; apply Zmod_small; destruct modulus; simpl; + apply prime_ge_2 in p; intuition. + Qed. + + Ltac GFpreprocess := + repeat rewrite injectZeroIsGFZero; + repeat rewrite injectOneIsGFOne. + + Ltac GFpostprocess := + repeat rewrite <- injectZeroIsGFZero; + repeat rewrite <- injectOneIsGFOne. + + Ltac GFconstant t := + match t with + | inject ?x => x + | _ => NotConstant + end. + Add Ring GFring_Z : GFring_theory (morphism GFring_morph, + constants [GFconstant], + div GFmorph_div_theory, power_tac GFpower_theory [GFexp_tac]). Add Field GFfield_Z : GFfield_theory (morphism GFring_morph, - power_tac GFpower_theory [GFexp_tac]). + preprocess [GFpreprocess], + postprocess [GFpostprocess], + constants [GFconstant], + div GFmorph_div_theory, + power_tac GFpower_theory [GFexp_tac]). End ZGaloisField. diff --git a/src/Rep/WordEquivalence.v b/src/Rep/WordEquivalence.v index 4005adc2a..840919a49 100644 --- a/src/Rep/WordEquivalence.v +++ b/src/Rep/WordEquivalence.v @@ -37,13 +37,13 @@ Module GFBits (M: Modulus). 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 toGF (b: BinGF) := inject ((toZ b) mod modulus) Definition fromZ (x: Z) := splitWords numWords (NToWord (Z.to_N x)) Definition fromGF (x: GF) := fromZ (proj1_sig x). toZ a + toZ b = toZ (a ^+ b) - + Lemma equivalent_GF : BinEquiv x y <-> x = toGF y. Admitted. |