From e8fab6b839e19da231333ca8173bbb2a3d8a4033 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 11 Feb 2017 21:59:58 -0500 Subject: split the algebra library; use fsatz more --- src/Spec/CompleteEdwardsCurve.v | 4 +- src/Spec/Ed25519.v | 10 ++- src/Spec/MontgomeryCurve.v | 181 ++++++++++++++++++++++++++++++++++++++++ src/Spec/WeierstrassCurve.v | 58 ++++++------- 4 files changed, 213 insertions(+), 40 deletions(-) create mode 100644 src/Spec/MontgomeryCurve.v (limited to 'src/Spec') diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index d475f78c2..05f61f159 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -20,7 +20,7 @@ Module E. Context {a d: F}. Class twisted_edwards_params := { - char_gt_2 : forall p : BinNums.positive, BinPos.Pos.le p 2 -> Pre.ZtoR (BinNums.Zpos p) <> 0; + char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two; nonzero_a : a <> 0; square_a : exists sqrt_a, sqrt_a^2 = a; nonsquare_d : forall x, x^2 <> d @@ -34,7 +34,7 @@ Module E. snd (coordinates P) = snd (coordinates Q). Program Definition zero : point := (0, 1). - Next Obligation. eauto using Pre.onCurve_zero. Qed. + Next Obligation. destruct H; eauto using Pre.onCurve_zero. Qed. Program Definition add (P1 P2:point) : point := let x1y1 := coordinates P1 in let x1 := fst x1y1 in let y1 := snd x1y1 in diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 3d1a30559..7ac33d890 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -11,13 +11,15 @@ Module Pre. Local Open Scope F_scope. Lemma curve25519_params_ok {prime_q:Znumtheory.prime (2^255-19)} : @E.twisted_edwards_params (F (2 ^ 255 - 19)) (@eq (F (2 ^ 255 - 19))) (@F.zero (2 ^ 255 - 19)) - (@F.one (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19)) + (@F.one (2 ^ 255 - 19)) (@F.opp (2 ^ 255 - 19)) (@F.add (2 ^ 255 - 19)) (@F.sub (2 ^ 255 - 19)) (@F.mul (2 ^ 255 - 19)) (@F.opp (2 ^ 255 - 19) 1) (@F.opp (2 ^ 255 - 19) (F.of_Z (2 ^ 255 - 19) 121665) / F.of_Z (2 ^ 255 - 19) 121666). Proof. pose (@PrimeFieldTheorems.F.Decidable_square (2^255-19) _); - SpecializeBy.specialize_by Decidable.vm_decide; split; Decidable.vm_decide_no_check. - Qed. + SpecializeBy.specialize_by Decidable.vm_decide; split; try Decidable.vm_decide_no_check. + { intros n one_le_n n_le_two. + assert ((n = 1 \/ n = 2)%N) as Hn by admit; destruct Hn; subst; Decidable.vm_decide. } + Admitted. End Pre. (* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *) Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q. @@ -48,7 +50,7 @@ Section Ed25519. Global Instance curve_params : E.twisted_edwards_params - (F:=Fq) (Feq:=Logic.eq) (Fzero:=F.zero) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul) + (F:=Fq) (Feq:=Logic.eq) (Fzero:=F.zero) (Fone:=F.one) (Fopp:=F.opp) (Fadd:=F.add) (Fsub:=F.sub) (Fmul:=F.mul) (a:=a) (d:=d). Proof Pre.curve25519_params_ok. Definition E : Type := E.point diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v new file mode 100644 index 000000000..4e448392f --- /dev/null +++ b/src/Spec/MontgomeryCurve.v @@ -0,0 +1,181 @@ +Require Crypto.Algebra. +Require Crypto.Util.GlobalSettings. + +Require Import Crypto.Spec.WeierstrassCurve. + +Module M. + Section MontgomeryCurve. + Import BinNat. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 2}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "- x" := (Fopp x). + Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "( x , y )" := (inl (pair x y)). + Local Open Scope core_scope. + + Context {a b: F} {b_nonzero:b <> 0}. + + Definition point := { P | match P with + | (x, y) => b*y^2 = x^3 + a*x^2 + x + | ∞ => True + end }. + Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + + Import Crypto.Util.Tactics Crypto.Algebra.Field. + Ltac t := + destruct_head' point; destruct_head' sum; destruct_head' prod; + break_match; simpl in *; break_match_hyps; trivial; try discriminate; + repeat match goal with + | |- _ /\ _ => split + | [H:@eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + | [H:@eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H + end; + subst; try fsatz. + + Program Definition add (P1 P2:point) : point := + exist _ + match coordinates P1, coordinates P2 return _ with + (x1, y1), (x2, y2) => + if Decidable.dec (x1 = x2) + then if Decidable.dec (y1 = - y2) + then ∞ + else (b*(3*x1^2+2*a*x1+1)^2/(2*b*y1)^2-a-x1-x1, (2*x1+x1+a)*(3*x1^2+2*a*x1+1)/(2*b*y1)-b*(3*x1^2+2*a*x1+1)^3/(2*b*y1)^3-y1) + else (b*(y2-y1)^2/(x2-x1)^2-a-x1-x2, (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 + end _. + Next Obligation. Proof. t. Qed. + + Program Definition opp (P:point) : point := + exist _ + match P with + | (x, y) => (x, -y) + | ∞ => ∞ + end _. + Next Obligation. + Proof. t. Qed. + + Local Notation "4" := (1+3). + Local Notation "16" := (4*4). + Local Notation "9" := (3*3). + Local Notation "27" := (3*9). + Context {char_gt_27:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul 27}. + + Let WeierstrassA := ((3-a^2)/(3*b^2)). + Let WeierstrassB := ((2*a^3-9*a)/(27*b^3)). + + Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). + Program Definition MontgomeryOfWeierstrass (P:Wpoint) : point := + exist + _ + match W.coordinates P return _ with + | (x,y) => (b*x-a/3, b*y) + | _ => ∞ + end + _. + Next Obligation. + Proof. subst WeierstrassA; subst WeierstrassB; destruct P; t. Qed. + + Definition eq (P1 P2:point) := + match coordinates P1, coordinates P2 with + | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 + | ∞, ∞ => True + | _, _ => False + end. + + Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_gt_2 WeierstrassA WeierstrassB). + Lemma MontgomeryOfWeierstrass_add P1 P2 : + eq (MontgomeryOfWeierstrass (W.add P1 P2)) + (add (MontgomeryOfWeierstrass P1) (MontgomeryOfWeierstrass P2)). + Proof. + cbv [WeierstrassA WeierstrassB eq MontgomeryOfWeierstrass W.add add coordinates W.coordinates proj1_sig] in *; t. + Qed. + + Section AddX. + Lemma homogeneous_x_differential_addition_releations P1 P2 : + match coordinates (add P2 (opp P1)), coordinates P1, coordinates P2, coordinates (add P1 P2) with + | (x, _), (x1, _), (x2, _), (x3, _) => + if Decidable.dec (x1 = x2) + then x3 * (4*x1*(x1^2 + a*x1 + 1)) = (x1^2 - 1)^2 + else x3 * (x*(x1-x2)^2) = (x1*x2 - 1)^2 + | _, _, _, _ => True + end. + Proof. t. Qed. + + Definition onCurve xy := let 'pair x y := xy in b*y^2 = x^3 + a*x^2 + x. + Definition xzpoint := { xz | let 'pair x z := xz in (z = 0 \/ exists y, onCurve (pair (x/z) y)) }. + Definition xzcoordinates (P:xzpoint) : F*F := proj1_sig P. + Program Definition toxz (P:point) : xzpoint := + exist _ + match coordinates P with + | (x, y) => pair x 1 + | ∞ => pair 1 0 + end _. + Next Obligation. t; [right; exists f0; t | left; reflexivity ]. Qed. + + Definition sig_pair_to_pair_sig {T T' I I'} (xy:{xy | let 'pair x y := xy in I x /\ I' y}) + : prod {x:T | I x} {y:T' | I' y} + := let 'exist (pair x y) (conj pfx pfy) := xy in pair (exist _ x pfx) (exist _ y pfy). + + (* From Explicit Formulas Database by Lange and Bernstein, + credited to 1987 Montgomery "Speeding the Pollard and elliptic curve + methods of factorization", page 261, fifth and sixth displays, plus + common-subexpression elimination, plus assumption Z1=1 *) + + Context {a24:F} {a24_correct:4*a24 = a+2}. + Definition xzladderstep (X1:F) (P1 P2:xzpoint) : prod xzpoint xzpoint. refine ( + sig_pair_to_pair_sig (exist _ + match xzcoordinates P1, xzcoordinates P2 return _ with + pair X2 Z2, pair X3 Z3 => + let A := X2+Z2 in + let AA := A^2 in + let B := X2-Z2 in + let BB := B^2 in + let E := AA-BB in + let C := X3+Z3 in + let D := X3-Z3 in + let DA := D*A in + let CB := C*B in + let X5 := (DA+CB)^2 in + let Z5 := X1*(DA-CB)^2 in + let X4 := AA*BB in + let Z4 := E*(BB + a24*E) in + (pair (pair X4 Z4) (pair X5 Z5)) + end _) ). + Proof. + destruct P1, P2; cbv [onCurve xzcoordinates] in *. t; intuition idtac. + { left. fsatz. } + { left. fsatz. } + admit. + admit. + admit. + admit. + { right. + admit. (* the following used to work, but slowly: + exists ((fun x1 y1 x2 y2 => (2*x1+x1+a)*(3*x1^2+2*a*x1+1)/(2*b*y1)-b*(3*x1^2+2*a*x1+1)^3/(2*b*y1)^3-y1) (f1/f2) x0 (f/f0) x). + Algebra.common_denominator_in H. + Algebra.common_denominator_in H0. + Algebra.common_denominator. + abstract Algebra.nsatz. + + idtac. + admit. + admit. + admit. + admit. + admit. *) } + { right. + (* exists ((fun x1 y1 x2 y2 => (2*x1+x2+a)*(y2-y1)/(x2-x1)-b*(y2-y1)^3/(x2-x1)^3-y1) (f1/f2) x0 (f/f0) x). *) + (* XXX: this case is probably not true -- there is not necessarily a guarantee that the output x/z is on curve if [X1] was not the x coordinate of the difference of input points as requored *) + Abort. + End AddX. + End MontgomeryCurve. +End M. \ No newline at end of file diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 484a67c89..8b5480620 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -1,6 +1,6 @@ Require Crypto.WeierstrassCurve.Pre. -Module E. +Module W. Section WeierstrassCurves. (* Short Weierstrass curves with addition laws. References: * @@ -9,7 +9,7 @@ Module E. * (page 79) *) - Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_gt_2:@Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two}. Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope. Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope. @@ -19,57 +19,47 @@ Module E. Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30). Local Notation "'∞'" := unit : type_scope. Local Notation "'∞'" := (inr tt) : core_scope. - Local Notation "0" := Fzero. Local Notation "1" := Fone. - Local Notation "2" := (1+1). Local Notation "3" := (1+2). Local Notation "4" := (1+3). - Local Notation "8" := (1+(1+(1+(1+4)))). Local Notation "12" := (1+(1+(1+(1+8)))). - Local Notation "16" := (1+(1+(1+(1+12)))). Local Notation "20" := (1+(1+(1+(1+16)))). - Local Notation "24" := (1+(1+(1+(1+20)))). Local Notation "27" := (1+(1+(1+24))). Local Notation "( x , y )" := (inl (pair x y)). Local Open Scope core_scope. Context {a b: F}. - (** N.B. We may require more conditions to prove that points form - a group under addition (associativity, in particular. If - that's the case, more fields will be added to this class. *) - Class weierstrass_params := - { - char_gt_2 : 2 <> 0; - char_ne_3 : 3 <> 0; - nonzero_discriminant : -(16) * (4 * a^3 + 27 * b^2) <> 0 - }. - Context `{weierstrass_params}. - Definition point := { P | match P with | (x, y) => y^2 = x^3 + a*x + b | ∞ => True end }. Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. - (** The following points are indeed on the curve -- see [WeierstrassCurve.Pre] for proof *) - Local Obligation Tactic := - try solve [ Program.Tactics.program_simpl - | intros; apply (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)) ]. + Definition eq (P1 P2:point) := + match coordinates P1, coordinates P2 with + | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 + | ∞, ∞ => True + | _, _ => False + end. Program Definition zero : point := ∞. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Program Definition add (P1 P2:point) : point := exist _ (match coordinates P1, coordinates P2 return _ with | (x1, y1), (x2, y2) => if x1 =? x2 then - if y2 =? -y1 then ∞ - else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, - (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) - else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, - (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) - | ∞, ∞ => ∞ - | ∞, _ => coordinates P2 - | _, ∞ => coordinates P1 + if y2 =? -y1 then ∞ + else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, + (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) + else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, + (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 end) _. + Next Obligation. exact (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed. Fixpoint mul (n:nat) (P : point) : point := match n with @@ -77,8 +67,8 @@ Module E. | S n' => add P (mul n' P) end. End WeierstrassCurves. -End E. +End W. -Delimit Scope E_scope with E. -Infix "+" := E.add : E_scope. -Infix "*" := E.mul : E_scope. +Delimit Scope W_scope with W. +Infix "+" := W.add : W_scope. +Infix "*" := W.mul : W_scope. -- cgit v1.2.3