diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 10:32:15 +0100 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-11 10:32:15 +0100 |
commit | f8d32a19caf88733a9bbeee976f5c2fc549d4f92 (patch) | |
tree | f9640e62f85e5cd86e7e3645011e5e93f79df520 /kvx | |
parent | b45d9ac4b98ed9ce095a1ad64a4192fea89f7b5f (diff) | |
download | compcert-kvx-f8d32a19caf88733a9bbeee976f5c2fc549d4f92.tar.gz compcert-kvx-f8d32a19caf88733a9bbeee976f5c2fc549d4f92.zip |
rewrite with longu -> double -> single conversions
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/FPDivision64.v | 61 |
1 files changed, 38 insertions, 23 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 411865ba..a4d609f0 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -532,7 +532,7 @@ Proof. Qed. Definition step1_real_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 Val.floatofsingle invb_s. Definition step1_real_inv_thresh := (3/33554432)%R. @@ -543,7 +543,7 @@ Theorem step1_real_inv_longu_correct : (0 < Int64.unsigned b)%Z -> exists (f : float), (step1_real_inv_longu (Vlong b)) = Vfloat f /\ - (B2R _ _ f) = (rd (rs (1 / rs (IZR (Int64.unsigned b))))) /\ + (B2R _ _ f) = (rd (rs (1 / rs (rd (IZR (Int64.unsigned b)))))) /\ is_finite _ _ f = true /\ Bsign _ _ f = false. Proof. @@ -553,8 +553,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 *. @@ -565,25 +565,37 @@ Proof. } assert (-16777216 <= 1 <= 16777216)%Z as SILLY by lia. - destruct (BofZ_exact 24 128 re re 1 SILLY) as (C0R & C0F & _). + destruct (BofZ_exact 24 128 re re 1 SILLY) as (C0R & C0F & C0S). 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 C0'. + rewrite Rlt_bool_true in C0'; cycle 1. + { apply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. lia. } + cbn. + gappa. + } + cbn in C0'. + destruct C0' as (C0'R & C0'F & C0'S). + 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 C0'F) as C1. + rewrite C0'R in C1. + rewrite C0'S in C1. rewrite Rlt_bool_true in C1; cycle 1. { clear C1. - eapply (Rabs_relax (IZR 18446744073709551616)). - lra. - set (b'' := IZR b') in *. + eapply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. lia. } + cbn. gappa. } - rewrite (Zlt_bool_false b' 0) in C1 by lia. destruct C1 as (C1R & C1F & C1S). - set (b_s := (BofZ 24 128 re re b')) in *. + 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. + cbn. gappa. } assert(B2R 24 128 b_s <> 0)%R as b_s_NONZ by lra. @@ -599,9 +611,12 @@ Proof. gappa. } rewrite C1R in C2. + rewrite C1S in C2. + rewrite C0S in C2. destruct C2 as (C2R & C2F & C2Sz). - rewrite C1S in C2Sz. - change (xorb _ _) with false in C2Sz. + change (1 <? 0)%Z with false in C2Sz. + replace (b' <? 0)%Z with false in C2Sz by lia. + change (xorb false false) with false in C2Sz. set (invb_s := (Bdiv 24 128 re re Float32.binop_nan mode_NE one_s b_s)) in *. rewrite C0F in C2F. assert (is_nan 24 128 invb_s = false) as NAN. @@ -709,7 +724,7 @@ Definition step1_div_longu a b := Val.maketotal (Val.longuoffloat_ne (step1_real_div_longu a b)). Definition step1_real_quotient (a b : R) := - rd ((rd (a)) * (rd (rs (1 / rs (b))))). + rd ((rd (a)) * (rd (rs (1 / rs (rd (b)))))). Theorem step1_real_div_longu_correct: forall a b, @@ -794,10 +809,10 @@ Proof. unfold smallb_thresh in b_RANGE. unfold smallb_approx_real_range. unfold step1_real_quotient. - set (q := ((rd (a)) * (rd (rs (1 / rs (b)))))%R) in *. + set (q := ((rd (a)) * (rd (rs (1 / rs (rd b)))))%R) in *. replace ((rd q) *b - a)%R with - ((rd(q)-q)/q * rd(a) * (1 + (rd (rs (1 / rs (b))) - 1/b)/(1/b)) + - (rd (a)) * ((rd (rs (1 / rs (b))) - 1 / b) / (1/b)) + + ((rd(q)-q)/q * rd(a) * (1 + (rd (rs (1 / rs (rd b))) - 1/b)/(1/b)) + + (rd (a)) * ((rd (rs (1 / rs (rd b))) - 1 / b) / (1/b)) + (rd(a) - a))%R; cycle 1. { unfold q. field. @@ -1140,7 +1155,7 @@ Proof. } cbn. econstructor; split. reflexivity. - set (q_r := (rd (rd (IZR a') * rd (rs (1 / rs (IZR b')))))%R). + set (q_r := (rd (rd (IZR a') * rd (rs (1 / rs ( rd (IZR b'))))))%R). assert (Rabs (IZR (ZnearestE q_r) - q_r) <= /2)%R as NEAR by apply Znearest_imp2. set (delta1 := (IZR (ZnearestE q_r) - q_r)%R) in NEAR. apply le_IZR3. @@ -1159,11 +1174,11 @@ Proof. unfold q_r. set (a1 := IZR a') in *. set (b1 := IZR b') in *. - replace (rd (rd a1 * rd (rs (1 / rs b1))))%R with - ((((rd (rd a1 * rd (rs (1 / rs b1)))-(a1 * (1 / b1))) / (a1 * (1 / b1)))+1) * (a1 / b1))%R; + replace (rd (rd a1 * rd (rs (1 / rs (rd b1)))))%R with + ((((rd (rd a1 * rd (rs (1 / rs (rd b1))))-(a1 * (1 / b1))) / (a1 * (1 / b1)))+1) * (a1 / b1))%R; cycle 1. { field. lra. } - set (delta2 := ((rd (rd a1 * rd (rs (1 / rs b1)))-(a1 * (1 / b1))) / (a1 * (1 / b1)))%R) in *. + set (delta2 := ((rd (rd a1 * rd (rs (1 / rs (rd b1))))-(a1 * (1 / b1))) / (a1 * (1 / b1)))%R) in *. (* assert (Rabs (delta2) <= 1/4194304)%R. { unfold delta2. gappa. } *) replace (a1 - b1 * (delta1 + (delta2 + 1) * (a1 / b1)))%R with |