diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-25 23:04:13 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-04-25 23:04:13 -0400 |
| commit | f1ef056a7a153931c7f05c126742d941d0908d25 (patch) | |
| tree | f1a64257c9bf69b0108833d6c40da466757724f0 /src/Spec/Ed25519.v | |
| parent | 7de4975fd738a82f38028307afb48275b01491b2 (diff) | |
consolidate and rename Edwards curve lemmas
Diffstat (limited to 'src/Spec/Ed25519.v')
| -rw-r--r-- | src/Spec/Ed25519.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 30892c006..6543823cb 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -145,9 +145,9 @@ Qed. Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding. Definition H : forall n : nat, word n -> word (b + b). Admitted. -Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) -Definition B_nonzero : B <> zero. Admitted. -Definition l_order_B : scalarMult l B = zero. Admitted. +Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) +Definition B_nonzero : B <> E.zero. Admitted. +Definition l_order_B : (l * B)%E = E.zero. Admitted. Local Instance ed25519params : EdDSAParams := { E := curve25519params; |