added proofs about addition chain exponentiation for later use in ModularBaseSystem [pow], which we need for sqrt and inversion.

7 files changed, 139 insertions, 15 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 62b216b92..f9dfbd519 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -345,9 +345,11 @@ Module Group.
         auto using associative, left_identity, right_identity, left_inverse, right_inverse.
     Qed.
   End GroupByHomomorphism.
+End Group.
 
-  Section ScalarMult.
-    Context {G eq add zero opp} `{@group G eq add zero opp}.
+Module ScalarMult.
+  Section ScalarMultProperties.
+    Context {G eq add zero} `{@monoid G eq add zero}.
     Context {mul:nat->G->G}.
     Local Infix "=" := eq : type_scope. Local Infix "=" := eq.
     Local Infix "+" := add. Local Infix "*" := mul.
@@ -377,14 +379,8 @@ Module Group.
     Proof.
       induction n; intros.
       { 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 !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. }
+      { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l.
+        rewrite IHn. reflexivity. }
     Qed.
 
     Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero.
@@ -396,8 +392,16 @@ Module Group.
       rewrite (NPeano.Nat.div_mod n l Hnz) at 2.
       rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
     Qed.
-  End ScalarMult.
-End Group.
+    Context {opp} {group:@group G eq add zero opp}.
+
+    Lemma opp_mul : forall n P, opp (n * P) = n * (opp P).
+      induction n; intros.
+      { rewrite !scalarmult_0_l, Group.inv_id; reflexivity. }
+      { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1.
+        rewrite scalarmult_add_l, scalarmult_1_l, Group.inv_op, scalarmult_S_l, Group.cancel_left; eauto. }
+    Qed.
+  End ScalarMultProperties.
+End ScalarMult.
 
 Require Coq.nsatz.Nsatz.
 
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 0afc07c5d..65d899463 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -10,7 +10,7 @@ Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Notations.
 
 Module E.
-  Import Group Ring Field CompleteEdwardsCurve.E.
+  Import Group ScalarMult Ring Field CompleteEdwardsCurve.E.
   Section CompleteEdwardsCurveTheorems.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
