From 191af63b4e3db42f203a5a2a62c5f924d7f37d81 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 15 Feb 2022 20:01:24 +0100 Subject: mods 64 --- kvx/FPDivision64.v | 235 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 235 insertions(+) diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 1d0fd2ee..113bf07a 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2406,3 +2406,238 @@ Proof. rewrite Int64.mul_commut. reflexivity. Qed. + +Definition e_is_negl a := Eop (Ocmp (Ccomplimm Clt Int64.zero)) (a ::: Enil). +Definition e_xorw a b := Eop Oxor (a ::: b ::: Enil). +Definition e_negl a := Eop Onegl (a ::: Enil). +Definition e_absl a := Eop (Oabsdifflimm Int64.zero) (a ::: Enil). + +Definition fp_divs64 a b := + Elet a (Elet (lift b) + (Elet (fp_divu64 (e_absl (Eletvar (1%nat))) (e_absl (Eletvar (0%nat)))) + (e_ite Tlong (Ccompu0 Cne) (e_xorw (e_is_negl (Eletvar 2%nat)) + (e_is_negl (Eletvar 1%nat))) + (e_negl (Eletvar 0%nat)) (Eletvar 0%nat)))). + +Lemma nonneg_signed_unsigned: + forall x (x_NONNEG : (Int64.signed x >= 0)%Z), + (Int64.signed x) = (Int64.unsigned x). +Proof. + intros. + pose proof (Int64.unsigned_range x). + unfold Int64.signed in *. + destruct zlt. reflexivity. + change Int64.modulus with 18446744073709551616%Z in *. + change Int64.half_modulus with 9223372036854775808%Z in *. + lia. +Qed. + +Lemma long_min_signed_unsigned : + (- Int64.min_signed < Int64.max_unsigned)%Z. +Proof. + reflexivity. +Qed. + +Lemma long_divs_divu : + forall a b + (b_NOT0 : (Int64.signed b <> 0)%Z), + Int64.divs a b = if xorb (Int64.lt a Int64.zero) + (Int64.lt b Int64.zero) + then Int64.neg (Int64.divu (ExtValues.long_abs a) + (ExtValues.long_abs b)) + else Int64.divu (ExtValues.long_abs a) (ExtValues.long_abs b). +Proof. + intros. + unfold Int64.divs, Int64.divu, Int64.lt, ExtValues.long_abs. + pose proof (Int64.signed_range a) as a_RANGE. + pose proof (Int64.signed_range b) as b_RANGE. + change (Int64.signed Int64.zero) with 0%Z. + destruct zlt. + - cbn. rewrite (Z.abs_neq (Int64.signed a)) by lia. + rewrite (Int64.unsigned_repr (- Int64.signed a)); cycle 1. + { pose proof long_min_signed_unsigned. lia. } + + destruct zlt. + + rewrite (Z.abs_neq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof long_min_signed_unsigned. lia. } + rewrite <- (Z.opp_involutive (Int64.signed b)) at 1. + rewrite Z.quot_opp_r by lia. + rewrite <- (Z.opp_involutive (Int64.signed a)) at 1. + rewrite Z.quot_opp_l by lia. + rewrite Z.quot_div_nonneg by lia. + rewrite Z.opp_involutive. + reflexivity. + + + rewrite (Z.abs_eq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof Int64.max_signed_unsigned. lia. } + rewrite <- (Z.opp_involutive (Int64.signed a)) at 1. + rewrite Z.quot_opp_l by lia. + rewrite Z.quot_div_nonneg by lia. + rewrite Int64.neg_repr. + reflexivity. + + - cbn. rewrite (Z.abs_eq (Int64.signed a)) by lia. + rewrite (Int64.unsigned_repr (Int64.signed a)); cycle 1. + { pose proof Int64.max_signed_unsigned. lia. } + destruct zlt. + + rewrite (Z.abs_neq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof long_min_signed_unsigned. lia. } + rewrite Int64.neg_repr. + rewrite <- (Z.opp_involutive (Int64.signed b)) at 1. + rewrite Z.quot_opp_r by lia. + rewrite Z.quot_div_nonneg by lia. + reflexivity. + + + rewrite (Z.abs_eq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof Int64.max_signed_unsigned. lia. } + rewrite Z.quot_div_nonneg by lia. + reflexivity. +Qed. + +Lemma nonzero_unsigned_signed : + forall b, (Int64.unsigned b > 0 -> Int64.signed b <> 0)%Z. +Proof. + intros b GT EQ. + rewrite Int64.unsigned_signed in GT. + unfold Int64.lt in GT. + rewrite Int64.signed_zero in GT. + destruct zlt in GT; lia. +Qed. + +Theorem fp_divs64_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_divs64 expr_a expr_b) + (Vlong (Int64.divs a b)). +Proof. + intros. + unfold fp_divs64. + Local Opaque fp_divu64. + repeat (econstructor + apply eval_lift + eassumption). + apply fp_divu64_correct. + all: repeat (econstructor + apply eval_lift + eassumption). + { unfold ExtValues.long_absdiff, ExtValues.Z_abs_diff. + rewrite Int64.signed_zero. rewrite Z.sub_0_r. + rewrite Int64.unsigned_repr. + { pose proof (nonzero_unsigned_signed b b_nz). + lia. + } + pose proof Int64.max_signed_unsigned. + pose proof long_min_signed_unsigned. + pose proof (Int64.signed_range b). + lia. + } + cbn. + rewrite long_divs_divu ; cycle 1. + { apply nonzero_unsigned_signed. assumption. } + unfold Int64.lt, ExtValues.long_abs, ExtValues.long_absdiff, ExtValues.Z_abs_diff. + change (Int64.signed Int64.zero) with 0%Z. + repeat rewrite Z.sub_0_r. + destruct zlt; destruct zlt; reflexivity. +Qed. + +Lemma long_mods_modu : + forall a b + (b_NOT0 : (Int64.signed b <> 0)%Z), + Int64.mods a b = if Int64.lt a Int64.zero + then Int64.neg (Int64.modu (ExtValues.long_abs a) + (ExtValues.long_abs b)) + else Int64.modu (ExtValues.long_abs a) (ExtValues.long_abs b). +Proof. + intros. + unfold Int64.mods, Int64.modu, Int64.lt, ExtValues.long_abs. + pose proof (Int64.signed_range a) as a_RANGE. + pose proof (Int64.signed_range b) as b_RANGE. + change (Int64.signed Int64.zero) with 0%Z. + destruct zlt. + - cbn. rewrite (Z.abs_neq (Int64.signed a)) by lia. + rewrite (Int64.unsigned_repr (- Int64.signed a)); cycle 1. + { pose proof long_min_signed_unsigned. lia. } + + destruct (zlt (Int64.signed b) 0%Z). + + rewrite (Z.abs_neq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof long_min_signed_unsigned. lia. } + rewrite <- (Z.opp_involutive (Int64.signed b)) at 1. + rewrite Z.rem_opp_r by lia. + rewrite <- (Z.opp_involutive (Int64.signed a)) at 1. + rewrite Z.rem_opp_l by lia. + rewrite Z.rem_mod_nonneg by lia. + rewrite Int64.neg_repr. + reflexivity. + + + rewrite (Z.abs_eq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof Int64.max_signed_unsigned. lia. } + rewrite <- (Z.opp_involutive (Int64.signed a)) at 1. + rewrite Z.rem_opp_l by lia. + rewrite Z.rem_mod_nonneg by lia. + rewrite Int64.neg_repr. + reflexivity. + + - cbn. rewrite (Z.abs_eq (Int64.signed a)) by lia. + rewrite (Int64.unsigned_repr (Int64.signed a)); cycle 1. + { pose proof Int64.max_signed_unsigned. lia. } + destruct (zlt (Int64.signed b) 0%Z). + + rewrite (Z.abs_neq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof long_min_signed_unsigned. lia. } + rewrite <- (Z.opp_involutive (Int64.signed b)) at 1. + rewrite Z.rem_opp_r by lia. + rewrite Z.rem_mod_nonneg by lia. + reflexivity. + + + rewrite (Z.abs_eq (Int64.signed b)) by lia. + rewrite Int64.unsigned_repr ; cycle 1. + { pose proof Int64.max_signed_unsigned. lia. } + rewrite Z.rem_mod_nonneg by lia. + reflexivity. +Qed. + +Definition fp_mods64 a b := + Elet a (Elet (lift b) + (Elet (fp_modu64 (e_absl (Eletvar (1%nat))) (e_absl (Eletvar (0%nat)))) + (e_ite Tlong (Ccompl0 Clt) (Eletvar 2%nat) + (e_negl (Eletvar 0%nat)) (Eletvar 0%nat)))). + +Theorem fp_mods64_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_mods64 expr_a expr_b) + (Vlong (Int64.mods a b)). +Proof. + intros. + unfold fp_mods64. + Local Opaque fp_modu64. + repeat (econstructor + apply eval_lift + eassumption). + apply fp_modu64_correct. + all: repeat (econstructor + apply eval_lift + eassumption). + { unfold ExtValues.long_absdiff, ExtValues.Z_abs_diff. + rewrite Int64.signed_zero. rewrite Z.sub_0_r. + rewrite Int64.unsigned_repr. + { pose proof (nonzero_unsigned_signed b b_nz). + lia. + } + pose proof Int64.max_signed_unsigned. + pose proof long_min_signed_unsigned. + pose proof (Int64.signed_range b). + lia. + } + cbn. + rewrite long_mods_modu ; cycle 1. + { apply nonzero_unsigned_signed. assumption. } + unfold Int64.lt, ExtValues.long_abs, ExtValues.long_absdiff, ExtValues.Z_abs_diff. + change (Int64.signed Int64.zero) with 0%Z. + repeat rewrite Z.sub_0_r. + destruct zlt; reflexivity. +Qed. -- cgit