From 6af8f4275f7f9572d4d0783818cbfb85357807c6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 2 Mar 2020 13:17:54 +0100
Subject: loadv_storev_same

---
 common/Memory.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'common')

diff --git a/common/Memory.v b/common/Memory.v
index b68a5049..89b920b3 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -1169,6 +1169,24 @@ Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
 Local Hint Resolve store_valid_access_1 store_valid_access_2
              store_valid_access_3: mem.
 
+
+Section STOREV.
+Variable chunk: memory_chunk.
+Variable m1: mem.
+Variables addr v: val.
+Variable m2: mem.
+Hypothesis STORE: storev chunk m1 addr v = Some m2.
+
+
+Theorem loadv_storev_same:
+  loadv chunk m2 addr = Some (Val.load_result chunk v).
+Proof.
+  destruct addr; simpl in *; try discriminate.
+  eapply load_store_same.
+  eassumption.
+Qed.
+End STOREV.
+
 Lemma load_store_overlap:
   forall chunk m1 b ofs v m2 chunk' ofs' v',
   store chunk m1 b ofs v = Some m2 ->
-- 
cgit