diff options
Diffstat (limited to 'kvx/FPDivision64.v')
| -rw-r--r-- | kvx/FPDivision64.v | 65 |
1 files changed, 35 insertions, 30 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index a4d609f0..bbd94321 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -50,7 +50,7 @@ Proof. Qed. Definition approx_inv_longu b := - let invb_s := ExtValues.invfs (Val.maketotal (Val.singleoflongu b)) in + let invb_s := ExtValues.invfs (Val.singleoffloat (Val.maketotal (Val.floatoflongu b))) in let invb_d := Val.floatofsingle invb_s in let b_d := Val.maketotal (Val.floatoflongu b) in let one := Vfloat (ExtFloat.one) in @@ -68,7 +68,8 @@ Qed. Definition approx_inv_thresh := (25/2251799813685248)%R. (* 1.11022302462516e-14 *) - + +(* Theorem approx_inv_longu_correct_abs : forall b, (0 < Int64.unsigned b)%Z -> @@ -302,6 +303,7 @@ Proof. unfold approx_inv_thresh. gappa. Qed. + *) Local Notation "'rd'" := (round radix2 (FLT_exp (-1074) 53) ZnearestE). Local Notation "'rs'" := (round radix2 (FLT_exp (-149) 24) ZnearestE). @@ -320,8 +322,8 @@ Proof. econstructor. split. reflexivity. - Local Transparent Float.neg Float.of_single Float32.of_longu Float32.div Float.of_longu Float32.of_int Float.of_int. - unfold Float.fma, Float.neg, Float.of_single, Float32.of_longu, ExtFloat32.inv, Float32.div, Float.of_longu, ExtFloat32.one, Float32.of_int, ExtFloat.one, Float.of_int. + Local Transparent Float.neg Float.of_single Float32.of_longu Float32.div Float.of_longu Float32.of_int Float.of_int Float.to_single. + unfold Float.fma, Float.neg, Float.of_single, Float32.of_longu, ExtFloat32.inv, Float32.div, Float.of_longu, ExtFloat32.one, Float32.of_int, ExtFloat.one, Float.of_int, Float.to_single. set (re := (@eq_refl Datatypes.comparison Lt)). change (Int.signed (Int.repr 1)) with 1%Z. set (b' := Int64.unsigned b) in *. @@ -336,20 +338,34 @@ Proof. clear SILLY. set (one_s := (BofZ 24 128 re re 1)) in *. - pose proof (BofZ_correct 24 128 re re b') as C1. - cbn in C1. + pose proof (BofZ_correct 53 1024 re re b') as C5. + rewrite Rlt_bool_true in C5; cycle 1. + { clear C5. + eapply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. lia. } + cbn. + gappa. + } + cbn in C5. + destruct C5 as (C5R & C5F & C5S). + set (b_d := (BofZ 53 1024 re re b')) in *. + + pose proof (Bconv_correct 53 1024 24 128 re re Float.to_single_nan mode_NE b_d C5F) as C1. rewrite Rlt_bool_true in C1; cycle 1. { clear C1. - eapply (Rabs_relax (IZR 18446744073709551616)). - lra. - set (b'' := IZR b') in *. + apply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. lia. } + rewrite C5R. + cbn. gappa. } - destruct C1 as (C1R & C1F & _). - set (b_s := (BofZ 24 128 re re b')) in *. - + cbn in C1. + destruct C1 as (C1R & C1F & C1S). + set (b_s := (Bconv 53 1024 24 128 re re Float.to_single_nan mode_NE b_d)) in *. assert(1 <= B2R 24 128 b_s <= 18446744073709551616)%R as b_s_RANGE. { rewrite C1R. + rewrite C5R. + cbn. gappa. } assert(B2R 24 128 b_s <> 0)%R as b_s_NONZ by lra. @@ -413,19 +429,7 @@ Proof. gappa. } destruct C4 as (C4R & C4F & _). - - pose proof (BofZ_correct 53 1024 re re b') as C5. - cbn in C5. - rewrite Rlt_bool_true in C5; cycle 1. - { clear C5. - eapply (Rabs_relax (IZR 18446744073709551616)). - lra. - set (b'' := IZR b') in *. - gappa. - } - destruct C5 as (C5R & C5F & _). - set (b_d := (BofZ 53 1024 re re b')) in *. - + assert(1 <= B2R 53 1024 b_d <= 18446744073709551616)%R as b_d_RANGE. { rewrite C5R. gappa. @@ -477,15 +481,16 @@ Proof. rewrite C3R. rewrite C2R. rewrite C1R. + rewrite C5R. rewrite C0R. cbn. set(b1 := IZR b') in *. replace (rd 1) with 1%R by gappa. - replace (rd (rs (1 / rs b1))) with - ((((rd (rs (1 / rs b1)) - (/b1))/(/b1))+1)*(/ b1))%R ; cycle 1. + replace (rd (rs (1 / rs (rd b1)))) with + ((((rd (rs (1 / rs (rd b1))) - (/b1))/(/b1))+1)*(/ b1))%R ; cycle 1. { field. lra. } - set (er0 := ((rd (rs (1 / rs b1)) - (/b1))/(/b1))%R). + set (er0 := ((rd (rs (1 / rs (rd b1))) - (/b1))/(/b1))%R). replace (rd b1) with ((((rd b1) - b1)/b1 + 1) * b1)%R; cycle 1. { field. lra. } set (er1 := (((rd b1) - b1)/b1)%R). @@ -2351,8 +2356,8 @@ Open Scope cminorsel_scope. Definition e_invfs a := Eop Oinvfs (a ::: Enil). Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil). Definition e_float_of_long a := Eop Ofloatoflong (a ::: Enil). -Definition e_single_of_longu a := Eop Osingleoflongu (a ::: Enil). Definition e_float_of_single a := Eop Ofloatofsingle (a ::: Enil). +Definition e_single_of_float a := Eop Osingleoffloat (a ::: Enil). Definition e_long_of_float_ne a := Eop Olongoffloat_ne (a ::: Enil). Definition e_longu_of_float_ne a := Eop Olonguoffloat_ne (a ::: Enil). Definition e_mulf a b := Eop Omulf (a ::: b ::: Enil). @@ -2378,7 +2383,7 @@ Definition binv_d_var1 := Eletvar (0%nat). Definition e_setup1 a b rest := Elet a (Elet (e_float_of_longu (Eletvar 0%nat)) (Elet (lift (lift b)) (Elet (e_float_of_longu (Eletvar 0%nat)) - (Elet (e_float_of_single (e_invfs (e_single_of_longu (Eletvar 1%nat)))) + (Elet (e_float_of_single (e_invfs (e_single_of_float (Eletvar 0%nat)))) rest)))). Definition e_step1 := e_longu_of_float_ne (e_mulf a_d_var1 binv_d_var1). |