progress

1 files changed, 121 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 1e5d8478..74303a7a 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1542,3 +1542,124 @@ Proof.
   unfold approx_inv_rel_thresh in *.
   gappa.
 Qed.
+                                                                        
+Lemma step2_div_long_bigb_correct :
+    forall a b
+           (b_BIG : ((Int64.unsigned b) > smallb_thresh)%Z)
+           (b_NOT_TOO_BIG : ((Int64.unsigned b) <= Int64.max_signed)%Z),
+      step2_div_long (Vlong a) (Vlong b) = Vlong (Int64.repr (Int64.signed a / Int64.unsigned b))%Z.
+Proof.
+  intros.
+  pose proof (Int64.unsigned_range b) as b_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in b_RANGE.
+  pose proof (Int64.signed_range a) as a_RANGE.
+  set (a' := (Int64.signed a)) in *.
+  set (b' := (Int64.unsigned b)) in *.
+  assert (IZR (1 + smallb_thresh) <= IZR b' <= 18446744073709551615)%R as b_RANGE'.
+  { split; apply IZR_le; lia.
+  }
+  assert(IZR Int64.min_signed <= IZR a' <= IZR Int64.max_signed)%R as a_RANGE'.
+  { split; apply IZR_le; lia.
+  }
+  unfold smallb_thresh in *; cbn in b_RANGE'.
+  change Int64.min_signed with (-9223372036854775808)%Z in *.
+  change Int64.max_signed with (9223372036854775807)%Z in *.
+  assert (0 < b')%Z as b_NOT0 by lia.
+
+  destruct (step2_real_div_long_bigb_correct a b b_BIG) as (q & C1R & C1E & C1F).
+  fold a' b' in C1E.
+  assert ((Int64.min_signed <=? ZnearestE (B2R 53 1024 q))=true)%Z as q_LOW.
+  { apply Zle_imp_le_bool.
+    change Int64.min_signed with (-9223372036854775808)%Z.
+    apply Znearest_lub.
+    set (q' :=  B2R 53 1024 q) in *.
+    replace q' with (IZR a' / IZR b' + (q' - IZR a' / IZR b'))%R by ring.
+    gappa.
+  }
+  assert ((ZnearestE (B2R 53 1024 q) <=? Int64.max_signed)=true)%Z as q_HIGH.
+  { apply Zle_imp_le_bool.
+    change Int64.max_signed with (9223372036854775807)%Z.
+    apply Znearest_glb.
+    set (q' :=  B2R 53 1024 q) in *.
+    replace q' with (IZR a' / IZR b' + (q' - IZR a' / IZR b'))%R by ring.
+    gappa.
+  }
+  unfold step2_div_long, step2_div_long'.
+  rewrite C1R.
+  cbn.
+  unfold Float.to_long_ne.
+  rewrite (ZofB_ne_range_correct _ _ q Int64.min_signed Int64.max_signed).
+  rewrite C1F.
+  rewrite q_LOW.
+  rewrite q_HIGH.
+  cbn.
+  rewrite normalize_ite.
+  cbn.
+  rewrite <- (function_ite Vlong).
+  f_equal.
+  unfold Int64.lt.
+  set (q' :=  B2R 53 1024 q) in *.
+  fold a'.
+  assert (Int64.signed (Int64.repr (ZnearestE q')) = ZnearestE q') as q_SIGNED.
+  { apply Int64.signed_repr.
+    split; lia.
+  }
+  rewrite Int64.add_signed.
+  rewrite q_SIGNED.
+  rewrite Int64.signed_mone.
+  rewrite Int64.signed_zero.
+  rewrite <- (function_ite Int64.repr).
+  f_equal.
+  replace  (ZnearestE q' + -1)%Z with (ZnearestE q' - 1)%Z by ring.
+  
+  set (q'' :=  (ZnearestE q')) in *.
+  Check Int64.sub_signed.
+  fold a'.
+  rewrite int64_mul_signed_unsigned.
+  rewrite q_SIGNED.
+  fold b'.
+
+  rewrite Int64.sub_signed.
+  fold a'.
+  rewrite signed_repr_sub.
+
+  assert ((Rabs (IZR a' / IZR b' - q') < / 2)%R) as HALF.
+  { replace (IZR a' / IZR b' - q')%R with
+      (-(q' - IZR a' / IZR b'))%R by ring.
+    rewrite Rabs_Ropp.
+    lra.
+  }
+  pose proof (find_quotient a' b' b_NOT0 q' HALF) as QUOTIENT.
+  fold q'' in QUOTIENT.
+  cbn zeta in QUOTIENT.
+
+  assert (b' <> 0)%Z as NONZ by lia.
+  pose proof (Zmod_eq_full a' b' NONZ) as MOD.
+  assert (b' > 0)%Z as b_GT0 by lia.
+  pose proof (Z_mod_lt a' b' b_GT0) as MOD_LT.
+  destruct (Z_lt_dec a' (b' * q'')) as [LT | GE].
+  { replace (b' * q'' >? a')%Z with true in QUOTIENT by lia.
+    replace q'' with (1 + (a' / b'))%Z by lia.
+    replace ((1 + a' / b') * b' - a')%Z
+      with (-(a' - a' / b' * b')+b')%Z by ring.
+    rewrite <- MOD.
+    rewrite Int64.signed_repr; cycle 1.
+    { change Int64.min_signed with (-9223372036854775808)%Z in *.
+      change Int64.max_signed with (9223372036854775807)%Z in *.
+      lia.
+    }
+    rewrite zlt_true by lia.
+    ring.
+  }
+  replace (b' * q'' >? a')%Z with false in QUOTIENT by lia.
+  rewrite <- QUOTIENT.
+  replace (a' / b' * b' - a')%Z with (-(a' - a' / b' * b'))%Z by ring.
+  rewrite <- MOD.
+  rewrite Int64.signed_repr ; cycle 1.
+  { change Int64.min_signed with (-9223372036854775808)%Z in *.
+    change Int64.max_signed with (9223372036854775807)%Z in *.
+    lia.
+  }
+  rewrite zlt_false by lia.
+  reflexivity.
+Qed.