signs

1 files changed, 31 insertions, 5 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 9cde7d97..1dbf2782 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -295,7 +295,9 @@ Theorem rough_approx_inv_longu_correct :
     (0 < Int64.unsigned b)%Z ->
     exists (f : float),
       (rough_approx_inv_longu (Vlong b)) = Vfloat f /\
-      is_finite _ _ f = true /\ (Rabs((B2R _ _ f) - (1 / IZR (Int64.unsigned b))) <= rough_approx_inv_thresh)%R.
+        is_finite _ _ f = true /\
+        (Rabs((B2R _ _ f) - (1 / IZR (Int64.unsigned b))) <= rough_approx_inv_thresh)%R (* /\
+        Bsign _ _ f = false. *)
 Proof.
   intros b NONZ.
   unfold rough_approx_inv_longu.
@@ -328,7 +330,8 @@ Proof.
     set (b'' := IZR b') in *.
     gappa.
   }
-  destruct C1 as (C1R & C1F & _).
+  rewrite (Zlt_bool_false b' 0) in C1 by lia.
+  destruct C1 as (C1R & C1F & C1S).
   set (b_s :=  (BofZ 24 128 re re b')) in *.
 
   assert(1 <= B2R 24 128 b_s <= 18446744073709551616)%R as b_s_RANGE.
@@ -347,10 +350,19 @@ Proof.
     cbn.
     gappa.
   }
-  
-  destruct C2 as (C2R & C2F & _).
+  destruct C2 as (C2R & C2F & C2Sz).
+  rewrite C1S in C2Sz.
+  change (xorb _ _) with false in C2Sz.
   set (invb_s := (Bdiv 24 128 re re Float32.binop_nan mode_NE one_s b_s)) in *.
   rewrite C0F in C2F.
+  assert (is_nan 24 128 invb_s = false) as NAN.
+  { apply is_finite_not_is_nan.
+    assumption.
+  }
+  pose proof (C2Sz NAN) as C2S.
+  clear C2Sz.
+  
+  apply is_finite_not_is_nan in C2S.
 
   assert ((1/18446744073709551616 <= B2R 24 128 invb_s <= 1)%R) as invb_s_RANGE.
   { rewrite C2R.
@@ -462,5 +474,19 @@ Proof.
                       (BofZ 53 1024 re re a') f) 0 Int64.max_unsigned) as C4.
   rewrite C3F in C4.
   rewrite C3R in C4.
-  
+  rewrite C2R in C4.
+
+  assert(0 <=
+      (round radix2 (FLT_exp (-1074) 53) ZnearestE
+              (round radix2 (FLT_exp (3 - 1024 - 53) 53) 
+                 (round_mode mode_NE) (IZR a') * B2R 53 1024 f))
+         <= IZR Int64.max_unsigned)%R as q_RANGE.
+  { clear C4.
+    change (IZR Int64.max_unsigned) with 18446744073709551615%R.
+    cbn.
+    replace (B2R 53 1024 f)%R with ((B2R 53 1024 f - 1 / IZR b') + 1 / IZR b')%R by ring.
+    unfold rough_approx_inv_thresh in C1D.
+    set (delta :=  (B2R 53 1024 f - 1 / IZR b')%R) in *.
+    gappa.
+  }
 Admitted.