diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-13 00:00:28 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-13 00:00:28 -0500 |
| commit | ed38cae1be2b255a85cf2416ab75de21bfe05df2 (patch) | |
| tree | cd02d3dadd6c89341f43c3695051c4c255a85fa6 /src/CompleteEdwardsCurve | |
| parent | c85f7283994da084a837b88d612a6b937ff2fbd5 (diff) | |
EdDSA spec ported over to new field implementation
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index b1be7dd63..bff6d1948 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -39,7 +39,7 @@ Section CompleteEdwardsCurveTheorems. Edefn; apply f_equal2; ring. Qed. - Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C. + Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E. Proof. (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *) Admitted. @@ -49,4 +49,4 @@ Section CompleteEdwardsCurveTheorems. Edefn; 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; exact eq_refl. Qed. -End CompleteEdwardsCurveTheorems.
\ No newline at end of file +End CompleteEdwardsCurveTheorems. |