From a32b5bf92865e354f81330353857ae2d9ec80d57 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 25 Jan 2022 11:49:19 +0100 Subject: anystep_div_longu_correct --- kvx/FPDivision64.v | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index d96ced31..e57f0d66 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -26,6 +26,7 @@ Require Import Values Globalenvs. Require Compopts. Require Import Psatz. Require Import IEEE754_extra. +Require Import Memory. From Gappa Require Import Gappa_tactic. @@ -1910,3 +1911,40 @@ Proof. rewrite zlt_false by lia. reflexivity. Qed. + +Definition anystep_div_longu a b m := + Val.select (Val.cmplu_bool (Mem.valid_pointer m) Cgt b (Vlong (Int64.repr smallb_thresh))) + (step2_div_longu a b) + (twostep_div_longu a b) Tlong. + +Lemma anystep_div_longu_correct : + forall a b m + (b_RANGE : (1 < Int64.unsigned b <= Int64.max_signed)%Z), + anystep_div_longu (Vlong a) (Vlong b) m = Vlong (Int64.repr (Int64.unsigned a / Int64.unsigned b))%Z. +Proof. + intros. + unfold anystep_div_longu. + set (a' := Int64.unsigned a). + set (b' := Int64.unsigned b). + assert (0 < b')%Z as b_NOT0 by lia. + cbn. + unfold Int64.ltu. + fold b'. + rewrite Int64.unsigned_repr; cycle 1. + { unfold smallb_thresh. + change Int64.max_unsigned with 18446744073709551615%Z. + lia. + } + destruct zlt. + { rewrite step2_div_longu_bigb_correct by lia. + reflexivity. + } + rewrite twostep_div_longu_smallb_correct by lia. + cbn. + rewrite Int64.eq_false ; cycle 1. + { intro Z. unfold b' in b_NOT0. rewrite Z in b_NOT0. + rewrite Int64.unsigned_zero in b_NOT0. + lia. + } + reflexivity. +Qed. -- cgit