From 533f5480932761073b9e55874d45d1c51825cfbb Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 8 Jan 2016 02:47:06 -0500 Subject: PointFormats: no zero denominators in Edwards addition --- src/Curves/PointFormats.v | 171 ++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 142 insertions(+), 29 deletions(-) (limited to 'src') diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 11b048cf4..4eb5a9ea5 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -3,16 +3,14 @@ Require Import Tactics.VerdiTactics. Require Import Logic.Eqdep_dec. Require Import BinNums NArith. -Module GaloisDefs (M : Modulus). - Module Export GT := GaloisTheory M. -End GaloisDefs. - Module Type TwistedEdwardsParams (M : Modulus). Module Export GFDefs := ZGaloisField M. Local Open Scope GF_scope. + Axiom char_gt_2 : (1+1) <> 0. Parameter a : GF. Axiom a_nonzero : a <> 0. - Axiom a_square : exists x, x * x = a. + Parameter sqrt_a : GF. + Axiom a_square : sqrt_a^2 = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End TwistedEdwardsParams. @@ -116,6 +114,119 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam Definition point := { P | onCurve P}. Definition mkPoint := exist onCurve. + Lemma GFdecidable_neq : forall x y : GF, Zbool.Zeq_bool x y = false -> x <> y. + Proof. + intros. intro. rewrite GFcomplete in H; intuition. + Qed. + + Ltac case_eq_GF a b := + case_eq (Zbool.Zeq_bool a b); intro Hx; + match type of Hx with + | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = true => + pose proof (GFdecidable a b Hx) + | Zbool.Zeq_bool (GFToZ a) (GFToZ b) = false => + pose proof (GFdecidable_neq a b Hx) + end; clear Hx. + + Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. + Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. + + (* https://eprint.iacr.org/2007/286.pdf Theorem 3.3 *) + (* c=1 and an extra a in front of x^2 *) + + Lemma onCurveDenominatorOk' x1 y1 x2 y2 : + onCurve (x1,y1) -> + onCurve (x2, y2) -> + (d*x1*x2*y1*y2)^2 <> 1. + Proof. + unfold onCurve; intros. intro. + (* TODO: lemma+tactic to inspect a*b*c*d*e<>0 *) + case_eq_GF x1 0%GF; [admit|]. + case_eq_GF y1 0%GF; [admit|]. + case_eq_GF x2 0%GF; [admit|]. + case_eq_GF y2 0%GF; [admit|]. + + (* Furthermore... *) + pose proof (eq_refl (d*x1^2*y1^2*(a*x2^2 + y2^2))) as Heqt. + rewrite H0 in Heqt at 2. + replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) + with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. + rewrite H1 in Heqt. + replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. + rewrite <-H in Heqt. + + (* main equation *) + case_eq_GF (sqrt_a*x2 + y2) 0%GF. + case_eq_GF (sqrt_a*x2 - y2) 0%GF. + + - destruct H4. + assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). + replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (inject 2 * sqrt_a * x2) in Hc by field. + (* TODO: lemma+tactic to inspect a*b*c*d*e=0 *) + admit. + + - rewrite <- a_square in *. + assert ((sqrt_a*x1 - d * x1 * x2 * y1 * y2*y1)^2 = (sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2 - d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1) as Heqw by field. + rewrite H1 in Heqw. + replace (1 * y1^2) with (y1^2) in Heqw by field. + rewrite <- Heqt in Heqw. + replace (d * x1^2 * y1^2 * (sqrt_a * sqrt_a * x2 ^ 2 + y2 ^ 2) + + d * x1 * x2 * y1 * y2 * sqrt_a * inject 2 * x1 * y1) + with (d * (x1 * y1 * (sqrt_a * x2 + y2))^2) + in Heqw by field. + assert (d = (sqrt_a * x1 - d * x1 * x2 * y1 * y2 * y1)^2 / (x1 * y1 * (sqrt_a * x2 - y2)) ^ 2) + by (rewriteAny; field; auto). + + (* FIXME: field fails if I remove this remember *) + remember (sqrt_a * x1 - d * x1 * x2 * y1 * y2 * y1) as p. + assert (d = (p/(x1 * y1 * (sqrt_a * x2 - y2)))^2) by (rewriteAny; field; auto). + subst p. + + edestruct d_nonsquare; eauto. + + - rewrite <- a_square in *. + assert ((sqrt_a*x1 + d * x1 * x2 * y1 * y2*y1)^2 = (sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2 + d * x1 * x2 * y1 * y2*sqrt_a*(inject 2)*x1*y1) as Heqw by field. + rewrite H1 in Heqw. + replace (1 * y1^2) with (y1^2) in Heqw by field. + rewrite <- Heqt in Heqw. + replace (d * x1^2 * y1^2 * (sqrt_a * sqrt_a * x2 ^ 2 + y2 ^ 2) + + d * x1 * x2 * y1 * y2 * sqrt_a * inject 2 * x1 * y1) + with (d * (x1 * y1 * (sqrt_a * x2 + y2))^2) + in Heqw by field. + assert (d = (sqrt_a * x1 + d * x1 * x2 * y1 * y2 * y1)^2 / (x1 * y1 * (sqrt_a * x2 + y2)) ^ 2) + by (rewriteAny; field; auto). + + (* FIXME: field fails if I remove this remember *) + remember (sqrt_a * x1 + d * x1 * x2 * y1 * y2 * y1) as p. + assert (d = (p/(x1 * y1 * (sqrt_a * x2 + y2)))^2) by (rewriteAny; field; auto). + subst p. + + edestruct d_nonsquare; eauto. + Qed. + + Lemma onCurveDenominatorOkPlus x1 y1 x2 y2 : + onCurve (x1,y1) -> + onCurve (x2, y2) -> + (1 + d*x1*x2*y1*y2) <> 0. + Proof. + unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (0-1)%GF. + - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (onCurveDenominatorOk' x1 y1 x2 y2); auto. + - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H1 by field. + intro; rewrite H2 in H1; intuition. + Qed. + + Lemma onCurveDenominatorOkMinus x1 y1 x2 y2 : + onCurve (x1,y1) -> + onCurve (x2, y2) -> + (1 - d*x1*x2*y1*y2) <> 0. + Proof. + unfold onCurve; intros; case_eq_GF (d*x1*x2*y1*y2) (1)%GF. + - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (onCurveDenominatorOk' x1 y1 x2 y2); auto. + - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H1 by field. + intro; rewrite H2 in H1; apply H1; field. + Qed. + Hint Resolve onCurveDenominatorOkPlus onCurveDenominatorOkMinus. + Definition projX (P:point) := fst (proj1_sig P). Definition projY (P:point) := snd (proj1_sig P). @@ -141,8 +252,6 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam * c=1 and an extra a in front of x^2 *) unfold unifiedAdd', onCurve in *; injection H; clear H; intros. - Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. - Ltac t x1 y1 x2 y2 := assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); @@ -164,12 +273,20 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ - ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field. + ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end; try field; auto. rewrite <-HT1, <-HT2; field; rewrite HT1. - (* denominators are not zero, I promise *) - Admitted. + - replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) + with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) + by field; simpl. + admit. + + - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) + with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) + by field. + admit. + Qed. Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). @@ -263,11 +380,13 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *) Admitted. - Lemma zeroIsIdentity' : forall P, unifiedAdd' P zero = P. - Admitted. - Hint Resolve zeroIsIdentity. + Lemma zeroIsIdentity' : forall P, unifiedAdd' P (proj1_sig zero) = P. + unfold unifiedAdd', zero; simpl; intros; break_let; f_equal; field; + assert (1 <> 0) by admit; auto. + Qed. Lemma zeroIsIdentity : forall P, P + zero = P. + (* Should follow from zeroIsIdentity', but dependent types... *) Admitted. Hint Resolve zeroIsIdentity. @@ -399,11 +518,13 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. - Module Export GFDefs := GaloisDefs M. + Module Export GFDefs := ZGaloisField M. Local Open Scope GF_scope. + Axiom char_gt_2 : (1+1) <> 0. Definition a := inject (- 1). Axiom a_nonzero : a <> 0. - Axiom a_square : exists x, x * x = a. + Parameter sqrt_a : GF. + Axiom a_square : sqrt_a^2 = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End Minus1Params. @@ -428,7 +549,10 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted Hint Unfold projectiveToTwisted twistedToProjective. Lemma GFdiv_1 : forall x, x/1 = x. - Admitted. + Proof. + intros; field. + assert (1 <> 0) by admit; auto. + Qed. Hint Resolve GFdiv_1. Lemma twistedProjectiveInv P : projectiveToTwisted (twistedToProjective P) = P. @@ -536,19 +660,8 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted unfold extendedValid, extendedToProjective, projectiveToTwisted in *. invcs HeqP3. subst. - (* field. -- fails. but it works in sage: -sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2"); -print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * -((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) == -((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) * -(2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * -((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * -((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) / -((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) * -(2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))' - Outputs: - True - *) + field. + (* TODO: prove that denominators are nonzero *) Admitted. Ltac extended0 := repeat progress (autounfold; simpl); intros; -- cgit v1.2.3