Moved some theorems

4 files changed, 101 insertions, 113 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 91e5ac89..cce180ac 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -294,6 +294,31 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
      end
   end.
 
+
+Theorem builtin_body_nil:
+  forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
+Proof.
+  intros. destruct bb as [hd bdy ex WF]. simpl in *.
+  apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
+  eapply H1; eauto.
+Qed.
+
+Theorem exec_body_app:
+  forall l l' rs m rs'' m'',
+  exec_body (l ++ l') rs m = Next rs'' m'' ->
+  exists rs' m',
+       exec_body l rs m = Next rs' m'
+    /\ exec_body l' rs' m' = Next rs'' m''.
+Proof.
+  induction l.
+  - intros. simpl in H. repeat eexists. auto.
+  - intros. rewrite <- app_comm_cons in H. simpl in H.
+    destruct (exec_basic_instr a rs m) eqn:EXEBI.
+    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
+      repeat eexists. simpl. rewrite EXEBI. eauto. auto.
+    + discriminate.
+Qed.
+
 (** Position corresponding to a label *)
 
 Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := par_goto_label f lbl rs rs m.
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index e130df45..220ae08b 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1353,19 +1353,6 @@ Proof.
     rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.
 Qed.
 
-Lemma exec_body_pc:
-  forall l rs1 m1 rs2 m2,
-  exec_body tge l rs1 m1 = Next rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  induction l.
-  - intros. inv H. auto.
-  - intros until m2. intro EXEB.
-    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
-    eapply IHl in H0. rewrite H0.
-    erewrite exec_basic_instr_pc; eauto.
-Qed.
-
 Lemma exec_body_control:
   forall b rs1 m1 rs2 m2 rs3 m3 fn,
   exec_body tge (body b) rs1 m1 = Next rs2 m2 ->
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index 07c445e2..d2450a9a 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -752,6 +752,82 @@ Proof.
   intros. destruct H. auto.
 Qed.
 
+Ltac Simplif :=
+  ((rewrite nextblock_inv by eauto with asmgen)
+  || (rewrite nextblock_inv1 by eauto with asmgen)
+  || (rewrite Pregmap.gss)
+  || (rewrite nextblock_pc)
+  || (rewrite Pregmap.gso by eauto with asmgen)
+  ); auto with asmgen.
+
+Ltac Simpl := repeat Simplif.
+
+Theorem exec_basic_instr_pc:
+  forall ge b rs1 m1 rs2 m2,
+  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  intros. destruct b; try destruct i; try destruct i.
+  all: try (inv H; Simpl).
+  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+
+  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+
+  { (* PLoadQRRO *)
+    unfold  parexec_load_q_offset in H1.
+    destruct (gpreg_q_expand _) as [r0 r1] in H1.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    inv H1. Simpl. }
+  { (* PLoadORRO *)
+    unfold  parexec_load_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    inv H1. Simpl. }
+  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
+  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
+  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
+  
+  { (* PStoreQRRO *)
+    unfold  parexec_store_q_offset in H1.
+    destruct (gpreg_q_expand _) as [r0 r1] in H1.
+    unfold eval_offset in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity. }
+  { (* PStoreORRO *)
+    unfold  parexec_store_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    unfold eval_offset in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity. }
+  - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
+  - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
+    destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
+  - destruct rs; try discriminate. inv H1. Simpl.
+  - destruct rd; try discriminate. inv H1; Simpl.
+  - reflexivity.
+Qed.
+
+Lemma exec_body_pc:
+  forall ge l rs1 m1 rs2 m2,
+  exec_body ge l rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  induction l.
+  - intros. inv H. auto.
+  - intros until m2. intro EXEB.
+    inv EXEB. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate.
+    eapply IHl in H0. rewrite H0.
+    erewrite exec_basic_instr_pc; eauto.
+Qed.
+
 Section STRAIGHTLINE.
 
 Variable ge: genv.
@@ -880,69 +956,6 @@ Qed.
 
 (** Linking exec_straight with exec_straight_blocks *)
 
-Ltac Simplif :=
-  ((rewrite nextblock_inv by eauto with asmgen)
-  || (rewrite nextblock_inv1 by eauto with asmgen)
-  || (rewrite Pregmap.gss)
-  || (rewrite nextblock_pc)
-  || (rewrite Pregmap.gso by eauto with asmgen)
-  ); auto with asmgen.
-
-Ltac Simpl := repeat Simplif.
-
-Lemma exec_basic_instr_pc:
-  forall b rs1 m1 rs2 m2,
-  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  intros. destruct b; try destruct i; try destruct i.
-  all: try (inv H; Simpl).
-  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  { (* PLoadQRRO *)
-    unfold  parexec_load_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  { (* PLoadORRO *)
-    unfold  parexec_load_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
-  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  
-  { (* PStoreQRRO *)
-    unfold  parexec_store_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  { (* PStoreORRO *)
-    unfold  parexec_store_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
-    destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct rs; try discriminate. inv H1. Simpl.
-  - destruct rd; try discriminate. inv H1; Simpl.
-  - reflexivity.
-Qed.
-
 Lemma exec_straight_pc:
   forall c c' rs1 m1 rs2 m2,
   exec_straight c rs1 m1 c' rs2 m2 ->
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 867c10c5..cdf8829f 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -30,43 +30,6 @@ Proof.
   intros. eapply match_transform_partial_program; eauto.
 Qed.
 
-Remark builtin_body_nil:
-  forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
-Proof.
-  intros. destruct bb as [hd bdy ex WF]. simpl in *.
-  apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
-  eapply H1; eauto.
-Qed.
-
-Lemma exec_body_app:
-  forall l l' ge rs m rs'' m'',
-  exec_body ge (l ++ l') rs m = Next rs'' m'' ->
-  exists rs' m',
-       exec_body ge l rs m = Next rs' m'
-    /\ exec_body ge l' rs' m' = Next rs'' m''.
-Proof.
-  induction l.
-  - intros. simpl in H. repeat eexists. auto.
-  - intros. rewrite <- app_comm_cons in H. simpl in H.
-    destruct (exec_basic_instr ge a rs m) eqn:EXEBI.
-    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
-      repeat eexists. simpl. rewrite EXEBI. eauto. auto.
-    + discriminate.
-Qed.
-
-Lemma exec_body_pc:
-  forall l ge rs1 m1 rs2 m2,
-  exec_body ge l rs1 m1 = Next rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  induction l.
-  - intros. inv H. auto.
-  - intros until m2. intro EXEB.
-    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
-    eapply IHl in H0. rewrite H0.
-    erewrite exec_basic_instr_pc; eauto.
-Qed.
-
 Lemma next_eq:
   forall (rs rs': regset) m m',
   rs = rs' -> m = m' -> Next rs m = Next rs' m'.