consolidate and rename Edwards curve lemmas

10 files changed, 408 insertions, 367 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 2fdaff4a5..f70479c3a 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -7,187 +7,294 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Tactics.VerdiTactics.
 
-Section CompleteEdwardsCurveTheorems.
-  Context {prm:TwistedEdwardsParams}.
-  Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *)
-  Existing Instance prime_q.
+Module E.
+  Section CompleteEdwardsCurveTheorems.
+    Context {prm:TwistedEdwardsParams}.
+    Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *)
+    Existing Instance prime_q.
+  
+    Add Field Ffield_p' : (@Ffield_theory q _)
+      (morphism (@Fring_morph q),
+       preprocess [Fpreprocess],
+       postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
+       constants [Fconstant],
+       div (@Fmorph_div_theory q),
+       power_tac (@Fpower_theory q) [Fexp_tac]).
+  
+    Add Field Ffield_notConstant : (OpaqueFieldTheory q)
+      (constants [notConstant]).
+  
+    Ltac clear_prm :=
+      generalize dependent a; intro a; intros;
+      generalize dependent d; intro d; intros;
+      generalize dependent prime_q; intro prime_q; intros;
+      generalize dependent q; intro q; intros;
+      clear prm.
+  
+    Lemma point_eq : forall xy1 xy2 pf1 pf2,
+      xy1 = xy2 -> exist E.onCurve xy1 pf1 = exist E.onCurve xy2 pf2.
+    Proof.
+      destruct xy1, xy2; intros; find_injection; intros; subst. apply f_equal.
+      apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *)
+    Qed. Hint Resolve point_eq.
+  
+    Definition point_eqb (p1 p2:E.point) : bool := andb
+        (F_eqb (fst (proj1_sig p1)) (fst (proj1_sig p2)))
+        (F_eqb (snd (proj1_sig p1)) (snd (proj1_sig p2))).
+  
+    Local Ltac t :=
+      unfold point_eqb;
+        repeat match goal with
+        | _ => progress intros
+        | _ => progress simpl in *
+        | _ => progress subst
+        | [P:E.point |- _ ] => destruct P
+        | [x: (F q * F q)%type |- _ ] => destruct x
+        | [H: _ /\ _ |- _ ] => destruct H
+        | [H: _ |- _ ] => rewrite Bool.andb_true_iff in H
+        | [H: _ |- _ ] => apply F_eqb_eq in H
+        | _ => rewrite F_eqb_refl
+        end; eauto.
+  
+    Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2.
+    Proof.
+      t.
+    Qed.
+  
+    Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true.
+    Proof.
+      t.
+    Qed.
+  
+    Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2.
+    Proof.
+      intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
+      apply point_eqb_complete in H0; congruence.
+    Qed.
+  
+    Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false.
+    Proof.
+      intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
+      apply point_eqb_sound in Hneq. congruence.
+    Qed.
+  
+    Lemma point_eqb_refl : forall p, point_eqb p p = true.
+    Proof.
+      t.
+    Qed.
+  
+    Definition point_eq_dec (p1 p2:E.point) : {p1 = p2} + {p1 <> p2}.
+      destruct (point_eqb p1 p2) eqn:H; match goal with
+                                        | [ H: _ |- _ ] => apply point_eqb_sound in H
+                                        | [ H: _ |- _ ] => apply point_eqb_neq in H
+                                        end; eauto.
+    Qed.
+  
+    Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false.
+    Proof.
+      intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete.
+    Qed.
+  
+    Ltac Edefn := unfold E.add, E.add', E.zero; intros;
+                    repeat match goal with
+                           | [ p : E.point |- _ ] =>
+                             let x := fresh "x" p in
+                             let y := fresh "y" p in
+                             let pf := fresh "pf" p in
+                             destruct p as [[x y] pf]; unfold E.onCurve in pf
+                    | _ => eapply point_eq, (f_equal2 pair)
+                    | _ => eapply point_eq
+    end.
+    Lemma add_comm : forall A B, (A+B = B+A)%E.
+    Proof.
+      Edefn; apply (f_equal2 div); ring.
+    Qed.
+  
+    Ltac unifiedAdd_nonzero := match goal with
+    | [ |- (?op 1 (d * _ * _ * _ * _ *
+      inv (1 - d * ?xA * ?xB * ?yA * ?yB) * inv (1 + d * ?xA * ?xB * ?yA * ?yB)))%F <> 0%F]
+      => let Hadd := fresh "Hadd" in
+       pose proof (@unifiedAdd'_onCurve _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d (xA, yA) (xB, yB)) as Hadd;
+       simpl in Hadd;
+       match goal with
+       | [H : (1 - d * ?xC * xB * ?yC * yB)%F <> 0%F |- (?op 1 ?other)%F <> 0%F] =>
+         replace other with
+          (d * xC * ((xA * yB + yA * xB) / (1 + d * xA * xB * yA * yB)) 
+          * yC * ((yA * yB - a * xA * xB) / (1 - d * xA * xB * yA * yB)))%F by (subst; unfold div; ring);
+          auto
+      end
+    end.
+  
+    Lemma add_assoc : forall A B C, (A+(B+C) = (A+B)+C)%E.
+    Proof.
+      Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz);
+        pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
+        pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
+        cbv beta iota in *;
+        repeat split; field_nonzero idtac; unifiedAdd_nonzero.
+    Qed.
+  
+    Lemma add_0_r : forall P, (P + E.zero = P)%E.
+    Proof.
+      Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
+             ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl.
+    Qed.
 
-  Add Field Ffield_p' : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]).
+    Lemma add_0_l : forall P, (E.zero + P)%E = P.
+    Proof.
+      intros; rewrite add_comm. apply add_0_r.
+    Qed.
 
-  Add Field Ffield_notConstant : (OpaqueFieldTheory q)
-    (constants [notConstant]).
+    Lemma mul_0_l : forall P, (0 * P = E.zero)%E.
+    Proof.
+      auto.
+    Qed.
 
