Merge branch 'master' of github.mit.edu:plv/fiat-crypto

7 files changed, 318 insertions, 92 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 7f4fe06cc..b1fdc69a3 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1,8 +1,14 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
 Require Import Crypto.Util.Tactics Crypto.Tactics.Nsatz.
 Require Import Crypto.Util.Decidable.
+Require Coq.Numbers.Natural.Peano.NPeano.
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
 
+Module Import ModuloCoq8485.
+  Import NPeano Nat.
+  Infix "mod" := modulo (at level 40, no associativity).
+End ModuloCoq8485.
+
 Notation is_eq_dec := (DecidableRel _) (only parsing).
 Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop))
                                   (at level 10, T at level 8, R at level 8, only parsing).
@@ -212,7 +218,7 @@ Module Group.
     Proof. eauto using Monoid.cancel_right, right_inverse. Qed.
     Lemma inv_inv x : inv(inv(x)) = x.
     Proof. eauto using Monoid.inv_inv, left_inverse. Qed.
-    Lemma inv_op x y : (inv y*inv x)*(x*y) =id.
+    Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id.
     Proof. eauto using Monoid.inv_op, left_inverse. Qed.
 
     Lemma inv_unique x ix : ix * x = id -> ix = inv x.
@@ -223,6 +229,14 @@ Module Group.
       - rewrite Hix, left_identity; reflexivity.
     Qed.
 
+    Lemma inv_op x y : inv (x*y) = inv y*inv x.
+    Proof.
+      symmetry. etransitivity.
+      2:eapply inv_unique.
+      2:eapply inv_op_ext.
+      reflexivity.
+    Qed.
+
     Lemma inv_id : inv id = id.
     Proof. symmetry. eapply inv_unique, left_identity. Qed.
 
@@ -329,6 +343,58 @@ Module Group.
         auto using associative, left_identity, right_identity, left_inverse, right_inverse.
     Qed.
   End GroupByHomomorphism.
+
+  Section ScalarMult.
+    Context {G eq add zero opp} `{@group G eq add zero opp}.
+    Context {mul:nat->G->G}.
+    Local Infix "=" := eq : type_scope. Local Infix "=" := eq.
+    Local Infix "+" := add. Local Infix "*" := mul.
+    Class is_scalarmult :=
+      {
+        scalarmult_0_l : forall P, 0 * P = zero;
+        scalarmult_S_l : forall n P, S n * P = P + n * P;
+
+        scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul
+      }.
+    Global Existing Instance scalarmult_Proper.
+    Context `{is_scalarmult}.
+
+    Lemma scalarmult_1_l : forall P, 1*P = P.
+    Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
+
+    Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
+    Proof.
+      induction n; intros;
+        rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
+    Qed.
+
+    Lemma scalarmult_zero_r : forall m, m * zero = zero.
+    Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
+
+    Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
+    Proof.
+      induction n; intros.
+      { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. }
+      { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. apply cancel_left, IHn. }
+    Qed.
+
+    Lemma opp_mul : forall n P, opp (n * P) = n * (opp P).
+      induction n; intros.
+      { rewrite !scalarmult_0_l, inv_id; reflexivity. }
+      { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1.
+        rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. }
+    Qed.
+
+    Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero.
+    Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed.
+
+    Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B.
+    Proof.
+      intros ? ? Hnz Hmod ?.
+      rewrite (NPeano.Nat.div_mod n l Hnz) at 2.
+      rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
+    Qed.
+  End ScalarMult.
 End Group.
 
 Require Coq.nsatz.Nsatz.
@@ -758,6 +824,21 @@ Ltac field_simplify_eq_hyps :=
 
 Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq.
 
+(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R] *)
+Ltac clear_algebraic_duplicates_step R :=
+  match goal with
+  | [ H : R ?x ?x |- _ ]
+    => clear H
+  end.
+Ltac clear_algebraic_duplicates_guarded R :=
+  let test_reflexive := constr:(_ : Reflexive R) in
+  repeat clear_algebraic_duplicates_step R.
+Ltac clear_algebraic_duplicates :=
+  clear_duplicates;
+  repeat match goal with
+         | [ H : ?R ?x ?x |- _ ] => clear_algebraic_duplicates_guarded R
+         end.
+
 (*** Inequalities over fields *)
 Ltac assert_expr_by_nsatz H ty :=
   let H' := fresh in
@@ -851,8 +932,62 @@ Section ExtraLemmas.
   Proof.
     intros; setoid_subst z; eauto using only_two_square_roots'.
   Qed.
+
+  Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y.
+  Proof.
+    intro H.
+    destruct (eq_dec x y); [ left; assumption | right ].
+    destruct (eq_dec x (opp y)); [ assumption | exfalso ].
+    eapply only_two_square_roots'; eassumption.
+  Qed.
+
+  Lemma only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y.
+  Proof.
+    intros; setoid_subst z; eauto using only_two_square_roots'_choice.
+  Qed.
 End ExtraLemmas.
 
