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

6 files changed, 396 insertions, 152 deletions

diff --git a/_CoqProject b/_CoqProject
index 9e1717dd5..b3819871e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,8 +15,8 @@ src/ModularArithmetic/ModularBaseSystem.v
 src/ModularArithmetic/ModularBaseSystemProofs.v
 src/ModularArithmetic/Pre.v
 src/ModularArithmetic/PrimeFieldTheorems.v
-src/ModularArithmetic/PseudoMersenneBaseParams.v
 src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+src/ModularArithmetic/PseudoMersenneBaseParams.v
 src/ModularArithmetic/PseudoMersenneBaseRep.v
 src/ModularArithmetic/Tutorial.v
 src/Spec/CompleteEdwardsCurve.v
@@ -34,5 +34,6 @@ src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v
 src/Util/NumTheoryUtil.v
+src/Util/Tactics.v
 src/Util/WordUtil.v
 src/Util/ZUtil.v
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 3740f5a29..6ea5ec283 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -57,8 +57,26 @@ Section CompleteEdwardsCurveTheorems.
   Proof.
     (* The Ltac takes ~15s, the Qed no longer takes longer than I have had patience for *)
     Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz);
-      repeat split; match goal with [ |- _ = 0%F -> False ] => admit end;
-        fail "unreachable".
+      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
+      pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
+      cbv beta iota in *;
+      repeat split.
+    { field_nonzero idtac. }
+    { field_nonzero idtac. }
+    2: field_nonzero idtac.
+    2: field_nonzero idtac.
+    3: field_nonzero idtac.
+    3: field_nonzero idtac.
+    4: field_nonzero idtac.
+    4: field_nonzero idtac.
+    4:field_nonzero idtac.
+    3:field_nonzero idtac.
+    2:field_nonzero idtac.
+    1:field_nonzero idtac.
+    admit.
+    admit.
+    admit.
+    admit.
   Qed.
 
   Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 976fe59c1..a9fbf5e40 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -3,7 +3,7 @@ Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.FField.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Util.IterAssocOp BinNat NArith. 
+Require Import Util.IterAssocOp BinNat NArith.
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
 Local Open Scope equiv_scope.
 Local Open Scope F_scope.
@@ -19,10 +19,10 @@ Section ExtendedCoordinates.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Add Field Ffield_notConstant : (OpaqueFieldTheory q)
-    (constants [notConstant]). 
+    (constants [notConstant]).
 
   (** [extended] represents a point on an elliptic curve using extended projective
   * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
@@ -44,8 +44,8 @@ Section ExtendedCoordinates.
   Local Hint Unfold twistedToExtended extendedToTwisted rep.
   Local Notation "P '~=' rP" := (rep P rP) (at level 70).
 
-  Ltac unfoldExtended := 
-    repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros); 
+  Ltac unfoldExtended :=
+    repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros);
     repeat match goal with
       | [ p : (F q*F q)%type |- _ ] =>
           let x := fresh "x" p in
@@ -61,7 +61,7 @@ Section ExtendedCoordinates.
       | [ H: @eq (F q * F q)%type _ _ |- _ ] => invcs H
       | [ H: @eq F q ?x _ |- _ ] => isVar x; rewrite H; clear H
   end.
-  
+
   Ltac solveExtended := unfoldExtended;
     repeat match goal with
       | [ |- _ /\ _ ] => split
@@ -137,6 +137,8 @@ Section ExtendedCoordinates.
       (X3, Y3, Z3, T3).
     Local Hint Unfold unifiedAdd.
 
