From 1da660b30f87a161f866deb44717d0ba5c78cd9d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 27 Jun 2016 13:23:11 -0400 Subject: scalarmult support; EdDSA.sign produces valid signatures --- .../CompleteEdwardsCurveTheorems.v | 23 ++++++---------------- 1 file changed, 6 insertions(+), 17 deletions(-) (limited to 'src/CompleteEdwardsCurve') diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index e3809bb8a..0afc07c5d 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -138,25 +138,14 @@ Module E. match goal with | |- _ <> 0 => admit end. Admitted. - (* TODO: move to [Group] and [AbelianGroup] as appropriate *) - Lemma mul_0_l : forall P, (0 * P = zero)%E. - Proof. intros; reflexivity. Qed. - Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E. - Proof. intros; reflexivity. Qed. - Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E. + Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul. Proof. - induction n; intros; - rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. + intros n m Hnm P Q HPQ. rewrite <-Hnm; clear Hnm m. + induction n; simpl; rewrite ?IHn, ?HPQ; reflexivity. Qed. - Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E. - Proof. - induction n; intros; [reflexivity|]. - rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity. - Qed. - Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E. - Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed. - Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E. - Admitted. + + Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul. + Proof. split; intros; reflexivity || typeclasses eauto. Qed. Section PointCompression. Local Notation "x ^ 2" := (x*x). -- cgit v1.2.3