diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 19:36:11 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 19:36:11 +0100 |
| commit | cb47d75e20231f06b3e5928b003dc3b5e265b6f8 (patch) | |
| tree | fd1499cad7dcb37b3b685176eb3ffd825a5b2eae /kvx | |
| parent | e71543cef7a06dbe7091fac15aba7ca4d7ab32fd (diff) | |
| download | compcert-kvx-cb47d75e20231f06b3e5928b003dc3b5e265b6f8.tar.gz compcert-kvx-cb47d75e20231f06b3e5928b003dc3b5e265b6f8.zip | |
test gappa
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 89b54346..afa31a72 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -35,7 +35,7 @@ Definition approx_inv b := let x := Eop Ofmaddf (invb_d_var ::: alpha ::: invb_d_var ::: Enil) in Elet b (Elet invb_d x). -Definition approx_inv_thresh := (0.1)%R. +Definition approx_inv_thresh := (1/10)%R. (* Lemma BofZ_exact_zero: @@ -74,7 +74,7 @@ Proof. 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'. + assert (1 <= IZR b' <= 4294967295)%R as RANGE'. { split. { apply IZR_le. lia. } apply IZR_le. lia. @@ -86,11 +86,11 @@ Proof. unfold Float.of_longu in b_d. assert(SILLY : (- 2 ^ 24 <= 1 <= 2 ^ 24)%Z) by lia. - destruct (BofZ_exact 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1 SILLY) as (C0E & C0F & C0S). + destruct (BofZ_exact 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1 SILLY) as (C0E & C0F & _). clear SILLY. assert(SILLY : (- 2 ^ 53 <= 1 <= 2 ^ 53)%Z) by lia. - destruct (BofZ_exact 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1 SILLY) as (C9E & C9F & C9S). + destruct (BofZ_exact 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1 SILLY) as (C9E & C9F & _). clear SILLY. pose proof (BofZ_correct 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') as C1. @@ -138,13 +138,9 @@ Proof. assumption. } - pose proof (BofZ_correct 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 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 & _). + assert(SILLY : (- 2 ^ 53 <= b' <= 2 ^ 53)%Z) by lia. + destruct (BofZ_exact 53 1024 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b' SILLY) as (C4E & C4F & _). + clear SILLY. assert (is_finite 53 1024 b_d = true) as b_d_F. { unfold b_d. @@ -191,10 +187,16 @@ Proof. rewrite Int64.unsigned_repr by lia. rewrite C4E. cbn. - set (rd := round radix2 (FLT_exp (-1074) 53) ZnearestE). - set (rs := round radix2 (FLT_exp (-149) 24) ZnearestE). - set (bi := IZR b'). - set (invb := rd (rs (1/ rs bi))%R). + set (rd := round radix2 (FLT_exp (-1074) 53) ZnearestE) in *. + set (rs := round radix2 (FLT_exp (-149) 24) ZnearestE) in *. + set (bi := IZR b') in *. + set (invb0 := rd (rs (1/ rs bi))%R) in *. + set (alpha := (- invb0 * bi + 1)%R) in *. + assert (-1/IZR (2^21)%Z <= ((1 / bi) - rd (rs(1/ rs bi)))/(1/bi) <= 1/IZR(2^21)%Z)%R. + { unfold rd, rs. + cbn. + gappa. + } Admitted. Definition approx_div a b := |