some progress

1 files changed, 157 insertions, 19 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 74303a7a..e4f883e7 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -29,6 +29,25 @@ Require Import IEEE754_extra.
 
 From Gappa Require Import Gappa_tactic.
 
+
+Lemma Znearest_lub :
+  forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z.
+Proof.
+  intros until x. intro BND.
+  pose proof (Zfloor_lub n x BND).
+  pose proof (Znearest_ge_floor choice x).
+  lia.
+Qed.
+
+Lemma Znearest_glb :
+  forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z.
+Proof.
+  intros until x. intro BND.
+  pose proof (Zceil_glb n x BND).
+  pose proof (Znearest_le_ceil choice x).
+  lia.
+Qed.
+
 Definition approx_inv_longu b :=
   let invb_s := ExtValues.invfs (Val.maketotal (Val.singleoflongu b)) in
   let invb_d := Val.floatofsingle invb_s in
@@ -851,7 +870,99 @@ Proof.
   rewrite C4.
   reflexivity.
 Qed.
-                                         
+
+Lemma step1_div_longu_correct_anyb :
+    forall a b
+     (b_NOT01 : (1 < Int64.unsigned b)%Z),
+    exists (q : int64),
+      (step1_div_longu (Vlong a) (Vlong b)) = Vlong q.
+Proof.
+  intros.
+
+  pose proof (Int64.unsigned_range a) as a_RANGE.
+  pose proof (Int64.unsigned_range b) as b_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in *.
+  set (a' := Int64.unsigned a) in *.
+  set (b' := Int64.unsigned b) in *.
+  assert (0 <= IZR a' <= 18446744073709551615)%R as a_RANGE'.
+  { split; apply IZR_le; lia. }
+  assert (2 <= IZR b' <= 18446744073709551615)%R as b_RANGE'.
+  { split; apply IZR_le; lia. }
+
+  assert (0 < b')%Z as b_NOT0 by lia.
+                                  
+  destruct (Z_le_gt_dec a' 0).
+  { assert (a' = 0%Z) as ZERO by lia.
+    replace a with Int64.zero; cycle 1.
+    {
+      unfold a' in ZERO.
+      unfold Int64.zero.
+      rewrite <- ZERO.
+      apply Int64.repr_unsigned.
+    }
+    exists Int64.zero.
+    apply step1_div_longu_a0.
+    exact b_NOT0.
+  }
+
+  unfold step1_div_longu.
+  unfold step1_real_div_longu.
+  destruct (step1_real_inv_longu_correct b b_NOT0) as (f & C1E & C1R & C1F & C1S).
+  rewrite C1E.
+  cbn.
+  unfold Float.of_longu, Float.mul, Float.to_longu_ne.
+  set (re := (@eq_refl Datatypes.comparison Lt)).
+  fold a'.
+  fold b' in C1R.
+  pose proof (BofZ_correct 53 1024 re re a') as C2.
+  rewrite Rlt_bool_true in C2; cycle 1.
+  { clear C2.
+    apply Rabs_relax with (b := bpow radix2 64).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  cbn in C2.
+  destruct C2 as (C2R & C2F & C2S).
+  pose proof  (Bmult_correct 53 1024 re re Float.binop_nan mode_NE
+                             (BofZ 53 1024 re re a') f) as C3.
+  rewrite C2R in C3.
+  rewrite C2F in C3.
+  rewrite C2S in C3.
+  rewrite C1R in C3.
+  rewrite C1F in C3.
+  rewrite C1S in C3.
+  rewrite Rlt_bool_true in C3; cycle 1.
+  { clear C3.
+    apply Rabs_relax with (b := bpow radix2 64).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  cbn in C3.
+  destruct C3 as (C3R & C3F & _).
+  pose proof (ZofB_ne_range_correct 53 1024
+               (Bmult 53 1024 re re Float.binop_nan mode_NE
+                      (BofZ 53 1024 re re a') f) 0 Int64.max_unsigned) as C4.
+  rewrite C3R in C4.
+  rewrite C3F in C4.
+  cbn zeta in C4.
+  rewrite Zle_bool_true in C4 ; cycle 1.
+  { clear C4.
+    apply Znearest_lub.
+    gappa.
+  }
+  rewrite Zle_bool_true in C4 ; cycle 1.
+  { clear C4.
+    apply Znearest_glb.
+    cbn.
+    gappa.
+  }
+  rewrite C4.
+  cbn.
+  eauto.
+Qed.
+
 Definition smallb_approx_range := 4400000000000%Z.
 Lemma step1_div_longu_correct :
     forall a b,
@@ -1194,24 +1305,6 @@ Definition step2_div_long a b :=
   Val.select (Val.cmpl_bool Cgt (Val.subl (Val.mull q b) a) (Vlong Int64.zero))
              (Val.addl q (Vlong Int64.mone)) q Tlong.
 
-Lemma Znearest_lub :
-  forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z.
-Proof.
-  intros until x. intro BND.
-  pose proof (Zfloor_lub n x BND).
-  pose proof (Znearest_ge_floor choice x).
-  lia.
-Qed.
-
-Lemma Znearest_glb :
-  forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z.
-Proof.
-  intros until x. intro BND.
-  pose proof (Zceil_glb n x BND).
-  pose proof (Znearest_le_ceil choice x).
-  lia.
-Qed.
-
 Lemma function_ite :
   forall {A B : Type} (fn : A->B) (b : bool) (x y: A),
     fn (if b then x else y) = (if b then fn x else fn y).
@@ -1663,3 +1756,48 @@ Proof.
   rewrite zlt_false by lia.
   reflexivity.
 Qed.
+  
+Lemma twostep_div_longu_bigb_correct :
+    forall a b
+           (b_BIG : ((Int64.unsigned b) > smallb_thresh)%Z)
+           (b_NOT_TOO_BIG : ((Int64.unsigned b) <= Int64.max_signed)%Z),
+          (twostep_div_longu (Vlong a) (Vlong b)) =
+            (Val.maketotal (Val.divlu (Vlong a) (Vlong b))).
+Proof.
+  intros.
+  unfold twostep_div_longu.
+  set (b' := Int64.unsigned b) in *.
+  set (a' := Int64.unsigned a) in *.
+Admitted.
+
+(*
+  assert (0 < b')%Z as b_NOT0 by lia.
+  assert (b' <= Int64.max_signed)%Z as b_NOTBIG.
+  { change Int64.max_signed with (9223372036854775807)%Z.
+    unfold smallb_thresh in b_RANGE.
+    lia.
+  }
+  cbn.
+  rewrite (step2_div_long_bigb_correct (Int64.sub a (Int64.mul b q1)) b r1_SMALL b_NOT0 b_NOTBIG).
+  unfold Int64.add, Int64.sub, Int64.mul, Int64.divu.
+  fold q1' b' a'.
+  rewrite <- unsigned_repr_sub.
+  rewrite <- unsigned_repr_add.
+  rewrite Int64.signed_repr ; cycle 1.
+  {
+    change Int64.min_signed with (-9223372036854775808)%Z.
+    change Int64.max_signed with (9223372036854775807)%Z.
+    unfold smallb_approx_range in *.
+    lia.
+  }
+  rewrite Z.add_comm.
+  rewrite <- Z.div_add by lia.
+  replace (a' - b' * q1' + q1' * b')%Z with a' by ring.
+  rewrite Int64.eq_false ; cycle 1.
+  { intro Z. unfold b' in b_NOT0. rewrite Z in b_NOT0.
+    rewrite Int64.unsigned_zero in b_NOT0.
+    lia.
+  }
+  reflexivity.
+Qed.
+*)