diff options
-rw-r--r-- | kvx/FPDivision64.v | 39 |
1 files changed, 37 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index f61cc48c..608b3710 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -242,5 +242,40 @@ Proof. field. lra. } - -Admitted. + assert(Rabs alpha0 <= 257/2147483648)%R as alpha0_ABS. + { rewrite alpha0_EQ. + unfold x0, bd. + gappa. + } + assert (Rabs (x0 - 1 / b1) <= 3/33554432)%R as x0_delta_ABS. + { unfold x0. + gappa. + } + set (x0_delta := (x0 - 1 / b1)%R) in *. + assert (Rabs ((bd - b1) / b1) <= 1/9007199254740992)%R as bd_delta_ABS. + { unfold bd. + gappa. + } + set (bd_delta := ((bd - b1) / b1)%R) in *. + set (rnd_alpha0_delta := (round radix2 (FLT_exp (-1074) 53) ZnearestE alpha0 - alpha0)%R) in *. + assert (Rabs rnd_alpha0_delta <= 1/75557863725914323419136)%R as rnd_alpha0_delta_ABS. + { unfold rnd_alpha0_delta. + gappa. + } + assert (1/18446744073709551616 <= x0 <= 1)%R as x0_RANGE. + { unfold x0. + gappa. + } + assert (Rabs (y1 - 1 / b1) <= 49/4503599627370496)%R as y1_delta_ABS. + { rewrite y1_EQ. + gappa. + } + assert (Rabs(x1 - y1) <= 1/9007199254740992)%R as x1_delta_ABS. + { unfold x1. + gappa. + } + set (y1_delta := (y1 - 1 / b1)%R) in *. + set (x1_delta := (x1-y1)%R) in *. + unfold approx_inv_thresh. + gappa. +Qed. |