+    Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q).
+
     Lemma unifiedAddM1'_rep: forall P Q rP rQ, onCurve rP -> onCurve rQ ->
       P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (unifiedAdd' rP rQ).
     Proof.
@@ -146,31 +148,8 @@ Section ExtendedCoordinates.
       unfoldExtended; rewrite a_eq_minus1 in *; simpl in *.
         repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto;
         repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
-           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r.
-
-    Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q).
-    (* If we we had reasoning modulo associativity and commutativity,
-    *  the following tactic would probably solve all remaining goals here:
-    repeat match goal with [H1: @eq (F p) _ _, H2: @eq (F p) _ _ |- _ ] =>
-      let H := fresh "H" in ( 
-        pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H;
-        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
-      ) || (
-        pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H;
-        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
-      ); tnz
-    end. *)
-
-      - replace (ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-        replace (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r;
+        field_nonzero tnz.
     Qed.
 
     Lemma unifiedAdd'_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (unifiedAdd' P Q).
@@ -238,4 +217,4 @@ Section ExtendedCoordinates.
 
   End TwistMinus1.
 
-End ExtendedCoordinates.
\ No newline at end of file
+End ExtendedCoordinates.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 77d84c455..130f85c84 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -9,6 +9,7 @@ Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
 Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.
 
 Existing Class prime.
 
@@ -67,7 +68,7 @@ Module FieldModulo (Import M : PrimeModulus).
      postprocess [Fpostprocess],
      constants [Fconstant],
      div morph_div_theory_modulo,
-     power_tac power_theory_modulo [Fexp_tac]). 
+     power_tac power_theory_modulo [Fexp_tac]).
 End FieldModulo.
 
 Section VariousModPrime.
@@ -79,8 +80,8 @@ Section VariousModPrime.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
-  
+     power_tac (@Fpower_theory q) [Fexp_tac]).
+
   Lemma Fq_mul_eq : forall x y z : F q, z <> 0 -> x * z = y * z -> x = y.
   Proof.
     intros ? ? ? z_nonzero mul_z_eq.
@@ -139,27 +140,27 @@ Section VariousModPrime.
       apply ZToField_eqmod.
       demod; reflexivity.
   Qed.
- 
+
   Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0.
     intros.
     assert (Z := F_eq_dec a 0); destruct Z.
-  
+
     - left; intuition.
-  
+
     - assert (a * b / a = 0) by
         ( rewrite H; field; intuition ).
-  
+
       replace (a*b/a) with (b) in H0 by (field; trivial).
       right; intuition.
   Qed.
-  
+
   Lemma Fq_mul_nonzero_nonzero : forall a b : F q, a <> 0 -> b <> 0 -> a*b <> 0.
     intros; intuition; subst.
     apply Fq_mul_zero_why in H1.
     destruct H1; subst; intuition.
   Qed.
   Hint Resolve Fq_mul_nonzero_nonzero.
-  
+
   Lemma Fq_pow_zero : forall (p: N), p <> 0%N -> (0^p = @ZToField q 0)%F.
     induction p using N.peano_ind;
     rewrite <-?N.add_1_l, ?(proj2 (@F_pow_spec q _) _), ?(proj1 (@F_pow_spec q _)).
@@ -232,7 +233,7 @@ Section VariousModPrime.
       left.
       eapply Fq_square_mul; eauto.
       instantiate (1 := x).
-      assert (x ^ 2 = z * y ^ 2 - x ^ 2 + x ^ 2) as plus_minus_x2 by 
+      assert (x ^ 2 = z * y ^ 2 - x ^ 2 + x ^ 2) as plus_minus_x2 by
         (rewrite <- eq_zero_sub; ring).
       rewrite plus_minus_x2; ring.
     }
@@ -352,6 +353,22 @@ Section VariousModPrime.
   Proof.
     econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0.
   Qed.
+
+  Lemma add_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q)
+    : x * y + z = (x + (z * (inv y))) * y.
+  Proof. field. Qed.
+
+  Lemma sub_cancel_mul_r_nonzero {y : F q} (H : y <> 0) (x z : F q)
+    : x * y - z = (x - (z * (inv y))) * y.
+  Proof. field. Qed.
+
+  Lemma add_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q)
+    : y + z = (1 + (z * (inv y))) * y.
+  Proof. field. Qed.
+
+  Lemma sub_cancel_l_nonzero {y : F q} (H : y <> 0) (z : F q)
+    : y - z = (1 - (z * (inv y))) * y.
+  Proof. field. Qed.
 End VariousModPrime.
 
 Section SquareRootsPrime5Mod8.
