Commit 76ae7789 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Zp^2 is defined with polynom X^2 - 2

parent 585723d4
...@@ -483,4 +483,20 @@ have ->: (2 * 289480223093290488558927462521719769633174961664101410098643960019 ...@@ -483,4 +483,20 @@ have ->: (2 * 289480223093290488558927462521719769633174961664101410098643960019
rewrite /p -lock //. rewrite /p -lock //.
rewrite Z.mul_1_l. rewrite Z.mul_1_l.
apply modZp. 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.
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 ->: (28948022309329048855892746252171976963317496166410141009864396001978282409975 * 2) mod p = 1.
rewrite /p -lock //.
rewrite Z.mul_1_l.
symmetry ;
apply modZp.
Qed. Qed.
\ No newline at end of file
...@@ -27,7 +27,7 @@ Definition one : type := pi (Zmodp.one, Zmodp.zero). ...@@ -27,7 +27,7 @@ Definition one : type := pi (Zmodp.one, Zmodp.zero).
Definition opp (x : type) : type := pi (Zmodp.opp x.1 , Zmodp.opp x.2). Definition opp (x : type) : type := pi (Zmodp.opp x.1 , Zmodp.opp x.2).
Definition add (x y : type) : type := pi (Zmodp.add x.1 y.1, Zmodp.add x.2 y.2). Definition add (x y : type) : type := pi (Zmodp.add x.1 y.1, Zmodp.add x.2 y.2).
Definition sub (x y : type) : type := pi (Zmodp.sub x.1 y.1, Zmodp.sub x.2 y.2). Definition sub (x y : type) : type := pi (Zmodp.sub x.1 y.1, Zmodp.sub x.2 y.2).
Definition mul (x y : type) : type := pi (Zmodp.sub (Zmodp.mul x.1 y.1) (Zmodp.mul x.2 y.2), Zmodp.add (Zmodp.mul x.1 y.2) (Zmodp.mul x.2 y.1)). Definition mul (x y : type) : type := pi (Zmodp.add (Zmodp.mul x.1 y.1) (Zmodp.mul (Zmodp.pi 2) (Zmodp.mul x.2 y.2)), Zmodp.add (Zmodp.mul x.1 y.2) (Zmodp.mul x.2 y.1)).
Lemma pi_of_reprK : cancel repr pi. Lemma pi_of_reprK : cancel repr pi.
Proof. by case. Qed. Proof. by case. Qed.
...@@ -199,9 +199,7 @@ rewrite Zmodp_ring.mul_left_id. ...@@ -199,9 +199,7 @@ rewrite Zmodp_ring.mul_left_id.
rewrite Zmodp_ring.mul_left_id. rewrite Zmodp_ring.mul_left_id.
have ->: Zmodp.mul Zmodp.zero x2 = Zmodp.zero => //. have ->: Zmodp.mul Zmodp.zero x2 = Zmodp.zero => //.
have ->: Zmodp.mul Zmodp.zero x1 = Zmodp.zero => //. have ->: Zmodp.mul Zmodp.zero x1 = Zmodp.zero => //.
rewrite Zmodp_zmod.add_sub. have ->: Zmodp.add x1 (Zmodp.mul (Zmodp.pi 2) Zmodp.zero) = x1 by ring.
have ->: Zmodp.opp Zmodp.zero = Zmodp.zero by ring.
have ->: Zmodp.add x1 Zmodp.zero = x1 by ring.
have ->: Zmodp.add x2 Zmodp.zero = x2 by ring. have ->: Zmodp.add x2 Zmodp.zero = x2 by ring.
reflexivity. reflexivity.
Qed. Qed.
...@@ -273,10 +271,9 @@ End Exports. ...@@ -273,10 +271,9 @@ End Exports.
End Zmodp2_ring. End Zmodp2_ring.
Import Zmodp2_ring.Exports. Import Zmodp2_ring.Exports.
Lemma Zmodp2_mulE x y : (pi x * pi y)%R = pi (x.1 * y.1 - x.2 * y.2, x.1 * y.2 + x.2 * y.1). Lemma Zmodp2_mulE x y : (pi x * pi y)%R = pi (x.1 * y.1 + (Zmodp.pi 2) * (x.2 * y.2), x.1 * y.2 + x.2 * y.1).
Proof. Proof.
apply/eqP; rewrite eqE; apply/eqP=> /=. apply/eqP; rewrite eqE; apply/eqP=> /=.
rewrite Zmodp_zmod.add_sub.
apply: esym. f_equal; apply val_inj => /=. apply: esym. f_equal; apply val_inj => /=.
Qed. Qed.
......
...@@ -35,27 +35,27 @@ move/eqP => H. ...@@ -35,27 +35,27 @@ move/eqP => H.
inversion H. inversion H.
Qed. Qed.
Canonical Structure curve25519_mcuType := Build_mcuType b_neq0 asq_neq4. Canonical Structure curve25519_Fp2_mcuType := Build_mcuType b_neq0 asq_neq4.
Lemma curve25519_chi2 : 2%:R != 0 :> Zmodp2.type. Lemma curve25519_Fp2_chi2 : 2%:R != 0 :> Zmodp2.type.
Proof. Proof.
simpl. simpl.
have -> : 2%:R = Zmodp2.one + Zmodp2.one :> Zmodp2.type by rewrite Zmodp2_addE. have -> : 2%:R = Zmodp2.one + Zmodp2.one :> Zmodp2.type by rewrite Zmodp2_addE.
apply Zmodp2_ring.two_neq_zero. apply Zmodp2_ring.two_neq_zero.
Qed. Qed.
Lemma curve25519_chi3 : 3%:R != 0 :> Zmodp2.type. Lemma curve25519_Fp2_chi3 : 3%:R != 0 :> Zmodp2.type.
Proof. Proof.
have -> : 3%:R = Zmodp2.one + Zmodp2.one + Zmodp2.one :> Zmodp2.type. have -> : 3%:R = Zmodp2.one + Zmodp2.one + Zmodp2.one :> Zmodp2.type.
2: apply Zmodp2_ring.three_neq_zero. 2: apply Zmodp2_ring.three_neq_zero.
by apply/eqP; zmodp2_compute; zmodp_compute; apply/andP; split; zmodp_compute. by apply/eqP; zmodp2_compute; zmodp_compute; apply/andP; split; zmodp_compute.
Qed. Qed.
Definition curve25519_ecuFieldMixin := Definition curve25519_Fp2_ecuFieldMixin :=
ECUFieldMixin curve25519_chi2 curve25519_chi3. ECUFieldMixin curve25519_Fp2_chi2 curve25519_Fp2_chi3.
Canonical Structure curve25519_ecuFieldType := Canonical Structure curve25519_Fp2_ecuFieldType :=
Eval hnf in ECUFieldType Zmodp2.type curve25519_ecuFieldMixin. Eval hnf in ECUFieldType Zmodp2.type curve25519_Fp2_ecuFieldMixin.
Canonical Structure curve25519_finECUFieldType := Canonical Structure curve25519_Fp2_finECUFieldType :=
Eval hnf in [finECUFieldType of Zmodp2.type]. Eval hnf in [finECUFieldType of Zmodp2.type].
(* Lemma curve25519_residute (x : Zmodp.type) : x ^+ 2 != a ^+ 2 - 4%:R. (* Lemma curve25519_residute (x : Zmodp.type) : x ^+ 2 != a ^+ 2 - 4%:R.
...@@ -97,17 +97,17 @@ destruct (ClassicalDescription.excluded_middle_informative _). ...@@ -97,17 +97,17 @@ destruct (ClassicalDescription.excluded_middle_informative _).
rewrite modZp => <- //. rewrite modZp => <- //.
Qed. *) Qed. *)
Definition curve25519_ladder n x := Definition curve25519_Fp2_ladder n x :=
@opt_montgomery curve25519_finECUFieldType curve25519_mcuType n 255 x. @opt_montgomery curve25519_Fp2_finECUFieldType curve25519_Fp2_mcuType n 255 x.
Local Notation "p '#x0'" := (point_x0 p) (at level 30). Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Theorem curve25519_ladder_ok (n : nat) (x : Zmodp.type) : Theorem curve25519_Fp2_ladder_ok (n : nat) (x : Zmodp.type) :
(n < 2^255)%nat -> x != 0 -> (n < 2^255)%nat -> x != 0 ->
forall (p : mc curve25519_mcuType), p#x0 = Zmodp2.pi (x, Zmodp.zero) -> curve25519_ladder n (Zmodp2.pi (x, Zmodp.zero)) = (p *+ n)#x0. 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.
Proof. Proof.
move => Hn Hx p Hp. move => Hn Hx p Hp.
rewrite /curve25519_ladder. rewrite /curve25519_Fp2_ladder.
apply opt_montgomery_ok=> //=. apply opt_montgomery_ok=> //=.
2: by apply/eqP => H ; inversion H ; subst. 2: by apply/eqP => H ; inversion H ; subst.
Admitted. Admitted.
......
...@@ -138,3 +138,86 @@ move => [] y [Hy|Hy] ; [left|right]. ...@@ -138,3 +138,86 @@ move => [] y [Hy|Hy] ; [left|right].
exists (MC OC) => //. exists (MC OC) => //.
} }
Qed. Qed.
From Tweetnacl.High Require Import Zmodp2.
From Tweetnacl.High Require Import curve25519_Fp2.
Local Lemma expr3 : forall x:Zmodp2.type, (x^+3 = x*x*x)%R.
Proof.
move => x; rewrite ?exprSr expr0 GRing.mul1r //.
Qed.
Local Lemma expr3' : forall x:Zmodp.type, (x^+3 = x*x*x)%R.
Proof.
move => x; rewrite ?exprSr expr0 GRing.mul1r //.
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.
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.
rewrite /curve25519.a /curve25519.b.
rewrite ?expr2 ?expr3'.
rewrite ?GRing.mul1r.
move/eqP.
move=> ->.
rewrite ?GRing.mul0r ?GRing.mulr0 ?GRing.addr0.
apply/eqP; f_equal ; f_equal.
rewrite /a /b.
exists (MC OC) => /=.
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 ->
k = x -> exists p0 : mc curve25519_Fp2_mcuType, p0 #x0 = Zmodp2.Zmodp2 x 0.
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.
rewrite /twist25519.b /twist25519.a.
rewrite ?expr2 ?expr3'.
rewrite ?GRing.mul1r.
move/eqP.
move=> ->.
rewrite ?GRing.mul0r ?GRing.mulr0 ?GRing.addr0 ?GRing.add0r.
apply/eqP; f_equal ; f_equal.
exists (MC OC) => /=.
have ->: Zmodp.pi 0 = Zmodp.zero => //=.
Qed.
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2: forall (x:Zmodp.type),
exists (p: mc curve25519_Fp2_mcuType), p#x0 = Zmodp2.Zmodp2 x 0.
Proof.
move=> x.
have := x_is_on_curve_or_twist x.
move=> [] [] [] [] /=.
- move=> _ <- ; exists (MC oncurve_00) => //=.
- apply oncurve25519.
- move=> _ <- ; exists (MC oncurve_00) => //=.
- apply ontwist25519.
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