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

3 files changed, 68 insertions, 43 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.
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 6e4bea1e5..f98bf2d12 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -13,7 +13,7 @@ Local Infix "++" := Word.combine.
 Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40).
 Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40).
 Local Arguments H {_} _.
-Local Arguments scalarMultM1 {_} {_} _ _.
+Local Arguments scalarMultM1 {_} {_} _ _ _.
 Local Arguments unifiedAddM1 {_} {_} _ _.
 
 Local Ltac set_evars :=
@@ -32,9 +32,10 @@ Proof.
   revert x; induction n as [|n IHn]; simpl; congruence.
 Qed.
 
-Lemma iter_op_proj {T T'} (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') x y z
+Lemma iter_op_proj {T T' S} (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') x y z
+      (testbit : S -> nat -> bool) (bound : nat)
       (op_proj : forall a b, proj (op a b) = op' (proj a) (proj b))
-  : proj (iter_op op x y z) = iter_op op' (proj x) y (proj z).
+  : proj (iter_op op x testbit y z bound) = iter_op op' (proj x) testbit y (proj z) bound.
 Proof.
   unfold iter_op.
   simpl.
@@ -208,8 +209,8 @@ Proof.
   { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
     set_evars.
     repeat match goal with
-           | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?x ?y ?z)] ]
-             => erewrite (@iter_op_proj T A (@proj1_sig _ _)) by reflexivity
+           | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ]
+             => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity 
            end.
     subst_evars.
     reflexivity. }
@@ -305,14 +306,17 @@ Proof.
                (@unifiedAddM1' curve25519params
                   (@iter_op (@extended curve25519params) 
                      (@unifiedAddM1' curve25519params) 
-                     (@twistedToExtended curve25519params (0%F, 1%F)) a
-                     (@twistedToExtended curve25519params Bc))
+                     (@twistedToExtended curve25519params (0%F, 1%F)) 
+                     N N.testbit_nat
+                     a
+                     (@twistedToExtended curve25519params Bc) (N.size_nat a))
                   (negateExtendedc
                      (@iter_op (@extended curve25519params) 
                         (@unifiedAddM1' curve25519params) 
                         (@twistedToExtended curve25519params (0%F, 1%F))
+                        N N.testbit_nat
                         (@wordToN (b + b) (@H (b + (b + l)) (sig [:b] ++ pk ++ msg)))
-                        (twistedToExtended p))))))
+                        (twistedToExtended p) (N.size_nat (@wordToN (b + b) (@H (b + (b + l)) (sig [:b] ++ pk ++ msg)))))))))
         else false) false
        (wire2rep_F (@wtl (b - 1) pk))
                 )
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 016a4f7bd..5e23bb987 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -9,7 +9,11 @@ Section IterAssocOp.
           (assoc: forall a b c, op a (op b c) === op (op a b) c)
           (neutral:T)
           (neutral_l : forall a, op neutral a === a)
-          (neutral_r : forall a, op a neutral === a).
+          (neutral_r : forall a, op a neutral === a)
+          {scalar : Type}
+          (testbit : scalar -> nat -> bool)
+          (scToN : scalar -> N)
+          (testbit_spec : forall x i, testbit x i = N.testbit_nat (scToN x) i).
   Existing Instance op_proper.
 
   Fixpoint nat_iter_op n a :=
@@ -51,19 +55,19 @@ Section IterAssocOp.
     | S exp' => f (funexp f a exp')
     end.
 
-  Definition test_and_op n a (state : nat * T) :=
+  Definition test_and_op sc a (state : nat * T) :=
     let '(i, acc) := state in
     let acc2 := op acc acc in
     match i with
     | O => (0, acc)
-    | S i' => (i', if N.testbit_nat n i' then op a acc2 else acc2)
+    | S i' => (i', if testbit sc i' then op a acc2 else acc2)
     end.
 
-  Definition iter_op n a : T := 
-    snd (funexp (test_and_op n a) (N.size_nat n, neutral) (N.size_nat n)).
+  Definition iter_op sc a bound : T := 
+    snd (funexp (test_and_op sc a) (bound, neutral) bound).
 
-  Definition test_and_op_inv n a (s : nat * T) :=
-    snd s === nat_iter_op (N.to_nat (N.shiftr_nat n (fst s))) a.
+  Definition test_and_op_inv sc a (s : nat * T) :=
+    snd s === nat_iter_op (N.to_nat (N.shiftr_nat (scToN sc) (fst s))) a.
 
   Hint Rewrite
     N.succ_double_spec
