Merge branch 'kvx-work' into kvx-work-merge3.8

Conflicts:
	Makefile
	configure

2 files changed, 33 insertions, 0 deletions

diff --git a/common/Memory.v b/common/Memory.v
index cd8a2001..65f36966 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1322,6 +1322,18 @@ Proof.
   eapply load_store_same.
   eassumption.
 Qed.
+
+Theorem storev_preserv_valid (b : block) (ofs: Z): valid_pointer m1 b ofs = valid_pointer m2 b ofs.
+Proof.
+  unfold storev in STORE.
+  cut (valid_pointer m1 b ofs = true <-> valid_pointer m2 b ofs = true).
+  { destruct (valid_pointer _ _ _), (valid_pointer _ _ _); intuition congruence. }
+  destruct addr; try congruence.
+  rewrite! valid_pointer_valid_access. split.
+  - intros; eapply store_valid_access_1; eauto.
+  - intros; eapply store_valid_access_2; eauto.
+Qed.
+
 End STOREV.
 
 Lemma load_store_overlap:
diff --git a/common/Values.v b/common/Values.v
index 6401ba52..41138e8e 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -2706,3 +2706,24 @@ Proof.
   unfold compose_meminj; rewrite H1; rewrite H3; eauto.
   rewrite Ptrofs.add_assoc. decEq. unfold Ptrofs.add. apply Ptrofs.eqm_samerepr. auto with ints.
 Qed.
+
+
+(** Particular cases of extensionality lemma *)
+
+Lemma cmpu_bool_valid_pointer_eq vptr1 vptr2 c v1 v2:
+   (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) ->
+   Val.cmpu_bool vptr1 c v1 v2 = Val.cmpu_bool vptr2 c v1 v2.
+Proof.
+  intros EQ; unfold Val.cmpu_bool; destruct v1; try congruence;
+  destruct v2; try congruence;
+  rewrite !EQ; auto.
+Qed.
+
+Lemma cmplu_bool_valid_pointer_eq  vptr1 vptr2 c v1 v2:
+   (forall (b : block) (z : Z), vptr1 b z = vptr2 b z) ->
+   Val.cmplu_bool vptr1 c v1 v2 = Val.cmplu_bool vptr2 c v1 v2.
+Proof.
+  intros EQ; unfold Val.cmplu_bool; destruct v1; try congruence;
+  destruct v2; try congruence;
+  rewrite !EQ; auto.
+Qed.