Merge and refactor of GF25519

1 files changed, 134 insertions, 140 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 14a7332e7..00669dd86 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -1,6 +1,9 @@
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
 Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Import ListNotations.
@@ -36,18 +39,16 @@ Ltac brute_force_indices := intros; unfold sum_firstn, limb_widths; simpl in *;
   | _ => omega
   end.
 
-Instance params : PseudoMersenneBaseParams modulus := { limb_widths := limb_widths }.
+Instance params25519 : PseudoMersenneBaseParams modulus := { limb_widths := limb_widths }.
 Proof.
-  + apply fold_right_and_True_forall_In_iff.
-    simpl.
-    repeat (split; [omega |]); auto.
-  + unfold limb_widths; congruence.
-  + brute_force_indices.
-  + compute; eauto.
-  + unfold modulus; eauto.
-  + apply prime_modulus.
-  + brute_force_indices.
-Qed.
+  + abstract (apply fold_right_and_True_forall_In_iff; simpl; repeat (split; [omega |]); auto).
+  + abstract (unfold limb_widths; congruence).
+  + abstract brute_force_indices.
+  + cbv; reflexivity.
+  + unfold modulus; reflexivity.
+  + abstract apply prime_modulus.
+  + abstract brute_force_indices.
+Defined.
 
 Ltac twoIndices i j base :=
     intros;
@@ -56,12 +57,6 @@ Ltac twoIndices i j base :=
     repeat match goal with [ x := _ |- _ ] => subst x end;
     simpl in *; repeat break_or_hyp; try omega; vm_compute; reflexivity.
 
-
-Module F25519Base25Point5 := PseudoMersenneBase Base25Point5_10limbs Modulus25519 F25519Base25Point5Params.
-
-Section F25519Base25Point5Formula.
-  Import F25519Base25Point5 Base25Point5_10limbs F25519Base25Point5 F25519Base25Point5Params.
-
 Definition Z_add_opt := Eval compute in Z.add.
 Definition Z_sub_opt := Eval compute in Z.sub.
 Definition Z_mul_opt := Eval compute in Z.mul.
@@ -69,6 +64,7 @@ Definition Z_div_opt := Eval compute in Z.div.
 Definition Z_pow_opt := Eval compute in Z.pow.
 
 Definition nth_default_opt {A} := Eval compute in @nth_default A.
+Definition set_nth_opt {A} := Eval compute in @set_nth A.
 Definition map_opt {A B} := Eval compute in @map A B.
 
 Ltac opt_step :=
@@ -78,125 +74,122 @@ Ltac opt_step :=
        destruct e
   end.
 
-Definition E_mul_bi'_step
-           (mul_bi' : nat -> E.digits -> list Z)
-           (i : nat) (vsr : E.digits)
+Definition mul_bi'_step
+           (mul_bi' : nat -> digits -> list Z -> list Z)
+           (i : nat) (vsr : digits) (bs : list Z)
   : list Z
   := match vsr with
      | [] => []
-     | v :: vsr' => (v * E.crosscoef i (length vsr'))%Z :: mul_bi' i vsr'
+     | v :: vsr' => (v * crosscoef bs i (length vsr'))%Z :: mul_bi' i vsr' bs
      end.
 
