From 3e4edb9a9b8cc15bdc02b9005e0b94561645b77b Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 7 Mar 2019 15:18:42 -0500 Subject: Get new Barrett proofs to generate Fancy code as before --- src/Fancy/Barrett256.v | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) (limited to 'src/Fancy') diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v index 21da40aa7..0474e6e07 100644 --- a/src/Fancy/Barrett256.v +++ b/src/Fancy/Barrett256.v @@ -29,27 +29,13 @@ Module Barrett256. Lemma barrett_red256_correct : COperationSpecifications.BarrettReduction.barrett_red_correct machine_wordsize M (expr.Interp (@ident.gen_interp cast_oor) barrett_red256). Proof. - apply barrett_red_correct with (n:=2%nat) (nout:=2%nat) (machine_wordsize:=machine_wordsize). + apply barrett_red_correct with (machine_wordsize:=machine_wordsize). { lazy. reflexivity. } { apply barrett_red256_eq. } Qed. Definition muLow := Eval lazy in (2 ^ (2 * machine_wordsize) / M) mod (2^machine_wordsize). - Lemma barrett_reduce_correct_specialized : - forall (xLow xHigh : Z), - 0 <= xLow < 2 ^ machine_wordsize -> - 0 <= xHigh < M -> - BarrettReduction.barrett_reduce machine_wordsize M muLow 2 2 xLow xHigh = (xLow + 2 ^ machine_wordsize * xHigh) mod M. - Proof. - intros. - apply BarrettReduction.barrett_reduce_correct; cbv [machine_wordsize M muLow] in *; - try omega; - try match goal with - | |- context [weight] => intros; cbv [weight]; autorewrite with zsimplify; auto using Z.pow_mul_r with omega - end; lazy; try split; congruence. - Qed. - Definition barrett_red256_fancy' (xLow xHigh RegMuLow RegMod RegZero error : positive) := of_Expr 6%positive (make_consts [(RegMuLow, muLow); (RegMod, M); (RegZero, 0)]) @@ -136,7 +122,10 @@ Module Barrett256. | _ => econstructor end. } { cbn. cbv [muLow M]. - repeat (econstructor; [ solve [valid_expr_subgoal] | intros ]). + repeat (match goal with + | _ => eapply valid_LetInZZ + | _ => eapply valid_LetInZ + end; [ solve [valid_expr_subgoal] | intros ]). econstructor. valid_expr_subgoal. } { reflexivity. } Qed. -- cgit v1.2.3