Cleaned up and revised DoubleAndAdd.

1 files changed, 10 insertions, 19 deletions

diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v
index d04cefc3d..d58a06c55 100644
--- a/src/CompleteEdwardsCurve/DoubleAndAdd.v
+++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v
@@ -5,8 +5,8 @@ Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.
 
 Section EdwardsDoubleAndAdd.
   Context {prm:TwistedEdwardsParams}.
-  Definition doubleAndAdd (n : nat) (P : point) : point :=
-    iter_op unifiedAdd zero N.testbit_nat (N.of_nat n) P (N.size_nat (N.of_nat n)).
+  Definition doubleAndAdd (bound n : nat) (P : point) : point :=
+    iter_op unifiedAdd 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.
   Proof.
@@ -17,23 +17,14 @@ Section EdwardsDoubleAndAdd.
     f_equal; auto.
   Qed.
 
-  Lemma iter_op_double : forall p P,
-    Pos.iter_op unifiedAdd (p + p) P = Pos.iter_op unifiedAdd p (P + P)%E.
+  Lemma doubleAndAdd_spec : forall bound n P, N.size_nat (N.of_nat n) <= bound ->
+    scalarMult n P = doubleAndAdd bound n P.
   Proof.
-    intros.
-    rewrite Pos.add_diag.
-    unfold Pos.iter_op; simpl.
-    auto.
-  Qed.
-
-
-  Lemma doubleAndAdd_spec : forall n P, scalarMult n P = doubleAndAdd 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 || apply twistedAddAssoc || rewrite twistedAddComm; apply zeroIsIdentity).
+    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).
   Qed.
 End EdwardsDoubleAndAdd.
\ No newline at end of file