full_div_longu_correct

1 files changed, 28 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index bf9be23d..4e91b853 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1982,6 +1982,8 @@ Lemma full_div_longu_correct :
            (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.
+
+  Local Opaque anystep_div_longu.
   intros.
   unfold full_div_longu.
   cbn.
@@ -2023,5 +2025,29 @@ Proof.
     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 anystep_div_longu_correct.
+    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.div_1_r.
+  unfold a'.
+  rewrite Int64.repr_unsigned.
+  reflexivity.
+Qed.