@@ -91,7 +95,7 @@ Section IterAssocOp.
     reflexivity.
   Qed.
 
-  Lemma shiftr_succ : forall n i,
+  Lemma Nshiftr_succ : forall n i,
     N.to_nat (N.shiftr_nat n i) =
     if N.testbit_nat n i
     then S (2 * N.to_nat (N.shiftr_nat n (S i)))
@@ -115,21 +119,23 @@ Section IterAssocOp.
       apply N2Nat.id.
   Qed.
 
-  Lemma test_and_op_inv_step : forall n a s,
-    test_and_op_inv n a s ->
-    test_and_op_inv n a (test_and_op n a s).
+  Lemma test_and_op_inv_step : forall sc a s,
+    test_and_op_inv sc a s ->
+    test_and_op_inv sc a (test_and_op sc a s).
   Proof.
     destruct s as [i acc].
     unfold test_and_op_inv, test_and_op; simpl; intro Hpre.
     destruct i; [ apply Hpre | ].
     simpl.
-    rewrite shiftr_succ.
-    case_eq (N.testbit_nat n i); intro; simpl; rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity.
+    rewrite Nshiftr_succ.
+    case_eq (testbit sc i); intro testbit_eq; simpl;
+      rewrite testbit_spec in testbit_eq; rewrite testbit_eq;
+      rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity.
   Qed.
 
-  Lemma test_and_op_inv_holds : forall n a i s,
-    test_and_op_inv n a s ->
-    test_and_op_inv n a (funexp (test_and_op n a) s i).
+  Lemma test_and_op_inv_holds : forall sc a i s,
+    test_and_op_inv sc a s ->
+    test_and_op_inv sc a (funexp (test_and_op sc a) s i).
   Proof.
     induction i; intros; auto; simpl; apply test_and_op_inv_step; auto.
   Qed.
@@ -144,14 +150,14 @@ Section IterAssocOp.
     destruct i; rewrite NPeano.Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity.
   Qed.
 
-  Lemma iter_op_termination : forall n a,
-    test_and_op_inv n a 
-      (funexp (test_and_op n a) (N.size_nat n, neutral) (N.size_nat n)) -> 
-    iter_op n a === nat_iter_op (N.to_nat n) a.
+  Lemma iter_op_termination : forall sc a bound,
+    N.size_nat (scToN sc) <= bound ->
+    test_and_op_inv sc a 
+      (funexp (test_and_op sc a) (bound, neutral) bound) -> 
+    iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a.
   Proof.
-    unfold test_and_op_inv, iter_op; simpl; intros ? ? Hinv.
+    unfold test_and_op_inv, iter_op; simpl; intros ? ? ? ? Hinv.
     rewrite Hinv, funexp_test_and_op_index, Minus.minus_diag.
-    replace (N.shiftr_nat n 0) with n by auto.
     reflexivity.
   Qed.
 
@@ -160,25 +166,33 @@ Section IterAssocOp.
     destruct n; auto; simpl; induction p; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity.
   Qed.
 
-  Lemma Nshiftr_size : forall n, N.shiftr_nat n (N.size_nat n) = 0%N.
+  Lemma Nshiftr_size : forall n bound, N.size_nat n <= bound ->
+    N.shiftr_nat n bound = 0%N.
   Proof.
     intros.
-    rewrite Nsize_nat_equiv.
+    rewrite <- (Nat2N.id bound).
     rewrite Nshiftr_nat_equiv.
-    destruct (N.eq_dec n 0); subst; auto.
+    destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|].
     apply N.shiftr_eq_0.
-    rewrite N.size_log2 by auto.
-    apply N.lt_succ_diag_r.
+    rewrite Nsize_nat_equiv in *.
+    rewrite N.size_log2 in * by auto.
+    apply N.le_succ_l.
+    rewrite <- N.compare_le_iff.
+    rewrite N2Nat.inj_compare.
+    rewrite <- Compare_dec.nat_compare_le.
+    rewrite Nat2N.id.
+    auto.
   Qed.
   
-  Lemma iter_op_spec : forall n a, iter_op n a === nat_iter_op (N.to_nat n) a.
+  Lemma iter_op_spec : forall sc a bound, N.size_nat (scToN sc) <= bound ->
+    iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a.
   Proof.
     intros.
-    apply iter_op_termination.
+    apply iter_op_termination; auto.
     apply test_and_op_inv_holds.
     unfold test_and_op_inv.
     simpl.
-    rewrite Nshiftr_size.
+    rewrite Nshiftr_size by auto.
     reflexivity.
   Qed.