+(** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *)
+Ltac pose_proof_only_two_square_roots x y H :=
+  not constr_eq x y;
+  match goal with
+  | [ H' : ?eq (?mul x x) (?mul y y) |- _ ]
+    => pose proof (only_two_square_roots'_choice x y H') as H
+  | [ H0 : ?eq (?mul x x) ?z, H1 : ?eq (?mul y y) ?z |- _ ]
+    => pose proof (only_two_square_roots_choice x y z H0 H1) as H
+  end.
+Ltac reduce_only_two_square_roots x y :=
+  let H := fresh in
+  pose_proof_only_two_square_roots x y H;
+  destruct H;
+  try setoid_subst y.
+Ltac pre_clean_only_two_square_roots :=
+  clear_algebraic_duplicates.
+(** Remove duplicates; solve goals by contradiction, and, if goals still remain, substitute the square roots *)
+Ltac post_clean_only_two_square_roots x y :=
+  clear_algebraic_duplicates;
+  try (unfold not in *;
+       match goal with
+       | [ H : (?T -> False)%type, H' : ?T |- _ ] => exfalso; apply H; exact H'
+       | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity
+       end);
+  try setoid_subst x; try setoid_subst y.
+Ltac only_two_square_roots_step :=
+  match goal with
+  | [ H : not (?eq ?x (?opp ?y)) |- _ ]
+    (* this one comes first, because it the procedure is asymmetric
+       with respect to [x] and [y], and this order is more likely to
+       lead to solving goals by contradiction. *)
+    => is_var x; is_var y; reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
+  | [ H : ?eq (?mul ?x ?x) (?mul ?y ?y) |- _ ]
+    => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
+  | [ H : ?eq (?mul ?x ?x) ?z, H' : ?eq (?mul ?y ?y) ?z |- _ ]
+    => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
+  end.
+Ltac only_two_square_roots :=
+  pre_clean_only_two_square_roots;
+  repeat only_two_square_roots_step.
+
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index e3809bb8a..0afc07c5d 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -138,25 +138,14 @@ Module E.
       match goal with | |- _ <> 0 => admit end.
     Admitted.
 
-    (* TODO: move to [Group] and [AbelianGroup] as appropriate *)
-    Lemma mul_0_l : forall P, (0 * P = zero)%E.
-    Proof. intros; reflexivity. Qed.
-    Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E.
-    Proof. intros; reflexivity. Qed.
-    Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E.
+    Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul.
     Proof.
-      induction n; intros;
-        rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
+      intros n m Hnm P Q HPQ. rewrite <-Hnm; clear Hnm m.
+      induction n; simpl; rewrite ?IHn, ?HPQ; reflexivity.
     Qed.
-    Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E.
-    Proof.
-      induction n; intros; [reflexivity|].
-      rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity.
-    Qed.
-    Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
-    Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed.
-    Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E.
-    Admitted.
+
+    Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul.
+    Proof. split; intros; reflexivity || typeclasses eauto. Qed.
 
     Section PointCompression.
       Local Notation "x ^ 2" := (x*x).
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index e5b74085e..c0b6be25b 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -150,63 +150,6 @@ Proof.
          end.
 Qed.
 
-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.
-
-Global Instance option_rect_Proper_nd' {A T}
-  : Proper ((pointwise_relation _ eq) ==> eq  ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)).
-Proof.
-  intros ?? H ??? [|]; subst; simpl; congruence.
-Qed.
-
-Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances.
-
-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).
-Proof.
-  destruct v; reflexivity.
-Qed.
-
-Lemma option_rect_function {A B C S' N' v} f
-  : f (option_rect (fun _ : option A => option B) S' N' v)
-    = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
-Proof. destruct v; reflexivity. Qed.
-Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *)
-  idtac;
-  lazymatch goal with
-  | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ]
-    => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *)
-    cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta;
-    [ set_evars;
-      let H := fresh in
-      intro H;
-      rewrite H;
-      clear;
-      abstract (cbv [Let_In]; reflexivity)
-    | ]
-  end.
-
-(** TODO: possibly move me, remove local *)
-Local Ltac replace_option_match_with_option_rect :=
-  idtac;
-  lazymatch goal with
-  | [ |- _ = ?RHS :> ?T ]
-    => lazymatch RHS with
-       | match ?a with None => ?N | Some x => @?S x end
-         => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity)
-       end
-  end.
-Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *)
-  repeat match goal with
-         | [ |- context[option_rect ?P ?S ?N None] ]
-           => change (option_rect P S N None) with N
-         | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
-           => change (option_rect P S N (Some x)) with (S x); cbv beta
-         end.
-
 Definition COMPILETIME {T} (x:T) : T := x.
 
 Lemma N_to_nat_le_mono : forall a b, (a <= b)%N -> (N.to_nat a <= N.to_nat b)%nat.
@@ -348,4 +291,4 @@ End with_unqualified_modulo2.
 Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y.
 Proof.
   split; eauto using F_eqb_eq, F_eqb_complete.
