From 8c60bfedbad045a1d60994d46362d3c61e8b20a8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 Dec 2021 14:26:58 +0100 Subject: progress --- kvx/FPDivision.v | 45 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 40 insertions(+), 5 deletions(-) diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index c6613fac..be0fedfd 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -67,16 +67,25 @@ Proof. { eassumption. } { reflexivity. } } set (invb_d := (Float.of_single (ExtFloat32.inv (Float32.of_intu b)))). - set (b_d := (Float.of_longu (Int64.repr (Int.unsigned b)))). - cbn. + set (b' := Int.unsigned b) in *. pose proof (Int.unsigned_range b) as RANGE. + fold b' in RANGE. change Int.modulus with 4294967296%Z in RANGE. - set (b' := Int.unsigned b) in *. + assert (0 <= b' <= Int64.max_unsigned)%Z as b'RANGE. + { change Int64.max_unsigned with 18446744073709551615%Z. + lia. } assert (0 <= IZR b' <= 4294967295)%R as RANGE'. { split. { apply IZR_le. lia. } apply IZR_le. lia. } + cbn. + + set (b_d := (Float.of_longu (Int64.repr b'))) in *. + Local Transparent Float.of_longu. + unfold Float.of_longu in b_d. + + pose proof (BofZ_correct 24 128 eq_refl eq_refl b') as C1. rewrite Rlt_bool_true in C1; cycle 1. { clear C1. cbn. @@ -84,6 +93,7 @@ Proof. } rewrite Zlt_bool_false in C1 by lia. destruct C1 as (C1E & C1F & C1S). + Local Transparent Float32.of_intu Float32.of_int Float32.div. unfold ExtFloat32.inv, ExtFloat32.one, Float32.of_intu, Float32.of_int, Float32.div in invb_d. fold b' in invb_d. @@ -120,10 +130,35 @@ Proof. rewrite is_finite_Bopp. assumption. } - Set Printing Implicit. + + pose proof (BofZ_correct 53 1024 eq_refl eq_refl b') as C4. + rewrite Rlt_bool_true in C4; cycle 1. + { clear C4. + admit. + } + rewrite Zlt_bool_false in C4 by lia. + destruct C4 as (C4E & C4F & C4S). + + assert (is_finite 53 1024 b_d = true) as b_d_F. + { unfold b_d. + rewrite Int64.unsigned_repr by lia. + assumption. + } + + assert (is_finite 53 1024 ExtFloat.one = true) as one_F by reflexivity. + pose proof (Bfma_correct 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE - (Float.neg invb_d) b_d ExtFloat.one) as C4. + (Float.neg invb_d) b_d ExtFloat.one invb_d_F b_d_F one_F) as C5. + + rewrite Rlt_bool_true in C5; cycle 1. + { admit. } + destruct C5 as (C5E & C5F & C5S). + + pose proof (Bfma_correct 53 1024 eq_refl eq_refl Float.fma_nan mode_NE + (Bfma 53 1024 eq_refl eq_refl Float.fma_nan mode_NE + (Float.neg invb_d) b_d ExtFloat.one) invb_d invb_d C5F C3F C3F) as C6. + Admitted. Definition approx_div a b := -- cgit