From db85b47c5487ddfa051b01e444d2be555013e7f7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 24 Jan 2022 10:04:21 +0100 Subject: progress --- kvx/FPDivision64.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 6894460f..9ed12064 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1108,7 +1108,7 @@ Qed. Definition step2_real_div_long a b := Val.mulf (Val.maketotal (Val.floatoflong a)) (approx_inv_longu b). -Definition smalla_thresh := 35184372088832%Z. +Definition smalla_thresh := 34184372088832%Z. Lemma step2_real_div_long_smalla_correct : forall (a b : int64) @@ -1116,7 +1116,7 @@ Lemma step2_real_div_long_smalla_correct : (b_NOT0 : (0 < Int64.unsigned b)%Z), exists (q : float), (step2_real_div_long (Vlong a) (Vlong b)) = Vfloat q /\ - (Rabs ((B2R _ _ q) - (IZR (Int64.signed a)) / (IZR (Int64.unsigned b))) <= (255/256))%R. + (Rabs ((B2R _ _ q) - (IZR (Int64.signed a)) / (IZR (Int64.unsigned b))) <= (32767/65536))%R. Proof. intros. unfold step2_real_div_long. -- cgit