diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-16 21:22:17 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-16 21:22:17 -0500 |
| commit | b7aa0385bfbedccd486154900571e7244eca51a1 (patch) | |
| tree | 508dc7906369ad65aed1bda697098b94df6f8abb /src/Spec/Ed25519.v | |
| parent | 45a6a17c06f45e81cadf18ef984ec7cdd94c11c1 (diff) | |
moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from CompleteEdwardsCurve, where the precondition is not in scope.
Diffstat (limited to 'src/Spec/Ed25519.v')
| -rw-r--r-- | src/Spec/Ed25519.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 04e6a5fc2..c12799751 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -115,7 +115,10 @@ Qed. Definition FlEncoding : encoding of F (Z.of_nat l) as word b := @modular_word_encoding (Z.of_nat l) b l_pos l_bound. -Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding. +Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed. +(* Admitting until field exponentiation can compute this in reasonable time *) +Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (CompleteEdwardsCurve.q / 4)) ^ 2 = opp 1)%F. Admitted. +Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) |