From bc46f85d089099aa92d3ea12555e6510cbcffa78 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 12 Feb 2017 19:16:26 -0500 Subject: change weierstrass spec, prove most cases of associativity --- src/Spec/WeierstrassCurve.v | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v index 8b5480620..3f8ab2100 100644 --- a/src/Spec/WeierstrassCurve.v +++ b/src/Spec/WeierstrassCurve.v @@ -48,18 +48,24 @@ Module W. _ (match coordinates P1, coordinates P2 return _ with | (x1, y1), (x2, y2) => - if x1 =? x2 then - if y2 =? -y1 then ∞ - else ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1, - (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1) - else ((y2-y1)^2 / (x2-x1)^2 - x1 - x2, - (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1) + 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. exact (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed. + Next Obligation. Admitted. Fixpoint mul (n:nat) (P : point) : point := match n with -- cgit v1.2.3