diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-10 12:25:12 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-10 12:25:12 -0400 |
commit | 0226dcda7092cdfe72551adb49eccd7f97b34708 (patch) | |
tree | 3b157e854885a915777fadf351d8a92b39353eef /src/Arithmetic/MontgomeryReduction/WordByWord | |
parent | 54c89602d50fc4adc60931e34b8afe304b40da38 (diff) |
Add constraint on scmul scalar
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction/WordByWord')
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 96a0d031e..da51fa0c9 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -29,7 +29,7 @@ Section WordByWordMontgomery. {small_div : forall v, small v -> small (fst (divmod v))} {scmul : Z -> T -> T} (* uses double-output multiply *) {eval_scmul: forall a v, eval (scmul a v) = a * eval v} - {small_scmul : forall a v, small v -> small (scmul a v)} + {small_scmul : forall a v, 0 <= a < r -> small v -> small (scmul a v)} {R : positive} {R_big : R > 3} (* needed for [(N + B - 1) / R <= 1] *). Local Notation bn := (r * R) (only parsing). @@ -47,13 +47,22 @@ Section WordByWordMontgomery. Context (k : Z) (k_correct : k * eval N mod r = -1). Create HintDb push_eval discriminated. + Local Ltac t_small := + repeat first [ assumption + | apply small_add + | apply small_div + | apply small_scmul + | apply Z_mod_lt + | solve [ auto ] + | lia + | progress autorewrite with push_eval ]. Hint Rewrite eval_zero eval_div eval_mod eval_add eval_scmul - using (repeat autounfold with word_by_word_montgomery; auto) + using (repeat autounfold with word_by_word_montgomery; t_small) : push_eval. (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *) @@ -76,7 +85,7 @@ Section WordByWordMontgomery. Lemma S3_nonneg : 0 <= eval S3. Proof. repeat autounfold with word_by_word_montgomery; - autorewrite with push_eval; []. + autorewrite with push_eval; []. rewrite ?Npos_correct; Z.zero_bounds; lia. Qed. @@ -170,7 +179,7 @@ Section WordByWordMontgomery. Lemma small_S3 : small S3. Proof. - repeat autounfold with word_by_word_montgomery; auto. + repeat autounfold with word_by_word_montgomery; t_small. Qed. Lemma small_from_bound |