diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/Memory.v | 12 |
1 files changed, 12 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: |