progress

1 files changed, 64 insertions, 14 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index fad99f76..00e807d4 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -18,6 +18,8 @@ Require Compopts.
 Require Import Psatz.
 Require Import IEEE754_extra.
 
+From Gappa Require Import Gappa_tactic.
+
 Local Open Scope cminorsel_scope.
 
 Local Open Scope string_scope.
@@ -35,23 +37,70 @@ 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)
+         (Hmax : (prec < emax)%Z),
+  B2R (BofZ prec emax 0%Z (Hmax := Hmax)) = 0%R /\
+  is_finite (BofZ prec emax 0%Z (Hmax := Hmax)) = true /\
+    Bsign prec emax (BofZ prec emax 0%Z (Hmax := Hmax)) = false.
+Proof.
+  intros.
+  apply BofZ_exact.
+  pose proof (Z.pow_nonneg 2 prec).
+  lia.
+Qed.
+ *)
+
 Theorem approx_inv_correct :
   forall (ge : genv)  (sp: val) cmenv memenv
-         (le : letenv) (expr_b : expr) b
-         (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b)),
+         (le : letenv) (expr_b : expr) (b : int)
+         (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vint b))
+         (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.
-  repeat econstructor.
-  { eassumption. }
-  { reflexivity. }
-  all: set (invb_d := (Float.of_single (ExtFloat32.inv (Float32.of_intu b)))).
-  all: set (b_d := (Float.of_longu (Int64.repr (Int.unsigned b)))).
-  all: cbn.
-  - admit.
-  - admit.
+  econstructor. constructor.
+  { repeat econstructor.
+    { 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.
+  pose proof (Int.unsigned_range b) as RANGE.
+  change  Int.modulus with  4294967296%Z in RANGE.
+  set (b' := Int.unsigned b) in *. 
+  assert (0 <= IZR b' <= 4294967295)%R as RANGE'.
+  { split.
+    { apply IZR_le. lia. }
+    apply IZR_le. lia.
+  }
+  pose proof (BofZ_correct 24 128 eq_refl eq_refl b') as C1.
+  rewrite Rlt_bool_true in C1; cycle 1.
+  { clear C1. cbn.
+    admit.
+  }
+  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.
+  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.
+  rewrite Rlt_bool_true in C2; cycle 1.
+  { clear C2. cbn.
+    admit.
+  }
+  
+  Search B2R (BofZ _).
 Admitted.
 
 Definition approx_div a b :=
@@ -68,6 +117,7 @@ Definition approx_div a b :=
                    (qr_m1 ::: qr_var ::: rem ::: Enil) in (* (Elet qr cases) *)
   Eop Olowlong ((Elet a (Elet (lift b) (Elet qr cases))) ::: Enil).
 
+Open Scope Z.
 
 Definition div_approx_reals (a b : Z) (x : R) :=
     let q:=ZnearestE x in
@@ -134,7 +184,7 @@ Proof.
   assert (eval_expr ge sp cmenv memenv (Vint b :: Vint a :: le)
                     (Eletvar 0) (Vint b)) as EVAL_b'.
   { constructor. reflexivity. }
-  destruct (approx_inv_correct ge sp cmenv memenv (Vint b :: Vint a :: le) (Eletvar 0) b EVAL_b') as (inv_b & inv_b_eval & inv_b_finite & inv_b_correct).
+  destruct (approx_inv_correct ge sp cmenv memenv (Vint b :: Vint a :: le) (Eletvar 0) b EVAL_b' b_nz) as (inv_b & inv_b_eval & inv_b_finite & inv_b_correct).
   unfold approx_div.
   repeat econstructor.
   { exact EVAL_a. }
@@ -147,13 +197,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 53 1024 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.