-  Ltac clear_prm :=
-    generalize dependent a; intro a; intros;
-    generalize dependent d; intro d; intros;
-    generalize dependent prime_q; intro prime_q; intros;
-    generalize dependent q; intro q; intros;
-    clear prm.
+    Lemma mul_S_l : forall n P, (S n * P)%E = (P + n * P)%E.
+    Proof.
+      auto.
+    Qed.
 
-  Lemma point_eq' : forall xy1 xy2 pf1 pf2,
-    xy1 = xy2 -> exist onCurve xy1 pf1 = exist onCurve xy2 pf2.
-  Proof.
-    destruct xy1, xy2; intros; find_injection; intros; subst. apply f_equal.
-    apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *)
-  Qed.
+    Lemma mul_add_l : forall a b P, ((a + b)%nat * P)%E = E.add (a * P)%E (b * P)%E.
+    Proof.
+      induction a; intros; rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?mul_0_l, ?add_0_l, ?mul_S_, ?IHa, ?add_assoc; auto.
+    Qed.
 
-  Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2,
-    mkPoint p1 pf1 = mkPoint p2 pf2.
-  Proof.
-    eauto using point_eq'.
-  Qed.
-  Hint Resolve point_eq' point_eq.
+    Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E.
+    Proof.
+      induction n; intros; auto.
+      rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, add_comm. reflexivity.
+    Qed.
 
-  Definition point_eqb (p1 p2:point) : bool := andb
-      (F_eqb (fst (proj1_sig p1)) (fst (proj1_sig p2)))
-      (F_eqb (snd (proj1_sig p1)) (snd (proj1_sig p2))).
-
-  Local Ltac t :=
-    unfold point_eqb;
-      repeat match goal with
-      | _ => progress intros
-      | _ => progress simpl in *
-      | _ => progress subst
-      | [P:point |- _ ] => destruct P
-      | [x: (F q * F q)%type |- _ ] => destruct x
-      | [H: _ /\ _ |- _ ] => destruct H
-      | [H: _ |- _ ] => rewrite Bool.andb_true_iff in H
-      | [H: _ |- _ ] => apply F_eqb_eq in H
-      | _ => rewrite F_eqb_refl
-      end; eauto.
-
-  Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2.
-  Proof.
-    t.
-  Qed.
-
-  Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true.
-  Proof.
-    t.
-  Qed.
-
-  Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2.
-  Proof.
-    intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
-    apply point_eqb_complete in H0; congruence.
-  Qed.
-
-  Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false.
-  Proof.
-    intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition.
-    apply point_eqb_sound in Hneq. congruence.
-  Qed.
-
-  Lemma point_eqb_refl : forall p, point_eqb p p = true.
-  Proof.
-    t.
-  Qed.
-
-  Definition point_eq_dec (p1 p2:point) : {p1 = p2} + {p1 <> p2}.
-    destruct (point_eqb p1 p2) eqn:H; match goal with
-                                      | [ H: _ |- _ ] => apply point_eqb_sound in H
-                                      | [ H: _ |- _ ] => apply point_eqb_neq in H
-                                      end; eauto.
-  Qed.
-
-  Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false.
-  Proof.
-    intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete.
-  Qed.
-
-  Ltac Edefn := unfold unifiedAdd, unifiedAdd', zero; intros;
-                  repeat match goal with
-                         | [ p : point |- _ ] =>
-                           let x := fresh "x" p in
-                           let y := fresh "y" p in
-                           let pf := fresh "pf" p in
-                           destruct p as [[x y] pf]; unfold onCurve in pf
-                  | _ => eapply point_eq, (f_equal2 pair)
-                  | _ => eapply point_eq
-  end.
-  Lemma twistedAddComm : forall A B, (A+B = B+A)%E.
-  Proof.
-    Edefn; apply (f_equal2 div); ring.
-  Qed.
-
-  Ltac unifiedAdd_nonzero := match goal with
-  | [ |- (?op 1 (d * _ * _ * _ * _ *
-    inv (1 - d * ?xA * ?xB * ?yA * ?yB) * inv (1 + d * ?xA * ?xB * ?yA * ?yB)))%F <> 0%F]
-    => let Hadd := fresh "Hadd" in
-     pose proof (@unifiedAdd'_onCurve _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d (xA, yA) (xB, yB)) as Hadd;
-     simpl in Hadd;
-     match goal with
-     | [H : (1 - d * ?xC * xB * ?yC * yB)%F <> 0%F |- (?op 1 ?other)%F <> 0%F] =>
-       replace other with
-        (d * xC * ((xA * yB + yA * xB) / (1 + d * xA * xB * yA * yB)) 
-        * yC * ((yA * yB - a * xA * xB) / (1 - d * xA * xB * yA * yB)))%F by (subst; unfold div; ring);
-        auto
-    end
-  end.
-
-  Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E.
-  Proof.
-    (* The Ltac takes ~15s, the Qed no longer takes longer than I have had patience for *)
-    Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz);
-      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
-      pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
-      cbv beta iota in *;
-      repeat split; field_nonzero idtac; unifiedAdd_nonzero.
-  Qed.
-
-  Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
-  Proof.
-    Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
-           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl.
-  Qed.
-
-  (* solve for x ^ 2 *)
-  Definition solve_for_x2 (y : F q) := ((y ^ 2 - 1) / (d * (y ^ 2) - a))%F.
-
-  Lemma d_y2_a_nonzero : (forall y, 0 <> d * y ^ 2 - a)%F.
-    intros ? eq_zero.
-    pose proof prime_q.
-    destruct square_a as [sqrt_a sqrt_a_id].
-    rewrite <- sqrt_a_id in eq_zero.
-    destruct (Fq_square_mul_sub _ _ _ eq_zero) as [ [sqrt_d sqrt_d_id] | a_zero].
-    + pose proof (nonsquare_d sqrt_d); auto.
-    + subst.
-      rewrite Fq_pow_zero in sqrt_a_id by congruence.
-      auto using nonzero_a.
-  Qed.
-
-  Lemma a_d_y2_nonzero : (forall y, a - d * y ^ 2 <> 0)%F.
-  Proof.
-    intros y eq_zero.
-    pose proof prime_q.
-    eapply F_minus_swap in eq_zero.
-    eauto using (d_y2_a_nonzero y).
-  Qed.
-
-  Lemma solve_correct : forall x y, onCurve (x, y) <->
-    (x ^ 2 = solve_for_x2 y)%F.
-  Proof.
-    split.
-    + intro onCurve_x_y.
+    Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
+    Proof.
+      induction m; rewrite ?mul_S_l, ?add_0_l; auto.
+    Qed.
+  
+    (* solve for x ^ 2 *)
+    Definition solve_for_x2 (y : F q) := ((y ^ 2 - 1) / (d * (y ^ 2) - a))%F.
+  
+    Lemma d_y2_a_nonzero : (forall y, 0 <> d * y ^ 2 - a)%F.
+      intros ? eq_zero.
       pose proof prime_q.