index 79c9b05dd..484650934 100644
--- a/src/Experiments/EdDSARefinement.v
+++ b/src/Experiments/EdDSARefinement.v
@@ -1,6 +1,6 @@
 Require Import Crypto.Spec.EdDSA Bedrock.Word.
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Algebra. Import Group.
+Require Import Crypto.Algebra. Import Group ScalarMult.
 Require Import Util.Decidable Util.Option Util.Tactics.
 Require Import Omega.
 
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 03a723e10..25109bc4c 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -37,7 +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_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero EscalarMult;
 
         EdDSA_c_valid : c = 2 \/ c = 3;
 
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v
new file mode 100644
index 000000000..ca1394115
--- /dev/null
+++ b/src/Util/AdditionChainExponentiation.v
@@ -0,0 +1,102 @@
+Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations.
+Require Import Crypto.Util.ListUtil.
+Require Import Algebra. Import Monoid ScalarMult.
+Require Import VerdiTactics.
+Require Import Crypto.Util.Option.
+
+Section AddChainExp.
+  Function add_chain (is:list (nat*nat)) : list nat :=
+    match is with
+    | nil => nil
+    | (i,j)::is' =>
+      let chain' := add_chain is' in
+      nth_default 1 chain' i + nth_default 1 chain' j::chain'
+    end.
+
+Example wikipedia_addition_chain : add_chain (rev [
+(0, 0); (* 2 = 1 + 1 *) (* the indices say how far back the chain to look *)
+(0, 1); (* 3 = 2 + 1 *)
+(0, 0); (* 6 = 3 + 3 *)
+(0, 0); (* 12 = 6 + 6 *)
+(0, 0); (* 24 = 12 + 12 *)
+(0, 2); (* 30 = 24 + 6 *)
+(0, 6)] (* 31 = 30 + 1 *)
+) = [31; 30; 24; 12; 6; 3; 2]. reflexivity. Qed.
+
+  Context {G eq op id} {monoid:@Algebra.monoid G eq op id}.
+  Local Infix "=" := eq : type_scope.
+
+  Function add_chain_exp (is : list (nat*nat)) (x : G) : list G :=
+    match is with
+    | nil => nil
+    | (i,j)::is' =>
+      let chain' := add_chain_exp is' x in
+      op (nth_default x chain' i) (nth_default x chain' j) ::chain'
+    end.
+
+  Fixpoint scalarmult n (x : G) : G := match n with
+    | O    => id
+    | S n' => op x (scalarmult n' x)
+    end.
+
+  Lemma add_chain_exp_step : forall i j is x,
+    (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x) ->
+    (eqlistA eq)
+    (add_chain_exp ((i,j) :: is) x)
+      (op (scalarmult (nth_default 1 (add_chain is) i) x)
+         (scalarmult (nth_default 1 (add_chain is) j) x) :: add_chain_exp is x).
+  Proof.
+    intros.
+    unfold add_chain_exp; fold add_chain_exp.
+    apply eqlistA_cons; [ | reflexivity].
+    f_equiv; auto.
+  Qed.
+
+  Lemma scalarmult_same : forall c x y, eq x y -> eq (scalarmult c x) (scalarmult c y).
+  Proof.
+    induction c; intros.
+    + reflexivity.
+    + simpl. f_equiv; auto.
+  Qed.
+
+  Lemma scalarmult_pow_add : forall a b x, scalarmult (a + b) x = op (scalarmult a x) (scalarmult b x).
+  Proof.
+    intros; eapply scalarmult_add_l.
+    Grab Existential Variables.
+    2:eauto.
+    econstructor; try reflexivity.
+    repeat intro; subst.
+    auto using scalarmult_same.
+  Qed.
+
+  Lemma add_chain_exp_spec : forall is x,
+    (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x).
+  Proof.
+    induction is; intros.
+    + simpl; rewrite !nth_default_nil. cbv.
+      symmetry; apply right_identity.
+    + destruct a.
+      rewrite add_chain_exp_step by auto.
+      unfold add_chain; fold add_chain.
+      destruct n.
+      - rewrite !nth_default_cons, scalarmult_pow_add. reflexivity.
+      - rewrite !nth_default_cons_S; auto.
+  Qed.
+
+  Lemma add_chain_exp_answer : forall is x n, Logic.eq (head (add_chain is)) (Some n) ->
+    option_eq eq (Some (scalarmult n x)) (head (add_chain_exp is x)).
+  Proof.
+    intros.
+    change head with (fun {T} (xs : list T) => nth_error xs 0) in *.
+    cbv beta in *.
+    cbv [option_eq].
+    destruct is; [ discriminate | ].
+    destruct p.
+    simpl in *.
+    injection H; clear H; intro H.
+    subst n.
+    rewrite !add_chain_exp_spec.
+    apply scalarmult_pow_add.
+  Qed.
+
+End AddChainExp.
\ No newline at end of file
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 50927c2a4..b4285aad0 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -926,3 +926,12 @@ Proof.
   rewrite <-!app_comm_cons, !map2_cons.
   rewrite IHls1; auto.
 Qed.
+
+Require Import Coq.Lists.SetoidList.
+Global Instance Proper_nth_default : forall A eq,
+  Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)).
+Proof.
+  do 5 intro; subst; induction 1.
+  + repeat intro; rewrite !nth_default_nil; assumption.
+  + repeat intro; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto.
+Qed.
diff --git a/src/Util/Option.v b/src/Util/Option.v
index db4b69dde..2c11771ff 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -60,3 +60,12 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect
          | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
            => change (option_rect P S N (Some x)) with (S x); cbv beta
          end.
+
+Definition option_eq {A} eq (x y : option A) :=
+  match x with
+  | None    => y = None
+  | Some ax => match y with
+               | None => False
+               | Some ay => eq ax ay
+               end
+  end.