diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-17 19:10:54 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-17 19:10:54 -0500 |
| commit | a46dbbec5fc2cd3ffc5c6d4be751e42aa2b7cafb (patch) | |
| tree | 24576fec124d612be19cdca16dcc799250e2a7fa /src/Spec | |
| parent | 56fa6655b07e8992677805e4f89e131c221755a6 (diff) | |
efficient powmod
Diffstat (limited to 'src/Spec')
| -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. |