From b7875749ae445c43130fabd9eb9099eddea48318 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 10 Jan 2022 15:31:39 +0100 Subject: proof progress --- kvx/FPDivision64.v | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index e025fa94..9463313a 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -406,11 +406,12 @@ Theorem rough_approx_div_longu_correct : (rough_approx_div_longu (Vlong a) (Vlong b)) = Vlong q /\ (Z.abs ((Int64.unsigned a) - (Int64.unsigned q) * (Int64.unsigned b)) <= rough_approx_div_thresh)%Z. Proof. - intros a b b_RANGE. + intros a b b_NONZ. unfold rough_approx_div_longu. - destruct (rough_approx_inv_longu_correct b b_RANGE) as (f & C1R & C1F & C1D). + destruct (rough_approx_inv_longu_correct b b_NONZ) as (f & C1R & C1F & C1D). rewrite C1R. cbn. + Local Transparent Float.to_longu Float.mul. unfold Float.to_longu, Float.mul, Float.of_longu. set (re := (@eq_refl Datatypes.comparison Lt)). @@ -422,6 +423,13 @@ Proof. { split ; apply IZR_le; lia. } + pose proof (Int64.unsigned_range b) as b_RANGE. + change Int64.modulus with 18446744073709551616%Z in b_RANGE. + set (b' := Int64.unsigned b) in *. + assert (1 <= IZR b' <= 18446744073709551615)%R as IZR_b_RANGE. + { split ; apply IZR_le; lia. + } + pose proof (BofZ_correct 53 1024 re re a') as C2. rewrite Rlt_bool_true in C2; cycle 1. { clear C2. @@ -431,4 +439,18 @@ Proof. gappa. } destruct C2 as (C2R & C2F & _). + + pose proof (Bmult_correct 53 1024 re re Float.binop_nan mode_NE + (BofZ 53 1024 re re a') f) as C3. + rewrite Rlt_bool_true in C3; cycle 1. + { clear C3. + rewrite C2R. + replace (B2R 53 1024 f)%R with ((B2R 53 1024 f - 1 / IZR b') + 1 / IZR b')%R by ring. + unfold rough_approx_inv_thresh in C1D. + apply Rabs_relax with (b := bpow radix2 65). + { apply bpow_lt ; lia. } + cbn. + gappa. + } + Admitted. -- cgit