diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-12 08:36:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-12 08:46:16 -0400 |
| commit | c0317ed480096dd9148b2fb9b7223fca086f054b (patch) | |
| tree | fb644f32014c15d71faab02a48014d73174fec53 /src/Arithmetic/MontgomeryReduction | |
| parent | 079f1813cad0e1d8c62f30895d6d3b3bd5642bd3 (diff) | |
Remove eval_small_bounded_numlimbs
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index aaa043958..be0bcb71f 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -50,7 +50,6 @@ Section WordByWordMontgomery. (N : T) (Npos : positive) (Npos_correct: eval N = Z.pos Npos) (N_lt_R : eval N < R) (small_N : small N) - (eval_small_bounded_numlimbs : forall v, small v -> eval v < r ^ Z.of_nat (numlimbs v)) (B : T) (B_bounds : 0 <= eval B < R) (small_B : small B) @@ -501,14 +500,13 @@ Section WordByWordMontgomery. : numlimbs (redc A) = S (numlimbs B). Proof. rewrite numlimbs_redc_gen; subst; auto; destruct (numlimbs A); reflexivity. Qed. - Lemma redc_mod_N A (small_A : small A) (A_nonneg : 0 <= eval A) + Lemma redc_mod_N A (small_A : small A) (A_bound : 0 <= eval A < r ^ Z.of_nat (numlimbs A)) : (eval (redc A)) mod (eval N) = (eval A * eval B * ri^(Z.of_nat (numlimbs A))) mod (eval N). Proof. unfold redc. rewrite snd_redc_loop_mod_N; cbn [fst snd]; autorewrite with push_eval zsimplify; [ | rewrite ?Npos_correct; auto; lia.. ]. - pose proof (eval_small_bounded_numlimbs A small_A). Z.rewrite_mod_small. reflexivity. Qed. |