From c39f4255d14955e9ba6ca870a7bc4c15566dad01 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 18 May 2016 12:39:51 -0400 Subject: slightly nicer edwards curve extended coordinates addition --- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index e9c0313ab..e91bc084b 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -116,6 +116,8 @@ Section ExtendedCoordinates. repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. Qed. + Definition twice_d := d + d. + Section TwistMinus1. Context (a_eq_minus1 : a = opp 1). (** Second equation from section 3.1, also and *) @@ -124,8 +126,8 @@ Section ExtendedCoordinates. let '(X2, Y2, Z2, T2) := P2 in let A := (Y1-X1)*(Y2-X2) in let B := (Y1+X1)*(Y2+X2) in - let C := T1*ZToField 2*d*T2 in - let D := Z1*ZToField 2 *Z2 in + let C := T1*twice_d*T2 in + let D := Z1*(Z2+Z2) in let E := B-A in let F := D-C in let G := D+C in @@ -139,13 +141,17 @@ Section ExtendedCoordinates. Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q). + Lemma F_mul_2_l : forall x : F q, ZToField 2 * x = x + x. + intros. ring. + Qed. + Lemma unifiedAddM1'_rep: forall P Q rP rQ, E.onCurve rP -> E.onCurve rQ -> P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (E.add' rP rQ). Proof. intros P Q rP rQ HoP HoQ HrP HrQ. pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). - unfoldExtended; rewrite a_eq_minus1 in *; simpl in *. + unfoldExtended; unfold twice_d; rewrite a_eq_minus1 in *; simpl in *. repeat rewrite <-F_mul_2_l. repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r, ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; -- cgit v1.2.3