Proof of sisteps_correct_false

1 files changed, 31 insertions, 8 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index 2a8c4e3f..481c43da 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -432,7 +432,7 @@ Definition slocal_set_smem (st:sistate_local) (sm:smem) :=
 Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): option sistate :=
    Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}.
 
-(* FIXME - add notrap *)
+
 Definition sistep (i: instruction) (st: sistate): option sistate := 
   match i with
   | Inop pc' => 
@@ -718,18 +718,41 @@ Fixpoint sisteps (path:nat) (f: function) (st: sistate): option sistate :=
     sisteps p f st1
   end.
 
-Lemma sisteps_correct_false ge sp path f rs0 m0 st' is: 
+Lemma sist_set_local_preserves_si_exits st pc loc st':
+  sist_set_local st pc loc = Some st' ->
+  si_exits st' = si_exits st.
+Proof.
+  intros. inv H. simpl. reflexivity.
+Qed.
+
+Lemma sistep_preserves_allfu ge sp ext lx rs0 m0 st st' i:
+  all_fallthrough_upto_exit ge sp ext lx (si_exits st) rs0 m0 ->
+  sistep i st = Some st' ->
+  all_fallthrough_upto_exit ge sp ext lx (si_exits st') rs0 m0.
+Proof.
+  intros ALLFU SISTEP. destruct ALLFU as (ISTAIL & ALLF).
+  constructor; eauto.
+  destruct i; try discriminate; simpl in SISTEP; try (erewrite sist_set_local_preserves_si_exits; eauto; fail).
+  inv SISTEP. simpl. constructor. assumption.
+Qed.
+
+Lemma sisteps_correct_false ge sp f rs0 m0 st' is:
+  forall path,
   is.(icontinue)=false ->
-  forall st, ssem ge sp st rs0 m0 is -> 
+  forall st, ssem ge sp st rs0 m0 is ->
   sisteps path f st = Some st' ->
   ssem ge sp st' rs0 m0 is.
 Proof.
-  Local Hint Resolve sistep_preserves_ssem_exits: core.
-  intros CONT; unfold ssem; rewrite CONT.
   induction path; simpl.
-  + unfold sist_set_local; try_simplify_someHyps.
-  + intros st; inversion_SOME i.
-    inversion_SOME st1; eauto.
+  - intros. congruence.
+  - intros ICF st SSEM STEQ'.
+    destruct ((fn_code f) ! (si_pc st)) eqn:FIC; [|discriminate].
+    destruct (sistep _ _) eqn:SISTEP; [|discriminate].
+    eapply IHpath. 3: eapply STEQ'. eauto.
+    unfold ssem in SSEM. rewrite ICF in SSEM.
+    destruct SSEM as (ext & lx & SEXIT & ALLFU).
+    unfold ssem. rewrite ICF. exists ext, lx.
+    constructor; auto. eapply sistep_preserves_allfu; eauto.
 Qed.
 
 Lemma sisteps_preserves_sabort ge sp path f rs0 m0 st': forall st,