comment out theorem that cannot be proved

1 files changed, 33 insertions, 29 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index c54cc317..4d53763c 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -212,6 +212,12 @@ Definition store_eval (so: store_op) (l: list value) :=
 
 Local Open Scope Z.
 
+Remark size_chunk_positive: forall chunk,
+    (size_chunk chunk) > 0.
+Proof.
+  destruct chunk; simpl; lia.
+Qed.
+
 Definition disjoint_chunks
            (ofs1 : offset) (chunk1 : memory_chunk)
            (ofs2 : offset) (chunk2 : memory_chunk) :=
@@ -220,56 +226,54 @@ Definition disjoint_chunks
                 ((Ptrofs.unsigned ofs2),
                  ((Ptrofs.unsigned ofs2) + (size_chunk chunk2))).
 
-Definition same_memory (m m' : mem) :=
-  forall chunk block ofs,
-    (Mem.load chunk m block ofs) = (Mem.load chunk m' block ofs).
-
+(* THIS CANNOT BE PROVED DUE TO OVERFLOW WRAPPING
 (* use something like load_store_other *)
 Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m0' m1 m2 m1' m2',
     (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) ->
-    same_memory m0 m0' ->
     store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) ->
     store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) ->
     store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0'] = Some (Memstate m1') ->
     store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m1'] = Some (Memstate m2') ->
-    same_memory m2 m2'.
+    m2 = m2'.
 Proof.
   intros until m2'.
-  intros NO_OVERLAP SAME STORE0 STORE1 STORE0' STORE1'.
-  unfold same_memory.
-  intros rchunk rblock rofs.
-  unfold disjoint_chunks in NO_OVERLAP.
+  intros DISJOINT STORE0 STORE1 STORE0' STORE1'.
+  unfold disjoint_chunks in DISJOINT.
   destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence.
   destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence.
   destruct va as [base | ]; try congruence.
   unfold exec_store_deps_offset in *.
   destruct Ge.
-  destruct (eval_offset ofs1) as [ i1 |]; try congruence.
-  destruct (eval_offset ofs2) as [ i2 |]; try congruence.
+  unfold eval_offset in *; simpl in *.
   unfold Mem.storev in *.
   unfold Val.offset_ptr in *.
   destruct base as [ | | | | | wblock wpofs] in * ; try congruence.
-  destruct (Mem.store (store_chunk n1) m0 _ _ _) eqn:HS0; try congruence.
+  destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence.
   inv STORE0.
-  destruct (Mem.store (store_chunk n2) m1 _ _ _) eqn:HS1; try congruence.
+  destruct (Mem.store _ _ _ _) eqn:E1 in STORE1; try congruence.
   inv STORE1.
-  destruct (Mem.store (store_chunk n2) m0' _ _ _) eqn:HS0'; try congruence.
+  destruct (Mem.store _ _ _ _) eqn:E0' in STORE0'; try congruence.
   inv STORE0'.
-  destruct (Mem.store (store_chunk n1) m1' _ _ _) eqn:HS1'; try congruence.
+  destruct (Mem.store _ _ _ _) eqn:E1' in STORE1'; try congruence.
   inv STORE1'.
-  destruct (eq_block rblock wblock) as [SAME_BLOCK | DIF_BLOCKS].
-  { subst rblock.
-    admit.
-  }
-  { (* read from different base block *)
-  rewrite (Mem.load_store_other (store_chunk n2) m1 wblock (Ptrofs.unsigned (Ptrofs.add wpofs i2)) v2 m2 HS1) by tauto.
-  rewrite (Mem.load_store_other (store_chunk n1) m0 wblock (Ptrofs.unsigned (Ptrofs.add wpofs i1)) v1 m1 HS0) by tauto.
-  rewrite (Mem.load_store_other (store_chunk n1) m1' wblock (Ptrofs.unsigned (Ptrofs.add wpofs i1)) v1 m2' HS1') by tauto.
-  rewrite (Mem.load_store_other (store_chunk n2) m0' wblock (Ptrofs.unsigned (Ptrofs.add wpofs i2)) v2 m1' HS0') by tauto.
-  apply SAME.
-  }
-Admitted.
-  
+  assert (Some m2 = Some m2').
+  2: congruence.
+  rewrite <- E1.
+  rewrite <- E1'.
+  eapply Mem.store_store_other.
+  {
+    right.
+    pose proof (size_chunk_positive (store_chunk n1)).
+    pose proof (size_chunk_positive (store_chunk n2)).
+    destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]];
+      unfold Intv.empty in DIS; simpl in DIS.
+    1, 2: lia.
+    destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1;
+    destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2;
+    try lia.    
+   }
+*)
+
 Definition goto_label_deps (f: function) (lbl: label) (vpc: val) :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => None