Derive EdDSA.verify from equational specification

Experiments/SpecEd25519 will come back soon

3 files changed, 151 insertions, 236 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.
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
deleted file mode 100644
index 692254512..000000000
--- a/src/Experiments/SpecEd25519.v
+++ /dev/null
@@ -1,126 +0,0 @@
-Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
-Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
-Require Import Crypto.Spec.ModularWordEncoding.
-Require Import Crypto.Encoding.ModularWordEncodingTheorems.
-Require Import Crypto.Spec.EdDSA.
-Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
-Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil.
-Require Import Bedrock.Word.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Coq.Logic.Decidable Crypto.Util.Decidable.
-Require Import Coq.omega.Omega.
-
-(* TODO: move to PrimeFieldTheorems *)
-Lemma minus1_is_square {q} : prime q -> (q mod 4)%Z = 1%Z -> (exists y, y*y = F.opp (F.of_Z q 1))%F.
-  intros; pose proof prime_ge_2 q _.
-  rewrite F.square_iff.
-  destruct (minus1_square_1mod4 q) as [b b_id]; trivial; exists b.
-  rewrite b_id, F.to_Z_opp, F.to_Z_of_Z, Z.mod_opp_l_nz, !Zmod_small;
-    (repeat (omega || rewrite Zmod_small)).
-Qed.
-
-Definition q : Z := (2 ^ 255 - 19)%Z.
-Global Instance prime_q : prime q. Admitted.
-Lemma two_lt_q : (2 < q)%Z. Proof. reflexivity. Qed.
-Lemma char_gt_2 : (1 + 1 <> (0:F q))%F. vm_decide_no_check. Qed.
-
-Definition a : F q := F.opp 1%F.
-Lemma nonzero_a : a <> 0%F. Proof. vm_decide_no_check. Qed.
-Lemma square_a : exists b, (b*b=a)%F.
-Proof. pose (@F.Decidable_square q _ two_lt_q a); vm_decide_no_check. Qed.
-Definition d : F q := (F.opp (F.of_Z _ 121665) / (F.of_Z _ 121666))%F.
-
-Lemma nonsquare_d : forall x, (x*x <> d)%F.
-Proof. pose (@F.Decidable_square q _ two_lt_q d). vm_decide_no_check. Qed.
-
-Instance curve25519params : @E.twisted_edwards_params (F q) eq 0%F 1%F F.add F.mul a d :=
-  {
-    nonzero_a := nonzero_a;
-    char_gt_2 := char_gt_2;
-    square_a := square_a;
-    nonsquare_d := nonsquare_d
-  }.
-
-Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = (2 ^ n)%nat.
-Admitted.
-
-Definition b := 256%nat.
-Lemma b_valid : (2 ^ (b - 1) > Z.to_nat q)%nat.
-Proof.
-  unfold q, gt.
-  replace (2 ^ (b - 1))%nat with (Z.to_nat (2 ^ (Z.of_nat (b - 1))))
-    by (rewrite <- two_power_nat_equiv; apply two_power_nat_Z2Nat).
-  rewrite <- Z2Nat.inj_lt; compute; congruence.
-Qed.
-
-Definition c := 3%nat.
-Lemma c_valid : (c = 2 \/ c = 3)%nat.
-Proof.
-  right; auto.
-Qed.
-
-Definition n := (b - 2)%nat.
-Lemma n_ge_c : (n >= c)%nat.
-Proof.
-  unfold n, c, b; omega.
-Qed.
-Lemma n_le_b : (n <= b)%nat.
-Proof.
-  unfold n, b; omega.
-Qed.
-
-Definition l : nat := Z.to_nat (252 + 27742317777372353535851937790883648493)%Z.
-Lemma prime_l : prime (Z.of_nat l). Admitted.
-Lemma l_odd : (l > 2)%nat.
-Proof.
-  unfold l, proj1_sig.
-  rewrite Z2Nat.inj_add; try omega.
-  apply lt_plus_trans.
-  compute; omega.
-Qed.
-
-Require Import Crypto.Spec.Encoding.
-
-Lemma q_pos : (0 < q)%Z. pose proof prime_ge_2 q _; omega. Qed.
-Definition FqEncoding : canonical encoding of (F q) as word (b-1) :=
-  @modular_word_encoding q (b - 1) q_pos b_valid.
-
-Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed.
-Lemma l_bound : (Z.to_nat (Z.of_nat l) < 2 ^ b)%nat.
-Proof.
-  rewrite Nat2Z.id.
-  rewrite <- pow2_id.
-  rewrite Zpow_pow2.
-  unfold l.
-  apply Z2Nat.inj_lt; compute; congruence.
-Qed.
-Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b :=
-  @modular_word_encoding (Z.of_nat l) b l_pos l_bound.
-
-Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed.
-
-Lemma sqrt_minus1_valid : ((F.of_Z q 2 ^ Z.to_N (q / 4)) ^ 2 = F.opp 1)%F.
-Proof. vm_decide_no_check. Qed.
-
-Local Notation point := (@E.point (F q) eq 1%F F.add F.mul a d).
-Local Notation zero := (E.zero(field:=F.field_modulo q)).
-Local Notation add := (E.add(H:=curve25519params)).
-Local Infix "*" := (E.mul(H:=curve25519params)).
-Axiom H : forall n : nat, word n -> word (b + b).
-Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *)
-Axiom B_nonzero : B <> zero.
-Axiom l_order_B : E.eq (l * B) zero.
-Axiom Eenc : point -> word b.
-Axiom Senc : nat -> word b.
-
-Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B Eenc Senc :=
-  {
-    EdDSA_c_valid := c_valid;
-    EdDSA_n_ge_c := n_ge_c;
-    EdDSA_n_le_b := n_le_b;
-    EdDSA_B_not_identity := B_nonzero;
-    EdDSA_l_prime := prime_l;
-    EdDSA_l_odd := l_odd;
-    EdDSA_l_order_B := l_order_B
-  }.
diff --git a/src/Experiments/SpecificCurve25519.v b/src/Experiments/SpecificCurve25519.v
deleted file mode 100644
index 15752b2a2..000000000
--- a/src/Experiments/SpecificCurve25519.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Crypto.Util.Notations Coq.ZArith.BinInt.
-Require Import Crypto.Spec.ModularArithmetic.
-Require Import Crypto.Specific.GF25519.
-Require Import Crypto.Experiments.SpecEd25519.
-Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
-Local Infix "<<" := Z.shiftr.
-Local Infix "&" := Z.land.
-
-Section Curve25519.
-
-  Definition twice_d : fe25519 := Eval vm_compute in
-    @ModularBaseSystem.encode modulus params25519 (d + d)%F.
-
-  Definition ge25519_add :=
-    Eval cbv beta delta [Extended.add_coordinates fe25519 add mul sub ModularBaseSystemOpt.Let_In] in
-      @Extended.add_coordinates fe25519 add sub mul twice_d.
-End Curve25519.
\ No newline at end of file