From f503e4287bc76150fd3ec5be8c076bf734361493 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Mar 2020 17:56:53 +0100
Subject: ported to arm

---
 arm/CSE2depsproof.v | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'arm')

diff --git a/arm/CSE2depsproof.v b/arm/CSE2depsproof.v
index 2112a230..61fe5980 100644
--- a/arm/CSE2depsproof.v
+++ b/arm/CSE2depsproof.v
@@ -34,9 +34,8 @@ Section MEMORY_WRITE.
   Variable chunkw chunkr : memory_chunk.
   Variable base : val.
   
-  Variable addrw addrr valw valr : val.
+  Variable addrw addrr valw : val.
   Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
-  Hypothesis READ : Mem.loadv chunkr m addrr = Some valr.
 
   Section INDEXED_AWAY.
   Variable ofsw ofsr : int.
@@ -50,7 +49,7 @@ Section MEMORY_WRITE.
     forall RANGER : 0 <= Int.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
     forall SWAPPABLE :    Int.unsigned ofsw + size_chunk chunkw <= Int.unsigned ofsr
                        \/ Int.unsigned ofsr + size_chunk chunkr <= Int.unsigned ofsw,
-    Mem.loadv chunkr m2 addrr = Some valr.
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
   Proof.
     intros.
     
@@ -62,7 +61,6 @@ Section MEMORY_WRITE.
     simpl in *.
     inv ADDRR.
     inv ADDRW.
-    rewrite <- READ.
     destruct base; try discriminate.
     eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
     exact STORE.
@@ -83,7 +81,7 @@ Section MEMORY_WRITE.
   
   Theorem load_store_away :
     can_swap_accesses_ofs (Int.unsigned ofsr) chunkr (Int.unsigned ofsw) chunkw = true ->
-    Mem.loadv chunkr m2 addrr = Some valr.
+    Mem.loadv chunkr m2 addrr =  Mem.loadv chunkr m addrr.
   Proof.
     intro SWAP.
     unfold can_swap_accesses_ofs in SWAP.
@@ -105,16 +103,15 @@ Section SOUNDNESS.
 
 Lemma may_overlap_sound:
   forall m m' : mem,
-  forall chunk addr args chunk' addr' args' v a a' vl rs,
+  forall chunk addr args chunk' addr' args' v a a' rs,
     (eval_addressing genv sp addr (rs ## args)) = Some a ->
     (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
     (may_overlap chunk addr args chunk' addr' args') = false ->
     (Mem.storev chunk m a v) = Some m' ->
-    (Mem.loadv chunk' m  a') = Some vl ->
-    (Mem.loadv chunk' m' a') = Some vl.
+    (Mem.loadv chunk' m'  a') = (Mem.loadv chunk' m a').
 Proof.
   intros until rs.
-  intros ADDR ADDR' OVERLAP STORE LOAD.
+  intros ADDR ADDR' OVERLAP STORE.
   destruct addr; destruct addr'; try discriminate.
   { (* Aindexed / Aindexed *)
   destruct args as [ | base [ | ]]. 1,3: discriminate.
-- 
cgit