QED

High/Zmodp2_rules.v

@@ -163,6 +163,16 @@ Lemma Zmodp_mul_comm_2 (a:Zmodp.type) : 2%:R * a = a * 2%:R.
 Proof. by rewrite /GRing.mul /= Zmodp_ring.mul_comm. Qed.
 
 
+
+
+
+
+
+
+
+
+
+
 (*
  * Big rewrite tactic
  *)

High/curve25519.v

@@ -55,3 +55,10 @@ apply opt_montgomery_ok=> //=.
 rewrite /a.
 apply a_not_square.
 Qed.
+
+Lemma curve25519_0 (n : nat) :
+  curve25519_ladder n 0 = 0.
+Proof.
+  rewrite /curve25519_ladder.
+  apply opt_montgomery_0.
+Qed.
\ No newline at end of file

High/curve25519_Fp2.v

@@ -5,6 +5,7 @@ From Tweetnacl.High Require Import mcgroup.
 From Tweetnacl.High Require Import ladder.
 From Tweetnacl.High Require Import Zmodp.
 From Tweetnacl.High Require Import Zmodp2.
+From Tweetnacl.High Require Import Zmodp2_rules.
 From Tweetnacl.High Require Import opt_ladder.
 From Tweetnacl.High Require Import montgomery.
 From Tweetnacl.High Require Import curve25519_prime.
@@ -62,6 +63,72 @@ Definition curve25519_Fp2_ladder n x :=
 
 Local Notation "p '#x0'" := (point_x0 p) (at level 30).
 
+Lemma oncurve_0_0: oncurve curve25519_Fp2_mcuType (|0%:R ,0%:R|).
+Proof. move => /=. rewrite /b /a.
+have -> : Zmodp2.pi (1,0) = 1%:R => //=.
+Zmodpify => /= ; ringify => /= ; ring_simplify_this.
+Qed.
+
+Lemma oncurve_inf: oncurve curve25519_Fp2_mcuType ∞.
+Proof. done. Qed.
+
+Lemma p_x0_0_impl : forall p: mc curve25519_Fp2_mcuType,
+  p #x0 = 0%:R ->
+  p = MC oncurve_0_0 \/ p = MC oncurve_inf.
+Proof.
+  move => [] [p Hp|xp yp Hp] => /=.
+  + by right ; apply mc_eq.
+  + move => Hxp.
+  left ; apply mc_eq.
+  move: Hxp Hp -> => /=.
+  rewrite /a /b.
+  have -> : Zmodp2.pi (1,0) = 1%:R => //=.
+  Zmodpify => /= ; ringify => /= ; ring_simplify_this.
+  have ->: Zmodp2.Zmodp2 0 0 = 0%:R => //=.
+  by rewrite mulf_eq0; move /orP => []/eqP ->.
+Qed.
+
+Lemma n_inf : forall n p,
+  p = MC oncurve_inf -> 
+  p *+ n = MC oncurve_inf.
+Proof.
+  move => n p.
+  have ->: MC (M:=curve25519_Fp2_mcuType) (p:=∞) oncurve_inf = 0.
+  by rewrite /0 => /= ; apply mc_eq.
+  move => ->.
+  apply mul0rn.
+Qed.
+
+Lemma eq_0_0_0_0_inf : forall x y z,
+  x = MC oncurve_0_0 ->
+  y = MC oncurve_0_0 ->
+  z = MC oncurve_inf ->
+  x + y = z.
+Proof. by move => x y z -> -> ->; rewrite /GRing.add /= ; apply mc_eq. Qed.
+
+Lemma eq_0_0_inf_0_0 : forall x y z,
+  x = MC oncurve_0_0 ->
+  y = MC oncurve_inf ->
+  z = MC oncurve_0_0 ->
+  x + y = z.
+Proof. by move => x y z -> -> ->; rewrite /GRing.add /= ; apply mc_eq. Qed.
+
+Lemma p_x0_0_eq_0 : forall (n:nat) (p: mc curve25519_Fp2_mcuType),
+  p #x0 = 0%:R ->
+  (p *+ n) #x0 = 0%R.
+Proof.
+  elim => [| n IHn] => p.
+  move => _ ; rewrite mulr0n => //=.
+  rewrite mulrS => Hp.
+  have /IHn/p_x0_0_impl := Hp.
+  move => [] ->.
+  all: move/p_x0_0_impl:Hp.
+  all: move => [] ->.
+  all: rewrite /GRing.add //=.
+Qed.
+
+
+(*
 Theorem curve25519_Fp2_ladder_ok (n : nat) (x : Zmodp.type) :
     (n < 2^255)%nat -> x != 0 ->
     forall (p : mc curve25519_Fp2_mcuType), p#x0 = Zmodp2.pi (x, Zmodp.zero) -> curve25519_Fp2_ladder n (Zmodp2.pi (x, Zmodp.zero)) = (p *+ n)#x0.
@@ -71,5 +138,6 @@ rewrite /curve25519_Fp2_ladder.
 apply opt_montgomery_ok=> //=.
 2: by apply/eqP => H ; inversion H ; subst.
 Admitted.
+*)
 (* apply curve25519_residute. *)
 (* Qed. *)

