progress

1 files changed, 40 insertions, 5 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index c6613fac..be0fedfd 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -67,16 +67,25 @@ Proof.
     { eassumption. }
     { reflexivity. } }
   set (invb_d := (Float.of_single (ExtFloat32.inv (Float32.of_intu b)))).
-  set (b_d := (Float.of_longu (Int64.repr (Int.unsigned b)))).
-  cbn.
+  set (b' := Int.unsigned b) in *. 
   pose proof (Int.unsigned_range b) as RANGE.
+  fold b' in RANGE.
   change  Int.modulus with  4294967296%Z in RANGE.
-  set (b' := Int.unsigned b) in *. 
+  assert (0 <= b' <= Int64.max_unsigned)%Z as b'RANGE.
+  { change Int64.max_unsigned with 18446744073709551615%Z.
+    lia. }
   assert (0 <= IZR b' <= 4294967295)%R as RANGE'.
   { split.
     { apply IZR_le. lia. }
     apply IZR_le. lia.
   }
+  cbn.
+  
+  set (b_d := (Float.of_longu (Int64.repr b'))) in *.
+  Local Transparent Float.of_longu.
+  unfold Float.of_longu in b_d.
+  
+  
   pose proof (BofZ_correct 24 128 eq_refl eq_refl b') as C1.
   rewrite Rlt_bool_true in C1; cycle 1.
   { clear C1. cbn.
@@ -84,6 +93,7 @@ Proof.
   }
   rewrite Zlt_bool_false in C1 by lia.
   destruct C1 as (C1E & C1F & C1S).
+  
   Local Transparent Float32.of_intu Float32.of_int Float32.div.
   unfold ExtFloat32.inv, ExtFloat32.one, Float32.of_intu, Float32.of_int, Float32.div in invb_d.
   fold b' in invb_d.
@@ -120,10 +130,35 @@ Proof.
     rewrite is_finite_Bopp.
     assumption.
   }
-  Set Printing Implicit.
+
+  pose proof (BofZ_correct 53 1024 eq_refl eq_refl b') as C4.
+  rewrite Rlt_bool_true in C4; cycle 1.
+  { clear C4.
+    admit.
+  }
+  rewrite Zlt_bool_false in C4 by lia.
+  destruct C4 as (C4E & C4F & C4S).
+
+  assert (is_finite 53 1024 b_d = true) as b_d_F.
+  { unfold b_d.
+    rewrite Int64.unsigned_repr by lia.
+    assumption.
+  }
+  
+  assert (is_finite 53 1024 ExtFloat.one = true) as one_F by reflexivity.
+  
   pose proof (Bfma_correct 53 1024 (@eq_refl Datatypes.comparison Lt)
           (@eq_refl Datatypes.comparison Lt) Float.fma_nan mode_NE
-          (Float.neg invb_d) b_d ExtFloat.one) as C4.
+          (Float.neg invb_d) b_d ExtFloat.one invb_d_F b_d_F one_F) as C5.
+  
+  rewrite Rlt_bool_true in C5; cycle 1.
+  { admit. }
+  destruct C5 as (C5E & C5F & C5S).
+
+  pose proof (Bfma_correct 53 1024 eq_refl eq_refl Float.fma_nan mode_NE
+       (Bfma 53 1024 eq_refl eq_refl Float.fma_nan mode_NE 
+             (Float.neg invb_d) b_d ExtFloat.one) invb_d invb_d C5F C3F C3F) as C6.
+  
 Admitted.
 
 Definition approx_div a b :=