From 32a69b2acc078ffc5078ca5f12747170b16d9d78 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Tue, 25 Jan 2022 11:28:55 +0100
Subject: big progress on longu

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

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 69e49f29..d96ced31 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1747,7 +1747,40 @@ Proof.
   unfold approx_inv_rel_thresh in *.
   gappa.
 Qed.
-                                                                        
+
+Lemma repr_unsigned_mul:
+  forall a b,
+    (Int64.repr (Int64.unsigned (Int64.repr a) * b)) = Int64.repr (a * b).
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_mult.
+  - apply Int64.eqm_sym. apply Int64.eqm_unsigned_repr.
+  - apply Int64.eqm_refl.
+Qed.
+
+Lemma repr_unsigned_sub:
+  forall a b,
+    (Int64.repr (Int64.unsigned (Int64.repr a) - b)) = Int64.repr (a - b).
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_sub.
+  - apply Int64.eqm_sym. apply Int64.eqm_unsigned_repr.
+  - apply Int64.eqm_refl.
+Qed.
+
+Lemma repr_unsigned_add:
+  forall a b,
+    (Int64.repr (Int64.unsigned (Int64.repr a) + b)) = Int64.repr (a + b).
+Proof.
+  intros.
+  apply Int64.eqm_samerepr.
+  apply Int64.eqm_add.
+  - apply Int64.eqm_sym. apply Int64.eqm_unsigned_repr.
+  - apply Int64.eqm_refl.
+Qed.
+  
 Lemma step2_div_longu_bigb_correct :
   forall a b
            (b_BIG : ((Int64.unsigned b) > smallb_thresh)%Z)
@@ -1830,15 +1863,23 @@ Proof.
   pose proof (Zmod_eq_full a' b' NONZ) as MOD.
   assert (b' > 0)%Z as b_GT0 by lia.
   pose proof (Z_mod_lt a' b' b_GT0) as MOD_LT.
-  assert ((Int64.signed (Int64.sub (Int64.mul (Int64.repr q'') b) a))
-          = q''*b'-a')%Z as SIMPL.
-  { admit. }
-  rewrite SIMPL.
   destruct (Z_lt_dec a' (b' * q'')) as [LT | GE].
   { replace (b' * q'' >? a')%Z with true in QUOTIENT by lia.
+    unfold Int64.sub, Int64.mul.
+    fold a' b'.
+    replace q'' with (1 + a'/b')%Z by lia.
+    rewrite repr_unsigned_mul.
+    rewrite repr_unsigned_sub.
+    
+    replace ((1 + a' / b') * b' - a')%Z with (b' -  (a' - a' / b' * b'))%Z by ring.
+    rewrite <- MOD.
+    rewrite Int64.signed_repr ; cycle 1.
+    { change Int64.max_signed with 9223372036854775807%Z in *.
+      change Int64.min_signed with (-9223372036854775808)%Z in *.
+      lia.
+    }
     rewrite zlt_true by lia.
     replace q'' with (1 + (a' / b'))%Z by lia.
-    unfold Int64.add.
     apply Int64.eqm_samerepr.
     apply Int64.eqm_trans with (y := ((1 + a' / b') + (-1))%Z).
     { apply Int64.eqm_add.
@@ -1854,7 +1895,18 @@ Proof.
     replace (1 + a' / b' + -1)%Z with (a'/b')%Z by ring.
     apply Int64.eqm_refl.
   }
-  rewrite zlt_false by lia.
   replace (b' * q'' >? a')%Z with false in QUOTIENT by lia.
-  congruence.
-Admitted.
+  rewrite <- QUOTIENT.
+  unfold Int64.sub, Int64.mul.
+  fold a' b'.
+  rewrite repr_unsigned_mul.
+  rewrite repr_unsigned_sub.
+  replace (a' / b' * b' - a')%Z with (- (a' mod b'))%Z by lia.
+  rewrite Int64.signed_repr ; cycle 1.
+  { change Int64.max_signed with 9223372036854775807%Z in *.
+    change Int64.min_signed with (-9223372036854775808)%Z in *.
+    lia.
+  }
+  rewrite zlt_false by lia.
+  reflexivity.
+Qed.
-- 
cgit