From 2d8a28a1db545c2fc6f25fc55057ea230decb5c9 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Tue, 25 Jan 2022 13:06:18 +0100
Subject: some progress

---
 kvx/FPDivision64.v | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 66 insertions(+), 2 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 1739e5cf..bf9be23d 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1949,6 +1949,7 @@ 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
@@ -1956,8 +1957,71 @@ Definition full_div_longu a b m :=
   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))
+  Val.select (Val.cmp_bool Cne is_special (Vint Int.zero))
              if_special
              (anystep_div_longu a b m) Tlong.
 
-             
+Lemma one_bigb_div :
+  forall a b
+     (b_RANGE : (9223372036854775808 <= b < 18446744073709551616)%Z)
+     (ORDER : (b <= a < 18446744073709551616)%Z),
+  (a / b = 1)%Z.
+Proof.
+  intros.
+  assert (((a - b) / b) = 0)%Z as ZERO.
+  { apply Zdiv_small. lia.
+  }
+  replace a with (1 * b + (a - b))%Z by ring.
+  rewrite Z.div_add_l by lia.
+  rewrite ZERO.
+  ring.
+Qed.
+
+Lemma full_div_longu_correct :
+  forall a b m
+           (b_NOT0 : (0 < Int64.unsigned b)%Z),
+      full_div_longu (Vlong a) (Vlong b) m = Vlong (Int64.repr (Int64.unsigned a / Int64.unsigned b))%Z.
+Proof.
+  intros.
+  unfold full_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.
+  }
+  
+!
-- 
cgit