@@ -367,7 +384,7 @@ Section SquareRootsPrime5Mod8.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   (* This is only the square root of -1 if q mod 8 is 3 or 5 *)
   Definition sqrt_minus1 : F q :=  ZToField 2 ^ Z.to_N (q / 4).
@@ -382,7 +399,7 @@ Section SquareRootsPrime5Mod8.
   Qed.
 
   (* square root mod q relies on the fact that q is 5 mod 8 *)
-  Definition sqrt_mod_q (a : F q) := 
+  Definition sqrt_mod_q (a : F q) :=
     let b := a ^ Z.to_N (q / 8 + 1) in
     (match (F_eq_dec (b ^ 2) a) with
     | left A => b
@@ -445,4 +462,47 @@ Section SquareRootsPrime5Mod8.
     field.
   Qed.
 
-End SquareRootsPrime5Mod8.
\ No newline at end of file
+End SquareRootsPrime5Mod8.
+
+Local Open Scope F_scope.
+(** Tactics for solving inequalities. *)
+Ltac solve_cancel_by_field y tnz :=
+  solve [ generalize dependent y; intros;
+          field; tnz ].
+
+Ltac cancel_nonzero_factors' tnz :=
+  idtac;
+  match goal with
+  | [ |- ?x = 0 -> False ]
+    => change (x <> 0)
+  | [ |- ?x * ?y <> 0 ]
+    => apply Fq_mul_nonzero_nonzero
+  | [ H : ?y <> 0 |- _ ]
+    => progress rewrite ?(add_cancel_mul_r_nonzero H), ?(sub_cancel_mul_r_nonzero H), ?(add_cancel_l_nonzero H), ?(sub_cancel_l_nonzero H);
+       apply Fq_mul_nonzero_nonzero; [ | assumption ]
+  | [ |- ?op (?y * (ZToField (m := ?q) ?n)) ?z <> 0 ]
+    => unique assert (ZToField (m := q) n <> 0) by tnz;
+       generalize dependent (ZToField (m := q) n); intros
+  | [ |- ?op (?x * (?y * ?z)) _ <> 0 ]
+    => rewrite F_mul_assoc
+  end.
+Ltac cancel_nonzero_factors tnz := repeat cancel_nonzero_factors' tnz.
+Ltac specialize_quantified_equalities :=
+  repeat match goal with
+         | [ H : forall _ _ _ _, _ = _ -> _, H' : _ = _ |- _ ]
+           => unique pose proof (fun x2 y2 => H _ _ x2 y2 H')
+         | [ H : forall _ _, _ = _ -> _, H' : _ = _ |- _ ]
+           => unique pose proof (H _ _ H')
+         end.
+Ltac finish_inequality tnz :=
+  idtac;
+  match goal with
+  | [ H : ?x <> 0 |- ?y <> 0 ]
+    => replace y with x by (field; tnz); exact H
+  end.
+Ltac field_nonzero tnz :=
+  cancel_nonzero_factors tnz;
+  try (specialize_quantified_equalities;
+       progress cancel_nonzero_factors tnz);
+  try solve [ specialize_quantified_equalities;
+              finish_inequality tnz ].
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index f98bf2d12..50379b8d1 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -60,8 +60,9 @@ Qed.
 Axiom point_eqb : forall {prm : TwistedEdwardsParams}, point -> point -> bool.
 Axiom point_eqb_correct : forall P Q, point_eqb P Q = if point_eq_dec P Q then true else false.
 
-Axiom Bc : F q * F q.
-Axiom B_proj : proj1_sig B = Bc.
+Axiom xB : F q.
+Axiom yB : F q.
+Axiom B_proj : proj1_sig B = (xB, yB).
 
 Require Import Coq.Setoids.Setoid.
 Require Import Coq.Classes.Morphisms.
@@ -92,18 +93,36 @@ Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F
 Local Infix "==?" := point_eqb (at level 70) : E_scope.
 Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope.
 
-Axiom negate : point -> point.
+Axiom square_opp : forall (x:F q), (opp x ^ 2 = x ^ 2)%F.
+
+Program Definition negate (P:point) : point := let '(x, y) := proj1_sig P in (opp x, y).
+Next Obligation.
+Proof.
+  pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H.
+  rewrite square_opp; trivial.
+Qed.
+
 Definition point_sub P Q := (P + negate Q)%E.
 Infix "-" := point_sub : E_scope.
 Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E.
 
-Axiom negateExtendedc : extended -> extended.
-Definition negateExtended : extendedPoint -> extendedPoint.
+Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T).
+Local Notation "2" := (ZToField 2) : F_scope.
+
+Lemma mul_opp_1 : forall x y : F q, (opp x * y = opp (x * y))%F.
+Admitted.
+
+Lemma div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F.
+Admitted.
+
+Definition negateExtended' P := let '(X, Y, Z, T) := P in (opp X, Y, Z, opp T).
+Program Definition negateExtended (P:extendedPoint) : extendedPoint := negateExtended' (proj1_sig P).
+Next Obligation.
 Proof.
-  intro x.
-  exists (negateExtendedc (proj1_sig x)).
-  admit.
-Defined.
+  unfold negateExtended', rep; destruct P as [[X Y Z T] H]; simpl. destruct H as [[[] []] ?]; subst.
+  repeat rewrite ?div_opp_1, ?mul_opp_1, ?square_opp; repeat split; trivial.
+Qed.
+
 Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P).
 
 Local Existing Instance PointEncoding.
@@ -132,6 +151,105 @@ Defined.
 Definition enc'_correct : @enc (@point curve25519params) _ _ = (fun x => enc' (proj1_sig x))
   := eq_refl.
 
+    Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+    Global Instance Let_In_Proper_nd {A P}
+      : Proper (eq ==> pointwise_relation _ eq ==> eq) (@Let_In A (fun _ => P)).
+    Proof.
+      lazy; intros; congruence.
+    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. 
+    Local Ltac replace_let_in_with_Let_In :=
+      repeat match goal with
+             | [ |- context G[let x := ?y in @?z x] ]
+               => let G' := context G[Let_In y z] in change G'
+             | [ |- _ = Let_In _ _ ]
+               => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ]
+             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.
+
+Axiom SRep : Type.
+Axiom S2rep : N -> SRep.
+Axiom rep2S : SRep -> N.
+Axiom rep2S_S2rep : forall x, x = rep2S (S2rep x).
+
+Axiom FRep : Type.
+Axiom F2rep : F Ed25519.q -> FRep.
+Axiom rep2F : FRep -> F Ed25519.q.
+Axiom rep2F_F2rep : forall x, x = rep2F (F2rep x).
+Axiom wire2rep_F : word (b-1) -> option FRep.
+Axiom wire2rep_F_correct : forall x, Fm_dec x = option_map rep2F (wire2rep_F x).
+
+Axiom FRepMul : FRep -> FRep -> FRep.
+Axiom FRepMul_correct : forall x y, (rep2F x * rep2F y)%F = rep2F (FRepMul x y).
+
+Axiom FRepAdd : FRep -> FRep -> FRep.
+Axiom FRepAdd_correct : forall x y, (rep2F x + rep2F y)%F = rep2F (FRepAdd x y).
+
+Axiom FRepSub : FRep -> FRep -> FRep.
+Axiom FRepSub_correct : forall x y, (rep2F x - rep2F y)%F = rep2F (FRepSub x y).
+
+Axiom FRepInv : FRep -> FRep.
+Axiom FRepInv_correct : forall x, inv (rep2F x)%F = rep2F (FRepInv x).
+
+Axiom FSRepPow : FRep -> SRep -> FRep.
+Axiom FSRepPow_correct : forall x n, (rep2F x ^ rep2S n)%F = rep2F (FSRepPow x n).
+
+Axiom FRepOpp : FRep -> FRep.
+Axiom FRepOpp_correct : forall x, opp (rep2F x) = rep2F (FRepOpp x).
+Axiom wltu : forall {b}, word b -> word b -> bool.
+
+Axiom wltu_correct : forall {b} (x y:word b), wltu x y = (wordToN x <? wordToN y)%N.
+Axiom compare_enc : forall x y, F_eqb x y = weqb (@enc _ _ FqEncoding x) (@enc _ _ FqEncoding y).
+Axiom enc_rep2F : FRep -> word (b-1).
+Axiom enc_rep2F_correct : forall x, enc_rep2F x = @enc _ _ FqEncoding (rep2F x).
+
+Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed.
+
+Definition rep2E (r:FRep * FRep * FRep * FRep) : extended :=
+  match r with (((x, y), z), t) => mkExtended (rep2F x) (rep2F y) (rep2F z) (rep2F t) end.
+
+Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }.
+Proof.
+  unfold rep2E. cbv beta delta [unifiedAddM1'].
+  eexists; instantiate (1 := (((_,_), _), _)).
+Admitted.
+Definition unifiedAddM1Rep (a b:FRep * FRep * FRep * FRep) : FRep * FRep * FRep * FRep := Eval hnf in proj1_sig (unifiedAddM1Rep_sig a b).
+Definition unifiedAddM1Rep_correct a b : rep2E (unifiedAddM1Rep a b) = unifiedAddM1' (rep2E a) (rep2E b)  := Eval hnf in proj2_sig (unifiedAddM1Rep_sig a b).
+
+Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y).
+Proof.
+  destruct b; trivial.
+Qed.
+
+Local Ltac Let_In_rep2F :=
+  match goal with
+  | [ |- appcontext G[Let_In (rep2F ?x) ?f] ]
+    => change (Let_In (rep2F x) f) with (Let_In x (fun y => f (rep2F y))); cbv beta
+  end.
+
 Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}.
 Proof.
   eexists; intros.
