diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-28 13:13:08 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-28 13:13:08 -0400 |
| commit | cd07805915328fd5ee8d41b6cdd4d0340aa156aa (patch) | |
| tree | 04a869de660aaa874fca7be13f9fefb86c12cafb /src/Spec/Ed25519.v | |
| parent | 248282849e9b287fe817e64ccf53e09fa3991cbe (diff) | |
Cleanup: mostly moving lemmas to Util files, some moving lemmas to more general contexts.
Diffstat (limited to 'src/Spec/Ed25519.v')
| -rw-r--r-- | src/Spec/Ed25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 505797987..9ae03dcd5 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -146,8 +146,8 @@ Qed. Lemma b_minus1_nonzero : 0 < b - 1. Proof. cbv. omega. Qed. Definition PointEncoding : encoding of E.point as (word b) := - (@point_encoding _ _ b_minus1_nonzero b_valid q_5mod8 sqrt_minus1_valid FqEncoding - (@sign_bit _ prime_q two_lt_q _ b_valid) sign_bit_zero sign_bit_opp). + (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding + (@sign_bit _ prime_q two_lt_q (b - 1) b_valid) sign_bit_zero sign_bit_opp). Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) |