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

WIP Fixing Timmy mess

parent 3b6dda02
Hide whitespace changes
Inline Side-by-side
High/curve25519_Fp2.v
View file @ c74e6e73
......@@ -26,7 +26,6 @@ Proof.
rewrite expr2 /a.
change (Zmodp2.piZ (486662, 0%Z)) with (Zmodp2.pi (Zmodp.pi 486662, Zmodp.pi 0)).
rewrite Zmodp2_mulE /=.
change (Zmodp.pi 0) with Zmodp.zero.
apply/eqP => H.
inversion H ; clear H.
move/eqP: H1.
......
High/curve25519_twist25519_eq.v
View file @ c74e6e73
......@@ -117,7 +117,6 @@ Proof.
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.
......@@ -138,3 +137,4 @@ move => [] y [Hy|Hy] ; [left|right].
exists (MC OC) => //.
}
Qed.
High/mc.v
View file @ c74e6e73
......@@ -179,20 +179,47 @@ Module MCGroup.
(| xs, - s * (xs - x1) - y1 |)
end.
Definition add_no_check (p1 p2 : point K) :=
match p1, p2 with
| ∞, _ => p2 | _, ∞ => p1
| (|x1, y1|), (|x2, y2|) =>
if x1 == x2
then if (y1 == y2) && (y1 != 0)
then
let s := (3%:R * x1^+2 + 2%:R * M#a * x1 + 1) / (2%:R * M#b * y1) in
let xs := s^+2 * M#b - M#a - 2%:R * x1 in
(| xs, - s * (xs - x1) - y1 |)
else
∞
else
let s := (y2 - y1) / (x2 - x1) in
let xs := s^+2 * M#b - M#a - x1 - x2 in
(| xs, - s * (xs - x1) - y1 |)
end.
Lemma add_no_check_eq (p1 p2:point K) :
oncurve M p1 ->
oncurve M p2 ->
add_no_check p1 p2 = add p1 p2.
Proof.
rewrite /add_no_check /add => -> -> //.
Qed.
Lemma zeroO : oncurve M ∞.
Proof. by []. Qed.
Proof. by []. Defined.
Lemma negO : forall p, oncurve M p -> oncurve M (neg p).
Proof. by case=> [|x y] //=; rewrite sqrrN. Qed.
Proof. by case=> [|x y] //=; rewrite sqrrN. Defined.
Lemma oncurveN p: (oncurve M p) = (oncurve M (neg p)).
Proof.
apply/idP/idP; move/negO => //.
by case: p => [|x y] //=; rewrite opprK.
Qed.
Defined.
Lemma oncurveN_fin x y: oncurve M (|x, -y|) = oncurve M (|x, y|).
Proof. by move: (oncurveN (|x, y|)). Qed.
Proof. by move: (oncurveN (|x, y|)). Defined.
Local Notation sizep := (size : {poly _} -> _).
......@@ -255,7 +282,7 @@ Module MCGroup.
have nz_x2Bx1: x2 - x1 != 0 by rewrite subr_eq0 eq_sym.
congr (_ + _); apply/(@mulfI _ (x2 - x1)) => //.
by rewrite !mulrBr !mulrA [_ / _]mulrAC divff // !simp; ssring.
Qed.
Defined.
Lemma line_outcveE p q:
~~ (oncurve M (|p.1, p.2|) && oncurve M (|q.1, q.2|))
......@@ -421,6 +448,13 @@ Module MCGroup.
apply/eqP; rewrite -mul_polyC !(horner_exp, hornerE) /=.
rewrite -![(_ / u) * _]mulrA -![M#b * _ * _]mulrA -!expr2.
by rewrite !exprMn; congr (_ * _); rewrite -[c-_]opprK opprB sqrrN.
Defined.
Lemma addO' (p q: mc M): oncurve M (add_no_check p q).
Proof.
destruct p as [p Hp], q as [q Hq].
rewrite (add_no_check_eq Hp Hq).
apply addO.
Qed.
Lemma add0o : {in (oncurve M), left_id ∞ add}.
......@@ -429,6 +463,11 @@ Module MCGroup.
by rewrite /add /= oncve_p.
Qed.
Lemma add0o' : {in (oncurve M), left_id ∞ add_no_check}.
Proof.
done.
Qed.
Lemma addNo : left_inverse ∞ neg add.
Proof.
move=> p; rewrite /add -oncurveN.
......@@ -439,6 +478,15 @@ Module MCGroup.
by absurd false=> //; rewrite -Hy0 -eqrN_eq0 HyN.
Qed.
Lemma addNo' : {in (oncurve M), left_inverse ∞ neg add_no_check}.
Proof.
move=> p.
rewrite /in_mem /mem => /= Hp.
rewrite add_no_check_eq //.
2: rewrite -oncurveN //.
apply addNo.
Qed.
Lemma addoC : commutative add.
Proof.
move=> p1 p2; rewrite /add;
......@@ -467,20 +515,42 @@ Module MCGroup.
by rewrite addrC.
Qed.
Lemma addoC' : prop_in2 (mem (oncurve M)) (P:=fun x y : point K => eq (add_no_check x y) (add_no_check y x))
(inPhantom (commutative add_no_check)).
Proof.
move=> p q.
rewrite /in_mem /mem => /= Hp Hq.
rewrite ?add_no_check_eq //.
apply addoC.
Qed.
Notation zeromc := (MC zeroO).
Definition negmc := [fun p : mc M => MC (negO [oc of p])].
Definition addmc := [fun p1 p2 : mc M => MC (addO p1 p2)].
Definition addmc := [fun p1 p2 : mc M => MC (addO' p1 p2)].
Lemma addNm : left_inverse zeromc negmc addmc.
(* Lemma addNm : left_inverse zeromc negmc addmc.
Proof. by move=> [p Hp]; apply/eqP; rewrite eqE /= addNo. Qed.
*)
Lemma addNm : left_inverse zeromc negmc addmc.
Proof. by move=> [p Hp]; apply/eqP; rewrite eqE /= addNo'. Qed.
Lemma add0m : left_id zeromc addmc.
(* Lemma add0m : left_id zeromc addmc.
Proof. by move=> [p Hp]; apply/eqP; rewrite eqE /= add0o. Qed.
*)
Lemma add0m : left_id zeromc addmc.
Proof. by move=> [p Hp]; apply/eqP; rewrite eqE /=. Qed.
Lemma addmC : commutative addmc.
(* Lemma addmC : commutative addmc.
Proof.
move=> [p1 Hp1] [p2 Hp2]; apply/eqP=> /=.
by rewrite eqE /= addoC.
Qed.
*)
Lemma addmC : commutative addmc.
Proof.
move=> [p1 Hp1] [p2 Hp2]; apply/eqP=> /=.
by rewrite eqE /= addoC'.
Qed.
End Defs.
End MCGroup.
High/mcgroup.v
View file @ c74e6e73
......@@ -131,6 +131,14 @@ Section MCEC.
by congr (|_, _|); ssfield; rewrite ?neq0 //.
Qed.
Lemma ec_of_mc_pointD' : forall p q, oncurve M p -> oncurve M q ->
ec_of_mc_point (MCGroup.add_no_check M p q) = ECGroup.add E (ec_of_mc_point p) (ec_of_mc_point q).
Proof.
move => p q Hp Hq.
rewrite MCGroup.add_no_check_eq //.
by apply ec_of_mc_pointD.
Qed.
Lemma ec_of_mc_pointN : forall p,
ec_of_mc_point (MCGroup.neg p) = ECGroup.neg (ec_of_mc_point p).
Proof. by move=> [|x y] //=; rewrite mulNr. Qed.
......@@ -140,7 +148,9 @@ Section MCAssocFin.
Variable K : finECUFieldType.
Variable M : mcuType K.
Local Notation "x \+ y" := (@MCGroup.add _ _ x y).
(* Local Notation "x \+ y" := (@MCGroup.add _ _ x y). *)
Local Notation "x \+ y" := (@MCGroup.add_no_check _ _ x y).
Lemma addmA_fin: associative (@MCGroup.addmc K M).
Proof.
......@@ -149,12 +159,12 @@ Section MCAssocFin.
pose oncve_q := [oc of q].
pose oncve_r := [oc of r].
apply/eqP; rewrite !eqE /=; apply/eqP.
rewrite -[p \+ _](ec_of_mc_pointK M) !ec_of_mc_pointD //;
last exact: MCGroup.addO.
rewrite -[p \+ _](ec_of_mc_pointK M) !ec_of_mc_pointD' //;
last exact: MCGroup.addO'.
move: (addeA_fin (ec_of_mc p) (ec_of_mc q) (ec_of_mc r)).
move/eqP; rewrite !eqE /= => /eqP ->.
rewrite -!ec_of_mc_pointD // ?ec_of_mc_pointK //;
last exact: MCGroup.addO.
rewrite -!ec_of_mc_pointD' // ?ec_of_mc_pointK //;
last exact: MCGroup.addO'.
Qed.
Definition finmc_zmodMixin :=
......@@ -171,6 +181,6 @@ Section MCAssocFin.
pose oncve_p := [oc of p].
pose oncve_q := [oc of q].
apply/eqP; rewrite !eqE /=; apply/eqP.
by rewrite ec_of_mc_pointD -?MCGroup.oncurveN // ec_of_mc_pointN.
by rewrite ec_of_mc_pointD' -?MCGroup.oncurveN // ec_of_mc_pointN.
Qed.
End MCAssocFin.
High/montgomery.v
View file @ c74e6e73
......@@ -19,7 +19,8 @@ Section MontgomerysFormulas.
Variable M : mcuType K.
Local Notation "\- x" := (@MCGroup.neg _ x).
Local Notation "x \+ y" := (@MCGroup.add _ M x y).
(* Local Notation "x \+ y" := (@MCGroup.add _ M x y). *)
Local Notation "x \+ y" := (@MCGroup.add_no_check _ M x y).
Local Notation "x \- y" := (x \+ (\- y)).
Lemma same_x_opposite_points p1_x p1_y p2_x p2_y :
......@@ -71,7 +72,7 @@ Section MontgomerysFormulas.
rewrite Hp1 Hp2 in p1_neq_p2 x1_eq_x2 oncve_p1 oncve_p2 *.
by apply: same_x_opposite_points.
have p1_plus_p2_inf: p3 = ∞
by rewrite /p3 p1_eq_p2N MCGroup.addNo //.
by rewrite /p3 p1_eq_p2N MCGroup.addNo' //.
have p3_not_fin: ~~point_is_fin p3
by rewrite p1_plus_p2_inf //.
by rewrite -(andbN (point_is_fin p3)) p3_not_fin Hfin_p3.
......@@ -92,7 +93,7 @@ Section MontgomerysFormulas.
have oncve_p2N: oncurve M (\-p2) by apply: MCGroup.negO.
rewrite /p3 /p4 Hp1 Hp2 /=.
rewrite ?Hp1 ?Hp2 in oncve_p1 oncve_p2 oncve_p2N x1_neq_x2.
rewrite /MCGroup.add oncve_p1 oncve_p2 oncve_p2N (negbTE x1_neq_x2) /=.
rewrite /MCGroup.add_no_check (negbTE x1_neq_x2) /=.
clear Hp1 Hp2 Hall_fin Hfin_p1 Hfin_p2 p3 p4 p1_neq_p2 p1 p2.
case: (boolP (x1 * x2 == 0)).
* move=> x1_x2_eq0 {oncve_p2N}.
......@@ -193,9 +194,9 @@ Section MontgomerysFormulas.
rewrite /p3 -p1_eq_p2 Hp1.
have y1_neq0: y1 != 0.
apply/(@contraL _ (point_is_fin p3)) => [y1_eq0|]; last by [].
by rewrite /p3 -p1_eq_p2 /MCGroup.add oncve_p1 Hp1 !eq_refl y1_eq0.
by rewrite /p3 -p1_eq_p2 /MCGroup.add_no_check Hp1 !eq_refl y1_eq0.
rewrite {}Hp1 in oncve_p1.
rewrite /MCGroup.add oncve_p1 !eq_refl y1_neq0 /=.
rewrite /MCGroup.add_no_check !eq_refl y1_neq0 /=.
set c := (_ / _)^+2.
rewrite -[4%:R * x1 * _]mulrA [x1 * _]mulrC -2!mulrA.
have ->: x1 * (x1^+2 + M#a * x1 + 1) = x1^+3 + M#a * x1^+2 + x1 by ssring.
......@@ -209,12 +210,19 @@ Section MontgomerysFormulas.
Qed.
End MontgomerysFormulas.
Ltac oncurves := match goal with
| _ => apply MCGroup.negO => //
| _ => done
| _ => idtac
end.
Section MontgomerysHomFormulas.
Variable K : ecuFieldType.
Variable M : mcuType K.
Local Notation "\- x" := (@MCGroup.neg _ x).
Local Notation "x \+ y" := (@MCGroup.add _ M x y).
(* Local Notation "x \+ y" := (@MCGroup.add _ M x y). *)
Local Notation "x \+ y" := (@MCGroup.add_no_check _ M x y).
Local Notation "x \- y" := (x \+ (\- y)).
Inductive K_infty :=
......@@ -302,7 +310,7 @@ Section MontgomerysHomFormulas.
Proof.
move=> p1 p2 oncve_p1 oncve_p2 p1_neq_p2 p1_neq_p2N.
suff : (p1 \+ p2 != ∞) by case: (p1 \+ p2).
rewrite /MCGroup.add oncve_p1 oncve_p2 /=.
rewrite /MCGroup.add_no_check /=.
case: (boolP (p1_x == p2_x)) => // /eqP p1x_eq_p2x.
move: p1_neq_p2N.
have -> : p1 = \- p2 by apply: (same_x_opposite_points (M:=M)).
......@@ -355,7 +363,7 @@ Section MontgomerysHomFormulas.
oncurve M p -> p_x != 0 -> point_is_fin (p \+ p).
Proof.
move=> p oncve_p p_x_neq0.
rewrite /p /MCGroup.add oncve_p !eq_refl.
rewrite /p /MCGroup.add_no_check !eq_refl.
by rewrite -(@point_x_eq0_point_y_eq0 p_x) // p_x_neq0.
Qed.
......@@ -374,14 +382,15 @@ Section MontgomerysHomFormulas.
move=> Hp1x Hp2x Hp4x.
case: (boolP (p1 == p2)) => [/eqP p1_eq_p2 | p1_neq_p2].
move: Hp4x.
rewrite p1_eq_p2 MCGroup.addoC MCGroup.addNo /= => /eqP.
rewrite p1_eq_p2 MCGroup.addoC' ; oncurves => /=.
rewrite MCGroup.addNo'; oncurves => /= => /eqP.
by rewrite eq_sym inf_div_K_Inf (negbTE z4_neq_0).
case: p1 => [| p1_x p1_y] in oncve_p1 Hp1x Hp4x p1_neq_p2 *.
move: Hp1x => /eqP; rewrite eq_sym inf_div_K_Inf => /eqP z1_eq_0.
have x1_neq_0 : x1 != 0
by move: z1_eq_0 H1_ok => -> /orP; elim; rewrite ?eq_refl.
move: Hp4x.
rewrite MCGroup.add0o ?point_x_neg; last by apply: MCGroup.negO.
rewrite MCGroup.add0o' ?point_x_neg; last by apply: MCGroup.negO.
rewrite Hp2x /inf_div (negbTE z4_neq_0).
case: ifP => [| /negbT z2_neq_0]; first by [].
case; rewrite -[x4 / z4](mulfK z2_neq_0) => /(divIf z2_neq_0) Hx2.
......@@ -393,8 +402,8 @@ Section MontgomerysHomFormulas.
apply: mulf_neq0; first by [].
by rewrite -mulr2n -mulr_natl mulf_neq0 ?ecu_chi2.
rewrite /hom_ok z3_neq_0 orbT /=.
rewrite MCGroup.add0o // Hp2x /inf_div.
rewrite (negbTE z2_neq_0) (negbTE z3_neq_0).
have ->:(z3 == 0 = false).
apply/eqP; move/eqP: z3_neq_0 => //.
apply/eqP; apply: congr1.
rewrite /x3 /z3 Hx2 z1_eq_0 !addr0 !subr0.
rewrite -mulrN -!mulrDr opprB {1}[_ - z2]addrC [_ + (z2 - _)]addrC.
......@@ -405,7 +414,7 @@ Section MontgomerysHomFormulas.
have x2_neq_0 : x2 != 0
by move: z2_eq_0 H2_ok => -> /orP; elim; rewrite ?eq_refl.
move: Hp4x.
rewrite /MCGroup.add oncve_p1 /=.
rewrite /MCGroup.add_no_check /=.
rewrite /= in Hp1x.
rewrite Hp1x {1 2}/inf_div (negbTE z4_neq_0).
case: ifP => [| /negbT z1_neq_0]; first by [].
......@@ -429,7 +438,7 @@ Section MontgomerysHomFormulas.
case: (boolP ((|p1_x, p1_y|) == (|p2_x, -p2_y|))) => [/eqP H | p1_neq_Np2].
rewrite H in Hp1x *.
rewrite /= in Hp1x Hp2x.
rewrite -[(|p2_x, (- p2_y)|)]/(\- (|p2_x, p2_y|)) MCGroup.addNo /=.
rewrite -[(|p2_x, (- p2_y)|)]/(\- (|p2_x, p2_y|)) MCGroup.addNo' ; oncurves => /=.
have z1_neq_0 : z1 != 0 by apply/inf_div_K_Fin/sym_eq; exact Hp1x.
have z2_neq_0 : z2 != 0 by apply/inf_div_K_Fin/sym_eq; exact Hp2x.
have Hx1 : x1 = x2 / z2 * z1.
......@@ -444,8 +453,9 @@ Section MontgomerysHomFormulas.
have z3_eq0 : z3 = 0 by rewrite /z3 Hx1; ssfield.
have x3_neq0 : x3 != 0.
apply: contra_neq (x4_neq_0) => x3_eq0.
apply/eqP; rewrite -(@inf_div_eq0 _ z4) // -Hp4x H /=; apply/eqP.
set p2N := (|p2_x, _|).
apply/eqP; rewrite -(@inf_div_eq0 _ z4) // -Hp4x H.
apply/eqP.
set p2N := (|p2_x, (- p2_y)|).
have oncve_p2N : oncurve M p2N by rewrite MCGroup.oncurveN /= opprK.
have p2Ndouble_is_fin : point_is_fin (p2N \+ p2N).
by apply: point_x_neq0_double_finite.
......@@ -576,9 +586,11 @@ Section MontgomerysHomFormulas.
move: oncve_p.
rewrite /p px_eq_0 /oncurve !expr0n /= mulr0 !addr0 mulf_eq0.
by rewrite (negbTE (mcu_b_neq0 _)) orFb sqrf_eq0 => /eqP ->.
inversion p_eq_0.
rewrite {}p_eq_0 in oncve_p Hpx *.
rewrite /MCGroup.add oncve_p !eq_refl /=.
have x1z1_4_eq_0 : x1z1_4 = 0
rewrite !eq_refl /=.
(* rewrite /MCGroup.add_no_check !eq_refl /=. *)
have x1z1_4_eq_0 : x1z1_4 = 0.
by rewrite /x1z1_4 x1_eq_0 add0r sub0r sqrrN subrr.
have /eqP : z3 = 0 by rewrite /z3 x1z1_4_eq_0 mul0r.
by rewrite -(inf_div_K_Inf x3) => /eqP ->.
......@@ -597,23 +609,29 @@ Section MontgomerysHomFormulas.
rewrite [z1^-1^+2]expr2 mulrA mulfK // -mulrA.
by apply: aux_no_square; rewrite mulf_neq0 // invr_neq0.
have px_neq_0 : p_x != 0 by rewrite Hpx mulf_neq0 // invr_neq0.
have py_neq_0 : p_y != 0.
rewrite -sqrf_eq0 -(inj_eq (@mulfI _ (M#b) _)) ?mcu_b_neq0 // mulr0.
move: oncve_p; rewrite /oncurve /p => /eqP ->.
have -> : p_x^+3 + M #a * p_x^+2 + p_x = p_x * (p_x^+2 + M #a * p_x + 1)
by ssring.
by rewrite mulf_neq0 // aux_no_square.
have pDp_fin : point_is_fin (p \+ p).
have py_neq_0 : p_y != 0.
rewrite -sqrf_eq0 -(inj_eq (@mulfI _ (M#b) _)) ?mcu_b_neq0 // mulr0.
move: oncve_p; rewrite /oncurve /p => /eqP ->.
have -> : p_x^+3 + M #a * p_x^+2 + p_x = p_x * (p_x^+2 + M #a * p_x + 1)
by ssring.
by rewrite mulf_neq0 // aux_no_square.
by rewrite /MCGroup.add oncve_p /p !eq_refl py_neq_0.
have Hall_fin : all (@point_is_fin K) [:: p; p \+ p] by rewrite /= pDp_fin.
by rewrite /MCGroup.add_no_check /p !eq_refl py_neq_0.
apply/eqP; rewrite -point_x0_point_x //; apply/eqP.
rewrite !eq_refl py_neq_0 /=.
have Hall_fin : all (@point_is_fin K) [:: p; p \+ p] by rewrite /= pDp_fin.
apply/(@mulfI _ (4%:R * (point_x0 p))); first by rewrite mulf_neq0 //.
apply/(@mulIf _ ((point_x0 p)^+2 + M#a * (point_x0 p) + 1)).
by apply: aux_no_square.
apply/(@mulIf _ z3); first by [].
rewrite -[_ * z3 in RHS]mulrA [_ * z3 in RHS]mulrC [_ * (z3 * _)]mulrA.
rewrite [_ * (x3 / z3)]mulrA mulfVK //.
rewrite montgomery_eq //= Hpx /x3 /z3 /x1z1_4.
have Hp: p = p => //.
have Hp2: p = (|p_x, p_y|) => //.
have := montgomery_eq oncve_p Hp Hall_fin.
rewrite /MCGroup.add_no_check Hp2 !eq_refl py_neq_0 /=.
move=>->.
rewrite Hpx /x3 /z3 /x1z1_4.
by ssfield.
Qed.
End MontgomerysHomFormulas.
\ No newline at end of file
High/opt_ladder.v
View file @ c74e6e73
......@@ -77,7 +77,8 @@ Section OptimizedLadder.
Qed.
Local Notation "\- x" := (@MCGroup.neg _ x).
Local Notation "x \+ y" := (@MCGroup.add _ M x y).
(* Local Notation "x \+ y" := (@MCGroup.add _ M x y). *)
Local Notation "x \+ y" := (@MCGroup.add_no_check _ M x y).
Local Notation "x \- y" := (x \+ (\- y)).
Local Lemma opt_montgomery_rec_small (n m k : nat) (x a b c d : K) : k >= m ->
......
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