so that it compiles

1 files changed, 58 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index b5052917..64ac77a1 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1106,7 +1106,63 @@ Proof.
 Qed.
 
 Definition step2_real_div_long a b :=
-  Val.mulf (Val.maketotal (Val.floatoflong a)) (step1_real_inv_longu b).
+  Val.mulf (Val.maketotal (Val.floatoflong a)) (approx_inv_longu b).
+
+Definition smalla_thresh := 35184372088832%Z.
+
+Lemma step2_real_div_long_smalla_correct :
+    forall (a b : int64)
+           (a_SMALL : (Z.abs (Int64.signed a) <= smalla_thresh)%Z)
+           (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))) < (1/2))%R.
+Proof.
+  intros.
+  unfold step2_real_div_long.
+  destruct (approx_inv_longu_correct_rel b b_NOT0) as (f & C0E & C0F & C0R).
+  rewrite C0E.
+  econstructor.
+  split. reflexivity.
+  Local Transparent Float.of_long.
+  unfold Float.mul, Float.of_long.
+  set (re := (@eq_refl Datatypes.comparison Lt)) in *.
+  set (a' := Int64.signed a) in *.
+  set (b' := Int64.unsigned b) in *.
+  assert(Rabs (IZR a') <= IZR smalla_thresh)%R as a_RANGE'.
+  { rewrite Rabs_Zabs.
+    apply IZR_le.
+    assumption.
+  }
+  assert (- 2 ^ 53 <= a' <= 2 ^ 53)%Z as SILLY.
+  { unfold smalla_thresh in a_SMALL.
+    apply Z.abs_le.
+    lia.
+  } 
+  destruct (BofZ_exact 53 1024 re re (Int64.signed a) SILLY) as (C1R & C1F & C1S).
+  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).
+    { apply bpow_lt. lia. }
+    cbn.
+    rewrite C1R.
+    unfold approx_inv_rel_thresh in C0R.
+    admit.
+  }
+  cbn.
+Admitted.
+
+Definition step2_div_long' a b :=
+  Val.maketotal (Val.longuoffloat_ne (step2_real_div_long a b)).
 
 Definition step2_div_long a b :=
-  Val.maketotal (Val.longuoffloat_ne (step2_real_div_long a)).
+  let q := Val.maketotal (Val.longuoffloat_ne (step2_div_long' a b)) in
+  Val.select (Val.cmpl_bool Clt (Val.subl a (Val.mull q b)) (Vlong Int64.zero))
+             (Val.addl q (Vlong Int64.mone)) q Tlong.
+
+Lemma step2_div_long_smalla_correct :
+    forall a b,
+    (Z.abs (Int64.signed a) <= smalla_thresh)%Z ->
+      step2_div_long (Vlong a) (Vlong b) = Vlong (Int64.repr (Int64.signed a / Int64.unsigned b))%Z.
+Admitted.