From a1ab6f7b47173ff927958a19b952f26078ddf373 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 7 Jan 2016 11:20:39 -0500 Subject: Start writing PointFormats field proofs --- src/Curves/PointFormats.v | 34 +++++++++++++++++++++++++++++----- 1 file changed, 29 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 1e8df9337..cae6f939d 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -1,4 +1,4 @@ -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField. +Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ZGaloisField. Require Import Tactics.VerdiTactics. Require Import Logic.Eqdep_dec. Require Import BinNums NArith. @@ -8,7 +8,7 @@ Module GaloisDefs (M : Modulus). End GaloisDefs. Module Type TwistedEdwardsParams (M : Modulus). - Module Export GFDefs := GaloisDefs M. + Module Export GFDefs := ZGaloisField M. Local Open Scope GF_scope. Parameter a : GF. Axiom a_nonzero : a <> 0. @@ -125,7 +125,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam Hint Unfold onCurve mkPoint. Definition zero : point. exists (0, 1). - abstract (unfold onCurve; ring). + abstract (unfold onCurve; field). Defined. Definition unifiedAdd' (P1' P2' : (GF*GF)) := @@ -138,8 +138,28 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam let 'exist P2' pf2 := P2 in mkPoint (unifiedAdd' P1' P2') _). Proof. - destruct P1' as [x1 y1], P2' as [x2 y2]; unfold unifiedAdd', onCurve. - admit. (* field will likely work here, but I have not done this by hand *) + (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1, c=1 and an extra a in front of x^2 *) + destruct P1' as [x1 y1], P2' as [x2 y2]. + remember (unifiedAdd' (x1, y1) (x2, y2)) as P3. + destruct P3 as [x3 y3]. injection HeqP3; clear HeqP3; intros. + unfold unifiedAdd', onCurve in *. + + 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); + 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. + + 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. + assert (T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field). + assert (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. + (* change all fractions to a common denominator and merge. That fraction will be T/T based on the hypotheses. Which is 1. *) + admit. Defined. Local Infix "+" := unifiedAdd. @@ -221,6 +241,10 @@ 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, P + zero = P. Admitted. Hint Resolve zeroIsIdentity. -- cgit v1.2.3