some progress

1 files changed, 108 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 4e91b853..ddd96f8e 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1065,6 +1065,114 @@ Proof.
   gappa.
 Qed.
 
+Lemma le_IZR3 :
+  forall n m p : Z, (IZR n <= IZR m <= IZR p)%R -> (n <= m <= p)%Z.
+Proof.
+  intros ; split ; apply le_IZR ; lra.
+Qed.
+
+(* 9223372036854775808%Z. *)
+Definition bigb_thresh := 1000000000000000000%Z.
+Lemma step1_div_longu_correct_anyb2 :
+    forall a b,
+    (1 < Int64.unsigned b <= bigb_thresh)%Z ->
+    exists (q : int64),
+      (step1_div_longu (Vlong a) (Vlong b)) = Vlong q /\
+        (Int64.min_signed <= (Int64.unsigned a - Int64.unsigned b*Int64.unsigned q) <= Int64.max_signed)%Z.
+Proof.
+  intros a b b_RANGE.
+
+  pose proof (Int64.unsigned_range a) as a_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in a_RANGE.
+  set (a' := Int64.unsigned a) in *.
+  set (b' := Int64.unsigned b) in *.
+
+  destruct (Z_le_gt_dec a' 0).
+  { assert (a' = 0%Z) as ZERO by lia.
+    exists Int64.zero.
+    rewrite ZERO.
+    rewrite Int64.unsigned_zero.
+    replace (Z.abs (0 - b' * 0))%Z with 0%Z by lia.
+    replace a with Int64.zero; cycle 1.
+    {
+      unfold a' in ZERO.
+      unfold Int64.zero.
+      rewrite <- ZERO.
+      apply Int64.repr_unsigned.
+    }
+    split.
+    { apply step1_div_longu_a0.
+      lia.
+    }
+    change Int64.min_signed with (-9223372036854775808)%Z.
+    change Int64.max_signed with ( 9223372036854775807)%Z.
+    lia.
+  }
+
+  unfold step1_div_longu.
+  assert (1 < b')%Z as b_NOT01 by lia.   
+  destruct (step1_real_div_longu_correct a b b_NOT01) as (q & C1E & C1R & C1F & C1S).
+  rewrite C1E. cbn.
+  unfold Float.to_longu_ne.
+  pose proof (ZofB_ne_range_correct 53 1024 q 0 Int64.max_unsigned) as C2.
+  rewrite C1F in C2.
+
+  
+  assert (1 <= IZR a' <= 18446744073709551615)%R as a_RANGE'.
+  { split; apply IZR_le; lia. }
+  assert (2 <= IZR b' <= IZR bigb_thresh)%R as b_RANGE'.
+  { split; apply IZR_le; lia. }
+  assert (1 <= IZR b' <= IZR bigb_thresh)%R as b_RANGE'' by lra.
+  cbn zeta in C2.
+  rewrite C2.
+  cbn.
+  rewrite C1R.
+  unfold step1_real_quotient.
+  fold a' b'.
+  unfold bigb_thresh in *.
+  
+  rewrite Zle_bool_true ; cycle 1.
+  { apply Znearest_IZR_le.
+    gappa.
+  }
+  rewrite Zle_bool_true ; cycle 1.
+  { apply Znearest_le_IZR.
+    gappa.
+  }
+  cbn.
+  econstructor; split. reflexivity.
+  set (q_r := (rd (rd (IZR a') * rd (rs (1 / rs (IZR b')))))%R).
+  assert (Rabs (IZR (ZnearestE q_r) - q_r) <= /2)%R as NEAR by apply Znearest_imp2.
+  set (delta1 := (IZR (ZnearestE q_r) - q_r)%R) in NEAR.
+  apply le_IZR3.
+  rewrite minus_IZR.
+  rewrite mult_IZR.
+  rewrite Int64.unsigned_repr ; cycle 1.
+  { split.
+    - apply Znearest_IZR_le. unfold q_r.
+      gappa.
+    - apply Znearest_le_IZR. unfold q_r.
+      change Int64.max_unsigned with 18446744073709551615%Z.
+      gappa.
+  }
+  replace (IZR (ZnearestE q_r)) with ((IZR (ZnearestE q_r) - q_r) + q_r)%R by ring.
+  fold delta1.
+  unfold q_r.
+  set (a1 := IZR a') in *. 
+  set (b1 := IZR b') in *.
+  replace (rd (rd a1 * rd (rs (1 / rs b1))))%R with
+    ((((rd (rd a1 * rd (rs (1 / rs b1)))-(a1 * (1 / b1))) / (a1 * (1 / b1)))+1) * (a1 / b1))%R;
+    cycle 1.
+  { field. lra. }
+  set (delta2 := ((rd (rd a1 * rd (rs (1 / rs b1)))-(a1 * (1 / b1))) / (a1 * (1 / b1)))%R) in *.
+  assert (Rabs (delta2) <= 1/4194304)%R.
+  {  unfold delta2. gappa. }
+  replace (a1 - b1 * (delta1 + (delta2 + 1) * (a1 / b1)))%R with
+    (-b1*delta1 - a1*delta2)%R; cycle 1.
+  { field. lra. }
+  gappa.
+Qed.
+
 Lemma find_quotient:
   forall (a b : Z)
          (b_POS : (0 < b)%Z)