refactor scalar multiplication thoery, implement SRepERepMul

7 files changed, 188 insertions, 137 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 9db169816..c0d7dfbe2 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -148,6 +148,14 @@ Section Algebra.
   End AddMul.
 End Algebra.
 
+Section ZeroNeqOne.
+  Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}.
+
+  Lemma one_neq_zero : not (eq one zero).
+  Proof.
+    intro HH; symmetry in HH. auto using zero_neq_one.
+  Qed.
+End ZeroNeqOne.
 
 Module Monoid.
   Section Monoid.
@@ -192,16 +200,106 @@ Module Monoid.
     Qed.
 
   End Monoid.
+
+  Section Homomorphism.
+    Context {T  EQ OP ID} {monoidT:  @monoid T  EQ OP ID }.
+    Context {T' eq op id} {monoidT': @monoid T' eq op id }.
+    Context {phi:T->T'}.
+    Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
+    Class is_homomorphism :=
+      {
+        homomorphism : forall a b,  phi (OP a b) = op (phi a) (phi b);
+
+        is_homomorphism_phi_proper : Proper (respectful EQ eq) phi
+      }.
+    Global Existing Instance is_homomorphism_phi_proper.
+  End Homomorphism.
 End Monoid.
 
-Section ZeroNeqOne.
-  Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}.
+Module ScalarMult.
+  Section ScalarMultProperties.
+    Context {G eq add zero} `{monoidG:@monoid G eq add zero}.
+    Context {mul:nat->G->G}.
+    Local Infix "=" := eq : type_scope. Local Infix "=" := eq.
+    Local Infix "+" := add. Local Infix "*" := mul.
+    Class is_scalarmult :=
+      {
+        scalarmult_0_l : forall P, 0 * P = zero;
+        scalarmult_S_l : forall n P, S n * P = P + n * P;
 
-  Lemma one_neq_zero : not (eq one zero).
-  Proof.
-    intro HH; symmetry in HH. auto using zero_neq_one.
-  Qed.
-End ZeroNeqOne.
+        scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul
+      }.
+    Global Existing Instance scalarmult_Proper.
+    Context `{mul_is_scalarmult:is_scalarmult}.
+
+    Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} :=
+      match n with
+      | O => zero
+      | S n' => add P (scalarmult_ref n' P)
+      end.
+
+    Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref.
+    Proof.
+      repeat intro; subst.
+      match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end.
+      repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity.
+    Qed.
+
+    Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P.
+      induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l).
+    Qed.
+
+    Lemma scalarmult_1_l : forall P, 1*P = P.
+    Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
+
+    Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
+    Proof.
+      induction n; intros;
+        rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; 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 scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
+    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.
+        rewrite IHn. 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 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 scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
+    Qed.
+  End ScalarMultProperties.
+
+  Section ScalarMultHomomorphism.
+      Context {G EQ ADD ZERO} {monoidG:@monoid G EQ ADD ZERO}.
+      Context {H eq add zero} {monoidH:@monoid H eq add zero}.
+      Local Infix "=" := eq : type_scope. Local Infix "=" := eq : eq_scope.
+      Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO MUL }.
+      Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero mul }.
+      Context {phi} {homom:@Monoid.is_homomorphism G EQ ADD H eq add phi}.
+      Context (phi_ZERO:phi ZERO = zero).
+
+      Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P).
+      Proof.
+        setoid_rewrite scalarmult_ext.
+        induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy.
+      Qed.
+  End ScalarMultHomomorphism.
+
+  Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero}
+    : @is_scalarmult G eq add zero (@scalarmult_ref G add zero).
+  Proof. split; try exact _; intros; reflexivity. Qed.
+End ScalarMult.
 
 Module Group.
   Section BasicProperties.
@@ -279,30 +377,37 @@ Module Group.
   Section Homomorphism.
     Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
     Context {H eq op id inv} {groupH:@group H eq op id inv}.
-    Context {phi:G->H}.
+    Context {phi:G->H}`{homom:@Monoid.is_homomorphism G EQ OP H eq op phi}.
     Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
 
-    Class is_homomorphism :=
-      {
-        homomorphism : forall a b,  phi (OP a b) = op (phi a) (phi b);
-
-        is_homomorphism_phi_proper : Proper (respectful EQ eq) phi
-      }.
-    Global Existing Instance is_homomorphism_phi_proper.
-    Context `{is_homomorphism}.
-
     Lemma homomorphism_id : phi ID = id.
     Proof.
       assert (Hii: op (phi ID) (phi ID) = op (phi ID) id) by
