diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-24 23:05:35 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-24 23:05:35 -0400 |
| commit | 9fed6f528e57fb25972bd991dae726a9b5f8b106 (patch) | |
| tree | 6bad5d2ba83369943b138653764aad8804c96041 /src/CompleteEdwardsCurve | |
| parent | b74857e6cc90fffe2a07e6bcf414ac4774a145cb (diff) | |
Ported PointEncodings to parameterize over field rather than modulus.
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 8 |
1 files changed, 8 insertions, 0 deletions
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) -> |