Merge of Andrew Tolmach's HASP-related changes

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 52 insertions, 0 deletions

diff --git a/common/Memory.v b/common/Memory.v
index e1c68bd..059a27e 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -2817,6 +2817,41 @@ Proof.
   auto.
 Qed.
 
+Lemma drop_outside_inj: forall f m1 m2 b lo hi p m2',
+  mem_inj f m1 m2 -> 
+  drop_perm m2 b lo hi p = Some m2' -> 
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= lo 
+    \/ hi <= low_bound m1 b' + delta) ->
+  mem_inj f m1 m2'.
+Proof. 
+  intros. destruct H. constructor; intros.
+
+  (* access *)
+  inversion H2.
+  destruct (range_perm_in_bounds _ _ _ _ _ H3). 
+    pose proof (size_chunk_pos chunk). omega.
+  pose proof (mi_access0 b1 b2 delta chunk ofs p0 H H2). clear mi_access0 H2 H3. 
+  unfold valid_access in *.  intuition. clear H3. 
+  unfold range_perm in *. intros. 
+  eapply perm_drop_3; eauto.  
+  destruct (eq_block b2 b); subst; try (intuition; fail).  
+    destruct (H1 b1 delta H); intuition omega. 
+
+  (* memval *)
+  pose proof (mi_memval0 _ _ _ _  H H2). clear mi_memval0. 
+  unfold Mem.drop_perm in H0. 
+  destruct (Mem.range_perm_dec m2 b lo hi p); inversion H0; subst; clear H0. 
+  simpl.  unfold update.  destruct (zeq b2 b); subst; auto. 
+    pose proof (perm_in_bounds _ _ _ _ H2). 
+    destruct (H1 b1 delta H). 
+       destruct (zle lo (ofs + delta)); simpl; auto. exfalso; omega. 
+       destruct (zle lo (ofs + delta)); destruct (zlt (ofs + delta) hi); simpl; auto. 
+           exfalso; omega. 
+Qed.
+
+
 (** * Memory extensions *)
 
 (**  A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
@@ -3868,6 +3903,23 @@ Proof.
 Qed.
 *)
 
+Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2',
+  inject f m1 m2 -> 
+  drop_perm m2 b lo hi p = Some m2' -> 
+  (forall b' delta,
+    f b' = Some(b, delta) ->
+    high_bound m1 b' + delta <= lo 
+    \/ hi <= low_bound m1 b' + delta) ->
+  inject f m1 m2'.
+Proof.
+  intros. destruct H. constructor; eauto.
+  eapply drop_outside_inj; eauto.
+
+  intros.  unfold valid_block in *. erewrite nextblock_drop; eauto. 
+
+  intros.  erewrite bounds_drop; eauto. 
+Qed.
+
 (** Injecting a memory into itself. *)
 
 Definition flat_inj (thr: block) : meminj :=