-        (rewrite <- homomorphism, left_identity, right_identity; reflexivity).
+          (rewrite <- Monoid.homomorphism, left_identity, right_identity; reflexivity).
       rewrite cancel_left in Hii; exact Hii.
     Qed.
 
     Lemma homomorphism_inv x : phi (INV x) = inv (phi x).
     Proof.
       apply inv_unique.
-      rewrite <- homomorphism, left_inverse, homomorphism_id; reflexivity.
+      rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity.
     Qed.
+
+    Section ScalarMultHomomorphism.
+      Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }.
+      Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }.
+      Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P).
+      Proof. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed.
+
+      Import ScalarMult.
+      Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P).
+      Proof.
+        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 ScalarMultHomomorphism.
   End Homomorphism.
 
   Section Homomorphism_rev.
@@ -340,7 +445,7 @@ Module Group.
     Qed.
 
     Definition homomorphism_from_redundant_representation
-      : @is_homomorphism G EQ OP H eq op phi.
+      : @Monoid.is_homomorphism G EQ OP H eq op phi.
     Proof.
       split; repeat intro; apply phi'_eq; rewrite ?phi'_op, ?phi'_phi_id; easy.
     Qed.
@@ -358,7 +463,7 @@ Module Group.
           {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
           {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
           {phi_id : eq (phi ID) id}
-          : @group H eq op id inv.
+    : @group H eq op id inv.
     Proof.
       repeat split; eauto with core typeclass_instances; intros;
         repeat match goal with
@@ -370,7 +475,7 @@ Module Group.
                  end
                end;
         repeat rewrite <-?phi_op, <-?phi_inv, <-?phi_id;
-      f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse.
+        f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse.
     Qed.
 
     Lemma isomorphism_to_subgroup_group
@@ -384,7 +489,7 @@ Module Group.
           {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
           {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
           {phi_id : eq (phi ID) id}
-          : @group G EQ OP ID INV.
+      : @group G EQ OP ID INV.
     Proof.
       repeat split; eauto with core typeclass_instances; intros;
         eapply eq_phi_EQ;
@@ -398,101 +503,24 @@ Module Group.
     Context {H eq op id inv} {groupH:@group H eq op id inv}.
     Context {K eqK opK idK invK} {groupK:@group K eqK opK idK invK}.
     Context {phi:G->H} {phi':H->K}
-            {Hphi:@is_homomorphism G EQ OP H eq op phi}
-            {Hphi':@is_homomorphism H eq op K eqK opK phi'}.
+            {Hphi:@Monoid.is_homomorphism G EQ OP H eq op phi}
+            {Hphi':@Monoid.is_homomorphism H eq op K eqK opK phi'}.
     Lemma is_homomorphism_compose
           {phi'':G->K}
           (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x))
-      : @is_homomorphism G EQ OP K eqK opK phi''.
+      : @Monoid.is_homomorphism G EQ OP K eqK opK phi''.
     Proof.
       split; repeat intro; rewrite <- !Hphi''.
-      { rewrite !homomorphism; reflexivity. }
+      { rewrite !Monoid.homomorphism; reflexivity. }
       { apply Hphi', Hphi; assumption. }
     Qed.
 
     Global Instance is_homomorphism_compose_refl
-      : @is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x))
+      : @Monoid.is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x))
       := is_homomorphism_compose (fun x => reflexivity _).
   End HomomorphismComposition.
 End Group.
 
-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.
-    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}.
-
-    Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} :=
-      match n with
-      | O => zero
-      | S n' => add P (scalarmult_ref n' P)
-      end.
-
-    Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref.
-    Proof.
-      repeat intro; subst.
-      match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end.
-      repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity.
-    Qed.
-
-    Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P.
-      induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l).
-    Qed.
-
-    Lemma scalarmult_1_l : forall P, 1*P = P.
-    Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
-
-    Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
-    Proof.
-      induction n; intros;
-        rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; 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 scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
-    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.
-        rewrite IHn. 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 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 scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
-    Qed.
-    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.
-
-  Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero}
-    : @is_scalarmult G eq add zero (@scalarmult_ref G add zero).
-  Proof. split; try exact _; intros; reflexivity. Qed.
-End ScalarMult.
-
 Require Coq.nsatz.Nsatz.
 
 Ltac dropAlgebraSyntax :=
