From aebc0124ee411786cd711042da7abb67cdf5b40a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 6 Jan 2016 00:46:50 -0500 Subject: fix letify to only insert a term once --- src/Specific/GF25519.v | 240 +++++++++++++++++++++++-------------------------- src/Util/ListUtil.v | 9 ++ 2 files changed, 120 insertions(+), 129 deletions(-) (limited to 'src') diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index f6fd63c0d..51f1b14c8 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -6,17 +6,24 @@ Require Import QArith.QArith QArith.Qround. Require Import VerdiTactics. Close Scope Q. +Ltac twoIndices i j base := + intros; + assert (In i (seq 0 (length base))) by nth_tac; + assert (In j (seq 0 (length base))) by nth_tac; + repeat match goal with [ x := _ |- _ ] => subst x end; + simpl in *; repeat break_or_hyp; try omega; vm_compute; reflexivity. + Module Base25Point5_10limbs <: BaseCoefs. Local Open Scope Z_scope. Definition base := map (fun i => two_p (Qceiling (Z_of_nat i *255 # 10))) (seq 0 10). Lemma base_positive : forall b, In b base -> b > 0. Proof. - compute; intros; repeat break_or_hyp; intuition. + compute; intuition; subst; intuition. Qed. Lemma b0_1 : forall x, nth_default x base 0 = 1. Proof. - reflexivity. + auto. Qed. Lemma base_good : @@ -25,11 +32,7 @@ Module Base25Point5_10limbs <: BaseCoefs. let r := (b i * b j) / b (i+j)%nat in b i * b j = r * b (i+j)%nat. Proof. - intros. - assert (In i (seq 0 (length base))) by nth_tac. - assert (In j (seq 0 (length base))) by nth_tac. - subst b; subst r; simpl in *. - repeat break_or_hyp; try omega; vm_compute; reflexivity. + twoIndices i j base. Qed. End Base25Point5_10limbs. @@ -53,7 +56,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb Lemma modulus_pseudomersenne : primeToZ modulus = 2^k - c. Proof. - reflexivity. + auto. Qed. Lemma base_matches_modulus : @@ -65,53 +68,35 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in b i * b j = r * (2^k * b (i+j-length base)%nat). Proof. - intros. - assert (In i (seq 0 (length base))) by nth_tac. - assert (In j (seq 0 (length base))) by nth_tac. - subst b; subst r; simpl in *. - repeat break_or_hyp; try omega; vm_compute; reflexivity. + twoIndices i j base. Qed. Lemma base_succ : forall i, ((S i) < length base)%nat -> let b := nth_default 0 base in b (S i) mod b i = 0. Proof. - intros. - assert (In i (seq 0 (length base))) by nth_tac. - assert (In (S i) (seq 0 (length base))) by nth_tac. - subst b; simpl in *. - repeat break_or_hyp; try omega; vm_compute; reflexivity. + intros; twoIndices i (S i) base. Qed. Lemma base_tail_matches_modulus: 2^k mod nth_default 0 base (pred (length base)) = 0. Proof. - reflexivity. + auto. Qed. Lemma b0_1 : forall x, nth_default x base 0 = 1. Proof. - reflexivity. + auto. Qed. Lemma k_nonneg : 0 <= k. Proof. - rewrite Zle_is_le_bool; reflexivity. + rewrite Zle_is_le_bool; auto. Qed. End GF25519Base25Point5Params. Module GF25519Base25Point5 := GFPseudoMersenneBase Base25Point5_10limbs Modulus25519 GF25519Base25Point5Params. -(* TODO: move to ListUtil *) -Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y. -Proof. - intros; solve_by_inversion. -Qed. -Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys. -Proof. - intros; solve_by_inversion. -Qed. - Ltac expand_list ls := let Hlen := fresh "Hlen" in match goal with [H: ls = ?lsdef |- _ ] => @@ -121,6 +106,28 @@ Ltac expand_list ls := repeat progress (let n:=fresh ls in destruct ls as [|n ]; try solve [revert Hlen; clear; discriminate]); clear Hlen. +Ltac letify r := + match goal with + | [ H' : r = _ |- _ ] => + match goal with + | [ H : ?x = ?e |- _ ] => + is_var x; + match goal with (* only letify equations that appear nowhere other than r *) + | _ => clear H H' x; fail 1 + | _ => fail 2 + end || idtac; + pattern x in H'; + match type of H' with + | (fun z => r = @?e' z) x => + let H'' := fresh "H" in + assert (H'' : r = let x := e in e' x) by + (* congruence is slower for every subsequent letify *) + (rewrite H'; subst x; reflexivity); + clear H'; subst x; rename H'' into H'; cbv beta in H' + end + end + end. + Ltac expand_list_equalities := repeat match goal with | [H: (?x::?xs = ?y::?ys) |- _ ] => let eq_head := fresh "Heq" x in @@ -130,36 +137,81 @@ Ltac expand_list_equalities := repeat match goal with | [H:?x = ?x|-_] => clear H end. - -(* This tactic takes in [r], a variable that we want to use to instantiate an existential. - * We find one other variable mentioned in [r], with its own equality in the hypotheses. - * That equality is then switched into a [let] in [r]'s defining equation. *) -Ltac letify r := - match goal with - | [ H : ?x = ?e |- _ ] => - is_var x; - match goal with - | [ H' : r = _ |- _ ] => - pattern x in H'; - match type of H' with - | (fun z => r = @?e' z) x => - let H'' := fresh "H" in assert (H'' : r = let x := e in e' x) by congruence; - clear H'; subst x; rename H'' into H'; cbv beta in H' - end - end - end. - -(* To instantiate an existential, give a variable with a defining equation to this tactic. - * We instantiate with a [let]-ified version of that equation. *) -Ltac existsFromEquations r := repeat letify r; - match goal with - | [ _ : r = ?e |- context[?u] ] => unify u e - end. - Section GF25519Base25Point5Formula. Import GF25519Base25Point5. Import GF. + Hint Rewrite + Z.mul_0_l + Z.mul_0_r + Z.mul_1_l + Z.mul_1_r + Z.add_0_l + Z.add_0_r + Z.add_assoc + Z.mul_assoc + : Z_identities. + + Ltac deriveModularMultiplicationWithCarries carryscript := + let h := fresh "h" in + let fg := fresh "fg" in + let Hfg := fresh "Hfg" in + intros; + repeat match goal with + | [ Hf: rep ?fs ?f, Hg: rep ?gs ?g |- rep _ ?ret ] => + remember (carry_sequence carryscript (mul fs gs)) as fg; + assert (rep fg ret) as Hfg; [subst fg; apply carry_sequence_rep, mul_rep; eauto|] + | [ H: In ?x carryscript |- ?x < ?bound ] => abstract (revert H; clear; cbv; intros; repeat break_or_hyp; intuition) + | [ Heqfg: fg = carry_sequence _ (mul _ _) |- rep _ ?ret ] => + (* expand bignum multiplication *) + cbv [plus + seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error + mul reduce B.add Base25Point5_10limbs.base GF25519Base25Point5Params.c + E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base] in Heqfg; + repeat match goal with [H:context[E.crosscoef ?a ?b] |- _ ] => (* do this early for speed *) + let c := fresh "c" in set (c := E.crosscoef a b) in H; compute in c; subst c end; + autorewrite with Z_identities in Heqfg; + (* speparate out carries *) + match goal with [ Heqfg: fg = carry_sequence _ ?hdef |- _ ] => remember hdef as h end; + (* one equation per limb *) + expand_list h; expand_list_equalities; + (* expand carry *) + cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqfg + | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a + | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *) + let cr := fresh "cr" in + remember (carry i (x::xs)) as cr in Hfg; + match goal with [ Heq : cr = ?crdef |- _ ] => + (* is there any simpler way to do this? *) + cbv [carry carry_simple carry_and_reduce] in Heq; + simpl eq_nat_dec in Heq; cbv iota beta in Heq; + cbv [set_nth nth_default nth_error value add_to_nth] in Heq; + expand_list cr; expand_list_equalities + end + | [H: context[cap ?i] |- _ ] => let c := fresh "c" in remember (cap i) as c in H; + match goal with [Heqc: c = cap i |- _ ] => + (* is there any simpler way to do this? *) + unfold cap, Base25Point5_10limbs.base in Heqc; + simpl eq_nat_dec in Heqc; + cbv [nth_default nth_error value error] in Heqc; + simpl map in Heqc; + cbv [GF25519Base25Point5Params.k] in Heqc + end; + subst c; + repeat rewrite Zdiv_1_r in H; + repeat rewrite two_power_pos_equiv in H; + repeat rewrite <- Z.pow_sub_r in H by (abstract (clear; firstorder)); + repeat rewrite <- Z.land_ones in H by (abstract (apply Z.leb_le; reflexivity)); + repeat rewrite <- Z.shiftr_div_pow2 in H by (abstract (apply Z.leb_le; reflexivity)); + simpl Z.sub in H; + unfold GF25519Base25Point5Params.c in H + | [H: context[Z.ones ?l] |- _ ] => + (* postponing this to the main loop makes the autorewrite slow *) + let c := fresh "c" in set (c := Z.ones l) in H; compute in c; subst c + | [ |- _ ] => abstract (solve [auto]) + | [ |- _ ] => progress intros + end. + Lemma GF25519Base25Point5_mul_reduce_formula : forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 g0 g1 g2 g3 g4 g5 g6 g7 g8 g9, @@ -168,82 +220,12 @@ Section GF25519Base25Point5Formula. -> rep ls (f*g)%GF}. Proof. - Hint Rewrite - Z.mul_0_l - Z.mul_0_r - Z.mul_1_l - Z.mul_1_r - Z.add_0_l - Z.add_0_r - Z.add_assoc - Z.mul_assoc - : Z_identities. + eexists. - Ltac deriveModularMultiplicationWithCarries carryscript := - let h := fresh "h" in - let fg := fresh "fg" in - let Hfg := fresh "Hfg" in - repeat match goal with - | [ |- { _ | forall f g, rep ?fs f -> rep ?gs g -> rep _ ?ret } ] => - remember (carry_sequence carryscript (mul fs gs)) as fg; - assert (forall f g, rep fs f -> rep gs g -> rep fg ret) as Hfg - | [ H: In ?x carryscript |- ?x < ?bound ] => abstract (revert H; clear; cbv; intros; repeat break_or_hyp; intuition) - | [ Heqfg: fg = carry_sequence _ (mul _ _) |- { _ | forall f g, rep ?fs f -> rep ?gs g -> rep _ ?ret } ] => - (* expand bignum multiplication *) - cbv [plus - seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error - mul reduce B.add Base25Point5_10limbs.base GF25519Base25Point5Params.c - E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base] in Heqfg; - repeat match goal with [H:context[E.crosscoef ?a ?b] |- _ ] => (* do this early for speed *) - let c := fresh "c" in set (c := E.crosscoef a b) in H; compute in c; subst c end; - autorewrite with Z_identities in Heqfg; - (* speparate out carries *) - match goal with [ Heqfg: fg = carry_sequence _ ?hdef |- _ ] => remember hdef as h end; - (* one equation per limb *) - expand_list h; expand_list_equalities; - (* expand carry *) - cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqfg - | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a - | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *) - let cr := fresh "cr" in - idtac i x xs; - remember (carry i (x::xs)) as cr in Hfg; - match goal with [ Heq : cr = ?crdef |- _ ] => - cbv [carry carry_simple carry_and_reduce] in Heq; - simpl eq_nat_dec in Heq; cbv iota beta in Heq; - cbv [set_nth nth_default nth_error value add_to_nth] in Heq; - expand_list cr; expand_list_equalities - end - | [H: context[cap ?i] |- _ ] => let c := fresh "c" in remember (cap i) as c in H; - match goal with [Heqc: c = cap i |- _ ] => - unfold cap, Base25Point5_10limbs.base in Heqc; - simpl eq_nat_dec in Heqc; - cbv [nth_default nth_error value error] in Heqc; - simpl map in Heqc; - cbv [GF25519Base25Point5Params.k] in Heqc - end; - subst c; - repeat rewrite Zdiv_1_r in H; - repeat rewrite two_power_pos_equiv in H; - repeat rewrite <- Z.pow_sub_r in H by (abstract (clear; firstorder)); - repeat rewrite <- Z.land_ones in H by (abstract (apply Z.leb_le; reflexivity)); - repeat rewrite <- Z.shiftr_div_pow2 in H by (abstract (apply Z.leb_le; reflexivity)); - simpl Z.sub in H; - unfold GF25519Base25Point5Params.c in H - | [H: context[Z.ones ?l] |- _ ] => - (* postponing this to the main loop makes the autorewrite slow *) - let c := fresh "c" in set (c := Z.ones l) in H; compute in c; subst c - | [ |- _ ] => subst fg; apply carry_sequence_rep, mul_rep - | [ |- _ ] => abstract (solve [auto]) - | [ |- _ ] => progress intros - end. Time deriveModularMultiplicationWithCarries (rev [0;1;2;3;4;5;6;7;8;9;0]). - (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *) - eexists. - existsFromEquations fg. - subst; auto. + Time repeat letify fg; subst fg; eauto. Time Defined. End GF25519Base25Point5Formula. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 350f55dd8..783e3f527 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -524,3 +524,12 @@ Ltac set_nth_inbounds := end. Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds. + +Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y. +Proof. + intros; solve_by_inversion. +Qed. +Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys. +Proof. + intros; solve_by_inversion. +Qed. -- cgit v1.2.3