Canonicalization is now automated in GF25519 and added to GF1305.

3 files changed, 76 insertions, 107 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 8ac8c95c5..c0e942ece 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -30,6 +30,9 @@ Definition map_opt {A B} := Eval compute in @map A B.
 Definition full_carry_chain_opt := Eval compute in @full_carry_chain.
 Definition length_opt := Eval compute in length.
 Definition base_opt := Eval compute in @base.
+Definition max_ones_opt := Eval compute in @max_ones.
+Definition max_bound_opt := Eval compute in @max_bound.
+Definition minus_opt := Eval compute in minus.
 
 Definition Let_In {A P} (x : A) (f : forall y : A, P y)
   := let y := x in f y.
@@ -80,6 +83,10 @@ Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits
       2 ^ (x + 1) - (2 * c) :: map (fun w => 2 ^ (w + 1) - 2) tail
   end.
 
+Ltac compute_preconditions :=
+  cbv; intros; repeat match goal with H : _ \/ _ |- _  =>
+    destruct H; subst; [ congruence | ] end; (congruence || omega).
+
 Ltac subst_precondition := match goal with
   | [H : ?P, H' : ?P -> _ |- _] => specialize (H' H); clear H
 end.
@@ -97,8 +104,7 @@ Ltac compute_formula :=
     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 PseudoMersenneBaseRep.rep] in H;
-    repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in H;
-    exact H
+    repeat rewrite ?Z.mul_1_r, ?Z.add_0_l, ?Z.add_assoc, ?Z.mul_assoc in H
   end.
 
 Section Carries.
@@ -181,7 +187,7 @@ Section Carries.
     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.
+    change Z.add with Z_add_opt at 5 9 17 21.
     reflexivity.
   Defined.
 
@@ -536,62 +542,31 @@ Section Multiplication.
 
 End Multiplication.
 
+Record freezePreconditions {modulus} (prm : PseudoMersenneBaseParams modulus) int_width :=
+mkFreezePreconditions {
+    lt_1_length_base : (1 < length base)%nat;
+    int_width_pos : 0 < int_width;
+    int_width_compat : forall w, In w limb_widths -> w <= int_width;
+    c_pos : 0 < c;
+    c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < max_bound 0 + 1;
+    c_reduce2 : c <= max_bound 0 - c;
+    two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus
+}.
+Local Hint Resolve lt_1_length_base int_width_pos int_width_compat c_pos
+    c_reduce1 c_reduce2 two_pow_k_le_2modulus.
+
 Section Canonicalization.
   Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_)
