modulos

1 files changed, 44 insertions, 0 deletions

diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index e6cce0fa..cffa2583 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1951,6 +1951,50 @@ Proof.
     }
     inv EVAL.
     constructor.
+  - 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.modu i i0)). split.
+    {
+      apply FPDivision32.fp_modu32_correct; auto.
+      pose proof (Int.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
+  - 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 Int64.eq in EVAL.
+    change (Int64.unsigned Int64.zero) with 0 in EVAL.
+    unfold zeq in EVAL.
+    destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ].
+    { discriminate. }
+    exists (Vlong (Int64.modu i i0)). split.
+    {
+      apply FPDivision64.fp_modu64_correct; auto.
+      pose proof (Int64.unsigned_range i0).
+      lia.
+    }
+    inv EVAL.
+    constructor.
 Qed.
 
 End CMCONSTR.