Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinates and Ed25519 to use it.

1 files changed, 12 insertions, 5 deletions

diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index e918ac128..976fe59c1 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -219,11 +219,18 @@ Section ExtendedCoordinates.
       unfold equiv, extendedPoint_eq; intros.
       rewrite <-!unifiedAddM1_rep, twistedAddAssoc; auto.
     Qed.
-    
-    Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint zero).
-    Definition scalarMultM1_spec := iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint zero) unifiedAddM1_0_l.
-    Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P) = scalarMult n (unExtendedPoint P).
-      intros; rewrite scalarMultM1_spec, Nat2N.id.
+
+    Lemma testbit_conversion_identity : forall x i, N.testbit_nat x i = N.testbit_nat ((fun a => a) x) i.
+    Proof.
+      trivial.
+    Qed.
+
+    Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint zero) N.testbit_nat.
+    Definition scalarMultM1_spec :=
+      iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint 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).
+      intros; rewrite scalarMultM1_spec, Nat2N.id; auto.
       induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|].
       unfold scalarMult; fold scalarMult.
       rewrite <-IHn, unifiedAddM1_rep; auto.