proof of consistante on_enter & on_exit call

src/verification/FPSProp.v

@@ -836,6 +836,759 @@ Module FPS_PROP (EVAL_Def: EVAL_ENV)
   
     End stableFPS.
 
+    Section On_Enter_Exit_Verif.
+
+    (** * Proof that on_enter and on_exit are when changing block : *)
+    (** one of the new functionality of the VFPG is on_enter and on_exit
+      code taht are run when a block is enter or exit. we will prove that
+      theses codes are indeed executed if needed*)
+      
+    Lemma test_forbidden_deroute_add_trace :
+      forall e id1 id2 fb res e2,
+      Common_Sem.test_forbidden_deroute e id1 id2 fb = (res, e2) ->
+      exists (t' : fp_trace),
+      get_trace e2 = get_trace e ++ t'.
+    Proof.
+      intros e id1 id2 fb res e2.
+      rewrite /Common_Sem.test_forbidden_deroute /evalc.
+      destruct (_ && _).
+      - destruct (get_fbd_only_when _).
+        + intros H; eexists ; by inversion H.
+        + intros H; exists (nil)%list; inversion H. apply app_nil_end.
+      - intros H; exists (nil)%list; inversion H. apply app_nil_end.
+    Qed.
+      
+    Lemma test_forbidden_deroutes_add_trace :
+      forall e id1 id2 fbs res e2,
+      Common_Sem.test_forbidden_deroutes e id1 id2 fbs = (res, e2) ->
+      exists (t' : fp_trace),
+      get_trace e2 = get_trace e ++ t'.
+    Proof.
+      intros e id1 id2 fbs. generalize dependent e.
+      induction fbs.
+      - simpl.
+        intros e res e2 H; inversion H.
+        exists nil. apply app_nil_end.
+      - simpl.
+        intros e res e2.
+        destruct (Common_Sem.test_forbidden_deroute _ _ _ _)
+          as [b e1] eqn:Testfb.
+        destruct (test_forbidden_deroute_add_trace _ _ _ _ Testfb)
+          as [t' Ht].
+        destruct b. 
+        + intros H; inversion H; subst.
+          by exists t'.
+
+        + intros H.
+          destruct (IHfbs _ _ _ H) as [t'' Ht'].
+          exists (t' ++ t''). rewrite Ht' Ht.
+          by rewrite app_assoc.
+    Qed.
+      
+    Lemma forbidden_deroute_add_trace :
+      forall e id res e2,
+      Common_Sem.forbidden_deroute (` (` fps)) e id = (res, e2) ->
+      exists (t' : fp_trace),
+      get_trace e2 = get_trace e ++ t'.
+    Proof.
+      intros e id res e2.
+      rewrite /Common_Sem.forbidden_deroute.
+      apply test_forbidden_deroutes_add_trace.
+    Qed.
+
+    Lemma goto_block_add_trace :
+      forall e id e2,
+      Common_Sem.goto_block (` (` fps)) e id =  e2 ->
+      exists (t' : fp_trace),
+      get_trace e2 = get_trace e ++ t'.
+    Proof.
+      intros e id e2.
+      rewrite /Common_Sem.goto_block.
+      destruct (Common_Sem.forbidden_deroute _ _ _)
+        as [res e1] eqn:fb.
+      destruct (forbidden_deroute_add_trace _ _ fb) as [t' Ht].
+      destruct res.
+      - intros H; subst; by exists t'.
+      - intros H; subst.
+        rewrite /change_block.
+        destruct (_ =? _); simpl;
+        eexists; rewrite Ht; by rewrite <- app_assoc.
+    Qed.
+
+    Lemma test_exception_add_trace :
+      forall e ex res e2,
+      Common_Sem.test_exception (` (` fps)) e ex = (res, e2) ->
+      exists (t' : fp_trace),
+      get_trace e2 = get_trace e ++ t'.
+    Proof.
+      intros e ex res e2.
+      rewrite /Common_Sem.test_exception /evalc.
+      destruct (_ =? _).
+      - intros H; eexists; inversion H; by apply app_nil_end.
+      - destruct (~~ EVAL_Def.eval _ _).
+        + intros H; eexists; by inversion H.
+        + intros H; inversion H; rewrite H2.
+          destruct (goto_block_add_trace _ _ H2) as [t' Ht].
+          eexists. simpl in Ht.
+          repeat rewrite <- app_assoc in Ht.
+          apply Ht.
+    Qed.
+    
+    Lemma test_exceptions_add_trace :
+      forall e lex res e2,
+      Common_Sem.test_exceptions (` (` fps)) e lex = (res, e2) ->
+      exists (t' : fp_trace),
+      get_trace e2 = get_trace e ++ t'.
+    Proof.
+      intros e lex. generalize dependent e.
+      induction lex; intros e.
+      - simpl. intros res e2 H; exists nil.
+        inversion H. apply app_nil_end.
+      - simpl.
+        destruct (Common_Sem.test_exception _ _ _) as [b e'] eqn:Test.
+        destruct (test_exception_add_trace _ _ Test) as [t' Ht].
+        destruct b. 
+        + intros res e2 H; eexists; inversion H; subst. apply Ht.
+        + intros res e2 H.
+          destruct (IHlex _ _ _ H) as [t'' Ht'].
+          exists (t' ++ t''). rewrite Ht' Ht .
+          by rewrite app_assoc.
+    Qed.
+
+    Lemma exception_add_trace :
+      forall e1 e2 res,
+      Common_Sem.exception (` (` fps)) e1 = (res, e2)
+      -> exists (t' : fp_trace),
+        get_trace e2 = get_trace e1 ++ t'.
+    Proof.
+      rewrite /Common_Sem.exception.
+      intros e1 e2 res Hexc.
+      destruct (Common_Sem.test_exceptions _ _ _) as [b e1'] eqn:Hexc1.
+      destruct b. 
+      - inversion Hexc; subst.
+        apply (test_exceptions_add_trace _ _ Hexc1).
+      - destruct (test_exceptions_add_trace _ _ Hexc1)
+          as [t Ht].
+        destruct (test_exceptions_add_trace _ _ Hexc)
+          as [t' Ht'].
+        eexists.
+        rewrite Ht' //= Ht.
+        by repeat rewrite app_assoc_reverse.
+    Qed.
+
+    Lemma run_stage_add_trace : 
+      forall e1 res e2,
+      run_stage (` fps) e1 = (res, e2)
+      -> exists (t' : fp_trace),
+        get_trace e2 = get_trace e1 ++ t'.
+    Proof.
+      intros e1 re e2.
+      rewrite /run_stage.
+      destruct (get_current_stage _);
+      try by (intros H; inversion H; by eexists).
+
+      { (* while *)
+        rewrite /while_sem /evalc /break /continue 
+                /app_trace /next_stage //=.
+        destruct (EVAL_Def.eval _ _).
+        - intros H; inversion H.
+          eexists. by rewrite app_assoc_reverse.
+        - intros H; inversion H.
+          by eexists.
+      }
+
+      { (* end while *)
+        rewrite /end_while_sem /while_sem /evalc /break /continue 
+                /app_trace /next_stage //=.
+        destruct (EVAL_Def.eval _ _).
+        - intros H; inversion H.
+          eexists. by rewrite app_assoc_reverse.
+        - intros H; inversion H.
+          by eexists.
+      }
+
+      { (* call *)
+        rewrite /call_sem /evalc.
+        destruct (get_call_loop _).
+        - destruct (EVAL_Def.eval _ _).
+          + destruct (get_call_until _).
+            * destruct (EVAL_Def.eval _ _).
+              -- intros H; inversion H.
+                eexists. simpl.
+                by repeat rewrite app_assoc_reverse.
+              -- intros H; inversion H.
+                eexists. simpl.
+                by repeat rewrite app_assoc_reverse.
+            * intros H; inversion H.
+              eexists. simpl.
+              by repeat rewrite app_assoc_reverse.
+          + destruct (get_call_break _).
+            * intros H; inversion H.
+              eexists. simpl.
+              by repeat rewrite app_assoc_reverse.
+            * intros H; inversion H.
+              eexists. simpl.
+              by repeat rewrite app_assoc_reverse.
+        - destruct (get_call_break _).
+          + intros H; inversion H.
+            eexists. simpl.
+            by repeat rewrite app_assoc_reverse.
+          + intros H; inversion H.
+            eexists. simpl.
+            by repeat rewrite app_assoc_reverse.
+      }
+
+      { (* deroute *)
+        destruct params.
+        intros H; inversion H.
+        destruct (goto_block_add_trace _ _ H2) as [t' Ht].
+        rewrite H2 Ht //=. eexists.
+        by apply app_assoc_reverse.
+      }
+
+      { (* nav mode *)
+        rewrite /nav_sem /evalc /break /continue.
+        destruct (nav_cond_sem _).
+        - destruct (EVAL_Def.eval _ _).
+          + intros H; inversion H.
+            eexists. simpl.
+            by repeat rewrite app_assoc_reverse.
+          + rewrite /nav_code_sem /evalc /break /continue.
+            destruct until.
+            * destruct (EVAL_Def.eval _ _).
+              -- intros H; inversion H.
+                eexists; simpl.
+                by repeat rewrite app_assoc_reverse.
+              -- intros H; inversion H.
+                eexists; simpl.
+                by repeat rewrite app_assoc_reverse.
+            * intros H; inversion H.
+              eexists; simpl.
+              by repeat rewrite app_assoc_reverse.
+        - rewrite /nav_code_sem /evalc /break /continue.
+          destruct until.
+          * destruct (EVAL_Def.eval _ _).
+            -- intros H; inversion H.
+              eexists; simpl.
+              by repeat rewrite app_assoc_reverse.
+            -- intros H; inversion H.
+              eexists; simpl.
+              by repeat rewrite app_assoc_reverse.
+          * intros H; inversion H.
+            eexists; simpl.
+            by repeat rewrite app_assoc_reverse.
+      }
+
+      { (* default *)
+        rewrite /default_sem /break /next_block.
+        intros H; inversion H. rewrite H2.
+        destruct (_ <? _);
+        apply (goto_block_add_trace _ _ H2). 
+      }
+    Qed.
+    
+    Lemma run_step_add_trace :
+      forall e e',
+      run_step (` fps) e = e'
+      -> exists (t' : fp_trace), 
+        get_trace e' = get_trace e ++ t'.
+    Proof.
+      intros e e' H; subst.
+      apply run_step_ind; clear e; intros e e' H.
+      - intros [t' Ht].
+        destruct (run_stage_add_trace _ H) as [t'' Ht'].
+        rewrite Ht Ht'.
+        eexists.
+        by rewrite app_assoc_reverse.
+      - destruct (run_stage_add_trace _ H) as [t' Ht].
+        exists t'. apply Ht.
+    Qed.
+
+    Definition has_run_on_enter (e1 e2 : fp_env) (id : block_id) :=
+      exists (t1 t2 : fp_trace),
+      get_trace e2 = get_trace e1 ++ t1 ++ (Common.on_enter (` (` fps)) id) ++ t2.
+
+    Definition has_run_on_exit (e1 e2 : fp_env) (id : block_id) :=
+      exists (t1 t2 : fp_trace),
+      get_trace e2 = get_trace e1 ++ t1 ++ (Common.on_exit (` (` fps)) id) ++ t2.
+
+    Definition has_run_on_enter_and_exit (e1 e2 : fp_env) (id1 id2 : block_id) := 
+      has_run_on_enter e1 e2 id2 /\ has_run_on_exit e1 e2 id1.
+
+    Lemma goto_block_run_on_enter_and_exit :
+      forall e1 e1' e2 id2,
+      Common_Sem.forbidden_deroute (` (` fps)) e1 id2 = (false, e1')
+      -> Common_Sem.goto_block (` (` fps)) e1 id2 = e2
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) id2.
+    Proof.
+      intros e1 e1' e2 id2 Hfb Hgoto.
+      rewrite /Common_Sem.goto_block Hfb in Hgoto.
+      subst.
+      destruct (forbidden_deroute_add_trace _ _ Hfb)
+        as [t' Ht].
+      split.
+      + (* on_enter id2 *)
+        rewrite /has_run_on_enter.
+        rewrite /change_block /Common_Sem.c_change_block //=.
+        destruct (_ =? _); simpl.
+        * exists (t' ++ (Common.on_exit (` (` fps)) (nav_block (get_state e1))) ++ [::reset_time] ++ [::init_stage]); exists nil.
+          rewrite Ht //= /Common.on_enter. 
+          repeat rewrite <- app_assoc.
+          rewrite <- get_block_get_normalise.
+          by rewrite app_nil_r.
+        * exists (t' ++ (Common.on_exit (` (` fps)) (nav_block (get_state e1))) ++ [::reset_time] ++ [::init_stage]); exists nil.
+          rewrite Ht //= /Common.on_enter. 
+          repeat rewrite <- app_assoc.
+          rewrite <- get_block_get_normalise.
+          by rewrite app_nil_r.
+      + (* on exit id1 *)
+        rewrite /has_run_on_exit.
+        rewrite /change_block /Common_Sem.c_change_block //=.
+        destruct (_ =? _); simpl.
+        * exists t'; eexists.
+          rewrite Ht. 
+          by rewrite <- app_assoc.
+        * exists t'; eexists.
+          rewrite Ht. 
+          by rewrite <- app_assoc.
+    Qed.
+
+    Lemma test_exception_change_run_on_enter_and_exit :
+      forall e1 e2 ex,
+      Common_Sem.test_exception (` (` fps)) e1 ex = (true , e2)
+      -> get_nav_block e1 <> get_nav_block e2
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1 e2 ex.
+      rewrite /Common_Sem.test_exception /evalc.
+      destruct (_ =? _) eqn:Eex; try by [].
+      destruct (~~ EVAL_Def.eval _ _); try by [].
+      intros H Hid. inversion H; subst; clear H.
+      remember (app_trace (app_trace _ _) _) as e1'.
+      remember (Common_Sem.goto_block _ e1' _) as e2; symmetry in Heqe2.
+      apply Nat.eqb_neq in Eex. apply not_eq_sym in Eex.
+      destruct (Common_Sem.forbidden_deroute (` (` fps)) e1' (get_expt_block_id ex))
+      as [b e1''] eqn:fb.
+      destruct b.
+      - rewrite /Common_Sem.goto_block fb in Heqe2.
+        subst.
+        have contra := (forbidden_deroute_unchanged _ _ _ fb).
+        simpl in contra.
+        destruct (Hid contra).
+
+      - destruct (goto_block_run_on_enter_and_exit e1' _ fb Heqe2)
+        as [[t1 [t1' H1]] [t2 [t2' H2]]].
+        split.
+        + rewrite /has_run_on_enter H1 Heqe1' //=.
+          clear H2; clear t2; clear t2'.
+          have Hid2 := (goto_block_forbidden_derout_nraised _ _ _ fb Heqe2).
+          simpl in Hid2. rewrite Hid2 /Common.on_enter.
+          rewrite <- get_block_get_normalise.
+          eexists; eexists.
+          by rewrite (app_assoc _ t1 _) 
+                  (app_assoc_reverse _ (opt_c_code_to_trace _) _)
+                  (app_assoc_reverse _ [:: COND _ _] _)
+                  app_assoc_reverse.
+        + rewrite /has_run_on_exit H2 Heqe1' //=.
+          eexists; eexists.
+          by rewrite (app_assoc _ t2 _) 
+                  (app_assoc_reverse _ (opt_c_code_to_trace _) _)
+                  (app_assoc_reverse _ [:: COND _ _] _)
+                  app_assoc_reverse.
+    Qed.
+    
+    Lemma test_exceptions_change_run_on_enter_and_exit:
+      forall e1 lex e2,
+      Common_Sem.test_exceptions (` (` fps)) e1 lex = (true, e2) ->
+      get_nav_block e1 <> get_nav_block e2 ->
+      has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1 lex; generalize dependent e1.
+      induction lex.
+      - simpl. intros e1 e2 contra. by inversion contra.
+      - simpl. intros e1.
+        destruct (Common_Sem.test_exception _ _ _) as [b e1'] eqn:test_ex.
+        destruct b. 
+        + intros e2 H; inversion H; subst; clear H.
+          by apply test_exception_change_run_on_enter_and_exit with a.
+        + rewrite /Common_Sem.test_exception /evalc in test_ex.
+          destruct (_ =? _).
+          * inversion test_ex. 
+            by apply IHlex.
+          * destruct (~~ EVAL_Def.eval _ _); try by [].
+            inversion test_ex; rewrite H0.
+            intros e2 Hlex Hid.
+            clear test_ex.
+            assert (nav_block (get_state e1) = nav_block (get_state e1'));
+            try by rewrite <- H0.
+            simpl in IHlex. rewrite H in Hid.
+            destruct (IHlex _ _ Hlex Hid) as [[t1 [t1' H1]] [t2 [t2' H2]]].
+            split.
+            -- rewrite /has_run_on_enter H1.
+               rewrite <- H0.
+               rewrite //=
+                       (app_assoc _ t1 _)
+                       (app_assoc_reverse _ _ t1)
+                       (app_assoc_reverse).
+               eexists; by eexists.
+            -- rewrite /has_run_on_exit H2.
+               rewrite <- H0.
+               rewrite //=
+                       (app_assoc _ t2 _)
+                       (app_assoc_reverse _ _ t2)
+                       (app_assoc_reverse).
+               eexists; by eexists.
+    Qed.
+    
+    Lemma exception_change_run_on_enter_and_exit:
+      forall e1 e2,
+      Common_Sem.exception (` (` fps)) e1 = (true, e2) ->
+      get_nav_block e1 <> get_nav_block e2 ->
+      has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1.
+      rewrite /Common_Sem.exception.
+      destruct (Common_Sem.test_exceptions _ _ _)
+        as [b e1'] eqn:Test1.
+      destruct b. 
+      - intros e2 H Hid.
+        inversion H; subst; clear H.
+        by apply (test_exceptions_change_run_on_enter_and_exit _ _ Test1 Hid).
+      - have Hid := (test_exceptions_nraised_unchanged _ _ _ Test1).
+        rewrite Hid.
+        intros e2 Test2 Hid2.
+        remember (app_trace e1' _ ) as e1''.
+        destruct (test_exceptions_add_trace _ _ Test1) as [t Ht].
+        assert (get_nav_block e1' = get_nav_block e1''); try by rewrite Heqe1''.
+        rewrite H in Hid2.
+        destruct (test_exceptions_change_run_on_enter_and_exit _ _ Test2 Hid2)
+        as [[t1 [t1' H1]] [t2 [t2' H2]]].
+        split.
+        + rewrite /has_run_on_enter H1 Heqe1'' //= Ht.
+          rewrite (app_assoc _ t1 _)
+                  (app_assoc_reverse _ _ t1)
+                  (app_assoc_reverse _ t _)
+                  (app_assoc_reverse).
+          eexists; by eexists.
+        + rewrite /has_run_on_exit H2 Heqe1'' //= Ht.
+          rewrite (app_assoc _ t2 _)
+                  (app_assoc_reverse _ _ t2)
+                  (app_assoc_reverse _ t _)
+                  (app_assoc_reverse).
+          eexists; by eexists.
+    Qed.
+
+    Lemma deroute_change_run_on_enter_and_exit : 
+      forall e1 e2 id params res,
+      get_stage (` (` fps)) (get_nav_block e1) (get_nav_stage e1) = FP_E.DEROUTE id params
+      -> get_nav_block e1 <> get_nav_block e2
+      -> run_stage (` fps) e1 = (res, e2)
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1 e2 id [block id0] res Hstage Hid.
+      rewrite /run_stage /get_current_stage Hstage /deroute_sem /break /FPE_BS.fp.
+      remember (Common_Sem.goto_block _ _ _) as e1'' eqn:Hgoto.
+      symmetry in Hgoto.
+      intros H; inversion H; subst e1''; clear H.
+      destruct (Common_Sem.forbidden_deroute (` (` fps)) (app_trace (next_stage e1) [:: init_stage]) id0)
+        as [b e1'] eqn:fb.
+      destruct b.
+      - rewrite /Common_Sem.goto_block fb in H2.
+        subst.
+        have contra := (forbidden_deroute_unchanged _ _ _ fb).
+        simpl in contra. destruct (Hid contra).
+
+      - destruct (goto_block_run_on_enter_and_exit _ _ fb H2)
+        as [[t1 [t1' Ht1]] [t2 [t2' Ht2]]].
+        split.
+        + rewrite /has_run_on_enter Ht1.
+          have Hid2 := (goto_block_forbidden_derout_nraised _ _ _ fb H2).
+          simpl in Hid2. rewrite /Common.on_enter //= Hid2.
+          rewrite <- get_block_get_normalise.
+          rewrite (app_assoc _ t1 _)
+                  (app_assoc_reverse _ _ t1)
+                  (app_assoc_reverse).
+          eexists; by eexists.
+        + rewrite /has_run_on_exit Ht2 //=.
+          rewrite (app_assoc _ t2 _)
+                  (app_assoc_reverse _ _ t2)
+                  (app_assoc_reverse).
+          eexists; by eexists.
+    Qed.
+
+    Lemma default_run_on_enter_and_exit : 
+      forall e1 e2 id res,
+      get_stage (` (` fps)) (get_nav_block e1) (get_nav_stage e1) = FP_E.DEFAULT id
+      -> get_nav_block e1 <> get_nav_block e2
+      -> run_stage (` fps) e1 = (res, e2)
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1 e2 id res Hstage Hid.
+      rewrite /run_stage /get_current_stage Hstage //= 
+              /default_sem /break /FPE_BS.fp.
+      intros H; inversion H; clear H. rewrite H2.
+      rewrite /next_block /FPE_BS.fp in H2.
+      destruct (_ <? _) eqn:Eid.
+      - destruct (Common_Sem.forbidden_deroute (` (` fps)) (reset_stage (` (` fps)) e1) (get_nav_block (reset_stage (` (` fps)) e1) + 1))
+        as [b e1'] eqn:fb.
+        destruct b.
+        * rewrite /Common_Sem.goto_block fb in H2.
+          subst.
+          have contra := (forbidden_deroute_unchanged _ _ _ fb).
+          simpl in contra. destruct (Hid contra).
+        * destruct (goto_block_run_on_enter_and_exit _ _ fb H2)
+          as [[t1 [t1' Ht1]] [t2 [t2' Ht2]]].
+          split.
+          + rewrite /has_run_on_enter Ht1 //=.
+            have Hid2 := (goto_block_forbidden_derout_nraised _ _ _ fb H2).
+            simpl in Hid2. rewrite /Common.on_enter //= Hid2.
+            rewrite <- get_block_get_normalise.
+            eexists; by eexists.
+          + rewrite /has_run_on_exit Ht2 //=.
+            eexists; by eexists.
+      - destruct (Common_Sem.forbidden_deroute (` (` fps)) (reset_stage (` (` fps)) e1) (get_nav_block (reset_stage (` (` fps)) e1)))
+        as [b e1'] eqn:fb.
+        destruct b.
+        * rewrite /Common_Sem.goto_block fb in H2.
+          subst.
+          have contra := (forbidden_deroute_unchanged _ _ _ fb).
+          simpl in contra. destruct (Hid contra).
+        * destruct (goto_block_run_on_enter_and_exit _ _ fb H2)
+          as [[t1 [t1' Ht1]] [t2 [t2' Ht2]]].
+          split.
+          + rewrite /has_run_on_enter Ht1 //=.
+            have Hid2 := (goto_block_forbidden_derout_nraised _ _ _ fb H2).
+            simpl in Hid2. rewrite /Common.on_enter //= Hid2.
+            rewrite <- get_block_get_normalise.
+            eexists; by eexists.
+          + rewrite /has_run_on_exit Ht2 //=.
+            eexists; by eexists.
+    Qed.
+
+    Lemma return_run_on_enter_and_exit : 
+      forall e1 e2 id params res,
+      get_stage (` (` fps)) (get_nav_block e1) (get_nav_stage e1) = FP_E.RETURN id params
+      -> get_nav_block e1 <> get_nav_block e2
+      -> run_stage (` fps) e1 = (res, e2)
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1 e2 id params res Hstage Hid.
+      rewrite /run_stage /get_current_stage Hstage /return_sem.
+      intros H; inversion H. clear H. clear H1. clear H2.
+      rewrite /return_block /app_trace.
+
+      simpl. split.
+      - (* on_enter *)
+        rewrite /has_run_on_enter //=.
+        eexists; exists nil.
+        rewrite -cat1s cat_app
+                (app_assoc)
+                app_assoc
+                (app_assoc_reverse (get_trace _))
+                app_assoc_reverse.
+        repeat f_equal.
+        by apply app_nil_end.
+
+      - (* on_exit *)
+        rewrite /has_run_on_exit //=.
+        exists nil; eexists.
+        by f_equal.
+    Qed.
+
+    Lemma run_stage_change_run_on_enter_and_exit :
+      forall e1 e2 res,
+      run_stage (` fps) e1 = (res, e2)
+      -> get_nav_block e1 <> get_nav_block e2
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1 e2 res.
+      rewrite /run_stage.
+      destruct (get_current_stage _ _) eqn:Hstage;
+      try by ( intros H; inversion H; 
+          intros contra; exfalso; auto).
+      { (* while *)
+        rewrite /while_sem /evalc.
+        destruct (EVAL_Def.eval).
+        - intros H; inversion H. simpl. 
+          intros contra. exfalso. auto.
+        - intros H; inversion H. simpl. 
+          intros contra. exfalso. auto.
+      }
+
+      { (* end while *)
+        rewrite /end_while_sem /while_sem /evalc.
+        destruct (EVAL_Def.eval).
+        - intros H; inversion H. simpl. 
+          intros contra. exfalso. auto.
+        - intros H; inversion H. simpl. 
+          intros contra. exfalso. auto.
+      }
+
+      { (* call *)
+        rewrite /call_sem /evalc.
+        destruct (get_call_loop _).
+        - destruct (EVAL_Def.eval _ _).
+          + destruct (get_call_until _).
+            * destruct (EVAL_Def.eval _ _).
+              --intros H; inversion H; intros contra;
+                exfalso; auto.
+              --intros H; inversion H; intros contra;
+                exfalso; auto.
+            * intros H; inversion H; intros contra;
+              exfalso; auto.
+          + destruct (get_call_break _).
+            * intros H; inversion H; intros contra;
+              exfalso; auto.
+            * intros H; inversion H; intros contra;
+              exfalso; auto.
+        - destruct (get_call_break _).
+          + intros H; inversion H; intros contra;
+            exfalso; auto.
+          + intros H; inversion H; intros contra;
+            exfalso; auto.
+      }
+
+      { (* deroute *)
+        intros Hrun Hid.
+        eapply deroute_change_run_on_enter_and_exit.
+        - apply Hstage.
+        - apply Hid.
+        - by rewrite /run_stage Hstage Hrun.
+      }
+
+      { (* return *)
+        intros Hrun Hid.
+        eapply return_run_on_enter_and_exit.
+        - apply Hstage.
+        - apply Hid.
+        - by rewrite /run_stage Hstage Hrun.
+      }
+
+      { (* nav *)
+        rewrite /nav_sem /evalc /break.
+        destruct (nav_cond_sem _).
+        - destruct (EVAL_Def.eval _ _).
+          + intros H; inversion H. by [].
+          + rewrite /nav_code_sem /evalc /break /app_trace //=.
+            destruct until.
+            * destruct (EVAL_Def.eval _ _).
+              -- intros H; inversion H; by [].
+              -- intros H; inversion H; by [].
+            * intros H; inversion H; by [].
+        - rewrite /nav_code_sem /evalc /break /app_trace //=.
+          destruct until.
+          + destruct (EVAL_Def.eval _ _).
+            * intros H; inversion H; by [].
+            * intros H; inversion H; by [].
+          + intros H; inversion H; by [].
+      }
+
+      { (*default *)
+        intros Hrun Hid.
+        eapply default_run_on_enter_and_exit.
+        - apply Hstage.
+        - apply Hid.
+        - by rewrite /run_stage Hstage Hrun.
+      }
+    Qed.
+
+    Lemma run_step_change_run_on_enter_and_exit :
+      forall e1 e2,
+      run_step (` fps) e1 = e2
+      -> get_nav_block e1 <> get_nav_block e2
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      intros e1 e2 Hr.
+      rewrite <- Hr.
+      apply run_step_ind; clear Hr; clear e1; clear e2.
+      - intros e1 e2 Hr IH Hid.
+        destruct (get_nav_block e1 =? get_nav_block e2) eqn:Hid'.
+        + apply Nat.eqb_eq in Hid'. rewrite Hid' in Hid.
+          destruct (run_stage_add_trace _ Hr) as [t Ht].
+          destruct (IH Hid) as [[t1 [t1' Ht1]] [t2 [t2' Ht2]]].
+          split.
+          * rewrite /has_run_on_enter Ht1 Ht.
+            eexists; eexists.
+            by rewrite (app_assoc)
+                    (app_assoc_reverse _ _ t1)
+                    (app_assoc_reverse).
+          * rewrite /has_run_on_exit Ht2 Ht Hid'.
+            eexists; eexists.
+            by rewrite (app_assoc)
+                    (app_assoc_reverse _ _ t2)
+                    (app_assoc_reverse).
+        + apply Nat.eqb_neq in Hid'.
+          destruct (get_nav_block e2 =? get_nav_block (run_step (` fps) e2)) eqn:Hid''.
+          * apply Nat.eqb_eq in Hid''. rewrite -Hid''.
+            remember (run_step _ e2) as e2'; symmetry in Heqe2'.
+            destruct (run_step_add_trace _ Heqe2') as [t' Ht'].
+            destruct (run_stage_change_run_on_enter_and_exit _ Hr Hid')
+              as [[t1 [t1' Ht1]] [t2 [t2' Ht2]]].
+            split.
+            -- rewrite /has_run_on_enter Ht' Ht1.
+              eexists; eexists.
+              by repeat rewrite app_assoc_reverse.
+            -- rewrite /has_run_on_exit Ht' Ht2.
+              eexists; eexists.
+              by repeat rewrite app_assoc_reverse.
+          * apply Nat.eqb_neq in Hid''.
+            destruct (run_stage_change_run_on_enter_and_exit _ Hr Hid')
+              as [[t1 [t1' Ht1]] [t2 [t2' Ht2]]].
+            destruct (IH Hid'') as [[t3 [t3' Ht3]] [t4 [t4' Ht4]]].
+            split.
+            -- rewrite /has_run_on_enter Ht3 Ht1.
+               rewrite (app_assoc _ t3 _)
+                       (app_assoc_reverse _ _ t3)
+                       (app_assoc_reverse (get_trace e1) _ _).
+               eexists; by eexists.
+            -- rewrite /has_run_on_exit Ht3 Ht2.
+               eexists; eexists.
+               by repeat rewrite app_assoc_reverse.
+      - intros e e' Hr Hid.
+        by apply (run_stage_change_run_on_enter_and_exit _ Hr Hid).
+    Qed.
+
+    Lemma step_change_run_on_enter_and_exit :
+      forall e1 e2,
+      FPE_BS.step (` fps) e1 = e2
+      -> get_nav_block e1 <> get_nav_block e2
+      -> has_run_on_enter_and_exit e1 e2 (get_nav_block e1) (get_nav_block e2).
+    Proof.
+      rewrite /FPE_BS.step.
+      intros e1 e2 Hstep Hid.
+      destruct (Common_Sem.exception _ _) as [b e1'] eqn:Exception.
+      destruct b. 
+      - subst.
+        by apply (exception_change_run_on_enter_and_exit _ Exception Hid).
+      - remember (run_step _ e1') as e1''; symmetry in Heqe1''.
+        rewrite -Hstep //= in Hid.
+        rewrite /FPE_BS.fp in Exception.
+        have Hid' := (exception_nraised_unchanged _ _ Exception).
+        simpl in Hid'. rewrite Hid' in Hid.
+        destruct (run_step_change_run_on_enter_and_exit _ Heqe1'' Hid)
+          as [[t1 [t1' Ht1]] [t2 [t2' Ht2]]].
+        destruct (exception_add_trace _ Exception) as [t Ht].
+        split.
+        + rewrite /has_run_on_enter -Hstep //= Ht1 Ht.
+          eexists; eexists.
+          by rewrite (app_assoc _ t1 _)
+                    (app_assoc_reverse _ t t1)
+                    (app_assoc_reverse (get_trace e1))
+                    (app_assoc_reverse _ _ (get_code_block_post_call _))
+                    (app_assoc_reverse)
+                    (app_assoc_reverse _ t1').
+        + rewrite /has_run_on_exit -Hstep //= Hid' Ht2 Ht.
+          eexists; eexists. 
+          by rewrite (app_assoc _ t2 _)
+                    (app_assoc_reverse _ t t2)
+                    (app_assoc_reverse (get_trace e1))
+                    (app_assoc_reverse _ _ (get_code_block_post_call _))
+                    (app_assoc_reverse)
+                    (app_assoc_reverse _ t2').
+    Qed.
+
+    End On_Enter_Exit_Verif.
+
   End FLIGHT_PLAN.
 
 End FPS_PROP.
\ No newline at end of file