@@ -155,17 +273,20 @@ Proof.
            end.
     set_evars.
     rewrite<- point_eqb_correct.
-    rename x0 into R. rename x1 into S. rename x into A.
-    rewrite solve_for_R.
+    rewrite solve_for_R; unfold point_sub.
+    Axiom negate_scalarMult : forall n P, negate (scalarMult n P) = scalarMult n (negate P).
+    rewrite negate_scalarMult.
     let p1 := constr:(scalarMultM1_rep eq_refl) in
     let p2 := constr:(unifiedAddM1_rep eq_refl) in
     repeat match goal with
+           | |- context [(_ * negate ?P)%E] =>
+              rewrite <-(unExtendedPoint_mkExtendedPoint P);
+              rewrite negateExtended_correct;
+              rewrite <-p1
            | |- context [(_ * ?P)%E] =>
               rewrite <-(unExtendedPoint_mkExtendedPoint P);
-               rewrite <-p1
-           | |- context [(?P + unExtendedPoint _)%E] =>
-             rewrite <-(unExtendedPoint_mkExtendedPoint P);
-               rewrite p2
+              rewrite <-p1
+           | _ => rewrite p2
            end;
       rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat;
       subst_evars;
@@ -193,17 +314,13 @@ Proof.
     symmetry; apply decode_test_encode_test.
   } Unfocus.
 
