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.

2 files changed, 19 insertions, 17 deletions

diff --git a/src/Spec/CompleteEwardsCurve.v b/src/Spec/CompleteEwardsCurve.v
index 7ebf35988..8eeefe03b 100644
--- a/src/Spec/CompleteEwardsCurve.v
+++ b/src/Spec/CompleteEwardsCurve.v
@@ -6,17 +6,18 @@ Require Import Crypto.Spec.ModularArithmetic.
 Local Open Scope F_scope.
 
 Class TwistedEdwardsParams := {
-  p : BinInt.Z;
-  a : F p;
-  d : F p;
-  modulus_prime : Znumtheory.prime p;
+  q : BinInt.Z;
+  a : F q;
+  d : F q;
+  modulus_prime : Znumtheory.prime q;
   a_nonzero : a <> 0;
   a_square : exists sqrt_a, sqrt_a^2 = a;
   d_nonsquare : forall x, x^2 <> d
 }.
 
 Section TwistedEdwardsCurves.
-  Context `{prm:TwistedEdwardsParams}.
+  Context {prm:TwistedEdwardsParams}.
+
   (* Twisted Edwards curves with complete addition laws. References:
   * <https://eprint.iacr.org/2008/013.pdf>
   * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
@@ -24,9 +25,7 @@ Section TwistedEdwardsCurves.
   *)
   Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
   Definition point := { P | onCurve P}.
-  Definition mkPoint xy proof : point := exist onCurve xy proof.
-  Definition projX (P:point) : F p := fst (proj1_sig P).
-  Definition projY (P:point) : F p:= snd (proj1_sig P).
+  Definition mkPoint (xy:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf.
 
   Definition zero : point := mkPoint (0, 1) Pre.zeroOnCurve.
   
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