move B_order_l and prime_q

4 files changed, 165 insertions, 10 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index de6d39202..86c075e19 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -878,7 +878,6 @@ Proof.
   2:vm_decide.
   apply dec_bool.
   vm_cast_no_check (eq_refl true).
-Admitted.
 (* Time Qed. (* Finished transaction in 1646.167 secs (1645.753u,0.339s) (successful) *) *)
 
 Definition sign := @EdDSARepChange.sign E
@@ -903,7 +902,7 @@ Definition sign := @EdDSARepChange.sign E
             (@ModularArithmetic.F.opp q) (@ModularArithmetic.F.add q) (@ModularArithmetic.F.sub q)
             (@ModularArithmetic.F.mul q) (@ModularArithmetic.F.inv q) (@ModularArithmetic.F.div q)
             (@PrimeFieldTheorems.F.field_modulo q prime_q) (@ModularArithmeticTheorems.F.eq_dec q) Spec.Ed25519.a
-            Spec.Ed25519.d curve_params) b H c n l B Eenc Senc (@ed25519 H) Erep ERepEnc SRep SC25519.SRepDecModL
+            Spec.Ed25519.d curve_params) b H c n l B Eenc Senc (@ed25519 H B_order_l ) Erep ERepEnc SRep SC25519.SRepDecModL
          SRepERepMul SRepEnc SC25519.SRepAdd SC25519.SRepMul ERepB SC25519.SRepDecModLShort.
 
 Let sign_correct : forall pk sk {mlen} (msg:Word.word mlen), sign pk sk _ msg = EdDSA.sign pk sk msg :=
@@ -922,7 +921,7 @@ Let sign_correct : forall pk sk {mlen} (msg:Word.word mlen), sign pk sk _ msg =
       (* B := *) B
       (* Eenc := *) Eenc
       (* Senc := *) Senc
-      (* prm := *) ed25519
+      (* prm := *) (ed25519 B_order_l)
       (* Erep := *) Erep
       (* ErepEq := *) ExtendedCoordinates.Extended.eq
       (* ErepAdd := *) ErepAdd
@@ -1448,7 +1447,7 @@ Let verify_correct :
       (* B := *) B
       (* Eenc := *) Eenc
       (* Senc := *) Senc
-      (* prm := *) ed25519
+      (* prm := *) (ed25519 B_order_l)
       (* Proper_Eenc := *) (PointEncoding.Proper_encode_point (b:=b-1))
       (* Edec := *) Edec
       (* eq_enc_E_iff := *) eq_enc_E_iff
@@ -1480,4 +1479,4 @@ Let verify_correct :
       (* SRepDec_correct := *) SRepDec_correct
 .
 Let both_correct := (@sign_correct, @verify_correct).
