F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more broken...

2 files changed, 427 insertions, 334 deletions

diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 996aabb21..3db14f057 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -9,7 +9,7 @@ Require Import Crypto.Encoding.PointEncodingPre.
 Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.PointEncoding.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil.
+Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep.
 
 Local Infix "++" := Word.combine.
 Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40).
@@ -184,355 +184,352 @@ Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc'
                => 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 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.
-
-Create HintDb FRepOperations discriminated.
-Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations.
-
-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 unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }.
-Proof.
-  destruct a as [[[]]]; destruct b as [[[]]].
-  eexists.
-  lazymatch goal with |- ?LHS = ?RHS :> ?T =>
-                  evar (e:T); replace LHS with e; [subst e|]
-  end.
-  unfold rep2E. cbv beta delta [unifiedAddM1'].
-  pose proof (rep2F_F2rep twice_d) as H; rewrite H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *)
-   
-  { etransitivity; [|replace_let_in_with_Let_In; reflexivity].
-    repeat (
-      autorewrite with FRepOperations;
-      Let_In_rep2F;
-      eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]).
-      lazymatch goal with |- ?LHS = (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) =>
-                          change (LHS = (rep2E (((x, y), z), t)))
-      end.
-      reflexivity. }
-
-  subst e.
-  reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *)
-Defined.
-
-(*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *)
+Section Ed25519Frep.
+  Generalizable All Variables.
+  Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS).
+  Context `(rcF:RepConversions (F (Ed25519.q)) FRep) (rcFOK:RepConversionsOK rcF).
+  Context (FRepAdd FRepSub FRepMul:FRep->FRep->FRep) (FRepAdd_correct:RepBinOpOK rcF add FRepMul).
+  Context (FRepSub_correct:RepBinOpOK rcF sub FRepSub) (FRepMul_correct:RepBinOpOK rcF mul FRepMul).
+  Local Notation rep2F := (unRep : FRep -> F (Ed25519.q)).
+  Local Notation F2Rep := (toRep : F (Ed25519.q) -> FRep).
+  Local Notation rep2S := (unRep : SRep -> N).
+  Local Notation S2Rep := (toRep : N -> SRep).
+
+  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).
 
-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).
+  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.
 
-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.
+  Axiom compare_enc : forall x y, F_eqb x y = weqb (@enc _ _ FqEncoding x) (@enc _ _ FqEncoding y).
 
-Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}.
-Proof.
-  eexists; intros.
-  cbv [ed25519_verify EdDSA.verify
-                      ed25519params curve25519params
-                      EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H
-                      EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding].
+  Axiom wire2FRep : word (b-1) -> option FRep.
+  Axiom wire2FRep_correct : forall x, Fm_dec x = option_map rep2F (wire2FRep x).
 
-  etransitivity.
-  Focus 2.
-  { repeat match goal with
-           | [ |- ?x = ?x ] => reflexivity
-           | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ]
-             => etransitivity;
-               [
-               | refine (_ : option_rect (fun _ => T) _ N a = _);
-                 let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in
-                 refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end)
-                                     (fun x => _) _ a); intros; simpl @option_rect ];
-               [ reflexivity | .. ]
-           end.
-    set_evars.
-    rewrite<- E.point_eqb_correct.
-    rewrite solve_for_R; unfold E.sub.
-    rewrite E.opp_mul.
-    let p1 := constr:(scalarMultM1_rep eq_refl) in
-    let p2 := constr:(unifiedAddM1_rep eq_refl) in
-    repeat match goal with
-           | |- context [(_ * E.opp ?P)%E] =>
-              rewrite <-(unExtendedPoint_mkExtendedPoint P);
-              rewrite negateExtended_correct;
-              rewrite <-p1
-           | |- context [(_ * ?P)%E] =>
-              rewrite <-(unExtendedPoint_mkExtendedPoint P);
-              rewrite <-p1
-           | _ => rewrite p2
-           end;
-      rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat;
-      subst_evars;
-      reflexivity.
-    } Unfocus.
-
-  etransitivity.
-  Focus 2.
-  { lazymatch goal with |- _ = option_rect _ _ ?false ?dec =>
-                    symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)]
-    end.
-    eapply option_rect_Proper_nd; [intro|reflexivity..].
+  Axiom FRep2wire : FRep -> word (b-1).
+  Axiom FRep2wire_correct : forall x, FRep2wire 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 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.
+  
+  Create HintDb FRepOperations discriminated.
+  Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations.
+  
+  Local Ltac Let_In_unRep :=
     match goal with
-    | [ |- ?RHS = ?e ?v ]
-      => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in
-        unify e RHS'
+    | [ |- appcontext G[Let_In (unRep ?x) ?f] ]
+      => change (Let_In (unRep x) f) with (Let_In x (fun y => f (unRep y))); cbv beta
     end.
-    reflexivity.
-  } Unfocus.
-  rewrite <-decode_scalar_correct.
-
-  etransitivity.
-  Focus 2.
-  { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
-    symmetry; apply decode_test_encode_test.
-  } Unfocus.
   
-  rewrite enc'_correct.
-  cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1].
-  (* 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..]).
-    set_evars.
-    repeat match goal with
-           | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ]
-             => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity 
-           end.
-    subst_evars.
-    reflexivity. }
-  Unfocus.
-
-  cbv [mkExtendedPoint E.zero].
-  unfold proj1_sig at 1 2 3 5 6 7 8.
-  rewrite B_proj.
-
-  etransitivity.
-  Focus 2.
-  { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
-    set_evars.
-    lazymatch goal with |- _ = option_rect _ _ ?false ?dec =>
-                        symmetry; etransitivity; [|eapply (option_rect_option_map (@proj1_sig _ _) _ false dec)]
-    end.
-    eapply option_rect_Proper_nd; [intro|reflexivity..].
-    match goal with
-    | [ |- ?RHS = ?e ?v ]
-      => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in
-        unify e RHS'
+  Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }.
+  Proof.
+    destruct a as [[[]]]; destruct b as [[[]]].
+    eexists.
+    lazymatch goal with |- ?LHS = ?RHS :> ?T =>
+                    evar (e:T); replace LHS with e; [subst e|]
     end.
-    reflexivity.
-  } Unfocus.
-
-  cbv [dec PointEncoding point_encoding].
-  etransitivity.
-  Focus 2.
-  { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
+    unfold rep2E. cbv beta delta [unifiedAddM1'].
+    pose proof (rcFOK twice_d) as H; rewrite <-H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *)
+     
+    { etransitivity; [|replace_let_in_with_Let_In; reflexivity].
+      repeat (
+        autorewrite with FRepOperations;
+        Let_In_unRep;
+        eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]).
+        lazymatch goal with |- ?LHS = (unRep ?x, unRep ?y, unRep ?z, unRep ?t) =>
+                            change (LHS = (rep2E (((x, y), z), t)))
+        end.
+        reflexivity. }
+  
+    subst e.
+    reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *)
+  Defined.
+  
+  (*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *)
+  
+  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).
+  
+  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.
+  
+  Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}.
+  Proof.
+    eexists; intros.
+    cbv [ed25519_verify EdDSA.verify
+                        ed25519params curve25519params
+                        EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H
+                        EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding].
+  
+    etransitivity.
+    Focus 2.
+    { repeat match goal with
+             | [ |- ?x = ?x ] => reflexivity
+             | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ]
+               => etransitivity;
+                 [
+                 | refine (_ : option_rect (fun _ => T) _ N a = _);
+                   let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in
+                   refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end)
+                                       (fun x => _) _ a); intros; simpl @option_rect ];
+                 [ reflexivity | .. ]
+             end.
+      set_evars.
+      rewrite<- E.point_eqb_correct.
+      rewrite solve_for_R; unfold E.sub.
+      rewrite E.opp_mul.
+      let p1 := constr:(scalarMultM1_rep eq_refl) in
+      let p2 := constr:(unifiedAddM1_rep eq_refl) in
+      repeat match goal with
+             | |- context [(_ * E.opp ?P)%E] =>
+                rewrite <-(unExtendedPoint_mkExtendedPoint P);
+                rewrite negateExtended_correct;
+                rewrite <-p1
+             | |- context [(_ * ?P)%E] =>
+                rewrite <-(unExtendedPoint_mkExtendedPoint P);
+                rewrite <-p1
+             | _ => rewrite p2
+             end;
+        rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat;
+        subst_evars;
+        reflexivity.
+      } Unfocus.
+  
+    etransitivity.
+    Focus 2.
+    { lazymatch goal with |- _ = option_rect _ _ ?false ?dec =>
+                      symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)]
+      end.
+      eapply option_rect_Proper_nd; [intro|reflexivity..].
+      match goal with
+      | [ |- ?RHS = ?e ?v ]
+        => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in
+          unify e RHS'
+      end.
+      reflexivity.
+    } Unfocus.
+    rewrite <-decode_scalar_correct.
+  
+    etransitivity.
+    Focus 2.
+    { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
+      symmetry; apply decode_test_encode_test.
+    } Unfocus.
+    
+    rewrite enc'_correct.
+    cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1].
+    (* 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.
-    { apply f_equal.
-      symmetry.
-      apply point_dec_coordinates_correct. }
+    { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
+      set_evars.
+      repeat match goal with
+             | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ]
+               => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity 
+             end.
+      subst_evars.
+      reflexivity. }
     Unfocus.
-    reflexivity. }
-  Unfocus.
-
-  cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q].
-
-  etransitivity.
-  Focus 2. {
-    do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro.
+  
+    cbv [mkExtendedPoint E.zero].
+    unfold proj1_sig at 1 2 3 5 6 7 8.
+    rewrite B_proj.
+  
     etransitivity.
     Focus 2.
-    { apply f_equal.
-      lazymatch goal with
-      | [ |- _ = ?term :> ?T ]
-        => lazymatch term with (match ?a with None => ?N | Some x => @?S x end)
-          => let term' := constr:((option_rect (fun _ => T) S N) a) in
-            replace term with term' by reflexivity
-            end
+    { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
+      set_evars.
+      lazymatch goal with |- _ = option_rect _ _ ?false ?dec =>
+                          symmetry; etransitivity; [|eapply (option_rect_option_map (@proj1_sig _ _) _ false dec)]
       end.
-  reflexivity. } Unfocus. reflexivity. } Unfocus.
-
-  etransitivity.
-  Focus 2. {
-    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.
-
-  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.
-  } Unfocus.
-
-  cbv iota beta delta [q d a].
-  rewrite wire2rep_F_correct.
+      eapply option_rect_Proper_nd; [intro|reflexivity..].
+      match goal with
+      | [ |- ?RHS = ?e ?v ]
+        => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in
+          unify e RHS'
+      end.
+      reflexivity.
+    } Unfocus.
+  
+    cbv [dec PointEncoding point_encoding].
+    etransitivity.
+    Focus 2.
+    { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]).
+      etransitivity.
+      Focus 2.
+      { apply f_equal.
+        symmetry.
+        apply point_dec_coordinates_correct. }
+      Unfocus.
+      reflexivity. }
+    Unfocus.
+  
+    cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q].
+  
+    etransitivity.
+    Focus 2. {
+      do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro.
+      etransitivity.
+      Focus 2.
+      { apply f_equal.
+        lazymatch goal with
+        | [ |- _ = ?term :> ?T ]
+          => lazymatch term with (match ?a with None => ?N | Some x => @?S x end)
+            => let term' := constr:((option_rect (fun _ => T) S N) a) in
+              replace term with term' by reflexivity
+              end
+        end.
+    reflexivity. } Unfocus. reflexivity. } Unfocus.
+  
+    etransitivity.
+    Focus 2. {
+      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.
+  
+    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.
+    } Unfocus.
+  
+    cbv iota beta delta [q d a].
 
-  etransitivity.
-  Focus 2. {
-    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 (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.
-    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.
+    rewrite wire2FRep_correct.
+  
+    etransitivity.
+    Focus 2. {
+      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 <-(rcFOK 1%F).
+      pattern Ed25519.d at 1. rewrite <-(rcFOK Ed25519.d) at 1.
+      pattern Ed25519.a at 1. rewrite <-(rcFOK Ed25519.a) at 1.
+      rewrite !FRepMul_correct.
+      rewrite !FRepSub_correct.
+      rewrite !unfoldDiv.
+      rewrite !FRepInv_correct.
+      rewrite !FRepMul_correct.
+      Let_In_unRep.
+      rewrite <-(rcSOK (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]. {
+        (* TODO:
+           rewrite <-pow_nat_iter_op_correct.
+           erewrite <-iter_op_spec. *)
+        rewrite FSRepPow_correct.
+        Let_In_unRep.
+        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 <-!FRep2wire_correct.
+          rewrite <-(rcFOK 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.
-      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 (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).
-      match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite (rep2F_F2rep x) end end.
-      match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite (rep2F_F2rep x) end end.
+      Let_In_unRep.
+      eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro].
+      set_evars.
+      rewrite !F_pow_2_r.
       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
+      rewrite if_F_eq_dec_if_F_eqb.
+      rewrite compare_enc.
+      rewrite <-!FRep2wire_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 (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.
-      lazymatch goal with |- context [?X] =>
-                          lazymatch X with negateExtended' (rep2E ?E) =>
-                          replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; rewrite !FRepOpp_correct; reflexivity)
-      end 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.
-        rewrite <-erep2trep_correct; cbv beta delta [erep2trep].
+      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 <-(rcFOK 0%F).
+        rewrite <-(rcFOK 1%F).
+        match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite <-(rcFOK x) end end.
+        match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite <-(rcFOK x) end end.
+        autorewrite with FRepOperations. (* breaks reflexivity *)
+        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 [?X] =>
+                            lazymatch X with negateExtended' (rep2E ?E) =>
+                            replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; autorewrite with FRepOperations; reflexivity)
+        end 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, <-erep2trep_correct; cbv beta delta [erep2trep].
+
+        (*
         reflexivity. } Unfocus.
-        
+      (*
+      cbv beta iota delta
+        [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd
+         point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q].
+      *)
       reflexivity. } Unfocus.
-    (*
-    cbv beta iota delta
-      [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd
-       point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q].
-    *)
-    reflexivity. } Unfocus.
-  reflexivity.
-Admitted.
+    reflexivity.
+*)
+  Admitted.
+
+End Ed25519Frep.
\ No newline at end of file
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index b01e6280e..8aaf8caf6 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -7,6 +7,7 @@ Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.BaseSystem.
+Require Import Crypto.Rep.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Local Open Scope Z.
@@ -81,4 +82,99 @@ Proof.
   intros f g Hf Hg.
   pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
-Defined.
\ No newline at end of file
+Defined.
+
+Definition F25519Rep := (Z * Z * Z * Z * Z  *  Z * Z * Z * Z * Z)%type.
+
+Definition F25519toRep (x:F (2^255 - 19)) : F25519Rep := (0, 0, 0, 0, 0,  0, 0, 0, 0, FieldToZ x)%Z.
+Definition F25519unRep (rx:F25519Rep) :=
+  let '(x9, x8, x7, x6, x5, x4, x3, x2, x1, x0) := rx in
+                ModularBaseSystem.decode [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9].
+
+Global Instance F25519RepConversions : RepConversions (F (2^255 - 19)) F25519Rep :=
+  {
+    toRep := F25519toRep;
+    unRep := F25519unRep
+  }.
+
+Lemma F25519RepConversionsOK : RepConversionsOK F25519RepConversions.
+Proof.
+  unfold F25519RepConversions, RepConversionsOK, unRep, toRep, F25519toRep, F25519unRep; intros.
+  change (ModularBaseSystem.decode (ModularBaseSystem.encode x) = x).
+  eauto using ModularBaseSystemProofs.rep_decode, ModularBaseSystemProofs.encode_rep.
+Qed.
+
+Definition F25519Rep_mul (f g:F25519Rep) : F25519Rep.
+  refine (
+  let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in
+  let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _).
+  (* FIXME: the r should not be present in generated code *)
+  pose (r := proj1_sig (GF25519Base25Point5_mul_reduce_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+                                                             g0 g1 g2 g3 g4 g5 g6 g7 g8 g9)).
+  simpl in r.
+  unfold F25519Rep.
+  repeat let t' := (eval cbv beta delta [r] in r) in
+    lazymatch t' with Let_In ?arg ?f =>
+                      let x := fresh "x" in
+                      refine (let x := arg in _);
+                        let t'' := (eval cbv beta in (f x)) in
+                        change (Let_In arg f) with t'' in r
+    end.
+  let t' := (eval cbv beta delta [r] in r) in
+  lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] =>
+                    clear r;
+                    exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0)
+  end.
+Time Defined.
+
+Lemma F25519_mul_OK : RepBinOpOK F25519RepConversions ModularArithmetic.mul F25519Rep_mul.
+  cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_mul toRep unRep F25519toRep F25519unRep].
+  destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
+  destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
+  let E := constr:(GF25519Base25Point5_mul_reduce_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+    destruct E as [? r]; cbv [proj1_sig].
+  cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
+Qed.
+
+Definition F25519Rep_add (f g:F25519Rep) : F25519Rep.
+  refine (
+  let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in
+  let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _).
+  let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_add_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+                                                                       g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in
+  lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] =>
+                    exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0)
+  end.
+Defined.
+
+Definition F25519Rep_sub (f g:F25519Rep) : F25519Rep.
+  refine (
+  let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in
+  let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _).
+  let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_sub_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+                                                                       g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in
+  lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] =>
+                    exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0)
+  end.
+Defined.
+
+Lemma F25519_add_OK : RepBinOpOK F25519RepConversions ModularArithmetic.add F25519Rep_add.
+  cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_add toRep unRep F25519toRep F25519unRep].
+  destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
+  destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
+  let E := constr:(GF25519Base25Point5_add_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+    destruct E as [? r]; cbv [proj1_sig].
+  cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
+Qed.
+
+Lemma F25519_sub_OK : RepBinOpOK F25519RepConversions ModularArithmetic.sub F25519Rep_sub.
+  cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_sub toRep unRep F25519toRep F25519unRep].
+  destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
+  destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
+  let E := constr:(GF25519Base25Point5_sub_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+    destruct E as [? r]; cbv [proj1_sig].
+  cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
+Qed.
\ No newline at end of file