-    (lt_1_length_base : (1 < length base)%nat)
-    {int_width} (int_width_pos : 0 < int_width) (int_width_compat : forall w, In w limb_widths -> w <= int_width)
-    (c_pos : 0 < c)
-    (c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < max_bound 0 + 1)
-    (c_reduce2 : c <= max_bound 0 - c)
-    (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus).
-
-  Definition max_ones_opt := Eval compute in max_ones.
-  Definition max_bound_opt := Eval compute in max_bound.
-  Definition minus_opt := Eval compute in minus.
-
-  Definition isFull'_opt_sig (us : T) full i :
-    { b : bool | b = isFull' us full i }.
-  Proof.
-    eexists.
-    cbv [isFull'].
-    change max_bound with max_bound_opt.
-    rewrite c_subst.
-    change Z.sub with Z_sub_opt.
-    reflexivity.
-  Defined.
-
-  Definition isFull'_opt (us : T) full i: bool
-    := Eval cbv [proj1_sig isFull'_opt_sig] in proj1_sig (isFull'_opt_sig us full i).
-
-  Definition isFull'_opt_correct us full i: isFull'_opt us full i = isFull' us full i :=
-    proj2_sig (isFull'_opt_sig us full i).
-
-  Definition and_term_opt_sig (us : list Z) : { b : Z | b = and_term us }.
-  Proof.
-    eexists.
-    cbv [and_term isFull].
-    change length with length_opt.
-    rewrite <-isFull'_opt_correct.
-    change max_ones with max_ones_opt.
-    change @base with base_opt.
-    change minus with minus_opt.
-    reflexivity.
-  Defined.
-
-  Definition and_term_opt (us : digits) : Z
-    := Eval cbv [proj1_sig and_term_opt_sig] in proj1_sig (and_term_opt_sig us).
-
-  Definition and_term_opt_correct us : and_term_opt us = and_term us :=
-    proj2_sig (and_term_opt_sig us). 
+    {int_width} (preconditions : freezePreconditions prm int_width).
 
   Definition modulus_digits_opt_sig :
     { b : digits | b = modulus_digits }.
   Proof.
     eexists.
     cbv beta iota delta [modulus_digits modulus_digits' app].
-    change max_bound with max_bound_opt.
+    change @max_bound with max_bound_opt.
     rewrite c_subst.
     change length with length_opt.
     change minus with minus_opt.
@@ -646,13 +621,14 @@ Section Canonicalization.
     rewrite <-carry_full_3_opt_cps_correct with (f := RHSf).
     cbv beta iota delta [and_term isFull isFull'].
     change length with length_opt.
-    change max_bound with max_bound_opt.
+    change @max_bound with max_bound_opt.
     rewrite c_subst.
-    change max_ones with max_ones_opt.
+    change @max_ones with max_ones_opt.
     change @base with base_opt.
     change minus with minus_opt.
-    rewrite <-modulus_digits_opt_correct.
     change @map with @map_opt.
+    change Z.sub with Z_sub_opt at 1.
+    rewrite <-modulus_digits_opt_correct.
     reflexivity.
   Defined.
 
@@ -664,20 +640,23 @@ Section Canonicalization.
     := proj2_sig (freeze_opt_sig us).
 
   Lemma freeze_opt_canonical: forall us vs x,
-    @pre_carry_bounds _ _ int_width us -> rep us x -> 
-    @pre_carry_bounds _ _ int_width vs -> rep vs x ->
+    @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x -> 
+    @pre_carry_bounds _ _ int_width vs -> PseudoMersenneBaseRep.rep vs x ->
     freeze_opt us = freeze_opt vs.
   Proof.
     intros.
     rewrite !freeze_opt_correct.
+    change PseudoMersenneBaseRep.rep with rep in *.
     eapply freeze_canonical with (B := int_width); eauto.
   Qed.
 
-  Lemma freeze_opt_preserves_rep : forall us x, rep us x -> rep (freeze_opt us) x.
+  Lemma freeze_opt_preserves_rep : forall us x, PseudoMersenneBaseRep.rep us x ->
+    PseudoMersenneBaseRep.rep (freeze_opt us) x.
   Proof.
     intros.
     rewrite freeze_opt_correct.
-    eauto using freeze_preserves_rep.
+    change PseudoMersenneBaseRep.rep with rep in *.
+    eapply freeze_preserves_rep; eauto.
   Qed.
 
   Lemma freeze_opt_spec : forall us vs x, rep us x -> rep vs x ->
@@ -686,7 +665,6 @@ Section Canonicalization.
     (PseudoMersenneBaseRep.rep (freeze_opt us) x /\ freeze_opt us = freeze_opt vs).
   Proof.
     split; eauto using freeze_opt_canonical.
-    change PseudoMersenneBaseRep.rep with rep.
     auto using freeze_opt_preserves_rep.
   Qed.
 
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 31dee21f3..02ef714d9 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -15,6 +15,7 @@ Local Open Scope Z.
 
 Definition modulus : Z := 2^130 - 5.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := 32%Z.
 
 Instance params1305 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 5%nat 130.
@@ -26,16 +27,22 @@ Instance subCoeff : SubtractionCoefficient modulus params1305.
   apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto.
 Defined.
 
+Definition freezePreconditions1305 : freezePreconditions params1305 int_width.
+Proof.
+  constructor; compute_preconditions.
+Defined.
+
 (* END PseudoMersenneBaseParams instance construction. *)
 
 (* Precompute k and c *)
 Definition k_ := Eval compute in k.
 Definition c_ := Eval compute in c.
+Definition c_subst : c = c_ := eq_refl 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.
+  Let_In digits Z.add Pos.add Z.pos_sub andb Z.eqb Z.ltb.
 
 Local Open Scope nat_scope.
 Lemma GF1305Base26_mul_reduce_formula :
@@ -45,8 +52,9 @@ Lemma GF1305Base26_mul_reduce_formula :
                       -> rep ls (f*g)%F}.
 Proof.
   eexists; intros ? ? Hf Hg.
-  pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg.
+  pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) c_subst _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
+  exact Hfg.
 Defined.
 
 Lemma GF1305Base26_add_formula :
@@ -58,17 +66,30 @@ Proof.
   eexists; intros ? ? Hf Hg.
   pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
+  exact Hfg.
 Defined.
 
-Lemma GF25519Base25Point5_sub_formula :
-  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
-    g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
-    {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f
-                   -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
+Lemma GF1305Base26_sub_formula :
+  forall f0 f1 f2 f3 f4 g0 g1 g2 g3 g4,
+    {ls | forall f g, rep [f0;f1;f2;f3;f4] f
+                   -> rep [g0;g1;g2;g3;g4] g
                    -> rep ls (f - g)%F}.
 Proof.
   eexists.
   intros f g Hf Hg.
   pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
-Defined.
\ No newline at end of file
+  exact Hfg.
+Defined.
+
+Lemma GF1305Base26_freeze_formula :
+  forall f0 f1 f2 f3 f4,
+    {ls | forall x, rep [f0;f1;f2;f3;f4] x
+                 -> rep ls x}.
+Proof.
+  eexists.
+  intros x Hf.
+  pose proof (freeze_opt_preserves_rep _ c_subst freezePreconditions1305 _ _ Hf) as Hfreeze_rep.
+  compute_formula.
+  exact Hfreeze_rep.
+Defined.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 2ec338625..8ee9b25d8 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -16,6 +16,7 @@ Local Open Scope Z.
 
 Definition modulus : Z := 2^255 - 19.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := 32%Z.
 
 Instance params25519 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 10%nat 255.
@@ -27,31 +28,18 @@ Instance subCoeff : SubtractionCoefficient modulus params25519.
   apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto.
 Defined.
 
+Definition freezePreconditions25519 : freezePreconditions params25519 int_width.
+Proof.
+  constructor; compute_preconditions.
+Defined.
+
 (* END PseudoMersenneBaseParams instance construction. *)
 
 (* Precompute k and c *)
 Definition k_ := Eval compute in k.
 Definition c_ := Eval compute in c.
-Definition base_ := Eval compute in base.
-Definition limb_widths_ := Eval compute in limb_widths.
-
 Definition c_subst : c = c_ := eq_refl c_.
 
-Lemma c_reduce1 : (c * Z.ones (32 - log_cap (pred (length base))) < max_bound 0 + 1)%Z.
-Proof.
-  cbv; congruence.
-Qed.
-
-Lemma c_reduce2 : c <= max_bound 0 - c.
-Proof.
-  cbv; congruence.
-Qed.
-
-Lemma two_pow_k_le_2modulus : (2 ^ k <= 2 * modulus)%Z.
-Proof.
-  cbv; congruence.
-Qed.
-
 (* 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
@@ -68,6 +56,7 @@ Proof.
   eexists; intros ? ? Hf Hg.
   pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) c_subst _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
+  exact Hfg.
 Time Defined.
 
 Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
@@ -88,6 +77,7 @@ Proof.
   intros f g Hf Hg.
   pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
+  exact Hfg.
 Defined.
 
 Lemma GF25519Base25Point5_sub_formula :
@@ -101,6 +91,7 @@ Proof.
   intros f g Hf Hg.
   pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
+  exact Hfg.
 Defined.
 
 Lemma GF25519Base25Point5_freeze_formula :
@@ -110,35 +101,14 @@ Lemma GF25519Base25Point5_freeze_formula :
 Proof.
   eexists.
   intros x Hf.
-  assert (1 < length base)%nat as lt_1_length_base by (cbv; repeat constructor).
-  assert (0 < 32)%Z by omega.
-  assert (forall w : Z, In w limb_widths -> (w <= 32)%Z) by
-    (cbv [limb_widths params25519 limb_widths_from_len In]; intros w w_cases;
-     repeat (destruct w_cases as  [ ? | w_cases]; [ subst; omega | ]); exfalso; assumption).
-  assert (0 < c)%Z by (change c with c_; cbv; congruence).
-  pose proof c_reduce1.
-  pose proof c_reduce2.
-  pose proof two_pow_k_le_2modulus.
-  pose proof (@freeze_opt_preserves_rep modulus params25519 subCoeff c_ (eq_refl c_) lt_1_length_base 32) as Hfreeze_rep.
-  repeat match goal with H : ?P, H' : ?P -> _ |- _ => specialize (H' H) end.
-  specialize (Hfreeze_rep _ _ Hf).
-  change ModularBaseSystem.rep with rep in Hfreeze_rep.
-  match goal with H : @rep ?M ?P (?f ?l) ?result |- _ =>
-    let m := fresh "m" in
-        set (m := M) in H at 1; change M with m in |- * at 1;
-         (let p := fresh "p" in
-          set (p := P) in H at 1; change P with p in |- * at 1;
-           (let r := fresh "r" in
-            set (r := result) in H |- *))
-  end.
-  cbv [freeze_opt] in Hfreeze_rep.
-  cbv [carry_full_3_opt_cps] in Hfreeze_rep.
-  cbv -[m p r rep] in Hfreeze_rep.
+  pose proof (freeze_opt_preserves_rep _ c_subst freezePreconditions25519 _ _ Hf) as Hfreeze_rep.
+  compute_formula.
   exact Hfreeze_rep.
 Defined.
 
 (* Uncomment the below to see pretty-printed freeze function *)
 (*
+Set Printing Depth 1000.
 Local Transparent Let_In.
 Infix "<<" := Z.shiftr (at level 50).
 Infix "&" := Z.land (at level 50).