From 884cbaab11e294c9c5224b2fc98e68074d6a1584 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Feb 2022 20:42:32 +0100
Subject: twostep_mod_longu_mostb_correct

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

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 0d584283..73dba8eb 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1971,6 +1971,100 @@ Proof.
   reflexivity.
 Qed.
 
+Definition step2_mod_long a b :=
+  let q := step2_div_long' a b in
+  let r := Val.subl a (Val.mull q b) in
+  Val.select (Val.cmpl_bool Clt r (Vlong Int64.zero))
+             (Val.addl r b) r Tlong.
+
+Definition twostep_mod_longu a b :=
+  let q1 := step1_div_longu a b in
+  step2_mod_long (Val.subl a (Val.mull b q1)) b.
+
+Lemma vlong_eq: forall a b, (Vlong a) = (Vlong b) -> a = b.
+Proof.
+  intros a b EQ.
+  congruence.
+Qed.
+
+Lemma move_repr_in_mod :
+  forall a b c,
+    Int64.repr (a - b * c)%Z =
+      Int64.repr (a - b * Int64.unsigned (Int64.repr c))%Z.
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  auto 10 with ints.
+Qed.
+
+Lemma twostep_mod_longu_mostb_correct :
+    forall a b
+      (b_RANGE : (1 < Int64.unsigned b <= Int64.max_signed)%Z),
+          (twostep_mod_longu (Vlong a) (Vlong b)) =
+            (Val.maketotal (Val.modlu (Vlong a) (Vlong b))).
+Proof.
+  intros.
+  Local Transparent twostep_div_longu.
+  pose proof (twostep_div_longu_mostb_correct a b b_RANGE) as div_correct.
+  unfold twostep_div_longu, twostep_mod_longu, step2_div_long, step2_mod_long in *.
+  set (q1 := (step1_div_longu (Vlong a) (Vlong b))) in *.
+  set (q2 := (step2_div_long' (Val.subl (Vlong a) (Val.mull (Vlong b) q1)) (Vlong b))) in *.
+  cbn in div_correct.
+  cbn.
+  unfold Int64.eq in *.
+  change (Int64.unsigned Int64.zero) with 0%Z in *.
+  rewrite zeq_false by lia.
+  rewrite zeq_false in div_correct by lia.
+  cbn in div_correct.
+  cbn.
+  destruct q1 as [  |  | q1l |  |  |  ] ; cbn in *; try discriminate.
+  destruct q2 as [  |  | q2l |  |  |  ] ; cbn in *; try discriminate.
+  rewrite <- (function_ite Vlong).
+  rewrite <- (function_ite Vlong) in div_correct.
+  cbn. cbn in div_correct.
+  unfold Int64.lt, Int64.sub, Int64.mul, Int64.add, Int64.divu, Int64.modu in *.
+  set (a' := Int64.unsigned a) in *.
+  set (b' := Int64.unsigned b) in *.
+  set (q1' := Int64.unsigned q1l) in *.
+  set (q2' := Int64.unsigned q2l) in *.
+  change (Int64.signed Int64.zero) with 0%Z in *.
+  replace (Int64.repr
+               (Int64.unsigned
+                  (Int64.repr (a' - Int64.unsigned (Int64.repr (b' * q1')))) -
+                  Int64.unsigned (Int64.repr (q2' * b'))))
+    with (Int64.repr (a' - (b' * q1') - (q2' * b')))%Z in * ; cycle 1.
+  {
+    apply Int64.eqm_samerepr.
+    auto 10 with ints.
+  }
+  replace (a' - b' * q1' - q2' * b')%Z with (a' - b' * (q1' + q2'))%Z in * by ring.
+  f_equal.
+  apply vlong_eq in div_correct.
+  rewrite Z.mod_eq by lia.
+  rewrite (move_repr_in_mod a' b' (a' / b'))%Z.
+  rewrite <- div_correct.
+  clear div_correct.
+  rewrite <- (move_repr_in_mod a' b')%Z.
+ 
+  destruct zlt as [NEG | POS].
+  2: reflexivity.
+  rewrite repr_unsigned_add.
+  replace (a' - b' * (q1' + q2') + b')%Z with (a' - b' * (q1' + q2' - 1))%Z by ring.
+  apply Int64.eqm_samerepr.
+  assert (Int64.eqm (Int64.unsigned (Int64.repr (q2' + Int64.unsigned Int64.mone)))
+                    (q2' -1))%Z as EQM.
+  { apply Int64.eqm_trans with (y :=  (q2' + Int64.unsigned Int64.mone)%Z).
+    apply Int64.eqm_sym.
+    apply Int64.eqm_unsigned_repr.
+    apply Int64.eqm_add.
+    apply Int64.eqm_refl.
+    exists (1)%Z.
+    reflexivity.
+  }
+  replace  (q1' + q2' - 1)%Z with (q1' + (q2' - 1))%Z by ring.
+  auto with ints.
+Qed.
+    
 Open Scope cminorsel_scope.
 Definition e_invfs a := Eop Oinvfs (a ::: Enil).
 Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil).
-- 
cgit