From f651db91393a3df1b3c65e4249423a5c744761e5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 11 Feb 2022 21:19:55 +0100 Subject: fp_modu64_correct --- kvx/FPDivision64.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 56170419..1d0fd2ee 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2376,3 +2376,33 @@ Proof. rewrite <- full2_div_longu_correct with (m := memenv) by lia. apply e_step7_correct; assumption. Qed. + +Definition fp_modu64 a b := Elet a (Elet (lift b) (e_msubl (Eletvar 1%nat) (Eletvar 0%nat) + (fp_divu64 (Eletvar 1%nat) (Eletvar 0%nat)))). + +Theorem fp_modu64_correct : + forall (ge : genv) (sp: val) cmenv memenv + (le : letenv) (expr_a expr_b : expr) (a b : int64) + (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vlong a)) + (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vlong b)) + (b_nz : (Int64.unsigned b > 0)%Z), + eval_expr ge sp cmenv memenv le (fp_modu64 expr_a expr_b) + (Vlong (Int64.modu a b)). +Proof. + intros. + rewrite Int64.modu_divu; cycle 1. + { intro Z. + subst. + rewrite Int64.unsigned_zero in b_nz. + lia. + } + unfold fp_modu64. + Local Opaque fp_divu64. + repeat (econstructor + apply eval_lift + eassumption). + { apply fp_divu64_correct; + repeat (econstructor + apply eval_lift + eassumption). + } + cbn. + rewrite Int64.mul_commut. + reflexivity. +Qed. -- cgit