moving forward.

High/Zmodp.v

@@ -500,6 +500,28 @@ rewrite Z.mul_1_l.
 apply modZp.
 Qed.
 
+Open Scope ring_scope.
+Lemma add_eq_mul2: forall (x:Zmodp.type),
+  2%:R * x = x + x.
+Proof.
+  move => x.
+  have -> : 2%:R = 1%:R + 1%:R :> Zmodp.type by apply val_inj => //=.
+  rewrite GRing.mulrDl GRing.mul1r //.
+Qed.
+
+Lemma time_2_eq_0 (a:Zmodp.type) : 2%:R * a = 0 ->  a = 0.
+Proof.
+  move/(f_equal (fun x => (2%:R^-1) * x)).
+  rewrite GRing.mulrA GRing.mulr0 (mulrC 2%:R^-1) GRing.mulfV.
+  rewrite GRing.mul1r //.
+  by zmodp_compute.
+Qed.
+
+Lemma mult_xy_eq_0: forall (x y: Zmodp.type),
+  x * y = 0 -> x = 0 \/ y = 0.
+Proof. by move => x y/eqP; rewrite mulf_eq0 ; move/orP => []/eqP -> ; [left|right]. Qed.
+
+Close Scope ring_scope.
 (* Lemma eq_inv_2' : forall (x m:Zmodp.type), ((Zmodp.pi 2) * m = x)%R -> (m = (Zmodp.pi 28948022309329048855892746252171976963317496166410141009864396001978282409975%Z) * x)%R.
 Proof.
 move => m x <-.

High/Zmodp2.v

@@ -50,6 +50,9 @@ split.
   by move/andP => [] /Refl.eqb_spec -> /Refl.eqb_spec ->.
 Qed.
 
+Lemma Zmodp2_inv : forall a b c d, Zmodp2 a c = Zmodp2 b d -> a = b /\ c = d.
+Proof. by move => a b c d H; inversion H. Qed.
+
 End Zmodp2.
 
 Import Zmodp2.

High/Zmodp2_rules.v

@@ -139,9 +139,7 @@ move => []; move/Refl.eqb_spec.
   apply/eqP => H2a.
   apply: Ha.
   move: H2a.
-  move/(f_equal (fun x => (2%:R^-1) * x)).
-  rewrite GRing.mulrA GRing.mulr0 (mulrC 2%:R^-1) GRing.mulfV ; ring_simplify_this.
-  by zmodp_compute.
+  apply time_2_eq_0.
 Qed.
 
 (*

High/curve25519_twist25519_eq.v

@@ -9,10 +9,10 @@ From Tweetnacl.High Require Import opt_ladder.
 From Tweetnacl.High Require Import curve25519_prime.
 From Tweetnacl.High Require Import prime_ssrprime.
 From Reciprocity Require Import Reciprocity.Reciprocity.
+From Tweetnacl.High Require Import Zmodp.
 Require Import ZArith.
 
 Import BinInt.
-
 Open Scope ring_scope.
 Import GRing.Theory.
 
@@ -23,7 +23,8 @@ move => n x.
 rewrite /curve25519_ladder /twist25519_ladder  /opt_montgomery.
 elim 255 => //.
 Qed.
-From Tweetnacl.High Require Import Zmodp.
+
+Open Scope Z.
 
 Local Notation "p '#x0'" := (point_x0 p) (at level 30).
 Local Notation "Z.R A" := (Zmodp.repr A) (at level 30).

High/curve_incl_Fp2.v

@@ -137,6 +137,7 @@ Proof.
   by rewrite ?GRing.mulrS -IHn curve25519_add_Fp_to_Fp2.
 Qed.
 
+(* this is a truncation, meaning we do not have the garantee that y = 0 *)
 Definition cFp_to_Fp2 p := match p with
   | Zmodp2.Zmodp2 x y => x
   end.
@@ -150,14 +151,16 @@ Local Notation "p '/p'" := (cFp_to_Fp2 p) (at level 40).
 From mathcomp Require Import ssrnat.
 
 Theorem curve25519_ladder_really_ok (n : nat) x :
-    (n < 2^255)%nat -> x != 0 ->
+    (n < 2^255)%nat ->
+    x != 0 ->
     forall (p  : mc curve25519_mcuType),
-    (curve25519_Fp_to_Fp2 p)#x0 /p = x -> curve25519_ladder n x = ((curve25519_Fp_to_Fp2 p) *+ n)#x0 /p.
+    (curve25519_Fp_to_Fp2 p)#x0 = Zmodp2.Zmodp2 x 0 ->
+    curve25519_ladder n x = ((curve25519_Fp_to_Fp2 p) *+ n)#x0 /p.
 Proof.
   move => Hn Hx p Hp.
   have Hp' := cFp_to_Fp2_cancel p.
   have Hp'' : p #x0 = x.
-  by rewrite Hp'.
+  move: Hp'; rewrite Hp => //=.
   rewrite (curve25519_ladder_ok n x Hn Hx p Hp'').
   rewrite -nP_is_nP2.
   rewrite cFp_to_Fp2_cancel //.

High/curve_twist_incl_Fp2.v

@@ -91,42 +91,70 @@ Proof. reflexivity. Qed.
 Lemma Fp_to_Fp2_eq_T: Fp_to_Fp2 = tFp_to_Fp2.
 Proof. reflexivity. Qed.
 
-From mathcomp Require Import ssrnat.
 Local Notation "p '/p'" := (Fp_to_Fp2 p) (at level 40).
 
-Lemma curve25519_ladder_maybe_ok (n : nat) x :
-    (n < 2^255)%nat -> x != 0 ->
-    forall (p'  : mc curve25519_Fp2_mcuType),
-    (exists p, curve25519_Fp_to_Fp2 p #x0 /p = x) \/ (exists p, twist25519_Fp_to_Fp2 p #x0 /p = x) ->
-    p'#x0 /p = x -> curve25519_ladder n x = (p' *+ n)#x0 /p.
+Lemma Fp2_to_Fp :
+  forall (x: Zmodp.type) (p : mc curve25519_Fp2_mcuType),
+  p #x0 = Zmodp2.Zmodp2 x 0 ->
+  (exists c:mc curve25519_mcuType, curve25519_Fp_to_Fp2 c = p) \/ (exists t:mc twist25519_mcuType, twist25519_Fp_to_Fp2 t = p).
 Proof.
-  move => Hn Hx p' [[p Hp]|[p Hp]] Hp'.
-(*   have [[p Hp]|[p Hp]]:= x_is_on_curve_or_twist x. *)
-  rewrite (curve25519_ladder_really_ok n x Hn Hx p Hp) -Fp_to_Fp2_eq_C.
-  f_equal.
-  f_equal.
-  f_equal.
+  move => x [[|xp yp] Hp].
+  + (* is p is at infinity *)
+  move => _ ; left.
+  have Hc : oncurve curve25519_mcuType ∞ => //=.
+  exists (MC Hc) => /= ; apply mc_eq => //.
+  + (* if p is (x,y) *)
+  have := Hp.
+  rewrite /oncurve /= /a /b.
+  destruct yp as [yp1 yp2].
+  move => Hp' Hx.
+  have : (Zmodp2.Zmodp2 yp1 yp2) ^+ 2 == (Zmodp2.Zmodp2 x 0) ^+ 3 + Zmodp2.pi (Zmodp.pi 486662, 0) * (Zmodp2.Zmodp2 x 0) ^+ 2 + (Zmodp2.Zmodp2 x 0).
+  rewrite -Hx -(GRing.mul1r (Zmodp2.Zmodp2 yp1 yp2 ^+ 2)) //.
+  rewrite expr3 ?expr2.
+  Zmodpify => /=.
+  have ->: Zmodp2.Zmodp2 yp1 yp2 * Zmodp2.Zmodp2 yp1 yp2 = Zmodp2.Zmodp2 (yp1^+2 + 2%:R * yp2^+2) (2%:R * yp1 * yp2).
+  rewrite /GRing.mul /= /Zmodp2.mul /Zmodp2.pi expr2 /=.
+  ringify .
   f_equal.
-  destruct p, p' => /=.
-  apply mc_eq.
-  destruct p, p0 => //=.
-  move: Hp Hp' Hx => /= <- //=.
-  move: Hp Hp' Hx => /= <- <- //=.
-  move: Hp Hp' => /= -> <-.
-Admitted.
-
-Theorem curve25519_ladder_really_ok (n : nat) (x:Zmodp.type) :
+  rewrite /GRing.mul /= (Zmodp_ring.mul_comm yp2).
+  symmetry.
+  rewrite -Zmodp_ring.mul_assoc.
+  ringify.
+  apply add_eq_mul2.
+  move/eqP.
+  move/Zmodp2.Zmodp2_inv => [].
+  ringify.
+  move => Hxy.
+  rewrite -GRing.mulrA.
+  move/time_2_eq_0/mult_xy_eq_0 => [] Hy; rewrite Hy in Hxy;
+  move: Hxy ; ring_simplify_this => Hxy.
+  - right.
+  have OC : oncurve twist25519_mcuType (| x, yp2 |).
+    by apply/eqP => /= ; rewrite /twist25519.a /twist25519.b ?expr2 ?expr3' ; ringify.
+  exists (MC OC) => /=.
+  apply mc_eq ; congruence.
+  - left.
+  have OC : oncurve curve25519_mcuType (| x, yp1 |).
+    by apply/eqP => /= ; rewrite /curve25519.a /curve25519.b ?expr2 ?expr3' mul1r; ringify.
+  exists (MC OC) => /=.
+  apply mc_eq ; congruence.
+Qed.
+
+From mathcomp Require Import ssrnat.
+
+Lemma curve25519_ladder_maybe_ok (n : nat) x :
     (n < 2^255)%nat -> x != 0 ->
-    forall (p'  : mc curve25519_Fp2_mcuType),
-    p'#x0 /p = x -> curve25519_ladder n x = (p' *+ n)#x0 /p.
+    forall (p  : mc curve25519_Fp2_mcuType),
+    p #x0 = Zmodp2.Zmodp2 x 0 ->
+    curve25519_ladder n x = (p *+ n)#x0 /p.
 Proof.
-  have : (exists p, curve25519_Fp_to_Fp2 p #x0 /p = x) \/ (exists p, twist25519_Fp_to_Fp2 p #x0 /p = x).
-  have := (x_is_on_curve_or_twist x).
-  move => [[p Hp]|[p Hp]].
-  by left; exists p;  move: p Hp => [[| xp yp] Hp] /=.
-  by right; exists p;  move: p Hp => [[| xp yp] Hp] /=.
-  intros ; apply curve25519_ladder_maybe_ok => //.
+  move => Hn Hx p Hp.
+  have [[c] Hc|[t] Ht] := Fp2_to_Fp x p Hp.
+  + have Hcx0: curve25519_Fp_to_Fp2 c #x0 = Zmodp2.Zmodp2 x 0 by rewrite Hc.
+    rewrite (curve25519_ladder_really_ok n x Hn Hx c Hcx0) -Fp_to_Fp2_eq_C Hc //.
+  + have Htx0: twist25519_Fp_to_Fp2 t #x0 = Zmodp2.Zmodp2 x 0 by rewrite Ht.
+    rewrite curve_twist_eq.
+    rewrite (twist25519_ladder_really_ok n x Hn Hx t Htx0) -Fp_to_Fp2_eq_T Ht //.
 Qed.
 
-
-Close Scope ring_scope.
+Close Scope ring_scope.
\ No newline at end of file

High/opt_ladder.v

@@ -154,4 +154,18 @@ Section OptimizedLadder.
       - by apply: point_x0_neq0_fin; rewrite p_x_eqx.
   Qed.
 
+  Lemma neg_x : forall (p : mc M),
+    p#x0 = (-p)#x0.
+  Proof.
+    move=> [[|xp yp] Hp] //=.
+  Qed.
+
+  Lemma neg_x_n : forall (n:nat) (p : mc M),
+    (p *+ n)#x0 = ((-p) *+ n)#x0.
+  Proof.
+    move => n p.
+    rewrite GRing.mulNrn.
+    apply neg_x.
+  Qed.
+
 End OptimizedLadder.

High/twist_incl_Fp2.v

@@ -153,12 +153,13 @@ From mathcomp Require Import ssrnat.
 Theorem twist25519_ladder_really_ok (n : nat) x :
     (n < 2^255)%nat -> x != 0 ->
     forall (p  : mc twist25519_mcuType),
-    (twist25519_Fp_to_Fp2 p)#x0 /p = x -> twist25519_ladder n x = ((twist25519_Fp_to_Fp2 p) *+ n)#x0 /p.
+    twist25519_Fp_to_Fp2 p #x0 = Zmodp2.Zmodp2 x 0 ->
+    twist25519_ladder n x = ((twist25519_Fp_to_Fp2 p) *+ n)#x0 /p.
 Proof.
   move => Hn Hx p Hp.
   have Hp' := tFp_to_Fp2_cancel p.
   have Hp'' : p #x0 = x.
-  by rewrite Hp'.
+    rewrite Hp' Hp //.
   rewrite (twist25519_ladder_ok n x Hn Hx p Hp'').
   rewrite -nP_is_nP2.
   rewrite tFp_to_Fp2_cancel //.