diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 21:50:49 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 21:50:49 +0100 |
| commit | 3ae38acc45f9a9cddab0be68058f28743f8c7a47 (patch) | |
| tree | 800866b87f0a2dc1e092281430038ec03aff4fea /kvx | |
| parent | de209fbba248e47f703f90c90817041cfdbf3d06 (diff) | |
| download | compcert-kvx-3ae38acc45f9a9cddab0be68058f28743f8c7a47.tar.gz compcert-kvx-3ae38acc45f9a9cddab0be68058f28743f8c7a47.zip | |
some more gappa
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 37aa76ea..311632fd 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -51,7 +51,16 @@ Proof. lia. Qed. *) - + +Lemma Rabs_relax: + forall b b' (INEQ : (b < b')%R) x, + (-b <= x <= b)%R -> (Rabs x < b')%R. +Proof. + intros. + apply Rabs_lt. + lra. +Qed. + Theorem approx_inv_correct : forall (ge : genv) (sp: val) cmenv memenv (le : letenv) (expr_b : expr) (b : int) @@ -96,10 +105,9 @@ Proof. pose proof (BofZ_correct 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') as C1. rewrite Rlt_bool_true in C1; cycle 1. { clear C1. cbn. - assert (1 <= (round radix2 (FLT_exp (-149) 24) ZnearestE (IZR b')) <= 4294967296)%R. - gappa. - apply Rabs_lt. + eapply (Rabs_relax (IZR 4294967296)). lra. + gappa. } rewrite Zlt_bool_false in C1 by lia. destruct C1 as (C1E & C1F & _). @@ -113,7 +121,12 @@ Proof. (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1) (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b')) as C2. rewrite Rlt_bool_true in C2; cycle 1. - { clear C2. admit. } + { clear C2. rewrite C1E. + apply (Rabs_relax (bpow radix2 24) (bpow radix2 128)). + { cbn; lra. } + unfold F2R. cbn. unfold F2R. cbn. + gappa. + } 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 & _). @@ -130,7 +143,9 @@ Proof. (@eq_refl Datatypes.comparison Lt) b'))) as C3. fold invb_d in C3. rewrite Rlt_bool_true in C3; cycle 1. - { clear C3. admit. } + { 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 & _). unfold Float.fma. |