scalarmult support; EdDSA.sign produces valid signatures

4 files changed, 45 insertions, 61 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 1b2a62ea6..b1fdc69a3 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1,10 +1,11 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
 Require Import Crypto.Util.Tactics Crypto.Tactics.Nsatz.
 Require Import Crypto.Util.Decidable.
+Require Coq.Numbers.Natural.Peano.NPeano.
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
 
 Module Import ModuloCoq8485.
-  Require Import NPeano Nat.
+  Import NPeano Nat.
   Infix "mod" := modulo (at level 40, no associativity).
 End ModuloCoq8485.
 
@@ -345,45 +346,53 @@ Module Group.
 
   Section ScalarMult.
     Context {G eq add zero opp} `{@group G eq add zero opp}.
-    Context {mul:nat->G->G} {Proper_mul : Proper (Logic.eq==>eq==>eq) mul}.
+    Context {mul:nat->G->G}.
     Local Infix "=" := eq : type_scope. Local Infix "=" := eq.
     Local Infix "+" := add. Local Infix "*" := mul.
-    Context {mul_0_l : forall P, 0 * P = zero} {mul_S_l : forall n P, S n * P = P + n * P}.
+    Class is_scalarmult :=
+      {
+        scalarmult_0_l : forall P, 0 * P = zero;
+        scalarmult_S_l : forall n P, S n * P = P + n * P;
+
+        scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul
+      }.
+    Global Existing Instance scalarmult_Proper.
+    Context `{is_scalarmult}.
 
-    Lemma mul_1_l : forall P, 1*P = P.
-    Proof. intros. rewrite mul_S_l, mul_0_l, right_identity; reflexivity. Qed.
+    Lemma scalarmult_1_l : forall P, 1*P = P.
+    Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
 
-    Lemma mul_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
+    Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
     Proof.
       induction n; intros;
-        rewrite ?mul_0_l, ?mul_S_l, ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
+        rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
     Qed.
 
-    Lemma mul_zero_r : forall m, m * zero = zero.
-    Proof. induction m; rewrite ?mul_S_l, ?mul_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
+    Lemma scalarmult_zero_r : forall m, m * zero = zero.
+    Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
 
-    Lemma mul_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
+    Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
     Proof.
       induction n; intros.
-      { rewrite PeanoNat.Nat.mul_0_r, !mul_0_l. reflexivity. }
-      { rewrite mul_S_l, <-mult_n_Sm, <-PeanoNat.Nat.add_comm, mul_add_l. apply cancel_left, IHn. }
+      { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. }
+      { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. apply cancel_left, IHn. }
     Qed.
 
     Lemma opp_mul : forall n P, opp (n * P) = n * (opp P).
       induction n; intros.
-      { rewrite !mul_0_l, inv_id; reflexivity. }
-      { rewrite <-PeanoNat.Nat.add_1_r at 1.
-        rewrite mul_add_l, mul_1_l, inv_op, mul_S_l, cancel_left; eauto. }
+      { rewrite !scalarmult_0_l, inv_id; reflexivity. }
+      { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1.
+        rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. }
     Qed.
 
-    Lemma mul_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero.
-    Proof. intros ? ? Hl ?. rewrite <-mul_assoc, Hl, mul_zero_r. reflexivity. Qed.
+    Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero.
+    Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed.
 
-    Lemma mul_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B.
+    Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B.
     Proof.
       intros ? ? Hnz Hmod ?.
       rewrite (NPeano.Nat.div_mod n l Hnz) at 2.
-      rewrite mul_add_l, mul_times_order, left_identity by auto. reflexivity.
+      rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
     Qed.
   End ScalarMult.
 End Group.
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index e3809bb8a..0afc07c5d 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -138,25 +138,14 @@ Module E.
       match goal with | |- _ <> 0 => admit end.
     Admitted.
 
-    (* TODO: move to [Group] and [AbelianGroup] as appropriate *)
-    Lemma mul_0_l : forall P, (0 * P = zero)%E.
-    Proof. intros; reflexivity. Qed.
-    Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E.
-    Proof. intros; reflexivity. Qed.
-    Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E.
+    Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul.
     Proof.
-      induction n; intros;
-        rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
+      intros n m Hnm P Q HPQ. rewrite <-Hnm; clear Hnm m.
+      induction n; simpl; rewrite ?IHn, ?HPQ; reflexivity.
     Qed.
-    Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E.
-    Proof.
-      induction n; intros; [reflexivity|].
-      rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity.
-    Qed.
-    Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
-    Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed.
-    Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E.
-    Admitted.
+
+    Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul.
+    Proof. split; intros; reflexivity || typeclasses eauto. Qed.
 
     Section PointCompression.
       Local Notation "x ^ 2" := (x*x).
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
index 44e251b3b..cf9083061 100644
--- a/src/Experiments/EdDSARefinement.v
+++ b/src/Experiments/EdDSARefinement.v
@@ -2,6 +2,7 @@ Require Import Crypto.Spec.EdDSA Bedrock.Word.
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Algebra. Import Group.
 Require Import Util.Decidable Util.Option Util.Tactics.
+Require Import Omega.
 
 Module Import NotationsFor8485.
   Import NPeano Nat.
@@ -19,7 +20,6 @@ Section EdDSA.
   Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
   Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}.
   Context {Proper_Eadd : Proper (Eeq==>Eeq==>Eeq) Eadd}.
-  Context {Proper_EscalarMult : Proper (Logic.eq==>Eeq==>Eeq) EscalarMult}.
 
   Context {decE:word b-> option E}.
   Context {decS:word b-> option nat}.
@@ -85,28 +85,12 @@ Section EdDSA.
 
   Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
   Proof.
-    cbv [sign public].
-    intros. subst. constructor.
-    rewrite (@mul_mod_order E Eeq Eadd Ezero Eopp _ EscalarMult _).
-    rewrite (@mul_add_l E Eeq Eadd Ezero Eopp _ EscalarMult).
-    eapply cancel_left.
-    rewrite (@mul_mod_order E Eeq Eadd Ezero Eopp _ EscalarMult _).
-    symmetry.
-    rewrite NPeano.Nat.mul_comm.
-    eapply (@mul_assoc E Eeq Eadd Ezero Eopp _ EscalarMult _ _ (wordToNat _) (curveKey sk) B).
-
-    admit.
-    admit.
-    admit.
-
-    admit.
-    
-    admit.
-    admit.
-    admit.
-    admit.
-    admit.
-
-    admit.
-  Admitted.
+    cbv [sign public]. intros. subst. split.
+    rewrite scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, NPeano.Nat.mul_comm, scalarmult_assoc;
+      try solve [ reflexivity
+                | pose proof EdDSA_l_odd; omega
+                | apply EdDSA_l_order_B
+                | rewrite scalarmult_assoc, mult_comm, <-scalarmult_assoc,
+                             EdDSA_l_order_B, scalarmult_zero_r; reflexivity ].
+  Qed.
 End EdDSA.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 7e4d3ed25..03a723e10 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -37,6 +37,7 @@ Section EdDSA.
     :=
       {
         EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
+        EdDSA_scalarmult:@Algebra.Group.is_scalarmult E Eeq Eadd Ezero EscalarMult;
 
         EdDSA_c_valid : c = 2 \/ c = 3;
 
@@ -50,6 +51,7 @@ Section EdDSA.
         EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero
       }.
   Global Existing Instance EdDSA_group.
+  Global Existing Instance EdDSA_scalarmult.
 
   Context `{prm:EdDSA}.