From a2895ce0fd849c1fc5913cee24bc77af71b9b506 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 14 Apr 2016 21:26:17 -0400 Subject: Retrieved updated version of Util/IterAssocOp and modified ExtendedCoordinates and Ed25519 to use it. --- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 17 ++++-- src/Specific/Ed25519.v | 20 ++++--- src/Util/IterAssocOp.v | 74 +++++++++++++++----------- 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. -- cgit v1.2.3