-  etransitivity.
-  Focus 2.
-  { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
-    unfold point_sub. rewrite negateExtended_correct.
-    let p := constr:(unifiedAddM1_rep eq_refl) in rewrite p.
-    reflexivity.
-  } Unfocus.
-
   rewrite enc'_correct.
   cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1].
-  unfold proj1_sig at 1 2 5 6.
+  (* Why does this take too long?
+  lazymatch goal with |- context [ proj1_sig ?x ] =>
+                  fail 5
+  end. *)
+  unfold proj1_sig at 1 2.
   etransitivity.
   Focus 2.
   { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
@@ -217,7 +334,7 @@ Proof.
   Unfocus.
 
   cbv [mkExtendedPoint zero mkPoint].
-  unfold proj1_sig at 1 2 3 5 6 7.
+  unfold proj1_sig at 1 2 3 5 6 7 8.
   rewrite B_proj.
 
   etransitivity.
@@ -249,20 +366,8 @@ Proof.
     reflexivity. }
   Unfocus.
 
-  Set Printing Depth 1000000.
-  Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T).
-  Local Notation "2" := (ZToField 2) : F_scope.
-
   cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding CompleteEdwardsCurveTheorems.solve_for_x2 sqrt_mod_q].
 
-  Axiom FRep : Type.
-  Axiom F2rep : F Ed25519.q -> FRep.
-  Axiom rep2F : FRep -> F Ed25519.q.
-  Axiom rep2F_F2rep : forall x, x = rep2F (F2rep x).
-  Axiom wire2rep_F : word (b-1) -> option FRep.
-  Axiom wire2rep_F_correct : forall x, Fm_dec x = option_map rep2F (wire2rep_F x).
-  rewrite wire2rep_F_correct.
-
   etransitivity.
   Focus 2. {
     do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro.
@@ -277,83 +382,139 @@ Proof.
             end
       end.
   reflexivity. } Unfocus. reflexivity. } Unfocus.