High/curve_incl_Fp2.v

@@ -23,8 +23,6 @@ Open Scope ring_scope.
 Import GRing.Theory.
 
 Local Notation "p '#x0'" := (point_x0 p) (at level 30).
-Local Notation "Z.R A" := (Zmodp.repr A) (at level 30).
-Local Notation "-. A" := (Zmodp.opp A) (at level 30).
 
 (* Conversion between curve25519 over F_p and F_p2 *)
 Definition curve_Fp_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
@@ -84,7 +82,7 @@ Proof.
   case_eq ((yp == yq) && (yp != 0)) => -> //=.
 Qed.
 
-Local Lemma on_curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType),
+(* Local Lemma on_curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType),
   oncurve curve25519_mcuType p ->
   oncurve curve25519_mcuType q ->
    oncurve curve25519_Fp2_mcuType (curve_Fp_to_Fp2 (MCGroup.add curve25519_mcuType p q)).
@@ -97,13 +95,13 @@ Proof.
   have OCq' : oncurve curve25519_Fp2_mcuType q' by subst q' ; apply on_curve_Fp_to_Fp2.
   by apply MCGroup.addO'.
 Qed.
-
-Lemma on_curve25519_add_Fp_to_Fp2: forall (p q: mc curve25519_mcuType),
+ *)
+(* Lemma on_curve25519_add_Fp_to_Fp2: forall (p q: mc curve25519_mcuType),
   oncurve curve25519_Fp2_mcuType (curve25519_Fp_to_Fp2 (p + q)).
 Proof.
   by move => [p Hp] [q Hq] => /=; apply on_curve_add_Fp_to_Fp2.
 Qed.
-
+ *)
 
 Local Lemma curve25519_add_Fp_to_Fp2' : forall (p q: mc curve25519_mcuType) (p' q': mc curve25519_Fp2_mcuType),
   p' = curve25519_Fp_to_Fp2 p ->

High/curve_twist_incl_Fp2.v

@@ -23,8 +23,6 @@ Open Scope ring_scope.
 Import GRing.Theory.
 
 Local Notation "p '#x0'" := (point_x0 p) (at level 30).
-Local Notation "Z.R A" := (Zmodp.repr A) (at level 30).
-Local Notation "-. A" := (Zmodp.opp A) (at level 30).
 
 Lemma oncurve_inf : oncurve curve25519_Fp2_mcuType (EC_Inf Zmodp2.type).
 Proof. done. Defined.
@@ -77,14 +75,10 @@ Definition Fp_to_Fp2 p := match p with
   | Zmodp2.Zmodp2 x y => x
   end.
 
-Lemma Fp_to_Fp2_t : forall p:mc twist25519_mcuType,
-  p#x0 = Fp_to_Fp2 ((twist25519_Fp_to_Fp2 p)#x0).
+Lemma Fp_to_Fp2_t : forall p:mc twist25519_mcuType, p#x0 = Fp_to_Fp2 ((twist25519_Fp_to_Fp2 p)#x0).
 Proof. by case; case. Qed.
-
-Lemma Fp_to_Fp2_c : forall p:mc curve25519_mcuType,
-  p#x0 = Fp_to_Fp2 ((curve25519_Fp_to_Fp2 p)#x0).
+Lemma Fp_to_Fp2_c : forall p:mc curve25519_mcuType, p#x0 = Fp_to_Fp2 ((curve25519_Fp_to_Fp2 p)#x0).
 Proof. by case; case. Qed.
-
 Lemma Fp_to_Fp2_eq_C: Fp_to_Fp2 = cFp_to_Fp2.
 Proof. reflexivity. Qed.
 
