From 759e546e570d82792e4611918cc365dd1000be61 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 15 Feb 2022 19:47:21 +0100 Subject: fp_divs32_correct --- kvx/FPDivision32.v | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/kvx/FPDivision32.v b/kvx/FPDivision32.v index 4e9b2fb2..48e4bbbc 100644 --- a/kvx/FPDivision32.v +++ b/kvx/FPDivision32.v @@ -811,3 +811,44 @@ Proof. rewrite Z.rem_mod_nonneg by lia. reflexivity. Qed. + +Definition fp_mods32 a b := + Elet a (Elet (lift b) + (Elet (fp_modu32 (e_abs (Eletvar (1%nat))) (e_abs (Eletvar (0%nat)))) + (e_ite Tint (Ccomp0 Clt) (Eletvar 2%nat) + (e_neg (Eletvar 0%nat)) (Eletvar 0%nat)))). + +Theorem fp_mods32_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_mods32 expr_a expr_b) + (Vint (Int.mods a b)). +Proof. + intros. + unfold fp_mods32. + Local Opaque fp_modu32. + repeat (econstructor + apply eval_lift + eassumption). + apply fp_modu32_correct. + all: repeat (econstructor + apply eval_lift + eassumption). + { unfold ExtValues.int_absdiff, ExtValues.Z_abs_diff. + rewrite Int.signed_zero. rewrite Z.sub_0_r. + rewrite Int.unsigned_repr. + { pose proof (nonzero_unsigned_signed b b_nz). + lia. + } + pose proof Int.max_signed_unsigned. + pose proof int_min_signed_unsigned. + pose proof (Int.signed_range b). + lia. + } + cbn. + rewrite int_mods_modu ; cycle 1. + { apply nonzero_unsigned_signed. assumption. } + unfold Int.lt, ExtValues.int_abs, ExtValues.int_absdiff, ExtValues.Z_abs_diff. + change (Int.signed Int.zero) with 0%Z. + repeat rewrite Z.sub_0_r. + destruct zlt; reflexivity. +Qed. -- cgit