fix for aarch64

1 files changed, 9 insertions, 11 deletions

diff --git a/aarch64/CSE2depsproof.v b/aarch64/CSE2depsproof.v
index e20824e3..4aac23af 100644
--- a/aarch64/CSE2depsproof.v
+++ b/aarch64/CSE2depsproof.v
@@ -32,9 +32,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 : int64.
@@ -48,7 +47,7 @@ Section MEMORY_WRITE.
     forall RANGER : 0 <= Int64.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
     forall SWAPPABLE :    Int64.unsigned ofsw + size_chunk chunkw <= Int64.unsigned ofsr
                        \/ Int64.unsigned ofsr + size_chunk chunkr <= Int64.unsigned ofsw,
-    Mem.loadv chunkr m2 addrr = Some valr.
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
   Proof.
     intros.
     
@@ -60,7 +59,7 @@ 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.
@@ -80,8 +79,8 @@ Section MEMORY_WRITE.
   Qed.
   
   Theorem load_store_away :
-    can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true ->
-    Mem.loadv chunkr m2 addrr = Some valr.
+    can_swap_accesses_ofs (Int64.unsigned ofsr) chunkr (Int64.unsigned ofsw) chunkw = true ->
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
   Proof.
     intro SWAP.
     unfold can_swap_accesses_ofs in SWAP.
@@ -103,16 +102,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.
@@ -120,7 +118,7 @@ Proof.
   simpl in OVERLAP.
   destruct (peq base base'). 2: discriminate.
   subst base'.
-  destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
+  destruct (can_swap_accesses_ofs (Int64.unsigned ofs0) chunk' (Int64.unsigned ofs) chunk) eqn:SWAP.
   2: discriminate.
   simpl in *.
   eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.