progress

1 files changed, 26 insertions, 0 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index a95072a5..4ea3f5a3 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -384,7 +384,9 @@ Proof.
   rewrite ZofB_ne_range_correct by lia.
   set (prod := (Float.mul (Float.of_intu a) inv_b)).
   pose proof (Int.unsigned_range a) as a_range.
+  pose proof (Int.unsigned_range b) as b_range.
   change Int.modulus with 4294967296 in a_range.
+  change Int.modulus with 4294967296 in b_range.
   set (prod' := (B2R _ _ prod)).
   set (prod_r := ZnearestE prod') in *.
 
@@ -409,6 +411,30 @@ Proof.
   destruct C1 as (C1E & C1F & _).
   rewrite C1F. cbn.
 
+  assert(prod'_range : (0 <= prod' <= 4294967296)%R).
+  {
+    rewrite C1E.
+    apply Rabs_def2b in inv_b_correct.
+    set (inv_b_r :=  B2R 53 1024 inv_b) in *.
+    assert (INV_RANGE : (1/4294967296 <= 1/IZR b' <= 1)%R).
+    {
+      unfold Rdiv. split.
+      - apply Rmult_le_compat_l. lra. apply Rinv_le.
+        apply IZR_lt. lia. apply IZR_le. lia.
+      - replace 1%R with (1 * / 1)%R at 2 by field.
+        apply Rmult_le_compat_l. lra.
+        apply Rinv_le. lra. apply IZR_le. lia.
+    }
+    replace inv_b_r with (1/IZR b' + (inv_b_r - 1 / IZR b'))%R by ring.
+    assert (a'_RANGE : (0 <= IZR a' <= 4294967295)%R).
+    { split; apply IZR_le; lia.
+    }
+    unfold approx_inv_thresh in inv_b_correct.
+    set (true_inv := (1 / IZR b')%R) in *.
+    set (delta := (inv_b_r - true_inv)%R) in *.
+    gappa.
+  }
+
   replace (_ && _ ) with true; cycle 1.
   {
     symmetry.