From e97200ea903c57574026c6b6d0be73ad0bfed991 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 29 Mar 2017 00:27:15 -0400 Subject: use improved fsatz on various elliptic curve things partial correctness of projective addition stronger projective addition proof fixup --- src/CompleteEdwardsCurve/EdwardsMontgomery.v | 113 ++++++++++++++++ src/MontgomeryCurveTheorems.v | 112 ++++++++++++++++ src/MontgomeryX.v | 82 ++++++++++++ src/Spec/MontgomeryCurve.v | 186 ++++++--------------------- src/WeierstrassCurve/Projective.v | 153 ++++++++++++++++++++++ 5 files changed, 498 insertions(+), 148 deletions(-) create mode 100644 src/CompleteEdwardsCurve/EdwardsMontgomery.v create mode 100644 src/MontgomeryCurveTheorems.v create mode 100644 src/MontgomeryX.v create mode 100644 src/WeierstrassCurve/Projective.v (limited to 'src') diff --git a/src/CompleteEdwardsCurve/EdwardsMontgomery.v b/src/CompleteEdwardsCurve/EdwardsMontgomery.v new file mode 100644 index 000000000..2a987735d --- /dev/null +++ b/src/CompleteEdwardsCurve/EdwardsMontgomery.v @@ -0,0 +1,113 @@ +Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems. + +Require Import Crypto.Util.Notations Crypto.Util.Decidable. +Require Import Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod. +Require Import Crypto.Algebra Crypto.Algebra.Field. + +Module E. + Section EdwardsMontgomery. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} + {Feq_dec:DecidableRel Feq}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "x ^ 2" := (x*x). + + Context {a d: F} + {nonzero_a : a <> 0} + {square_a : exists sqrt_a, sqrt_a^2 = a} + {nonsquare_d : forall x, x^2 <> d}. + Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). + Local Notation Ezero := (E.zero(nonzero_a:=nonzero_a)(d:=d)). + Local Notation Eadd := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). + Local Notation Eopp := (E.opp(nonzero_a:=nonzero_a)(d:=d)). + + Let a_neq_d : a <> d. + Proof. intro X. + edestruct square_a. eapply nonsquare_d. + rewrite <-X. eassumption. Qed. + + + Local Notation "2" := (1+1). Local Notation "4" := (1+1+1+1). + Local Notation MontgomeryA := (2*(a+d)/(a-d)). + Local Notation MontgomeryB := (4/(a-d)). + + Let b_nonzero : MontgomeryB <> 0. Proof. fsatz. Qed. + + Local Notation Mpoint := (@M.point F Feq Fadd Fmul MontgomeryA MontgomeryB). + Local Notation Madd := (@M.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 MontgomeryA MontgomeryB b_nonzero). + Local Notation "'∞'" := (inr tt) : core_scope. + + Ltac t_step := + match goal with + | _ => solve [ contradiction | trivial ] + | _ => progress intros + | _ => progress subst + | _ => progress Tactics.DestructHead.destruct_head' @M.point + | _ => progress Tactics.DestructHead.destruct_head' @prod + | _ => progress Tactics.DestructHead.destruct_head' @sum + | _ => progress Tactics.DestructHead.destruct_head' @and + | _ => progress Sum.inversion_sum + | _ => progress Prod.inversion_prod + | _ => progress Tactics.BreakMatch.break_match_hyps + | _ => progress Tactics.BreakMatch.break_match + | _ => progress cbv [E.coordinates M.coordinates E.add M.add E.zero M.zero E.eq M.eq E.opp M.opp proj1_sig fst snd] in * + | |- _ /\ _ => split + end. + Ltac t := repeat t_step. + + Program Definition to_Montgomery (P:Epoint) : Mpoint := + match E.coordinates P return F*F+_ with + | (x, y) => + if dec (y <> 1 /\ x <> 0) + then inl ((1+y)/(1-y), (1+y)/(x-x*y)) + else ∞ + end. + Next Obligation. Proof. t. fsatz. Qed. + + (* The exceptional cases are tricky. *) + (* See https://eprint.iacr.org/2008/013.pdf page 5 before continuing *) + + Program Definition of_Montgomery (P:Mpoint) : Epoint := + match M.coordinates P return F*F with + | inl (x,y) => + if dec (y = 0) + then (0, Fopp 1) + else (x/y, (x-1)/(x+1)) + | ∞ => pair 0 1 + end. + Next Obligation. + Proof. + t; try fsatz. + assert (f1 <> Fopp 1) by admit (* ad, d are nonsero *); fsatz. + Admitted. + + Import BinNums. + (* TODO: characteristic weakening lemmas *) + Context {char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}. + Context {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. + + Program Definition _EM : _ /\ _ /\ _ := + @Group.group_from_redundant_representation + Mpoint M.eq Madd M.zero M.opp + (M.group(discr_nonzero:=_)) + Epoint E.eq Eadd Ezero Eopp + of_Montgomery + to_Montgomery + _ _ _ _ _ + . + Next Obligation. Proof. Admitted. (* discriminant nonzero *) + Next Obligation. Proof. Admitted. (* M->E->M *) + Next Obligation. Proof. Admitted. (* M->E->M *) + Next Obligation. Proof. Admitted. (* add *) + Next Obligation. Proof. Admitted. (* opp *) + Next Obligation. Proof. cbv [of_Montgomery to_Montgomery]; t; fsatz. Qed. + + Global Instance homomorphism_of_Montgomery : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 _EM). + Global Instance homomorphism_to_Montgomery : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 _EM). + End EdwardsMontgomery. +End E. diff --git a/src/MontgomeryCurveTheorems.v b/src/MontgomeryCurveTheorems.v new file mode 100644 index 000000000..2f226b594 --- /dev/null +++ b/src/MontgomeryCurveTheorems.v @@ -0,0 +1,112 @@ +Require Import Crypto.Algebra Crypto.Algebra.Field. +Require Import Crypto.Util.GlobalSettings. +Require Import Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod. +Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve. +Require Import Crypto.WeierstrassCurve.WeierstrassCurveTheorems. + +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_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + 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}. + + Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b := + match P return F*F+∞ with + | (x, y) => (x, -y) + | ∞ => ∞ + end. + Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed. + + Ltac t := + repeat + match goal with + | _ => solve [ trivial ] + | _ => progress intros + | _ => progress subst + | _ => progress Tactics.DestructHead.destruct_head' @M.point + | _ => progress Tactics.DestructHead.destruct_head' @prod + | _ => progress Tactics.DestructHead.destruct_head' @sum + | _ => progress Tactics.DestructHead.destruct_head' @and + | _ => progress Sum.inversion_sum + | _ => progress Prod.inversion_prod + | _ => progress Tactics.BreakMatch.break_match_hyps + | _ => progress Tactics.BreakMatch.break_match + | _ => progress cbv [M.coordinates M.add M.zero M.eq opp proj1_sig] in * + | _ => progress cbv [W.coordinates W.add W.zero W.eq W.inv proj1_sig] in * + | |- _ /\ _ => split | |- _ <-> _ => split + end. + + Local Notation add := (M.add(b_nonzero:=b_nonzero)). + Local Notation point := (@M.point F Feq Fadd Fmul a b). + + Section MontgomeryWeierstrass. + Local Notation "4" := (1+3). + Local Notation "16" := (4*4). + Local Notation "9" := (3*3). + Local Notation "27" := (3*9). + Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. + + + Local Notation WeierstrassA := ((3-a^2)/(3*b^2)). + Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)). + Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). + Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB). + Program Definition to_Weierstrass (P:@point) : Wpoint := + match M.coordinates P return F*F+∞ with + | (x, y) => ((x + a/3)/b, y/b) + | _ => ∞ + end. + Next Obligation. Proof. t; fsatz. Qed. + + Program Definition of_Weierstrass (P:Wpoint) : point := + match W.coordinates P return F*F+∞ with + | (x,y) => (b*x-a/3, b*y) + | _ => ∞ + end. + Next Obligation. Proof. t. fsatz. Qed. + + (*TODO: rename inv to opp, make it not require [discr_nonzero] *) + Context {discr_nonzero : (2 + 1 + 1) * WeierstrassA * WeierstrassA * WeierstrassA + + ((2 + 1 + 1) ^ 2 + (2 + 1 + 1) + (2 + 1 + 1) + 1 + 1 + 1) * + WeierstrassB * WeierstrassB <> 0}. + (* TODO: weakening lemma for characteristic *) + Context {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}. + Local Notation Wopp := (@W.inv F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec discr_nonzero). + + Program Definition _MW : _ /\ _ /\ _ := + @Group.group_from_redundant_representation + Wpoint W.eq Wadd W.zero Wopp + (abelian_group_group (W.commutative_group(discriminant_nonzero:=discr_nonzero))) + point M.eq (M.add(b_nonzero:=b_nonzero)) M.zero opp + of_Weierstrass + to_Weierstrass + _ _ _ _ _ + . + Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. + Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. + Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. + Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. + Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed. + + Global Instance group : Algebra.group := proj1 _MW. + Global Instance homomorphism_of_Weierstrass : Monoid.is_homomorphism(phi:=of_Weierstrass) := proj1 (proj2 _MW). + Global Instance homomorphism_to_Weierstrass : Monoid.is_homomorphism(phi:=to_Weierstrass) := proj2 (proj2 _MW). + End MontgomeryWeierstrass. + End MontgomeryCurve. +End M. \ No newline at end of file diff --git a/src/MontgomeryX.v b/src/MontgomeryX.v new file mode 100644 index 000000000..b3e9a5ae8 --- /dev/null +++ b/src/MontgomeryX.v @@ -0,0 +1,82 @@ +Require Import Crypto.Algebra Crypto.Algebra.Field. +Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations. +Require Import Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod. +Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems. + +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_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} + {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}. + 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 ^ 2" := (x*x). + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "( x , y )" := (inl (pair x y)). + + Context {a b: F} {b_nonzero:b <> 0}. + Local Notation add := (M.add(b_nonzero:=b_nonzero)). + Local Notation opp := (M.opp(b_nonzero:=b_nonzero)). + Local Notation point := (@M.point F Feq Fadd Fmul a b). + + Program Definition to_xz (P:point) : F*F := + match M.coordinates P with + | (x, y) => pair x 1 + | ∞ => pair 1 0 + end. + + (* From Curve25519 paper by djb, appendix B. Credited to Montgomery *) + Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}. + Definition xzladderstep (x1:F) (Q Q':F*F) : ((F*F)*(F*F)) := + match Q, Q' with + pair x z, pair x' z' => + let A := x+z in + let B := x-z in + let AA := A^2 in + let BB := B^2 in + let x2 := AA*BB in + let E := AA-BB in + let z2 := E*(AA + a24*E) in + let C := x'+z' in + let D := x'-z' in + let CB := C*B in + let DA := D*A in + let x3 := (DA+CB)^2 in + let z3 := x1*(DA-CB)^2 in + (pair (pair x2 z2) (pair x3 z3)) + end. + + Ltac t := + repeat + match goal with + | _ => solve [ contradiction | trivial ] + | _ => progress intros + | _ => progress subst + | _ => progress Tactics.DestructHead.destruct_head' @M.point + | _ => progress Tactics.DestructHead.destruct_head' @prod + | _ => progress Tactics.DestructHead.destruct_head' @sum + | _ => progress Tactics.DestructHead.destruct_head' @and + | _ => progress Sum.inversion_sum + | _ => progress Prod.inversion_prod + | _ => progress Tactics.BreakMatch.break_match_hyps + | _ => progress Tactics.BreakMatch.break_match + | _ => progress cbv [fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig xzladderstep to_xz] in * + | |- _ /\ _ => split + end. + + Lemma xzladderstep_correct + (Q Q':point) x z x' z' x1 x2 z2 x3 z3 + (Hl:Logic.eq (pair(pair x2 z2)(pair x3 z3)) (xzladderstep x1 (pair x z) (pair x' z'))) + (H:match M.coordinates Q with∞=>z=0/\x<>0|(xQ,y)=>xQ=x/z/\z<>0 (* TODO *) /\ y <> 0 (* TODO: prove this from non-squareness of a^2 - 4 *) end) + (H':match M.coordinates Q' with∞=>z'=0/\x'<>0|(xQ',_)=>xQ'=x'/z'/\z'<>0 end) + (H1:match M.coordinates (add Q (opp Q')) with∞=>False|(x,y)=>x=x1/\x<>0 end): + match M.coordinates (add Q Q) with∞=>z2=0/\x2<>0|(xQQ,_)=>xQQ=x2/z2/\z2<>0 end /\ + match M.coordinates (add Q Q') with∞=>z3=0/\x3<>0|(xQQ',_)=>xQQ'=x3/z3/\z3<>0 end. + Proof. t; abstract fsatz. Qed. + End MontgomeryCurve. +End M. \ No newline at end of file diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v index cff35104c..a12f2ef96 100644 --- a/src/Spec/MontgomeryCurve.v +++ b/src/Spec/MontgomeryCurve.v @@ -1,20 +1,22 @@ -Require Crypto.Algebra. +Require Crypto.Algebra Crypto.Algebra.Field. Require Crypto.Util.GlobalSettings. - -Require Import Crypto.Spec.WeierstrassCurve. +Require Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod. 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_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. + 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_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}. 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 "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)). @@ -22,12 +24,14 @@ Module M. 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 point := { P : F*F+∞ | 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. + Program Definition zero : point := ∞. + Definition eq (P1 P2:point) := match coordinates P1, coordinates P2 with | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2 @@ -35,150 +39,36 @@ Module M. | _, _ => False end. - 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:@Logic.eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H - | [H:@Logic.eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H - end; - subst; try fsatz. - Program Definition add (P1 P2:point) : point := match coordinates P1, coordinates P2 return F*F+∞ 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 + else let k := (3*x1^2 + 2*a*x1 + 1)/(2*b*y1) in + (b*k^2 - a - x1 - x1, (2*x1 + x1 + a)*k - b*k^3 - y1) + else let k := (y2 - y1)/(x2-x1) in + (b*k^2 - a - x1 - x2, (2*x1 + x2 + a)*k - b*k^3 - y1) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 end. - Next Obligation. Proof. t. Qed. - - Program Definition zero : point := ∞. - - Program Definition opp (P:point) : point := - match P return F*F+∞ 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_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. - - Local Notation WeierstrassA := ((3-a^2)/(3*b^2)). - Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)). - Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB). - Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB). - - Program Definition to_Weierstrass (P:point) : Wpoint := - match coordinates P return F*F+∞ with - | (x, y) => ((x + a/3)/b, y/b) - | _ => ∞ - end. - Next Obligation. - Proof. clear char_ge_3; destruct P; t. Qed. - - Program Definition of_Weierstrass (P:Wpoint) : point := - match W.coordinates P return F*F+∞ with - | (x,y) => (b*x-a/3, b*y) - | _ => ∞ - end. - Next Obligation. - Proof. clear char_ge_3; destruct P; t. Qed. - - (* TODO: move *) - Program Definition Wopp (P:Wpoint) : Wpoint := - match P return F*F+∞ with - | (x, y) => (x, -y) - | ∞ => ∞ - end. - Next Obligation. destruct P; t. Qed. - - Axiom Wgroup : @Algebra.group Wpoint (@W.eq F Feq Fadd Fmul WeierstrassA WeierstrassB) - Wadd (@W.zero F Feq Fadd Fmul WeierstrassA WeierstrassB) Wopp. - Program Definition _MW : _ /\ _ /\ _ := - @Group.group_from_redundant_representation - Wpoint W.eq Wadd W.zero Wopp - Wgroup - point eq add zero opp - of_Weierstrass - to_Weierstrass - _ _ _ _ _ - . - Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *; t. Qed. - Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. 2:intuition idtac. 2:intuition idtac. 2:intuition idtac. - { repeat split; destruct_head' and; t. } Qed. Next Obligation. - (* addition case, same issue as in Weierstrass associativity *) - cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *. - clear char_ge_3. t. Qed. - Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add Wopp opp coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. Qed. - Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add Wopp opp coordinates W.coordinates proj1_sig] in *. clear char_ge_3. 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. - - Program Definition to_xz (P:point) : F*F := - match coordinates P with - | (x, y) => pair x 1 - | ∞ => pair 1 0 - end. - - (* 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}. (* TODO: +2 or -2 ? *) - Definition xzladderstep (X1:F) (P1 P2:F*F) : ((F*F)*(F*F)) := - match P1, P2 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. - - Require Import Crypto.Util.Tuple. - - (* TODO: look up this lemma statement -- the current one may not be right *) - Lemma xzladderstep_to_xz X1 P1 P2 - (HX1 : match coordinates (add P1 (opp P2)) with (x,y) => X1 = x | _ => False end) - : fieldwise (n:=2) (fieldwise (n:=2) Feq) - (xzladderstep X1 (to_xz P1) (to_xz P2)) - (pair (to_xz (add P1 P2)) (to_xz (add P1 P1))). - destruct P1 as [[[??]|?]?], P2 as [[[??]|?]?]; - cbv [fst snd xzladderstep to_xz add coordinates proj1_sig opp fieldwise fieldwise'] in *; - break_match_hyps; break_match; repeat split; try contradiction. - Abort. - End AddX. + Proof. + repeat match goal with + | _ => solve [ trivial ] + | _ => progress Tactics.DestructHead.destruct_head' @point + | _ => progress Tactics.DestructHead.destruct_head' @prod + | _ => progress Tactics.DestructHead.destruct_head' @sum + | _ => progress Sum.inversion_sum + | _ => progress Prod.inversion_prod + | _ => progress Tactics.BreakMatch.break_match_hyps + | _ => progress Tactics.BreakMatch.break_match + | _ => progress subst + | _ => progress cbv [coordinates proj1_sig] in * + | |- _ /\ _ => split + | |- _ => Field.fsatz + end. + Qed. End MontgomeryCurve. -End M. \ No newline at end of file +End M. diff --git a/src/WeierstrassCurve/Projective.v b/src/WeierstrassCurve/Projective.v new file mode 100644 index 000000000..a62bf027a --- /dev/null +++ b/src/WeierstrassCurve/Projective.v @@ -0,0 +1,153 @@ +Require Import Crypto.Spec.WeierstrassCurve. +Require Import Crypto.Util.Decidable Crypto.Util.Tactics Crypto.Algebra.Field. +Require Import Crypto.Util.Notations Crypto.Util.FixCoqMistakes. +Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.Sigma. + +Module Projective. + Section Projective. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} + {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))} + {Feq_dec:DecidableRel Feq}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Infix "+" := Fadd. Local Infix "-" := Fsub. + Local Infix "*" := Fmul. Local Infix "/" := Fdiv. + Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2). + Local Notation Wpoint := (@W.point F Feq Fadd Fmul a b). + + (* Originally from + + "Commplete Systems of Addition Laws" by Bosma and Lenstra; + optimized in "Complete + addition formulas for prime order elliptic curves" Algorithm 1 + "Complete, projective point addition for arbitrary prime order + short Weierstrass curves" by Joost Renes, Craig Costello, and + Lejla Batina. *) + + Ltac t := + repeat match goal with + | _ => solve [ contradiction | trivial ] + | _ => progress cbv zeta + | _ => progress intros + | _ => progress destruct_head' @W.point + | _ => progress destruct_head' sum + | _ => progress destruct_head' prod + | _ => progress destruct_head' unit + | _ => progress destruct_head' and + | _ => progress specialize_by assumption + | _ => progress cbv [W.eq W.add W.coordinates proj1_sig] in * + | _ => progress break_match_hyps + | _ => progress break_match + | |- _ /\ _ => split + end. + + Definition point : Type := { P : F*F*F | let '(X,Y,Z) := P in Y^2*Z = X^3 + a*X*Z^2 + b*Z^3 /\ (Z = 0 -> Y <> 0) }. + + Program Definition to_affine (P:point) : Wpoint := + match proj1_sig P return F*F+_ with + | (X, Y, Z) => + if dec (Z = 0) then inr tt + else inl (X/Z, Y/Z) + end. + Next Obligation. Proof. t. fsatz. Qed. + + Program Definition of_affine (P:Wpoint) : point := + match W.coordinates P return F*F*F with + | inl (x, y) => (x, y, 1) + | inr _ => (0, 1, 0) + end. + Next Obligation. Proof. t; fsatz. Qed. + + Program Definition opp (P:point) : point := + match proj1_sig P return F*F*F with + | (X, Y, Z) => (X, Fopp Y, Z) + end. + Next Obligation. Proof. t; fsatz. Qed. + + Context (three_b:F) (three_b_correct: three_b = b+b+b). + Local Notation "4" := (1+1+1+1). Local Notation "27" := (4*4 + 4+4 +1+1+1). + Context {discriminant_nonzero: id(4*a*a*a + 27*b*b <> 0)}. + + Program Definition add (P Q:point) + (y_PmQ_nz: match W.coordinates (W.add (to_affine P) (to_affine (opp Q))) return Prop with + | inr _ => True + | inl (_, y) => y <> 0 + end) : point := + match proj1_sig P, proj1_sig Q return F*F*F with (X1, Y1, Z1), (X2, Y2, Z2) => + let t0 := X1*X2 in + let t1 := Y1*Y2 in + let t2 := Z1*Z2 in + let t3 := X1+Y1 in + let t4 := X2+Y2 in + let t3 := t3*t4 in + let t4 := t0+t1 in + let t3 := t3-t4 in + let t4 := X1+Z1 in + let t5 := X2+Z2 in + let t4 := t4*t5 in + let t5 := t0+t2 in + let t4 := t4-t5 in + let t5 := Y1+Z1 in + let X3 := Y2+Z2 in + let t5 := t5*X3 in + let X3 := t1+t2 in + let t5 := t5-X3 in + let Z3 := a*t4 in + let X3 := three_b*t2 in + let Z3 := X3+Z3 in + let X3 := t1-Z3 in + let Z3 := t1+Z3 in + let Y3 := X3*Z3 in + let t1 := t0+t0 in + let t1 := t1+t0 in + let t2 := a*t2 in + let t4 := three_b*t4 in + let t1 := t1+t2 in + let t2 := t0-t2 in + let t2 := a*t2 in + let t4 := t4+t2 in + let t0 := t1*t4 in + let Y3 := Y3+t0 in + let t0 := t5*t4 in + let X3 := t3*X3 in + let X3 := X3-t0 in + let t0 := t3*t1 in + let Z3 := t5*Z3 in + let Z3 := Z3+t0 in + (X3, Y3, Z3) + end. + Next Obligation. + Proof. + destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1]. + destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2]. + t. + all: try abstract fsatz. + (* FIXME: the final fsatz starts requiring 56 <> 0 if + - the next assert block is removed + - the assertion is changed to [Y2 = Fopp Y1] *) + assert (Y2 / Z2 = Fopp (Y1 / Z1)) by ( + assert (forall pfP pfQ, match W.coordinates (W.add (to_affine (exist _ (X1,Y1,Z1) pfP)) (to_affine (exist _ (X2,Y2,Z2) pfQ))) with inl _ => False | _ => True end) by (cbv [to_affine]; t; fsatz); cbv [to_affine] in *; t; specialize_by (t;fsatz); t; fsatz). + unfold id in discriminant_nonzero; fsatz. + Qed. + + Lemma to_affine_add P Q H : + W.eq + (to_affine (add P Q H)) + (WeierstrassCurve.W.add (to_affine P) (to_affine Q)). + Proof. + destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1]. + destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2]. + cbv [add opp to_affine] in *; t. + all: try abstract fsatz. + + (* zero + P = P -- cases for x and y *) + assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. + assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. + + (* P + zero = P -- cases for x and y *) + assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. + assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz. + Qed. + End Projective. +End Projective. \ No newline at end of file -- cgit v1.2.3