exec_basic_simulation proof OK

1 files changed, 23 insertions, 32 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index f0350628..b26e8d4c 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1245,45 +1245,36 @@ Proof.
     destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto;
     simpl in *; inv_matchi; find_rwrt_ag. }
   { (* Pallocframe *)
-    monadInv TRANSBI.
-    simpl in *.
-    inversion MATCHI; subst;
-    destruct Mem.alloc;
-    destruct Mem.store in BASIC;
-    inversion BASIC; subst; clear BASIC.
-    destruct Mem.store.
-    (* TODO find a way to complete this proof *)
-    + eexists; eexists; split; eauto.
-      repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]).
-      pc_not_sp.
-      -- econstructor; eauto.
-         all:admit.
-      -- eapply AG; pc_not_sp.
-    + repeat (econstructor; eauto).
-      admit.
-      
-    (* TODO *)
-    all:admit. }
+    monadInv TRANSBI;
+    inv_matchi; try pc_not_sp;
+    destruct sz eqn:EQSZ;
+    destruct Mem.alloc eqn:EQALLOC;
+    destruct Mem.store eqn:EQSTORE; inversion BASIC; try pc_not_sp;
+    eexists; eexists; split; eauto;
+    repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]);
+    try (econstructor; eauto);
+    try (eapply nextinstr_agree_but_pc; eauto);
+    try (eapply ptrofs_nextinstr_agree; eauto). }
   { (* Pfreeframe *)
-    (* TODO seems similar as the above subcase *)
-    monadInv TRANSBI.
-    simpl in *.
-    inversion MATCHI; subst;
-    destruct Mem.loadv in BASIC;
-    inversion BASIC; subst; clear BASIC.
-    destruct Mem.loadv.
-    (* TODO find a way to complete this proof *)
-    + eexists; eexists; split; eauto.
-      repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]).
-      all:admit.
-    + all:admit. }
+    monadInv TRANSBI;
+    inv_matchi; try pc_not_sp;
+    destruct sz eqn:EQSZ;
+    destruct Mem.loadv eqn:EQLOAD;
+    destruct (rs1 SP) eqn:EQRS1SP;
+    try (destruct Mem.free eqn:EQFREE);
+    inversion BASIC; try pc_not_sp;
+    eexists; eexists; split; eauto;
+    repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]);
+    try (econstructor; eauto);
+    try (eapply nextinstr_agree_but_pc; eauto);
+    try (eapply ptrofs_nextinstr_agree; eauto). }
   1,2,3,4: (* Ploadsymbol, Pcvtsw2x, Pcvtuw2x, Pcvtx2w *)
     try (monadInv TRANSBI);
     try (inv_matchi);
     try (exploit next_inst_preserved; eauto);
     rewrite symbol_addresses_preserved; eauto;
     try (find_rwrt_ag).
-Admitted.
+Qed.
 
 Lemma exec_body_simulation_star': forall
   b ofs f bb tc bis end_of_body rs_start m_start s_start rs_end m_end