-      unfold onCurve in onCurve_x_y.
-      eapply F_div_mul; auto using (d_y2_a_nonzero y).
-      replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring.
-      rewrite F_sub_add_swap.
-      replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring.
-      rewrite onCurve_x_y.
-      ring.
-    + intro x2_eq.
-      unfold onCurve, solve_for_x2 in *.
-      rewrite x2_eq.
-      field.
-      auto using d_y2_a_nonzero.
-  Qed.
-
-End CompleteEdwardsCurveTheorems.
+      destruct square_a as [sqrt_a sqrt_a_id].
+      rewrite <- sqrt_a_id in eq_zero.
+      destruct (Fq_square_mul_sub _ _ _ eq_zero) as [ [sqrt_d sqrt_d_id] | a_zero].
+      + pose proof (nonsquare_d sqrt_d); auto.
+      + subst.
+        rewrite Fq_pow_zero in sqrt_a_id by congruence.
+        auto using nonzero_a.
+    Qed.
+  
+    Lemma a_d_y2_nonzero : (forall y, a - d * y ^ 2 <> 0)%F.
+    Proof.
+      intros y eq_zero.
+      pose proof prime_q.
+      eapply F_minus_swap in eq_zero.
+      eauto using (d_y2_a_nonzero y).
+    Qed.
+  
+    Lemma solve_correct : forall x y, E.onCurve (x, y) <->
+      (x ^ 2 = solve_for_x2 y)%F.
+    Proof.
+      split.
+      + intro onCurve_x_y.
+        pose proof prime_q.
+        unfold E.onCurve in onCurve_x_y.
+        eapply F_div_mul; auto using (d_y2_a_nonzero y).
+        replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring.
+        rewrite F_sub_add_swap.
+        replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring.
+        rewrite onCurve_x_y.
+        ring.
+      + intro x2_eq.
+        unfold E.onCurve, solve_for_x2 in *.
+        rewrite x2_eq.
+        field.
+        auto using d_y2_a_nonzero.
+    Qed.
+  
+  
+    Program Definition opp (P:E.point) : E.point := let '(x, y) := proj1_sig P in (opp x, y).
+    Next Obligation. Proof.
+      pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H.
+      rewrite F_square_opp; trivial.
+    Qed.
+    
+    Definition sub P Q := (P + opp Q)%E.
+    
+    Lemma opp_zero : opp E.zero = E.zero.
+    Proof.
+      pose proof @F_opp_0.
+      unfold opp, E.zero; eapply point_eq; congruence.
+    Qed.
+  
+    Lemma add_opp_r : forall P, (P + opp P = E.zero)%E.
+    Proof.
+      unfold opp; Edefn; rewrite ?@F_pow_2_r in *; (F_field_simplify_eq; [clear_prm; F_nsatz|..]);
+        rewrite <-?@F_pow_2_r in *;
+        pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP);
+        pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP);
+        field_nonzero idtac.
+    Qed.
+  
+    Lemma add_opp_l : forall P, (opp P + P = E.zero)%E.
+    Proof.
+      intros. rewrite add_comm. eapply add_opp_r.
+    Qed.
+  
+    Lemma add_cancel_r : forall A B C, (B+A = C+A -> B = C)%E.
+    Proof.
+      intros.
+      assert ((B + A) + opp A = (C + A) + opp A)%E as Hc by congruence.
+      rewrite <-!add_assoc, !add_opp_r, !add_0_r in Hc; exact Hc.
+    Qed.
+  
+    Lemma add_cancel_l : forall A B C, (A+B = A+C -> B = C)%E.
+    Proof.
+      intros.
+      rewrite (add_comm A C) in H.
+      rewrite (add_comm A B) in H.
+      eauto using add_cancel_r.
+    Qed.
+    
+    Lemma shuffle_eq_add_opp : forall P Q R, (P + Q = R <-> Q = opp P + R)%E.
+    Proof.
+      split; intros.
+      { assert (opp P + (P + Q) = opp P + R)%E as Hc by congruence.
+        rewrite add_assoc, add_opp_l, add_comm, add_0_r in Hc; exact Hc. }
+      { subst. rewrite add_assoc, add_opp_r, add_comm, add_0_r; reflexivity. }
+    Qed.
+        
+    Lemma opp_opp : forall P, opp (opp P) = P.
+    Proof.
+      intros.
+      pose proof (add_opp_r P%E) as H.
+      rewrite add_comm in H.
+      rewrite shuffle_eq_add_opp in H.
+      rewrite add_0_r in H.
+      congruence.
+    Qed.
+    
+    Lemma opp_add : forall P Q, opp (P + Q)%E = (opp P + opp Q)%E.
+    Proof.
+      intros.
+      pose proof (add_opp_r (P+Q)%E) as H.
+      rewrite <-!add_assoc in H.
+      rewrite add_comm in H.
+      rewrite <-!add_assoc in H.
+      rewrite shuffle_eq_add_opp in H.
+      rewrite add_comm in H.
+      rewrite shuffle_eq_add_opp in H.
+      rewrite add_0_r in H.
+      assumption.
+    Qed.
+      
+    Lemma opp_mul : forall n P, opp (E.mul n P) = E.mul n (opp P).
+    Proof.
+      pose proof opp_add; pose proof opp_zero.
+      induction n; simpl; intros; congruence.
+    Qed.
+  End CompleteEdwardsCurveTheorems.
+End E.
+Infix "-" := E.sub : E_scope.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v
index d58a06c55..50027349d 100644
--- a/src/CompleteEdwardsCurve/DoubleAndAdd.v
+++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v
@@ -5,26 +5,26 @@ Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.
 
 Section EdwardsDoubleAndAdd.
   Context {prm:TwistedEdwardsParams}.
