From c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 22:53:07 -0400 Subject: rename-everything --- src/Curves/Edwards/AffineProofs.v | 316 ++++++++++++++++++++++++++++++++++ src/Curves/Edwards/Montgomery.v | 114 ++++++++++++ src/Curves/Edwards/Pre.v | 46 +++++ src/Curves/Edwards/XYZT.v | 140 +++++++++++++++ src/Curves/Montgomery/Affine.v | 67 +++++++ src/Curves/Montgomery/AffineProofs.v | 83 +++++++++ src/Curves/Montgomery/XZ.v | 57 ++++++ src/Curves/Montgomery/XZProofs.v | 58 +++++++ src/Curves/Weierstrass/Affine.v | 18 ++ src/Curves/Weierstrass/AffineProofs.v | 196 +++++++++++++++++++++ src/Curves/Weierstrass/Pre.v | 62 +++++++ src/Curves/Weierstrass/Projective.v | 157 +++++++++++++++++ 12 files changed, 1314 insertions(+) create mode 100644 src/Curves/Edwards/AffineProofs.v create mode 100644 src/Curves/Edwards/Montgomery.v create mode 100644 src/Curves/Edwards/Pre.v create mode 100644 src/Curves/Edwards/XYZT.v create mode 100644 src/Curves/Montgomery/Affine.v create mode 100644 src/Curves/Montgomery/AffineProofs.v create mode 100644 src/Curves/Montgomery/XZ.v create mode 100644 src/Curves/Montgomery/XZProofs.v create mode 100644 src/Curves/Weierstrass/Affine.v create mode 100644 src/Curves/Weierstrass/AffineProofs.v create mode 100644 src/Curves/Weierstrass/Pre.v create mode 100644 src/Curves/Weierstrass/Projective.v (limited to 'src/Curves') diff --git a/src/Curves/Edwards/AffineProofs.v b/src/Curves/Edwards/AffineProofs.v new file mode 100644 index 000000000..2d1db7126 --- /dev/null +++ b/src/Curves/Edwards/AffineProofs.v @@ -0,0 +1,316 @@ +Require Export Crypto.Spec.CompleteEdwardsCurve. + +Require Import Crypto.Algebra.Hierarchy Crypto.Util.Decidable. +Require Import Coq.Logic.Eqdep_dec. +Require Import Coq.Classes.Morphisms. +Require Import Coq.Relations.Relation_Definitions. +Require Import Crypto.Util.Tuple Crypto.Util.Notations. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SetoidSubst. +Require Export Crypto.Util.FixCoqMistakes. + +Module E. + Import Group ScalarMult Ring Field CompleteEdwardsCurve.E. + + Notation onCurve_zero := Pre.onCurve_zero. + Notation denominator_nonzero := Pre.denominator_nonzero. + Notation denominator_nonzero_x := Pre.denominator_nonzero_x. + Notation denominator_nonzero_y := Pre.denominator_nonzero_y. + Notation onCurve_add := Pre.onCurve_add. + + Section CompleteEdwardsCurveTheorems. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@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 onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). + Local Notation point := (@E.point F Feq Fone Fadd Fmul a d). + Local Notation eq := (@E.eq F Feq Fone Fadd Fmul a d). + Local Notation zero := (E.zero(nonzero_a:=nonzero_a)(d:=d)). + Local Notation add := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). + Local Notation mul := (E.mul(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). + + Program Definition opp (P:point) : point := (Fopp (fst P), (snd P)). + Next Obligation. destruct P as [ [??]?]; cbv; fsatz. Qed. + + Ltac t_step := + match goal with + | _ => solve [trivial | exact _ ] + | _ => intro + | |- Equivalence _ => split + | |- abelian_group => split | |- group => split | |- monoid => split + | |- is_associative => split | |- is_commutative => split + | |- is_left_inverse => split | |- is_right_inverse => split + | |- is_left_identity => split | |- is_right_identity => split + | _ => progress destruct_head' @E.point + | _ => progress destruct_head' prod + | _ => progress destruct_head' and + | |- context[E.add ?P ?Q] => + unique pose proof (Pre.denominator_nonzero_x _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q)); + unique pose proof (Pre.denominator_nonzero_y _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q)) + | _ => progress cbv [opp E.zero E.eq E.add E.coordinates proj1_sig fieldwise fieldwise'] in * + (* [_gather_nonzeros] must run before [fst_pair] or [simpl] but after splitting E.eq and unfolding [E.add] *) + | |- _ /\ _ => split | |- _ <-> _ => split + end. + Ltac t := repeat t_step; fsatz. + + Global Instance associative_add : is_associative(eq:=E.eq)(op:=add). + Proof using Type. + (* [nsatz_compute] for a denominator runs out of 6GB of stack space *) + (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5359 *) + Add Field _field : (Algebra.Field.field_theory_for_stdlib_tactic (T:=F)). + Import Field_tac. + repeat t_step; (field_simplify_eq; [IntegralDomain.nsatz|]); repeat split; trivial. + { intro. eapply H3. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } + { intro. eapply H. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } + { intro. eapply H4. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } + { intro. eapply H0. field_simplify_eq; repeat split; trivial. IntegralDomain.nsatz. } + Qed. + + Global Instance edwards_curve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp). + Proof using Type. t. Qed. + + Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof using Type. repeat t_step. Qed. + + Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul. + Proof using Type. + intros n n'; repeat intro; subst n'. + induction n; (reflexivity || eapply (_:Proper (eq==>eq==>eq) add); eauto). + Qed. + + Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul. + Proof using Type. split; intros; (reflexivity || exact _). Qed. + + Section PointCompression. + Local Notation "x ^ 2" := (x*x). + + Lemma solve_correct x y : onCurve x y <-> (x^2 = (y^2-1) / (d*y^2-a)). + Proof using Feq_dec field nonsquare_d nonzero_a square_a. destruct square_a as [sqrt_a]; pose proof (nonsquare_d (sqrt_a/y)); + split; intros; fsatz. Qed. + + (* TODO: move *) + Definition exist_option {A} (P : A -> Prop) (x : option A) + : match x with Some v => P v | None => True end -> option { a : A | P a }. + destruct x; intros; [apply Some | apply None]; eauto. Defined. + Lemma exist_option_Some {A} P (x:option A) pf s + (H:Logic.eq (exist_option P x pf) (Some s)) + : Logic.eq x (Some (proj1_sig s)). + Proof using Type. destruct x, s; cbv [exist_option proj1_sig] in *; congruence. Qed. + Lemma exist_option_None {A} P (x:option A) pf + (H:Logic.eq (exist_option P x pf) None) + : Logic.eq x None. + Proof using Type. destruct x; cbv [exist_option proj1_sig] in *; congruence. Qed. + + Context + {sqrt_div:F -> F -> option F} + {sqrt_Some: forall u v r, Logic.eq (sqrt_div u v) (Some r) -> r^2 = u/v} + {sqrt_None: forall u v, Logic.eq (sqrt_div u v) None -> forall r, r^2 <> u/v} + {parity:F -> bool} {Proper_parity: Proper (Feq ==> Logic.eq) parity} + {parity_opp: forall x, x <> 0 -> Logic.eq (parity (Fopp x)) (negb (parity x)) }. + + Definition compress (P:point) : (bool*F) := + let (x, y) := coordinates P in pair (parity x) y. + Definition set_sign r p : option F := + if dec (Logic.eq (parity r) p) + then Some r + else + let r' := Fopp r in + if dec (Logic.eq (parity r') p) + then Some r' + else None. + Lemma set_sign_None r p s (H:Logic.eq (set_sign r p) (Some s)) + : s^2 = r^2 /\ Logic.eq (parity s) p. + Proof using Feq_dec field nonzero_a. + repeat match goal with + | _ => progress subst + | _ => progress cbv [set_sign] in * + | _ => progress break_match_hyps + | _ => progress Option.inversion_option + | _ => split + | _ => solve [ trivial | fsatz ] + end. + Qed. + Lemma set_sign_Some r p (H:Logic.eq (set_sign r p) None) + : forall s, s^2 = r^2 -> not (Logic.eq (parity s) p). + repeat match goal with + | _ => progress intros + | _ => progress subst + | _ => progress cbv [set_sign] in * + | _ => progress break_match_hyps + | _ => progress Option.inversion_option + end. + destruct (dec (r = 0)). + assert (s = 0); [|solve[setoid_subst_rel Feq; trivial] ]. + admit. + progress rewrite parity_opp in * by assumption. + destruct (parity r), p; cbv [negb] in *; congruence. + Admitted. + + Local Ltac t_step := + match goal with + | _ => progress subst + | _ => progress destruct_head' @E.point + | _ => progress destruct_head' and + | _ => progress break_match + | _ => progress break_match_hyps + | _ => progress Option.inversion_option + | _ => progress Prod.inversion_prod + | H:_ |- _ => unique pose proof (sqrt_Some _ _ _ H); clear H + | H:_ |- _ => unique pose proof (sqrt_None _ _ H); clear H + | H:_ |- _ => unique pose proof (set_sign_None _ _ _ H); clear H + | H:_ |- _ => unique pose proof (set_sign_Some _ _ H); clear H + | H:_ |- _ => unique pose proof (exist_option_Some _ _ _ _ H); clear H + | H:_ |- _ => unique pose proof (exist_option_None _ _ _ H); clear H + | _ => solve [trivial | eapply solve_correct; fsatz] + end. + Local Ltac t := repeat t_step. + + Program Definition decompress (b:bool*F) : option point := + exist_option _ + match b return option (F*F) with + (p, y) => + match sqrt_div (y^2 - 1) (d*y^2 - a) return option (F*F) with + | None => None + | Some r => + match set_sign r p return option (F*F) with + | Some x => Some (x, y) + | None => None + end + end + end _. + Next Obligation. t. Qed. + + Lemma decompress_Some b P (H:Logic.eq (decompress b) (Some P)) + : Logic.eq (compress P) b. + Proof using Type. cbv [compress decompress] in *; t. Qed. + + Lemma decompress_None b (H:Logic.eq (decompress b) None) + : forall P, not (Logic.eq (compress P) b). + Proof. + cbv [compress decompress exist_option coordinates] in *; intros. + t. + intro. + apply (H0 f); [|congruence]. + admit. + intro. Prod.inversion_prod; subst. + rewrite solve_correct in y. + eapply H. eapply y. + Admitted. + End PointCompression. + End CompleteEdwardsCurveTheorems. + Section Homomorphism. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Fchar_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)} + {Feq_dec:DecidableRel Feq}. + + Context {Fa Fd: F} + {nonzero_a : not (Feq Fa Fzero)} + {square_a : exists sqrt_a, Feq (Fmul sqrt_a sqrt_a) Fa} + {nonsquare_d : forall x, not (Feq (Fmul x x) Fd)}. + + Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} + {fieldK: @Algebra.Hierarchy.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} + {Keq_dec:DecidableRel Keq}. + Context {FtoK:F->K} {HFtoK:@Ring.is_homomorphism F Feq Fone Fadd Fmul + K Keq Kone Kadd Kmul FtoK}. + Context {KtoF:K->F} {HKtoF:@Ring.is_homomorphism K Keq Kone Kadd Kmul + F Feq Fone Fadd Fmul KtoF}. + Context {HisoF:forall x, Feq (KtoF (FtoK x)) x}. + Context {Ka} {Ha:Keq (FtoK Fa) Ka} {Kd} {Hd:Keq (FtoK Fd) Kd}. + + Lemma nonzero_Ka : ~ Keq Ka Kzero. + Proof using Feq_dec HFtoK HKtoF Ha HisoF Keq_dec field fieldK nonzero_a. + rewrite <-Ha. + Ring.pull_homomorphism FtoK. + intro X. + eapply (Monoid.is_homomorphism_phi_proper(phi:=KtoF)) in X. + rewrite 2HisoF in X. + auto. + Qed. + + Lemma square_Ka : exists sqrt_a, Keq (Kmul sqrt_a sqrt_a) Ka. + Proof using Feq_dec HFtoK Ha Keq_dec field fieldK square_a. + destruct square_a as [sqrt_a]. exists (FtoK sqrt_a). + Ring.pull_homomorphism FtoK. rewrite <-Ha. + eapply Monoid.is_homomorphism_phi_proper; assumption. + Qed. + + Lemma nonsquare_Kd : forall x, not (Keq (Kmul x x) Kd). + Proof using Feq_dec HKtoF Hd HisoF Keq_dec field fieldK nonsquare_d. + intros x X. apply (nonsquare_d (KtoF x)). + Ring.pull_homomorphism KtoF. rewrite X. rewrite <-Hd, HisoF. + reflexivity. + Qed. + + (* TODO: character respects isomorphism *) + Global Instance Kchar_ge_2 : + @char_ge K Keq Kzero Kone Kopp Kadd Ksub Kmul (BinNat.N.succ_pos BinNat.N.two). + Proof. + intros p Hp X; apply (Fchar_ge_3 p Hp). + eapply Monoid.is_homomorphism_phi_proper in X. + rewrite (homomorphism_zero(zero:=Fzero)(phi:=KtoF)) in X. + etransitivity; [|eexact X]; clear X. + (* TODO: Ring.of_Z of isomorphism *) + Admitted. + + Local Notation Fpoint := (@E.point F Feq Fone Fadd Fmul Fa Fd). + Local Notation Kpoint := (@E.point K Keq Kone Kadd Kmul Ka Kd). + Local Notation FzeroP := (E.zero(nonzero_a:=nonzero_a)(d:=Fd)). + Local Notation KzeroP := (E.zero(nonzero_a:=nonzero_Ka)(d:=Kd)). + Local Notation FaddP := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)). + Local Notation KaddP := (E.add(nonzero_a:=nonzero_Ka)(square_a:=square_Ka)(nonsquare_d:=nonsquare_Kd)). + + Obligation Tactic := idtac. + Program Definition point_phi (P:Fpoint) : Kpoint := exist _ ( + let (x, y) := coordinates P in (FtoK x, FtoK y)) _. + Next Obligation. + destruct P as [ [? ?] ?]; cbv. + rewrite <-!Ha, <-!Hd; pull_homomorphism FtoK. + eapply Monoid.is_homomorphism_phi_proper; assumption. + Qed. + + Lemma Proper_point_phi : Proper (eq==>eq) point_phi. + Proof using Type. + intros P Q H. + destruct P as [ [? ?] ?], Q as [ [? ?] ?], H as [Hl Hr]; cbv. + rewrite !Hl, !Hr. split; reflexivity. + Qed. + + Lemma lift_ismorphism : @Monoid.is_homomorphism Fpoint eq FaddP + Kpoint eq KaddP point_phi. + Proof using Type. + repeat match goal with + | |- _ => intro + | |- Monoid.is_homomorphism => split + | _ => progress destruct_head' @E.point + | _ => progress destruct_head' prod + | _ => progress destruct_head' and + | |- context[E.add ?P ?Q] => + unique pose proof (Pre.denominator_nonzero_x _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q)); + unique pose proof (Pre.denominator_nonzero_y _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q)) + | _ => progress cbv [eq add point_phi coordinates] in * + | |- _ /\ _ => split + | _ => rewrite !(homomorphism_div(phi:=FtoK)) by assumption + | _ => rewrite !Ha + | _ => rewrite !Hd + | _ => Ring.push_homomorphism FtoK + | |- _ ?x ?x => reflexivity + | _ => eapply Monoid.is_homomorphism_phi_proper; assumption + end. + Qed. + End Homomorphism. +End E. diff --git a/src/Curves/Edwards/Montgomery.v b/src/Curves/Edwards/Montgomery.v new file mode 100644 index 000000000..d274356c9 --- /dev/null +++ b/src/Curves/Edwards/Montgomery.v @@ -0,0 +1,114 @@ +Require Import Crypto.Curves.Edwards.AffineProofs. +Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.AffineProofs. +Require Import Crypto.Curves.Montgomery.Affine. + +Require Import Crypto.Util.Notations Crypto.Util.Decidable. +Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod. +Require Import Crypto.Algebra.Field. +Import BinNums. + +Module E. + Section EdwardsMontgomery. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28} + {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). + + Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12. + Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed. + Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3. + Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed. + + 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(char_ge_3:=char_ge_3)(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. + + Program Definition _EM (discr_nonzero:id _) : _ /\ _ /\ _ := + @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. (* M->E->M *) + Next Obligation. Proof. Admitted. (* equivalences match *) + 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 discr_nonzero : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 (_EM discr_nonzero)). + Global Instance homomorphism_to_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 (_EM discr_nonzero)). + End EdwardsMontgomery. +End E. diff --git a/src/Curves/Edwards/Pre.v b/src/Curves/Edwards/Pre.v new file mode 100644 index 000000000..244acc9b5 --- /dev/null +++ b/src/Curves/Edwards/Pre.v @@ -0,0 +1,46 @@ +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid Crypto.Util.Relations. +Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.Field. +Require Import Crypto.Util.Notations Crypto.Util.Decidable (*Crypto.Util.Tactics*). +Require Import Coq.PArith.BinPos. + +Section Edwards. + Context {F eq zero one opp add sub mul inv div} + {field:@Algebra.Hierarchy.field F eq zero one opp add sub mul inv div} + {eq_dec:DecidableRel eq}. + + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + Local Infix "-" := sub. Local Infix "/" := div. + Local Notation "x ^ 2" := (x*x). + + Context (a:F) (a_nonzero : a<>0) (a_square : exists sqrt_a, sqrt_a^2 = a). + Context (d:F) (d_nonsquare : forall sqrt_d, sqrt_d^2 <> d). + Context {char_ge_3:@Ring.char_ge F eq zero one opp add sub mul 3}. + + Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). + Lemma onCurve_zero : onCurve 0 1. + Proof using a_nonzero eq_dec field. + fsatz. Qed. + + Section Addition. + Context (x1 y1:F) (P1onCurve: onCurve x1 y1). + Context (x2 y2:F) (P2onCurve: onCurve x2 y2). + Lemma denominator_nonzero : (d*x1*x2*y1*y2)^2 <> 1. + Proof using Type*. + destruct a_square as [sqrt_a], (dec(sqrt_a*x2+y2 = 0)), (dec(sqrt_a*x2-y2 = 0)); + try match goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] + => pose proof (d_nonsquare ((f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) + /(f (sqrt_a * x2) y2 * x1 * y1 ))) + end; Field.fsatz. + Qed. + + Lemma denominator_nonzero_x : 1 + d*x1*x2*y1*y2 <> 0. + Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed. + Lemma denominator_nonzero_y : 1 - d*x1*x2*y1*y2 <> 0. + Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed. + Lemma onCurve_add : onCurve ((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)). + Proof using Type*. pose proof denominator_nonzero. Field.fsatz. Qed. + End Addition. +End Edwards. \ No newline at end of file diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v new file mode 100644 index 000000000..160866b64 --- /dev/null +++ b/src/Curves/Edwards/XYZT.v @@ -0,0 +1,140 @@ +Require Import Coq.Classes.Morphisms. + +Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Curves.Edwards.AffineProofs. + +Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings. +Require Export Crypto.Util.FixCoqMistakes. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.UniquePose. + +Module Extended. + Section ExtendedCoordinates. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.Hierarchy.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 onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing). + (** [Extended.point] represents a point on an elliptic curve using extended projective + * Edwards coordinates 1 (see ). *) + Definition point := { P | let '(X,Y,Z,T) := P in + a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2 + /\ X * Y = Z * T + /\ Z <> 0 }. + Definition coordinates (P:point) : F*F*F*F := proj1_sig P. + Definition eq (P1 P2:point) := + let '(X1, Y1, Z1, _) := coordinates P1 in + let '(X2, Y2, Z2, _) := coordinates P2 in + Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2. + + Ltac t_step := + match goal with + | |- Proper _ _ => intro + | _ => progress intros + | _ => progress destruct_head' prod + | _ => progress destruct_head' @E.point + | _ => progress destruct_head' point + | _ => progress destruct_head' and + | _ => progress cbv [eq CompleteEdwardsCurve.E.eq E.eq E.zero E.add E.opp fst snd coordinates E.coordinates proj1_sig] in * + | |- _ /\ _ => split | |- _ <-> _ => split + end. + Ltac t := repeat t_step; Field.fsatz. + + Global Instance Equivalence_eq : Equivalence eq. + Proof using Feq_dec field nonzero_a. split; repeat intro; t. Qed. + Global Instance DecidableRel_eq : Decidable.DecidableRel eq. + Proof. intros P Q; destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; exact _. Defined. + + Program Definition from_twisted (P:Epoint) : point := + let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy * snd xy). + Next Obligation. t. Qed. + Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. + Proof using Type. cbv [from_twisted]; t. Qed. + + Program Definition to_twisted (P:point) : Epoint := + let XYZT := coordinates P in let T := snd XYZT in + let XYZ := fst XYZT in let Z := snd XYZ in + let XY := fst XYZ in let Y := snd XY in + let X := fst XY in + let iZ := Finv Z in ((X*iZ), (Y*iZ)). + Next Obligation. t. Qed. + Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. + Proof using Type. cbv [to_twisted]; t. Qed. + + Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P. + Proof using Type. cbv [to_twisted from_twisted]; t. Qed. + Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P. + Proof using Type. cbv [to_twisted from_twisted]; t. Qed. + + Program Definition zero : point := (0, 1, 1, 0). + Next Obligation. t. Qed. + + Program Definition opp P : point := + match coordinates P return F*F*F*F with (X,Y,Z,T) => (Fopp X, Y, Z, Fopp T) end. + Next Obligation. t. Qed. + + Section TwistMinusOne. + Context {a_eq_minus1:a = Fopp 1} {twice_d} {k_eq_2d:twice_d = d+d}. + Program Definition m1add + (P1 P2:point) : point := + match coordinates P1, coordinates P2 return F*F*F*F with + (X1, Y1, Z1, T1), (X2, Y2, Z2, T2) => + let A := (Y1-X1)*(Y2-X2) in + let B := (Y1+X1)*(Y2+X2) in + let C := T1*twice_d*T2 in + let D := Z1*(Z2+Z2) in + let E := B-A in + let F := D-C in + let G := D+C in + let H := B+A in + let X3 := E*F in + let Y3 := G*H in + let T3 := E*H in + let Z3 := F*G in + (X3, Y3, Z3, T3) + end. + Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2))); t. Qed. + + Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : Algebra.Hierarchy.group /\ _ /\ _ := + @Group.group_from_redundant_representation + _ _ _ _ _ + ((E.edwards_curve_abelian_group(a:=a)(d:=d)(nonzero_a:=nonzero_a')(square_a:=square_a') + (nonsquare_d:=nonsquare_d')).(Algebra.Hierarchy.abelian_group_group)) + _ + eq + m1add + zero + opp + from_twisted + to_twisted + to_twisted_from_twisted + _ _ _ _. + Next Obligation. cbv [to_twisted]. t. Qed. + Next Obligation. + match goal with + | |- context[E.add ?P ?Q] => + unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig P) _ _ (proj2_sig Q)) + end. cbv [to_twisted m1add]. t. Qed. + Next Obligation. cbv [to_twisted opp]. t. Qed. + Next Obligation. cbv [to_twisted zero]. t. Qed. + Global Instance group x y z + : Algebra.Hierarchy.group := proj1 (_group_proof x y z). + Global Instance homomorphism_from_twisted x y z : + Monoid.is_homomorphism := proj1 (proj2 (_group_proof x y z)). + Global Instance homomorphism_to_twisted x y z : + Monoid.is_homomorphism := proj2 (proj2 (_group_proof x y z)). + End TwistMinusOne. + End ExtendedCoordinates. +End Extended. diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v new file mode 100644 index 000000000..721908a6a --- /dev/null +++ b/src/Curves/Montgomery/Affine.v @@ -0,0 +1,67 @@ +Require Import Crypto.Algebra.Field. +Require Import Crypto.Util.GlobalSettings. +Require Import Crypto.Util.Sum Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve. + +Module M. + Section MontgomeryCurve. + Import BinNat. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.Hierarchy.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 "'∞'" := 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. + + Local Notation add := (M.add(b_nonzero:=b_nonzero)). + Local Notation point := (@M.point F Feq Fadd Fmul a b). + + Section MontgomeryWeierstrass. + Local Notation "2" := (1+1). + Local Notation "3" := (1+2). + 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. destruct P; cbv; break_match; trivial; 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. destruct P; cbv; break_match; trivial; fsatz. Qed. + End MontgomeryWeierstrass. + End MontgomeryCurve. +End M. \ No newline at end of file diff --git a/src/Curves/Montgomery/AffineProofs.v b/src/Curves/Montgomery/AffineProofs.v new file mode 100644 index 000000000..a83109a55 --- /dev/null +++ b/src/Curves/Montgomery/AffineProofs.v @@ -0,0 +1,83 @@ +Require Import Crypto.Algebra.Field. +Require Import Crypto.Util.GlobalSettings. +Require Import Crypto.Util.Sum Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine. +Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine. +Require Import Crypto.Curves.Weierstrass.AffineProofs. + +Module M. + Section MontgomeryCurve. + Import BinNat. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:Decidable.DecidableRel Feq} + {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}. + Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12. + Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed. + Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3. + Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed. + + 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 "9" := (3*3). Local Notation "27" := (3*9). + 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}. + + 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). + Local Notation Wopp := (@W.opp F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec). + + 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 M.opp proj1_sig + W.coordinates W.add W.zero W.eq W.opp + M.of_Weierstrass M.to_Weierstrass] in * + | |- _ /\ _ => split | |- _ <-> _ => split + end. + + Program Definition _MW (discr_nonzero:id _) : _ /\ _ /\ _ := + @Group.group_from_redundant_representation + Wpoint W.eq Wadd W.zero Wopp + (Algebra.Hierarchy.abelian_group_group (W.commutative_group(char_ge_12:=char_ge_12)(discriminant_nonzero:=discr_nonzero))) + (@M.point F Feq Fadd Fmul a b) M.eq (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero)) M.zero (M.opp(b_nonzero:=b_nonzero)) + (M.of_Weierstrass(b_nonzero:=b_nonzero)) + (M.to_Weierstrass(b_nonzero:=b_nonzero)) + _ _ _ _ _ + . + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. + Next Obligation. Proof. t; fsatz. Qed. + + Global Instance group discr_nonzero : Algebra.Hierarchy.group := proj1 (_MW discr_nonzero). + Global Instance homomorphism_of_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.of_Weierstrass) := proj1 (proj2 (_MW discr_nonzero)). + Global Instance homomorphism_to_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.to_Weierstrass) := proj2 (proj2 (_MW discr_nonzero)). + End MontgomeryCurve. +End M. diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v new file mode 100644 index 000000000..60020827c --- /dev/null +++ b/src/Curves/Montgomery/XZ.v @@ -0,0 +1,57 @@ +Require Import Crypto.Algebra.Field. +Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations. +Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine. + +Module M. + Section MontgomeryCurve. + Import BinNat. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:Decidable.DecidableRel Feq} + {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. + + Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)). + Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed. + + (* 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' => + dlet A := x+z in + dlet B := x-z in + dlet AA := A^2 in + dlet BB := B^2 in + dlet x2 := AA*BB in + dlet E := AA-BB in + dlet z2 := E*(AA + a24*E) in + dlet C := x'+z' in + dlet D := x'-z' in + dlet CB := C*B in + dlet DA := D*A in + dlet x3 := (DA+CB)^2 in + dlet z3 := x1*(DA-CB)^2 in + (pair (pair x2 z2) (pair x3 z3)) + end. + End MontgomeryCurve. +End M. diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v new file mode 100644 index 000000000..d24d1398c --- /dev/null +++ b/src/Curves/Montgomery/XZProofs.v @@ -0,0 +1,58 @@ +Require Import Crypto.Algebra.Field. +Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine. +Require Import Crypto.Curves.Montgomery.XZ BinPos. + +Module M. + Section MontgomeryCurve. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:Decidable.DecidableRel Feq} + {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 "0" := Fzero. Local Notation "1" := Fone. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "( x , y )" := (inl (pair x y)). + + Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)). + Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed. + + Context {a b: F} {b_nonzero:b <> 0}. + Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}. + Local Notation add := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)). + Local Notation opp := (M.opp(a:=a)(b_nonzero:=b_nonzero)). + Local Notation point := (@M.point F Feq Fadd Fmul a b). + Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)). + + 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 M.xzladderstep M.to_xz Let_In] 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 using a24_correct char_ge_5. t; abstract fsatz. Qed. + End MontgomeryCurve. +End M. diff --git a/src/Curves/Weierstrass/Affine.v b/src/Curves/Weierstrass/Affine.v new file mode 100644 index 000000000..90bb3bdbc --- /dev/null +++ b/src/Curves/Weierstrass/Affine.v @@ -0,0 +1,18 @@ +Require Import Crypto.Spec.WeierstrassCurve. +Require Import Crypto.Algebra.Field. +Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch. + +Module W. + Section W. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} + {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:DecidableRel Feq}. + + Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b + := match W.coordinates P return F*F+_ with + | inl (x1, y1) => inl (x1, Fopp y1) + | _ => P + end. + Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed. + End W. +End W. \ No newline at end of file diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v new file mode 100644 index 000000000..81583d88f --- /dev/null +++ b/src/Curves/Weierstrass/AffineProofs.v @@ -0,0 +1,196 @@ +Require Import Coq.Numbers.BinNums. +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine. +Require Import Crypto.Algebra.Field Crypto.Algebra.Hierarchy. +Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch. +Require Import Coq.PArith.BinPos. + +Module W. + Section W. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F} + {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Feq_dec:DecidableRel Feq} + {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}. (* FIXME: shouldn't need we need 4, not 12? *) + Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3. + Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed. + 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 Notation "4" := (1+1+1+1). Local Notation "27" := (4*4 + 4+4 +1+1+1). + + Global Instance commutative_group {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} : abelian_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp). + Proof using Type. + Time + repeat match goal with + | _ => solve [ contradiction | trivial | exact _ ] + | _ => intro + | |- Equivalence _ => split + | |- abelian_group => split | |- group => split | |- monoid => split + | |- is_associative => split | |- is_commutative => split + | |- is_left_inverse => split | |- is_right_inverse => split + | |- is_left_identity => split | |- is_right_identity => split + | _ => progress destruct_head' @W.point + | _ => progress destruct_head' sum + | _ => progress destruct_head' prod + | _ => progress destruct_head' unit + | _ => progress destruct_head' and + | _ => progress cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig]in* + | _ => progress break_match + end. + (* Finished transaction in 2.098 secs (2.099u,0.s) (successful) *) + all: try split. + (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *) + + (* The [discriminant_nonzero] hypothesis makes [fsatz] slow but + is necessary in some cases. Thus, we wrap it in [id] by detault + to hide it from [nsatz] but unfold it when normal [fsatz] fails. *) + (* Variable re-ordering is a micro-optimization *) + (* TODO: why does par not work here? *) + Ltac s := abstract ( + match goal with [H:id _ |- _] => move H at bottom end; + move b at bottom; + move a at bottom; + repeat match goal with [H: ?x = Fopp ?y |- _] => is_var x; is_var y; revert H end; intros; + repeat match goal with [H: ?x = ?y |- _] => is_var x; is_var y; revert H end; intros; + repeat split; + solve + [ fsatz + | cbv [id] in *; fsatz] + ). + Time s. (* Finished transaction in 0.099 secs (0.096u,0.003s) (successful) *) + Time s. (* Finished transaction in 0.094 secs (0.093u,0.s) (successful) *) + Time s. (* Finished transaction in 0.48 secs (0.48u,0.s) (successful) *) + Time s. (* Finished transaction in 2.229 secs (2.226u,0.003s) (successful) *) + Time s. (* Finished transaction in 3.164 secs (3.153u,0.01s) (successful) *) + Time s. (* Finished transaction in 2.218 secs (2.199u,0.019s) (successful) *) + Time s. (* Finished transaction in 3.499 secs (3.486u,0.01s) (successful) *) + Time s. (* Finished transaction in 1.164 secs (1.16u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.971 secs (1.953u,0.016s) (successful) *) + Time s. (* Finished transaction in 2.344 secs (2.343u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.287 secs (1.286u,0.s) (successful) *) + Time s. (* Finished transaction in 1.781 secs (1.783u,0.s) (successful) *) + Time s. (* Finished transaction in 0.497 secs (0.496u,0.s) (successful) *) + Time s. (* Finished transaction in 1.859 secs (1.856u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.499 secs (1.499u,0.s) (successful) *) + Time s. (* Finished transaction in 1.6 secs (1.6u,0.s) (successful) *) + Time s. (* Finished transaction in 1.446 secs (1.443u,0.s) (successful) *) + Time s. (* Finished transaction in 1.56 secs (1.563u,0.s) (successful) *) + Time s. (* Finished transaction in 1.62 secs (1.616u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.973 secs (1.966u,0.006s) (successful) *) + Time s. (* Finished transaction in 7.66 secs (7.663u,0.s) (successful) *) + Time s. (* Finished transaction in 7.645 secs (7.643u,0.003s) (successful) *) + Time s. (* Finished transaction in 5.956 secs (5.949u,0.006s) (successful) *) + Time s. (* Finished transaction in 7.835 secs (7.803u,0.s) (successful) *) + Time s. (* Finished transaction in 1.893 secs (1.893u,0.s) (successful) *) + Time s. (* Finished transaction in 10.23 secs (10.229u,0.003s) (successful) *) + Time s. (* Finished transaction in 11.059 secs (11.036u,0.02s) (successful) *) + Time s. (* Finished transaction in 8.965 secs (8.963u,0.s) (successful) *) + Time s. (* Finished transaction in 9.539 secs (9.539u,0.003s) (successful) *) + Time s. (* Finished transaction in 2.019 secs (2.013u,0.003s) (successful) *) + Time s. (* Finished transaction in 2.907 secs (2.9u,0.01s) (successful) *) + Time s. (* Finished transaction in 1.622 secs (1.613u,0.01s) (successful) *) + Time s. (* Finished transaction in 13.205 secs (13.203u,0.003s) (successful) *) + Time s. (* Finished transaction in 14.689 secs (14.686u,0.s) (successful) *) + Time s. (* Finished transaction in 10.672 secs (10.673u,0.s) (successful) *) + Time s. (* Finished transaction in 13.509 secs (13.509u,0.s) (successful) *) + Time s. (* Finished transaction in 1.389 secs (1.386u,0.003s) (successful) *) + Time s. (* Finished transaction in 10.331 secs (10.329u,0.003s) (successful) *) + Time s. (* Finished transaction in 12.182 secs (12.176u,0.006s) (successful) *) + Time s. (* Finished transaction in 9.826 secs (9.829u,0.s) (successful) *) + Time s. (* Finished transaction in 13.709 secs (13.703u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.059 secs (1.06u,0.s) (successful) *) + Time s. (* Finished transaction in 1.894 secs (1.896u,0.s) (successful) *) + Time s. (* Finished transaction in 1.358 secs (1.356u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.537 secs (1.536u,0.s) (successful) *) + Time s. (* Finished transaction in 1.342 secs (1.343u,0.s) (successful) *) + Time s. (* Finished transaction in 1.095 secs (1.096u,0.s) (successful) *) + Time s. (* Finished transaction in 1.157 secs (1.153u,0.003s) (successful) *) + Time s. (* Finished transaction in 1.603 secs (1.603u,0.s) (successful) *) + Time s. (* Finished transaction in 6.196 secs (6.196u,0.s) (successful) *) + Time s. (* Finished transaction in 6.949 secs (6.949u,0.s) (successful) *) + Time s. (* Finished transaction in 4.685 secs (4.68u,0.006s) (successful) *) + Time s. (* Finished transaction in 6.483 secs (6.483u,0.s) (successful) *) + Time s. (* Finished transaction in 1.451 secs (1.453u,0.s) (successful) *) + Time s. (* Finished transaction in 13.648 secs (13.646u,0.s) (successful) *) + Time s. (* Finished transaction in 18.053 secs (18.056u,0.s) (successful) *) + Time s. (* Finished transaction in 7.186 secs (7.186u,0.s) (successful) *) + Time s. (* Finished transaction in 8.817 secs (8.819u,0.s) (successful) *) + Time s. (* Finished transaction in 1.251 secs (1.25u,0.s) (successful) *) + Time s. (* Finished transaction in 1.569 secs (1.569u,0.s) (successful) *) + Time s. (* Finished transaction in 1.356 secs (1.356u,0.s) (successful) *) + Time s. (* Finished transaction in 11.45 secs (11.446u,0.003s) (successful) *) + Time s. (* Finished transaction in 17.968 secs (17.969u,0.003s) (successful) *) + Time s. (* Finished transaction in 12.418 secs (12.366u,0.046s) (successful) *) + Time s. (* Finished transaction in 15.323 secs (15.316u,0.01s) (successful) *) + Time s. (* Finished transaction in 1.589 secs (1.586u,0.003s) (successful) *) + Time s. (* Finished transaction in 10.22 secs (10.223u,0.s) (successful) *) + Time s. (* Finished transaction in 11.887 secs (11.889u,0.s) (successful) *) + Time s. (* Finished transaction in 7.284 secs (7.283u,0.003s) (successful) *) + Time s. (* Finished transaction in 8.75 secs (8.753u,0.s) (successful) *) + Time s. (* Finished transaction in 0.291 secs (0.29u,0.s) (successful) *) + Time s. (* Finished transaction in 0.348 secs (0.346u,0.s) (successful) *) + Time s. (* Finished transaction in 0.222 secs (0.223u,0.s) (successful) *) + Time s. (* Finished transaction in 0.266 secs (0.266u,0.s) (successful) *) + Time s. (* Finished transaction in 0.296 secs (0.296u,0.s) (successful) *) + Time s. (* Finished transaction in 0.737 secs (0.736u,0.s) (successful) *) + Time s. (* Finished transaction in 0.227 secs (0.226u,0.s) (successful) *) + Time s. (* Finished transaction in 0.269 secs (0.269u,0.s) (successful) *) + Time s. (* Finished transaction in 0.054 secs (0.056u,0.s) (successful) *) + Time s. (* Finished transaction in 0.057 secs (0.056u,0.s) (successful) *) + Time s. (* Finished transaction in 0.308 secs (0.309u,0.s) (successful) *) + Time s. (* Finished transaction in 0.362 secs (0.363u,0.s) (successful) *) + Time s. (* Finished transaction in 0.226 secs (0.226u,0.s) (successful) *) + Time s. (* Finished transaction in 0.279 secs (0.279u,0.s) (successful) *) + Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.057 secs (0.06u,0.s) (successful) *) + Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.052 secs (0.049u,0.s) (successful) *) + Time s. (* Finished transaction in 0.053 secs (0.056u,0.s) (successful) *) + Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.2 secs (0.203u,0.s) (successful) *) + Time s. (* Finished transaction in 0.21 secs (0.21u,0.s) (successful) *) + Time s. (* Finished transaction in 0.208 secs (0.206u,0.s) (successful) *) + Time s. (* Finished transaction in 1.162 secs (1.163u,0.s) (successful) *) + Time s. (* Finished transaction in 1.256 secs (1.256u,0.s) (successful) *) + Time s. (* Finished transaction in 0.994 secs (0.996u,0.s) (successful) *) + Time s. (* Finished transaction in 1.017 secs (1.016u,0.s) (successful) *) + Time s. (* Finished transaction in 0.186 secs (0.186u,0.s) (successful) *) + Time s. (* Finished transaction in 1.044 secs (1.043u,0.s) (successful) *) + Time s. (* Finished transaction in 1.123 secs (1.123u,0.s) (successful) *) + Time s. (* Finished transaction in 0.892 secs (0.889u,0.s) (successful) *) + Time s. (* Finished transaction in 0.961 secs (0.963u,0.s) (successful) *) + Time s. (* Finished transaction in 0.051 secs (0.05u,0.s) (successful) *) + Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *) + Time s. (* Finished transaction in 0.085 secs (0.086u,0.s) (successful) *) + Time s. (* Finished transaction in 0.081 secs (0.08u,0.s) (successful) *) + Time s. (* Finished transaction in 0.12 secs (0.119u,0.s) (successful) *) + Time s. (* Finished transaction in 0.116 secs (0.12u,0.s) (successful) *) + Time s. (* Finished transaction in 0.074 secs (0.073u,0.s) (successful) *) + Time s. (* Finished transaction in 0.067 secs (0.066u,0.s) (successful) *) + Time s. (* Finished transaction in 0.07 secs (0.073u,0.s) (successful) *) + Time s. (* Finished transaction in 0.063 secs (0.063u,0.s) (successful) *) + Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *) + Time s. (* Finished transaction in 0.084 secs (0.083u,0.s) (successful) *) + Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *) + Time s. (* Finished transaction in 0.097 secs (0.096u,0.s) (successful) *) + Time s. (* Finished transaction in 0.108 secs (0.106u,0.s) (successful) *) + Time s. (* Finished transaction in 0.658 secs (0.66u,0.s) (successful) *) + Time s. (* Finished transaction in 0.775 secs (0.773u,0.s) (successful) *) + Time s. (* Finished transaction in 0.527 secs (0.526u,0.s) (successful) *) + Time s. (* Finished transaction in 0.625 secs (0.623u,0.003s) (successful) *) + Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *) + Time s. (* Finished transaction in 0.586 secs (0.586u,0.s) (successful) *) + Time s. (* Finished transaction in 0.687 secs (0.686u,0.s) (successful) *) + Time s. (* Finished transaction in 0.189 secs (0.189u,0.s) (successful) *) + Time s. (* Finished transaction in 0.21 secs (0.209u,0.s) (successful) *) + Time s. (* Finished transaction in 0.066 secs (0.066u,0.s) (successful) *) + Time s. (* Finished transaction in 0.078 secs (0.08u,0.s) (successful) *) + Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *) + Time s. (* Finished transaction in 0.068 secs (0.066u,0.s) (successful) *) + (* Total: 414.396 seconds, roughly 7 minutes*) + + Time Qed. (* Finished transaction in 390.998 secs (390.783u,0.276s) (successful) *) + End W. +End W. diff --git a/src/Curves/Weierstrass/Pre.v b/src/Curves/Weierstrass/Pre.v new file mode 100644 index 000000000..6647d8e76 --- /dev/null +++ b/src/Curves/Weierstrass/Pre.v @@ -0,0 +1,62 @@ +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Require Import Crypto.Algebra.Field. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Decidable. +Import BinNums. + +Local Open Scope core_scope. + +Section Pre. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {field:@Algebra.Hierarchy.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))} + {eq_dec: DecidableRel Feq}. + Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)). + 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" := (Fopp x). + Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2). + Local Notation "'∞'" := unit : type_scope. + Local Notation "'∞'" := (inr tt) : core_scope. + Local Notation "2" := (1+1). Local Notation "3" := (1+2). + Local Notation "( x , y )" := (inl (pair x y)). + + Context {a:F}. + Context {b:F}. + + (* the canonical definitions are in Spec *) + Let onCurve (P:F*F + ∞) := match P with + | (x, y) => y^2 = x^3 + a*x + b + | ∞ => True + end. + Let add (P1' P2':F*F + ∞) : F*F + ∞ := + match P1', P2' return _ with + | (x1, y1), (x2, y2) => + if dec (x1 = x2) + then + if dec (y2 = -y1) + then ∞ + else let k := (3*x1^2+a)/(2*y1) in + let x3 := k^2-x1-x1 in + let y3 := k*(x1-x3)-y1 in + (x3, y3) + else let k := (y2-y1)/(x2-x1) in + let x3 := k^2-x1-x2 in + let y3 := k*(x1-x3)-y1 in + (x3, y3) + | ∞, ∞ => ∞ + | ∞, _ => P2' + | _, ∞ => P1' + end. + + Lemma add_onCurve P1 P2 (_:onCurve P1) (_:onCurve P2) : + onCurve (add P1 P2). + Proof using a b char_ge_3 eq_dec field. + destruct_head' sum; destruct_head' prod; + cbv [onCurve add] in *; break_match; trivial; [|]; fsatz. + Qed. +End Pre. diff --git a/src/Curves/Weierstrass/Projective.v b/src/Curves/Weierstrass/Projective.v new file mode 100644 index 000000000..20866ca5d --- /dev/null +++ b/src/Curves/Weierstrass/Projective.v @@ -0,0 +1,157 @@ +Require Import Crypto.Spec.WeierstrassCurve. +Require Import Crypto.Util.Decidable Crypto.Algebra.Field. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.SetoidSubst. +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.Hierarchy.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 using Type. + 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. -- cgit v1.2.3