@@ -606,7 +634,7 @@ Module Ring.
 
     Class is_homomorphism :=
       {
-        homomorphism_is_homomorphism : Group.is_homomorphism (phi:=phi) (OP:=ADD) (op:=add) (EQ:=EQ) (eq:=eq);
+        homomorphism_is_homomorphism : Monoid.is_homomorphism (phi:=phi) (OP:=ADD) (op:=add) (EQ:=EQ) (eq:=eq);
         homomorphism_mul : forall x y, phi (MUL x y) = mul (phi x) (phi y);
         homomorphism_one : phi ONE = one
       }.
@@ -615,7 +643,7 @@ Module Ring.
     Context `{is_homomorphism}.
 
     Lemma homomorphism_add : forall x y,  phi (ADD x y) = add (phi x) (phi y).
-    Proof. apply Group.homomorphism. Qed.
+    Proof. apply Monoid.homomorphism. Qed.
 
     Definition homomorphism_opp : forall x,  phi (OPP x) = opp (phi x) :=
       (Group.homomorphism_inv (INV:=OPP) (inv:=opp)).
@@ -623,7 +651,7 @@ Module Ring.
     Lemma homomorphism_sub : forall x y, phi (SUB x y) = sub (phi x) (phi y).
     Proof.
       intros.
-      rewrite !ring_sub_definition, Group.homomorphism, homomorphism_opp. reflexivity.
+      rewrite !ring_sub_definition, Monoid.homomorphism, homomorphism_opp. reflexivity.
     Qed.
   End Homomorphism.
 
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index be0a80d1f..e90aad0d8 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -160,17 +160,17 @@ Module E.
     Next Obligation.
       destruct P as [ [? ?] ?]; simpl.
       rewrite_strat bottomup hints field_homomorphism.
-      eauto using is_homomorphism_phi_proper; assumption.
+      eauto using Monoid.is_homomorphism_phi_proper; assumption.
     Qed.
 
     Context {point_phi:Fpoint->Kpoint}
             {point_phi_Proper:Proper (eq==>eq) point_phi}
             {point_phi_correct: forall (P:point), eq (point_phi P) (ref_phi P)}.
 
-    Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi.
+    Lemma lift_homomorphism : @Monoid.is_homomorphism Fpoint eq add Kpoint eq add point_phi.
     Proof.
       repeat match goal with
-             | |- Group.is_homomorphism => split
+             | |- Monoid.is_homomorphism => split
              | |- _ => intro
              | |-  _ /\ _ => split
              | [H: _ /\ _ |- _ ] => destruct H
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 189c4d08b..ab52445ca 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -135,7 +135,7 @@ Module Extended.
         transitivity (to_twisted x + to_twisted x0)%E; rewrite to_twisted_add, ?H, ?H0; reflexivity.
       Qed.
 
-      Lemma homomorphism_to_twisted : @Group.is_homomorphism point eq add Epoint E.eq E.add to_twisted.
+      Lemma homomorphism_to_twisted : @Monoid.is_homomorphism point eq add Epoint E.eq E.add to_twisted.
       Proof. split; trivial using Proper_to_twisted, to_twisted_add. Qed.
 
       Lemma add_from_twisted P Q : eq (from_twisted (P + Q)%E) (add (from_twisted P) (from_twisted Q)).
@@ -145,7 +145,7 @@ Module Extended.
         symmetry; assumption.
       Qed.
 
-      Lemma homomorphism_from_twisted : @Group.is_homomorphism Epoint E.eq E.add point eq add from_twisted.
+      Lemma homomorphism_from_twisted : @Monoid.is_homomorphism Epoint E.eq E.add point eq add from_twisted.
       Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed.
 
       Definition zero : point := from_twisted E.zero.
@@ -235,17 +235,17 @@ Module Extended.
     Next Obligation.
       destruct P as [ [ [ [ ] ? ] ? ] [ ? [ ? ? ] ] ]; unfold onCurve in *; simpl.
       (rewrite_strat bottomup hints field_homomorphism); try assumption.
-      eauto 10 using is_homomorphism_phi_proper, phi_nonzero.
+      eauto 10 using Monoid.is_homomorphism_phi_proper, phi_nonzero.
     Qed.
 
     Context {point_phi:Fpoint->Kpoint}
             {point_phi_Proper:Proper (eq==>eq) point_phi}
             {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}.
 
-    Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq (add(a_eq_minus1:=HFa)(Htwice_d:=HFdd)) Kpoint eq (add(a_eq_minus1:=HKa)(Htwice_d:=HKdd)) point_phi.
+    Lemma lift_homomorphism : @Monoid.is_homomorphism Fpoint eq (add(a_eq_minus1:=HFa)(Htwice_d:=HFdd)) Kpoint eq (add(a_eq_minus1:=HKa)(Htwice_d:=HKdd)) point_phi.
     Proof.
       repeat match goal with
-             | |- Group.is_homomorphism => split
+             | |- Monoid.is_homomorphism => split
              | |- _ => intro
              | |-  _ /\ _ => split
              | [H: _ /\ _ |- _ ] => destruct H
diff --git a/src/EdDSARepChange.v b/src/EdDSARepChange.v
index 5bbea7f48..1efa0d689 100644
--- a/src/EdDSARepChange.v
+++ b/src/EdDSARepChange.v
@@ -1,7 +1,7 @@
 Require Import Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Spec.EdDSA Bedrock.Word.
 Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
-Require Import Crypto.Algebra. Import Group ScalarMult.
+Require Import Crypto.Algebra. Import Monoid Group ScalarMult.
 Require Import Crypto.Util.Decidable Crypto.Util.Option Crypto.Util.Tactics.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.Notations.
diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v
index 92ba91a6d..10d4387a2 100644
--- a/src/Encoding/PointEncoding.v
+++ b/src/Encoding/PointEncoding.v
@@ -126,7 +126,7 @@ Section PointEncoding.
             {phi_sqrt : forall x, Keq (phi (Fsqrt x)) (Ksqrt (phi x))}
             {Fsqrt_square : forall x root, eq x (F.mul root root) -> eq (Fsqrt x) root}.
 
-    Lemma point_phi_homomorphism: @Algebra.Group.is_homomorphism
+    Lemma point_phi_homomorphism: @Algebra.Monoid.is_homomorphism
                                     Fpoint E.eq Fpoint_add
                                     Kpoint Kpoint_eq Kpoint_add point_phi.
     Proof.
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 718d8435d..1deb5fa80 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -4,6 +4,7 @@ Require Import Crypto.Util.Decidable.
 Require Crypto.Specific.GF25519.
 Require Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 Require Crypto.Encoding.PointEncoding.
+Require Crypto.Util.IterAssocOp.
 Import Morphisms.
 
 Context {H: forall n : nat, Word.word n -> Word.word (b + b)}.
@@ -127,6 +128,8 @@ Let ERepEnc :=
                                 (ExtendedCoordinates.Extended.to_twisted P))
   ).
 
+Let SRep := Tuple.tuple (Word.word 32) 8.
+
 Let S2Rep := fun (x : ModularArithmetic.F.F l) =>
                Tuple.map (ZNWord 32)
                (Tuple.from_list_default (BinInt.Z.of_nat 0) 8
@@ -150,6 +153,28 @@ Let ErepAdd :=
                                      a d GF25519.field25519 twedprm_ERep _
                                      eq_a_minus1 twice_d (eq_refl _) ).
 
+Axiom SRep_testbit : SRep -> nat -> bool.
+Axiom ERepSel : bool -> Erep -> Erep -> Erep.
+
+Let SRepERepMul : SRep -> Erep -> Erep := 
+  IterAssocOp.iter_op
+    (op:=ErepAdd)
+    (id:=ExtendedCoordinates.Extended.zero(field:=GF25519.field25519)(prm:=twedprm_ERep))
+    (scalar:=SRep)
+    SRep_testbit
+    (sel:=ERepSel)
+    (BinInt.Z.to_nat (BinInt.Z.log2_up l))
+.
+
+Lemma SRepERepMul_correct n P : 
+  ExtendedCoordinates.Extended.eq
+    (EToRep (CompleteEdwardsCurve.E.mul n P))
+    (SRepERepMul (S2Rep (ModularArithmetic.F.of_nat l n)) (EToRep P)).
+Proof.
+  pose proof @IterAssocOp.iter_op_correct.
+  pose proof @Algebra.ScalarMult.homomorphism_scalarmult.
+Abort.
+
 (* TODO : unclear what we're doing with the placeholder [feEnc] at the moment, so
    leaving this admitted for now *)
 Lemma feEnc_correct : forall x,
@@ -232,13 +257,13 @@ Check @sign_correct
       (* ERepEnc := *) ERepEnc
       (* ERepEnc_correct := *) ERepEnc_correct
       (* Proper_ERepEnc := *) (PointEncoding.Proper_Kencode_point (Kpoint_eq_correct := ext_eq_correct) (Proper_Kenc := Proper_feEnc))
-      (* SRep := *) (Tuple.tuple (Word.word 32) 8)
+      (* SRep := *) SRep
       (* SRepEq := *) (Tuple.fieldwise Logic.eq)
       (* H0 := *) Tuple.Equivalence_fieldwise
       (* S2Rep := *) S2Rep
       (* SRepDecModL := *) _
       (* SRepDecModL_correct := *) _
-      (* SRepERepMul := *) _
+      (* SRepERepMul := *) SRepERepMul
       (* SRepERepMul_correct := *) _
       (* Proper_SRepERepMul := *) _
       (* SRepEnc := *) _
@@ -355,7 +380,7 @@ Check @verify_correct
       (* S2Rep := *) S2Rep
       (* SRepDecModL := *) _
       (* SRepDecModL_correct := *) _
-      (* SRepERepMul := *) _
+      (* SRepERepMul := *) SRepERepMul
       (* SRepERepMul_correct := *) _
       (* Proper_SRepERepMul := *) _
       (* SRepDec := *) _
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 1d553bd55..53d3a14d5 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -11,19 +11,14 @@ Section IterAssocOp.
   Context {T eq op id} {moinoid : @monoid T eq op id}
           {scalar : Type} (scToN : scalar -> N)
           (testbit : scalar -> nat -> bool)
-          (testbit_spec : forall x i, testbit x i = N.testbit_nat (scToN x) i).
+          (testbit_correct : forall x i, testbit x i = N.testbit_nat (scToN x) i).
+  Local Infix "===" := eq. Local Infix "===" := eq : type_scope.
 
-  Fixpoint nat_iter_op n a : T :=
-    match n with
-    | 0%nat => id
-    | S n' => op a (nat_iter_op n' a)
-    end.
+  Local Notation nat_iter_op := (ScalarMult.scalarmult_ref (add:=op) (zero:=id)).
 
-  Lemma nat_iter_op_plus : forall m n a,
+  Lemma nat_iter_op_plus m n a :
     op (nat_iter_op m a) (nat_iter_op n a) === nat_iter_op (m + n) a.
-  Proof.
-    induction m; intros; simpl; rewrite ?left_identity, <-?IHm, ?associative; reflexivity.
-  Qed.
+  Proof. symmetry; eapply ScalarMult.scalarmult_add_l. Qed.
 
   Definition N_iter_op n a :=
     match n with
@@ -46,6 +41,8 @@ Section IterAssocOp.
     induction n using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity.
   Qed.
 
+  Context {sel:bool->T->T->T} {sel_correct:forall b x y, sel b x y = if b then y else x}.
+
   Fixpoint funexp {A} (f : A -> A) (a : A) (exp : nat) : A :=
     match exp with
     | O => a
@@ -55,9 +52,10 @@ Section IterAssocOp.
   Definition test_and_op sc a (state : nat * T) :=
     let '(i, acc) := state in
     let acc2 := op acc acc in
+    let acc2a := op a acc2 in
     match i with
     | O => (0, acc)
-    | S i' => (i', if testbit sc i' then op a acc2 else acc2)
+    | S i' => (i', sel (testbit sc i') acc2 acc2a)
     end.
 
   Definition iter_op bound sc a : T :=
@@ -125,8 +123,9 @@ Section IterAssocOp.
     destruct i; [ apply Hpre | ].
     simpl.
     rewrite Nshiftr_succ.
+    rewrite sel_correct.
     case_eq (testbit sc i); intro testbit_eq; simpl;
-      rewrite testbit_spec in testbit_eq; rewrite testbit_eq;
+      rewrite testbit_correct in testbit_eq; rewrite testbit_eq;
       rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity.
   Qed.
 
@@ -138,7 +137,7 @@ Section IterAssocOp.
   Qed.
 
   Lemma funexp_test_and_op_index : forall n a x acc y,
-    fst (funexp (test_and_op n a) (x, acc) y) === x - y.
+    fst (funexp (test_and_op n a) (x, acc) y) = x - y.
   Proof.
     induction y; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity.
     match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end.
@@ -181,7 +180,7 @@ Section IterAssocOp.
     auto.
   Qed.
 
-  Lemma iter_op_spec : forall sc a bound, N.size_nat (scToN sc) <= bound ->
+  Lemma iter_op_correct : forall sc a bound, N.size_nat (scToN sc) <= bound ->
     iter_op bound sc a === nat_iter_op (N.to_nat (scToN sc)) a.
   Proof.
     intros.
@@ -192,5 +191,4 @@ Section IterAssocOp.
     rewrite Nshiftr_size by auto.
     reflexivity.
   Qed.
-
-End IterAssocOp.
+End IterAssocOp.
\ No newline at end of file