progress

1 files changed, 31 insertions, 4 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index a5be3d0a..a95072a5 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -35,7 +35,7 @@ Definition approx_inv b :=
   let x := Eop Ofmaddf (invb_d_var ::: alpha ::: invb_d_var ::: Enil) in
   Elet b (Elet invb_d x).
 
-Definition approx_inv_thresh := (1/4294967296)%R.
+Definition approx_inv_thresh := (1/17179869184)%R.
 
 (*
 Lemma BofZ_exact_zero:
@@ -383,11 +383,38 @@ Proof.
   unfold Float.to_longu_ne.
   rewrite ZofB_ne_range_correct by lia.
   set (prod := (Float.mul (Float.of_intu a) inv_b)).
-  set (a' := Int.unsigned a) in *.
-  set (b' := Int.unsigned b) in *.
+  pose proof (Int.unsigned_range a) as a_range.
+  change Int.modulus with 4294967296 in a_range.
   set (prod' := (B2R _ _ prod)).
   set (prod_r := ZnearestE prod') in *.
-  replace (_ && _ && _) with true by admit.
+
+  Local Transparent Float.mul Float.of_intu.
+  unfold Float.mul, Float.of_intu in prod.
+  set (a' := Int.unsigned a) in *.
+  set (b' := Int.unsigned b) in *.
+  assert (SILLY : -2^53 <= a' <= 2^53).
+  { cbn; lia. }
+  destruct (BofZ_exact 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) a' SILLY) as (C0E  & C0F & _).
+  clear SILLY.
+  pose proof (Bmult_correct  53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_nan mode_NE
+                               (BofZ 53 1024  (@eq_refl _ Lt) (@eq_refl _ Lt)a') inv_b) as C1.
+  rewrite Rlt_bool_true in C1; cycle 1.
+  { admit. }
+  rewrite C0F in C1.
+  cbn in C1.
+  rewrite C0E in C1.
+  rewrite inv_b_finite in C1.
+  fold prod in C1.
+  fold prod' in C1.
+  destruct C1 as (C1E & C1F & _).
+  rewrite C1F. cbn.
+
+  replace (_ && _ ) with true; cycle 1.
+  {
+    symmetry.
+    rewrite andb_true_iff.
+    admit.
+  }
   cbn.
   f_equal.
   unfold Int.divu.