diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-15 15:57:15 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-15 15:57:15 +0100 |
| commit | c254d0b3935fa956ea220731b6ee209ab4cc641a (patch) | |
| tree | 46aa4e959f1f538abfd3668dd7b38c72aad19804 /kvx | |
| parent | ec82303f25209670189572f07865430255da0fd5 (diff) | |
| download | compcert-kvx-c254d0b3935fa956ea220731b6ee209ab4cc641a.tar.gz compcert-kvx-c254d0b3935fa956ea220731b6ee209ab4cc641a.zip | |
progress
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 35 |
1 files changed, 28 insertions, 7 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 86c21fe0..46598501 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -51,7 +51,7 @@ Proof. lia. Qed. *) - + Theorem approx_inv_correct : forall (ge : genv) (sp: val) cmenv memenv (le : letenv) (expr_b : expr) (b : int) @@ -99,7 +99,7 @@ Proof. admit. } rewrite Zlt_bool_false in C1 by lia. - destruct C1 as (C1E & C1F & C1S). + destruct C1 as (C1E & C1F & _). 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. @@ -113,7 +113,7 @@ Proof. { clear C2. admit. } assert (B2R 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') <> 0%R) as NONZ. { admit. } - destruct (C2 NONZ) as (C2E & C2F & C2S). + destruct (C2 NONZ) as (C2E & C2F & _). clear C2 NONZ. Local Transparent Float.of_single. unfold Float.of_single in invb_d. @@ -129,7 +129,7 @@ Proof. rewrite Rlt_bool_true in C3; cycle 1. { clear C3. admit. } change (is_finite 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1)) with true in C2F. - destruct (C3 C2F) as (C3E & C3F & C3S). + destruct (C3 C2F) as (C3E & C3F & _). unfold Float.fma. assert (is_finite _ _ (Float.neg invb_d) = true) as invb_d_F. { Local Transparent Float.neg. @@ -144,7 +144,7 @@ Proof. admit. } rewrite Zlt_bool_false in C4 by lia. - destruct C4 as (C4E & C4F & C4S). + destruct C4 as (C4E & C4F & _). assert (is_finite 53 1024 b_d = true) as b_d_F. { unfold b_d. @@ -160,14 +160,14 @@ Proof. rewrite Rlt_bool_true in C5; cycle 1. { admit. } - destruct C5 as (C5E & C5F & C5S). + destruct C5 as (C5E & C5F & _). pose proof (Bfma_correct 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE (Bfma 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) invb_d invb_d C5F C3F C3F) as C6. rewrite Rlt_bool_true in C6; cycle 1. { admit. } - destruct C6 as (C6E & C6F & C6S). + destruct C6 as (C6E & C6F & _). split. { exact C6F. } rewrite C6E. @@ -183,6 +183,27 @@ Proof. unfold Float.of_int. rewrite (Int.signed_repr 1) by (cbn ; lia). rewrite C9E. + rewrite C3E. + rewrite C2E. + rewrite C0E. + rewrite C1E. + unfold b_d. + rewrite Int64.unsigned_repr by lia. + rewrite C4E. + cbn. + set (rnd_d := round radix2 (FLT_exp (-1074) 53) ZnearestE). + set (rnd_s := round radix2 (FLT_exp (-149) 24) ZnearestE). + set (bi := IZR b'). + replace (- rnd_d (rnd_s (1 / rnd_s bi)) * rnd_d bi + 1)%R + with ((- rnd_d (rnd_s (1 / rnd_s bi)) + 1 / rnd_d bi) / (1 /rnd_d bi))%R; + cycle 1. + { field. + cut (1 <= bi <= 4294967295)%R. + unfold rnd_d. + gappa. + split; apply IZR_le; lia. + } + Admitted. Definition approx_div a b := |