Commit c7c836c1 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Proof of addition equivalence

parent c74e6e73
Set Warnings "-notation-overridden,-parsing".
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype ssralg finalg.
From Tweetnacl.High Require Import Zmodp.
From Tweetnacl.High Require Import Zmodp2.
Require Import Ring.
Open Scope ring_scope.
Import GRing.Theory.
Import Zmodp2.
Lemma expr3 : forall x:Zmodp2.type, x^+3 = x*x*x :> Zmodp2.type.
Proof.
move => x; rewrite ?exprSr expr0 GRing.mul1r //.
Qed.
Lemma expr3' : forall x:Zmodp.type, (x^+3 = x*x*x)%R.
Proof.
move => x; rewrite ?exprSr expr0 GRing.mul1r //.
Qed.
Ltac ring_simplify_this :=
repeat match goal with
| _ => rewrite expr2
| _ => rewrite expr3
| _ => rewrite GRing.mul1r
| _ => rewrite GRing.mulr1
| _ => rewrite GRing.mul0r
| _ => rewrite GRing.mulr0
| _ => rewrite GRing.add0r
| _ => rewrite GRing.oppr0
| _ => rewrite GRing.addr0
| _ => done
end.
Ltac ringify := repeat match goal with
| [ |- context[Zmodp.mul ?a ?b]] => have ->: (Zmodp.mul a b) = a * b => //
| [ |- context[Zmodp.add ?a (Zmodp.opp ?b)]] => have ->: (Zmodp.add a (Zmodp.opp b)) = a - b => //
| [ |- context[Zmodp.opp ?a]] => have ->: Zmodp.opp a = -a => //
| [ |- context[Zmodp.add ?a ?b]] => have ->: (Zmodp.add a b) = a + b => //
| [ |- context[Zmodp2.mul ?a ?b]] => have ->: (Zmodp2.mul a b) = a * b => //
| [ |- context[Zmodp2.add ?a ?b]] => have ->: (Zmodp2.add a b) = a + b => //
| [ |- context[Zmodp.one] ] => have ->: Zmodp.one = 1 => //
| [ |- context[Zmodp.zero] ] => have ->: Zmodp.zero = 0 => //
end.
Lemma Zmodp2_add_Zmodp a b: Zmodp2 a 0 + Zmodp2 b 0 = Zmodp2 (a + b) 0.
Proof.
rewrite /GRing.add /= /add /=.
ringify ; ring_simplify_this.
Qed.
Lemma Zmodp2_opp_Zmodp a :- Zmodp2 a 0 = Zmodp2 (-a) 0.
Proof.
rewrite /GRing.opp /= /opp /=.
ringify ; ring_simplify_this.
Qed.
Lemma Zmodp2_sub_Zmodp a b:Zmodp2 a 0 - Zmodp2 b 0 = Zmodp2 (a - b) 0.
Proof.
rewrite /GRing.add /= /add /=.
ringify ; ring_simplify_this.
Qed.
Lemma Zmodp2_mul_Zmodp a b :Zmodp2 a 0 * Zmodp2 b 0 = Zmodp2 (a * b) 0.
Proof.
rewrite /GRing.mul /= /mul /=.
ringify ; ring_simplify_this.
Qed.
Lemma Zmodp2_pow_Zmodp : forall n a, (Zmodp2 a 0) ^+ n = Zmodp2 (a^+n) 0.
Proof.
elim => [| n IHn] a.
- by rewrite ?expr0.
- by rewrite ?exprS IHn Zmodp2_mul_Zmodp.
Qed.
Lemma Zmodp2_inv_Zmodp a :(Zmodp2 a 0)^-1 = Zmodp2 (a^-1) 0.
Proof.
have/orP := orbN (Zmodp.eqb a 0).
move => []; move/Refl.eqb_spec.
- by move => ->; rewrite ?invr0.
- move => Ha.
apply GRing.mulr1_eq.
rewrite Zmodp2_mul_Zmodp GRing.mulfV //.
by apply/eqP.
Qed.
Lemma Zmodp2_div_Zmodp a b : (Zmodp2 a 0) / (Zmodp2 b 0) = Zmodp2 (a/b) 0.
Proof.
by rewrite Zmodp2_inv_Zmodp Zmodp2_mul_Zmodp.
Qed.
Ltac Zmodpify := repeat match goal with
| _ => rewrite Zmodp2_add_Zmodp
| _ => rewrite Zmodp2_sub_Zmodp
| _ => rewrite Zmodp2_opp_Zmodp
| _ => rewrite Zmodp2_mul_Zmodp
| _ => rewrite Zmodp2_pow_Zmodp
| _ => rewrite Zmodp2_inv_Zmodp
| _ => rewrite Zmodp2_div_Zmodp
end.
......@@ -10,13 +10,14 @@ 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 Zmodp.
Require Import Ring.
Require Import ZArith.
Import BinInt.
(* Import BinInt. *)
Open Scope ring_scope.
Import GRing.Theory.
......@@ -25,45 +26,57 @@ 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 :> Zmodp2.type.
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.
Lemma oncurve_inf : oncurve curve25519_Fp2_mcuType (EC_Inf Zmodp2.type).
Proof. done. Defined.
Local Lemma oncurve_00 : (oncurve curve25519_Fp2_mcuType (EC_In 0 0)).
Proof.
simpl; rewrite /a /b ; apply/eqP.
have ->: (0 ^+ 2)%R = 0 :> Zmodp2.type by rewrite expr2 ?GRing.mulr0.
have ->: (0 ^+ 3)%R = 0 :> Zmodp2.type by rewrite expr3 ?GRing.mulr0.
have ->: (0 ^+ 2)%R = 0 :> Zmodp2.type by ring_simplify_this.
have ->: (0 ^+ 3)%R = 0 :> Zmodp2.type by ring_simplify_this.
rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
f_equal; f_equal; apply/eqP ; zmodp_compute => //=.
Qed.
Lemma oncurve25519_impl : forall (x y: Zmodp.type),
oncurve curve25519_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.
ring_simplify_this.
move/eqP => -> /=.
apply/eqP.
f_equal.
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)))) => /=.
have : oncurve curve25519_mcuType (EC_In k k') => //.
move/oncurve25519_impl => HOC.
exists (MC HOC) => /=.
have ->: Zmodp.pi 0 = Zmodp.zero => //=.
Qed.
Lemma ontwist25519_impl : forall (x y: Zmodp.type),
oncurve twist25519_mcuType (EC_In x y) ->
(oncurve curve25519_Fp2_mcuType (EC_In (Zmodp2.pi (x, Zmodp.pi 0)) (Zmodp2.pi (Zmodp.pi 0, y)))).
Proof.
move => x y /=.
rewrite /a /b.
rewrite ?expr2 ?expr3.
rewrite ?expr2 ?expr3 ?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 => //=.
rewrite /twist25519.a /twist25519.b.
ring_simplify_this.
move/eqP => -> /=.
apply/eqP.
f_equal.
Qed.
Local Lemma ontwist25519 : forall x k k0 : Zmodp.type,
......@@ -71,23 +84,14 @@ 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.
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 : oncurve twist25519_mcuType (EC_In k k') => //.
move/ontwist25519_impl => HOC.
exists (MC HOC) => /=.
have ->: Zmodp.pi 0 = Zmodp.zero => //=.
Qed.
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2: forall (x:Zmodp.type),
(* May actually not be in the right direction... *)
Theorem 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.
......@@ -99,24 +103,82 @@ Proof.
- 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.
(* a great definition ... *)
(* Definition curve_to_Fp2 (p: mc curve25519_mcuType) : (mc curve25519_Fp2_mcuType) :=
match p with
| MC u P =>
match u, P with
| EC_Inf, _ => MC (MCGroup.zeroO curve25519_Fp2_mcuType)
| EC_In x y, P => MC (oncurve25519_impl x y P)
end
end.
*)
(* a not so great definition ... *)
Definition curve_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
match p with
| EC_Inf => EC_Inf Zmodp2.type
| EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
end.
(* Lemma curve_to_Fp2_inf : curve_to_Fp2 (MC (MCGroup.zeroO curve25519_mcuType)) = MC (MCGroup.zeroO curve25519_Fp2_mcuType).
Proof. done. Qed.
*)
(* Lemma curve_to_Fp2_xy x y (P: oncurve curve25519_mcuType (|x , y|)): curve_to_Fp2 (MC P) = MC (oncurve25519_impl x y P).
Proof. done. Qed.
*)
(* a not so great definition ... *)
(* Definition curve_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
match p with
| EC_Inf => EC_Inf Zmodp2.type
| EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
end.
*)
Lemma nP_is_nP2 : forall (x1 x2 xs: Zmodp.type),
(* a great definition ... *)
(* Definition twist_to_Fp2 (p: mc twist25519_mcuType) : (mc curve25519_Fp2_mcuType) :=
match p with
| MC (EC_Inf) _ => MC oncurve_inf
| MC (EC_In x y) P => MC (ontwist25519_impl x y P)
end.
*)
(* a not so great definition ... *)
Definition twist_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
match p with
| EC_Inf => EC_Inf Zmodp2.type
| EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 0 y)
end.
Lemma add_stable : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
p' = curve_to_Fp2 p ->
q' = curve_to_Fp2 q ->
MCGroup.add_no_check curve25519_Fp2_mcuType p' q' = curve_to_Fp2 (MCGroup.add_no_check curve25519_mcuType p q).
Proof.
move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //=.
move => [] -> -> [] -> ->.
rewrite /curve25519.a /curve25519.b.
match goal with
| [ |- _ = ?A ] => remember A as Freezer
end.
rewrite /eq_op.
rewrite /Equality.op /=.
rewrite /eq_op.
rewrite /Equality.op /=.
rewrite !eq_refl.
rewrite ?Bool.andb_true_r.
rewrite ?expr2.
ring_simplify_this.
have ->: 2%:R = Zmodp2.Zmodp2 (2%:R) 0 => //.
have ->: 3%:R = Zmodp2.Zmodp2 (3%:R) 0 => //.
Zmodpify => /=.
ringify.
subst Freezer.
ring_simplify_this.
case_eq (xp == xq) => -> //=.
case_eq ((yp == yq) && (yp != 0)) => -> //=.
Qed.
(* 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 ->
......@@ -126,6 +188,7 @@ Lemma nP_is_nP2 : forall (x1 x2 xs: Zmodp.type),
(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
......@@ -191,7 +254,7 @@ Admitted.
*)
Lemma nP_is_nP2' : forall (n:nat) (x xn: Zmodp.type),
(* 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 ->
......@@ -202,4 +265,4 @@ Proof.
rewrite GRing.mulrS.
rewrite GRing.mulrS.
elim (p *+ n).
SearchAbout "*+".
\ No newline at end of file
SearchAbout "*+". *)
\ No newline at end of file
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