From c46cded7f85c692f12c1d5d912ba4a64150a0696 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 12 Jan 2022 20:15:39 +0100
Subject: proof progresses

---
 kvx/FPDivision64.v | 44 ++++++++++++++++++++++++++++++++++++++------
 1 file changed, 38 insertions(+), 6 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 76959118..c17e4f1b 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -564,6 +564,12 @@ Proof.
   gappa.
 Qed.
 
+Lemma step1_div_longu_a0 :
+  forall b,
+    (0 < Int64.unsigned b)%Z ->
+    (step1_div_longu (Vlong Int64.zero) (Vlong b)) = Vlong Int64.zero.
+Admitted.
+                                         
 Definition smallb_approx_range := 4400000000000%Z.
 Lemma step1_div_longu_correct :
     forall a b,
@@ -573,25 +579,50 @@ Lemma step1_div_longu_correct :
         (Z.abs (Int64.unsigned a - Int64.unsigned b*Int64.unsigned q) <= smallb_approx_range)%Z.
 Proof.
   intros a b b_RANGE.
+
+  pose proof (Int64.unsigned_range a) as a_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in a_RANGE.
+  set (a' := Int64.unsigned a) in *.
+  set (b' := Int64.unsigned b) in *.
+
+  destruct (Z_le_gt_dec a' 0).
+  { assert (a' = 0%Z) as ZERO by lia.
+    exists Int64.zero.
+    rewrite ZERO.
+    rewrite Int64.unsigned_zero.
+    replace (Z.abs (0 - b' * 0))%Z with 0%Z by lia.
+    replace a with Int64.zero; cycle 1.
+    {
+      unfold a' in ZERO.
+      unfold Int64.zero.
+      rewrite <- ZERO.
+      apply Int64.repr_unsigned.
+    }
+    split.
+    { apply step1_div_longu_a0.
+      lia.
+    }
+    unfold smallb_approx_range.
+    lia.
+  }
+
   unfold step1_div_longu.
-  assert (1 < Int64.unsigned b)%Z as b_NOT01 by lia.   
+  assert (1 < 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.
+  fold a' in C1R.
+  fold b' in C1R.
   rewrite <- C1R in DELTA.
 
   assert (0 <= B2R _ _ q)%R as q_NONNEG.
@@ -638,3 +669,4 @@ Proof.
   set (delta1 := (q_i - q_r)%R) in *.
   set (delta2 := (q_r * IZR b' - IZR a')%R) in *.
   gappa.
+Qed.
-- 
cgit