diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 23:50:57 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 23:50:57 +0100 |
| commit | 226b4b55b3518fc2e4e2627cd368725488e3f8c3 (patch) | |
| tree | 4ca2391b46f0f09614456d6ba449dbfe2c35cebe /kvx | |
| parent | ddc5dbba8f6e6eaf0bb08a401a679e6c8fdfe07b (diff) | |
| download | compcert-kvx-226b4b55b3518fc2e4e2627cd368725488e3f8c3.tar.gz compcert-kvx-226b4b55b3518fc2e4e2627cd368725488e3f8c3.zip | |
less admit
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index b23e3e57..41bb27d5 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -404,8 +404,26 @@ Proof. clear SILLY. pose proof (Bmult_correct 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_nan mode_NE (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt)a') inv_b) as C1. + set (inv_b_r := B2R 53 1024 inv_b) in *. + assert (INV_RANGE : (1/4294967296 <= 1/IZR b' <= 1)%R). + apply Rabs_def2b in inv_b_correct. rewrite Rlt_bool_true in C1; cycle 1. - { admit. } + { clear C1. + rewrite C0E. + apply (Rabs_relax (bpow radix2 64)). + { apply bpow_lt. lia. } + replace inv_b_r with (1 / IZR b' + (inv_b_r - 1 / IZR b'))%R by ring. + set (delta := (inv_b_r - 1 / IZR b')%R) in *. + unfold approx_inv_thresh in inv_b_correct. + cbn. + assert (b'_RANGE : (1 <= IZR b' <= 4294967295)%R). + { split; apply IZR_le; lia. + } + assert (a'_RANGE : (0 <= IZR a' <= 4294967295)%R). + { split; apply IZR_le; lia. + } + gappa. + } rewrite C0F in C1. cbn in C1. rewrite C0E in C1. @@ -418,9 +436,6 @@ Proof. assert(prod'_range : (0 <= prod' <= 17179869181/4)%R). { rewrite C1E. - apply Rabs_def2b in inv_b_correct. - set (inv_b_r := B2R 53 1024 inv_b) in *. - assert (INV_RANGE : (1/4294967296 <= 1/IZR b' <= 1)%R). { unfold Rdiv. split. - apply Rmult_le_compat_l. lra. apply Rinv_le. |