From 684d356bcb81ca36314cd7864c62a1d97af4ea99 Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 12:46:00 -0400 Subject: finish proofs --- src/PushButtonSynthesis/BarrettReduction.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/PushButtonSynthesis') diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index c0078b117..504a26a0c 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -177,6 +177,7 @@ Section rbarrett_red. | progress cbv [weight] | rewrite mut_correct | rewrite Mt_correct + | rewrite UniformWeight.uweight_eq_alt' | rewrite Z.pow_mul_r by lia ]. Local Strategy -100 [barrett_red]. (* needed for making Qed not take forever *) @@ -185,6 +186,7 @@ Section rbarrett_red. Proof using M curve_good. cbv [barrett_red_correct]; intros. assert (1 < machine_wordsize) by apply use_curve_good. + pose proof (Z.mod_pos_bound mu (2^machine_wordsize) ltac:(lia)). rewrite <-Fancy.fancy_reduce_correct with (mu := muLow + 2^machine_wordsize) (width:=machine_wordsize) (sz:=1%nat) (mut:=[muLow;1]) (Mt:=[M]) by solve_barrett_red_preconditions. prove_correctness' ltac:(fun _ => idtac) use_curve_good. { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower]. rewrite Bool.andb_true_iff, !Z.leb_le. lia. } -- cgit v1.2.3