ed25519 derivation down to word until main equation

1 files changed, 180 insertions, 79 deletions

diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index f98bf2d12..baad7a184 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -132,6 +132,96 @@ 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 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.
+
+Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. 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.
+
+Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T).
+Local Notation "2" := (ZToField 2) : F_scope.
+
 Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}.
 Proof.
   eexists; intros.
@@ -249,20 +339,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 +355,106 @@ 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].
+
+    (*
+    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. } Unfocus.
+  reflexivity.
+Admitted.
\ No newline at end of file