fixup

1 files changed, 36 insertions, 33 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index 05d6cee7..9bfacb80 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -497,6 +497,9 @@ Proof.
   cbn.
   f_equal.
   unfold Int.divu.
+  assert(Rabs
+             (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - (IZR a' * inv_b_r)) <= 1/512)%R as R1 by gappa.
+
   rewrite <- div_approx_reals_correct with (x := B2R _ _ prod).
   2: lia.
   {
@@ -508,40 +511,39 @@ Proof.
     unfold Int64.sub.
     rewrite Int64.unsigned_repr by (cbn; lia).
     rewrite Int64.unsigned_repr by (cbn; nia).
-    assert(Rabs
-           (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - (IZR a' * inv_b_r)) <= 1/512)%R as R1 by gappa.
+    assert (FMA_RANGE : Int64.min_signed <= a' - prod_r * b' <= Int64.max_signed).
+    { cbn.
+      unfold prod_r.
+      rewrite <- C1E in R1.
+      assert (IZR (-9223372036854775808) <= IZR (a' - ZnearestE prod' * b') <= IZR 9223372036854775807)%R.
+      2: split; apply le_IZR; lra.
+      rewrite minus_IZR.
+      rewrite mult_IZR.
+      replace (IZR (ZnearestE prod')) with (prod' + (IZR (ZnearestE prod') - prod'))%R by ring.
+      pose proof (Znearest_imp2 (fun x => negb (Z.even x)) prod') as R2.
+      set (delta1 := (IZR (ZnearestE prod') - prod')%R) in *.
+      replace prod' with ((prod' - IZR a' * inv_b_r) + IZR a' * (inv_b_r - 1 / IZR b')
+                          + IZR a' / IZR b')%R by (field; lra).
+      set (delta2 :=  (inv_b_r - 1 / IZR b')%R) in *.
+      set (delta3 := (prod' - IZR a' * inv_b_r)%R) in *.
+      replace (IZR a' - (delta3 + IZR a' * delta2 + IZR a' / IZR b' + delta1) * IZR b')%R with
+        (- (delta3 + IZR a' * delta2 + delta1) * IZR b')%R by (field; lra).
+      unfold approx_inv_thresh in *.
+      assert (Rabs(IZR a' * delta2) <= 1/4)%R as R4.
+      { apply Rabs_le.
+        split; 
+          nra. }
+      set (delta4 := (IZR a' * delta2)%R) in *.
+      apply Rabs_def2b in R1.
+      apply Rabs_def2b in R2.
+      apply Rabs_def2b in R4.
+      split; nra.
+    }
     case Z.ltb_spec; intro CMP.
     - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with true; cycle 1.
       { unfold Int64.lt.
         change (Int64.signed Int64.zero) with 0.
-        rewrite Int64.signed_repr; cycle 1.
-        { cbn.
-          unfold prod_r.
-          rewrite <- C1E in R1.
-          assert (IZR (-9223372036854775808) <= IZR (a' - ZnearestE prod' * b') <= IZR 9223372036854775807)%R.
-          2: split; apply le_IZR; lra.
-          rewrite minus_IZR.
-          rewrite mult_IZR.
-          replace (IZR (ZnearestE prod')) with (prod' + (IZR (ZnearestE prod') - prod'))%R by ring.
-          pose proof (Znearest_imp2 (fun x => negb (Z.even x)) prod') as R2.
-          set (delta1 := (IZR (ZnearestE prod') - prod')%R) in *.
-          replace prod' with ((prod' - IZR a' * inv_b_r) + IZR a' * (inv_b_r - 1 / IZR b')
-                              + IZR a' / IZR b')%R by (field; lra).
-          set (delta2 :=  (inv_b_r - 1 / IZR b')%R) in *.
-          set (delta3 := (prod' - IZR a' * inv_b_r)%R) in *.
-          replace (IZR a' - (delta3 + IZR a' * delta2 + IZR a' / IZR b' + delta1) * IZR b')%R with
-            (- (delta3 + IZR a' * delta2 + delta1) * IZR b')%R by (field; lra).
-          unfold approx_inv_thresh in *.
-          assert (Rabs(IZR a' * delta2) <= 1/4)%R as R4.
-          { apply Rabs_le.
-            split; 
-              nra. }
-          set (delta4 := (IZR a' * delta2)%R) in *.
-          apply Rabs_def2b in R1.
-          apply Rabs_def2b in R2.
-          apply Rabs_def2b in R4.
-          split; nra.
-        }
+        rewrite Int64.signed_repr by exact FMA_RANGE.
         rewrite zlt_true by lia.
         reflexivity.
       }
@@ -551,8 +553,7 @@ Proof.
     - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with false; cycle 1.
       { unfold Int64.lt.
         change (Int64.signed Int64.zero) with 0.
-        rewrite Int64.signed_repr; cycle 1.
-        admit.
+        rewrite Int64.signed_repr by exact FMA_RANGE.
         rewrite zlt_false by lia.
         reflexivity.
       }
@@ -592,7 +593,9 @@ Proof.
   { apply Rabs_le.
     split; nra.
   }
-  pose proof (Rabs_triang (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - IZR a' * inv_b_r)  (IZR a' * delta))%R.
+  rewrite <- C1E.
+  rewrite <- C1E in R1.
+  pose proof (Rabs_triang (prod' - IZR a' * inv_b_r)  (IZR a' * delta))%R.
   lra.
 Admitted.