From f42abd286e90cad92174cd77b2dd068ed8dd11ae Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 10 Jan 2022 15:49:39 +0100 Subject: wrong operator --- kvx/FPDivision64.v | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 9463313a..9cde7d97 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -394,7 +394,7 @@ Proof. Qed. Definition rough_approx_div_longu a b := - Val.maketotal (Val.longuoffloat + Val.maketotal (Val.longuoffloat_ne (Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b))). Definition rough_approx_div_thresh := 1649267441663%Z. @@ -413,7 +413,7 @@ Proof. cbn. Local Transparent Float.to_longu Float.mul. - unfold Float.to_longu, Float.mul, Float.of_longu. + unfold Float.to_longu_ne, Float.mul, Float.of_longu. set (re := (@eq_refl Datatypes.comparison Lt)). pose proof (Int64.unsigned_range a) as a_RANGE. @@ -452,5 +452,15 @@ Proof. cbn. gappa. } + rewrite C1F in C3. + rewrite C2F in C3. + cbn in C3. + destruct C3 as (C3R & C3F & _). + + pose proof (ZofB_ne_range_correct 53 1024 + (Bmult 53 1024 re re Float.binop_nan mode_NE + (BofZ 53 1024 re re a') f) 0 Int64.max_unsigned) as C4. + rewrite C3F in C4. + rewrite C3R in C4. Admitted. -- cgit