Drop second projections in Ed25519

2 files changed, 127 insertions, 6 deletions

diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index 4823ef28f..e1d3744fb 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -57,6 +57,18 @@ Section PointEncoding.
 Definition sign_bit (x : F q) := (wordToN (enc (opp x)) <? wordToN (enc x))%N.
 Definition point_enc (p : point) : word (S sz) := let '(x,y) := proj1_sig p in
   WS (sign_bit x) (enc y).
+Definition point_dec_coordinates (w : word (S sz)) : option (F q * F q) :=
+  match dec (wtl w) with
+  | None => None
+  | Some y => let x2 := solve_for_x2 y in
+      let x := sqrt_mod_q x2 in
+      if F_eq_dec (x ^ 2) x2
+      then if Bool.eqb (whd w) (sign_bit x)
+           then Some (x, y)
+           else Some (opp x, y)
+      else None
+  end.
+
 Definition point_dec (w : word (S sz)) : option point :=
   match dec (wtl w) with
   | None => None
@@ -70,6 +82,15 @@ Definition point_dec (w : word (S sz)) : option point :=
       end
   end.
 
+Lemma point_dec_coordinates_correct w
+  : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates w.
+Proof.
+  unfold point_dec, point_dec_coordinates.
+  edestruct dec; [ | reflexivity ].
+  edestruct @F_eq_dec; [ | reflexivity ].
+  edestruct @Bool.eqb; reflexivity.
+Qed.
+
 Lemma y_decode : forall p, dec (wtl (point_enc p)) = Some (snd (proj1_sig p)).
 Proof.
   intros.
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index a705ceb90..32de3dc13 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -14,18 +14,52 @@ Local Arguments H {_} _.
 Local Arguments scalarMultM1 {_} {_} _ _.
 Local Arguments unifiedAddM1 {_} {_} _ _.
 
-Ltac set_evars :=
+Local Ltac set_evars :=
   repeat match goal with
          | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
          end.
-Ltac subst_evars :=
+Local Ltac subst_evars :=
   repeat match goal with
          | [ e := ?E |- _ ] => is_evar E; subst e
          end.
 
+Lemma funexp_proj {T T'} (proj : T -> T') (f : T -> T) (f' : T' -> T') x n
+      (f_proj : forall a, proj (f a) = f' (proj a))
+  : proj (funexp f x n) = funexp f' (proj x) n.
+Proof.
+  revert x; induction n as [|n IHn]; simpl; congruence.
+Qed.
+
+Lemma iter_op_proj {T T'} (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') x y z
+      (op_proj : forall a b, proj (op a b) = op' (proj a) (proj b))
+  : proj (iter_op op x y z) = iter_op op' (proj x) y (proj z).
+Proof.
+  unfold iter_op.
+  simpl.
+  lazymatch goal with
+  | [ |- ?proj (snd (funexp ?f ?x ?n)) = snd (funexp ?f' _ ?n) ]
+    => pose proof (fun x0 x1 => funexp_proj (fun x => (fst x, proj (snd x))) f f' (x0, x1)) as H'
+  end.
+  simpl in H'.
+  rewrite <- H'.
+  { reflexivity. }
+  { intros [??]; simpl.
+    repeat match goal with
+           | [ |- context[match ?n with _ => _ end] ]
+             => destruct n eqn:?
+           | _ => progress simpl
+           | _ => progress subst
+           | _ => reflexivity
+           | _ => rewrite op_proj
+           end. }
+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.
+
 Require Import Coq.Setoids.Setoid.
 Require Import Coq.Classes.Morphisms.
 Global Instance option_rect_Proper_nd {A T}
@@ -59,7 +93,13 @@ 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 negateExtended : extendedPoint -> extendedPoint.
+Axiom negateExtendedc : extended -> extended.
+Definition negateExtended : extendedPoint -> extendedPoint.
+Proof.
+  intro x.
+  exists (negateExtendedc (proj1_sig x)).
+  admit.
+Defined.
 Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P).
 
 Local Existing Instance PointEncoding.
@@ -76,6 +116,18 @@ Proof.
     apply weqb_true_iff in Heqb. subst. rewrite encoding_valid in H; discriminate. }
 Qed.
 
+Definition enc' : F q * F q -> word (S (b - 1)).
+Proof.
+  intro x.
+  let enc' := (eval hnf in (@enc (@point curve25519params) _ _)) in
+  match (eval cbv [proj1_sig] in (fun pf => enc' (exist _ x pf))) with
+  | (fun _ => ?enc') => exact enc'
+  end.
+Defined.
+
+Definition enc'_correct : @enc (@point curve25519params) _ _ = (fun x => enc' (proj1_sig x))
+  := eq_refl.
+
 Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}.
 Proof.
   eexists; intros.
@@ -145,11 +197,59 @@ Proof.
     reflexivity.
   } Unfocus.
 
-  cbv [scalarMultM1 iter_op].
+  rewrite enc'_correct.
+  cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1].
+  unfold proj1_sig at 1 2 5 6.
+  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 ?x ?y ?z)] ]
+             => erewrite (@iter_op_proj T A (@proj1_sig _ _)) by reflexivity
+           end.
+    subst_evars.
+    reflexivity. }
+  Unfocus.
+
+  cbv [mkExtendedPoint zero mkPoint].
+  unfold proj1_sig at 1 2 3 5 6 7.
+  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'
+    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 zeta delta [test_and_op].
   Local Arguments funexp {_} _ {_} {_}. (* do not display the initializer and iteration bound for now *)
 
   Axiom rep : forall {m}, list Z -> F m -> Prop.
   Axiom decode_point_limbs : word (S (b-1)) -> option (list Z * list Z).
-  Axiom point_dec_rep : forall P_ P lx ly, dec P_ = Some P -> decode_point_limbs P_ = Some (lx, ly) -> rep lx (fst (proj1_sig P)) /\ rep ly (fst (proj1_sig P)).
-Admitted.
\ No newline at end of file
+  Axiom point_dec_rep : forall P_ P lx ly, dec P_ = Some P -> decode_point_limbs P_ = Some (lx, ly) -> rep lx (fst (proj1_sig P)) /\ rep ly (fst (proj1_sig P)).*)
+Admitted.