Merge branch 'specific-rewrite'

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.