diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-20 23:04:06 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-06-21 03:13:05 -0400 |
| commit | edef48b5c4b080d4273f0b228d58b7f29630d1f9 (patch) | |
| tree | bd1520b69c6f744ca20e5e85937d2fe304072f3e /src/Arithmetic/MontgomeryReduction | |
| parent | e4a6944a8bfb7da31b9bff4871f8e06bd1a66c4c (diff) | |
Prove some admitted lemmas about uweight
Not sure if locally adding hypotheses is the best way to do it.
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 9787f9c34..4cedadfd0 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -70,7 +70,7 @@ Section WordByWordMontgomery. Local Notation conditional_sub_cps := (fun V : T (S R_numlimbs) => @conditional_sub_cps (Z.pos r) _ (Z.pos r - 1) V N _). Local Notation conditional_sub := (fun V : T (S R_numlimbs) => @conditional_sub (Z.pos r) _ (Z.pos r - 1) V N). - Local Notation eval_conditional_sub' := (fun V small_V V_bound => @eval_conditional_sub (Z.pos r) (Zorder.Zgt_pos_0 _) _ (Z.pos r - 1) V N small_V small_N N_mask V_bound). + Local Notation eval_conditional_sub' := (fun V small_V V_bound => @eval_conditional_sub (Z.pos r) (Zorder.Zgt_pos_0 _) r_big _ (Z.pos r - 1) V N small_V small_N N_mask V_bound). Local Lemma eval_conditional_sub : forall v, small v -> 0 <= eval v < eval N + R -> eval (conditional_sub v) = eval v + if R <=? eval v then -eval N else 0. Proof. rewrite R_correct; exact eval_conditional_sub'. Qed. |