diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-08-14 15:32:57 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-08-14 15:32:57 -0400 |
| commit | f4d27f9218990b904da65ec4e87ed5d84358ce65 (patch) | |
| tree | fcdc2187d38fa1afa3ced2403c5ac9a615376236 /src | |
| parent | 32c34659f93cb89b955b91f23b4fc3019dc25589 (diff) | |
Fix another proof broken by wrong behavior of cbn
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 6cd771e57..e35e14616 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -2924,7 +2924,8 @@ Module Montgomery256. xy = true -> expr.Interp (@ident.interp) montred256 xy = MontgomeryReduction.montred' N R N' (Z.log2 R) 2 2 xy. Proof. intros; rewrite montred256_correct_proj2 by assumption; unfold app_curried; exact eq_refl. Qed. -*) + *) + Local Arguments is_bounded_by_bool / . Lemma montred256_correct_full R' (R'_correct : Z.equiv_modulo N (R * R') 1) : forall (lo hi : Z), 0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N -> |