1 files changed, 10 insertions, 0 deletions
diff --git a/kvx/Op.v b/kvx/Op.v
index 794bc87b..f9501485 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -1238,6 +1238,16 @@ Proof.
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma cond_valid_pointer_eq:
+  forall cond args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence.
+  all: repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 Lemma op_valid_pointer_eq:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->