progress

1 files changed, 12 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 64ac77a1..0dfa9882 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1127,8 +1127,13 @@ Proof.
   Local Transparent Float.of_long.
   unfold Float.mul, Float.of_long.
   set (re := (@eq_refl Datatypes.comparison Lt)) in *.
+  pose proof (Int64.unsigned_range b) as b_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in b_RANGE.
   set (a' := Int64.signed a) in *.
   set (b' := Int64.unsigned b) in *.
+  assert (1 <= IZR b' <= 18446744073709551615)%R as b_RANGE'.
+  { split; apply IZR_le; lia.
+  }
   assert(Rabs (IZR a') <= IZR smalla_thresh)%R as a_RANGE'.
   { rewrite Rabs_Zabs.
     apply IZR_le.
@@ -1143,12 +1148,17 @@ Proof.
   fold a' in C1R.
   pose proof (Bmult_correct 53 1024 re re Float.binop_nan mode_NE (BofZ 53 1024 re re a') f) as C2.
   rewrite Rlt_bool_true in C2 ; cycle 1.
-  { apply Rabs_relax with (b := bpow radix2 53).
+  { clear C2.
+    apply Rabs_relax with (b := bpow radix2 53).
     { apply bpow_lt. lia. }
     cbn.
     rewrite C1R.
     unfold approx_inv_rel_thresh in C0R.
-    admit.
+    replace (B2R 53 1024 f) with
+      ((1/IZR b') * ((IZR b' * B2R 53 1024 f - 1) + 1))%R ; cycle 1.
+    { field. lra. }
+    unfold smalla_thresh in *.
+    gappa.
   }
   cbn.
 Admitted.