-  Definition doubleAndAdd (bound n : nat) (P : point) : point :=
-    iter_op unifiedAdd zero N.testbit_nat (N.of_nat n) P bound.
+  Definition doubleAndAdd (bound n : nat) (P : E.point) : E.point :=
+    iter_op E.add E.zero N.testbit_nat (N.of_nat n) P bound.
 
-  Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P)%E.
+  Lemma scalarMult_double : forall n P, E.mul (n + n) P = E.mul n (P + P)%E.
   Proof.
     intros.
     replace (n + n)%nat with (n * 2)%nat by omega.
     induction n; simpl; auto.
-    rewrite twistedAddAssoc.
+    rewrite E.add_assoc.
     f_equal; auto.
   Qed.
 
   Lemma doubleAndAdd_spec : forall bound n P, N.size_nat (N.of_nat n) <= bound ->
-    scalarMult n P = doubleAndAdd bound n P.
+    E.mul n P = doubleAndAdd bound n P.
   Proof.
     induction n; auto; intros; unfold doubleAndAdd;
       rewrite iter_op_spec with (scToN := fun x => x); (
         unfold Morphisms.Proper, Morphisms.respectful, Equivalence.equiv;
         intros; subst; try rewrite Nat2N.id;
-        reflexivity || assumption || apply twistedAddAssoc
-        || rewrite twistedAddComm; apply zeroIsIdentity).
+        reflexivity || assumption || apply E.add_assoc
+        || rewrite E.add_comm; apply E.add_0_r).
   Qed.
 End EdwardsDoubleAndAdd.
\ No newline at end of file
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index a9fbf5e40..5e4fe0b0b 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -45,7 +45,7 @@ Section ExtendedCoordinates.
   Local Notation "P '~=' rP" := (rep P rP) (at level 70).
 
   Ltac unfoldExtended :=
-    repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros);
+    repeat progress (autounfold; unfold E.onCurve, E.add, E.add', rep in *; intros);
     repeat match goal with
       | [ p : (F q*F q)%type |- _ ] =>
           let x := fresh "x" p in
@@ -83,14 +83,14 @@ Section ExtendedCoordinates.
     solveExtended.
   Qed.
 
-  Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ onCurve (extendedToTwisted P) }.
+  Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P) }.
 
-  Program Definition mkExtendedPoint : point -> extendedPoint := twistedToExtended.
+  Program Definition mkExtendedPoint : E.point -> extendedPoint := twistedToExtended.
   Next Obligation.
     destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep.
   Qed.
 
-  Program Definition unExtendedPoint : extendedPoint -> point := extendedToTwisted.
+  Program Definition unExtendedPoint : extendedPoint -> E.point := extendedToTwisted.
   Next Obligation.
     destruct x; simpl; intuition.
   Qed.
@@ -103,7 +103,7 @@ Section ExtendedCoordinates.
 
   Lemma unExtendedPoint_mkExtendedPoint : forall P, unExtendedPoint (mkExtendedPoint P) = P.
   Proof.
-    destruct P; eapply point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep.
+    destruct P; eapply E.point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep.
   Qed.
 
   Global Instance Proper_mkExtendedPoint : Proper (eq==>equiv) mkExtendedPoint.
@@ -135,12 +135,12 @@ Section ExtendedCoordinates.
       let T3 := E*H in
       let Z3 := F*G in
       (X3, Y3, Z3, T3).
-    Local Hint Unfold unifiedAdd.
+    Local Hint Unfold E.add.
 
     Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q).
 
-    Lemma unifiedAddM1'_rep: forall P Q rP rQ, onCurve rP -> onCurve rQ ->
-      P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (unifiedAdd' rP rQ).
+    Lemma unifiedAddM1'_rep: forall P Q rP rQ, E.onCurve rP -> E.onCurve rQ ->
+      P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (E.add' rP rQ).
     Proof.
       intros P Q rP rQ HoP HoQ HrP HrQ.
       pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d).
@@ -152,9 +152,9 @@ Section ExtendedCoordinates.
         field_nonzero tnz.
     Qed.
 
-    Lemma unifiedAdd'_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (unifiedAdd' P Q).
+    Lemma unifiedAdd'_onCurve : forall P Q, E.onCurve P -> E.onCurve Q -> E.onCurve (E.add' P Q).
     Proof.
-      intros; pose proof (proj2_sig (unifiedAdd (mkPoint _ H) (mkPoint _ H0))); eauto.
+      intros; pose proof (proj2_sig (E.add (exist _ _ H) (exist _ _ H0))); eauto.
     Qed.
 
     Program Definition unifiedAddM1 : extendedPoint -> extendedPoint -> extendedPoint := unifiedAddM1'.
@@ -167,9 +167,9 @@ Section ExtendedCoordinates.
         eauto using unifiedAdd'_onCurve.
     Qed.
 
-    Lemma unifiedAddM1_rep : forall P Q, unifiedAdd (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q).
+    Lemma unifiedAddM1_rep : forall P Q, E.add (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q).
     Proof.
