diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-15 11:54:18 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-15 11:54:18 +0100 |
| commit | 80c707afa9eb1042b7fca7367011e37343b89042 (patch) | |
| tree | 6b50d4e587e2c93949c0d82331e8d121565d83d9 /kvx | |
| parent | 3043b099fc4837c1cb3727e5b317148154dcc364 (diff) | |
| download | compcert-kvx-80c707afa9eb1042b7fca7367011e37343b89042.tar.gz compcert-kvx-80c707afa9eb1042b7fca7367011e37343b89042.zip | |
progress
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 00e807d4..fdcd455e 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -55,7 +55,7 @@ Proof. lia. Qed. *) - + Theorem approx_inv_correct : forall (ge : genv) (sp: val) cmenv memenv (le : letenv) (expr_b : expr) (b : int) @@ -96,11 +96,19 @@ Proof. (BofZ 24 128 1 (Hmax := eq_refl)) (BofZ 24 128 b' (Hmax := eq_refl))) as C2. rewrite Rlt_bool_true in C2; cycle 1. - { clear C2. cbn. - admit. - } + { clear C2. admit. } + assert (B2R (BofZ 24 128 b' (Hmax:=eq_refl)) <> 0%R) as NONZ. + { admit. } + destruct (C2 NONZ) as (C2E & C2F & C2S). + clear C2 NONZ. + Local Transparent Float.of_single. + unfold Float.of_single in invb_d. + pose proof (Bconv_correct 24 128 53 1024 eq_refl eq_refl Float.of_single_nan mode_NE (Bdiv 24 128 eq_refl eq_refl Float32.binop_nan mode_NE + (BofZ 24 128 1) (BofZ 24 128 b')) C2F) as C3. + rewrite Rlt_bool_true in C3; cycle 1. + { clear C3. admit. } + destruct C3 as (C3E & C3F & C3S). - Search B2R (BofZ _). Admitted. Definition approx_div a b := |