diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-06-14 00:36:23 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-06-14 13:05:52 -0400 |
commit | 53d6e0a991ce110864b2293eb25feca4042186eb (patch) | |
tree | 5a63e122cd2444aa12531f5f7a3bef159c7cca69 /src/Util | |
parent | 362eaa5da1f291b86aa04e8d745738a647ee34ce (diff) |
ScalarMult: Z -> G -> G (closes #193)
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/AdditionChainExponentiation.v | 35 | ||||
-rw-r--r-- | src/Util/IterAssocOp.v | 179 |
2 files changed, 6 insertions, 208 deletions
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index f35c4e9ea..8de191eda 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -6,6 +6,12 @@ Require Import Crypto.Util.Option. Require Import Crypto.Util.Tactics.BreakMatch. Section AddChainExp. + (* TODO: rewrite this. + - use CPS and Loop + - use an inner loop for repeated squaring + - connect to something that abstracts over F.pow, Z.pow, N.pow NOT scalarmult + *) + Function fold_chain {T} (id:T) (op:T->T->T) (is:list (nat*nat)) (acc:list T) {struct is} : T := match is with | nil => @@ -27,33 +33,4 @@ Section AddChainExp. (0, 2); (* 30 = 24 + 6 *) (0, 6)] (* 31 = 30 + 1 *) [1] = 31. reflexivity. Qed. - - Context {G eq op id} {monoid:@Algebra.Hierarchy.monoid G eq op id}. - Context {scalarmult} {is_scalarmult:@ScalarMult.is_scalarmult G eq op id scalarmult}. - Local Infix "=" := eq : type_scope. - Local Open Scope N_scope. - Local Notation "n * P" := (scalarmult (N.to_nat n) P) (only parsing). - - Lemma fold_chain_exp' : forall (x:G) is acc ref - (H:forall i, nth_default id acc i = (nth_default 0 ref i) * x) - (Hl:Logic.eq (length acc) (length ref)), - fold_chain id op is acc = (fold_chain 0 N.add is ref) * x. - Proof using Type*. - intro x; induction is; intros acc ref H Hl; simpl @fold_chain. - { repeat break_match; specialize (H 0%nat); rewrite ?nth_default_cons, ?nth_default_cons_S in H; - solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. } - { repeat break_match. eapply IHis; intros; [|auto with distr_length]; []. - match goal with - [H:context [nth_default _ ?l _] |- context[nth_default _ (?h::?l) ?i] ] - => destruct i; rewrite ?nth_default_cons, ?nth_default_cons_S; - solve [ apply H | rewrite !H, <-scalarmult_add_l, Nnat.N2Nat.inj_add; reflexivity ] - end. } - Qed. - - Lemma fold_chain_exp x is: fold_chain id op is [x] = (fold_chain 0 N.add is [1]) * x. - Proof using Type*. - eapply fold_chain_exp'; trivial; intros i. - destruct i as [|i]; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil; - rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity. - Qed. End AddChainExp. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v deleted file mode 100644 index 4d9365e4d..000000000 --- a/src/Util/IterAssocOp.v +++ /dev/null @@ -1,179 +0,0 @@ -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. -Require Import Crypto.Util.NUtil. -Require Import Crypto.Util.Tactics.BreakMatch. - -Local Open Scope equiv_scope. - -Generalizable All Variables. -Section IterAssocOp. - Context {T eq op id} {moinoid : @Algebra.Hierarchy.monoid T eq op id} (testbit : nat -> bool). - Local Infix "===" := eq. Local Infix "===" := eq : type_scope. - - Local Notation nat_iter_op := (ScalarMult.scalarmult_ref (add:=op) (zero:=id)). - - Lemma nat_iter_op_plus m n a : - op (nat_iter_op m a) (nat_iter_op n a) === nat_iter_op (m + n) a. - Proof using Type*. symmetry; eapply ScalarMult.scalarmult_add_l. Qed. - - Definition N_iter_op n a := - match n with - | 0%N => id - | Npos p => Pos.iter_op op p a - end. - - Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a). - Proof using Type*. - induction p as [p IHp|p IHp|]; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity. - Qed. - - Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a === op a (N_iter_op n a). - Proof using Type*. - destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?Algebra.Hierarchy.right_identity; reflexivity. - Qed. - - Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a. - Proof using Type*. - induction n as [|n IHn] using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity. - Qed. - - Context {sel:bool->T->T->T} {sel_correct:forall b x y, sel b x y = if b then y else x}. - - Fixpoint funexp {A} (f : A -> A) (a : A) (exp : nat) : A := - match exp with - | O => a - | S exp' => f (funexp f a exp') - end. - - Definition test_and_op a (state : nat * T) := - let '(i, acc) := state in - let acc2 := op acc acc in - let acc2a := op a acc2 in - match i with - | O => (0, acc) - | S i' => (i', sel (testbit i') acc2 acc2a) - end. - - Definition iter_op bound a : T := - snd (funexp (test_and_op a) (bound, id) bound). - - (* correctness reference *) - Context {x:N} {testbit_correct : forall i, testbit i = N.testbit_nat x i}. - - Definition test_and_op_inv a (s : nat * T) := - snd s === nat_iter_op (N.to_nat (N.shiftr_nat x (fst s))) a. - - Lemma test_and_op_inv_step : forall a s, - test_and_op_inv a s -> - test_and_op_inv a (test_and_op a s). - Proof using Type*. - destruct s as [i acc]. - unfold test_and_op_inv, test_and_op; simpl; intro Hpre. - destruct i; [ apply Hpre | ]. - simpl. - rewrite N.shiftr_succ. - rewrite sel_correct. - case_eq (testbit i); intro testbit_eq; simpl; - rewrite testbit_correct in testbit_eq; rewrite testbit_eq; - rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity. - Qed. - - Lemma test_and_op_inv_holds : forall a i s, - test_and_op_inv a s -> - test_and_op_inv a (funexp (test_and_op a) s i). - Proof using Type*. - induction i; intros; auto; simpl; apply test_and_op_inv_step; auto. - Qed. - - Lemma funexp_test_and_op_index : forall a x acc y, - fst (funexp (test_and_op a) (x, acc) y) = x - y. - Proof using Type. - induction y as [|? IHy]; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity. - match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end. - simpl in IHy. - unfold test_and_op. - destruct i; rewrite Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. - Qed. - - Lemma iter_op_termination : forall a bound, - N.size_nat x <= bound -> - test_and_op_inv a - (funexp (test_and_op a) (bound, id) bound) -> - iter_op bound a === nat_iter_op (N.to_nat x) a. - Proof using moinoid. - unfold test_and_op_inv, iter_op; simpl; intros ? ? ? Hinv. - rewrite Hinv, funexp_test_and_op_index, Minus.minus_diag. - reflexivity. - Qed. - - Lemma iter_op_correct : forall a bound, N.size_nat x <= bound -> - iter_op bound a === nat_iter_op (N.to_nat x) a. - Proof using Type*. - intros. - apply iter_op_termination; auto. - apply test_and_op_inv_holds. - unfold test_and_op_inv. - simpl. - rewrite N.shiftr_size by auto. - reflexivity. - Qed. -End IterAssocOp. - -Require Import Coq.Classes.Morphisms. -(*Require Import Crypto.Util.Tactics.*) -Require Import Crypto.Util.Relations. - -Global Instance Proper_funexp {T R} {Equivalence_R:Equivalence R} - : Proper ((R==>R) ==> R ==> Logic.eq ==> R) (@funexp T). -Proof. - repeat intro; subst. - match goal with [n0 : nat |- _ ] => rename n0 into n; induction n as [|n IHn] end; [solve [trivial]|]. - match goal with - [H: (_ ==> _)%signature _ _ |- _ ] => - etransitivity; solve [eapply (H _ _ IHn)|reflexivity] - end. -Qed. - -Global Instance Proper_test_and_op {T R} {Equivalence_R:@Equivalence T R} : - Proper ((R==>R==>R) - ==> pointwise_relation _ Logic.eq - ==> (Logic.eq==>R==>R==>R) - ==> R - ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) - ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) - ) (@test_and_op T). -Proof. - repeat match goal with - | _ => intro - | _ => split - | [p:prod _ _ |- _ ] => destruct p - | [p:and _ _ |- _ ] => destruct p - | _ => progress (cbv [fst snd test_and_op pointwise_relation respectful] in * ) - | _ => progress subst - | _ => progress break_match - | _ => solve [ congruence | eauto 99 ] - end. -Qed. - -Global Instance Proper_iter_op {T R} {Equivalence_R:@Equivalence T R} : - Proper ((R==>R==>R) - ==> R - ==> pointwise_relation _ Logic.eq - ==> (Logic.eq==>R==>R==>R) - ==> Logic.eq - ==> R - ==> R) - (@iter_op T). -Proof. - repeat match goal with - | _ => solve [ reflexivity | congruence | eauto 99 ] - | [ R : _ |- _ ] - => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) - | _ => progress eapply Proper_test_and_op - | _ => progress split - | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) - | _ => intro - end. -Qed. |