-  rewrite <-!(option_rect_option_map rep2F).
 
   etransitivity.
   Focus 2. {
-    do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro.
+    do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]).
+    do 1 (eapply option_rect_Proper_nd; [ intro; reflexivity | reflexivity | ]).
+    eapply option_rect_Proper_nd; [ cbv beta delta [pointwise_relation]; intro | reflexivity.. ].
+    replace_let_in_with_Let_In.
+    reflexivity.
+  } Unfocus.
 
-    unfold option_rect at 1.
-    cbv beta iota delta [q d CompleteEdwardsCurve.a enc].
-    let RHS' := constr:(
-     @option_rect FRep (fun _ : option FRep => bool)
-       (fun x : FRep =>
-        let x2 := ((rep2F x ^ 2 - 1) / (Ed25519.d * rep2F x ^ 2 - Ed25519.a))%F in
-        let x0 :=
-          let b := (x2 ^ Z.to_N (Ed25519.q / 8 + 1))%F in
-          if (b ^ 2 ==? x2)%F then b else (@sqrt_minus1 Ed25519.q * b)%F in
-        if (x0 ^ 2 ==? x2)%F
-        then
-         let p :=
-           (if Bool.eqb (@whd (b - 1) pk)
-                 (@wordToN (b - 1) (@Fm_enc Ed25519.q (b - 1) (@opp Ed25519.q x0)) <?
-                  @wordToN (b - 1) (@Fm_enc Ed25519.q (b - 1) x0))%N
-            then x0
-            else @opp Ed25519.q x0, rep2F x) in
-       @weqb (S (b - 1)) (sig [:b])
-         (enc'
-            (@extendedToTwisted curve25519params
-               (@unifiedAddM1' curve25519params
-                  (@iter_op (@extended curve25519params) 
-                     (@unifiedAddM1' curve25519params) 
-                     (@twistedToExtended curve25519params (0%F, 1%F)) 
-                     N N.testbit_nat
-                     a
-                     (@twistedToExtended curve25519params Bc) (N.size_nat a))
-                  (negateExtendedc
-                     (@iter_op (@extended curve25519params) 
-                        (@unifiedAddM1' curve25519params) 
-                        (@twistedToExtended curve25519params (0%F, 1%F))
-                        N N.testbit_nat
-                        (@wordToN (b + b) (@H (b + (b + l)) (sig [:b] ++ pk ++ msg)))
-                        (twistedToExtended p) (N.size_nat (@wordToN (b + b) (@H (b + (b + l)) (sig [:b] ++ pk ++ msg)))))))))
-        else false) false
-       (wire2rep_F (@wtl (b - 1) pk))
-                )
-    in match goal with [ |- _ = ?RHS] => replace RHS with RHS' end.
+  etransitivity.
+  Focus 2. {
+    do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]).
+    set_evars.
+    rewrite option_rect_function. (* turn the two option_rects into one *)
+    subst_evars.
+    simpl_option_rect.
+    do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]).
+    (* push the [option_rect] inside until it hits a [Some] or a [None] *)
+    repeat match goal with
+           | _ => commute_option_rect_Let_In
+           | [ |- _ = Let_In _ _ ]
+             => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ]
+           | [ |- ?LHS = option_rect ?P ?S ?N (if ?b then ?t else ?f) ]
+             => transitivity (if b then option_rect P S N t else option_rect P S N f);
+                 [
+                 | destruct b; reflexivity ]
+           | [ |- _ = if ?b then ?t else ?f ]
+             => apply (f_equal2 (fun x y => if b then x else y))
+           | [ |- _ = false ] => reflexivity
+           | _ => progress simpl_option_rect
+           end.
     reflexivity.