-Print Assumptions both_correct.
+Print Assumptions both_correct.
\ No newline at end of file
diff --git a/src/MxDHRepChange.v b/src/MxDHRepChange.v
new file mode 100644
index 000000000..1b8427afa
--- /dev/null
+++ b/src/MxDHRepChange.v
@@ -0,0 +1,157 @@
+Require Import Crypto.Spec.MxDH.
+Require Import Crypto.Algebra. Import Monoid Group Ring Field.
+Require Import Crypto.Util.Tuple.
+
+Section MxDHRepChange.
+  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {Fcswap:bool->F*F->F*F->(F*F)*(F*F)} {Fa24:F} {tb1:nat->bool}.
+  Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {impl_field:@Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {Keq_dec:Decidable.DecidableRel Keq} {Kcswap:bool->K*K->K*K->(K*K)*(K*K)} {Ka24:K} {tb2:nat->bool}.
+
+  Context {FtoK} {homom:@Ring.is_homomorphism F Feq Fone Fadd Fmul
+                                              K Keq Kone Kadd Kmul FtoK}.
+  Context {homomorphism_inv_zero:Keq (FtoK (Finv Fzero)) (Kinv Kzero)}.
+  Context {homomorphism_a24:Keq (FtoK Fa24) Ka24}.
+  Context {Fcswap_correct:forall b x y, Fcswap b x y = if b then (y,x) else (x,y)}.
+  Context {Kcswap_correct:forall b x y, Kcswap b x y = if b then (y,x) else (x,y)}.
+  Context {tb2_correct:forall i, tb2 i = tb1 i}.
+
+  (* TODO: move to algebra *)
+  Lemma homomorphism_multiplicative_inverse_complete' x : Keq (FtoK (Finv x)) (Kinv (FtoK x)).
+  Proof.
+    eapply (homomorphism_multiplicative_inverse_complete).
+    intro J; rewrite J. rewrite homomorphism_inv_zero, homomorphism_id.
+    reflexivity.
+  Qed.
+
+  Ltac t :=
+    repeat (
+        rewrite homomorphism_id ||
+        rewrite homomorphism_one ||
+        rewrite homomorphism_a24 ||
+        rewrite homomorphism_sub ||
+        rewrite homomorphism_add ||
+        rewrite homomorphism_mul ||
+        rewrite homomorphism_multiplicative_inverse_complete' ||
+        reflexivity
+      ).
+
+  Import Crypto.Util.Tactics.
+  Import List.
+  Import Coq.Classes.Morphisms.
+
+  Global Instance Proper_ladderstep :
+    Proper (Keq ==> (fieldwise (n:=2) Keq) ==> fieldwise (n:=2) Keq ==> fieldwise (n:=2) (fieldwise (n:=2) Keq)) (@MxDH.ladderstep K Kadd Ksub Kmul Ka24).
+  Proof.
+    cbv [MxDH.ladderstep tuple tuple' fieldwise fieldwise' fst snd];
+      repeat intro; destruct_head' prod; destruct_head' and; repeat split;
+        repeat match goal with [H:Keq ?x ?y |- _ ] => rewrite !H; clear H x end; reflexivity.
+  Qed.
+
+  Lemma MxLadderstepRepChange u P Q Ku (Ku_correct:Keq (FtoK u) Ku):
+    fieldwise (n:=2) (fieldwise (n:=2) Keq)
+    ((Tuple.map (n:=2) (Tuple.map (n:=2) FtoK)) (@MxDH.ladderstep F Fadd Fsub Fmul Fa24 u P Q))
+    (@MxDH.ladderstep K Kadd Ksub Kmul Ka24 Ku (Tuple.map (n:=2) FtoK P) (Tuple.map (n:=2) FtoK Q)).
+  Proof.
+    destruct P as [? ?], Q as [? ?]; cbv; repeat split; rewrite <-?Ku_correct; t.
+  Qed.
+
+  Let loopiter_sig F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u :
+    { loopiter | @MxDH.montladder F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u =
+      let '(_, _, _) := MxDH.downto _ _ loopiter in  _ } := exist _ _ eq_refl.
+  Let loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u :=
+  Eval cbv [proj1_sig loopiter_sig] in (
+    proj1_sig (loopiter_sig F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u)).
+
+  Let loopiter_phi s : ((K * K) * (K * K)) * bool :=
+    (Tuple.map (n:=2) (Tuple.map (n:=2) FtoK) (fst s), snd s).
+
+  Let loopiter_eq (a b: (((K * K) * (K * K)) * bool)) :=
+    fieldwise (n:=2) (fieldwise (n:=2) Keq) (fst a) (fst b) /\ snd a = snd b.
+
+  Local Instance Equivalence_loopiter_eq : Equivalence loopiter_eq.
+  Proof.
+    unfold loopiter_eq; split; repeat intro;
+      intuition (reflexivity||symmetry;eauto||etransitivity;symmetry;eauto).
+  Qed.
+
+  Lemma MxLoopIterRepChange b Fu s i Ku (HKu:Keq (FtoK Fu) Ku) : loopiter_eq
+    (loopiter_phi (loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 Fu s i))
+    (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 Ku (loopiter_phi s) i).  
+  Proof.
+    destruct_head' prod; break_match.
+    simpl.
+    rewrite !Fcswap_correct, !Kcswap_correct, tb2_correct in *.
+    break_match; cbv [loopiter_eq loopiter_phi fst snd]; split; try reflexivity;
+      (etransitivity;[|etransitivity]; [ | eapply (MxLadderstepRepChange _ _ _ _ HKu) | ];
+            match goal with Heqp:_ |- _ => rewrite <-Heqp; reflexivity end).
+  Qed.
+
+  Global Instance Proper_fold_left {A RA B RB} :
+    Proper ((RA==>RB==>RA) ==> SetoidList.eqlistA RB ==> RA ==> RA) (@fold_left A B).
+  Proof.
+    intros ? ? ? ? ? Hl; induction Hl; repeat intro; [assumption|].
+    simpl; cbv [Proper respectful] in *; eauto.
+  Qed.
+
+  Lemma proj_fold_left {A B L} R {Equivalence_R:@Equivalence B R} (proj:A->B) step step' {Proper_step':(R ==> eq ==> R)%signature step' step'} (xs:list L) init init' (H0:R (proj init) init') (Hproj:forall x i, R (proj (step x i)) (step' (proj x) i)) :
+         R (proj (fold_left step xs init)) (fold_left step' xs init').
+  Proof.
+    generalize dependent init; generalize dependent init'.
+    induction xs; [solve [eauto]|].
+    repeat intro; simpl; rewrite IHxs by eauto.
+    f_equiv; eapply Proper_step'; eauto.
+  Qed.
+
+  Global Instance Proper_downto {T R} {Equivalence_R:@Equivalence T R} :
+    Proper (R ==> Logic.eq ==> (R==>Logic.eq==>R) ==> R) MxDH.downto.
+  Proof.
+    intros s0 s0' Hs0 n' n Hn'; subst n'; generalize dependent s0; generalize dependent s0'.
+    induction n; repeat intro; [assumption|].
+    unfold MxDH.downto; simpl.
+    eapply Proper_fold_left; try eassumption; try reflexivity.
+    cbv [Proper respectful] in *; eauto.
+  Qed.
+
+  Global Instance Proper_loopiter a b c :
+   Proper (loopiter_eq ==> eq ==> loopiter_eq) (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap a b c).
+  Proof.
+    unfold loopiter; intros [? ?] [? ?] [[[] []] ?] ? ? ?; cbv [fst snd] in * |-; subst.
+    repeat VerdiTactics.break_match; subst; repeat (VerdiTactics.find_injection; intros; subst).
+    split; [|reflexivity].
+    etransitivity; [|etransitivity]; [ | eapply Proper_ladderstep | ];
+      [eapply eq_subrelation; [ exact _ | symmetry; eassumption ]
+      | reflexivity | |
+      | eapply eq_subrelation; [exact _ | eassumption ] ];
+      rewrite !Kcswap_correct in *;
+      match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end;
+      repeat (VerdiTactics.find_injection; intros; subst);
+    split; simpl; eauto.
+  Qed.
+
+  Lemma MxDHRepChange b (x:F) :
+    Keq
+      (FtoK (@MxDH.montladder F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 x))
+      (@MxDH.montladder K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 (FtoK x)).
+  Proof.
+    cbv [MxDH.montladder].
+    repeat break_match.
+    assert (Hrel:loopiter_eq (loopiter_phi (p, p0, b0)) (p1, p3, b1)).
+    {
+      rewrite <-Heqp0; rewrite <-Heqp.
+      unfold MxDH.downto.
+      eapply (proj_fold_left (L:=nat) loopiter_eq loopiter_phi).
+      { eapply @Proper_loopiter. }
+      { cbv; repeat split; t. }
+      { intros; eapply MxLoopIterRepChange; reflexivity. }
+    }
+    { destruct_head' prod; destruct Hrel as [[[] []] ?]; simpl in *; subst.
+      rewrite !Fcswap_correct, !Kcswap_correct in *.
+      match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end;
+        repeat (VerdiTactics.find_injection; intros; subst);
+        repeat match goal with [H: Keq (FtoK ?x) (?kx)|- _ ] => rewrite <- H end;
+        t.
+    }
+    Grab Existential Variables.
+    exact 0.
+    exact 0.
+  Qed.
+End MxDHRepChange.
\ No newline at end of file
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index d6873607f..aa904fc7e 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -71,15 +71,13 @@ Section Ed25519.
     let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x).
   Definition Senc : Fl -> Word.word b := Fencode (len:=b).
 
-  (* TODO(andreser): prove this after we have fast scalar multplication *)
-  Axiom B_order_l : CompleteEdwardsCurveTheorems.E.eq (BinInt.Z.to_nat l * B)%E E.zero.
-
   Require Import Crypto.Util.Decidable.
   Definition ed25519 :
+    CompleteEdwardsCurveTheorems.E.eq (BinInt.Z.to_nat l * B)%E E.zero -> (* TODO: prove this earlier than Experiments/Ed25519? *)
     EdDSA (E:=E) (Eadd:=E.add) (Ezero:=E.zero) (EscalarMult:=E.mul) (B:=B)
           (Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp) (* TODO: move defn *)
           (Eeq:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.eq) (* TODO: move defn *)
           (l:=l) (b:=b) (n:=n) (c:=c)
           (Eenc:=Eenc) (Senc:=Senc) (H:=H).
-  Proof. split; try exact _; try exact B_order_l; vm_decide. Qed.
+  Proof. split; try (assumption || exact _); vm_decide. Qed.
 End Ed25519.
\ No newline at end of file
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 0a487b1e2..2c0365fd2 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -14,6 +14,7 @@ Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
+Require Crypto.Spec.Ed25519.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Local Open Scope Z.
@@ -21,7 +22,7 @@ Local Open Scope Z.
 (* BEGIN precomputation. *)
 
 Definition modulus : Z := Eval compute in 2^255 - 19.
-Lemma prime_modulus : prime modulus. Admitted.
+Definition prime_modulus : prime modulus := Crypto.Spec.Ed25519.prime_q.
 Definition int_width := 64%Z.
 Definition freeze_input_bound := 32%Z.