diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-17 19:10:54 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:40:31 -0400 |
| commit | 7ca35a366c38a5977bf1b02b14a3f2ffcf1869c2 (patch) | |
| tree | d371007363d45201910f016d1d1e83c1f614e365 /src/Spec/Ed25519.v | |
| parent | e907b22802825e9ff102e284b8f4b9ddd119fdca (diff) | |
efficient powmod
Diffstat (limited to 'src/Spec/Ed25519.v')
| -rw-r--r-- | src/Spec/Ed25519.v | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index c12799751..adc40dae6 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -116,8 +116,22 @@ Definition FlEncoding : encoding of F (Z.of_nat l) as word b := @modular_word_encoding (Z.of_nat l) b l_pos l_bound. 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. + +Hint Rewrite + @FieldToZ_pow_efficient + @FieldToZ_ZToField + @FieldToZ_opp + @FieldToZ_ZToField : ZToField + . + +Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F. +Proof. + apply F_eq. + autorewrite with ZToField. + vm_compute. + reflexivity. +Qed. + Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. Definition H : forall n : nat, word n -> word (b + b). Admitted. |