blob: 6647d8e76e8569f86bbf9f47a66cc14f58d3a5f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
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.
|
