Preliminaries: minor extensions to Memory

- Make Mem.unchanged_on transitive.
- Add Mem.drop_perm_unchanged_on.

1 files changed, 58 insertions, 3 deletions

diff --git a/common/Memory.v b/common/Memory.v
index 93d0e432..0ea9e3b0 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -4143,6 +4143,8 @@ Section UNCHANGED_ON.
 Variable P: block -> Z -> Prop.
 
 Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
+  unchanged_on_nextblock:
+    Ple (nextblock m_before) (nextblock m_after);
   unchanged_on_perm:
     forall b ofs k p,
     P b ofs -> valid_block m_before b ->
@@ -4157,15 +4159,22 @@ Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
 Lemma unchanged_on_refl:
   forall m, unchanged_on m m.
 Proof.
-  intros; constructor; tauto.
+  intros; constructor. apply Ple_refl. tauto. tauto.
+Qed.
+
+Lemma valid_block_unchanged_on:
+  forall m m' b,
+  unchanged_on m m' -> valid_block m b -> valid_block m' b.
+Proof.
+  unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega.
 Qed.
 
 Lemma perm_unchanged_on:
   forall m m' b ofs k p,
-  unchanged_on m m' -> P b ofs -> valid_block m b ->
+  unchanged_on m m' -> P b ofs ->
   perm m b ofs k p -> perm m' b ofs k p.
 Proof.
-  intros. destruct H. apply unchanged_on_perm0; auto.
+  intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. 
 Qed.
 
 Lemma perm_unchanged_on_2:
@@ -4176,6 +4185,17 @@ Proof.
   intros. destruct H. apply unchanged_on_perm0; auto.
 Qed.
 
+Lemma unchanged_on_trans:
+  forall m1 m2 m3, unchanged_on m1 m2 -> unchanged_on m2 m3 -> unchanged_on m1 m3.
+Proof.
+  intros; constructor.
+- apply Ple_trans with (nextblock m2); apply unchanged_on_nextblock; auto.
+- intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto.
+  eapply valid_block_unchanged_on; eauto.
+- intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto.
+  eapply perm_unchanged_on; eauto. 
+Qed.
+
 Lemma loadbytes_unchanged_on_1:
   forall m m' b ofs n,
   unchanged_on m m' ->
@@ -4243,6 +4263,7 @@ Lemma store_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_store _ _ _ _ _ _ H). apply Ple_refl.
 - split; intros; eauto with mem.
 - erewrite store_mem_contents; eauto. rewrite PMap.gsspec.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
@@ -4259,6 +4280,7 @@ Lemma storebytes_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_storebytes _ _ _ _ _ H). apply Ple_refl.
 - split; intros. eapply perm_storebytes_1; eauto. eapply perm_storebytes_2; eauto.
 - erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
@@ -4273,6 +4295,7 @@ Lemma alloc_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_alloc _ _ _ _ _ H). apply Ple_succ.
 - split; intros.
   eapply perm_alloc_1; eauto.
   eapply perm_alloc_4; eauto.
@@ -4288,6 +4311,7 @@ Lemma free_unchanged_on:
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
+- rewrite (nextblock_free _ _ _ _ _ H). apply Ple_refl.
 - split; intros.
   eapply perm_free_1; eauto.
   destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto.
@@ -4297,8 +4321,39 @@ Proof.
   simpl. auto.
 Qed.
 
+Lemma drop_perm_unchanged_on:
+  forall m b lo hi p m',
+  drop_perm m b lo hi p = Some m' ->
+  (forall i, lo <= i < hi -> ~ P b i) ->
+  unchanged_on m m'.
+Proof.
+  intros; constructor; intros.
+- rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl.
+- split; intros. eapply perm_drop_3; eauto.
+  destruct (eq_block b0 b); auto.
+  subst b0. 
+  assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. }
+  right; omega.
+  eapply perm_drop_4; eauto. 
+- unfold drop_perm in H. 
+  destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto.
+Qed. 
+
 End UNCHANGED_ON.
 
+Lemma unchanged_on_implies:
+  forall (P Q: block -> Z -> Prop) m m',
+  unchanged_on P m m' ->
+  (forall b ofs, Q b ofs -> valid_block m b -> P b ofs) ->
+  unchanged_on Q m m'.
+Proof.
+  intros. destruct H. constructor; intros.
+- auto.
+- apply unchanged_on_perm0; auto. 
+- apply unchanged_on_contents0; auto. 
+  apply H0; auto. eapply perm_valid_block; eauto. 
+Qed.
+
 End Mem.
 
 Notation mem := Mem.mem.