From cba593ad55f11631055ae1337efde89acae67eca Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 10 Jul 2016 15:11:44 -0400 Subject: added proofs about addition chain exponentiation for later use in ModularBaseSystem [pow], which we need for sqrt and inversion. --- src/Algebra.v | 28 +++--- .../CompleteEdwardsCurveTheorems.v | 2 +- src/Experiments/EdDSARefinement.v | 2 +- src/Spec/EdDSA.v | 2 +- src/Util/AdditionChainExponentiation.v | 102 +++++++++++++++++++++ src/Util/ListUtil.v | 9 ++ src/Util/Option.v | 9 ++ 7 files changed, 139 insertions(+), 15 deletions(-) create mode 100644 src/Util/AdditionChainExponentiation.v diff --git a/src/Algebra.v b/src/Algebra.v index 62b216b92..f9dfbd519 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -345,9 +345,11 @@ Module Group. auto using associative, left_identity, right_identity, left_inverse, right_inverse. Qed. End GroupByHomomorphism. +End Group. - Section ScalarMult. - Context {G eq add zero opp} `{@group G eq add zero opp}. +Module ScalarMult. + Section ScalarMultProperties. + Context {G eq add zero} `{@monoid G eq add zero}. Context {mul:nat->G->G}. Local Infix "=" := eq : type_scope. Local Infix "=" := eq. Local Infix "+" := add. Local Infix "*" := mul. @@ -377,14 +379,8 @@ Module Group. Proof. induction n; intros. { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } - { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. apply cancel_left, IHn. } - Qed. - - Lemma opp_mul : forall n P, opp (n * P) = n * (opp P). - induction n; intros. - { rewrite !scalarmult_0_l, inv_id; reflexivity. } - { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. - rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. } + { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. + rewrite IHn. reflexivity. } Qed. Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero. @@ -396,8 +392,16 @@ Module Group. rewrite (NPeano.Nat.div_mod n l Hnz) at 2. rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity. Qed. - End ScalarMult. -End Group. + Context {opp} {group:@group G eq add zero opp}. + + Lemma opp_mul : forall n P, opp (n * P) = n * (opp P). + induction n; intros. + { rewrite !scalarmult_0_l, Group.inv_id; reflexivity. } + { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. + rewrite scalarmult_add_l, scalarmult_1_l, Group.inv_op, scalarmult_S_l, Group.cancel_left; eauto. } + Qed. + End ScalarMultProperties. +End ScalarMult. Require Coq.nsatz.Nsatz. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 0afc07c5d..65d899463 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -10,7 +10,7 @@ Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. Module E. - Import Group Ring Field CompleteEdwardsCurve.E. + Import Group ScalarMult Ring Field CompleteEdwardsCurve.E. Section CompleteEdwardsCurveTheorems. Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v index 79c9b05dd..484650934 100644 --- a/src/Experiments/EdDSARefinement.v +++ b/src/Experiments/EdDSARefinement.v @@ -1,6 +1,6 @@ Require Import Crypto.Spec.EdDSA Bedrock.Word. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Algebra. Import Group. +Require Import Crypto.Algebra. Import Group ScalarMult. Require Import Util.Decidable Util.Option Util.Tactics. Require Import Omega. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 03a723e10..25109bc4c 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -37,7 +37,7 @@ Section EdDSA. := { EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; - EdDSA_scalarmult:@Algebra.Group.is_scalarmult E Eeq Eadd Ezero EscalarMult; + EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero EscalarMult; EdDSA_c_valid : c = 2 \/ c = 3; diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v new file mode 100644 index 000000000..ca1394115 --- /dev/null +++ b/src/Util/AdditionChainExponentiation.v @@ -0,0 +1,102 @@ +Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations. +Require Import Crypto.Util.ListUtil. +Require Import Algebra. Import Monoid ScalarMult. +Require Import VerdiTactics. +Require Import Crypto.Util.Option. + +Section AddChainExp. + Function add_chain (is:list (nat*nat)) : list nat := + match is with + | nil => nil + | (i,j)::is' => + let chain' := add_chain is' in + nth_default 1 chain' i + nth_default 1 chain' j::chain' + end. + +Example wikipedia_addition_chain : add_chain (rev [ +(0, 0); (* 2 = 1 + 1 *) (* the indices say how far back the chain to look *) +(0, 1); (* 3 = 2 + 1 *) +(0, 0); (* 6 = 3 + 3 *) +(0, 0); (* 12 = 6 + 6 *) +(0, 0); (* 24 = 12 + 12 *) +(0, 2); (* 30 = 24 + 6 *) +(0, 6)] (* 31 = 30 + 1 *) +) = [31; 30; 24; 12; 6; 3; 2]. reflexivity. Qed. + + Context {G eq op id} {monoid:@Algebra.monoid G eq op id}. + Local Infix "=" := eq : type_scope. + + Function add_chain_exp (is : list (nat*nat)) (x : G) : list G := + match is with + | nil => nil + | (i,j)::is' => + let chain' := add_chain_exp is' x in + op (nth_default x chain' i) (nth_default x chain' j) ::chain' + end. + + Fixpoint scalarmult n (x : G) : G := match n with + | O => id + | S n' => op x (scalarmult n' x) + end. + + Lemma add_chain_exp_step : forall i j is x, + (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x) -> + (eqlistA eq) + (add_chain_exp ((i,j) :: is) x) + (op (scalarmult (nth_default 1 (add_chain is) i) x) + (scalarmult (nth_default 1 (add_chain is) j) x) :: add_chain_exp is x). + Proof. + intros. + unfold add_chain_exp; fold add_chain_exp. + apply eqlistA_cons; [ | reflexivity]. + f_equiv; auto. + Qed. + + Lemma scalarmult_same : forall c x y, eq x y -> eq (scalarmult c x) (scalarmult c y). + Proof. + induction c; intros. + + reflexivity. + + simpl. f_equiv; auto. + Qed. + + Lemma scalarmult_pow_add : forall a b x, scalarmult (a + b) x = op (scalarmult a x) (scalarmult b x). + Proof. + intros; eapply scalarmult_add_l. + Grab Existential Variables. + 2:eauto. + econstructor; try reflexivity. + repeat intro; subst. + auto using scalarmult_same. + Qed. + + Lemma add_chain_exp_spec : forall is x, + (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x). + Proof. + induction is; intros. + + simpl; rewrite !nth_default_nil. cbv. + symmetry; apply right_identity. + + destruct a. + rewrite add_chain_exp_step by auto. + unfold add_chain; fold add_chain. + destruct n. + - rewrite !nth_default_cons, scalarmult_pow_add. reflexivity. + - rewrite !nth_default_cons_S; auto. + Qed. + + Lemma add_chain_exp_answer : forall is x n, Logic.eq (head (add_chain is)) (Some n) -> + option_eq eq (Some (scalarmult n x)) (head (add_chain_exp is x)). + Proof. + intros. + change head with (fun {T} (xs : list T) => nth_error xs 0) in *. + cbv beta in *. + cbv [option_eq]. + destruct is; [ discriminate | ]. + destruct p. + simpl in *. + injection H; clear H; intro H. + subst n. + rewrite !add_chain_exp_spec. + apply scalarmult_pow_add. + Qed. + +End AddChainExp. \ No newline at end of file diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 50927c2a4..b4285aad0 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -926,3 +926,12 @@ Proof. rewrite <-!app_comm_cons, !map2_cons. rewrite IHls1; auto. Qed. + +Require Import Coq.Lists.SetoidList. +Global Instance Proper_nth_default : forall A eq, + Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)). +Proof. + do 5 intro; subst; induction 1. + + repeat intro; rewrite !nth_default_nil; assumption. + + repeat intro; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto. +Qed. diff --git a/src/Util/Option.v b/src/Util/Option.v index db4b69dde..2c11771ff 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -60,3 +60,12 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ] => change (option_rect P S N (Some x)) with (S x); cbv beta end. + +Definition option_eq {A} eq (x y : option A) := + match x with + | None => y = None + | Some ax => match y with + | None => False + | Some ay => eq ax ay + end + end. -- cgit v1.2.3