@@ -144,18 +138,22 @@ From mathcomp Require Import ssrnat.
 
 Lemma curve25519_ladder_maybe_ok (n : nat) (x:Zmodp.type) :
     (n < 2^255)%nat ->
-    x != 0 ->
     forall (p  : mc curve25519_Fp2_mcuType),
     p #x0 = Zmodp2.Zmodp2 x 0 ->
     curve25519_ladder n x = (p *+ n)#x0 /p.
 Proof.
-  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 //.
+  move => Hn p Hp.
+  have /orP[Hx|Hx] := orNb (x == 0).
+  + 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 //.
+  + move/eqP: Hx Hp => ->.
+    rewrite curve25519_0.
+    have -> : Zmodp2.Zmodp2 0 0 = 0 => //=.
+    move/(p_x0_0_eq_0 n) => -> //.
 Qed.
 
 Close Scope ring_scope.
\ No newline at end of file

High/opt_ladder.v

@@ -168,4 +168,39 @@ Section OptimizedLadder.
     apply neg_x.
   Qed.
 
+Local Ltac ring_simplify_this :=
+  repeat match goal with
+  | _ => rewrite expr2
+  | _ => rewrite exprS
+  | _ => rewrite GRing.mul1r
+  | _ => rewrite GRing.mulr1
+  | _ => rewrite GRing.mul0r
+  | _ => rewrite GRing.mulr0
+  | _ => rewrite GRing.add0r
+  | _ => rewrite GRing.oppr0
+  | _ => rewrite GRing.addr0
+  | _ => done
+end.
+
+
+Lemma opt_montgomery_rec_0 : forall (m n: nat) a b d,
+  opt_montgomery_rec n m 0 a b 0 d = 0.
+Proof.
+  elim => [| m IHm] n a b d /=.
+  + rewrite GRing.invr0 mulr0 //.
+  + have/orP := bitnV n m.
+    move => []/eqP => ->.
+    all: rewrite /cswap => /=.
+    all: ring_simplify_this.
+    all: rewrite addrN.
+    all: ring_simplify_this.
+Qed.
+
+Theorem opt_montgomery_0 (n m: nat):
+  opt_montgomery n m 0 = 0.
+Proof.
+  rewrite /opt_montgomery.
+  apply opt_montgomery_rec_0.
+Qed.
+
 End OptimizedLadder.

High/twist_incl_Fp2.v

@@ -23,8 +23,6 @@ Open Scope ring_scope.
 Import GRing.Theory.
 
 Local Notation "p '#x0'" := (point_x0 p) (at level 30).
-Local Notation "Z.R A" := (Zmodp.repr A) (at level 30).
-Local Notation "-. A" := (Zmodp.opp A) (at level 30).
 
 (* Conversion between twist25519 over F_p and F_p2 *)
 Definition twist_Fp_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
@@ -60,7 +58,6 @@ match p with
   | MC u P => MC (on_twist_Fp_to_Fp2 u P)
 end.
 
-
 Local Lemma twist_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
   p' = twist_Fp_to_Fp2 p ->
   q' = twist_Fp_to_Fp2 q ->
@@ -85,7 +82,7 @@ Proof.
   case_eq ((yp == yq) && (yp != 0)) => -> //=.
 Qed.
 
-Local Lemma on_twist_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType),
+(* Local Lemma on_twist_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType),
   oncurve twist25519_mcuType p ->
   oncurve twist25519_mcuType q ->
    oncurve curve25519_Fp2_mcuType (twist_Fp_to_Fp2 (MCGroup.add twist25519_mcuType p q)).
@@ -105,7 +102,7 @@ Proof.
   by move => [p Hp] [q Hq] => /=; apply on_twist_add_Fp_to_Fp2.
 Qed.
 
-
+ *)
 Local Lemma twist25519_add_Fp_to_Fp2_ : forall (p q: mc twist25519_mcuType) (p' q': mc curve25519_Fp2_mcuType),
   p' = twist25519_Fp_to_Fp2 p ->
   q' = twist25519_Fp_to_Fp2 q ->

Low/Crypto_Scalarmult_.v

@@ -95,5 +95,4 @@ Proof.
   apply curve25519_ladder_maybe_ok => //.
   move: (ZofList 8 n) => N.
   apply Zclamp_istrue.
-  (* YES OF COURSE ! x != 0 !! *)
-Admitted.
+Qed.