full2_div_longu_correct

1 files changed, 93 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 53961294..38eb6c1b 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2227,3 +2227,96 @@ Proof.
   f_equal. f_equal.
   ring.
 Qed.
+
+Definition full2_div_longu a b m :=
+  let is_big := Val.cmpl_bool Clt b (Vlong Int64.zero) in
+  let is_one := Val.cmplu_bool (Mem.valid_pointer m) Cle b (Vlong Int64.one) in
+  let is_special := Val.or (Val.of_optbool is_big) (Val.of_optbool is_one) in
+  let if_big := Val.select (Val.cmplu_bool (Mem.valid_pointer m) Clt a b)
+                           (Vlong Int64.zero) (Vlong Int64.one) Tlong in
+  let if_special := Val.select is_big if_big a Tlong in
+  Val.select (Val.cmp_bool Cne is_special (Vint Int.zero))
+             if_special
+             (twostep_div_longu a b) Tlong.
+
+Lemma full2_div_longu_correct :
+  forall a b m
+           (b_NOT0 : (0 < Int64.unsigned b)%Z),
+      full2_div_longu (Vlong a) (Vlong b) m = Vlong (Int64.repr (Int64.unsigned a / Int64.unsigned b))%Z.
+Proof.
+
+  Local Opaque twostep_div_longu.
+  intros.
+  unfold full2_div_longu.
+  cbn.
+  unfold Int64.lt, Int64.ltu.
+  pose proof (Int64.unsigned_range a).
+  pose proof (Int64.unsigned_range b).
+  set (a' := Int64.unsigned a) in *.
+  set (b' := Int64.unsigned b) in *.
+  rewrite Int64.signed_zero.
+  rewrite Int64.unsigned_one.
+  destruct zlt.
+  { replace  (Val.cmp_bool Cne
+       (Val.or Vtrue
+          (if negb (if zlt 1 b' then true else false) then Vtrue else Vfalse))
+       (Vint Int.zero)) with (Some true) ; cycle 1.
+    { destruct zlt; reflexivity.
+    }
+    cbn.
+    destruct zlt; cbn.
+    { rewrite Zdiv_small by lia.
+      reflexivity.
+    }
+    rewrite one_bigb_div.
+    reflexivity.
+    {
+      change Int64.modulus with 18446744073709551616%Z in *.
+      split. 2: lia.
+      unfold b'.
+      rewrite Int64.unsigned_signed.
+      unfold Int64.lt.
+      rewrite Int64.signed_zero.
+      rewrite zlt_true by lia.
+      pose proof (Int64.signed_range b).
+      change Int64.min_signed with (-9223372036854775808)%Z in *.
+      change Int64.max_signed with (9223372036854775807)%Z in *.
+      change Int64.modulus with 18446744073709551616%Z in *.
+      lia.
+    }
+    change Int64.modulus with 18446744073709551616%Z in *.
+    lia.
+  }
+  destruct zlt; cbn.
+  { change (negb (Int.eq (Int.or Int.zero Int.zero) Int.zero)) with false.
+    cbn.
+    rewrite twostep_div_longu_mostb_correct.
+    {
+      cbn.
+      unfold Int64.eq.
+      fold b'.
+      rewrite Int64.unsigned_zero.
+      rewrite zeq_false by lia.
+      reflexivity.
+    }
+    
+    change Int64.modulus with 18446744073709551616%Z in *.
+    split. lia.
+    rewrite Int64.unsigned_signed.
+    unfold Int64.lt.
+    rewrite Int64.signed_zero.
+    rewrite zlt_false by lia.
+    pose proof (Int64.signed_range b).
+    change Int64.min_signed with (-9223372036854775808)%Z in *.
+    change Int64.max_signed with (9223372036854775807)%Z in *.
+    change Int64.modulus with 18446744073709551616%Z in *.
+    lia.
+  }
+  change (negb (Int.eq (Int.or Int.zero Int.one) Int.zero)) with true.
+  cbn.
+  replace b' with 1%Z by lia.
+  rewrite Z.div_1_r.
+  unfold a'.
+  rewrite Int64.repr_unsigned.
+  reflexivity.
+Qed.