From 87bbbd23d6681bfdc29ac5f8bd24b28ba89da4aa Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Feb 2022 21:01:17 +0100
Subject: full2 mod correct

---
 kvx/FPDivision64.v | 98 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 73dba8eb..56170419 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2065,6 +2065,104 @@ Proof.
   auto with ints.
 Qed.
     
+Definition full2_mod_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) Cge a b) (Val.subl a b) a Tlong in
+  let if_special := Val.select is_big if_big (Vlong Int64.zero) Tlong in
+  Val.select (Val.cmp_bool Cne is_special (Vint Int.zero))
+             if_special
+             (twostep_mod_longu a b) Tlong.
+
+Lemma full2_mod_longu_correct :
+  forall a b m
+           (b_NOT0 : (0 < Int64.unsigned b)%Z),
+      full2_mod_longu (Vlong a) (Vlong b) m = Vlong (Int64.repr ((Int64.unsigned a) mod (Int64.unsigned b)))%Z.
+Proof.
+
+  Local Opaque twostep_mod_longu.
+  intros.
+  unfold full2_mod_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.
+    rewrite Z.mod_eq by lia.
+    
+    destruct zlt; cbn.
+    { rewrite Zdiv_small by lia.
+      replace (a' - b' * 0)%Z with a' by ring.
+      unfold a'.
+      rewrite Int64.repr_unsigned.
+      reflexivity.
+    }
+    rewrite one_bigb_div.
+    { unfold Int64.sub.
+      fold a' b'.
+      repeat f_equal. ring.
+    }
+    {
+      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_mod_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.mod_1_r.
+  reflexivity.
+Qed.
+
 Open Scope cminorsel_scope.
 Definition e_invfs a := Eop Oinvfs (a ::: Enil).
 Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil).
-- 
cgit