diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Curves/Weierstrass | |
parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) |
rename-everything
Diffstat (limited to 'src/Curves/Weierstrass')
-rw-r--r-- | src/Curves/Weierstrass/Affine.v | 18 | ||||
-rw-r--r-- | src/Curves/Weierstrass/AffineProofs.v | 196 | ||||
-rw-r--r-- | src/Curves/Weierstrass/Pre.v | 62 | ||||
-rw-r--r-- | src/Curves/Weierstrass/Projective.v | 157 |
4 files changed, 433 insertions, 0 deletions
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 + <http://www.mat.uniroma3.it/users/pappa/CORSI/CR510_13_14/BosmaLenstra.pdf> + "Commplete Systems of Addition Laws" by Bosma and Lenstra; + optimized in <https://eprint.iacr.org/2015/1060.pdf> "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. |