From c61b77be54b4696e5c5d5ed2a60f00fbc3dedb56 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 24 Jan 2022 14:35:52 +0100
Subject: progress

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

(limited to 'kvx/FPDivision64.v')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 63b48140..766ff80f 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1192,7 +1192,7 @@ Definition step2_div_long' a b :=
 
 Definition step2_div_long a b :=
   let q := step2_div_long' a b in
-  Val.select (Val.cmpl_bool Clt (Val.subl a (Val.mull q b)) (Vlong Int64.zero))
+  Val.select (Val.cmpl_bool Cgt (Val.subl (Val.mull q b) a) (Vlong Int64.zero))
              (Val.addl q (Vlong Int64.mone)) q Tlong.
 
 Lemma Znearest_lub :
@@ -1229,7 +1229,44 @@ Proof.
   intros.
   destruct b; reflexivity.
 Qed.
-  
+
+
+Lemma int64_mul_signed_unsigned:
+    forall x y : int64,
+      Int64.mul x y = Int64.repr (Int64.signed x * Int64.unsigned y).
+Proof.
+  intros.
+  unfold Int64.mul.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_mult.
+  - apply Int64.eqm_sym.
+    apply Int64.eqm_signed_unsigned.
+  - apply Int64.eqm_refl.
+Qed.
+
+Lemma int64_eqm_signed_repr:
+  forall z : Z, Int64.eqm z (Int64.signed (Int64.repr z)).
+Proof.
+  intros.
+  apply Int64.eqm_trans with (y := Int64.unsigned (Int64.repr z)).
+  - apply Int64.eqm_unsigned_repr.
+  - apply Int64.eqm_sym.
+    apply Int64.eqm_signed_unsigned.
+Qed.
+
+Lemma signed_repr_sub:
+  forall x y,
+    Int64.repr (Int64.signed (Int64.repr x) - y) =
+    Int64.repr (x - y).
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_sub.
+  - apply Int64.eqm_sym.
+    apply int64_eqm_signed_repr.
+  - apply Int64.eqm_refl.
+Qed.
+                                                                        
 Lemma step2_div_long_smalla_correct :
     forall a b
       (a_SMALL : (Z.abs (Int64.signed a) <= smalla_thresh)%Z)
@@ -1282,6 +1319,35 @@ Proof.
   cbn.
   rewrite <- (function_ite Vlong).
   f_equal.
+  unfold Int64.lt.
   set (q' :=  B2R 53 1024 q) in *.
+  fold a'.
+  assert (Int64.signed (Int64.repr (ZnearestE q')) = ZnearestE q') as q_SIGNED.
+  { apply Int64.signed_repr.
+    split; lia.
+  }
+  rewrite Int64.add_signed.
+  rewrite q_SIGNED.
+  rewrite Int64.signed_mone.
+  rewrite Int64.signed_zero.
+  rewrite <- (function_ite Int64.repr).
+  f_equal.
+  replace  (ZnearestE q' + -1)%Z with (ZnearestE q' - 1)%Z by ring.
   
+  set (q'' :=  (ZnearestE q')) in *.
+  Check Int64.sub_signed.
+  fold a'.
+  rewrite int64_mul_signed_unsigned.
+  rewrite q_SIGNED.
+  fold b'.
+
+  rewrite Int64.sub_signed.
+  fold a'.
+  rewrite signed_repr_sub.
+
+   
   
+  Check Int64.signed_repr.
+  
+  rewrite find_quotient with (qr := q').
+  cbn.
-- 
cgit