diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-07 01:06:15 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-07 01:06:15 -0500 |
| commit | 66fb5594c8b299c5179450f36d3869cb80c84c29 (patch) | |
| tree | 9b6d833185046e3d90a240b33a763dc07635fb17 /src/Curves | |
| parent | 9e5cc1ab4b30b6d0de790437ba113d2701aa69af (diff) | |
PointFormats: prove dangling admit
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/PointFormats.v | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index 85f69b87a..218d60299 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -264,9 +264,6 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam onCurve (x2, y2) -> (d*x1*x2*y1*y2)^2 <> 1. Proof. - (* TODO: this proof was made inconsistent by an actually - correct version of root_nonzero. This adds the necessary - hypothesis*) unfold onCurve; intuition; whatsNotZero. pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. @@ -339,7 +336,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam Defined. Local Hint Unfold onCurve mkPoint. - Definition zero : point. exists (0, 1). + Definition zero : point. refine (mkPoint (0, 1) _). abstract (unfold onCurve; field). Defined. @@ -399,6 +396,7 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam let 'exist P2' pf2 := P2 in mkPoint (unifiedAdd' P1' P2') (unifiedAdd'_onCurve' _ _ pf1 pf2). Local Infix "+" := unifiedAdd. + SearchAbout Pos.iter_op. Fixpoint scalarMult (n:nat) (P : point) : point := match n with @@ -472,8 +470,12 @@ Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParam Qed. Lemma zeroIsIdentity : forall P, P + zero = P. - (* Should follow from zeroIsIdentity', but dependent types... *) - Admitted. + Proof. + unfold zero, unifiedAdd. + destruct P as [[x y] pf]. + simpl. + apply point_eq; field; auto. + Qed. Hint Resolve zeroIsIdentity. Lemma scalarMult_double : forall n P, scalarMult (n + n) P = scalarMult n (P + P). @@ -719,7 +721,7 @@ Module ExtendedM1 (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEd pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H; match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end ) || ( - pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as Hm; + pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H; match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end ); repeat apply mul_nonzero_nonzero; auto 10 end. |