Proof of ssem_exit_exclude_sabort - on avance !

1 files changed, 11 insertions, 41 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index 9978b3f3..fae3c557 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -136,9 +136,11 @@ Definition ssem_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (
  /\ ssem_local ge sp (si_elocal ext) rs m rs' m'
  /\ (si_ifso ext) = pc'.
 
+(* Either an abort on the condition evaluation OR an abort on the sistate_local IF the condition was true *)
 Definition sabort_exit (ge: RTL.genv) (sp: val) (ext: sistate_exit) (rs: regset) (m: mem) : Prop :=
-  seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = None
-  \/ sabort_local ge sp ext.(si_elocal) rs m.
+  let sev_cond := seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m in
+  sev_cond = None
+  \/ (sev_cond = Some true /\ sabort_local ge sp ext.(si_elocal) rs m).
 
 (** * Syntax and Semantics of symbolic internal state *)
 Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. 
@@ -394,39 +396,6 @@ Proof.
   - destruct H as (ext & lx & ALLFU & SABORT). inv ALLFU. eapply ssem_local_exclude_sabort_exit; eauto.
 Qed.
 
-(* Lemma ssem_exit_exclude_sabort_local ge sp st rs m rs' m' pc':
-  ssem_exit ge sp (si_exit st) rs m rs' m' pc' ->
-  all_fallthrough ge sp (si_exits st) rs m ->
-  sabort_local ge sp (si_local st) rs m ->
-  False.
-Proof.
- intros SIML ALLF ABORT.
- inv SIML.
- exploit ALLF; eauto.
- congruence.
-Qed. *)
-
-(* Lemma ssem_exits_exclude_sabort_exits ge sp exits rs m rs' m' pc':
-  ssem_exits ge sp exits rs m rs' m' pc' ->
-  sabort_exits ge sp exits rs m ->
-  False.
-Proof.
-  intros SIML ABORT.
-  inv SIML.
-  inv ABORT.
-Admitted. *)
-
-(* Lemma ssem_exits_exclude_sabort ge sp st rs m rs' m' pc':
-  ssem_exits ge sp (si_exits st) rs m rs' m' pc' ->
-  sabort ge sp st rs m ->
-  False.
-Proof.
-  intros SIME ABORT.
-  inv ABORT. 
-  - intuition. eapply ssem_exits_exclude_sabort_local; eauto.
-  - eapply ssem_exits_exclude_sabort_exits; eauto.
-Qed. *)
-
 Lemma ssem_exit_fallthrough_upto_exit ge sp ext ext' lx lx' exits rs m rs' m' pc':
   ssem_exit ge sp ext rs m rs' m' pc' ->
   all_fallthrough_upto_exit ge sp ext lx exits rs m ->
@@ -442,7 +411,7 @@ Lemma ssem_exit_exclude_sabort_exit ge sp ext rs m rs' m' pc':
 Proof.
   intros A B. destruct A as (A & A' & A''). inv B.
   - congruence.
-  - eapply ssem_local_exclude_sabort_local; eauto.
+  - destruct H as (_ & H). eapply ssem_local_exclude_sabort_local; eauto.
 Qed.
 
 Lemma ssem_exit_exclude_sabort ge sp ext st lx rs m rs' m' pc':
@@ -453,16 +422,17 @@ Lemma ssem_exit_exclude_sabort ge sp ext st lx rs m rs' m' pc':
 Proof.
   intros SSEM ALLFU ABORT.
   inv ABORT.
-  - admit. (* FIXME - we can have a sabort_local ; we don't have any ssem_local on si_local st ! *)
+  - destruct H as (ALLF & _). destruct ALLFU as (TAIL & _).
+    eapply is_tail_in in TAIL.
+    destruct SSEM as (SEVAL & _ & _).
+    eapply ALLF in TAIL. congruence.
   - destruct H as (ext' & lx' & ALLFU' & ABORT).
     exploit ssem_exit_fallthrough_upto_exit; eauto. intros ITAIL.
     destruct ALLFU as (ALLFU1 & ALLFU2). destruct ALLFU' as (ALLFU1' & ALLFU2').
     exploit (is_tail_cons_eq ext' ext lx' lx); eauto. intro. inv H.
     + eapply ssem_exit_exclude_sabort_exit; eauto.
-    + admit. 
-      (* we can prove we cannot abort on the seval_condition because ext' is in lx, and all_fallthrough lx
-         However, we run into the same issue as above for si_elocal *)
-Admitted.
+    + eapply ALLFU2 in H0. destruct ABORT as [ABORT | (ABORT & ABORT')]; congruence.
+Qed.
 
 Lemma ssem_exclude_sabort ge sp st rs m is:
   sabort ge sp st rs m ->