From bd39778e0679d1f67b5595e655aba1f62ac14e97 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 4 Jan 2016 08:43:33 -0500 Subject: prettier GF25519 derivation that runs out of memory --- src/Specific/GF25519.v | 207 +++++++++++++++++++++++-------------------------- 1 file changed, 97 insertions(+), 110 deletions(-) (limited to 'src') diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index a96997612..f6fd63c0d 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -86,7 +86,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb Lemma base_tail_matches_modulus: 2^k mod nth_default 0 base (pred (length base)) = 0. Proof. - nth_tac. + reflexivity. Qed. Lemma b0_1 : forall x, nth_default x base 0 = 1. @@ -112,17 +112,14 @@ Proof. intros; solve_by_inversion. Qed. -Ltac measure_length ls := - pose proof (eq_refl (length ls)) as Hlen; - match goal with [H: ls = ?lsdef |- _ ] => rewrite H in Hlen at 2 end; - simpl in Hlen. - -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]). +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 expand_list_equalities := repeat match goal with | [H: (?x::?xs = ?y::?ys) |- _ ] => @@ -133,8 +130,33 @@ 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. - Local Open Scope Z_scope. Import GF25519Base25Point5. Import GF. @@ -145,122 +167,84 @@ 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. - cbv [plus - seq rev app length map fold_right fold_left skipn firstn nth_default nth_error value error - Base25Point5_10limbs.base GF25519Base25Point5Params.k GF25519Base25Point5Params.c - mul reduce - B.add - E.add E.mul E.mul' E.mul_each E.mul_bi E.mul_bi' E.crosscoef E.zeros - EC.base] in *. - simpl two_p in *. - Ltac acfo := abstract (clear; firstorder). Hint Rewrite - two_power_pos_equiv Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r - Zdiv_1_r + Z.add_assoc + Z.mul_assoc : Z_identities. - Hint Rewrite <- Zpower_exp using acfo : Z_identities. - Hint Rewrite <- Z.pow_sub_r using acfo : Z_identities. (* division is too slow to even compute once, simplify it away*) - autorewrite with Z_identities in *. - - simpl Z.pow in *. cbv [Z.pow_pos Pos.iter] in *. (* compute the exponents that no longer need division *) - autorewrite with Z_identities in *. - - (* remove redundant parentheses *) - repeat rewrite Z.add_assoc in *. - repeat rewrite Z.mul_assoc in *. - (* one equation per limb *) - measure_length h; expand_list h; expand_list_equalities. - (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *) - (* --- 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 HmulRef); auto. { - subst is; clear. intros. simpl in *. repeat break_or_hyp; firstorder. - } - 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. + 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 - | [H: context[GF25519Base25Point5.carry ?i (?x::?xs)] |- _ ] => + | [Hfg: context[carry ?i (?x::?xs)] |- _ ] => (* simplify carry *) let cr := fresh "cr" in - remember (GF25519Base25Point5.carry i (x::xs)) as cr; + idtac i x xs; + remember (carry i (x::xs)) as cr in Hfg; match goal with [ Heq : cr = ?crdef |- _ ] => - cbv [GF25519Base25Point5.carry GF25519Base25Point5.carry_simple GF25519Base25Point5.carry_and_reduce] in Heq; + 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 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 + 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]). - (* 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 *) - 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. + (* pretty-print: sh -c "tr -d '\n' | tr 'Z' '\n' | tr -d \% | sed 's:\s\s*\*\s\s*:\*:g' | column -o' ' -t" *) - clear HmulRef Hh Hf Hg. - existsFromEquations r. - split; auto; congruence. - Defined. + eexists. + existsFromEquations fg. + subst; auto. + Time Defined. End GF25519Base25Point5Formula. Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. @@ -268,3 +252,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. *) + + + -- cgit v1.2.3