diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-07 23:05:19 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-07 23:05:19 +0100 |
| commit | bfbd4b7235fe67cc3fa023bcdec88d89ca6f3c99 (patch) | |
| tree | 9daf5a665a21b9b65412e663edf51a8acfe8a705 /kvx | |
| parent | cf534a7a5144f4dadc0b98fc078cd2b11530650f (diff) | |
| download | compcert-kvx-bfbd4b7235fe67cc3fa023bcdec88d89ca6f3c99.tar.gz compcert-kvx-bfbd4b7235fe67cc3fa023bcdec88d89ca6f3c99.zip | |
nice intervals
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 608b3710..ffcc1ef9 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -50,7 +50,7 @@ Qed. Theorem approx_inv_longu_correct : forall b, - (1 <= Int64.unsigned b <= 18446744073709551616)%Z -> + (0 < Int64.unsigned b)%Z -> exists (f : float), (approx_inv_longu (Vlong b)) = Vfloat f /\ is_finite _ _ f = true /\ (Rabs((B2R _ _ f) - (1 / IZR (Int64.unsigned b))) <= approx_inv_thresh)%R. @@ -66,7 +66,9 @@ Proof. set (re := (@eq_refl Datatypes.comparison Lt)). change (Int.signed (Int.repr 1)) with 1%Z. set (b' := Int64.unsigned b) in *. - assert(1 <= IZR b' <= 18446744073709551616)%R as RANGE. + pose proof (Int64.unsigned_range b) as RANGE. + change Int64.modulus with 18446744073709551616%Z in RANGE. + assert(1 <= IZR b' <= 18446744073709551616)%R as RANGE'. { split; apply IZR_le; lia. } |