Derive EdDSA.verify from equational specification

Experiments/SpecEd25519 will come back soon

9 files changed, 254 insertions, 272 deletions

diff --git a/_CoqProject b/_CoqProject
index d87842e49..797f2a12c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -38,8 +38,6 @@ src/Encoding/PointEncodingPre.v
 src/Experiments/DerivationsOptionRectLetInEncoding.v
 src/Experiments/EdDSARefinement.v
 src/Experiments/GenericFieldPow.v
-src/Experiments/SpecEd25519.v
-src/Experiments/SpecificCurve25519.v
 src/ModularArithmetic/ExtPow2BaseMulProofs.v
 src/ModularArithmetic/ExtendedBaseVector.v
 src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -102,12 +100,14 @@ src/Util/HProp.v
 src/Util/Isomorphism.v
 src/Util/IterAssocOp.v
 src/Util/ListUtil.v
+src/Util/Logic.v
 src/Util/NatUtil.v
 src/Util/Notations.v
 src/Util/NumTheoryUtil.v
 src/Util/Option.v
 src/Util/PointedProp.v
 src/Util/Prod.v
+src/Util/Relations.v
 src/Util/Sigma.v
 src/Util/Sum.v
 src/Util/Tactics.v
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
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 38dc64cef..2971bfef8 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -3,6 +3,10 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
+Require Import Omega. (* TODO: remove this import when we drop 8.4 *)
+
+Require Import Crypto.Spec.ModularArithmetic.
+
 (** In Coq 8.4, we have [NPeano.pow] and [NPeano.modulo].  In Coq 8.5,
     they are [Nat.pow] and [Nat.modulo].  To allow this file to work
     with both versions, we create a module where we (locally) import
@@ -28,12 +32,12 @@ Section EdDSA.
         {H : forall {n}, Word.word n -> Word.word (b + b)} (* main hash function *)
         {c : nat} (* cofactor E = 2^c *)
         {n : nat} (* secret keys are (n+1) bits *)
-        {l : nat} (* order of the subgroup of E generated by B *)
+        {l : BinInt.Z} (* order of the subgroup of E generated by B *)
 
         {B : E} (* base point *)
 
         {Eenc : E   -> Word.word b} (* normative encoding of elliptic cuve points *)
-        {Senc : nat -> Word.word b} (* normative encoding of scalars *)
+        {Senc : F l -> Word.word b} (* normative encoding of scalars *)
     :=
       {
         EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
@@ -44,19 +48,19 @@ Section EdDSA.
         EdDSA_n_ge_c : n >= c;
         EdDSA_n_le_b : n <= b;
 
-        EdDSA_B_not_identity : B <> Ezero;
+        EdDSA_B_not_identity : not (Eeq B Ezero);
 
-        EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
-        EdDSA_l_odd : l > 2;
-        EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero
+        EdDSA_l_prime : Znumtheory.prime l;
+        EdDSA_l_odd : BinInt.Z.lt 2 l;
+        EdDSA_l_order_B : Eeq (EscalarMult (BinInt.Z.to_nat l) B) Ezero
       }.
   Global Existing Instance EdDSA_group.
   Global Existing Instance EdDSA_scalarmult.
 
   Context `{prm:EdDSA}.
 
-  Local Infix "=" := Eeq : type_scope.
   Local Coercion Word.wordToNat : Word.word >-> nat.
+  Local Coercion BinInt.Z.to_nat : BinInt.Z >-> nat.
   Local Notation secretkey := (Word.word b) (only parsing).
   Local Notation publickey := (Word.word b) (only parsing).
   Local Notation signature := (Word.word (b + b)) (only parsing).
@@ -64,8 +68,7 @@ Section EdDSA.
   Local Arguments H {n} _.
   Local Notation wfirstn n w := (@WordUtil.wfirstn n _ w _) (only parsing).
 
-  Require Import Coq.omega.Omega.
-  Obligation Tactic := simpl; intros; try apply NPeano.Nat.mod_upper_bound; destruct prm; omega.
+  Local Obligation Tactic := destruct prm; simpl; intros; omega.
 
   Program Definition curveKey (sk:secretkey) : nat :=
     let x := wfirstn n (H sk) in (* hash the key, use first "half" for secret scalar *)
@@ -82,12 +85,10 @@ Section EdDSA.
     let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
     let R : E := r * B in (* commitment to nonce *)
     let s : nat := curveKey sk in (* secret scalar *)
-    let S : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l in
+    let S : F l := F.nat_mod l (r + H (Eenc R ++ A_ ++ M) * s) in
         Eenc R ++ Senc S.
 
-  (* For a [n]-bit [message] from public key [A_], validity of a signature [R_ ++ S_] *)
-  Inductive valid {n:nat} : Word.word n -> publickey -> signature -> Prop :=
-    ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat),
-      S * B = R + (H (Eenc R ++ Eenc A ++ message) mod l) * A
-      -> valid message (Eenc A) (Eenc R ++ Senc S).
+  Definition valid {n} (message : Word.word n) pubkey signature :=
+    exists A S R, Eenc A = pubkey /\ Eenc R ++ Senc S = signature /\
+                  Eeq (F.to_nat S * B) (R + (H (Eenc R ++ Eenc A ++ message) mod l) * A).
 End EdDSA.
diff --git a/src/Util/Logic.v b/src/Util/Logic.v
new file mode 100644
index 000000000..d518069a9
--- /dev/null
+++ b/src/Util/Logic.v
@@ -0,0 +1,19 @@
+Require Import Crypto.Util.FixCoqMistakes.
+
+(* WHY does this solve goals that [intuition] does not solve? *)
+Ltac logic :=
+  repeat match goal with
+         | |- _ => intro
+         | H:exists _, _ |- _ => destruct H
+         | H:_ /\ _ |- _ => destruct H
+         | |- _ => solve [eauto]
+         | |- _ => split
+         end.
+
+Lemma exists_and_indep_l {A B} P Q :
+  (exists a b, P a /\ Q a b) <-> (exists a:A, P a /\ exists b:B, Q a b).
+Proof. logic. Qed.
+
+Lemma exists_and_indep_r {A B} P Q :
+  (exists a b, Q a b /\ P a) <-> (exists a:A, P a /\ exists b:B, Q a b).
+Proof. logic. Qed.
diff --git a/src/Util/Option.v b/src/Util/Option.v
index df922f8c1..98e172ad4 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -1,18 +1,42 @@
 Require Import Coq.Classes.Morphisms.
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.Logic.
 
-Global Instance option_rect_Proper_nd {A T}
-  : Proper ((pointwise_relation _ eq) ==> eq  ==> eq ==> eq) (@option_rect A (fun _ => T)).
-Proof.
-  intros ?? H ??? [|]??; subst; simpl; congruence.
-Qed.
+Definition option_eq {A} eq (x y : option A) :=
+  match x with
+  | None    => y = None
+  | Some ax => match y with
+               | None => False
+               | Some ay => eq ax ay
+               end
+  end.
 
-Global Instance option_rect_Proper_nd' {A T}
-  : Proper ((pointwise_relation _ eq) ==> eq  ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)).
+Global Instance Equivalence_option_eq {T} {R} {Equivalence_R:@Equivalence T R}
+  : Equivalence (option_eq R).
 Proof.
-  intros ?? H ??? [|]; subst; simpl; congruence.
+  split; cbv; repeat (break_match || intro || intuition congruence ||
+                      solve [ reflexivity | symmetry; eassumption | etransitivity; eassumption ] ).
 Qed.
 
-Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances.
+
+Global Instance Proper_option_rect_nd_changebody
+      {A B:Type} {RB:relation B} {a:option A}
+  : Proper (pointwise_relation _ RB ==> RB ==> RB) (fun S N => option_rect (fun _ => B) S N a).
+Proof. cbv; repeat (intro || break_match); intuition. Qed.
+
+(* FIXME: there used to be a typeclass resolution hint here, something like
+  Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?B))) => exact (@Proper_option_rect_nd_changebody A B _ _) : typeclass_instances.
+ but I could not get it working after generalizing [RB] from [Logic.eq] ~ andreser *)
+
+Global Instance Proper_option_rect_nd_changevalue
+      {A B RA RB} some {Proper_some: Proper (RA==>RB) some}
+  : Proper (RB ==> option_eq RA ==> RB) (@option_rect A (fun _ => B) some).
+Proof. cbv; repeat (intro || break_match || f_equiv || intuition congruence). Qed.
+
+Lemma option_rect_false_returns_true_iff {T} (f:T->bool) (o:option T) :
+  option_rect (fun _ => bool) f false o = true <-> exists s:T, o = Some s /\ f s = true.
+Proof. unfold option_rect; break_match; logic; congruence. Qed.
 
 Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v,
     option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v).
@@ -42,7 +66,6 @@ Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect p
   end.
 *)
 
-(** TODO: possibly move me, remove local *)
 Ltac replace_option_match_with_option_rect :=
   idtac;
   lazymatch goal with
@@ -61,15 +84,6 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect
            => change (option_rect P S N (Some x)) with (S x); cbv beta
          end.
 
-Definition option_eq {A} eq (x y : option A) :=
-  match x with
-  | None    => y = None
-  | Some ax => match y with
-               | None => False
-               | Some ay => eq ax ay
-               end
-  end.
-
 Definition option_leq_to_eq {A} (x y : option A) : x = y -> option_eq eq x y.
 Proof. destruct x; intro; subst; simpl; reflexivity. Qed.
 
diff --git a/src/Util/Relations.v b/src/Util/Relations.v
new file mode 100644
index 000000000..aa280db26
--- /dev/null
+++ b/src/Util/Relations.v
@@ -0,0 +1,29 @@
+Require Import Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Logic.
+Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
+
+Lemma symmetry_iff {T} {R} {Rsym:@Symmetric T R} x y: R x y <-> R y x.
+  intuition eauto using symmetry.
+Qed.
+
+Lemma and_rewrite_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB}
+      (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a
+  : (RB (f a) ref /\ P a (f a)) <-> (RB (f a) ref /\ P a ref).
+Proof.
+  logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end.
+Qed.
+
+Lemma and_rewriteleft_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB}
+      (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a
+  : (RB ref (f a) /\ P a (f a)) <-> (RB ref (f a) /\ P a ref).
+Proof.
+  logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end.
+Qed.
+
+Lemma exists_and_equiv_r {A} {RA} {Equivalence_RA:Equivalence RA}
+      P {Proper_P: Proper (RA==>iff) P} (ref:A)
+  : (exists a, P a /\ RA a ref) <-> P ref.
+Proof.
+  logic; try match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end.
+  repeat (assumption||reflexivity||econstructor); assumption. (* WHY the last [assumption]?*)
+Qed.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 6a8831b14..9e88c1731 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -59,3 +59,7 @@ Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
   refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
                             | eq_refl => w
                             end)); abstract omega. Defined.
+
+Lemma combine_eq_iff {a b} (A:word a) (B:word b) C :
+  combine A B = C <-> A = split1 a b C /\ B = split2 a b C.
+Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed.