diff options
author | 2016-02-11 16:32:41 -0500 | |
---|---|---|
committer | 2016-06-22 13:39:03 -0400 | |
commit | 15978c2ec1dea0ee4c1a84d8d56409b575af52cc (patch) | |
tree | bcd7c1cd23ac35a001774782cf981f4f0caef590 /src/Spec/ModularArithmetic.v | |
parent | 0a8df431e015d70695c6a8d0c5fb73937d9db89f (diff) |
Define F m, a replacement for GF with several benefits.
- F has a human readable complete specification
- F is a parametric type, not a parametric module
- Different F instances can be disambiguated by type inference,
which is more conventient that notation scopes.
- F has significant support for non-prime moduli
- It should be relatively easy to port existing GF code to F.
Since the repository currently contains code referencing both F and GF,
it makes sense to keep the names different for now. Later, F may or may
not be renamed to GF.
Diffstat (limited to 'src/Spec/ModularArithmetic.v')
-rw-r--r-- | src/Spec/ModularArithmetic.v | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index 7f31161e2..e2243dfff 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -1,4 +1,4 @@ -Require Znumtheory BinInt BinNums. +Require Znumtheory BinNums. Require Crypto.ModularArithmetic.Pre. @@ -19,29 +19,32 @@ Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope. Local Open Scope Z_scope. Definition F (modulus : BinInt.Z) := { z : BinInt.Z | z = z mod modulus }. +Coercion FieldToZ {m} (a:F m) : BinNums.Z := proj1_sig a. + Section FieldOperations. Context {m : BinInt.Z}. - Let Fm := F m. (* TODO: if inlined, coercions say "anomaly please report" *) - Coercion ZToField (a:BinInt.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m). - Coercion FieldToZ (a:Fm) : BinInt.Z := proj1_sig a. - + Let Fm := F m. (* Note: if inlined, coercions say "anomaly please report" *) + Coercion unfoldFm (a:Fm) : F m := a. + Coercion ZToField (a:BinNums.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m). + Definition add (a b:Fm) : Fm := ZToField (a + b). Definition mul (a b:Fm) : Fm := ZToField (a * b). Parameter opp : Fm -> Fm. - Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0 /\ opp a = opp a mod m. + Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0. Definition sub (a b:Fm) : Fm := add a (opp b). Parameter inv : Fm -> Fm. - Axiom F_inv_spec : forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0 /\ inv a = inv a mod m. + Axiom F_inv_spec : Znumtheory.prime m -> forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0. Definition div (a b:Fm) : Fm := mul a (inv b). Parameter pow : Fm -> BinNums.N -> Fm. - Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x y, pow a (x + y)%N = pow a x * pow a y. + Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x, pow a (1 + x)%N = mul a (pow a x). End FieldOperations. Delimit Scope F_scope with F. +Arguments F _%Z. Arguments ZToField {_} _%Z : simpl never. Arguments add {_} _%F _%F : simpl never. Arguments mul {_} _%F _%F : simpl never. @@ -57,4 +60,4 @@ Infix "-" := sub : F_scope. Infix "/" := div : F_scope. Infix "^" := pow : F_scope. Notation "0" := (ZToField 0) : F_scope. -Notation "1" := (ZToField 1) : F_scope. +Notation "1" := (ZToField 1) : F_scope.
\ No newline at end of file |