Skip to content
GitLab
Commit 3b6dda02 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

WIP

parent 6f8eced2
Hide whitespace changes
Inline Side-by-side
High/Zmodp.v
View file @ 3b6dda02
......@@ -467,8 +467,23 @@ apply Zmodp_zmod.add_sub.
move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //.
Defined.
Lemma Zmodp_GRingSort_ringType : @ring_theory (GRing.Zmodule.sort 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.
Add Ring Zmodp_GRingSort_ringType : Zmodp_GRingSort_ringType.
Lemma eq_inv_2 : forall (x m:Zmodp.type), (m = (Zmodp.pi 28948022309329048855892746252171976963317496166410141009864396001978282409975%Z) * x)%R -> ((Zmodp.pi 2) * m = x)%R.
Proof.
......@@ -485,7 +500,7 @@ rewrite Z.mul_1_l.
apply modZp.
Qed.
Lemma eq_inv_2' : forall (x m:Zmodp.type), ((Zmodp.pi 2) * m = x)%R -> (m = (Zmodp.pi 28948022309329048855892746252171976963317496166410141009864396001978282409975%Z) * x)%R.
(* 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 <-.
apply val_inj => /=.
......@@ -499,4 +514,4 @@ rewrite /p -lock //.
rewrite Z.mul_1_l.
symmetry ;
apply modZp.
Qed.
\ No newline at end of file
Qed. *)
\ No newline at end of file
High/Zmodp2.v
View file @ 3b6dda02
......@@ -380,4 +380,19 @@ apply Zmodp2_zmod.add_sub.
move => x. rewrite Zmodp2_zmod.add_comm Zmodp2_zmod.add_left_inv //.
Defined.
Lemma Zmodp2_ring2 : @ring_theory (GRing.Ring.sort Zmodp2_ringType) Zmodp2.zero Zmodp2.one Zmodp2.add Zmodp2.mul Zmodp2.sub Zmodp2.opp eq.
Proof.
apply mk_rt.
apply Zmodp2_zmod.add_left_id.
apply Zmodp2_zmod.add_comm.
apply Zmodp2_zmod.add_assoc.
apply Zmodp2_ring.mul_left_id.
apply Zmodp2_ring.mul_comm.
apply Zmodp2_ring.mul_assoc.
apply Zmodp2_ring.mul_left_distr.
apply Zmodp2_zmod.add_sub.
move => x. rewrite Zmodp2_zmod.add_comm Zmodp2_zmod.add_left_inv //.
Defined.
Add Ring Zmodp2_ring : Zmodp2_ring.
Add Ring Zmodp2_ring2 : Zmodp2_ring2.
\ No newline at end of file
High/Zmodp_Ring.v 0 → 100644
View file @ 3b6dda02
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 Reciprocity Require Import Reciprocity.Reciprocity.
From Tweetnacl.High Require Import Zmodp.
Import BinInt.
Require Import Ring.
Open Scope ring_scope.
Import GRing.Theory.
Local Lemma a_2_4 : (Zmodp.pi 486662) ^+ 2 - 4%:R = Zmodp.pi 236839902240.
Proof.
rewrite expr2 Zmodp_mulE /= Zmodp_oppE /= /Zmodp.p -lock /= Zmodp_addE //=.
Qed.
Lemma a_not_square (x : Zmodp.type) : x ^+ 2 != (Zmodp.pi 486662) ^+ 2 - 4%:R.
Proof.
rewrite a_2_4.
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 (Zmodp.pi 236839902240)).
rewrite /legendre in Eulers_Criterion.
destruct (ClassicalDescription.excluded_middle_informative _).
- rename e into H.
exfalso.
move: H.
rewrite piK /p -lock //.
- destruct (ClassicalDescription.excluded_middle_informative _).
+ rename e into H.
exfalso.
move: Eulers_Criterion.
rewrite piK /p.
2: rewrite -lock //.
replace (236839902240 ^ ((locked (2 ^ 255 - 19)%Z - 1) / 2) mod locked (2 ^ 255 - 19)%Z)
with ((-1) mod (2^255 - 19)) %Z.
rewrite -lock //=.
apply legendre_compute.
+ rename n0 into H.
apply /negP => Hx.
apply H.
move: Hx.
move /eqP => Hx.
apply (f_equal (fun x => Zmodp.repr x)) in Hx.
exists (Zmodp.repr x).
move: Hx.
rewrite expr2.
rewrite Z.pow_2_r.
rewrite modZp => <- //.
Qed.
Close Scope ring_scope.
High/curve25519.v
View file @ 3b6dda02
......@@ -4,6 +4,7 @@ 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.
......@@ -11,6 +12,7 @@ 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.
......@@ -18,7 +20,7 @@ Definition a : Zmodp.type := Zmodp.pi 486662.
Definition b : Zmodp.type := 1%R.
Lemma asq_neq4 : a^+2 != 4%:R.
Proof. by rewrite expr2; zmodp_compute. Qed.
Proof. by rewrite expr2 ; zmodp_compute. Qed.
Lemma b_neq0 : b != 0.
Proof. exact: oner_neq0. Qed.
......@@ -38,45 +40,6 @@ Canonical Structure curve25519_ecuFieldType :=
Canonical Structure curve25519_finECUFieldType :=
Eval hnf in [finECUFieldType of Zmodp.type].
Lemma curve25519_residute (x : Zmodp.type) : x ^+ 2 != a ^+ 2 - 4%:R.
Proof.
replace (a ^+ 2 - 4%:R) with (Zmodp.pi 236839902240).
2: rewrite /a expr2 Zmodp_mulE /= Zmodp_oppE /= /Zmodp.p -lock /= Zmodp_addE //=.
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 (Zmodp.pi 236839902240)).
rewrite /legendre in Eulers_Criterion.
destruct (ClassicalDescription.excluded_middle_informative _).
- rename e into H.
exfalso.
move: H.
rewrite piK /p -lock //.
- destruct (ClassicalDescription.excluded_middle_informative _).
+ rename e into H.
exfalso.
move: Eulers_Criterion.
rewrite piK /p.
2: rewrite -lock //.
replace (236839902240 ^ ((locked (2 ^ 255 - 19)%Z - 1) / 2) mod locked (2 ^ 255 - 19)%Z)
with ((-1) mod (2^255 - 19)) %Z.
rewrite -lock //=.
apply legendre_compute.
+ rename n0 into H.
apply /negP => Hx.
apply H.
move: Hx.
move /eqP => Hx.
apply (f_equal (fun x => Zmodp.repr x)) in Hx.
exists (Zmodp.repr x).
move: Hx.
rewrite expr2.
rewrite Z.pow_2_r.
rewrite modZp => <- //.
Qed.
Definition curve25519_ladder n x :=
@opt_montgomery curve25519_finECUFieldType curve25519_mcuType n 255 x.
......@@ -89,5 +52,6 @@ Proof.
move => Hn Hx p Hp.
rewrite /curve25519_ladder.
apply opt_montgomery_ok=> //=.
apply curve25519_residute.
rewrite /a.
apply a_not_square.
Qed.
High/curve25519_Fp2.v
View file @ 3b6dda02
......@@ -15,8 +15,8 @@ Import BinInt.
Open Scope ring_scope.
Import GRing.Theory.
Definition a : Zmodp2.type := Zmodp2.piZ (486662, 0%Z).
Definition b : Zmodp2.type := Zmodp2.piZ (1%Z, 0%Z).
Definition a : Zmodp2.type := Zmodp2.pi (Zmodp.pi 486662, 0).
Definition b : Zmodp2.type := Zmodp2.pi (1, 0).
Lemma b_neq0 : b != 0.
Proof. exact: oner_neq0. Qed.
......@@ -58,45 +58,6 @@ Canonical Structure curve25519_Fp2_ecuFieldType :=
Canonical Structure curve25519_Fp2_finECUFieldType :=
Eval hnf in [finECUFieldType of Zmodp2.type].
(* Lemma curve25519_residute (x : Zmodp.type) : x ^+ 2 != a ^+ 2 - 4%:R.
Proof.
replace (a ^+ 2 - 4%:R) with (Zmodp.pi 236839902240).
2: rewrite /a expr2 Zmodp_mulE /= Zmodp_oppE /= /Zmodp.p -lock /= Zmodp_addE //=.
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 (Zmodp.pi 236839902240)).
rewrite /legendre in Eulers_Criterion.
destruct (ClassicalDescription.excluded_middle_informative _).
- rename e into H.
exfalso.
move: H.
rewrite piK /p -lock //.
- destruct (ClassicalDescription.excluded_middle_informative _).
+ rename e into H.
exfalso.
move: Eulers_Criterion.
rewrite piK /p.
2: rewrite -lock //.
replace (236839902240 ^ ((locked (2 ^ 255 - 19)%Z - 1) / 2) mod locked (2 ^ 255 - 19)%Z)
with ((-1) mod (2^255 - 19)) %Z.
rewrite -lock //=.
apply legendre_compute.
+ rename n0 into H.
apply /negP => Hx.
apply H.
move: Hx.
move /eqP => Hx.
apply (f_equal (fun x => Zmodp.repr x)) in Hx.
exists (Zmodp.repr x).
move: Hx.
rewrite expr2.
rewrite Z.pow_2_r.
rewrite modZp => <- //.
Qed. *)
Definition curve25519_Fp2_ladder n x :=
@opt_montgomery curve25519_Fp2_finECUFieldType curve25519_Fp2_mcuType n 255 x.
......
High/curve_twist_incl_Fp2.v
View file @ 3b6dda02
......@@ -13,7 +13,7 @@ From Tweetnacl.High Require Import Zmodp2.
From Tweetnacl.High Require Import curve25519_Fp2.
From Tweetnacl.High Require Import curve25519_twist25519_eq.
From Tweetnacl.High Require Import Zmodp.
Require Import Ring.
Require Import ZArith.
Import BinInt.
......@@ -25,7 +25,7 @@ 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).
Local Lemma expr3 : forall x:Zmodp2.type, (x^+3 = x*x*x)%R.
Local Lemma expr3 : forall x:Zmodp2.type, x^+3 = x*x*x :> Zmodp2.type.
Proof.
move => x; rewrite ?exprSr expr0 GRing.mul1r //.
Qed.
......@@ -38,15 +38,12 @@ Qed.
Local Lemma oncurve_00 : (oncurve curve25519_Fp2_mcuType (EC_In 0 0)).
Proof.
simpl; rewrite /a /b ; apply/eqP.
have ->: (Zmodp2.piZ (1%Z, 0%Z)) = Zmodp2.pi (Zmodp.pi 1, Zmodp.pi 0) => //.
have ->: (Zmodp2.piZ (486662%Z, 0%Z)) = Zmodp2.pi (Zmodp.pi 486662, Zmodp.pi 0) => //.
have ->: (0 ^+ 2)%R = 0 :> Zmodp2.type by rewrite expr2 ?GRing.mulr0.
have ->: (0 ^+ 3)%R = 0 :> Zmodp2.type by rewrite expr3 ?GRing.mulr0.
rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
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 ->
k = x -> exists p0 : mc curve25519_Fp2_mcuType, p0 #x0 = Zmodp2.Zmodp2 x 0.
......@@ -54,8 +51,6 @@ Proof.
move => x k k' Hx <-. clear x.
have OC: (oncurve curve25519_Fp2_mcuType (EC_In (Zmodp2.pi (k, Zmodp.pi 0)) (Zmodp2.pi (k', Zmodp.pi 0)))) => /=.
rewrite /a /b.
have ->: (Zmodp2.piZ (1%Z, 0%Z)) = Zmodp2.pi (Zmodp.pi 1, Zmodp.pi 0) => //.
have ->: (Zmodp2.piZ (486662%Z, 0%Z)) = Zmodp2.pi (Zmodp.pi 486662, Zmodp.pi 0) => //.
rewrite ?expr2 ?expr3.
rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
move: Hx.
......@@ -78,8 +73,6 @@ Proof.
move => x k k' Hx <-. clear x.
have OC: (oncurve curve25519_Fp2_mcuType (EC_In (Zmodp2.pi (k, Zmodp.pi 0)) (Zmodp2.pi (Zmodp.pi 0, k')))) => /=.
rewrite /a /b.
have ->: (Zmodp2.piZ (1%Z, 0%Z)) = Zmodp2.pi (Zmodp.pi 1, Zmodp.pi 0) => //.
have ->: (Zmodp2.piZ (486662%Z, 0%Z)) = Zmodp2.pi (Zmodp.pi 486662, Zmodp.pi 0) => //.
rewrite ?expr2 ?expr3.
rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
move: Hx.
......@@ -105,3 +98,108 @@ Proof.
- move=> _ <- ; exists (MC oncurve_00) => //=.
- apply ontwist25519.
Qed.
(*
Lemma Zmodp2_ring : ring_theory Zmodp2.zero Zmodp2.one Zmodp2.add Zmodp2.mul Zmodp2.sub Zmodp2.opp eq.
Proof.
apply mk_rt.
apply Zmodp2_zmod.add_left_id.
apply Zmodp2_zmod.add_comm.
apply Zmodp2_zmod.add_assoc.
apply Zmodp2_ring.mul_left_id.
apply Zmodp2_ring.mul_comm.
apply Zmodp2_ring.mul_assoc.
apply Zmodp2_ring.mul_left_distr.
apply Zmodp2_zmod.add_sub.
move => x. rewrite Zmodp2_zmod.add_comm Zmodp2_zmod.add_left_inv //.
Defined.
Add Ring Zmodp2_ring : Zmodp2_ring.
*)
Lemma nP_is_nP2 : forall (x1 x2 xs: Zmodp.type),
forall (p1 : mc curve25519_mcuType), p1#x0 = x1 ->
forall (p2 : mc curve25519_mcuType), p2#x0 = x2 ->
(p1 + p2)#x0 = xs ->
forall (p'1: mc curve25519_Fp2_mcuType), p'1#x0 = Zmodp2.Zmodp2 x1 0 ->
forall (p'2: mc curve25519_Fp2_mcuType), p'2#x0 = Zmodp2.Zmodp2 x2 0 ->
(p'1 + p'2)#x0 = Zmodp2.Zmodp2 xs 0.
Proof.
Admitted.
(* move=> x1 x2 xs [p1 OCp1] Hp1
[p2 OCp2] Hp2
[p'1 OCp'1] Hp'1
[p'2 OCp'2] Hp'2 /= ;
rewrite /MCGroup.add ?OCp1 ?OCp2 ?OCp'1 ?OCp'2.
move: p1 OCp1 Hp1 => [|xp1 yp1] OCp1 Hp1.
+{
move => <- //.
move: p'1 OCp'1 Hp'1 => [|xp'1 yp'1] OCp'1 Hp'1.
- move: Hp2 Hp'2 <- => //=.
- move: p'2 OCp'2 Hp'2 => [|xp'2 yp'2] OCp'2 Hp'2 //.
move: Hp1 Hp'1 <- => /= ->.
move: Hp2 Hp'2 => /= -> <- //=.
move: Hp1 Hp'1 => /= <- ->.
case_eq (Zmodp2.Zmodp2 0 0 == xp'2) => eq_xp'2 ; rewrite eq_xp'2 /=.
* move/eqP:eq_xp'2 => eq_xp'2.
case_eq ((yp'1 == yp'2) && (yp'1 != 0)) => eq2 ; rewrite eq2 /=.
rewrite (expr2 (Zmodp2.pi (0,0))).
rewrite ?GRing.mulr0.
rewrite ?GRing.add0r.
rewrite ?GRing.subr0.
move/andb_prop:eq2 => [].
move/eqP ->. move/eqP.
move=> Hyp'2.
move: Hp2 Hp'2 eq_xp'2 => /= -> ->.
move: OCp'2 => /=.
rewrite /b.
move/eqP.
rewrite ?GRing.mulr1.
rewrite ?GRing.mul1r.
move=>HP2 H2'.
inversion H2' as [H]; clear H2'.
move: H HP2. => <-.
SearchAbout (_ == _ = true).
move/andb_prop.
ring.
rewrite Zmodp2_mulE /=.
rewrite /GRing.mul /= /Zmodp2.mul /=.
zmodp_compute.
ring.
reflexivity.
have: (if_spec (Zmodp2.Zmodp2 0 0 == xp'2)).
move: Hp2 Hp'2 => /= <-.
+ move:
+ move => <- /=.
move: Hp'2 => /=.
move: Hp2 => /= <- //.
+ move => <- /=.
move: Hp'1 => /=.
move: Hp1 => /= <- //.
Search "_ + _".
rewrite /add.
*)
Lemma nP_is_nP2' : forall (n:nat) (x xn: Zmodp.type),
forall (p : mc curve25519_mcuType), p#x0 = x ->
forall (p': mc curve25519_Fp2_mcuType), p'#x0 = Zmodp2.Zmodp2 x 0 ->
(p *+ n)#x0 = xn ->
(p' *+ n)#x0 = Zmodp2.Zmodp2 xn 0.
Proof.
elim => [|n IHn] x xn p Hp p' Hp'.
rewrite ?mulr0n /= => <- //.
rewrite GRing.mulrS.
rewrite GRing.mulrS.
elim (p *+ n).
SearchAbout "*+".
\ No newline at end of file
High/twist25519.v
View file @ 3b6dda02
......@@ -4,6 +4,7 @@ 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.
......@@ -38,45 +39,6 @@ Canonical Structure twist25519_ecuFieldType :=
Canonical Structure twist25519_finECUFieldType :=
Eval hnf in [finECUFieldType of Zmodp.type].
Lemma twist25519_residute (x : Zmodp.type) : x ^+ 2 != a ^+ 2 - 4%:R.
Proof.
replace (a ^+ 2 - 4%:R) with (Zmodp.pi 236839902240).
2: rewrite /a expr2 Zmodp_mulE /= Zmodp_oppE /= /Zmodp.p -lock /= Zmodp_addE //=.
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 (Zmodp.pi 236839902240)).
rewrite /legendre in Eulers_Criterion.
destruct (ClassicalDescription.excluded_middle_informative _).
- rename e into H.
exfalso.
move: H.
rewrite piK /p -lock //.
- destruct (ClassicalDescription.excluded_middle_informative _).
+ rename e into H.
exfalso.
move: Eulers_Criterion.
rewrite piK /p.
2: rewrite -lock //.
replace (236839902240 ^ ((locked (2 ^ 255 - 19)%Z - 1) / 2) mod locked (2 ^ 255 - 19)%Z)
with ((-1) mod (2^255 - 19)) %Z.
rewrite -lock //=.
apply legendre_compute.
+ rename n0 into H.
apply /negP => Hx.
apply H.
move: Hx.
move /eqP => Hx.
apply (f_equal (fun x => Zmodp.repr x)) in Hx.
exists (Zmodp.repr x).
move: Hx.
rewrite expr2.
rewrite Z.pow_2_r.
rewrite modZp => <- //.
Qed.
Definition twist25519_ladder n x :=
@opt_montgomery twist25519_finECUFieldType twist25519_mcuType n 255 x.
......@@ -89,5 +51,6 @@ Proof.
move => Hn Hx p Hp.
rewrite /twist25519_ladder.
apply opt_montgomery_ok => //=.
apply twist25519_residute.
rewrite /a.
apply a_not_square.
Qed.
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