diff options
Diffstat (limited to 'src/Spec')
| -rw-r--r-- | src/Spec/MontgomeryCurve.v | 25 | ||||
| -rw-r--r-- | src/Spec/WeierstrassCurve.v | 46 |
2 files changed, 32 insertions, 39 deletions
diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v index ff6d3a080..55c73c7fd 100644 --- a/src/Spec/MontgomeryCurve.v +++ b/src/Spec/MontgomeryCurve.v @@ -28,7 +28,7 @@ Module M. | (x, y) => b*y^2 = x^3 + a*x^2 + x | ∞ => True end }. - Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + Definition coordinates (P:point) : (F*F + ∞) := let (xyi, _) := P in xyi. Program Definition zero : point := ∞. @@ -46,29 +46,20 @@ Module M. then if Decidable.dec (y1 = - y2) then ∞ 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) + let x := b*k^2 - a - x1 - x2 in + let y := (2*x1 + x2 + a)*k - b*k^3 - y1 in + (x, y) else let k := (y2 - y1)/(x2-x1) in - (b*k^2 - a - x1 - x2, (2*x1 + x2 + a)*k - b*k^3 - y1) + let x := b*k^2 - a - x1 - x2 in + let y := (2*x1 + x2 + a)*k - b*k^3 - y1 in + (x, y) | ∞, ∞ => ∞ | ∞, _ => coordinates P2 | _, ∞ => coordinates P1 end. Next Obligation. 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. + cbv [coordinates]; BreakMatch.break_match; trivial; Field.fsatz. Qed. End MontgomeryCurve. End M. diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 226ec6616..fc7c64198 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -1,4 +1,4 @@ -Require Crypto.Curves.Weierstrass.Pre. +Require Crypto.Algebra.Field. Module W. Section WeierstrassCurves. @@ -29,7 +29,7 @@ Module W. | (x, y) => y^2 = x^3 + a*x + b | ∞ => True end }. - Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P. + Definition coordinates (P:point) : F*F + ∞ := let (xyi,_) := P in xyi. Definition eq (P1 P2:point) := match coordinates P1, coordinates P2 with @@ -43,26 +43,28 @@ Module W. Local Notation "0" := Fzero. Local Notation "1" := Fone. Local Notation "2" := (1+1). Local Notation "3" := (1+2). - Program Definition add (P1 P2:point) : point := exist _ - (match coordinates P1, coordinates P2 return _ with - | (x1, y1), (x2, y2) => - if x1 =? x2 - then - if y2 =? -y1 - then ∞ - else 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) - | ∞, ∞ => ∞ - | ∞, _ => coordinates P2 - | _, ∞ => coordinates P1 - end) _. - Next Obligation. apply (Pre.add_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed. + Program Definition add (P1 P2:point) : point := + match coordinates P1, coordinates P2 return F*F+∞ with + | (x1, y1), (x2, y2) => + if x1 =? x2 + then + if y2 =? -y1 + then ∞ + else let k := (3*x1^2+a)/(2*y1) in + let x3 := k^2-x1-x2 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) + | ∞, ∞ => ∞ + | ∞, _ => coordinates P2 + | _, ∞ => coordinates P1 + end. + Next Obligation. + cbv [coordinates]; BreakMatch.break_match; trivial; Field.fsatz. + Qed. Fixpoint mul (n:nat) (P : point) : point := match n with |