proof forward

1 files changed, 25 insertions, 6 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 5da53535..76959118 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -564,13 +564,13 @@ Proof.
   gappa.
 Qed.
 
-Definition smallb_approx_range := 2200000000000%Z.
+Definition smallb_approx_range := 4400000000000%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.
+        (Z.abs (Int64.unsigned a - Int64.unsigned b*Int64.unsigned q) <= smallb_approx_range)%Z.
 Proof.
   intros a b b_RANGE.
   unfold step1_div_longu.
@@ -599,7 +599,7 @@ Proof.
   cbn in C2.
   rewrite Zle_bool_true in C2; cycle 1.
   { apply Znearest_IZR_le. assumption. }
-  assert (B2R _ _ q <= 18446744073709551615)%R as q_SMALL.
+  assert (B2R _ _ q <= 9223376000000000000)%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. }
@@ -609,7 +609,7 @@ Proof.
     gappa.
   }
   rewrite Zle_bool_true in C2; cycle 1.
-  { apply Znearest_le_IZR. assumption. }
+  { apply Znearest_le_IZR. lra. }
   cbn in C2.
 
   change Int64.max_unsigned with 18446744073709551615%Z.
@@ -617,5 +617,24 @@ Proof.
   cbn.
 
   econstructor. split. reflexivity.
-  
- 
+  rewrite Int64.unsigned_repr; cycle 1.
+  { split.
+    - apply Znearest_IZR_le. lra.
+    - apply Znearest_le_IZR.
+      change Int64.max_unsigned with 18446744073709551615%Z.
+      lra.
+  }
+  apply le_IZR.
+  rewrite abs_IZR.
+  unfold smallb_approx_real_range, smallb_approx_range, smallb_thresh in *.
+  rewrite minus_IZR.
+  rewrite mult_IZR.
+  set (q_r := B2R 53 1024 q) in *.
+  assert (Rabs (IZR (ZnearestE q_r) - q_r) <= / 2)%R as NEAR
+      by apply Znearest_imp2.
+  set (q_i := IZR (ZnearestE q_r)) in *.
+  replace  (IZR a' - IZR b' * q_i)%R with
+    (-(IZR b' * (q_i - q_r)) - (q_r * IZR b' - IZR a'))%R by ring.
+  set (delta1 := (q_i - q_r)%R) in *.
+  set (delta2 := (q_r * IZR b' - IZR a')%R) in *.
+  gappa.