anystep_div_longu_correct

1 files changed, 38 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index d96ced31..e57f0d66 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -26,6 +26,7 @@ Require Import Values Globalenvs.
 Require Compopts.
 Require Import Psatz.
 Require Import IEEE754_extra.
+Require Import Memory.
 
 From Gappa Require Import Gappa_tactic.
 
@@ -1910,3 +1911,40 @@ Proof.
   rewrite zlt_false by lia.
   reflexivity.
 Qed.
+
+Definition anystep_div_longu a b m :=
+  Val.select (Val.cmplu_bool (Mem.valid_pointer m) Cgt b (Vlong (Int64.repr smallb_thresh)))
+             (step2_div_longu a b)
+             (twostep_div_longu a b) Tlong.
+
+Lemma anystep_div_longu_correct :
+  forall a b m
+           (b_RANGE : (1 < Int64.unsigned b <= Int64.max_signed)%Z),
+      anystep_div_longu (Vlong a) (Vlong b) m = Vlong (Int64.repr (Int64.unsigned a / Int64.unsigned b))%Z.
+Proof.
+  intros.
+  unfold anystep_div_longu.
+  set (a' := Int64.unsigned a).
+  set (b' := Int64.unsigned b).
+  assert (0 < b')%Z as b_NOT0 by lia.
+  cbn.
+  unfold Int64.ltu.
+  fold b'.
+  rewrite Int64.unsigned_repr; cycle 1.
+  { unfold smallb_thresh.
+    change Int64.max_unsigned with 18446744073709551615%Z.
+    lia.
+  }
+  destruct zlt.
+  { rewrite step2_div_longu_bigb_correct by lia.
+    reflexivity.
+  }
+  rewrite twostep_div_longu_smallb_correct 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.
+  }
+  reflexivity.
+Qed.