automated most of the code in GF25519

2 files changed, 67 insertions, 51 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index e2369f5d6..f93534a99 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -20,6 +20,8 @@ Definition Z_sub_opt := Eval compute in Z.sub.
 Definition Z_mul_opt := Eval compute in Z.mul.
 Definition Z_div_opt := Eval compute in Z.div.
 Definition Z_pow_opt := Eval compute in Z.pow.
+Definition Z_opp_opt := Eval compute in Z.opp.
+Definition Z_shiftl_opt := Eval compute in Z.shiftl.
 Definition Z_shiftl_by_opt := Eval compute in Z_shiftl_by.
 
 Definition nth_default_opt {A} := Eval compute in @nth_default A.
@@ -27,6 +29,10 @@ Definition set_nth_opt {A} := Eval compute in @set_nth A.
 Definition map_opt {A B} := Eval compute in @map A B.
 Definition base_from_limb_widths_opt := Eval compute in base_from_limb_widths.
 
+Definition Let_In {A P} (x : A) (f : forall y : A, P y)
+  := let y := x in f y.
+
+(* Some automation that comes in handy when constructing base parameters *)
 Ltac opt_step :=
   match goal with
   | [ |- _ = match ?e with nil => _ | _ => _ end :> ?T ]
@@ -44,8 +50,47 @@ Ltac brute_force_indices limb_widths := intros; unfold sum_firstn, limb_widths;
   | _ => omega
   end.
 
