diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-15 18:00:35 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-15 18:00:35 -0400 |
| commit | 4a2c65e57a107545654c2ae815efd734ca7d8321 (patch) | |
| tree | 2ff73f22315e8b15f22a263ce068a0b805c690cc /src/Specific | |
| parent | b3ddc5cfb84c952785196a9e27e497dc14af9188 (diff) | |
PseudoMersenneBaseRep.mul now carries by default (made possible by strictly base-length digit vectors)
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF1305.v | 2 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index b004a60d1..31dee21f3 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -45,7 +45,7 @@ Lemma GF1305Base26_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_correct k_ c_ (eq_refl k) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. compute_formula. Defined. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 68278ce4c..37e0c08db 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -47,7 +47,7 @@ Lemma GF25519Base25Point5_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_correct k_ c_ (eq_refl k_) (eq_refl c_) [0;9;8;7;6;5;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. compute_formula. Time Defined. |