attempt at definition

1 files changed, 13 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index e57f0d66..1739e5cf 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1948,3 +1948,16 @@ Proof.
   }
   reflexivity.
 Qed.
+
+Definition full_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 (Vlong Int64.zero))
+             if_special
+             (anystep_div_longu a b m) Tlong.
+
+