From 6ee0923290cca4782e6c863d752fb74c2c01df4f Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 17 Dec 2021 14:28:00 +0100
Subject: fpdivu

---
 kvx/SelectOpproof.v | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

(limited to 'kvx/SelectOpproof.v')

diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index a374ec54..658bf0b3 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1883,6 +1883,9 @@ Proof.
       destruct v2; simpl; trivial.
 Qed.
 
+
+Require FPDivision32.
+
 Theorem eval_platform_builtin:
   forall bf al a vl v le,
   platform_builtin bf al = Some a ->
@@ -1903,7 +1906,29 @@ Proof.
   - cbn in *;
       destruct vl; trivial. destruct vl; trivial.
       destruct v0; try discriminate;
-      cbn; rewrite H0; reflexivity.
+        cbn; rewrite H0; reflexivity.
+  - cbn in *.
+    intro EVAL.
+    inv EVAL. discriminate.
+    inv H0. discriminate.
+    inv H2. 2: discriminate.
+    inv Heval.
+    intro EVAL.
+    destruct v1; try discriminate.
+    destruct v0; try discriminate.
+    unfold Int.eq in EVAL.
+    change (Int.unsigned Int.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vint (Int.divu i i0)). split.
+    {
+      apply FPDivision32.fp_divu32_correct; auto.
+      pose proof (Int.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
 Qed.
 
 End CMCONSTR.
-- 
cgit