diff options
author | jadep <jadep@mit.edu> | 2019-03-07 15:18:42 -0500 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2019-03-25 06:13:45 -0400 |
commit | 3e4edb9a9b8cc15bdc02b9005e0b94561645b77b (patch) | |
tree | 765489dd5ce02b3baf141190b1f52e3eb2ffb1fb /src/Fancy | |
parent | bbabd295594448f12161075c5d19dd369ed04a53 (diff) |
Get new Barrett proofs to generate Fancy code as before
Diffstat (limited to 'src/Fancy')
-rw-r--r-- | src/Fancy/Barrett256.v | 21 |
1 files changed, 5 insertions, 16 deletions
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. |