Commit 585723d4 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add proof x is either on curve or twist

parent 3b55aafb
......@@ -128,6 +128,29 @@ Proof. apply: val_inj. apply: modZp. Qed.
Lemma piK (x : Z) : betweenb 0 p x -> repr (pi x) = x.
Proof. by move/betweenbP=> Hx /=; apply: Zmod_small. Qed.
Lemma x_eq_0 : forall x:Z,
0 <= x < p -> x <> 0 -> x mod p <> 0.
Proof.
move=> x Hx Hx' Hx''.
apply:Hx'.
move: Hx''.
rewrite Z.mod_divide; last by rewrite /p -lock.
move => Hx'.
rewrite -(Zmod_small x p Hx).
by apply Zdivide_mod.
Qed.
Lemma oppZ (x:Z) : betweenb 0 p x -> repr (pi (-x)) = (- (pi x)) mod p.
Proof. move/betweenbP=> Hx /=.
have := Z.eq_dec x 0.
move => [].
+ move => -> //=.
+ move => Hx'.
rewrite Z_mod_nz_opp_full ; last by apply x_eq_0 => //=.
rewrite Z_mod_nz_opp_full ; last by rewrite Zmod_mod; apply x_eq_0 => //=.
rewrite Zmod_mod //.
Qed.
Module Zmodp_finite.
Definition pn := Z.to_nat p.
......@@ -415,6 +438,7 @@ Export Zmodp_field.Exports.
Import GRing.Theory.
Lemma Zmodp_ring : ring_theory zero one add mul sub opp eq.
Proof.
apply mk_rt.
......@@ -429,4 +453,34 @@ apply Zmodp_zmod.add_sub.
move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //.
Defined.
Lemma Zmodp_ringTypeR : @ring_theory Zmodp_ringType zero one add mul sub opp eq.
Proof.
apply mk_rt.
apply Zmodp_zmod.add_left_id.
apply Zmodp_zmod.add_comm.
apply Zmodp_zmod.add_assoc.
apply Zmodp_ring.mul_left_id.
apply Zmodp_ring.mul_comm.
apply Zmodp_ring.mul_assoc.
apply Zmodp_ring.mul_left_distr.
apply Zmodp_zmod.add_sub.
move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //.
Defined.
Add Ring Zmodp_ring : Zmodp_ring.
Add Ring Zmodp_ringType : Zmodp_ringTypeR.
Lemma eq_inv_2 : forall (x m:Zmodp.type), (m = (Zmodp.pi 28948022309329048855892746252171976963317496166410141009864396001978282409975%Z) * x)%R -> ((Zmodp.pi 2) * m = x)%R.
Proof.
move => m x ->.
apply val_inj => /=.
rewrite Z.mul_mod_idemp_l ; last apply Hp_neq0.
rewrite Z.mul_mod_idemp_l ; last apply Hp_neq0.
rewrite Z.mul_mod_idemp_r ; last apply Hp_neq0.
rewrite Z.mul_assoc.
rewrite -Z.mul_mod_idemp_l ; last apply Hp_neq0.
have ->: (2 * 28948022309329048855892746252171976963317496166410141009864396001978282409975) mod p = 1.
rewrite /p -lock //.
rewrite Z.mul_1_l.
apply modZp.
Qed.
\ No newline at end of file
......@@ -26,10 +26,10 @@ Proof. exact: oner_neq0. Qed.
Canonical Structure curve25519_mcuType := Build_mcuType b_neq0 asq_neq4.
Lemma curve25519_chi2 : 2%:R != 0 :> Zmodp.type.
Proof. by zmodp_compute. Qed.
Proof. by zmodp_compute. Defined.
Lemma curve25519_chi3 : 3%:R != 0 :> Zmodp.type.
Proof. by zmodp_compute. Qed.
Proof. by zmodp_compute. Defined.
Definition curve25519_ecuFieldMixin :=
ECUFieldMixin curve25519_chi2 curve25519_chi3.
......
......@@ -42,3 +42,14 @@ Proof.
rewrite -Zpow_mod_correct -lock ; vm_compute ; congruence.
Qed.
Lemma legendre_compute2:
(-1 mod (2 ^ 255 - 19))%Z = (2 mod (2 ^ 255 - 19)) ^ ((locked (2 ^ 255 - 19)%Z - 1) / 2) mod locked (2 ^ 255 - 19)%Z.
Proof.
rewrite -Zpow_mod_correct -lock ; vm_compute ; congruence.
Qed.
Lemma legendre_compute28948022309329048855892746252171976963317496166410141009864396001978282409975:
(-1 mod (2 ^ 255 - 19))%Z = (28948022309329048855892746252171976963317496166410141009864396001978282409975 mod (2 ^ 255 - 19)) ^ ((locked (2 ^ 255 - 19)%Z - 1) / 2) mod locked (2 ^ 255 - 19)%Z.
Proof.
rewrite -Zpow_mod_correct -lock ; vm_compute ; congruence.
Qed.
Set Warnings "-notation-overridden,-parsing".
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 opt_ladder.
From Tweetnacl.High Require Import curve25519_prime.
From Tweetnacl.High Require Import prime_ssrprime.
From Reciprocity Require Import Reciprocity.Reciprocity.
Require Import ZArith.
Import BinInt.
Open Scope ring_scope.
Import GRing.Theory.
Theorem curve_twist_eq: forall n x,
curve25519_ladder n x = twist25519_ladder n x.
Proof.
move => n x.
rewrite /curve25519_ladder /twist25519_ladder /opt_montgomery.
elim 255 => //.
Qed.
From Tweetnacl.High Require Import Zmodp.
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 x_square_minus_x: forall (x:Zmodp.type),
exists (y:Zmodp.type), (y^+2 = x \/ (Zmodp.pi 2)* y^+2 = x)%R.
Proof.
move => x.
have Prime:(Znumtheory.prime Zmodp.p).
rewrite /Zmodp.p -lock ; apply curve25519_numtheory_prime.
have Prime2:= ZmodP_mod2_eq_1.
replace (BinInt.Z.sub (BinInt.Z.pow 2 255) 19) with Zmodp.p in Prime2.
2: rewrite /Zmodp.p -lock //.
have Eulers_Criterion := Eulers_criterion Zmodp.p Prime Prime2 (Zmodp.repr x).
rewrite /legendre in Eulers_Criterion.
destruct (ClassicalDescription.excluded_middle_informative _).
+ exists Zmodp.zero.
left.
have ->: Zmodp.zero ^+2 = Zmodp.zero => //.
move/modZp0/eqP:e -> => //.
+ destruct (ClassicalDescription.excluded_middle_informative _).
move: e => [y Hy].
exists (Zmodp.pi y).
left.
apply val_inj => /=.
move: Hy.
rewrite modZp => <-.
rewrite Z.mul_mod_idemp_l; last by rewrite /p -lock.
rewrite Z.mul_mod_idemp_r; last by rewrite /p -lock.
f_equal ; ring.
+ (* Okayyyy So we cannot *create* y, thus we will have to redo it. *)
have Eulers_Criterion2 := Eulers_criterion Zmodp.p Prime Prime2 (28948022309329048855892746252171976963317496166410141009864396001978282409975 * (Zmodp.repr x)).
rewrite /legendre in Eulers_Criterion2.
destruct (ClassicalDescription.excluded_middle_informative _).
* exfalso.
clear Eulers_Criterion Eulers_Criterion2 n0 Prime2.
rewrite modZp in n.
have HP : 0 <= (Z.R x) < p by rewrite -modZp ; apply Z.mod_pos_bound ; rewrite /p -lock.
move: n.
have Hp : p <> 0 by rewrite /p -lock.
have : Znumtheory.rel_prime p 28948022309329048855892746252171976963317496166410141009864396001978282409975.
apply Znumtheory.rel_prime_sym.
apply Znumtheory.rel_prime_le_prime => //=.
by rewrite /p -lock.
move: e.
move/(Znumtheory.Zmod_divide (28948022309329048855892746252171976963317496166410141009864396001978282409975 * Z.R x) p Hp).
move/Znumtheory.Gauss.
move=> H/H.
move/Znumtheory.Zdivide_bounds.
move=> H'/H'.
have ->: Z.abs p = p by rewrite /p -lock.
have ->: Z.abs (Z.R x) = (Z.R x).
rewrite Z.abs_eq_iff; omega.
move => H''.
omega.
* destruct (ClassicalDescription.excluded_middle_informative _).
clear Eulers_Criterion Eulers_Criterion2 n0 Prime2.
move: e => [y Hy].
exists (Zmodp.pi y).
right.
apply eq_inv_2.
apply val_inj => /=.
rewrite Z.mul_mod_idemp_l; last by rewrite /p -lock.
rewrite Z.mul_mod_idemp_r; last by rewrite /p -lock.
move: Hy.
have ->: y^2 = y*y by ring.
have ->: 28948022309329048855892746252171976963317496166410141009864396001978282409975 mod p = 28948022309329048855892746252171976963317496166410141009864396001978282409975 => //.
by rewrite /p -lock.
* exfalso.
have Hp : p <> 0 by rewrite /p -lock.
clear n0 n1 n2.
move: Eulers_Criterion2.
rewrite Z.pow_mul_l.
rewrite -Zmult_mod_idemp_l.
rewrite -Zmult_mod_idemp_r.
rewrite -Eulers_Criterion.
clear n Prime2 Prime Eulers_Criterion.
have <-: -1 mod p = 28948022309329048855892746252171976963317496166410141009864396001978282409975 ^ ((p - 1) / 2) mod p.
rewrite /p.
have Hn : 0 < locked (2 ^ 255 - 19) by rewrite -lock.
have := legendre_compute28948022309329048855892746252171976963317496166410141009864396001978282409975.
have := Zpow_facts.Zpower_mod 28948022309329048855892746252171976963317496166410141009864396001978282409975 ((locked (2 ^ 255 - 19) - 1) / 2) (locked (2 ^ 255 - 19)) Hn.
rewrite -lock.
remember (28948022309329048855892746252171976963317496166410141009864396001978282409975 ^ ((2 ^ 255 - 19 - 1) / 2) mod (2 ^ 255 - 19)) as m.
remember ((28948022309329048855892746252171976963317496166410141009864396001978282409975 mod (2 ^ 255 - 19)) ^ ((2 ^ 255 - 19 - 1) / 2) mod (2 ^ 255 - 19)) as m'.
remember (-1 mod (2 ^ 255 - 19)) as m''.
clear Heqm Heqm' Heqm''.
move => -> -> //.
rewrite /p -lock; compute ; congruence.
Qed.
Lemma x_is_on_curve_or_twist: forall x,
(* (x != 0)%R -> *)
(exists (p : mc curve25519_mcuType), p#x0 = x) \/
(exists (p' : mc twist25519_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 ->: (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)).
simpl; rewrite /b /a.
apply/eqP => //.
exists (MC OC) => //.
}
Qed.
......@@ -15,7 +15,7 @@ Open Scope ring_scope.
Import GRing.Theory.
Definition a : Zmodp.type := Zmodp.pi 486662.
Definition b : Zmodp.type := -1%R.
Definition b : Zmodp.type := Zmodp.pi 2.
Lemma asq_neq4 : a^+2 != 4%:R.
Proof. by rewrite expr2; zmodp_compute. Qed.
......@@ -26,10 +26,10 @@ Proof. by rewrite /b; zmodp_compute. Qed.
Canonical Structure twist25519_mcuType := Build_mcuType b_neq0 asq_neq4.
Lemma twist25519_chi2 : 2%:R != 0 :> Zmodp.type.
Proof. by zmodp_compute. Qed.
Proof. by zmodp_compute. Defined.
Lemma twist25519_chi3 : 3%:R != 0 :> Zmodp.type.
Proof. by zmodp_compute. Qed.
Proof. by zmodp_compute. Defined.
Definition twist25519_ecuFieldMixin :=
ECUFieldMixin twist25519_chi2 twist25519_chi3.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment