twostep_div_longu_mostb_correct

1 files changed, 75 insertions, 11 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 79bfdc3b..53961294 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1071,16 +1071,15 @@ Proof.
   intros ; split ; apply le_IZR ; lra.
 Qed.
 
-Definition bigb_thresh := 18446740000000000000%Z.
-Lemma step1_div_longu_correct_anyb2 :
+Definition mostb_thresh := 18446740000000000000%Z.
+Lemma step1_div_longu_correct_mostb :
     forall a b,
-      (1 < Int64.unsigned b <= bigb_thresh)%Z ->
-      (Int64.unsigned b <= Int64.unsigned a)%Z ->
+      (1 < Int64.unsigned b <= mostb_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 LESS.
+  intros a b b_RANGE.
 
   pose proof (Int64.unsigned_range a) as a_RANGE.
   change Int64.modulus with 18446744073709551616%Z in a_RANGE.
@@ -1120,16 +1119,16 @@ Proof.
   
   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'.
+  assert (2 <= IZR b' <= IZR mostb_thresh)%R as b_RANGE'.
   { split; apply IZR_le; lia. }
-  assert (1 <= IZR b' <= IZR bigb_thresh)%R as b_RANGE'' by lra.
+  assert (1 <= IZR b' <= IZR mostb_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 *.
+  unfold mostb_thresh in *.
   
   rewrite Zle_bool_true ; cycle 1.
   { apply Znearest_IZR_le.
@@ -1170,9 +1169,6 @@ Proof.
   replace (a1 - b1 * (delta1 + (delta2 + 1) * (a1 / b1)))%R with
     (-b1*delta1 - a1*delta2)%R; cycle 1.
   { field. lra. }
-  assert (b1 <= a1)%R as LESS'.
-  { unfold a1, b1.
-    apply IZR_le. lia. }
   unfold delta2.
   gappa.
 Qed.
@@ -2163,3 +2159,71 @@ Proof.
   rewrite Int64.repr_unsigned.
   reflexivity.
 Qed.
+
+Lemma repr_unsigned_sub2:
+  forall a b,
+    (Int64.repr (a - Int64.unsigned (Int64.repr b))) = Int64.repr (a - b).
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_sub.
+  - apply Int64.eqm_refl.
+  - apply Int64.eqm_sym. apply Int64.eqm_unsigned_repr.
+Qed.
+
+Lemma repr_unsigned_add2:
+  forall a b,
+    (Int64.repr (a + Int64.unsigned (Int64.repr b))) = Int64.repr (a + b).
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_add.
+  - apply Int64.eqm_refl.
+  - apply Int64.eqm_sym. apply Int64.eqm_unsigned_repr.
+Qed.
+    
+Lemma twostep_div_longu_mostb_correct :
+    forall a b
+      (b_RANGE : (1 < Int64.unsigned b <= Int64.max_signed)%Z),
+          (twostep_div_longu (Vlong a) (Vlong b)) =
+            (Val.maketotal (Val.divlu (Vlong a) (Vlong b))).
+Proof.
+  intros.
+  destruct (Z_le_gt_dec (Int64.unsigned b) smallb_thresh).
+  { apply twostep_div_longu_smallb_correct. lia. }
+  set (a' := Int64.unsigned a).
+  set (b' := Int64.unsigned b).
+  assert (0 < b')%Z as b_NOT0 by lia.
+  cbn.
+  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.
+  }
+  cbn.
+
+  unfold twostep_div_longu.
+  assert (1 < Int64.unsigned b <= mostb_thresh)%Z as MOST_B.
+  { unfold mostb_thresh.
+    change Int64.max_signed with 9223372036854775807%Z in b_RANGE.
+    lia.
+  }
+  destruct (step1_div_longu_correct_mostb a b MOST_B) as
+    (q & step1_REW & step1_RANGE).
+  rewrite step1_REW.
+  cbn.
+  rewrite step2_div_long_bigb_correct; cycle 1.
+  1, 2: lia.
+  f_equal.
+
+  unfold Int64.sub, Int64.mul.
+  rewrite repr_unsigned_sub2.
+  rewrite Int64.signed_repr by lia.
+  unfold Int64.add, Int64.divu.
+  fold a' b'.
+  set (q' := Int64.unsigned q) in *.
+  rewrite repr_unsigned_add2.
+  rewrite <- Z.div_add_l by lia.
+  f_equal. f_equal.
+  ring.
+Qed.