From c31acf1e0448b9c6d0a6b175d0ac605a9b1b82ba Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 10 Jan 2022 15:17:10 +0100 Subject: progress in proofs --- kvx/FPDivision64.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 9baa3f94..e025fa94 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -406,4 +406,29 @@ 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. + unfold rough_approx_div_longu. + destruct (rough_approx_inv_longu_correct b b_RANGE) 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)). + + pose proof (Int64.unsigned_range a) as a_RANGE. + change Int64.modulus with 18446744073709551616%Z in a_RANGE. + set (a' := Int64.unsigned a) in *. + assert (0 <= IZR a' <= 18446744073709551615)%R as IZR_a_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. + apply Rabs_relax with (b := bpow radix2 64). + { apply bpow_lt. lia. } + cbn. + gappa. + } + destruct C2 as (C2R & C2F & _). Admitted. -- cgit