proof progress

1 files changed, 24 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index e025fa94..9463313a 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -406,11 +406,12 @@ Theorem rough_approx_div_longu_correct :
       (rough_approx_div_longu (Vlong a) (Vlong b)) = Vlong q /\
         (Z.abs ((Int64.unsigned a) - (Int64.unsigned q) * (Int64.unsigned b)) <= rough_approx_div_thresh)%Z.
 Proof.
-  intros a b b_RANGE.
+  intros a b b_NONZ.
   unfold rough_approx_div_longu.
-  destruct (rough_approx_inv_longu_correct b b_RANGE) as (f & C1R & C1F & C1D).
+  destruct (rough_approx_inv_longu_correct b b_NONZ) as (f & C1R & C1F & C1D).
   rewrite C1R.
   cbn.
+
   Local Transparent Float.to_longu Float.mul.
   unfold Float.to_longu, Float.mul, Float.of_longu.
   set (re := (@eq_refl Datatypes.comparison Lt)).
@@ -422,6 +423,13 @@ Proof.
   { split ; apply IZR_le; lia.
   }
 
+  pose proof (Int64.unsigned_range b) as b_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in b_RANGE.
+  set (b' := Int64.unsigned b) in *.
+  assert (1 <= IZR b' <= 18446744073709551615)%R as IZR_b_RANGE.
+  { split ; apply IZR_le; lia.
+  }
+
   pose proof (BofZ_correct 53 1024 re re a') as C2.
   rewrite Rlt_bool_true in C2; cycle 1.
   { clear C2.
@@ -431,4 +439,18 @@ Proof.
     gappa.
   }
   destruct C2 as (C2R & C2F & _).
+
+  pose proof (Bmult_correct  53 1024 re re Float.binop_nan mode_NE
+                             (BofZ 53 1024 re re a') f) as C3.
+  rewrite Rlt_bool_true in C3; cycle 1.
+  { clear C3.
+    rewrite C2R.
+    replace (B2R 53 1024 f)%R with ((B2R 53 1024 f - 1 / IZR b') + 1 / IZR b')%R by ring.
+    unfold rough_approx_inv_thresh in C1D.
+    apply Rabs_relax with (b := bpow radix2 65).
+    { apply bpow_lt ; lia. }
+    cbn.
+    gappa.
+  }
+  
 Admitted.