From 13876421ac06c904e9c8ea7636f5bef1fc4c8988 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 12 Jan 2022 19:15:06 +0100
Subject: progress in proofs

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

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index e7ba56e3..5da53535 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -461,7 +461,7 @@ Definition step1_real_div_longu a b :=
   Val.mulf (Val.maketotal (Val.floatoflongu a)) (step1_real_inv_longu b).
 
 Definition step1_div_longu a b :=
-  Val.maketotal (Val.longuoffloat (Val.mulf (Val.maketotal (Val.floatoflongu a)) (step1_real_inv_longu b))).
+  Val.maketotal (Val.longuoffloat_ne (step1_real_div_longu a b)).
 
 Definition step1_real_quotient (a b : R) :=
              rd ((rd (a)) * (rd (rs (1 / rs (b))))).
@@ -538,16 +538,16 @@ Qed.
 
 Definition smallb_thresh :=       4398046511104%Z.
 
-Definition smallb_approx_range := 2200000000000%R.
-Lemma step1_smallb :
+Definition smallb_approx_real_range := 2200000000000%R.
+Lemma step1_smallb_real :
   forall a b
     (a_RANGE : (1 <= a <= 18446744073709551615)%R)
     (b_RANGE : (1 <= b <= IZR smallb_thresh)%R),
-    (Rabs((step1_real_quotient a b) * b - a) <= smallb_approx_range)%R.
+    (Rabs((step1_real_quotient a b) * b - a) <= smallb_approx_real_range)%R.
 Proof.
   intros.
   unfold smallb_thresh in b_RANGE.
-  unfold smallb_approx_range.
+  unfold smallb_approx_real_range.
   unfold step1_real_quotient.
   set (q := ((rd (a)) * (rd (rs (1 / rs (b)))))%R) in *.
   replace ((rd q) *b - a)%R with
@@ -563,3 +563,59 @@ Proof.
   unfold q.
   gappa.
 Qed.
+
+Definition smallb_approx_range := 2200000000000%Z.
+Lemma step1_div_longu_correct :
+    forall a b,
+    (1 < Int64.unsigned b <= smallb_thresh)%Z ->
+    exists (q : int64),
+      (step1_div_longu (Vlong a) (Vlong b)) = Vlong q /\
+        (Z.abs (Int64.unsigned a - Int64.unsigned b*Int64.signed q) <= smallb_approx_range)%Z.
+Proof.
+  intros a b b_RANGE.
+  unfold step1_div_longu.
+  assert (1 < Int64.unsigned b)%Z as b_NOT01 by lia.   
+  destruct (step1_real_div_longu_correct a b b_NOT01) as (q & C1E & C1R & C1F & C1S).
+  rewrite C1E. cbn.
+  unfold Float.to_longu_ne.
+  pose proof (ZofB_ne_range_correct 53 1024 q 0 Int64.max_unsigned) as C2.
+  rewrite C1F in C2.
+  pose proof (Int64.unsigned_range a) as a_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in a_RANGE.
+  set (a' := Int64.unsigned a) in *.
+  assert (1 <= a')%Z by admit.
+  
+  set (b' := Int64.unsigned b) in *.
+  assert (1 <= IZR a' <= 18446744073709551615)%R as a_RANGE'.
+  { split; apply IZR_le; lia. }
+  assert (2 <= IZR b' <= IZR smallb_thresh)%R as b_RANGE'.
+  { split; apply IZR_le; lia. }
+  assert (1 <= IZR b' <= IZR smallb_thresh)%R as b_RANGE'' by lra.
+  pose proof (step1_smallb_real (IZR a') (IZR b') a_RANGE' b_RANGE'') as DELTA.
+  rewrite <- C1R in DELTA.
+
+  assert (0 <= B2R _ _ q)%R as q_NONNEG.
+  { apply Bsign_false_nonneg. assumption. }
+  cbn in C2.
+  rewrite Zle_bool_true in C2; cycle 1.
+  { apply Znearest_IZR_le. assumption. }
+  assert (B2R _ _ q <= 18446744073709551615)%R as q_SMALL.
+  { replace (B2R _ _ q) with
+      ((IZR a' / IZR b') + (B2R _ _ q * IZR b' - IZR a') / IZR b')%R; cycle 1.
+    { field. lra. }
+    unfold smallb_approx_real_range in DELTA.
+    unfold smallb_thresh in b_RANGE'.
+    set (y := (B2R 53 1024 q * IZR b' - IZR a')%R) in *.
+    gappa.
+  }
+  rewrite Zle_bool_true in C2; cycle 1.
+  { apply Znearest_le_IZR. assumption. }
+  cbn in C2.
+
+  change Int64.max_unsigned with 18446744073709551615%Z.
+  rewrite C2.
+  cbn.
+
+  econstructor. split. reflexivity.
+  
+ 
-- 
cgit