diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-14 14:57:49 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-14 14:57:49 +0100 |
| commit | 478cabe3acf7ac68f4ab14d7211836ac23ba31ec (patch) | |
| tree | 03e2b86f5f45beac9fd8f2a6b662cb62dafbd9b3 /kvx | |
| parent | 7f6cf940516fbdc769b12b61ede81ef710a21537 (diff) | |
| download | compcert-kvx-478cabe3acf7ac68f4ab14d7211836ac23ba31ec.tar.gz compcert-kvx-478cabe3acf7ac68f4ab14d7211836ac23ba31ec.zip | |
approx_inv
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 7fae685f..4e7fce31 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -1,3 +1,5 @@ +From Flocq Require Import Core Digits Operations Round Bracket Sterbenz + Binary Round_odd. Require Archi. Require Import Coqlib. Require Import Compopts. @@ -33,11 +35,15 @@ Theorem approx_inv_correct : forall (ge : genv) (sp: val) cmenv memenv (le : letenv) (expr_b : expr) b (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b)), - eval_expr ge sp cmenv memenv le (approx_inv expr_b) - (Vfloat ExtFloat.one). + exists f : float, + eval_expr ge sp cmenv memenv le (approx_inv expr_b) (Vfloat f) /\ + is_finite _ _ f = true /\ (Rabs((B2R _ _ f) - (1 / IZR (Int.unsigned b))) <= 0.1)%R. Proof. intros. unfold approx_inv. repeat econstructor. { eassumption. } - cbn. -Abort. + { reflexivity. } + all: set (invb_d := (Float.of_single (ExtFloat32.inv (Float32.of_intu b)))). + all: set (b_d := (Float.of_longu (Int64.repr (Int.unsigned b)))). + all: cbn. +Admitted. |