use [positive] for [F] modulus, char_ge_C instead of char_gt_C

7 files changed, 79 insertions, 103 deletions

diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 801b31ffc..daaa2ed74 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -11,7 +11,7 @@ Module E.
 
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)}
+            {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
             {Feq_dec:Decidable.DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 02f59c9e5..4fc3afce4 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -12,10 +12,10 @@ Section Ed25519.
 
   Local Open Scope Z_scope.
 
-  Definition q : BinNums.Z := 2^255 - 19.
+  Definition q : BinPos.positive := 2^255 - 19.
   Definition Fq : Type := F q.
 
-  Definition l : BinNums.Z := 2^252 + 27742317777372353535851937790883648493.
+  Definition l : BinPos.positive := 2^252 + 27742317777372353535851937790883648493.
   Definition Fl : Type := F l.
 
   Local Open Scope F_scope.
@@ -51,10 +51,10 @@ Section Ed25519.
     let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x).
   Definition Senc : Fl -> Word.word b := Fencode (len:=b).
 
-  Local Instance char_gt_2 : (* TODO: prove this in PrimeFieldTheorems *)
-    @Ring.char_gt (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0)
+  Local Instance char_gt_e : (* TODO: prove this in PrimeFieldTheorems *)
+    @Ring.char_ge (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0)
                   (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) 
-                  (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.one).
+                  (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.two).
   Proof. intros p ?.
          edestruct (fun p:p = (BinNat.N.succ_pos BinNat.N.zero) \/ p = (BinNat.N.succ_pos BinNat.N.one) => p); subst.
          { admit. (* 
@@ -75,21 +75,18 @@ Section Ed25519.
   Let mul := E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d).
   Let zero := E.zero(nonzero_a:=nonzero_a)(d:=d).
 
-  Definition ed25519 (l_order_B: E.eq (mul (BinInt.Z.to_nat l) B)%E zero) :
+  Definition ed25519 (l_order_B: E.eq(F:=Fq)(Fone:=F.one) (mul (BinInt.Z.to_nat l) B)%E zero) :
     EdDSA (E:=E) (Eadd:=add) (Ezero:=zero) (EscalarMult:=mul) (B:=B)
           (Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *)
           (Eeq:=E.eq) (* TODO: move defn *)
           (l:=l) (b:=b) (n:=n) (c:=c)
           (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512).
   Proof.
-    split; try exact _.
-    (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *)
-    (* timeout 1 match goal with H:?P |- ?P => idtac end. *)
-    Crypto.Util.Decidable.vm_decide.
-    Crypto.Util.Decidable.vm_decide.
-    Crypto.Util.Decidable.vm_decide.
-    Crypto.Util.Decidable.vm_decide.
-    Crypto.Util.Decidable.vm_decide.
-    exact l_order_B.
+    split; 
+      match goal with
+      | |- ?P => match goal with [H:P|-_] => exact H end (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *)
+      | _ => exact _
+      | _ => Crypto.Util.Decidable.vm_decide
+      end.
   Qed.
 End Ed25519.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index f8581c4c9..67a1014f6 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -33,7 +33,7 @@ Section EdDSA.
         {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *)
         {c : nat} (* cofactor E = 2^c *)
         {n : nat} (* secret keys are (n+1) bits *)
-        {l : BinInt.Z} (* order of the subgroup of E generated by B *)
+        {l : BinPos.positive} (* order of the subgroup of E generated by B *)
 
         {B : E} (* base point *)
 
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index a3e80fcf9..ed6a0c4a2 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -2,6 +2,13 @@ Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums.
 
 Require Crypto.ModularArithmetic.Pre.
 
+Delimit Scope positive_scope with positive.
+Bind Scope positive_scope with BinPos.positive.
+Infix "+" := BinPos.Pos.add : positive_scope.
+Infix "*" := BinPos.Pos.mul : positive_scope.
+Infix "-" := BinPos.Pos.sub : positive_scope.
+Infix "^" := BinPos.Pos.pow : positive_scope.
+
 Delimit Scope N_scope with N.
 Bind Scope N_scope with BinNums.N.
 Infix "+" := BinNat.N.add : N_scope.
@@ -18,17 +25,20 @@ Infix "-" := BinInt.Z.sub : Z_scope.
 Infix "/" := BinInt.Z.div : Z_scope.
 Infix "^" := BinInt.Z.pow : Z_scope.
 Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope.
+
 Local Open Scope Z_scope.
+Global Coercion BinInt.Z.pos : BinPos.positive >-> BinInt.Z.
+Global Coercion BinInt.Z.of_N : BinNums.N >-> BinInt.Z.
+Global Set Printing Coercions.
 
 Module F.
-  Definition F (m : BinInt.Z) := { z : BinInt.Z | z = z mod m }.
-  Bind Scope F_scope with F.
+  Definition F (m : BinPos.positive) := { z : BinInt.Z | z = z mod m }.
   Local Obligation Tactic := cbv beta; auto using Pre.Z_mod_mod.
   Program Definition of_Z  m  (a:BinNums.Z) : F m := a mod m.
   Definition to_Z {m} (a:F m) : BinNums.Z := proj1_sig a.
 
   Section FieldOperations.
-    Context {m : BinInt.Z}.
+    Context {m : BinPos.positive}.
     Definition zero : F m := of_Z m 0.
     Definition one : F m := of_Z m 1.
 
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v
index 7a9845e7e..5b0bdb545 100644
--- a/src/Spec/ModularWordEncoding.v
+++ b/src/Spec/ModularWordEncoding.v
@@ -11,7 +11,7 @@ Require Crypto.Encoding.ModularWordEncodingPre.
 Local Open Scope nat_scope.
 
 Section ModularWordEncoding.
-  Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}.
+  Context {m : positive} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}.
 
   Definition Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)).
 
diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v
index 5f7246011..2717f6bbc 100644
--- a/src/Spec/MontgomeryCurve.v
+++ b/src/Spec/MontgomeryCurve.v
@@ -6,7 +6,7 @@ Require Import Crypto.Spec.WeierstrassCurve.
 Module M.
   Section MontgomeryCurve.
     Import BinNat.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
@@ -28,20 +28,26 @@ Module M.
                               end }.
     Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P.
 
+    Definition eq (P1 P2:point) :=
+      match coordinates P1, coordinates P2 with
+      | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2
+      | ∞, ∞ => True
+      | _, _ => False
+      end.
+
     Import Crypto.Util.Tactics Crypto.Algebra.Field.
     Ltac t :=
       destruct_head' point; destruct_head' sum; destruct_head' prod;
         break_match; simpl in *; break_match_hyps; trivial; try discriminate;
         repeat match goal with
                | |- _ /\ _ => split
-               | [H:@eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H
-               | [H:@eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H
+               | [H:@Logic.eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H
+               | [H:@Logic.eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H
                end;
         subst; try fsatz.
 
     Program Definition add (P1 P2:point) : point :=
-      exist _
-            match coordinates P1, coordinates P2 return _ with
+            match coordinates P1, coordinates P2 return F*F+∞ with
               (x1, y1), (x2, y2) =>
               if Decidable.dec (x1 = x2)
               then if Decidable.dec (y1 = - y2)
@@ -51,53 +57,39 @@ Module M.
             | ∞, ∞ =>                      ∞
             | ∞, _ =>                      coordinates P2
             | _, ∞ =>                      coordinates P1
-            end _.
+            end.
     Next Obligation. Proof. t. Qed.
 
     Program Definition opp (P:point) : point :=
-      exist _
-            match P with
-            | (x, y) => (x, -y)
-            | ∞ => ∞
-            end _.
-    Next Obligation.
-    Proof. t. Qed.
+      match P return F*F+∞ with
+      | (x, y) => (x, -y)
+      | ∞ => ∞
+      end.
+    Next Obligation. Proof. t. Qed.
 
     Local Notation "4" := (1+3).
     Local Notation "16" := (4*4).
     Local Notation "9" := (3*3).
     Local Notation "27" := (3*9).
-    Context {char_gt_27:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 27}.
+    Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
 
     Let WeierstrassA := ((3-a^2)/(3*b^2)).
     Let WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
-
     Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
-    Program Definition MontgomeryOfWeierstrass (P:Wpoint) : point :=
-      exist
-        _
-        match W.coordinates P return _ with
-        | (x,y) => (b*x-a/3, b*y)
-        | _ => ∞
-        end
-        _.
-    Next Obligation.
-    Proof. subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed.
+    Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
 
-    Definition eq (P1 P2:point) :=
-      match coordinates P1, coordinates P2 with
-      | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2
-      | ∞, ∞ => True
-      | _, _ => False
+    Program Definition of_Weierstrass (P:Wpoint) : point :=
+      match W.coordinates P return F*F+∞ with
+      | (x,y) => (b*x-a/3, b*y)
+      | _ => ∞
       end.
+    Next Obligation.
+    Proof. clear char_ge_3; subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed.
 
-    Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_gt_2 WeierstrassA WeierstrassB).
-    Lemma MontgomeryOfWeierstrass_add P1 P2 :
-      eq (MontgomeryOfWeierstrass (W.add P1 P2))
-         (add (MontgomeryOfWeierstrass P1) (MontgomeryOfWeierstrass P2)).
-    Proof.
-      cbv [WeierstrassA WeierstrassB eq MontgomeryOfWeierstrass W.add add coordinates W.coordinates proj1_sig] in *; t.
-    Qed.
+    Lemma of_Weierstrass_add P1 P2 :
+      eq (of_Weierstrass (W.add P1 P2))
+         (add (of_Weierstrass P1) (of_Weierstrass P2)).
+    Proof. cbv [WeierstrassA WeierstrassB eq of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *; clear char_ge_3; t. Qed.
     
     Section AddX.
       Lemma homogeneous_x_differential_addition_releations P1 P2 :
@@ -110,30 +102,20 @@ Module M.
           end.
       Proof. t. Qed.
 
-      Definition onCurve xy := let 'pair x y := xy in b*y^2 = x^3 + a*x^2 + x.
-      Definition xzpoint := { xz | let 'pair x z := xz in (z = 0 \/ exists y, onCurve (pair (x/z) y)) }.
-      Definition xzcoordinates (P:xzpoint) : F*F := proj1_sig P.
-      Program Definition toxz (P:point) : xzpoint :=
-        exist _
-              match coordinates P with
-              | (x, y) => pair x 1
-              | ∞ => pair 1 0
-              end _.
-      Next Obligation. t; [right; exists f0; t | left; reflexivity ]. Qed.
-
-      Definition sig_pair_to_pair_sig {T T' I I'} (xy:{xy | let 'pair x y := xy in I x /\ I' y})
-        : prod {x:T | I x} {y:T' | I' y}
-        := let 'exist (pair x y) (conj pfx pfy) := xy in  pair  (exist _ x pfx) (exist _ y pfy).
+      Program Definition to_xz (P:point) : F*F :=
+        match coordinates P with
+        | (x, y) => pair x 1
+        | ∞ => pair 1 0
+        end.
 
       (* From Explicit Formulas Database by Lange and Bernstein,
          credited to 1987 Montgomery "Speeding the Pollard and elliptic curve
          methods of factorization", page 261, fifth and sixth displays, plus
          common-subexpression elimination, plus assumption Z1=1 *)
       
-      Context {a24:F} {a24_correct:4*a24 = a+2}.
-      Definition xzladderstep (X1:F) (P1 P2:xzpoint) : prod xzpoint xzpoint. refine (
-        sig_pair_to_pair_sig (exist _
-        match xzcoordinates P1, xzcoordinates P2 return _ with
+      Context {a24:F} {a24_correct:4*a24 = a+2}. (* TODO: +2 or -2 ? *)
+      Definition xzladderstep (X1:F) (P1 P2:F*F) : ((F*F)*(F*F)) :=
+        match P1, P2 with
           pair X2 Z2, pair X3 Z3 => 
           let A := X2+Z2 in
           let AA := A^2 in
@@ -149,32 +131,19 @@ Module M.
           let X4 := AA*BB in
           let Z4 := E*(BB + a24*E) in
           (pair (pair X4 Z4) (pair X5 Z5))
-        end _) ).
-      Proof.
-        destruct P1, P2; cbv [onCurve xzcoordinates] in *. t; intuition idtac.
-        { left. fsatz. }
-        { left. fsatz. }
-        admit.
-        admit.
-        admit.
-        admit.
-        { right.
-          admit. (* the following used to work, but slowly:
-          exists ((fun x1 y1 x2 y2 => (2*x1+x1+a)*(3*x1^2+2*a*x1+1)/(2*b*y1)-b*(3*x1^2+2*a*x1+1)^3/(2*b*y1)^3-y1) (f1/f2) x0 (f/f0) x).
-          Algebra.common_denominator_in H.
-          Algebra.common_denominator_in H0.
-          Algebra.common_denominator.
-          abstract Algebra.nsatz.
-
-          idtac.
-          admit.
-          admit.
-          admit.
-          admit.
-          admit. *) }
-        { right.
-          (* exists ((fun x1 y1 x2 y2 => (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) (f1/f2) x0 (f/f0) x). *)
-          (* XXX: this case is probably not true -- there is not necessarily a guarantee that the output x/z is on curve if [X1] was not the x coordinate of the difference of input points as requored *)
+        end.
+
+      Require Import Crypto.Util.Tuple.
+
+      (* TODO: look up this lemma statement -- the current one may not be right *)
+      Lemma xzladderstep_to_xz X1 P1 P2
+        (HX1 : match coordinates (add P1 (opp P2)) with (x,y) => X1 = x | _ => False end)
+        : fieldwise (n:=2) (fieldwise (n:=2) Feq)
+                    (xzladderstep X1 (to_xz P1) (to_xz P2))
+                    (pair (to_xz (add P1 P2)) (to_xz (add P1 P1))).
+        destruct P1 as [[[??]|?]?], P2 as [[[??]|?]?];
+          cbv [fst snd xzladderstep to_xz add coordinates proj1_sig opp fieldwise fieldwise'] in *;
+          break_match_hyps; break_match; repeat split; try contradiction.
       Abort.
     End AddX.
   End MontgomeryCurve.
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index d19f3f786..87b5bcffd 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -9,7 +9,7 @@ Module W.
      * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79)
      *)
 
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope.
     Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope.