diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-22 15:27:42 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-04-22 15:27:42 -0400 |
| commit | 2b43845eabdb5522162d52a86ecf6dfaf6dbc847 (patch) | |
| tree | 00c193d89adbd22bac516072164b76f363241d9e /src/Specific | |
| parent | 30ef733d1a5820456d5e5aac774270b51a9c9dde (diff) | |
point_eq_dec
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Ed25519.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 50379b8d1..2bafd4c8a 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -7,6 +7,7 @@ Require Import ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. +Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Util.IterAssocOp. Local Infix "++" := Word.combine. @@ -57,9 +58,6 @@ Proof. end. } Qed. -Axiom point_eqb : forall {prm : TwistedEdwardsParams}, point -> point -> bool. -Axiom point_eqb_correct : forall P Q, point_eqb P Q = if point_eq_dec P Q then true else false. - Axiom xB : F q. Axiom yB : F q. Axiom B_proj : proj1_sig B = (xB, yB). @@ -517,4 +515,4 @@ Proof. point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. *) reflexivity. -Admitted.
\ No newline at end of file +Admitted. |