-Qed.
+Qed.
\ No newline at end of file
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
new file mode 100644
index 000000000..cf9083061
--- /dev/null
+++ b/src/Experiments/EdDSARefinement.v
@@ -0,0 +1,96 @@
+Require Import Crypto.Spec.EdDSA Bedrock.Word.
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Algebra. Import Group.
+Require Import Util.Decidable Util.Option Util.Tactics.
+Require Import Omega.
+
+Module Import NotationsFor8485.
+  Import NPeano Nat.
+  Infix "mod" := modulo (at level 40).
+End NotationsFor8485.
+
+Section EdDSA.
+  Context `{prm:EdDSA}.
+  Context {eq_dec:DecidableRel Eeq}.
+  Local Infix "==" := Eeq (at level 69, no associativity).
+  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).
+
+  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.
+
+  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 (b + (b + mlen)) (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.
+  Proof.
+    cbv [verify option_rect option_map].
+    split.
+    {
+      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
+             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;
+      try solve [ reflexivity
+                | 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.
+End EdDSA.
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index 4e30313d9..659a0ec66 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -149,11 +149,11 @@ Local Infix "*" := (E.mul(H0:=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 : l * B = zero.
-Axiom point_encoding : canonical encoding of point as word b.
-Axiom scalar_encoding : canonical encoding of {n : nat | n < l} as word b.
+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 point_encoding scalar_encoding :=
+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;
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index c28ff0482..03a723e10 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,4 +1,3 @@
-Require Import Crypto.Spec.Encoding.
 Require Bedrock.Word Crypto.Util.WordUtil.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
@@ -33,11 +32,12 @@ Section EdDSA.
 
         {B : E} (* base point *)
 
-        {PointEncoding : canonical encoding of E as Word.word b} (* wire format *)
-        {FlEncoding : canonical encoding of { n | n < l } as Word.word b}
+        {Eenc : E   -> Word.word b} (* normative encoding of elliptic cuve points *)
+        {Senc : nat -> Word.word b} (* normative encoding of scalars *)
     :=
       {
         EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
+        EdDSA_scalarmult:@Algebra.Group.is_scalarmult E Eeq Eadd Ezero EscalarMult;
 
         EdDSA_c_valid : c = 2 \/ c = 3;
 
@@ -48,13 +48,14 @@ Section EdDSA.
 
         EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
         EdDSA_l_odd : l > 2;
-        EdDSA_l_order_B : EscalarMult l B = Ezero
+        EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero
       }.
   Global Existing Instance EdDSA_group.
+  Global Existing Instance EdDSA_scalarmult.
 
   Context `{prm:EdDSA}.
 
-  Local Infix "=" := Eeq.
+  Local Infix "=" := Eeq : type_scope.
   Local Coercion Word.wordToNat : Word.word >-> nat.
   Local Notation secretkey := (Word.word b) (only parsing).
   Local Notation publickey := (Word.word b) (only parsing).
@@ -75,18 +76,18 @@ Section EdDSA.
   Local Infix "*" := EscalarMult.
 
   Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk).
-  Definition public (sk:secretkey) : publickey := enc (curveKey sk*B).
+  Definition public (sk:secretkey) : publickey := Eenc (curveKey sk*B).
 
   Program Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
     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 : {n|n<l} := exist _ ((r + H (enc R ++ public sk ++ M) * s) mod l) _ in
-        enc R ++ enc S.
+    let S : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l 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_lt_l,
-      S * B = R + (H (enc R ++ enc A ++ message) mod l) * A
-      -> valid message (enc A) (enc R ++ enc (exist _ S S_lt_l)).
-End EdDSA.
+    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).
+End EdDSA.
\ No newline at end of file
diff --git a/src/Util/Option.v b/src/Util/Option.v
new file mode 100644
index 000000000..db4b69dde
--- /dev/null
+++ b/src/Util/Option.v
@@ -0,0 +1,62 @@
+Require Import Coq.Classes.Morphisms.
+
+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.
+
+Global Instance option_rect_Proper_nd' {A T}
+  : Proper ((pointwise_relation _ eq) ==> eq  ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)).
+Proof.
+  intros ?? H ??? [|]; subst; simpl; congruence.
+Qed.
+
+Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances.
+
+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).
+Proof.
+  destruct v; reflexivity.
+Qed.
+
+Lemma option_rect_function {A B C S' N' v} f
+  : f (option_rect (fun _ : option A => option B) S' N' v)
+    = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
+Proof. destruct v; reflexivity. Qed.
+
+(*
+Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *)
+  idtac;
+  lazymatch goal with
+  | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ]
+    => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *)
+    cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta;
+    [ set_evars;
+      let H := fresh in
+      intro H;
+      rewrite H;
+      clear;
+      abstract (cbv [Let_In]; reflexivity)
+    | ]
+  end.
+*)
+
+(** TODO: possibly move me, remove local *)
+Ltac replace_option_match_with_option_rect :=
+  idtac;
+  lazymatch goal with
+  | [ |- _ = ?RHS :> ?T ]
+    => lazymatch RHS with
+       | match ?a with None => ?N | Some x => @?S x end
+         => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity)
+       end
+  end.
+
+Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *)
+  repeat match goal with
+         | [ |- context[option_rect ?P ?S ?N None] ]
+           => change (option_rect P S N None) with N
+         | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
+           => change (option_rect P S N (Some x)) with (S x); cbv beta
+         end.