From f4d27f9218990b904da65ec4e87ed5d84358ce65 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Aug 2018 15:32:57 -0400 Subject: Fix another proof broken by wrong behavior of cbn --- src/Experiments/NewPipeline/Toplevel2.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') 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 -> -- cgit v1.2.3