-    {
-      unfold option_rect.
-      repeat progress match goal with [ |- context [match ?x with _ => _ end] ] => destruct x; trivial end.
-    }
   } Unfocus.
-  
-  Axiom FRepMul : FRep -> FRep -> FRep.
-  Axiom FRepMul_correct : forall x y, (rep2F x * rep2F y)%F = rep2F (FRepMul x y).
-  
-  Axiom FRepAdd : FRep -> FRep -> FRep.
-  Axiom FRepAdd_correct : forall x y, (rep2F x + rep2F y)%F = rep2F (FRepAdd x y).
-  
-  Axiom FRepSub : FRep -> FRep -> FRep.
-  Axiom FRepSub_correct : forall x y, (rep2F x - rep2F y)%F = rep2F (FRepSub x y).
-
-  Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed.
+
+  cbv iota beta delta [q d a].
+  rewrite wire2rep_F_correct.
 
   etransitivity.
   Focus 2. {
-    do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro.
-    do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro.
+    eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro.
+    rewrite <-!(option_rect_option_map rep2F).
+    eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro.
     rewrite !F_pow_2_r.
-    rewrite !unfoldDiv.
-    rewrite (rep2F_F2rep Ed25519.d), (rep2F_F2rep Ed25519.a), (rep2F_F2rep 1%F).
+    rewrite (rep2F_F2rep 1%F).
+    pattern Ed25519.d at 1. rewrite (rep2F_F2rep Ed25519.d) at 1.
+    pattern Ed25519.a at 1. rewrite (rep2F_F2rep Ed25519.a) at 1.
     rewrite !FRepMul_correct.
     rewrite !FRepSub_correct.
-    cbv zeta.
-    rewrite F_pow_2_r.
-    
-  cbv beta delta [twistedToExtended].
-  
-  cbv beta iota delta
+    rewrite !unfoldDiv.
+    rewrite !FRepInv_correct.
+    rewrite !FRepMul_correct.
+    Let_In_rep2F.
+    rewrite (rep2S_S2rep (Z.to_N (Ed25519.q / 8 + 1))).
+    eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro].
+    etransitivity. Focus 2. eapply Let_In_Proper_nd; [|cbv beta delta [pointwise_relation]; intro;reflexivity]. {
+      rewrite FSRepPow_correct.
+      Let_In_rep2F.
+      etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. {
+        set_evars.
+        rewrite !F_pow_2_r.
+        rewrite !FRepMul_correct.
+        rewrite if_F_eq_dec_if_F_eqb.
+        rewrite compare_enc.
+        rewrite <-!enc_rep2F_correct.
+        rewrite (rep2F_F2rep sqrt_minus1).
+        rewrite !FRepMul_correct.
+        rewrite (if_map rep2F).
+        subst_evars.
+        reflexivity. } Unfocus.
+      match goal with |- ?e = Let_In ?xval (fun x => rep2F (@?f x)) => change (e = rep2F (Let_In xval f)) end.
+      reflexivity. } Unfocus.
+    Let_In_rep2F.
+    eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro].
+    set_evars.
+    rewrite !F_pow_2_r.
+    rewrite !FRepMul_correct.
+    rewrite if_F_eq_dec_if_F_eqb.
+    rewrite compare_enc.
+    rewrite <-!enc_rep2F_correct.
+    subst_evars.
+    lazymatch goal with  |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity].
+
+    set_evars.
+    rewrite !FRepOpp_correct.
+    rewrite <-!enc_rep2F_correct.
+    rewrite <-wltu_correct.
+    rewrite (if_map rep2F).
+    lazymatch goal with
+      |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) =>
+        change (e = Let_In (x, y) (fun p => r (rep2F (fst p), rep2F (snd p)))); cbv beta zeta
+    end.
+    subst_evars.
+    eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro].
+
+    set_evars; erewrite (f_equal2 (@weqb b)); subst_evars; [|reflexivity|symmetry]. Focus 2. {
+      unfold twistedToExtended.
+      rewrite F_mul_0_l.
+      unfold curve25519params, q. (* TODO: do we really wanna do it here? *)
+      rewrite (rep2F_F2rep 0%F).
+      rewrite (rep2F_F2rep 1%F).
+      rewrite (rep2F_F2rep xB%F).
+      rewrite (rep2F_F2rep yB%F).
+      rewrite !FRepMul_correct.
+      repeat match goal with |- appcontext [ ?E ] =>
+                      match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) =>
+                                   change E with (rep2E (((x, y), z), t))
+                      end
+      end.
+      lazymatch goal with |- context [negateExtended' (rep2E ?E)] =>
+                          replace (negateExtended' (rep2E E)) with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; rewrite !FRepOpp_correct; reflexivity)
+      end; simpl fst; simpl snd. (* we actually only want to simpl in the with clause *)
+      do 2 erewrite <- (fun x y z => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat) by apply unifiedAddM1Rep_correct.
+      rewrite <-unifiedAddM1Rep_correct.
+      
+      
+      etransitivity. Focus 2. {
+        apply f_equal.
+        Definition rep2T (P:FRep * FRep) := (rep2F (fst P), rep2F (snd P)).
+        Definition erep2trep (P:FRep * FRep * FRep * FRep) := Let_In P (fun P => Let_In (FRepInv (snd (fst P))) (fun iZ => (FRepMul (fst (fst (fst P))) iZ, FRepMul (snd (fst (fst P))) iZ))).
+        Lemma erep2trep_correct : forall P, rep2T (erep2trep P) = extendedToTwisted (rep2E P).
+        Proof.
+          unfold rep2T, rep2E, erep2trep, extendedToTwisted; destruct P as [[[]]]; simpl.
+          rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity.
+        Qed.
+        rewrite <-erep2trep_correct; cbv beta delta [erep2trep].
+        reflexivity. } Unfocus.
+        
+    reflexivity. } Unfocus.
+    (*
+    cbv beta iota delta
       [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd
-       point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q ].
-Admitted.
+       point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q].
+    *)
+  reflexivity.
+Admitted.
\ No newline at end of file
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
new file mode 100644
index 000000000..08ebfe13e
--- /dev/null
+++ b/src/Util/Tactics.v
@@ -0,0 +1,25 @@
+(** * Generic Tactics *)
+
+(* [pose proof defn], but only if no hypothesis of the same type exists.
+   most useful for proofs of a proposition *)
+Tactic Notation "unique" "pose" "proof" constr(defn) :=
+  let T := type of defn in
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => pose proof defn
+  end.
+(* [assert T], but only if no hypothesis of the same type exists.
+   most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T
+  end.
+
+(* [assert T], but only if no hypothesis of the same type exists.
+   most useful for proofs of a proposition *)
+Tactic Notation "unique" "assert" constr(T) "by" tactic3(tac) :=
+  match goal with
+  | [ H : T |- _ ] => fail 1
+  | _ => assert T by tac
+  end.