From 64552329d9e6c1ae4071f2f144f7c767287f75c6 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 24 Jan 2022 11:31:04 +0100
Subject: fix issue

---
 kvx/FPDivision64.v | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 66 insertions(+), 5 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 72ad43d1..7f7aa71a 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1188,15 +1188,76 @@ Proof.
 Qed.
 
 Definition step2_div_long' a b :=
-  Val.maketotal (Val.longuoffloat_ne (step2_real_div_long a b)).
+  Val.maketotal (Val.longoffloat_ne (step2_real_div_long a b)).
 
 Definition step2_div_long a b :=
-  let q := Val.maketotal (Val.longuoffloat_ne (step2_div_long' a b)) in
+  let q := 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 Znearest_lub :
+  forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z.
+Proof.
+  intros until x. intro BND.
+  pose proof (Zfloor_lub n x BND).
+  pose proof (Znearest_ge_floor choice x).
+  lia.
+Qed.
+
+Lemma Znearest_glb :
+  forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z.
+Proof.
+  intros until x. intro BND.
+  pose proof (Zceil_glb n x BND).
+  pose proof (Znearest_le_ceil choice x).
+  lia.
+Qed.
+
 Lemma step2_div_long_smalla_correct :
-    forall a b,
-    (Z.abs (Int64.signed a) <= smalla_thresh)%Z ->
+    forall a b
+      (a_SMALL : (Z.abs (Int64.signed a) <= smalla_thresh)%Z)
+      (b_NOT0 : (0 < Int64.unsigned b)%Z),
       step2_div_long (Vlong a) (Vlong b) = Vlong (Int64.repr (Int64.signed a / Int64.unsigned b))%Z.
-Admitted.
+Proof.
+  intros.
+  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 (Rabs (IZR a') <= IZR smalla_thresh)%R as a_RANGE'.
+  { rewrite Rabs_Zabs.
+    apply IZR_le.
+    assumption.
+  }
+  assert (1 <= IZR b' <= 18446744073709551615)%R as b_RANGE'.
+  { split; apply IZR_le; lia.
+  } 
+  destruct (step2_real_div_long_smalla_correct a b a_SMALL b_NOT0) as (q & C1R & C1E & C1F).
+  fold a' b' in C1E.
+  assert ((Int64.min_signed <=? ZnearestE (B2R 53 1024 q))=true)%Z as q_LOW.
+  { apply Zle_imp_le_bool.
+    change Int64.min_signed with (-9223372036854775808)%Z.
+  set (q' :=  B2R 53 1024 q) in *.
+    apply Znearest_lub.
+    replace q' with (IZR a' / IZR b' + (q' - IZR a' / IZR b'))%R by ring.
+    unfold smalla_thresh in a_RANGE'.
+    gappa.
+  }
+  assert ((ZnearestE (B2R 53 1024 q) <=? Int64.max_signed)=true)%Z as q_HIGH.
+  { apply Zle_imp_le_bool.
+    change Int64.max_signed with (9223372036854775807)%Z.
+    apply Znearest_glb.
+    set (q' :=  B2R 53 1024 q) in *.
+    replace q' with (IZR a' / IZR b' + (q' - IZR a' / IZR b'))%R by ring.
+    unfold smalla_thresh in a_RANGE'.
+    gappa.
+  }
+  unfold step2_div_long, step2_div_long'.
+  rewrite C1R.
+  cbn.
+  unfold Float.to_long_ne.
+  rewrite (ZofB_ne_range_correct _ _ q Int64.min_signed Int64.max_signed).
+  rewrite C1F.
+  rewrite q_LOW.
+  rewrite q_HIGH.
+  cbn.
-- 
cgit