From 41701fa253bf8adb790e0f27559bb4e6e6276ea8 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 12 Jan 2022 13:10:49 +0100
Subject: more proofs

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

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index b1ba6938..81d587f7 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -421,9 +421,6 @@ Proof.
   gappa.
 Qed.
 
-Definition rough_approx_div_longu a b :=
-  Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b).
-
 Lemma Bsign_false_nonneg:
   forall prec emax f,
     (Bsign prec emax f) = false -> (0 <= (B2R prec emax f))%R.
@@ -459,7 +456,83 @@ Proof.
   rewrite Zceil_IZR in KK.
   lia.
 Qed.
+
+
+Definition rough_approx_div_longu a b :=
+  Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b).
+Definition smallb_threshold := 4398046511104%Z.
+Definition rough_approx_div_longu_smallb_delta := 3917010173952%Z.
+
+Theorem rough_approx_div_longu_correct:
+  forall a b,
+    (1 < Int64.unsigned b)%Z ->
+    exists (q : float),
+      (rough_approx_div_longu (Vlong a) (Vlong b)) = Vfloat q /\
+        (B2R _ _ q) = rd (rd (IZR (Int64.unsigned a)) * (rd (rs (1 / rs (IZR (Int64.unsigned b)))))) /\
+        is_finite _ _ q = true /\
+        Bsign _ _ q = false.
+Proof.
+  intros a b b_NON01.
+  assert (0 < Int64.unsigned b)%Z as b_NON0 by lia.
+  destruct (rough_approx_inv_longu_correct b b_NON0) as (f & C1E & C1R & C1F & C1S).
+  unfold rough_approx_div_longu.
+  rewrite C1E.
+  cbn.
+  set (b' := Int64.unsigned b) in *.
+  Local Transparent Float.mul.
+  unfold Float.mul, Float.of_longu.
+  econstructor.
+  split. reflexivity.
+  set (a' := Int64.unsigned a) in *.
+  set (re :=  (@eq_refl Datatypes.comparison Lt)).
+
+  pose proof (Int64.unsigned_range a) as a_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in a_RANGE.
+  assert (0 <= IZR a' <= 18446744073709551615)%R as IZR_a_RANGE.
+  { split; apply IZR_le; lia. }
+  pose proof (Int64.unsigned_range b) as b_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in b_RANGE.
+  assert (2 <= IZR b' <= 18446744073709551615)%R as IZR_b_RANGE.
+  { split; apply IZR_le; lia. }
   
+  pose proof (BofZ_correct 53 1024 re re a') as C2.
+  rewrite Rlt_bool_true in C2; cycle 1.
+  { clear C2.
+    apply Rabs_relax with (b := bpow radix2 64).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  destruct C2 as (C2R & C2F & C2S).
+  rewrite Zlt_bool_false in C2S by lia.
+
+  pose proof (Bmult_correct 53 1024 re re Float.binop_nan mode_NE (BofZ 53 1024 re re a') f) as C3.
+  rewrite C1S in C3.
+  rewrite C2S in C3.
+  rewrite C1F in C3.
+  rewrite C2F in C3.
+  rewrite C1R in C3.
+  rewrite C2R in C3.
+  rewrite Rlt_bool_true in C3; cycle 1.
+  { apply Rabs_relax with (b := bpow radix2 64).
+    { apply bpow_lt ; lia. }
+    cbn.
+    gappa.
+  }
+  cbn in C3.
+  destruct C3 as (C3R & C3F & C3Sz).
+  assert (is_nan 53 1024
+          (Bmult 53 1024 re re Float.binop_nan mode_NE 
+                 (BofZ 53 1024 re re a') f) = false) as NAN.
+  { apply is_finite_not_is_nan.
+    assumption. }
+  pose proof (C3Sz NAN) as C3S.
+  clear NAN C3Sz.
+
+  auto.
+Qed.
+  
+(*
 Definition rough_approx_div_thresh := 1683627180032%R.
 
 Theorem rough_approx_div_longu_correct :
@@ -572,12 +645,11 @@ Proof.
   set (delta3 := (f_r - 1 / IZR b')%R) in *.
   gappa.
 Qed.
+ *)
 
 Definition rough_approx_euclid_div_longu a b :=
   Val.maketotal (Val.longuoffloat_ne (rough_approx_div_longu a b)).
 
-Definition smallb_threshold := 4398046511104%Z.
-Definition rough_approx_div_longu_smallb_delta := 3917010173952%Z.
 
 Theorem rough_approx_div_longu_smallb :
   forall a b,
-- 
cgit