-Definition Let_In {A P} (x : A) (f : forall y : A, P y)
-  := let y := x in f y.
+
+Definition limb_widths_from_len len k := Eval compute in
+  (fix loop i prev :=
+    match i with
+    | O => nil
+    | S i' => let x := (if (Z.eq_dec ((k * Z.of_nat (len - i + 1)) mod (Z.of_nat len)) 0)
+                        then (k * Z.of_nat (len - i + 1)) / Z.of_nat len
+                        else (k * Z.of_nat (len - i + 1)) / Z.of_nat len + 1)in
+      x - prev:: (loop i' x)
+    end) len 0.
+
+Ltac construct_params prime_modulus len k :=
+  let lw := fresh "lw" in set (lw := limb_widths_from_len len k);
+  cbv in lw;
+  eapply Build_PseudoMersenneBaseParams with (limb_widths := lw);
+  [ abstract (apply fold_right_and_True_forall_In_iff; simpl; repeat (split; [omega |]); auto)
+  | abstract (unfold limb_widths; cbv; congruence)
+  | abstract brute_force_indices lw
+  | abstract apply prime_modulus
+  | abstract brute_force_indices lw].
+
+Ltac subst_precondition := match goal with
+  | [H : ?P, H' : ?P -> _ |- _] => specialize (H' H); clear H
+end.
+
+Ltac kill_precondition H := 
+  forward H; [abstract (try exact eq_refl; clear; cbv; intros; repeat break_or_hyp; intuition)|];
+  subst_precondition.
+
+Ltac compute_formula :=
+  match goal with
+  | [H : _ -> _ -> rep _ ?result |- rep _ ?result] => kill_precondition H; compute_formula
+  | [H : _ -> rep _ ?result |- rep _ ?result] => kill_precondition H; compute_formula
+  | [H : @rep ?M ?P _ ?result |- @rep ?M ?P _ ?result] =>
+    let m := fresh "m" in set (m := M) in H at 1; change M with m at 1;
+    let p := fresh "p" in set (p := P) in H at 1; change P with p at 1;
+    let r := fresh "r" in set (r := result) in H |- *;
+    cbv -[m p r rep] in H;
+    repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in H;
+    exact H
+  end.
 
 Section Carries.
   Context `{prm : PseudoMersenneBaseParams}
@@ -69,9 +114,8 @@ Section Carries.
     | [ |- _ = (if ?br then ?c else ?d) ]
       => let x := fresh "x" in let y := fresh "y" in evar (x:digits); evar (y:digits); transitivity (if br then x else y); subst x; subst y
     end.
-    Focus 2.
-    cbv zeta.
-    break_if; reflexivity.
+    2:cbv zeta.
+    2:break_if; reflexivity.
 
     change @nth_default with @nth_default_opt.
     rewrite c_subst.
@@ -126,6 +170,9 @@ Section Carries.
     let RHS := match goal with |- ?LHS = ?RHS => RHS end in
     let RHSf := match (eval pattern (nth_default_opt 0%Z b i) in RHS) with ?RHSf _ => RHSf end in
     change (LHS = Let_In (nth_default_opt 0%Z b i) RHSf).
+    change Z.shiftl with Z_shiftl_opt.
+    change (-1) with (Z_opp_opt 1).
+    change Z.add with Z_add_opt at 8 12 20 24.
     reflexivity.
   Defined.
 
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 695cfc254..1f6be80cc 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -15,24 +15,20 @@ Local Open Scope Z.
 Definition modulus : Z := 2^255 - 19.
 Lemma prime_modulus : prime modulus. Admitted.
 
-Definition limb_widths : list Z := [26;25;26;25;26;25;26;25;26;25].
-
-Instance params25519 : PseudoMersenneBaseParams modulus := { limb_widths := limb_widths }.
-Proof.
-  + abstract (apply fold_right_and_True_forall_In_iff; simpl; repeat (split; [omega |]); auto).
-  + abstract (unfold limb_widths; congruence).
-  + abstract brute_force_indices limb_widths.
-  + abstract apply prime_modulus.
-  + abstract brute_force_indices limb_widths.
+Instance params25519 : PseudoMersenneBaseParams modulus.
+  construct_params prime_modulus 10%nat 255.
 Defined.
 
 (* END PseudoMersenneBaseParams instance construction. *)
 
 (* Precompute k and c *)
-Definition k_ := 255.
-Lemma k_subst : k_ = k. reflexivity. Qed.
-Definition c_ := 19.
-Lemma c_subst : c_ = c. reflexivity. Qed.
+Definition k_ := Eval compute in k.
+Definition c_ := Eval compute in c.
+
+(* Makes Qed not take forever *)
+Opaque Z.shiftr Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land
+  Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul
+  Let_In digits Z.add Pos.add Z.pos_sub.
 
 Local Open Scope nat_scope.
 Lemma GF25519Base25Point5_mul_reduce_formula :
@@ -42,29 +38,9 @@ Lemma GF25519Base25Point5_mul_reduce_formula :
                       -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
                       -> rep ls (f*g)%F}.
 Proof.
-  eexists.
-  intros f g Hf Hg.
-  pose proof (carry_mul_opt_correct k_ c_ k_subst c_subst [0;9;8;7;6;5;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg.
-  forward Hfg; [abstract (clear; cbv; intros; repeat break_or_hyp; intuition)|].
-  specialize (Hfg H); clear H.
-  forward Hfg; [exact eq_refl|].
-  specialize (Hfg H); clear H.
-
-  set (p := params25519) in Hfg at 1.
-  change (params25519) with p at 1.
-  set (fg := (f * g)%F) in Hfg |- * .
-
-  Opaque Z.shiftl Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land
-    Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul
-    Let_In digits Z.add Pos.add Z.pos_sub.
-
-  cbv -[fg rep] in Hfg.
-
-  change (Z.shiftl 1 26 + -1)%Z with 67108863%Z in Hfg.
-  change (Z.shiftl 1 25 + -1)%Z with 33554431%Z in Hfg.
-  repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in Hfg.
-
-  exact Hfg.
+  eexists; intros ? ? Hf Hg.
+  pose proof (carry_mul_opt_correct k_ c_ (eq_refl k_) (eq_refl c_) [0;9;8;7;6;5;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg.
+  compute_formula.
 Time Defined.
 
 Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
@@ -73,6 +49,7 @@ Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
  * The easiest fix will be to make the proof script above fully automated,
  * using [abstract] to contain the proof part. *)
 
+
 Lemma GF25519Base25Point5_add_formula :
   forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
     g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
@@ -83,13 +60,5 @@ Proof.
   eexists.
   intros f g Hf Hg.
   pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg.
-
-  set (p := params25519) in Hfg at 1.
-  change (params25519) with p at 1.
-  set (fg := (f + g)%F) in Hfg |- * .
-
-  cbv -[fg rep] in Hfg.
-  change (Z.shiftl 1 26 + -1)%Z with 67108863%Z in Hfg.
-  change (Z.shiftl 1 25 + -1)%Z with 33554431%Z in Hfg.
-  exact Hfg.
-Defined.
+  compute_formula.
+Defined.
\ No newline at end of file