-      destruct P, Q; unfold unExtendedPoint, unifiedAdd, unifiedAddM1; eapply point_eq; simpl in *; intuition.
+      destruct P, Q; unfold unExtendedPoint, E.add, unifiedAddM1; eapply E.point_eq; simpl in *; intuition.
       pose proof (unifiedAddM1'_rep x x0 (extendedToTwisted x) (extendedToTwisted x0));
         destruct (unifiedAddM1' x x0);
         unfold rep in *; intuition.
@@ -180,23 +180,23 @@ Section ExtendedCoordinates.
       repeat (econstructor || intro).
       repeat match goal with [H: _ === _ |- _ ] => inversion H; clear H end; unfold equiv, extendedPoint_eq.
       rewrite <-!unifiedAddM1_rep.
-      destruct x, y, x0, y0; simpl in *; eapply point_eq; congruence.
+      destruct x, y, x0, y0; simpl in *; eapply E.point_eq; congruence.
     Qed.
 
-    Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint zero) === P.
+    Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P.
       unfold equiv, extendedPoint_eq; intros.
-      rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto.
+      rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto.
     Qed.
 
-    Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint zero) P === P.
+    Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint E.zero) P === P.
       unfold equiv, extendedPoint_eq; intros.
-      rewrite <-!unifiedAddM1_rep, twistedAddComm, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto.
+      rewrite <-!unifiedAddM1_rep, E.add_comm, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto.
     Qed.
 
     Lemma unifiedAddM1_assoc : forall a b c, unifiedAddM1 a (unifiedAddM1 b c) === unifiedAddM1 (unifiedAddM1 a b) c.
     Proof.
       unfold equiv, extendedPoint_eq; intros.
-      rewrite <-!unifiedAddM1_rep, twistedAddAssoc; auto.
+      rewrite <-!unifiedAddM1_rep, E.add_assoc; auto.
     Qed.
 
     Lemma testbit_conversion_identity : forall x i, N.testbit_nat x i = N.testbit_nat ((fun a => a) x) i.
@@ -204,14 +204,14 @@ Section ExtendedCoordinates.
       trivial.
     Qed.
 
-    Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint zero) N.testbit_nat.
+    Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint E.zero) N.testbit_nat.
     Definition scalarMultM1_spec :=
-      iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint zero) unifiedAddM1_0_l
+      iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint E.zero) unifiedAddM1_0_l
         N.testbit_nat (fun x => x) testbit_conversion_identity.
-    Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P (N.size_nat (N.of_nat n))) = scalarMult n (unExtendedPoint P).
+    Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P (N.size_nat (N.of_nat n))) = E.mul n (unExtendedPoint P).
       intros; rewrite scalarMultM1_spec, Nat2N.id; auto.
       induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|].
-      unfold scalarMult; fold scalarMult.
+      unfold E.mul; fold E.mul.
       rewrite <-IHn, unifiedAddM1_rep; auto.
     Qed.
 
diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v
index 83467bf6d..dba71b49c 100644
--- a/src/EdDSAProofs.v
+++ b/src/EdDSAProofs.v
@@ -37,7 +37,7 @@ Section EdDSAProofs.
   Lemma decode_sign_split2 : forall sk {n} (M : word n),
     split2 b b (sign (public sk) sk M) =
     let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
-    let R : point := (r * B)%E in (* commitment to nonce *)
+    let R : E.point := (r * B)%E in (* commitment to nonce *)
     let s : nat := curveKey sk in (* secret scalar *)
     let S : F (Z.of_nat l) := ZToField (Z.of_nat (r + H (enc R ++ public sk ++ M) * s)) in
         enc S.
@@ -46,62 +46,21 @@ Section EdDSAProofs.
   Qed.
   Hint Rewrite decode_sign_split2.
 
-  Lemma zero_times : forall P, (0 * P = zero)%E.
-  Proof.
-    auto.
-  Qed.
-
-  Lemma zero_plus : forall P, (zero + P = P)%E.
-  Proof.
-    intros; rewrite twistedAddComm; apply zeroIsIdentity.
-  Qed.
-
-  Lemma times_S : forall n m, S n * m = m + n * m.
-  Proof.
-    auto.
-  Qed.
-
-  Lemma times_S_nat : forall n m, (S n * m = m + n * m)%nat.
-  Proof.
-    auto.
-  Qed.
-
-  Hint Rewrite plus_O_n plus_Sn_m times_S times_S_nat.
-  Hint Rewrite zeroIsIdentity zero_times zero_plus twistedAddAssoc.
-
-  Lemma scalarMult_distr : forall n0 m, ((n0 + m)%nat * B)%E = unifiedAdd (n0 * B)%E (m * B)%E.
-  Proof.
-    unfold scalarMult; induction n0; arith. 
-  Qed.
-  Hint Rewrite scalarMult_distr.
-
-  Lemma scalarMult_assoc : forall (n0 m : nat), (n0 * (m * B) = (n0 * m)%nat * B)%E.
-  Proof.
-    induction n0; arith; simpl; arith.
-  Qed.
-  Hint Rewrite scalarMult_assoc.
-
-  Lemma scalarMult_zero : forall m, (m * zero = zero)%E.
-  Proof.
-    unfold scalarMult; induction m; arith.
-  Qed.
-  Hint Rewrite scalarMult_zero.
+  Hint Rewrite E.add_0_r E.add_0_l E.add_assoc.
+  Hint Rewrite E.mul_assoc E.mul_add_l E.mul_0_l E.mul_zero_r.
+  Hint Rewrite plus_O_n plus_Sn_m mult_0_l mult_succ_l.
   Hint Rewrite l_order_B.
-
-  Lemma l_order_B' : forall x, (l * x * B = zero)%E.
+  Lemma l_order_B' : forall x, (l * x * B = E.zero)%E.
   Proof.
-    intros; rewrite Mult.mult_comm. rewrite <- scalarMult_assoc. arith.
-  Qed.
-
-  Hint Rewrite l_order_B'.
+    intros; rewrite Mult.mult_comm. rewrite <- E.mul_assoc. arith.
+  Qed. Hint Rewrite l_order_B'.
 
   Lemma scalarMult_mod_l : forall n0, (n0 mod l * B = n0 * B)%E.
   Proof.
     intros.
     rewrite (div_mod n0 l) at 2 by (generalize l_odd; omega).
     arith.
