Commit 09970ac6 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

fixes names

parent aa0a1f9a
......@@ -2,7 +2,7 @@ Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg.
Require Import ZArith ZArith.Znumtheory.
From Tweetnacl.High Require Import curve25519_prime_cert.
From Tweetnacl.High Require Import prime_cert.
Set Implicit Arguments.
Unset Strict Implicit.
......
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg finfield prime.
Require Import ZArith ZArith.Znumtheory.
From Tweetnacl.High Require Import curve25519_prime Zmodp Zmodp_Ring prime_ssrprime.
From mathcomp Require Import galois.
From mathcomp Require Import fintype ssralg finalg.
Require Import ZArith.
From Tweetnacl.High Require Import Zmodp Zmodp_Ring.
Set Implicit Arguments.
Unset Strict Implicit.
......@@ -280,9 +279,6 @@ apply/eqP; rewrite eqE; apply/eqP=> /=.
apply: esym. f_equal; apply val_inj => /=.
Qed.
Fact Hp_prime : prime p.
Proof. by unlock p; apply: primo. Qed.
Inductive Zinv_spec (x : type) : Type :=
| Zinv_spec_zero : x = zero -> Zinv_spec x
| Zinv_spec_unit : x <> zero -> forall y, (y * x)%R = one -> Zinv_spec x.
......
......@@ -2,11 +2,8 @@ Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg.
Require Import ZArith ZArith.Znumtheory.
From Tweetnacl.High Require Import curve25519_prime_cert.
From Tweetnacl.High Require Import curve25519_prime.
From Tweetnacl.High Require Import prime_ssrprime.
From Tweetnacl.High Require Import prime_and_legendre Zmodp.
From Reciprocity Require Import Reciprocity.Reciprocity.
From Tweetnacl.High Require Import Zmodp.
Import BinInt.
Require Import Ring.
......
......@@ -2,17 +2,12 @@ Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div ssralg.
From Tweetnacl.High Require Import mc.
From Tweetnacl.High Require Import mcgroup.
From Tweetnacl.High Require Import ladder.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import Zmodp_Ring.
From Tweetnacl.High Require Import opt_ladder.
From Tweetnacl.High Require Import montgomery.
From Tweetnacl.High Require Import curve25519_prime.
From Tweetnacl.High Require Import prime_ssrprime.
From Reciprocity Require Import Reciprocity.Reciprocity.
Import BinInt.
Require Import Ring.
Open Scope ring_scope.
Import GRing.Theory.
......@@ -25,40 +20,33 @@ Proof. by rewrite expr2 ; zmodp_compute. Qed.
Lemma b_neq0 : b != 0.
Proof. exact: oner_neq0. Qed.
Canonical Structure curve25519_mcuType := Build_mcuType b_neq0 asq_neq4.
Canonical Structure curve25519_Fp_mcuType := Build_mcuType b_neq0 asq_neq4.
Lemma curve25519_chi2 : 2%:R != 0 :> Zmodp.type.
Lemma curve25519_Fp_chi2 : 2%:R != 0 :> Zmodp.type.
Proof. by zmodp_compute. Defined.
Lemma curve25519_chi3 : 3%:R != 0 :> Zmodp.type.
Lemma curve25519_Fp_chi3 : 3%:R != 0 :> Zmodp.type.
Proof. by zmodp_compute. Defined.
Definition curve25519_ecuFieldMixin :=
ECUFieldMixin curve25519_chi2 curve25519_chi3.
Canonical Structure curve25519_ecuFieldType :=
Eval hnf in ECUFieldType Zmodp.type curve25519_ecuFieldMixin.
Canonical Structure curve25519_finECUFieldType :=
Definition curve25519_Fp_ecuFieldMixin :=
ECUFieldMixin curve25519_Fp_chi2 curve25519_Fp_chi3.
Canonical Structure curve25519_Fp_ecuFieldType :=
Eval hnf in ECUFieldType Zmodp.type curve25519_Fp_ecuFieldMixin.
Canonical Structure curve25519_Fp_finECUFieldType :=
Eval hnf in [finECUFieldType of Zmodp.type].
Definition curve25519_ladder n x :=
@opt_montgomery curve25519_finECUFieldType curve25519_mcuType n 255 x.
Definition curve25519_Fp_ladder n x :=
opt_montgomery curve25519_Fp_mcuType n 255 x.
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Theorem curve25519_ladder_ok (n : nat) x :
Theorem curve25519_Fp_ladder_ok (n : nat) x :
(n < 2^255)%nat ->
forall (p : mc curve25519_mcuType), p#x0 = x -> curve25519_ladder n x = (p *+ n)#x0.
forall (p : mc curve25519_Fp_mcuType), p#x0 = x -> curve25519_Fp_ladder n x = (p *+ n)#x0.
Proof.
move => Hn p Hp.
rewrite /curve25519_ladder.
rewrite /curve25519_Fp_ladder.
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
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div ssralg.
From Tweetnacl.High Require Import mc.
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.
From Tweetnacl.High Require Import prime_ssrprime.
From Reciprocity Require Import Reciprocity.Reciprocity.
Import BinInt.
Open Scope ring_scope.
......@@ -57,44 +49,3 @@ Canonical Structure curve25519_Fp2_ecuFieldType :=
Eval hnf in ECUFieldType Zmodp2.type curve25519_Fp2_ecuFieldMixin.
Canonical Structure curve25519_Fp2_finECUFieldType :=
Eval hnf in [finECUFieldType of Zmodp2.type].
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 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.
\ No newline at end of file
......@@ -3,16 +3,12 @@ From mathcomp Require Import ssreflect ssrbool eqtype div ssralg.
From Tweetnacl.High Require Import mc.
From Tweetnacl.High Require Import mcgroup.
From Tweetnacl.High Require Import montgomery.
From Tweetnacl.High Require Import curve25519.
From Tweetnacl.High Require Import twist25519.
From Tweetnacl.High Require Import curve25519_Fp.
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 Zmodp2.
From Tweetnacl.High Require Import Zmodp2_rules.
From Tweetnacl.High Require Import curve25519_Fp2.
From Tweetnacl.High Require Import curve25519_twist25519_eq.
From Tweetnacl.High Require Import curve25519_Fp_twist25519_Fp_eq.
From Tweetnacl.High Require Import Zmodp.
Require Import Ring.
Require Import ZArith.
......@@ -31,29 +27,29 @@ match p with
| EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
end.
Lemma oncurve25519_impl : forall (x y: Zmodp.type),
oncurve curve25519_mcuType (EC_In x y) ->
Lemma oncurve25519_Fp_impl : forall (x y: Zmodp.type),
oncurve curve25519_Fp_mcuType (EC_In x y) ->
(oncurve curve25519_Fp2_mcuType (EC_In (Zmodp2.pi (x, Zmodp.pi 0)) (Zmodp2.pi (y, Zmodp.pi 0)))).
Proof.
move => x y /=.
rewrite /a /b.
rewrite ?expr2 ?expr3 ?expr3'.
rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
rewrite /curve25519.a /curve25519.b.
rewrite /curve25519_Fp.a /curve25519_Fp.b.
ring_simplify_this.
move/eqP => -> /=.
apply/eqP.
f_equal.
Qed.
Lemma on_curve_Fp_to_Fp2 : forall (p: point Zmodp.type),
oncurve curve25519_mcuType p -> oncurve curve25519_Fp2_mcuType (curve_Fp_to_Fp2 p).
Local Lemma on_curve_Fp_to_Fp2 : forall (p: point Zmodp.type),
oncurve curve25519_Fp_mcuType p -> oncurve curve25519_Fp2_mcuType (curve_Fp_to_Fp2 p).
Proof.
move=> [|x y] => //.
apply oncurve25519_impl.
apply oncurve25519_Fp_impl.
Qed.
Definition curve25519_Fp_to_Fp2 (p: mc curve25519_mcuType) : (mc curve25519_Fp2_mcuType) :=
Definition curve25519_Fp_to_Fp2 (p: mc curve25519_Fp_mcuType) : (mc curve25519_Fp2_mcuType) :=
match p with
| MC u P => MC (on_curve_Fp_to_Fp2 u P)
end.
......@@ -61,10 +57,10 @@ end.
Local Lemma curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
p' = curve_Fp_to_Fp2 p ->
q' = curve_Fp_to_Fp2 q ->
MCGroup.add curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add curve25519_mcuType p q).
MCGroup.add curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add curve25519_Fp_mcuType p q).
Proof.
move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //= [] -> -> [] -> ->.
rewrite /curve25519.a /curve25519.b.
rewrite /curve25519_Fp.a /curve25519_Fp.b.
match goal with
| [ |- _ = ?A ] => remember A as Freezer
end.
......@@ -82,10 +78,10 @@ Proof.
case_eq ((yp == yq) && (yp != 0)) => -> //=.
Qed.
Local Lemma curve25519_add_Fp_to_Fp2' : forall (p q: mc curve25519_mcuType) (p' q': mc curve25519_Fp2_mcuType),
Local Lemma curve25519_add_Fp_to_Fp2' : forall (p q: mc curve25519_Fp_mcuType) (p' q': mc curve25519_Fp2_mcuType),
p' = curve25519_Fp_to_Fp2 p ->
q' = curve25519_Fp_to_Fp2 q ->
MCGroup.add curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add curve25519_mcuType p q).
MCGroup.add curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add curve25519_Fp_mcuType p q).
Proof.
move => [p Hp] [q Hq] [p' Hp'] [q' Hq'] Hpp' Hqq'.
apply curve_add_Fp_to_Fp2.
......@@ -93,7 +89,7 @@ Proof.
by simpl in Hqq'; inversion Hqq'.
Qed.
Lemma curve25519_add_Fp_to_Fp2: forall (p q: mc curve25519_mcuType),
Local Lemma curve25519_add_Fp_to_Fp2: forall (p q: mc curve25519_Fp_mcuType),
curve25519_Fp_to_Fp2 p + curve25519_Fp_to_Fp2 q = curve25519_Fp_to_Fp2 (p + q).
Proof.
move => p q.
......@@ -105,7 +101,7 @@ Proof.
reflexivity.
Qed.
Lemma nP_is_nP2 : forall (n:nat) (p: mc curve25519_mcuType),
Lemma nP_is_nP2 : forall (n:nat) (p: mc curve25519_Fp_mcuType),
curve25519_Fp_to_Fp2 (p *+ n) = (curve25519_Fp_to_Fp2 p) *+n.
Proof.
elim => [|n IHn] p.
......@@ -119,7 +115,7 @@ Definition cFp_to_Fp2 p := match p with
| Zmodp2.Zmodp2 x y => x
end.
Lemma cFp_to_Fp2_cancel : forall p: mc curve25519_mcuType,
Lemma cFp_to_Fp2_cancel : forall p: mc curve25519_Fp_mcuType,
p#x0 = cFp_to_Fp2 ((curve25519_Fp_to_Fp2 p)#x0).
Proof. by case ; case. Qed.
......@@ -127,17 +123,17 @@ Local Notation "p '/p'" := (cFp_to_Fp2 p) (at level 40).
From mathcomp Require Import ssrnat.
Theorem curve25519_ladder_really_ok (n : nat) x :
Theorem curve25519_ladder_Fp_Fp2 (n : nat) x :
(n < 2^255)%nat ->
forall (p : mc curve25519_mcuType),
forall (p : mc curve25519_Fp_mcuType),
(curve25519_Fp_to_Fp2 p)#x0 = Zmodp2.Zmodp2 x 0 ->
curve25519_ladder n x = ((curve25519_Fp_to_Fp2 p) *+ n)#x0 /p.
curve25519_Fp_ladder n x = ((curve25519_Fp_to_Fp2 p) *+ n)#x0 /p.
Proof.
move => Hn p Hp.
have Hp' := cFp_to_Fp2_cancel p.
have Hp'' : p #x0 = x.
move: Hp'; rewrite Hp => //=.
rewrite (curve25519_ladder_ok n x Hn p Hp'').
rewrite (curve25519_Fp_ladder_ok n x Hn p Hp'').
rewrite -nP_is_nP2.
rewrite cFp_to_Fp2_cancel //.
Qed.
......
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrbool eqtype div ssralg.
From mathcomp Require Import ssreflect ssrbool eqtype ssralg.
From Tweetnacl.High Require Import mc.
From Tweetnacl.High Require Import mcgroup.
From Tweetnacl.High Require Import montgomery.
From Tweetnacl.High Require Import curve25519.
From Tweetnacl.High Require Import twist25519.
From Tweetnacl.High Require Import montgomery. (* point_x0 *)
From Tweetnacl.High Require Import curve25519_Fp.
From Tweetnacl.High Require Import twist25519_Fp.
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.
From Tweetnacl.High Require Import Zmodp_Ring.
Require Import ZArith.
......@@ -17,32 +13,32 @@ Import BinInt.
Open Scope ring_scope.
Import GRing.Theory.
Theorem curve_twist_eq: forall n x,
curve25519_ladder n x = twist25519_ladder n x.
Theorem curve25519_twist25519_Fp_eq: forall n x,
curve25519_Fp_ladder n x = twist25519_Fp_ladder n x.
Proof.
move => n x.
rewrite /curve25519_ladder /twist25519_ladder /opt_montgomery.
rewrite /curve25519_Fp_ladder /twist25519_Fp_ladder /opt_montgomery.
elim 255 => //.
Qed.
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Lemma x_is_on_curve_or_twist: forall x,
(exists (p : mc curve25519_mcuType), p#x0 = x) \/
(exists (p' : mc twist25519_mcuType), p'#x0 = x).
(exists (p : mc curve25519_Fp_mcuType), p#x0 = x) \/
(exists (p' : mc twist25519_Fp_mcuType), p'#x0 = x).
Proof.
move => x.
have := x_square_minus_x (x^+3 + (Zmodp.pi 486662) * x^+2 + x)%R.
move => [] y [Hy|Hy] ; [left|right].
+{
have OC : (oncurve curve25519_mcuType (EC_In x y)).
simpl; rewrite /curve25519.b /curve25519.a.
have OC : (oncurve curve25519_Fp_mcuType (EC_In x y)).
simpl; rewrite /curve25519_Fp.b /curve25519_Fp.a.
have ->: (1 * y ^+ 2 = y ^+ 2)%R by apply Zmodp_ring.mul_left_id.
apply/eqP => //.
exists (MC OC) => //.
}
+{
have OC : (oncurve twist25519_mcuType (EC_In x y)).
have OC : (oncurve twist25519_Fp_mcuType (EC_In x y)).
simpl; rewrite /b /a.
apply/eqP => //.
exists (MC OC) => //.
......
......@@ -3,18 +3,18 @@ From mathcomp Require Import ssreflect ssrbool eqtype div ssralg.
From Tweetnacl.High Require Import mc.
From Tweetnacl.High Require Import mcgroup.
From Tweetnacl.High Require Import montgomery.
From Tweetnacl.High Require Import curve25519.
From Tweetnacl.High Require Import twist25519.
From Tweetnacl.High Require Import curve25519_Fp.
From Tweetnacl.High Require Import twist25519_Fp.
From Tweetnacl.High Require Import opt_ladder.
From Tweetnacl.High Require Import curve25519_prime.
From Tweetnacl.High Require Import prime_and_legendre.
From Tweetnacl.High Require Import prime_ssrprime.
From Reciprocity Require Import Reciprocity.Reciprocity.
From Tweetnacl.High Require Import Zmodp2.
From Tweetnacl.High Require Import Zmodp2_rules.
From Tweetnacl.High Require Import curve25519_Fp2.
From Tweetnacl.High Require Import curve25519_twist25519_eq.
From Tweetnacl.High Require Import curve_incl_Fp2.
From Tweetnacl.High Require Import twist_incl_Fp2.
From Tweetnacl.High Require Import curve25519_Fp_twist25519_Fp_eq.
From Tweetnacl.High Require Import curve25519_Fp_incl_Fp2.
From Tweetnacl.High Require Import twist25519_Fp_incl_Fp2.
From Tweetnacl.High Require Import Zmodp.
Require Import Ring.
Require Import ZArith.
......@@ -33,24 +33,24 @@ Proof.
f_equal; f_equal; apply/eqP ; zmodp_compute => //=.
Qed.
Local Lemma oncurve25519 : forall x k k0 : Zmodp.type,
curve25519.b * k0 ^+ 2 == k ^+ 3 + curve25519.a * k ^+ 2 + k ->
Local Lemma oncurve25519_Fp : forall x k k0 : Zmodp.type,
curve25519_Fp.b * k0 ^+ 2 == k ^+ 3 + curve25519_Fp.a * k ^+ 2 + k ->
k = x -> exists p0 : mc curve25519_Fp2_mcuType, p0 #x0 = Zmodp2.Zmodp2 x 0.
Proof.
move => x k k' Hx <-. clear x.
have : oncurve curve25519_mcuType (EC_In k k') => //.
move/oncurve25519_impl => HOC.
have : oncurve curve25519_Fp_mcuType (EC_In k k') => //.
move/oncurve25519_Fp_impl => HOC.
exists (MC HOC) => /=.
have ->: Zmodp.pi 0 = Zmodp.zero => //=.
Qed.
Local Lemma ontwist25519 : forall x k k0 : Zmodp.type,
twist25519.b * k0 ^+ 2 == k ^+ 3 + twist25519.a * k ^+ 2 + k ->
Local Lemma ontwist25519_Fp : forall x k k0 : Zmodp.type,
twist25519_Fp.b * k0 ^+ 2 == k ^+ 3 + twist25519_Fp.a * k ^+ 2 + k ->
k = x -> exists p0 : mc curve25519_Fp2_mcuType, p0 #x0 = Zmodp2.Zmodp2 x 0.
Proof.
move => x k k' Hx <-. clear x.
have : oncurve twist25519_mcuType (EC_In k k') => //.
move/ontwist25519_impl => HOC.
have : oncurve twist25519_Fp_mcuType (EC_In k k') => //.
move/ontwist25519_Fp_impl => HOC.
exists (MC HOC) => /=.
have ->: Zmodp.pi 0 = Zmodp.zero => //=.
Qed.
......@@ -63,9 +63,9 @@ Proof.
have := x_is_on_curve_or_twist x.
move=> [] [] [] [] /=.
- move=> _ <- ; exists (MC oncurve_00) => //=.
- apply oncurve25519.
- apply oncurve25519_Fp.
- move=> _ <- ; exists (MC oncurve_00) => //=.
- apply ontwist25519.
- apply ontwist25519_Fp.
Qed.
Definition Fp_to_Fp2 p := match p with
......@@ -80,68 +80,73 @@ Proof. reflexivity. Qed.
Local Notation "p '/p'" := (Fp_to_Fp2 p) (at level 40).
Local Lemma temp: forall x xp yp1 yp2,
xp = Zmodp2.Zmodp2 x 0 ->
oncurve curve25519_Fp2_mcuType (|xp, Zmodp2.Zmodp2 yp1 yp2|) ->
yp1 ^+ 2 + 2%:R * yp2 ^+ 2 = x * x * x + Zmodp.pi 486662 * (x * x) + x /\
2%:R * (yp1 * yp2) = 0.
Proof.
move => x xp yp1 yp2 Hx.
rewrite /oncurve /= /a /b => Hp'.
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; 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: Hxy.
done.
Qed.
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).
(exists c:mc curve25519_Fp_mcuType, curve25519_Fp_to_Fp2 c = p) \/ (exists t:mc twist25519_Fp_mcuType, twist25519_Fp_to_Fp2 t = p).
Proof.
move => x [[|xp yp] Hp].
move => x [[|xp yp] Hp] /= => Hx.
+ (* is p is at infinity *)
move => _ ; left.
have Hc : oncurve curve25519_mcuType => //=.
left; have Hc : oncurve curve25519_Fp_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.
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.
have [Hxy] := temp x xp yp1 yp2 Hx Hp.
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.
have OC : oncurve twist25519_Fp_mcuType (| x, yp2 |).
by apply/eqP => /= ; rewrite /twist25519_Fp.a /twist25519_Fp.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.
have OC : oncurve curve25519_Fp_mcuType (| x, yp1 |).
by apply/eqP => /= ; rewrite /curve25519_Fp.a /curve25519_Fp.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:Zmodp.type) :
Lemma curve25519_Fp2_ladder_ok (n : nat) (x:Zmodp.type) :
(n < 2^255)%nat ->
forall (p : mc curve25519_Fp2_mcuType),
p #x0 = Zmodp2.Zmodp2 x 0 ->
curve25519_ladder n x = (p *+ n)#x0 /p.
curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
Proof.
move => Hn 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 c Hcx0) -Fp_to_Fp2_eq_C Hc //.
rewrite (curve25519_ladder_Fp_Fp2 n x Hn 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 t Htx0) -Fp_to_Fp2_eq_T Ht //.
rewrite curve25519_twist25519_Fp_eq.
rewrite (twist25519_ladder_Fp_Fp2 n x Hn t Htx0) -Fp_to_Fp2_eq_T Ht //.
Qed.
Close Scope ring_scope.
\ No newline at end of file
From Tweetnacl Require Import Libs.Export.
From Tweetnacl.High Require Import Zmodp opt_ladder curve25519 curve25519_prime prime_ssrprime.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import prime_and_legendre.
From Tweetnacl.High Require Import prime_ssrprime.
From mathcomp Require Import ssreflect ssrbool eqtype ssralg prime div.
From Tweetnacl Require Import Mod.
......
From Coqprime Require Import PocklingtonRefl.
From mathcomp Require Import ssreflect ssrbool prime.
From Tweetnacl.High Require Export curve25519_prime_cert prime_ssrprime.
From Tweetnacl.High Require Export prime_cert prime_ssrprime.
Local Open Scope positive_scope.
Require Import Znat.
......
......@@ -2,14 +2,10 @@ Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div ssralg.
From Tweetnacl.High Require Import mc.
From Tweetnacl.High Require Import mcgroup.
From Tweetnacl.High Require Import ladder.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import Zmodp_Ring.
From Tweetnacl.High Require Import opt_ladder.
From Tweetnacl.High Require Import montgomery.
From Tweetnacl.High Require Import curve25519_prime.
From Tweetnacl.High Require Import prime_ssrprime.
From Reciprocity Require Import Reciprocity.Reciprocity.
Import BinInt.
Open Scope ring_scope.
......@@ -24,32 +20,32 @@ Proof. by rewrite expr2; zmodp_compute. Qed.