-Definition E_mul_bi'_opt_step_sig
-           (mul_bi' : nat -> E.digits -> list Z)
-           (i : nat) (vsr : E.digits)
-  : { l : list Z | l = E_mul_bi'_step mul_bi' i vsr }.
+Definition mul_bi'_opt_step_sig
+           (mul_bi' : nat -> digits -> list Z -> list Z)
+           (i : nat) (vsr : digits) (bs : list Z)
+  : { l : list Z | l = mul_bi'_step mul_bi' i vsr bs }.
 Proof.
   eexists.
-  cbv [E_mul_bi'_step].
+  cbv [mul_bi'_step].
   opt_step.
   { reflexivity. }
-  { cbv [E.crosscoef EC.base Base25Point5_10limbs.base].
+  { cbv [crosscoef ext_base base].
     change Z.div with Z_div_opt.
-    change Z.pow with Z_pow_opt.
-    change Z.mul with Z_mul_opt at 2 3 4 5.
     change @nth_default with @nth_default_opt.
-    change @map with @map_opt.
     reflexivity. }
 Defined.
 
-Definition E_mul_bi'_opt_step
-           (mul_bi' : nat -> E.digits -> list Z)
-           (i : nat) (vsr : E.digits)
+Definition mul_bi'_opt_step
+           (mul_bi' : nat -> digits -> list Z -> list Z)
+           (i : nat) (vsr : digits) (bs : list Z)
   : list Z
-  := Eval cbv [proj1_sig E_mul_bi'_opt_step_sig] in
-      proj1_sig (E_mul_bi'_opt_step_sig mul_bi' i vsr).
+  := Eval cbv [proj1_sig mul_bi'_opt_step_sig] in
+      proj1_sig (mul_bi'_opt_step_sig mul_bi' i vsr bs).
 
-Fixpoint E_mul_bi'_opt
-         (i : nat) (vsr : E.digits) {struct vsr}
+Fixpoint mul_bi'_opt
+         (i : nat) (vsr : digits) (bs : list Z) {struct vsr}
   : list Z
-  := E_mul_bi'_opt_step E_mul_bi'_opt i vsr.
+  := mul_bi'_opt_step mul_bi'_opt i vsr bs.
 
-Definition E_mul_bi'_opt_correct
-           (i : nat) (vsr : E.digits)
-  : E_mul_bi'_opt i vsr = E.mul_bi' i vsr.
+Definition mul_bi'_opt_correct
+           (i : nat) (vsr : digits) (bs : list Z)
+  : mul_bi'_opt i vsr bs = mul_bi' bs i vsr.
 Proof.
   revert i; induction vsr as [|vsr vsrs IHvsr]; intros.
   { reflexivity. }
-  { simpl E.mul_bi'.
+  { simpl mul_bi'.
     rewrite <- IHvsr; clear IHvsr.
-    unfold E_mul_bi'_opt, E_mul_bi'_opt_step.
+    unfold mul_bi'_opt, mul_bi'_opt_step.
     apply f_equal2; [ | reflexivity ].
-    cbv [E.crosscoef EC.base Base25Point5_10limbs.base].
+    cbv [crosscoef ext_base base].
     change Z.div with Z_div_opt.
-    change Z.pow with Z_pow_opt.
-    change Z.mul with Z_mul_opt at 2.
+    change Z.mul with Z_mul_opt at 2 4.
     change @nth_default with @nth_default_opt.
-    change @map with @map_opt.
     reflexivity. }
 Qed.
 
-Definition E_mul'_step
-           (mul' : E.digits -> E.digits -> E.digits)
-           (usr vs : E.digits)
-  : E.digits
+Definition mul'_step
+           (mul' : digits -> digits -> list Z -> digits)
+           (usr vs : digits) (bs : list Z)
+  : digits
   := match usr with
      | [] => []
-     | u :: usr' => E.add (E.mul_each u (E.mul_bi (length usr') vs)) (mul' usr' vs)
+     | u :: usr' => add (mul_each u (mul_bi bs (length usr') vs)) (mul' usr' vs bs)
      end.
 
-Definition E_mul'_opt_step_sig
-           (mul' : E.digits -> E.digits -> E.digits)
-           (usr vs : E.digits)
-  : { d : E.digits | d = E_mul'_step mul' usr vs }.
+Definition mul'_opt_step_sig
+           (mul' : digits -> digits -> list Z -> digits)
+           (usr vs : digits) (bs : list Z)
+  : { d : digits | d = mul'_step mul' usr vs bs }.
 Proof.
   eexists.
-  cbv [E_mul'_step].
+  cbv [mul'_step].
   match goal with
   | [ |- _ = match ?e with nil => _ | _ => _ end :> ?T ]
     => refine (_ : match e with nil => _ | _ => _ end = _);
          destruct e
   end.
   { reflexivity. }
-  { cbv [E.mul_each E.mul_bi].
-    rewrite <- E_mul_bi'_opt_correct.
+  { cbv [mul_each mul_bi].
+    rewrite <- mul_bi'_opt_correct.
+    change @map with @map_opt.
     reflexivity. }
 Defined.
 
-Definition E_mul'_opt_step
-           (mul' : E.digits -> E.digits -> E.digits)
-           (usr vs : E.digits)
-  : E.digits
-  := Eval cbv [proj1_sig E_mul'_opt_step_sig] in proj1_sig (E_mul'_opt_step_sig mul' usr vs).
+Definition mul'_opt_step
+           (mul' : digits -> digits -> list Z -> digits)
+           (usr vs : digits) (bs : list Z)
+  : digits
+  := Eval cbv [proj1_sig mul'_opt_step_sig] in proj1_sig (mul'_opt_step_sig mul' usr vs bs).
 
-Fixpoint E_mul'_opt
-         (usr vs : E.digits)
-  : E.digits
-  := E_mul'_opt_step E_mul'_opt usr vs.
+Fixpoint mul'_opt
+         (usr vs : digits) (bs : list Z)
+  : digits
+  := mul'_opt_step mul'_opt usr vs bs.
 
-Definition E_mul'_opt_correct
-         (usr vs : E.digits)
-  : E_mul'_opt usr vs = E.mul' usr vs.
+Definition mul'_opt_correct
+         (usr vs : digits) (bs : list Z)
+  : mul'_opt usr vs bs = mul' bs usr vs.
 Proof.
   revert vs; induction usr as [|usr usrs IHusr]; intros.
   { reflexivity. }
   { simpl.
     rewrite <- IHusr; clear IHusr.
     apply f_equal2; [ | reflexivity ].
-    cbv [E.mul_each E.mul_bi].
-    rewrite <- E_mul_bi'_opt_correct.
+    cbv [mul_each mul_bi].
+    rewrite <- mul_bi'_opt_correct.
     reflexivity. }
 Qed.
 
-Definition mul_opt_sig (us vs : T) : { b : B.digits | b = mul us vs }.
+Definition mul_opt_sig (us vs : T) : { b : digits | b = mul us vs }.
 Proof.
   eexists.
-  cbv [mul E.mul E.mul_each E.mul_bi E.mul_bi' E.zeros EC.base reduce].
-  rewrite <- E_mul'_opt_correct.
+  cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce].
+  rewrite <- mul'_opt_correct.
+  change @map with @map_opt.
   reflexivity.
 Defined.
 
-Definition mul_opt (us vs : T) : B.digits
+Definition mul_opt (us vs : T) : digits
   := Eval cbv [proj1_sig mul_opt_sig] in proj1_sig (mul_opt_sig us vs).
 
 Definition mul_opt_correct us vs
@@ -224,12 +217,13 @@ Proof.
   nth_tac.
 Qed.
 
+(*
 Definition log_cap_opt_sig
            (i : nat)
   : { z : Z | i < length (Base25Point5_10limbs.log_base) -> (2^z)%Z = cap i }.
 Proof.
   eexists.
-  cbv [cap Base25Point5_10limbs.base].
+  cbv [cap base].
   intros.
   rewrite map_length in *.
   erewrite map_nth_default; [|assumption].
@@ -263,45 +257,50 @@ Definition log_cap_opt (i : nat)
 Definition log_cap_opt_correct (i : nat)
   : i < length Base25Point5_10limbs.log_base -> (2^log_cap_opt i = cap i)%Z
   := proj2_sig (log_cap_opt_sig i).
+*)
 
 Definition carry_opt_sig
-           (i : nat) (b : B.digits)
-  : { d : B.digits | i < length Base25Point5_10limbs.log_base -> d = carry i b }.
+           (i : nat) (b : digits)
+  : { d : digits | (i < length limb_widths)%nat -> d = carry i b }.
 Proof.
   eexists ; intros.
   cbv [carry].
   rewrite <- pull_app_if_sumbool.
-  cbv beta delta [carry_and_reduce carry_simple add_to_nth Base25Point5_10limbs.base].
-  rewrite map_length.
-  repeat lazymatch goal with
-         | [ |- context[cap ?i] ]
-           => replace (cap i) with (2^log_cap_opt i)%Z by (apply log_cap_opt_correct; assumption)
-  end.
+  cbv beta delta [carry carry_and_reduce carry_simple add_to_nth log_cap pow2_mod Z.ones Z.pred].
+  cbv beta iota zeta delta [base PseudoMersenneBaseParams.limb_widths].
+  change @nth_default with @nth_default_opt in *.
+  change @set_nth with @set_nth_opt in *.
   lazymatch goal with
   | [ |- _ = (if ?br then ?c else ?d) ]
-    => let x := fresh "x" in let y := fresh "y" in evar (x:B.digits); evar (y:B.digits); transitivity (if br then x else y); subst x; subst y
+    => 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;
-    rewrite <- Z.land_ones, <- Z.shiftr_div_pow2 by (
-        pose proof (base_range i); pose proof (base_monotonic i);
-        change @nth_default with @nth_default_opt in *;
-        cbv beta delta [log_cap_opt]; rewrite beq_nat_eq_nat_dec; break_if; change Z_sub_opt with Z.sub; omega);
-    reflexivity.
+  break_if; reflexivity.
+
   change @nth_default with @nth_default_opt.
+  change @set_nth with @set_nth_opt.
   change @map with @map_opt.
   rewrite <- @beq_nat_eq_nat_dec.
   reflexivity.
 Defined.
 
+Print carry_opt_sig.
+Definition f := [2;3].
+Definition g := [7;5].
+Compute (mul f g).
+Compute (mul_opt f g).
+
+
 Definition carry_opt i b
   := Eval cbv beta iota delta [proj1_sig carry_opt_sig] in proj1_sig (carry_opt_sig i b).
 
-Definition carry_opt_correct i b : i < length Base25Point5_10limbs.log_base -> carry_opt i b = carry i b := proj2_sig (carry_opt_sig i b).
 
-Definition carry_sequence_opt_sig (is : list nat) (us : B.digits)
-  : { b : B.digits | (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> b = carry_sequence is us }.
+
+Definition carry_opt_correct i b : (i < length base)%nat -> carry_opt i b = carry i b := proj2_sig (carry_opt_sig i b).
+
+Definition carry_sequence_opt_sig (is : list nat) (us : digits)
+  : { b : digits | (forall i, In i is -> i < length base)%nat -> b = carry_sequence is us }.
 Proof.
   eexists. intros H.
   cbv [carry_sequence].
@@ -321,7 +320,7 @@ Definition carry_sequence_opt is us := Eval cbv [proj1_sig carry_sequence_opt_si
                                         proj1_sig (carry_sequence_opt_sig is us).
 
 Definition carry_sequence_opt_correct is us
-  : (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> carry_sequence_opt is us = carry_sequence is us
+  : (forall i, In i is -> i < length base)%nat -> carry_sequence_opt is us = carry_sequence is us
   := proj2_sig (carry_sequence_opt_sig is us).
 
 Definition Let_In {A P} (x : A) (f : forall y : A, P y)
@@ -330,32 +329,17 @@ Definition Let_In {A P} (x : A) (f : forall y : A, P y)
 Definition carry_opt_cps_sig
            {T}
            (i : nat)
-           (f : B.digits -> T)
-           (b : B.digits)
-  : { d : T |  i < length Base25Point5_10limbs.log_base -> d = f (carry i b) }.
+           (f : digits -> T)
+           (b : digits)
+  : { d : T |  (i < length base)%nat -> d = f (carry i b) }.
 Proof.
   eexists. intros H.
   rewrite <- carry_opt_correct by assumption.
   cbv beta iota delta [carry_opt].
-  (* TODO: how to match the goal here? Alternatively, rewrite under let binders in carry_opt_sig and remove cbv zeta and restore original match from jgross's commit *)
-  lazymatch goal with [ |- ?LHS = _ ] =>
-  change (LHS = Let_In (nth_default_opt 0%Z b i) (fun di => (f (if beq_nat i (pred (length Base25Point5_10limbs.log_base))
-      then
-       set_nth 0
-         (c *
-          Z.shiftr (di) (log_cap_opt i) +
-          nth_default_opt 0
-            (set_nth i (Z.land di (Z.ones (log_cap_opt i)))
-               b) 0)%Z
-         (set_nth i (Z.land (nth_default_opt 0%Z b i) (Z.ones (log_cap_opt i))) b)
-      else
-       set_nth (S i)
-         (Z.shiftr (di) (log_cap_opt i) +
-          nth_default_opt 0
-            (set_nth i (Z.land (di) (Z.ones (log_cap_opt i)))
-               b) (S i))%Z
-         (set_nth i (Z.land (nth_default_opt 0%Z b i) (Z.ones (log_cap_opt i))) b)))))
-  end.
+  let LHS := match goal with |- ?LHS = ?RHS => LHS end in
+  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).
   reflexivity.
 Defined.
 
@@ -363,19 +347,19 @@ Definition carry_opt_cps {T} i f b
   := Eval cbv beta iota delta [proj1_sig carry_opt_cps_sig] in proj1_sig (@carry_opt_cps_sig T i f b).
 
 Definition carry_opt_cps_correct {T} i f b :
-  i < length Base25Point5_10limbs.log_base ->
+  (i < length base)%nat ->
   @carry_opt_cps T i f b = f (carry i b)
   := proj2_sig (carry_opt_cps_sig i f b).
 
-Definition carry_sequence_opt_cps_sig (is : list nat) (us : B.digits)
-  : { b : B.digits | (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> b = carry_sequence is us }.
+Definition carry_sequence_opt_cps_sig (is : list nat) (us : digits)
+  : { b : digits | (forall i, In i is -> i < length base)%nat -> b = carry_sequence is us }.
 Proof.
   eexists.
   cbv [carry_sequence].
   transitivity (fold_right carry_opt_cps id (List.rev is) us).
   Focus 2.
   { 
-    assert (forall i, In i (rev is) -> i < length Base25Point5_10limbs.log_base) as Hr. {
+    assert (forall i, In i (rev is) -> i < length base)%nat as Hr. {
       subst. intros. rewrite <- in_rev in *. auto. }
     remember (rev is) as ris eqn:Heq.
     rewrite <- (rev_involutive is), <- Heq.
@@ -395,11 +379,11 @@ Definition carry_sequence_opt_cps is us := Eval cbv [proj1_sig carry_sequence_op
                                             proj1_sig (carry_sequence_opt_cps_sig is us).
 
 Definition carry_sequence_opt_cps_correct is us
-  : (forall i, In i is -> i < length Base25Point5_10limbs.log_base) -> carry_sequence_opt_cps is us = carry_sequence is us
+  : (forall i, In i is -> i < length base)%nat -> carry_sequence_opt_cps is us = carry_sequence is us
   := proj2_sig (carry_sequence_opt_cps_sig is us).
 
 Lemma mul_opt_rep:
-  forall (u v : T) (x y : F Modulus25519.modulus), rep u x -> rep v y -> rep (mul_opt u v) (x * y)%F.
+  forall (u v : T) (x y : F modulus), rep u x -> rep v y -> rep (mul_opt u v) (x * y)%F.
 Proof.
   intros.
   rewrite mul_opt_correct.
@@ -407,9 +391,9 @@ Proof.
 Qed.
 
 Lemma carry_sequence_opt_cps_rep
-     : forall (is : list nat) (us : list Z) (x : F Modulus25519.modulus),
-       (forall i : nat, In i is -> i < length Base25Point5_10limbs.base) ->
-       length us = length Base25Point5_10limbs.base ->
+     : forall (is : list nat) (us : list Z) (x : F modulus),
+       (forall i : nat, In i is -> i < length base)%nat ->
+       length us = length base ->
        rep us x -> rep (carry_sequence_opt_cps is us) x.
 Proof.
   intros.
@@ -421,19 +405,23 @@ Definition carry_mul_opt
            (is : list nat)
            (us vs : list Z)
            : list Z
-  := Eval cbv [B.add
-    E.add E.mul E.mul' E.mul_bi E.mul_bi' E.mul_each E.zeros EC.base E_mul'_opt
-    E_mul'_opt_step E_mul_bi'_opt E_mul_bi'_opt_step
-    List.app List.rev Z_div_opt Z_mul_opt Z_pow_opt
-    Z_sub_opt app beq_nat log_cap_opt carry_opt_cps carry_sequence_opt_cps error firstn
-    fold_left fold_right id length map map_opt mul mul_opt nth_default nth_default_opt
+  := Eval cbv [
+    add mul BaseSystem.mul mul' mul_bi mul_bi' mul_each zeros ext_base mul'_opt
+    mul'_opt_step mul_bi'_opt mul_bi'_opt_step
+    List.app List.rev Z_div_opt Z_mul_opt Z_pow_opt set_nth_opt
+    Z_sub_opt app beq_nat carry_opt_cps carry_sequence_opt_cps error firstn
+    base_from_limb_widths PseudoMersenneBaseParams.limb_widths pow2_mod two_p sum_firstn two_power_pos
+    fold_left fold_right id length map map_opt mul mul_opt nth_default nth_default_opt shift_pos Pos.iter
     nth_error plus pred reduce rev seq set_nth skipn value base] in 
     carry_sequence_opt_cps is (mul_opt us vs).
 
+Definition test := Eval cbv delta [carry_mul_opt] in (carry_mul_opt [0%nat] [1] [2]).
+Extraction "/tmp/test.ml" test.
+
 Lemma carry_mul_opt_correct
-  : forall (is : list nat) (us vs : list Z) (x  y: F Modulus25519.modulus),
+  : forall (is : list nat) (us vs : list Z) (x  y: F modulus),
     rep us x -> rep vs y ->
-    (forall i : nat, In i is -> i < length Base25Point5_10limbs.base) ->
+    (forall i : nat, In i is -> i < length base)%nat ->
     length (mul_opt us vs) = length base ->
     rep (carry_mul_opt is us vs) (x*y)%F.
 Proof.
@@ -442,7 +430,7 @@ Proof.
   apply carry_sequence_opt_cps_rep, mul_opt_rep; auto.
 Qed.
   
-
+Local Open Scope nat_scope.
   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,
@@ -458,9 +446,15 @@ Qed.
     specialize (Hfg H); clear H.
     forward Hfg; [exact eq_refl|].
     specialize (Hfg H); clear H.
-
-    cbv [log_base map k c carry_mul_opt] in Hfg.
-    cbv beta iota delta [Let_In] in Hfg.
+    
+    assert (exists p p0, rep [p0] p) as Hp by admit.
+    destruct Hp as [p [p0 Hp]].
+    assert (exists p p0, rep [p0] p) as Hq by admit.
+    destruct Hq as [q [q0 Hq]].
+    assert (rep (carry_mul_opt [0] [p0] [q0]) (p*q)%F) as Hpq by admit.
+    Timeout 5 cbv [carry_mul_opt] in Hpq.
+    Set Printing Depth 2.
+    cbv - [Z.mul Z.add Z.shiftr Z.land Let_In] in Hfg.
     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 in Hfg.
     rewrite ?Z.mul_assoc, ?Z.add_assoc in Hfg.
     exact Hfg.