-  Qed.
-  Hint Rewrite scalarMult_mod_l.
+  Qed. Hint Rewrite scalarMult_mod_l.
 
   Hint Rewrite @encoding_valid.
   Hint Rewrite @FieldToZ_ZToField.
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index 9eb5118bd..b7e907e10 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -27,12 +27,12 @@ Section PointEncoding.
 
   Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F.
 
-  Lemma solve_sqrt_valid : forall p, onCurve p ->
-    sqrt_valid (solve_for_x2 (snd p)).
+  Lemma solve_sqrt_valid : forall p, E.onCurve p ->
+    sqrt_valid (E.solve_for_x2 (snd p)).
   Proof.
     intros ? onCurve_xy.
     destruct p as [x y]; simpl.
-    rewrite (solve_correct x y) in onCurve_xy.
+    rewrite (E.solve_correct x y) in onCurve_xy.
     rewrite <- onCurve_xy.
     unfold sqrt_valid.
     eapply sqrt_mod_q_valid; eauto.
@@ -40,20 +40,20 @@ Section PointEncoding.
     Grab Existential Variables. eauto.
   Qed.
 
-  Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) ->
-    onCurve (sqrt_mod_q (solve_for_x2 y), y).
+  Lemma solve_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) ->
+    E.onCurve (sqrt_mod_q (E.solve_for_x2 y), y).
   Proof.
     intros.
     unfold sqrt_valid in *.
-    apply solve_correct; auto.
+    apply E.solve_correct; auto.
   Qed.
 
-  Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) ->
-    onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y).
+  Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (E.solve_for_x2 y) ->
+    E.onCurve (opp (sqrt_mod_q (E.solve_for_x2 y)), y).
   Proof.
     intros y sqrt_valid_x2.
     unfold sqrt_valid in *.
-    apply solve_correct.
+    apply E.solve_correct.
     rewrite <- sqrt_valid_x2 at 2.
     ring.
   Qed.
@@ -67,13 +67,13 @@ Section PointEncoding.
   Definition point_enc_coordinates (p : (F q * F q)) : Word.word (S sz) := let '(x,y) := p in
     Word.WS (sign_bit x) (enc y).
 
-  Let point_enc (p : CompleteEdwardsCurve.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in
+  Let point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in
     Word.WS (sign_bit x) (enc y).
 
   Definition point_dec_coordinates (sign_bit : F q -> bool) (w : Word.word (S sz)) : option (F q * F q) :=
     match dec (Word.wtl w) with
     | None => None
-    | Some y => let x2 := solve_for_x2 y in
+    | Some y => let x2 := E.solve_for_x2 y in
         let x := sqrt_mod_q x2 in
         if F_eq_dec (x ^ 2) x2
         then
@@ -86,7 +86,7 @@ Section PointEncoding.
 
   Ltac inversion_Some_eq := match goal with [H: Some ?x = Some ?y |- _] => inversion H; subst end.
 
-  Lemma point_dec_coordinates_onCurve : forall w p, point_dec_coordinates sign_bit w = Some p -> onCurve p.
+  Lemma point_dec_coordinates_onCurve : forall w p, point_dec_coordinates sign_bit w = Some p -> E.onCurve p.
   Proof.
     unfold point_dec_coordinates; intros.
     edestruct dec; [ | congruence].
@@ -108,13 +108,13 @@ Section PointEncoding.
   Admitted.
 
 
-  Definition point_dec' w p : option point :=
+  Definition point_dec' w p : option E.point :=
     match (option_eq_dec (point_dec_coordinates sign_bit w) (Some p)) with
-      | left EQ => Some (mkPoint p (point_dec_coordinates_onCurve w p EQ))
+      | left EQ => Some (exist _ p (point_dec_coordinates_onCurve w p EQ))
       | right _ => None (* this case is never reached *)
     end.
 
-  Definition point_dec (w : word (S sz)) : option point :=
+  Definition point_dec (w : word (S sz)) : option E.point :=
     match (point_dec_coordinates sign_bit w) with
     | Some p => point_dec' w p
     | None => None
@@ -192,7 +192,7 @@ Section PointEncoding.
     rewrite (shatter_word w).
     f_equal; rewrite dec_Some in *;
       do 2 (break_if; try congruence); inversion coord_dec_Some; subst.
-    + destruct (F_eq_dec (sqrt_mod_q (solve_for_x2 f1)) 0%F) as [sqrt_0 | ?].
+    + destruct (F_eq_dec (sqrt_mod_q (E.solve_for_x2 f1)) 0%F) as [sqrt_0 | ?].
       - rewrite sqrt_0 in *.
         apply sqrt_mod_q_0 in sqrt_0.
         rewrite sqrt_0 in *.
@@ -268,12 +268,12 @@ Proof.
   congruence.
 Qed.
 
-Lemma sign_bit_match : forall x x' y : F q, onCurve (x, y) -> onCurve (x', y) ->
+Lemma sign_bit_match : forall x x' y : F q, E.onCurve (x, y) -> E.onCurve (x', y) ->
   sign_bit x = sign_bit x' -> x = x'.
 Proof.
   intros ? ? ? onCurve_x onCurve_x' sign_match.
-  apply solve_correct in onCurve_x.
-  apply solve_correct in onCurve_x'.
+  apply E.solve_correct in onCurve_x.
+  apply E.solve_correct in onCurve_x'.
   destruct (F_eq_dec x' 0).
   + subst.
     rewrite Fq_pow_zero in onCurve_x' by congruence.
@@ -287,7 +287,7 @@ Qed.
 Lemma blah : forall x y, (F_eqb (sqrt_mod_q (solve_for_x2 y)) 0 && sign_bit x)%bool = true.
 *)
 
-Lemma point_encoding_coordinates_valid : forall p, onCurve p ->
+Lemma point_encoding_coordinates_valid : forall p, E.onCurve p ->
    point_dec_coordinates sign_bit (point_enc_coordinates p) = Some p.
 Proof.
   intros p onCurve_p.
