From f4425e8a1de9cff978f794e4783eff1bcfede412 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 8 Jan 2016 20:09:52 -0500 Subject: cleanup --- src/Curves/Curve25519.v | 7 ++- src/Curves/PointFormats.v | 135 +++++++++++++++------------------------------- src/Galois/EdDSA.v | 6 ++- 3 files changed, 53 insertions(+), 95 deletions(-) diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index 8bb2148db..4162d4c1c 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -1,5 +1,6 @@ Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. +Require Import Crypto.Galois.ZGaloisField. Require Import Crypto.Curves.PointFormats. Definition two_255_19 := 2^255 - 19. (* *) @@ -9,7 +10,11 @@ Module Modulus25519 <: Modulus. End Modulus25519. Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519. - Module Import GFDefs := GaloisDefs Modulus25519. + Module Import GFDefs := ZGaloisField Modulus25519. + + Lemma char_gt_2 : inject 2 <> 0%GF. + Admitted. + Local Open Scope GF_scope. Coercion inject : Z >-> GF. diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 7e1fd0f81..32e6acdd0 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -6,11 +6,10 @@ Require Import BinNums NArith. Module Type TwistedEdwardsParams (M : Modulus). Module Export GFDefs := ZGaloisField M. Local Open Scope GF_scope. - Axiom char_gt_2 : (1+1) <> 0. + Axiom char_gt_2 : inject 2 <> 0. Parameter a : GF. Axiom a_nonzero : a <> 0. - Parameter sqrt_a : GF. - Axiom a_square : sqrt_a^2 = a. + Axiom a_square : exists sqrt_a, sqrt_a^2 = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End TwistedEdwardsParams. @@ -148,6 +147,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam Admitted. Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}. Admitted. + Hint Resolve mul_nonzero_nonzero. Ltac whatsNotZero := repeat match goal with @@ -175,8 +175,12 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam Proof. unfold onCurve; intuition; whatsNotZero. + pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. + destruct a_square as [sqrt_a a_square]. + rewrite <- a_square in *. + (* Furthermore... *) - pose proof (eq_refl (d*x1^2*y1^2*(a*x2^2 + y2^2))) as Heqt. + pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*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. @@ -184,57 +188,29 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam 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. - - (* contradiction: product of nonzero things is zero *) - destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try (subst; field). - destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]. - + destruct char_gt_2; rewrite <- Hccc; field. - + destruct a_nonzero; rewrite <-a_square, Hccc; field. - - - 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. + (* main equation for both potentially nonzero denominators *) + case_eq_GF (sqrt_a*x2 + y2) 0; case_eq_GF (sqrt_a*x2 - y2) 0; + try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => + assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = + f ((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 Heqw1 by field; + rewrite H1 in *; + replace (1 * y1^2) with (y1^2) in * by field; + rewrite <- Heqt in *; + assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / + (x1 * y1 * (f (sqrt_a * x2) y2))^2) + by (rewriteAny; field; auto); + match goal with [H: d = (?n^2)/(?l^2) |- _ ] => + destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto) + end + end. + + 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. + + (* contradiction: product of nonzero things is zero *) + destruct (mul_zero_why _ _ Hc) as [Hcc|Hcc]; try solve [subst; intuition]; + destruct (mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition; apply Ha_nonzero; field. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : @@ -290,8 +266,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2 = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field). - t x1 y1 x2 y2. - t x2 y2 x1 y1. + t x1 y1 x2 y2; t x2 y2 x1 y1. remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 - (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T. @@ -299,7 +274,6 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam assert (HT2: T = (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)) by (subst; field). - replace 1 with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. match goal with [ |- ?x = 1 ] => replace x with @@ -307,18 +281,13 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam ((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; auto. - - rewrite <-HT1, <-HT2; field; rewrite HT1. - - - replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) + - rewrite <-HT1, <-HT2; field; rewrite HT1; + 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. - repeat apply mul_nonzero_nonzero; auto. - + by field; simpl; auto. - replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field. - repeat apply mul_nonzero_nonzero; auto. + by field; auto. Qed. Lemma unifiedAdd'_onCurve' : forall P1 P2, onCurve P1 -> onCurve P2 -> @@ -540,11 +509,10 @@ End CompleteTwistedEdwardsFacts. Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M. Module Export GFDefs := ZGaloisField M. Local Open Scope GF_scope. - Axiom char_gt_2 : (1+1) <> 0. + Axiom char_gt_2 : inject 2 <> 0. Definition a := inject (- 1). Axiom a_nonzero : a <> 0. - Parameter sqrt_a : GF. - Axiom a_square : sqrt_a^2 = a. + Axiom a_square : exists sqrt_a, sqrt_a^2 = a. Parameter d : GF. Axiom d_nonsquare : forall x, x * x <> d. End Minus1Params. @@ -586,13 +554,7 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted Definition point := extended. Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T). Definition extendedValid (P : point) : Prop := - let pP := extendedToProjective P in - let X := projectiveX pP in - let Y := projectiveY pP in - let Z := projectiveZ pP in - let T := extendedT P in - T = X*Y/Z. - + let '(X, Y, Z, T) := P in T = X*Y/Z. Definition twistedToExtended (P : (GF*GF)) : point := let '(x, y) := P in (x, y, 1, x*y). @@ -639,21 +601,12 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted Local Notation "2" := (1+1). (** Second equation from section 3.1, also and *) Definition unifiedAdd (P1 P2 : point) : point := - let k := 2 * d in - let pP1 := extendedToProjective P1 in - let X1 := projectiveX pP1 in - let Y1 := projectiveY pP1 in - let Z1 := projectiveZ pP1 in - let T1 := extendedT P1 in - let pP2 := extendedToProjective P2 in - let X2 := projectiveX pP2 in - let Y2 := projectiveY pP2 in - let Z2 := projectiveZ pP2 in - let T2 := extendedT P2 in + let '(X1, Y1, Z1, T1) := P1 in + let '(X2, Y2, Z2, T2) := P2 in let A := (Y1-X1)*(Y2-X2) in let B := (Y1+X1)*(Y2+X2) in - let C := T1*k*T2 in - let D := Z1*2*Z2 in + let C := T1*2*d*T2 in + let D := Z1*2 *Z2 in let E := B-A in let F := D-C in let G := D+C in @@ -676,9 +629,7 @@ Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwisted destruct P1 as [[X1 Y1 Z1] T1]. destruct P2 as [[X2 Y2 Z2] T2]. destruct P3 as [[X3 Y3 Z3] T3]. - unfold extendedValid, extendedToProjective, projectiveToTwisted in *. invcs HeqP3. - subst. field. (* TODO: prove that denominators are nonzero *) Admitted. diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v index af4f892ca..de26c678c 100644 --- a/src/Galois/EdDSA.v +++ b/src/Galois/EdDSA.v @@ -1,7 +1,7 @@ Require Import ZArith NPeano. Require Import Bedrock.Word. Require Import Crypto.Curves.PointFormats. -Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory. +Require Import Crypto.Galois.BaseSystem Crypto.Galois.ZGaloisField Crypto.Galois.GaloisTheory. Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. Require Import VerdiTactics. @@ -54,7 +54,7 @@ Module Type EdDSAParams. Axiom n_ge_c : n >= c. Axiom n_le_b : n <= b. - Module Import GFDefs := GaloisDefs Modulus_q. + Module Import GFDefs := ZGaloisField Modulus_q. Local Open Scope GF_scope. (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit @@ -83,6 +83,8 @@ Module Type EdDSAParams. * twisted Edwards addition law. *) Module CurveParameters <: TwistedEdwardsParams Modulus_q. Module GFDefs := GFDefs. + Definition char_gt_2 : inject 2 <> 0. + Admitted. (* follows from q_odd *) Definition a : GF := a. Definition a_nonzero := a_nonzero. Definition a_square := a_square. -- cgit v1.2.3