1 files changed, 105 insertions, 3 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index a7169881..45aa3343 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1533,6 +1533,70 @@ Proof.
   apply Val.swap_cmplu_bool.
 Qed.
 
+Lemma int_ltu_zero : forall i, Int.ltu i Int.zero = false.
+Proof.
+  intro.
+  unfold Int.ltu.
+  apply zlt_false.
+  rewrite Int.unsigned_zero.
+  pose proof (Int.unsigned_range i).
+  lia.
+Qed.
+
+Lemma cmpu_bool_Clt : forall pred v0 b,
+    Val.cmpu_bool pred Clt v0 (Vint Int.zero) = Some b -> b = false.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  inv CMP.
+  apply int_ltu_zero.
+Qed.
+
+Lemma cmpu_bool_Cge : forall pred v0 b,
+    Val.cmpu_bool pred Cge v0 (Vint Int.zero) = Some b -> b = true.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  inv CMP.
+  rewrite int_ltu_zero.
+  reflexivity.
+Qed.
+  
+Lemma int64_ltu_zero : forall i, Int64.ltu i Int64.zero = false.
+Proof.
+  intro.
+  unfold Int64.ltu.
+  apply zlt_false.
+  rewrite Int64.unsigned_zero.
+  pose proof (Int64.unsigned_range i).
+  lia.
+Qed.
+
+Lemma cmplu_bool_Clt : forall pred v0 b,
+    Val.cmplu_bool pred Clt v0 (Vlong Int64.zero) = Some b -> b = false.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  { inv CMP.
+    apply int64_ltu_zero.
+  }
+  repeat rewrite if_same in CMP.
+  discriminate.
+Qed.
+
+Lemma cmplu_bool_Cge : forall pred v0 b,
+    Val.cmplu_bool pred Cge v0 (Vlong Int64.zero) = Some b -> b = true.
+Proof.
+  intros until b. intro CMP.
+  destruct v0; cbn in CMP; try discriminate.
+  { inv CMP.
+    rewrite int64_ltu_zero.
+    reflexivity.
+  }
+  repeat rewrite if_same in CMP.
+  discriminate.
+Qed.
+
 Theorem eval_select: 
   forall le ty cond al vl a1 v1 a2 v2 a b,
   select ty cond al a1 a2 = Some a ->
@@ -1581,8 +1645,27 @@ Proof.
       simpl.
       change (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint Int.zero))
         with (eval_condition0 (Ccompu0 c) v0 m).
-      eapply eval_select0; eassumption.
-    }
+      destruct c.
+      all: try (eapply eval_select0; eassumption).
+      all: cbn.
+      all: cbn in HeC.
+      {
+      destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt v0 (Vint Int.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmpu_bool_Clt (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v2.
+      split; auto using Val.lessdef_normalize.
+      }
+      {
+      destruct (Val.cmpu_bool (Mem.valid_pointer m) Cge v0 (Vint Int.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmpu_bool_Cge (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v1.
+      split; auto using Val.lessdef_normalize.
+      }
+     }
     simpl.
     erewrite <- (bool_cond0_ne (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint x))).
     eapply eval_select0; repeat (try econstructor; try eassumption).
@@ -1609,7 +1692,26 @@ Proof.
       simpl.
       change (Val.cmplu_bool  (Mem.valid_pointer m) c v0 (Vlong Int64.zero))
       with (eval_condition0 (Ccomplu0 c) v0 m).
-      eapply eval_select0; eassumption.
+      destruct c.
+      all: try (eapply eval_select0; eassumption).
+      all: cbn.
+      all: cbn in HeC.
+      {
+      destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt v0 (Vlong Int64.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmplu_bool_Clt (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v2.
+      split; auto using Val.lessdef_normalize.
+      }
+      {
+      destruct (Val.cmplu_bool (Mem.valid_pointer m) Cge v0 (Vlong Int64.zero)) eqn:CMP; try discriminate.
+      inv HeC.
+      rewrite (cmplu_bool_Cge (Mem.valid_pointer m) v0 b CMP).
+      cbn.
+      exists v1.
+      split; auto using Val.lessdef_normalize.
+      }
     }
     simpl.
     erewrite <- (bool_cond0_ne (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong x))).