Removed old iter_op version and its last dependency.

1 files changed, 10 insertions, 42 deletions

diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v
index 84c1289f6..d04cefc3d 100644
--- a/src/CompleteEdwardsCurve/DoubleAndAdd.v
+++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v
@@ -1,15 +1,12 @@
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.BoundedIterOp.
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Util.IterAssocOp.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith.
 
 Section EdwardsDoubleAndAdd.
   Context {prm:TwistedEdwardsParams}.
-  Definition doubleAndAdd (b n : nat) (P : point) : point :=
-    match N.of_nat n with
-    | 0%N => zero
-    | N.pos p => iter_op unifiedAdd zero b p b P
-    end.
+  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)).
 
   Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P)%E.
   Proof.
@@ -29,43 +26,14 @@ Section EdwardsDoubleAndAdd.
     auto.
   Qed.
 
-  Lemma doubleAndAdd_spec : forall n b P, (Pos.size_nat (Pos.of_nat n) <= b) ->
-    scalarMult n P = doubleAndAdd b n P.
+
+  Lemma doubleAndAdd_spec : forall n P, scalarMult n P = doubleAndAdd n P.
   Proof.
     induction n; auto; intros.
-    unfold doubleAndAdd; simpl.
-    rewrite Pos.of_nat_succ.
-    rewrite iter_op_spec by (auto using zeroIsIdentity).
-    case_eq (Pos.of_nat (S n)); intros. {
-      simpl; f_equal.
-      rewrite (IHn b) by (pose proof (size_of_succ n); omega).
-      unfold doubleAndAdd.
-      rewrite H0 in H.
-      rewrite <- Pos.of_nat_succ in H0.
-      rewrite <- (xI_is_succ n p) by apply H0.
-      rewrite Znat.positive_nat_N; simpl.
-      rewrite iter_op_spec; auto using zeroIsIdentity.
-    } {
-      simpl; f_equal.
-      rewrite (IHn b) by (pose proof (size_of_succ n); omega).
-      unfold doubleAndAdd.
-      rewrite <- (xO_is_succ n p) by (rewrite Pos.of_nat_succ; auto).
-      rewrite Znat.positive_nat_N; simpl.
-      rewrite <- Pos.succ_pred_double in H0.
-      rewrite H0 in H.
-      rewrite iter_op_spec by (auto using zeroIsIdentity;
-        pose proof (Pos.lt_succ_diag_r (Pos.pred_double p));
-        apply Pos.size_nat_monotone in H1; omega; auto).
-      rewrite <- iter_op_double.
-      rewrite Pos.add_diag.
-      rewrite <- Pos.succ_pred_double.
-      rewrite Pos.iter_op_succ by apply twistedAddAssoc; auto.
-    } {
-      rewrite <- Pnat.Pos2Nat.inj_iff in H0.
-      rewrite Pnat.Nat2Pos.id in H0 by auto.
-      rewrite Pnat.Pos2Nat.inj_1 in H0.
-      assert (n = 0)%nat by omega; subst.
-      auto using zeroIsIdentity.
-    }
+    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).
   Qed.
 End EdwardsDoubleAndAdd.
\ No newline at end of file