diff options
Diffstat (limited to 'kvx/FPDivision32.v')
| -rw-r--r-- | kvx/FPDivision32.v | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v index 5cda1077..c920d22a 100644 --- a/kvx/FPDivision32.v +++ b/kvx/FPDivision32.v @@ -585,4 +585,34 @@ Proof. rewrite Int64.unsigned_repr by (cbn; lia). reflexivity. Qed. - + +Definition e_msubl a b c := Eop Omsub (a ::: b ::: c ::: Enil). +Definition fp_modu32 a b := Elet a (Elet (lift b) (e_msubl (Eletvar 1%nat) (Eletvar 0%nat) + (fp_divu32 (Eletvar 1%nat) (Eletvar 0%nat)))). + +Theorem fp_modu32_correct : + forall (ge : genv) (sp: val) cmenv memenv + (le : letenv) (expr_a expr_b : expr) (a b : int) + (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vint a)) + (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b)) + (b_nz : (Int.unsigned b > 0)%Z), + eval_expr ge sp cmenv memenv le (fp_modu32 expr_a expr_b) + (Vint (Int.modu a b)). +Proof. + intros. + rewrite Int.modu_divu; cycle 1. + { intro Z. + subst. + rewrite Int.unsigned_zero in b_nz. + lia. + } + unfold fp_modu32. + Local Opaque fp_divu32. + repeat (econstructor + apply eval_lift + eassumption). + { apply fp_divu32_correct; + repeat (econstructor + apply eval_lift + eassumption). + } + cbn. + rewrite Int.mul_commut. + reflexivity. +Qed. |