@@ -297,9 +297,9 @@ Proof.
   unfold sqrt_valid in *.
   destruct p as [x y].
   simpl in *.
-  destruct (F_eq_dec ((sqrt_mod_q (solve_for_x2 y)) ^ 2) (solve_for_x2 y)); intuition.
+  destruct (F_eq_dec ((sqrt_mod_q (E.solve_for_x2 y)) ^ 2) (E.solve_for_x2 y)); intuition.
   break_if; f_equal.
-  + case_eq (F_eqb (sqrt_mod_q (solve_for_x2 y)) 0); intros eqb_0.
+  + case_eq (F_eqb (sqrt_mod_q (E.solve_for_x2 y)) 0); intros eqb_0.
 (*
     SearchAbout F_eqb.
 
@@ -333,7 +333,7 @@ Proof.
   break_match.
   + f_equal.
     destruct p.
-    apply point_eq.
+    apply E.point_eq.
     reflexivity.
   + rewrite point_encoding_coordinates_valid in n by apply (proj2_sig p).
     congruence.
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 8dbfdf7b9..3348be1d9 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -16,38 +16,39 @@ Class TwistedEdwardsParams := {
   nonsquare_d : forall x, x^2 <> d
 }.
 
-Section TwistedEdwardsCurves.
-  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>
-  * <https://eprint.iacr.org/2015/677.pdf>
-  *)
-  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:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf.
-
-  Definition zero : point := mkPoint (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q).
+Module E.
+  Section TwistedEdwardsCurves.
+    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>
+    * <https://eprint.iacr.org/2015/677.pdf>
+    *)
+    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 zero : point := exist _ (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q).
+    
+    Definition add' P1' P2' :=
+      let '(x1, y1) := P1' in
+      let '(x2, y2) := P2' in
+        (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
+  
+    Definition add (P1 P2 : point) : point :=
+      let 'exist P1' pf1 := P1 in
+      let 'exist P2' pf2 := P2 in
+      exist _ (add' P1' P2')
+        (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2).
+  
+    Fixpoint mul (n:nat) (P : point) : point :=
+      match n with
+      | O => zero
+      | S n' => add P (mul n' P)
+      end.
+  End TwistedEdwardsCurves.
+End E.
   
-  Definition unifiedAdd' P1' P2' :=
-    let '(x1, y1) := P1' in
-    let '(x2, y2) := P2' in
-      (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
-
-  Definition unifiedAdd (P1 P2 : point) : point :=
-    let 'exist P1' pf1 := P1 in
-    let 'exist P2' pf2 := P2 in
-    mkPoint (unifiedAdd' P1' P2')
-      (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2).
-
-  Fixpoint scalarMult (n:nat) (P : point) : point :=
-    match n with
-    | O => zero
-    | S n' => unifiedAdd P (scalarMult n' P)
-    end.
-End TwistedEdwardsCurves.
-
 Delimit Scope E_scope with E.
-Infix "+" := unifiedAdd : E_scope.
-Infix "*" := scalarMult : E_scope.
\ No newline at end of file
+Infix "+" := E.add : E_scope.
+Infix "*" := E.mul : E_scope.
\ No newline at end of file
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 30892c006..6543823cb 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -145,9 +145,9 @@ Qed.
 Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding.
 
 Definition H : forall n : nat, word n -> word (b + b). Admitted.
-Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
-Definition B_nonzero : B <> zero. Admitted.
-Definition l_order_B : scalarMult l B = zero. Admitted.
+Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
+Definition B_nonzero : B <> E.zero. Admitted.
+Definition l_order_B : (l * B)%E = E.zero. Admitted.
 
 Local Instance ed25519params : EdDSAParams := {
   E := curve25519params;
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 8a48f4dea..80aed4a20 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -22,7 +22,7 @@ Section EdDSAParams.
     b : nat; (* public keys are k bits, signatures are 2*k bits *)
     b_valid : 2^(b - 1) > BinInt.Z.to_nat q;
     FqEncoding : encoding of F q as Word.word (b-1);
-    PointEncoding : encoding of point as Word.word b;
+    PointEncoding : encoding of E.point as Word.word b;
 
     H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *)
 
@@ -33,13 +33,13 @@ Section EdDSAParams.
     n_ge_c : n >= c;
     n_le_b : n <= b;
 
-    B : point;
-    B_not_identity : B <> zero;
+    B : E.point;
+    B_not_identity : B <> E.zero;
 
     l : nat; (* order of the subgroup of E generated by B *)
     l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
     l_odd : l > 2;
-    l_order_B : (l*B)%E = zero;
+    l_order_B : (l*B)%E = E.zero;
     FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b
   }.
 End EdDSAParams.
@@ -55,8 +55,7 @@ Section EdDSA.
   Notation secretkey := (Word.word b) (only parsing).
   Notation publickey := (Word.word b) (only parsing).
   Notation signature := (Word.word (b + b)) (only parsing).
-  Let point_eq_dec : forall P Q, {P = Q} + {P <> Q} := CompleteEdwardsCurveTheorems.point_eq_dec.
-  Local Infix "==" := point_eq_dec (at level 70) : E_scope .
+  Local Infix "==" := CompleteEdwardsCurveTheorems.E.point_eq_dec (at level 70) : E_scope .
 
   (* TODO: proofread curveKey and definition of n *)
   Definition curveKey (sk:secretkey) : nat :=
@@ -68,7 +67,7 @@ Section EdDSA.
 
   Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
     let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
-    let R : point := (r * B)%E in (* commitment to nonce *)
+    let R : E.point := (r * B)%E in (* commitment to nonce *)
     let s : nat := curveKey sk in (* secret scalar *)
     let S : F (BinInt.Z.of_nat l) := ZToField (BinInt.Z.of_nat
                               (r + H (enc R ++ public sk ++ M) * s)) in
@@ -78,8 +77,8 @@ Section EdDSA.
     let R_ := Word.split1 b b sig in
     let S_ := Word.split2 b b sig in
     match dec S_ : option (F (BinInt.Z.of_nat l)) with None => false | Some S' =>
-    match dec A_ : option point with None => false | Some A =>
-    match dec R_ : option point with None => false | Some R =>
+    match dec A_ : option E.point with None => false | Some A =>
+    match dec R_ : option E.point with None => false | Some R =>
     if BinInt.Z.to_nat (FieldToZ S') * B == R + (H (R_ ++ A_ ++ M)) * A
     then true else false
     end
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index 38b4b4224..1d79a018d 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -23,20 +23,19 @@ Section PointEncoding.
       | Word.WS b _ w' => b
     end.
 
-  Definition point_enc (p : CompleteEdwardsCurve.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in
+  Definition point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in
     Word.WS (sign_bit x) (enc y).
 
   Program Definition point_dec_with_spec :
-    {point_dec : Word.word (S sz) -> option CompleteEdwardsCurve.point
+    {point_dec : Word.word (S sz) -> option E.point
                | forall w x, point_dec w = Some x -> (point_enc x = w)
                } := PointEncodingPre.point_dec.
    
   Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec).
 
-  Instance point_encoding : encoding of CompleteEdwardsCurve.point as (Word.word (S sz)) := {
+  Instance point_encoding : encoding of E.point as (Word.word (S sz)) := {
     enc := point_enc;
     dec := point_dec;
     encoding_valid := PointEncodingPre.point_encoding_valid
   }.
-
-End PointEncoding.
+End PointEncoding.
\ No newline at end of file
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index f02c24ffb..f8fb5aad7 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -87,33 +87,9 @@ Axiom decode_scalar : word b -> option N.
 Local Existing Instance Ed25519.FlEncoding.
 Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat Ed25519.l) => Z.to_N x) (dec x).
 
-Local Infix "==?" := point_eqb (at level 70) : E_scope.
+Local Infix "==?" := E.point_eqb (at level 70) : E_scope.
 Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope.
 
-Program Definition negate (P:point) : point := let '(x, y) := proj1_sig P in (opp x, y).
-Next Obligation.
-Proof.
-  pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H.
-  rewrite F_square_opp; trivial.
-Qed.
-
-Definition point_sub P Q := (P + negate Q)%E.
-Infix "-" := point_sub : E_scope.
-
-Lemma negate_zero : negate zero = zero.
-Proof.
-  pose proof @F_opp_0.
-  unfold negate, zero; eapply point_eq'; congruence.
-Qed.
-
-Lemma negate_add : forall P Q, negate (P + Q)%E = (negate P + negate Q)%E. Admitted.
-  
-Lemma negate_scalarMult : forall n P, negate (scalarMult n P) = scalarMult n (negate P).
-Proof.
-  pose proof negate_add; pose proof negate_zero.
-  induction n; simpl; intros; congruence.
-Qed.
-
 Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E.
 
 Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T).
@@ -127,13 +103,13 @@ Proof.
   repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; trivial.
 Admitted.
 
-Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P).
+Axiom negateExtended_correct : forall P, E.opp (unExtendedPoint P) = unExtendedPoint (negateExtended P).
 
 Local Existing Instance PointEncoding.
-Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E.
+Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:E.point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E.
 
-Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option point => bool)
- (fun S : point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X).
+Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option E.point => bool)
+ (fun S : E.point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X).
 Proof.
   intros.
   destruct (dec S_) eqn:H.
@@ -146,13 +122,13 @@ Qed.
 Definition enc' : F q * F q -> word (S (b - 1)).
 Proof.
   intro x.
-  let enc' := (eval hnf in (@enc (@point curve25519params) _ _)) in
+  let enc' := (eval hnf in (@enc (@E.point curve25519params) _ _)) in
   match (eval cbv [proj1_sig] in (fun pf => enc' (exist _ x pf))) with
   | (fun _ => ?enc') => exact enc'
   end.
 Defined.
 
-Definition enc'_correct : @enc (@point curve25519params) _ _ = (fun x => enc' (proj1_sig x))
+Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc' (proj1_sig x))
   := eq_refl.
 
     Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
@@ -276,13 +252,13 @@ Proof.
                [ reflexivity | .. ]
            end.
     set_evars.
-    rewrite<- point_eqb_correct.
-    rewrite solve_for_R; unfold point_sub.
-    rewrite negate_scalarMult.
+    rewrite<- E.point_eqb_correct.
+    rewrite solve_for_R; unfold E.sub.
+    rewrite E.opp_mul.
     let p1 := constr:(scalarMultM1_rep eq_refl) in
     let p2 := constr:(unifiedAddM1_rep eq_refl) in
     repeat match goal with
-           | |- context [(_ * negate ?P)%E] =>
+           | |- context [(_ * E.opp ?P)%E] =>
               rewrite <-(unExtendedPoint_mkExtendedPoint P);
               rewrite negateExtended_correct;
               rewrite <-p1
@@ -336,7 +312,7 @@ Proof.
     reflexivity. }
   Unfocus.
 
-  cbv [mkExtendedPoint zero mkPoint].
+  cbv [mkExtendedPoint E.zero].
   unfold proj1_sig at 1 2 3 5 6 7 8.
   rewrite B_proj.
 
@@ -369,7 +345,7 @@ Proof.
     reflexivity. }
   Unfocus.
 
-  cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding CompleteEdwardsCurveTheorems.solve_for_x2 sqrt_mod_q].
+  cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q].
 
   etransitivity.
   Focus 2. {
@@ -484,8 +460,8 @@ Proof.
       unfold curve25519params, q. (* TODO: do we really wanna do it here? *)
       rewrite (rep2F_F2rep 0%F).
       rewrite (rep2F_F2rep 1%F).
-      match goal with |- context [?x] => match x with (fst (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end.
-      match goal with |- context [?x] => match x with (snd (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end.
+      match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite (rep2F_F2rep x) end end.
+      match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite (rep2F_F2rep x) end end.
       rewrite !FRepMul_correct.
       repeat match goal with |- appcontext [ ?E ] =>
                       match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) =>