Reverting change to sistate

1 files changed, 7 insertions, 39 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index c503936b..66e23cd8 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -112,25 +112,15 @@ Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop :=
 
 Inductive simatch_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop :=
   simatch_exits_intro: forall ext lx',
-    lx = ext::lx' ->
+    is_tail (ext::lx') lx ->
     all_fallthrough ge sp lx' rs m ->
     seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true ->
     simatch_local ge sp (si_elocal ext) rs m rs' m' ->
     (si_ifso ext) = pc' ->
     simatch_exits ge sp lx rs m rs' m' pc'.
 
-(* Ensuring there isn't more sistate_local after taking a branch *)
-Inductive simatch_exits_bind (ext: sistate_exit) (loc: sistate_local) : Prop :=
-  simatch_exits_bind_intro:
-    (forall ge sp lx rs m rs' m' pc', simatch_exits ge sp (ext::lx) rs m rs' m' pc' -> si_elocal ext = loc) ->
-    simatch_exits_bind ext loc.
-
-Definition sistate_wf exits loc :=
-  exists ext lx, exits = ext::lx /\ simatch_exits_bind ext loc.
-
 (** * Syntax and Semantics of symbolic internal state *)
-Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local;
-                    si_wf: sistate_wf si_exits si_local }. 
+Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. 
 
 Definition simatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop :=
   if (is.(icontinue)) 
@@ -185,7 +175,7 @@ Proof.
   Local Hint Resolve is_tail_in: core.
   destruct 1 as [ext lx' lc NYE' EVAL SEM PC]. subst.
   unfold all_fallthrough; intros NYE; rewrite NYE in EVAL; eauto.
-  try congruence. rewrite lc. econstructor; eauto.
+  try congruence. (*  rewrite lc. econstructor; eauto. *)
 Qed.
 
 Lemma simatch_exclude_incompatible_continue ge sp st rs m is1 is2:
@@ -257,8 +247,8 @@ Proof.
   Local Hint Resolve exit_cond_determ eq_sym: core.
   destruct 1 as [ext1 lx1 TAIL1 NYE1 EVAL1 SEM1 PC1]; subst.
   destruct 1 as [ext2 lx2 TAIL2 NYE2 EVAL2 SEM2 PC2]; subst.
-  assert (X:ext1=ext2) by congruence.
-(*{ destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. } *)
+  assert (X:ext1=ext2).
+  { destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. }
   subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto.
 Qed.
 
@@ -315,36 +305,14 @@ Lemma simatch_exits_exclude_sabort_local ge sp st rs m rs' m' pc':
   sabort_local ge sp (si_local st) rs m ->
   False.
 Proof.
-  destruct st as [spc exits loc SISTWF]. simpl.
-  intros SIMEX ABORT. inv SISTWF. inv H. inv H0.
-  inversion SIMEX. subst. inv H.
-  inv H1. eapply H in SIMEX. subst. clear H.
-  inv H3. destruct H1 as (H1 & H1').
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
-Qed.
-
-(* Weaker version if we don't have the simatch_exits_bind - not used anymore, couldn't get any use from it *)
-Remark simatch_exits_exclude_sabort_local' ge sp rs m rs' m' pc' exits ext:
-  simatch_exits ge sp (ext::exits) rs m rs' m' pc' ->
-  sabort_local ge sp (si_elocal ext) rs m ->
-  False.
-Proof.
-  intros SIMEX ABORT.
-  inv SIMEX. inv H. inv H2. destruct H3 as (H3 & H3').
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
-Qed.
+Admitted.
 
 Lemma simatch_exits_exclude_sabort_exits ge sp exits rs m rs' m' pc':
   simatch_exits ge sp exits rs m rs' m' pc' ->
   sabort_exits ge sp exits rs m ->
   False.
 Proof.
-  intros SIMEX ABORT.
-  inv ABORT. inv H. inv SIMEX. unfold all_fallthrough in H2.
-  inv H0.
-  - congruence.
-  - apply H2 in H. congruence.
-Qed.
+Admitted.
 
 Lemma simatch_exits_exclude_sabort ge sp st rs m rs' m' pc':
   simatch_exits ge sp (si_exits st) rs m rs' m' pc' ->