1 files changed, 151 insertions, 93 deletions

diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
index f8e93c6f3..afdf24604 100644
--- a/src/Experiments/EdDSARefinement.v
+++ b/src/Experiments/EdDSARefinement.v
@@ -1,9 +1,12 @@
+Require Import Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Spec.EdDSA Bedrock.Word.
-Require Import Coq.Classes.Morphisms.
+Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
 Require Import Crypto.Algebra. Import Group ScalarMult.
 Require Import Crypto.Util.Decidable Crypto.Util.Option Crypto.Util.Tactics.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil.
+Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.
 
 Module Import NotationsFor8485.
   Import NPeano Nat.
@@ -12,118 +15,173 @@ End NotationsFor8485.
 
 Section EdDSA.
   Context `{prm:EdDSA}.
-  Context {eq_dec:DecidableRel Eeq}.
-  Local Infix "==" := Eeq.
-  Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc).
-  Local Infix "*" := EscalarMult. Local Infix "+" := Eadd. Local Infix "++" := combine.
-  Local Notation "P - Q" := (P + Eopp Q).
-  Local Arguments H {_} _.
-
-  Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
-  Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}.
-  Context {Proper_Eadd : Proper (Eeq==>Eeq==>Eeq) Eadd}.
-
-  Context {decE:word b-> option E}.
-  Context {decS:word b-> option nat}.
-
-  Context {decE_canonical: forall x s, decE x = Some s -> x = Eenc s }.
-  Context {decS_canonical: forall x s, decS x = Some s -> x = Senc s }.
-
-  Context {decS_Senc: forall x, decS (Senc x) = Some x}.
-  Context {decE_Eenc: forall x, decE (Eenc x) = Some x}. (* FIXME: equivalence relation *)
-
-  Lemma solve_for_R : forall s B R n A, s * B == R + n * A <-> R == s*B - n*A.
-  Proof.
-    intros; split;
-      intro Heq; rewrite Heq; clear Heq.
-    { rewrite <-associative, right_inverse, right_identity; reflexivity. }
-    { rewrite <-associative, left_inverse, right_identity; reflexivity. }
-  Qed.
+  Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := EscalarMult.
 
-  Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
-    option_rect (fun _ => bool) (fun S : nat =>
-    option_rect (fun _ => bool) (fun A : E =>
-       weqb
-         (split1 b b sig)
-         (Eenc (S * B - (wordToNat (H (split1 b b sig ++ pk ++ message))) mod l * A))
-    ) false (decE pk)
-    ) false (decS (split2 b b sig))
-  .
-
-  Lemma verify_correct mlen (message:word mlen) (pk:word b) (sig:word (b+b)) :
-      verify message pk sig = true <-> valid message pk sig.
+  Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc).
+  Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
   Proof.
-    cbv [verify option_rect option_map].
-    split.
-    {
+    cbv [sign public Spec.EdDSA.valid]; intros; subst;
       repeat match goal with
-             | |- false = true -> _ => let H:=fresh "H" in intro H; discriminate H
-             | [H: _ |- _ ] => apply decS_canonical in H
-             | [H: _ |- _ ] => apply decE_canonical in H
-             | _ => rewrite weqb_true_iff
-             | _ => break_match
+             | |- exists _, _ => eexists
+             | |- _ /\ _ => eapply conj
+             | |- _ => reflexivity
              end.
-      intro.
-      subst.
-      rewrite <-combine_split.
-      rewrite Heqo.
-      rewrite H0.
-      constructor.
-      rewrite <-H0.
-      rewrite solve_for_R.
-      reflexivity.
-    }
-    {
-      intros [? ? ? ? Hvalid].
-      rewrite solve_for_R in Hvalid.
-      rewrite split1_combine.
-      rewrite split2_combine.
-      rewrite decS_Senc.
-      rewrite decE_Eenc.
-      rewrite weqb_true_iff.
-      f_equiv. exact Hvalid.
-    }
-  Qed.
-
-  Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
-  Proof.
-    cbv [sign public]. intros. subst. split.
-    rewrite scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, NPeano.Nat.mul_comm, scalarmult_assoc;
+    rewrite F.to_nat_of_nat, scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, NPeano.Nat.mul_comm, scalarmult_assoc;
       try solve [ reflexivity
-                | pose proof EdDSA_l_odd; omega
+                | setoid_rewrite (*unify 0*) (Z2Nat.inj_iff _ 0); pose proof EdDSA_l_odd; omega
+                                                                                                   | pose proof EdDSA_l_odd; omega
                 | apply EdDSA_l_order_B
                 | rewrite scalarmult_assoc, mult_comm, <-scalarmult_assoc,
                              EdDSA_l_order_B, scalarmult_zero_r; reflexivity ].
   Qed.
 
+  Lemma solve_for_R_sig : forall s B R n A, { solution | s * B == R + n * A <-> R == solution }.
+  Proof.
+    eexists.
+    set_evars.
+    setoid_rewrite <-(symmetry_iff(R:=Eeq)) at 1.
+    setoid_rewrite <-eq_r_opp_r_inv.
+    setoid_rewrite opp_mul.
+    subst_evars.
+    reflexivity.
+  Defined.
+  Definition solve_for_R := Eval cbv [proj2_sig solve_for_R_sig] in (fun s B R n A => proj2_sig (solve_for_R_sig s B R n A)).
+
+  Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
+  Global Instance Proper_eq_Eenc ref : Proper (Eeq ==> iff) (fun P => Eenc P = ref).
+  Proof. intros ? ? Hx; rewrite Hx; reflexivity. Qed.
+
+  Context {Edec:word b-> option E}   {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> Edec P_ = Some P}.
+  Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}.
+
+  Local Infix "++" := combine.
+  Definition verify_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)),
+      verify mlen message pk sig = true <-> valid message pk sig }.
+  Proof.
+    eexists; intros; set_evars.
+    unfold Spec.EdDSA.valid.
+    setoid_rewrite solve_for_R.
+    setoid_rewrite combine_eq_iff.
+    setoid_rewrite and_comm at 4. setoid_rewrite and_assoc. repeat setoid_rewrite exists_and_indep_l.
+    setoid_rewrite (and_rewrite_l Eenc (split1 b b sig)
+                            (fun x y => x == _ * B + wordToNat (H _ (y ++ Eenc _ ++ message)) mod _ * Eopp _)); setoid_rewrite eq_enc_S_iff.
+    setoid_rewrite (@exists_and_equiv_r _ _ _ _ _ _).
+    setoid_rewrite <- (fun A => and_rewriteleft_l (fun x => x) (Eenc A) (fun pk EencA => exists a,
+        Sdec (split2 b b sig) = Some a /\
+        Eenc (_ * B + wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message)) mod _ * Eopp A)
+        = split1 b b sig)); setoid_rewrite (eq_enc_E_iff pk).
+    setoid_rewrite <-weqb_true_iff.
+    repeat setoid_rewrite <-option_rect_false_returns_true_iff.
+
+    subst_evars.
+    (* TODO: generalize this higher order reflexivity *)
+    match goal with
+      |- ?f ?mlen ?msg ?pk ?sig = true <-> ?term = true
+      => let term := eval pattern sig in term in
+         let term := eval pattern pk in term in
+         let term := eval pattern msg in term in
+         let term := match term with
+                       (fun msg => (fun pk => (fun sig => @?body msg pk sig) sig) pk) msg =>
+                       body
+                     end in
+         let term := eval pattern mlen in term in
+         let term := match term with
+                       (fun mlen => @?body mlen) mlen => body
+                     end in
+         unify f term; reflexivity
+    end.
+  Defined.
+  Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
+    Eval cbv [proj1_sig verify_sig] in proj1_sig verify_sig mlen message pk sig.
+  Lemma verify_correct : forall {mlen} (message:word mlen) pk sig,
+    verify message pk sig = true <-> valid message pk sig.
+  Proof. exact (proj2_sig verify_sig). Qed.
+
   Section ChangeRep.
-    Context {A Aeq Aadd Aid Aopp} {Agroup:@group A Aeq Aadd Aid Aopp}.
-    Context {EtoA} {Ahomom:@is_homomorphism E Eeq Eadd A Aeq Aadd EtoA}.
+    Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@group Erep ErepEq ErepAdd ErepId ErepOpp}.
+    Context {EToRep} {Ahomom:@is_homomorphism E Eeq Eadd Erep ErepEq ErepAdd EToRep}.
+
+    Context {ERepEnc : Erep -> word b}
+            {ERepEnc_correct : forall P:E, Eenc P = ERepEnc (EToRep P)}
+            {Proper_ERepEnc:Proper (ErepEq==>Logic.eq) ERepEnc}.
 
-    Context {Aenc : A -> word b} {Proper_Aenc:Proper (Aeq==>Logic.eq) Aenc}
-            {Aenc_correct : forall P:E, Eenc P = Aenc (EtoA P)}.
+    Context {ERepDec : word b -> option Erep}
+            {ERepDec_correct : forall w, ERepDec w = option_map EToRep (Edec w) }.
 
-    Context {S Seq} `{@Equivalence S Seq} {natToS:nat->S}
-            {SAmul:S->A->A} {Proper_SAmul: Proper (Seq==>Aeq==>Aeq) SAmul}
-            {SAmul_correct: forall n P, Aeq (EtoA (n*P)) (SAmul (natToS n) (EtoA P))}
-            {SdecS} {SdecS_correct : forall w, (decS w) = (SdecS w)} (* FIXME: equivalence relation *)
-            {natToS_modl : forall n,  Seq (natToS (n mod l)) (natToS n)}.
+    Context {SRep SRepEq} `{@Equivalence SRep SRepEq} {S2Rep:F l->SRep}.
+
+    Context {SRepDecModL} {SRepDecModL_correct: forall (w:word (b+b)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModL w)}.
+
+    Context {SRepERepMul:SRep->Erep->Erep}
+            {SRepERepMul_correct:forall n P, ErepEq (EToRep (n*P)) (SRepERepMul (S2Rep (F.of_nat _ n)) (EToRep P))}
+            {Proper_SRepERepMul: Proper (SRepEq==>ErepEq==>ErepEq) SRepERepMul}.
+
+    Context {SRepDec: word b -> option SRep}
+            {SRepDec_correct : forall w, option_eq SRepEq (option_map S2Rep (Sdec w)) (SRepDec w)}.
 
     Definition verify_using_representation
                {mlen} (message:word mlen) (pk:word b) (sig:word (b+b))
                : { answer | answer = verify message pk sig }.
     Proof.
+      pose proof EdDSA_l_odd.
+      assert (l_pos:(0 < l)%Z) by omega.
       eexists.
       cbv [verify].
-      repeat (
-          setoid_rewrite Aenc_correct
-          || setoid_rewrite homomorphism
-          || setoid_rewrite homomorphism_id
-          || setoid_rewrite (homomorphism_inv(INV:=Eopp)(inv:=Aopp)(eq:=Aeq)(phi:=EtoA))
-          || setoid_rewrite SAmul_correct
-          || setoid_rewrite SdecS_correct
-          || setoid_rewrite natToS_modl
-        ).
+
+      etransitivity. Focus 2. {
+        eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
+        eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
+        repeat (
+            rewrite ERepEnc_correct
+            || rewrite homomorphism
+            || rewrite homomorphism_id
+            || rewrite (homomorphism_inv(INV:=Eopp)(inv:=ErepOpp)(eq:=ErepEq)(phi:=EToRep))
+            || rewrite SRepERepMul_correct
+            || rewrite SdecS_correct
+            || rewrite SRepDecModL_correct
+            || rewrite (@F.of_nat_to_nat _ l_pos _)
+            || rewrite (@F.of_nat_mod _ l_pos _)
+          ).
+        reflexivity.
+      } Unfocus.
+
+      (* lazymatch goal with |- _ _ (option_rect _ ?some _ _) => idtac some end. *)
+      setoid_rewrite (option_rect_option_map EToRep
+           (fun s =>
+            option_rect (fun _ : option _ => bool)
+              (fun s0 =>
+               weqb
+                 (ERepEnc
+                    (ErepAdd (SRepERepMul (_ s0) (EToRep B))
+                       (SRepERepMul
+                          (SRepDecModL
+                             (H _ (split1 b b sig ++ pk ++ message)))
+                          (ErepOpp (s))))) (split1 b b sig)) false
+              (Sdec (split2 b b sig)))
+                  false); rewrite <-(ERepDec_correct pk).
+
+      etransitivity. Focus 2. {
+        eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
+        set_evars.
+        setoid_rewrite (option_rect_option_map S2Rep
+            (fun s0 =>
+             weqb
+               (ERepEnc
+                  (ErepAdd (SRepERepMul (s0) (EToRep B))
+                     (SRepERepMul
+                        (SRepDecModL (H _ (split1 b b sig ++ pk ++ message)))
+                        (ErepOpp _)))) (split1 b b sig))
+            
+                   false).
+        subst_evars.
+
+        eapply Proper_option_rect_nd_changevalue;
+          [repeat intro; repeat f_equiv; eassumption|reflexivity|..].
+
+        symmetry.
+        eapply SRepDec_correct.
+      } Unfocus.
+
       reflexivity.
     Defined.
   End ChangeRep.