diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-12 15:37:43 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-12 15:37:43 +0100 |
| commit | fc58331d1aa0c1379df8b17d52f71b07d80c3045 (patch) | |
| tree | fb664ac8900ad4871dd3aae93d9220ae23c3fb91 /kvx | |
| parent | 41701fa253bf8adb790e0f27559bb4e6e6276ea8 (diff) | |
| download | compcert-kvx-fc58331d1aa0c1379df8b17d52f71b07d80c3045.tar.gz compcert-kvx-fc58331d1aa0c1379df8b17d52f71b07d80c3045.zip | |
give a name
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 81d587f7..e8e7f8be 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -463,12 +463,16 @@ Definition rough_approx_div_longu a b := Definition smallb_threshold := 4398046511104%Z. Definition rough_approx_div_longu_smallb_delta := 3917010173952%Z. +Definition step1_real_quotient (a b : R) := + rd ((rd a) * (rd (rs (1 / rs b)))). + Theorem rough_approx_div_longu_correct: forall a b, (1 < Int64.unsigned b)%Z -> exists (q : float), (rough_approx_div_longu (Vlong a) (Vlong b)) = Vfloat q /\ - (B2R _ _ q) = rd (rd (IZR (Int64.unsigned a)) * (rd (rs (1 / rs (IZR (Int64.unsigned b)))))) /\ + (B2R _ _ q) = step1_real_quotient (IZR (Int64.unsigned a)) + (IZR (Int64.unsigned b)) /\ is_finite _ _ q = true /\ Bsign _ _ q = false. Proof. |