diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-30 23:11:55 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-30 23:11:55 -0400 |
| commit | 3b0113a9c52855d5362eeaebabe2556efcafcb87 (patch) | |
| tree | 9734fd5ed429fc2e0e670541e2e38d867fbc3afa /src/Arithmetic/MontgomeryReduction | |
| parent | 518f79958112a93eae30942e62096173c4fb0b28 (diff) | |
Prove saturated carrying-addition-chain correct
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 83791ec5f..39382498a 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -226,7 +226,7 @@ Section WordByWordMontgomery. Local Notation eval_sub_then_maybe_add := (fun p q smp smq => @eval_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N smp smq small_N N_mask). Local Notation small_sub_then_maybe_add := - (fun p q => @small_sub_then_maybe_add (Z.pos r) (*(Zorder.Zgt_pos_0 _)*) _ (Z.pos r - 1) p q N). + (fun p q => @small_sub_then_maybe_add (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) p q N). Definition add_no_cps_bound : 0 <= eval add_no_cps < eval N := @add_bound T (@eval) r R R_numlimbs (@small) (@addT) (@eval_addT) (@small_addT) N N_lt_R (@conditional_sub) (@eval_conditional_sub) Av Bv small_Av small_Bv Av_bound Bv_bound. |