progress

1 files changed, 30 insertions, 15 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index fdcd455e..c6613fac 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -37,10 +37,6 @@ Definition approx_inv b :=
 
 Definition approx_inv_thresh := (0.000000000000001)%R.
 
-Arguments is_finite {prec emax}.
-Arguments B2R {prec emax}.
-Arguments BofZ (prec emax) {prec_gt_0_ Hmax}.
-
 (*
 Lemma BofZ_exact_zero:
   forall (prec emax : Z) (prec_gt_0_ : Prec_gt_0 prec)
@@ -55,7 +51,7 @@ Proof.
   lia.
 Qed.
  *)
-  
+
 Theorem approx_inv_correct :
   forall (ge : genv)  (sp: val) cmenv memenv
          (le : letenv) (expr_b : expr) (b : int)
@@ -63,7 +59,7 @@ Theorem approx_inv_correct :
          (b_nz : ((Int.unsigned b) > 0)%Z),
     exists f : float,
       eval_expr ge sp cmenv memenv le (approx_inv expr_b) (Vfloat f) /\
-        is_finite f = true /\ (Rabs((B2R f) - (1 / IZR (Int.unsigned b))) <= approx_inv_thresh)%R.
+        is_finite _ _ f = true /\ (Rabs((B2R _ _ f) - (1 / IZR (Int.unsigned b))) <= approx_inv_thresh)%R.
 Proof.
   intros. unfold approx_inv.
   econstructor. constructor.
@@ -91,24 +87,43 @@ Proof.
   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.
+  Check BofZ.
   change (Int.signed (Int.repr 1%Z)) with 1%Z in invb_d.
   pose proof (Bdiv_correct 24 128 eq_refl eq_refl Float32.binop_nan mode_NE
-                      (BofZ 24 128 1 (Hmax := eq_refl))
-                      (BofZ 24 128 b' (Hmax := eq_refl))) as C2.
+                      (BofZ 24 128 eq_refl eq_refl 1)
+                      (BofZ 24 128 eq_refl eq_refl b')) as C2.
   rewrite Rlt_bool_true in C2; cycle 1.
   { clear C2. admit. }
-  assert (B2R (BofZ 24 128 b' (Hmax:=eq_refl)) <> 0%R) as NONZ.
+  assert (B2R 24 128 (BofZ 24 128 eq_refl eq_refl b') <> 0%R) as NONZ.
   { admit. }
   destruct (C2 NONZ) as (C2E & C2F & C2S).
   clear C2 NONZ.
   Local Transparent Float.of_single.
   unfold Float.of_single in invb_d.
-  pose proof (Bconv_correct 24 128 53 1024 eq_refl eq_refl Float.of_single_nan mode_NE (Bdiv 24 128 eq_refl eq_refl Float32.binop_nan mode_NE
-                                                                                        (BofZ 24 128 1) (BofZ 24 128 b')) C2F) as C3.
+  pose proof (Bconv_correct 24 128 53 1024 (@eq_refl Datatypes.comparison Lt)
+              (@eq_refl Datatypes.comparison Lt) Float.of_single_nan mode_NE
+              (Bdiv 24 128 (@eq_refl Datatypes.comparison Lt)
+                 (@eq_refl Datatypes.comparison Lt) Float32.binop_nan mode_NE
+                 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt)
+                    (@eq_refl Datatypes.comparison Lt) 1)
+                 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt)
+                       (@eq_refl Datatypes.comparison Lt) b'))) as C3.
+  fold invb_d in C3.
   rewrite Rlt_bool_true in C3; cycle 1.
   { clear C3. admit. }
-  destruct C3 as (C3E & C3F & C3S).
-  
+  change (is_finite 24 128 (BofZ 24 128 eq_refl eq_refl 1)) with true in C2F.
+  destruct (C3 C2F) as (C3E & C3F & C3S).
+  unfold Float.fma.
+  assert (is_finite _ _ (Float.neg invb_d) = true) as invb_d_F.
+  { Local Transparent Float.neg.
+    unfold Float.neg.
+    rewrite is_finite_Bopp.
+    assumption.
+  }
+  Set Printing Implicit.
+  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.
 Admitted.
 
 Definition approx_div a b :=
@@ -205,13 +220,13 @@ Proof.
   set (prod := (Float.mul (Float.of_intu a) inv_b)).
   set (a' := Int.unsigned a) in *.
   set (b' := Int.unsigned b) in *.
-  set (prod' := (B2R prod)).
+  set (prod' := (B2R _ _ prod)).
   set (prod_r := ZnearestE prod') in *.
   replace (_ && _ && _) with true by admit.
   cbn.
   f_equal.
   unfold Int.divu.
-  rewrite <- div_approx_reals_correct with (x := B2R prod).
+  rewrite <- div_approx_reals_correct with (x := B2R _ _ prod).
   2: lia.
   {
     unfold div_approx_reals.