From 9fed6f528e57fb25972bd991dae726a9b5f8b106 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 24 Jun 2016 23:05:35 -0400 Subject: Ported PointEncodings to parameterize over field rather than modulus. --- src/CompleteEdwardsCurve/Pre.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/CompleteEdwardsCurve') diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index f10e587d6..4ef01c37b 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -63,6 +63,14 @@ Section Pre. assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0) end. + Lemma onCurve_subst : forall x1 x2 y1 y2, and (eq x1 y1) (eq x2 y2) -> onCurve (x1, x2) -> + onCurve (y1, y2). + Proof. + intros ? ? ? ? [eq_1 eq_2] ?. + rewrite eq_1, eq_2 in *. + assumption. + Qed. + Lemma edwardsAddComplete' x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> -- cgit v1.2.3