diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-01-06 01:14:06 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-01-06 01:14:06 -0500 |
commit | 90260a82f8ea511f1b9ba8d352c18b7e6a621e57 (patch) | |
tree | 3346ef42856d9c1fd90edf8faef9e9507e10616d | |
parent | 71553f59573301744c7d34aeec6a371ee50a65cf (diff) | |
parent | aebc0124ee411786cd711042da7abb67cdf5b40a (diff) |
Merge branch 'specific-rewrite'
-rw-r--r-- | src/Specific/GF25519.v | 323 | ||||
-rw-r--r-- | src/Util/ListUtil.v | 9 |
2 files changed, 133 insertions, 199 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 235c34a9b..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,59 +68,65 @@ 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. - nth_tac. + 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. -Ltac expand_list f := - assert ((length f < 100)%nat) as _ by (simpl length in *; omega); - repeat progress ( - let n := fresh f in - destruct f as [ | n ]; - try solve [simpl length in *; try discriminate]). - -(* 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 |- _ ] => + assert (Hlen:length ls=length lsdef) by (f_equal; exact H) + end; + simpl in Hlen; + 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) |- _ ] => @@ -129,10 +138,80 @@ Ltac expand_list_equalities := repeat match goal with end. Section GF25519Base25Point5Formula. - Local Open Scope Z_scope. 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, @@ -140,171 +219,14 @@ Section GF25519Base25Point5Formula. -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g -> rep ls (f*g)%GF}. Proof. - intros. - eexists. - intros f g Hf Hg. - pose proof (mul_rep _ _ _ _ Hf Hg) as HmulRef. - remember (GF25519Base25Point5.mul [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9]) as h. - unfold - GF25519Base25Point5.mul, - GF25519Base25Point5.B.add, - GF25519Base25Point5.E.mul, - GF25519Base25Point5.E.mul', - GF25519Base25Point5.E.mul_bi, - GF25519Base25Point5.E.mul_bi', - GF25519Base25Point5.E.mul_each, - GF25519Base25Point5.E.add, - GF25519Base25Point5.B.digits, - GF25519Base25Point5.E.digits, - Base25Point5_10limbs.base, - GF25519Base25Point5.E.crosscoef, - nth_default - in Heqh; simpl in Heqh. - - unfold - two_power_pos, - shift_pos - in Heqh; simpl in Heqh. - - (* evaluate row-column crossing coefficients for variable base multiplication *) - (* unfoldZ.div in Heqh; simpl in Heqh. *) (* THIS TAKES TOO LONG *) - repeat rewrite Z_div_same_full in Heqh by (abstract (apply Zeq_bool_neq; reflexivity)). - repeat match goal with [ Heqh : context[ (?a / ?b)%Z ] |- _ ] => - replace (a / b)%Z with 2%Z in Heqh by - (abstract (symmetry; erewrite <- Z.div_unique_exact; try apply Zeq_bool_neq; reflexivity)) - end. - - 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_identities. - autorewrite with Z_identities in Heqh. - - (* inline explicit formulas for modular reduction *) - cbv beta iota zeta delta [GF25519Base25Point5.reduce Base25Point5_10limbs.base] in Heqh. - remember GF25519Base25Point5Params.c as c in Heqh; unfold GF25519Base25Point5Params.c in Heqc. - simpl in Heqh. + eexists. - (* prettify resulting modular multiplication expression *) - repeat rewrite (Z.mul_add_distr_l c) in Heqh. - repeat rewrite (Z.mul_assoc _ _ 2) in Heqh. - repeat rewrite (Z.mul_comm _ 2) in Heqh. - repeat rewrite (Z.mul_assoc 2 c) in Heqh. - remember (2 * c)%Z as TwoC in Heqh; subst c; simpl in HeqTwoC; subst TwoC. (* perform operations on constants *) - repeat rewrite Z.add_assoc in Heqh. - repeat rewrite Z.mul_assoc in Heqh. - assert (Hhl: length h = 10%nat) by (subst h; reflexivity); expand_list h; clear Hhl. - expand_list_equalities. + 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" *) - (* output: - h0 = (f0*g0 + 38*f9*g1 + 19*f8*g2 + 38*f7*g3 + 19*f6*g4 + 38*f5*g5 + 19*f4*g6 + 38*f3*g7 + 19*f2*g8 + 38*f1*g9) - h1 = (f1*g0 + f0*g1 + 19*f9*g2 + 19*f8*g3 + 19*f7*g4 + 19*f6*g5 + 19*f5*g6 + 19*f4*g7 + 19*f3*g8 + 19*f2*g9) - h2 = (f2*g0 + 2*f1*g1 + f0*g2 + 38*f9*g3 + 19*f8*g4 + 38*f7*g5 + 19*f6*g6 + 38*f5*g7 + 19*f4*g8 + 38*f3*g9) - h3 = (f3*g0 + f2*g1 + f1*g2 + f0*g3 + 19*f9*g4 + 19*f8*g5 + 19*f7*g6 + 19*f6*g7 + 19*f5*g8 + 19*f4*g9) - h4 = (f4*g0 + 2*f3*g1 + f2*g2 + 2*f1*g3 + f0*g4 + 38*f9*g5 + 19*f8*g6 + 38*f7*g7 + 19*f6*g8 + 38*f5*g9) - h5 = (f5*g0 + f4*g1 + f3*g2 + f2*g3 + f1*g4 + f0*g5 + 19*f9*g6 + 19*f8*g7 + 19*f7*g8 + 19*f6*g9) - h6 = (f6*g0 + 2*f5*g1 + f4*g2 + 2*f3*g3 + f2*g4 + 2*f1*g5 + f0*g6 + 38*f9*g7 + 19*f8*g8 + 38*f7*g9) - h7 = (f7*g0 + f6*g1 + f5*g2 + f4*g3 + f3*g4 + f2*g5 + f1*g6 + f0*g7 + 19*f9*g8 + 19*f8*g9) - h8 = (f8*g0 + 2*f7*g1 + f6*g2 + 2*f5*g3 + f4*g4 + 2*f3*g5 + f2*g6 + 2*f1*g7 + f0*g8 + 38*f9*g9) - h9 = (f9*g0 + f8*g1 + f7*g2 + f6*g3 + f5*g4 + f4*g5 + f3*g6 + f2*g7 + f1*g8 + f0*g9) - *) - - (* prove equivalence of multiplication to the stated *) - assert (rep [h0; h1; h2; h3; h4; h5; h6; h7; h8; h9] (f * g)%GF) as Hh. { - subst h0. subst h1. subst h2. subst h3. subst h4. subst h5. subst h6. subst h7. subst h8. subst h9. - repeat match goal with [H: _ = _ |- _ ] => - rewrite <- H; clear H - end. - assumption. - } - (* --- carry phase --- *) - remember (rev [0;1;2;3;4;5;6;7;8;9;0])%nat as is; simpl in Heqis. - destruct (fun pf pf2 => carry_sequence_rep is _ _ pf pf2 Hh). { - subst is. clear. intros. simpl in *. firstorder. - } { - reflexivity. - } - remember (carry_sequence is [h0; h1; h2; h3; h4; h5; h6; h7; h8; h9]) as r; subst is. - - (* unroll the carry loop, create a separate variable for each of the 10 list elements *) - cbv [GF25519Base25Point5.carry_sequence fold_right rev app] in Heqr. - repeat match goal with - | [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a - | [H: context[GF25519Base25Point5.carry ?i (?x::?xs)] |- _ ] => - let cr := fresh "cr" in - remember (GF25519Base25Point5.carry i (x::xs)) as cr; - match goal with [ Heq : cr = ?crdef |- _ ] => - cbv [GF25519Base25Point5.carry GF25519Base25Point5.carry_simple GF25519Base25Point5.carry_and_reduce] in Heq; - simpl eq_nat_dec in Heq; cbv iota beta in Heq; - cbv [set_nth nth_default nth_error value GF25519Base25Point5.add_to_nth] in Heq; - let Heql := fresh "Heql" in - assert (length cr = length crdef) as Heql by (subst cr; reflexivity); - simpl length in Heql; expand_list cr; clear Heql; - expand_list_equalities - end - end. - - (* compute the human-meaningful froms of constants used during carrying *) - cbv [GF25519Base25Point5.cap Base25Point5_10limbs.base GF25519Base25Point5Params.k] in *. - simpl eq_nat_dec in *; cbv iota in *. - repeat match goal with - | [H: _ |- _ ] => - rewrite (map_nth_default _ _ _ _ 0%nat 0%Z) in H by (abstract (clear; rewrite seq_length; firstorder)) - end. - simpl two_p in *. - repeat rewrite two_power_pos_equiv in *. - repeat rewrite <- Z.pow_sub_r in * by (abstract (clear; firstorder)). - simpl Z.sub in *; - rewrite Zdiv_1_r in *. - - (* replace division and Z.modulo with bit operations *) - remember (2 ^ 25)%Z as t25 in *. - remember (2 ^ 26)%Z as t26 in *. - repeat match goal with [H1: ?a = ?b, H2: ?b = ?c |- _ ] => subst a end. - subst t25. subst t26. - rewrite <- Z.land_ones in * by (abstract (clear; firstorder)). - rewrite <- Z.shiftr_div_pow2 in * by (abstract (clear; firstorder)). - - (* evaluate the constant arguments to bit operations *) - remember (Z.ones 25) as m25 in *. compute in Heqm25. subst m25. - remember (Z.ones 26) as m26 in *. compute in Heqm26. subst m26. - unfold GF25519Base25Point5Params.c in *. - - (* 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. - - clear HmulRef Hh Hf Hg. - existsFromEquations r. - split; auto; congruence. - Defined. + Time repeat letify fg; subst fg; eauto. + Time Defined. End GF25519Base25Point5Formula. Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. @@ -312,3 +234,6 @@ Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. * More Ltac acrobatics will be needed to get out that formula for further use in Coq. * The easiest fix will be to make the proof script above fully automated, * using [abstract] to contain the proof part. *) + + + 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. |