Module Renumber2proof


Postorder renumbering of RTL control-flow graphs.

Require Import Coqlib.
Require Import Maps.
Require Import Postorder.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import Errors.
Require Import Renumber2.

Open Scope error_monad_scope.

Section PRESERVATION.

Variable prog tprog: program.
Hypothesis TRANSF: transf_program prog = OK tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma functions_translated:
  forall v f,
    Genv.find_funct ge v = Some f ->
    exists f',
      Genv.find_funct tge v = Some f' /\ transf_fundef f = OK f'.
Proof (@Genv.find_funct_transf_partial _ _ _ transf_fundef prog _ TRANSF).

Lemma function_ptr_translated:
  forall v f,
    Genv.find_funct_ptr ge v = Some f ->
    exists f',
      Genv.find_funct_ptr tge v = Some f' /\ transf_fundef f = OK f'.
Proof (@Genv.find_funct_ptr_transf_partial _ _ _ transf_fundef prog _ TRANSF).

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (@Genv.find_symbol_transf_partial _ _ _ transf_fundef prog _ TRANSF).

Lemma public_preserved:
  forall id,
  Genv.public_symbol tge id = Genv.public_symbol ge id.
Proof (@Genv.public_symbol_transf_partial _ _ _ transf_fundef prog _ TRANSF).

Lemma varinfo_preserved:
  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
Proof (@Genv.find_var_info_transf_partial _ _ _ transf_fundef prog _ TRANSF).

Lemma sig_preserved:
  forall f tf,
    transf_fundef f = OK tf ->
    funsig tf = funsig f.
Proof.
  intros; destruct f; monadInv H; try reflexivity.
  monadInv EQ. simpl; reflexivity.
Qed.

Lemma find_function_translated:
  forall ros rs fd,
    find_function ge ros rs = Some fd ->
    exists tfd,
      find_function tge ros rs = Some tfd /\ transf_fundef fd = OK tfd.
Proof.
  unfold find_function; intros. destruct ros as [r|id].
  eapply functions_translated; eauto.
  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
  eapply function_ptr_translated; eauto.
Qed.

Effect of an injective renaming of nodes on a CFG.

Section RENUMBER.

Variable f: PTree.t positive.

Hypothesis f_inj: forall x1 x2 y, f!x1 = Some y -> f!x2 = Some y -> x1 = x2.

Lemma renum_cfg_nodes:
  forall c c' x y i,
    c!x = Some i ->
    f!x = Some y ->
    renum_cfg f c = OK c' ->
    exists i',
      renum_instr f i = OK i' /\
      c'!y = Some i'.
Proof.
  set (P := fun (c: code) (e: res code) =>
              forall c' x y i, c!x = Some i -> f!x = Some y -> e = OK c' -> exists i', renum_instr f i = OK i' /\ c'!y = Some i').
  intros c0. change (P c0 (renum_cfg f c0)). unfold renum_cfg.
  apply PTree_Properties.fold_rec; unfold P; intros.
  - rewrite <- H in H1. apply (H0 _ _ _ _ H1 H2 H3).
  - rewrite PTree.gempty in H; congruence.
  - rewrite PTree.gsspec in H2. unfold renum_node in H4.
    destruct (peq x k).
    + inv H2. rewrite H3 in H4. monadInv H4.
      rewrite PTree.gss. exists x0; eauto.
    + destruct f!k as [y'|] eqn:?.
      * monadInv H4. rewrite PTree.gso.
        { eapply H1; eauto. }
        { red; intros; subst; eapply n; eapply f_inj; eauto. }
      * eapply H1; eauto.
Qed.

Lemma renum_cfg_nodes_inv:
  forall c c' x y i',
    c'!y = Some i' ->
    f!x = Some y ->
    renum_cfg f c = OK c' ->
    exists i,
      renum_instr f i = OK i' /\
      c!x = Some i.
Proof.
  set (P := fun (c: code) (e: res code) =>
              forall c' x y i', c'!y = Some i' -> f!x = Some y -> e = OK c' -> exists i, renum_instr f i = OK i' /\ c!x = Some i).
  intros c0. change (P c0 (renum_cfg f c0)). unfold renum_cfg.
  apply PTree_Properties.fold_rec; unfold P; intros.
  - rewrite <- H. eapply H0; eauto.
  - inv H1. rewrite PTree.gempty in H; congruence.
  - unfold renum_node in H4. rewrite PTree.gsspec.
    destruct (peq x k).
    + subst x. rewrite H3 in H4; monadInv H4.
      rewrite PTree.gss in H2; inv H2. exists v; eauto.
    + destruct f!k as [y'|] eqn:?.
      * monadInv H4. rewrite PTree.gso in H2.
        { eapply H1; eauto. }
        { red; intros; subst; eapply n; eapply f_inj; eauto. }
      * eapply H1; eauto.
Qed.
    
End RENUMBER.

Definition pnum (f: function) := postorder (successors_map f) f.(fn_entrypoint).

Definition reach (f: function) (pc: node) := reachable (successors_map f) f.(fn_entrypoint) pc.

Lemma transf_function_at:
  forall f tf pc pc' i,
  f.(fn_code)!pc = Some i ->
  reach f pc ->
  transf_function f = OK tf ->
  renum_pc (pnum f) pc = OK pc' ->
  exists i',
    renum_instr (pnum f) i = OK i' /\
    (fn_code tf)!pc' = Some i'.
Proof.
  intros. monadInv H1; simpl.
  destruct (postorder_correct (successors_map f) f.(fn_entrypoint)) as [A B].
  fold (pnum f) in *. unfold renum_pc in H2.
  destruct (pnum f)! pc as [pc''|] eqn:?; try (inv H2).
  eapply renum_cfg_nodes; eauto.
Qed.

Lemma transf_function_at_inv:
  forall f tf pc pc' i',
    (fn_code tf)!pc' = Some i' ->
    reach f pc ->
    transf_function f = OK tf ->
    renum_pc (pnum f) pc = OK pc' ->
    exists i,
      f.(fn_code)!pc = Some i /\
      renum_instr (pnum f) i = OK i'.
Proof.
  intros. monadInv H1; simpl.
  destruct (postorder_correct (successors_map f) f.(fn_entrypoint)) as [A B].
  fold (pnum f) in *. unfold renum_pc in H2.
  destruct (pnum f)! pc as [pc''|] eqn:?; try (inv H2).
  exploit renum_cfg_nodes_inv; eauto. intros [i [HA HB]]; eauto.
Qed.

Ltac TR_AT :=
  match goal with
  | [ A: (fn_code _)!_ = Some _ , B: reach _ _, C: transf_function _ = OK _, D: renum_pc _ _ = OK _ |- _ ] =>
        generalize (transf_function_at _ _ _ _ _ A B C D); simpl renum_instr; intros
  end.

Lemma reach_succ:
  forall f pc i s,
  f.(fn_code)!pc = Some i -> In s (successors_instr i) ->
  reach f pc -> reach f s.
Proof.
  unfold reach; intros. econstructor; eauto.
  unfold successors_map. rewrite PTree.gmap1. rewrite H. auto.
Qed.

Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
  | match_frames_intro: forall res f tf sp pc pc' rs
                          (TRANSF': transf_function f = OK tf)
                          (PC: renum_pc (pnum f) pc = OK pc')
                          (REACH: reach f pc),
      match_frames (Stackframe res f sp pc rs)
                   (Stackframe res tf sp pc' rs).

Inductive match_states: RTL.state -> RTL.state -> Prop :=
  | match_regular_states: forall stk f tf sp pc pc' rs m stk'
                          (TRANSF': transf_function f = OK tf)
                          (PC: renum_pc (pnum f) pc = OK pc')
                          (STACKS: list_forall2 match_frames stk stk')
                          (REACH: reach f pc),
      match_states (State stk f sp pc rs m)
                   (State stk' tf sp pc' rs m)
  | match_callstates: forall stk f tf args m stk'
                        (TRANSF': transf_fundef f = OK tf)
                        (STACKS: list_forall2 match_frames stk stk'),
      match_states (Callstate stk f args m)
                   (Callstate stk' tf args m)
  | match_returnstates: forall stk v m stk'
        (STACKS: list_forall2 match_frames stk stk'),
      match_states (Returnstate stk v m)
                   (Returnstate stk' v m).

Lemma list_nth_z_mmap:
  forall (A B : Type) (f : A -> res B) (l : list A) (l': list B) (n : Z),
    mmap f l = OK l' ->
    (forall x, list_nth_z l' n = Some x <-> option_map f (list_nth_z l n) = Some (OK x)).
Proof.
  induction l; intros.
  - simpl in H; inv H.
    split; simpl; intros; congruence.
  - simpl in H. monadInv H.
    simpl. destruct (zeq n 0); split; intros.
    + subst n. inv H. unfold option_map. congruence.
    + unfold option_map in H. subst n. congruence.
    + eapply (proj1 (IHl _ (Z.pred n) EQ1 x) H).
    + eapply (proj2 (IHl _ (Z.pred n) EQ1 x) H).
Qed.

Lemma list_forall2_in_1:
  forall (A B: Type) (P: A -> B -> Prop) (l1: list A) (l2: list B) (a: A),
    list_forall2 P l1 l2 ->
    In a l1 ->
    exists b, In b l2 /\ P a b.
Proof.
  induction l1; intros.
  - inv H0.
  - destruct H0 as [H0 | H0].
    + subst a0. inv H. exists b1; split; eauto. eapply in_eq.
    + inv H. generalize (IHl1 _ _ H5 H0). intros [b [HA HB]].
      exists b; split; eauto. eapply in_cons; auto.
Qed.

Lemma step_simulation:
  forall S1 t S2, RTL.step ge S1 t S2 ->
  forall S1', match_states S1 S1' ->
  exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
Proof.
  induction 1; intros S1' MS; inv MS; try TR_AT.
 nop *)  destruct H0 as [i' [A B]]; monadInv A.
  econstructor; split. eapply exec_Inop; eauto.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
 op *)  destruct H1 as [i' [A B]]; monadInv A.
  econstructor; split.
  eapply exec_Iop; eauto.
  instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
 load *)  destruct H2 as [i' [A B]]; monadInv A.
  econstructor; split.
  assert (eval_addressing tge sp addr rs ## args = Some a).
  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
  eapply exec_Iload; eauto.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
 store *)  destruct H2 as [i' [A B]]; monadInv A.
  econstructor; split.
  assert (eval_addressing tge sp addr rs ## args = Some a).
  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
  eapply exec_Istore; eauto.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
 call *)  destruct H1 as [i' [A B]]; monadInv A.
  generalize (find_function_translated _ _ _ H0). intros [tfd [HA HB]].
  econstructor; split.
  eapply exec_Icall with (fd := tfd); eauto.
    apply sig_preserved; eauto.
  constructor; auto. constructor; auto. constructor; auto. eapply reach_succ; eauto. simpl; auto.
 tailcall *)  destruct H1 as [i' [A B]]; monadInv A.
  generalize (find_function_translated _ _ _ H0). intros [tfd [HA HB]].
  econstructor; split.
  eapply exec_Itailcall with (fd := tfd); eauto.
    apply sig_preserved; auto.
    monadInv TRANSF'; simpl; eauto.
  constructor; auto.
 builtin *)  destruct H2 as [i' [A B]]; monadInv A.
  econstructor; split.
  eapply exec_Ibuiltin; eauto.
    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
    eapply external_call_symbols_preserved; eauto.
    exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
 cond *)  destruct H1 as [i' [A B]]; monadInv A.
  econstructor; split.
  eapply exec_Icond; eauto.
  replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot)
     with (renum_pc (pnum f) (if b then ifso else ifnot)).
  constructor; auto. destruct b; auto. eapply reach_succ; eauto. simpl. destruct b; auto.
  destruct b; auto.
 jumptbl *)  destruct H2 as [i' [A B]]; monadInv A.
  generalize (mmap_inversion _ _ EQ). intros HA. generalize (list_nth_z_in _ _ H1). intros HB.
  generalize (list_forall2_in_1 _ _ _ _ _ _ HA HB). intros [pc'' [XA XB]].
  econstructor; split.
  eapply exec_Ijumptable; eauto. eapply list_nth_z_mmap; eauto. rewrite H1; simpl; rewrite XB; reflexivity.
  constructor; auto. eapply reach_succ; eauto.
 return *)  destruct H1 as [i' [A B]]; monadInv A.
  econstructor; split.
  eapply exec_Ireturn; eauto.
  monadInv TRANSF'; simpl; eauto.
  constructor; auto.
 internal function *)  monadInv TRANSF'.
  simpl. econstructor; split.
  eapply exec_function_internal; eauto.
  monadInv EQ; simpl; eauto.
  monadInv EQ; simpl; eauto.
  constructor; auto. unfold reach. unfold transf_function; rewrite EQ0; rewrite EQ. eauto. constructor.
 external function *)  monadInv TRANSF'.
  econstructor; split.
  eapply exec_function_external; eauto.
    eapply external_call_symbols_preserved; eauto.
    exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
  constructor; auto.
 return *)  inv STACKS. inv H1.
  econstructor; split.
  eapply exec_return; eauto.
  constructor; auto.
Qed.

Lemma transf_initial_states:
  forall S1, RTL.initial_state prog S1 ->
  exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
Proof.
  intros. inv H. generalize (function_ptr_translated _ _ H2). intros [f' [HA HB]].
  econstructor; split.
  econstructor.
    eapply Genv.init_mem_transf_partial; eauto.
    simpl. rewrite symbols_preserved. erewrite AST.transform_partial_program_main; eauto.
    eapply HA.
    rewrite <- H3; apply sig_preserved; auto.
  constructor. auto. constructor.
Qed.

Lemma transf_final_states:
  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
Proof.
  intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_step.
  eexact public_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  exact step_simulation.
Qed.

Lemma renumber_match_genvs:
  Genv.match_genvs (fun fd1 fd2 => transf_fundef fd1 = OK fd2) (fun gv1 gv2 => OK gv1 = OK gv2) nil (Genv.globalenv prog) (Genv.globalenv tprog).
Proof.
  eapply Genv.globalenvs_match.
  eapply (AST.transform_partial_augment_program_match _ _ _ _ _ (Genv.transf_augment_OK _ _ _ TRANSF)).
Qed.

Lemma renumber_match_program:
  AST.match_program (fun fd tfd => transf_fundef fd = OK tfd) (fun gv1 gv2 => OK gv1 = OK gv2) nil (AST.prog_main prog) prog tprog.
Proof.
  eapply (AST.transform_partial_augment_program_match _ _ _ _ _ (Genv.transf_augment_OK _ _ _ TRANSF)).
Qed.
  
Lemma store_init_data_symbols_preserved:
  forall A B (ge ge': Genv.t A B) id m b p,
    (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
    Genv.store_init_data ge m b p id = Genv.store_init_data ge' m b p id.
Proof.
  destruct id; intros; auto.
  simpl. rewrite H; auto.
Qed.

Lemma store_init_data_list_symbols_preserved:
  forall A B (ge ge': Genv.t A B) id m b p,
    (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
    Genv.store_init_data_list ge m b p id = Genv.store_init_data_list ge' m b p id.
Proof.
  induction id; intros.
  - simpl; auto.
  - simpl. erewrite store_init_data_symbols_preserved; eauto.
    destruct (Genv.store_init_data ge' m b p a); eauto.
Qed.

Lemma alloc_globals_invariant_if_var_untouched:
  forall ge ge' gl gl' m m',
    Genv.alloc_globals ge m gl' = Some m' ->
    list_forall2 (AST.match_globdef (fun fd tfd : fundef => transf_fundef fd = OK tfd) (fun gv1 gv2 : unit => OK gv1 = OK gv2)) gl gl' ->
    (forall id, Genv.find_symbol ge id = Genv.find_symbol ge' id) ->
    Genv.alloc_globals ge' m gl = Some m'.
Proof.
  induction gl; intros.
  - simpl. inv H0; simpl in H. auto.
  - inv H0. simpl in H; simpl.
    destruct a. destruct g.
    + inv H4. simpl. simpl in H.
      destruct (let (m1, b) := Memory.Mem.alloc m 0 1 in Memory.Mem.drop_perm m1 b 0 1 Memtype.Nonempty); inv H.
      rewrite H2. eapply IHgl; eauto.
    + inv H4. inv H5. simpl. simpl in H.
      destruct (Memory.Mem.alloc m 0 (Genv.init_data_list_size init)).
      destruct (store_zeros m0 b 0 (Genv.init_data_list_size init)); try (inv H; fail).
      erewrite <- (store_init_data_list_symbols_preserved _ _ ge0 ge'); eauto.
      destruct (Genv.store_init_data_list ge0 m1 b 0 init); try (inv H; fail).
      destruct (Memory.Mem.drop_perm m2 b 0 (Genv.init_data_list_size init) (Genv.perm_globvar {| AST.gvar_info := info2; AST.gvar_init := init; AST.gvar_readonly := ro; AST.gvar_volatile := vo |})); try (inv H; fail).
      eapply IHgl; eauto.
Qed.

Lemma find_function_translated':
  forall ros rs tfd,
    find_function tge ros rs = Some tfd ->
    exists fd,
      find_function ge ros rs = Some fd /\ transf_fundef fd = OK tfd.
Proof.
  generalize renumber_match_genvs. intros XA. inv XA.
  unfold find_function; intros. destruct ros as [r|id].
  - unfold Genv.find_funct in *. destruct (rs#r); inv H.
    destruct (Integers.Int.eq_dec i Integers.Int.zero); inv H1.
    eapply mge_rev_funs in H0. simpl in H0. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); inv H0; eauto.
  - rewrite <- symbols_preserved. destruct (Genv.find_symbol tge id); try congruence.
    eapply mge_rev_funs in H. simpl in H. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); inv H; eauto.
Qed.

Theorem transf_program_backward_simulation:
  backward_simulation (RTL.semantics tprog) (RTL.semantics prog).
Proof.
  generalize renumber_match_genvs. intros HA.
  generalize renumber_match_program. intros XA.
  eapply backward_simulation_plus.
  - symmetry. eapply public_preserved.
  - intros. inv H.
    inv HA. generalize (mge_rev_funs _ _ H2). intros HA.
    destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try (inv HA; fail).
    destruct HA as [f1 [HA HB]].
    econstructor; econstructor.
    + unfold Genv.init_mem in *. inv XA. destruct H as [tglob [XA XB]].
      rewrite app_nil_r in XB. inv XB.
      eapply alloc_globals_invariant_if_var_untouched.
      * exact H0.
      * exact XA.
      * eapply symbols_preserved.
    + erewrite <- symbols_preserved; eauto.
      erewrite <- AST.transform_partial_program_main; eauto.
    + eapply HA.
    + generalize (sig_preserved f1 f HB). intros; congruence.
  - intros; exploit transf_initial_states; eauto.
    intros [s2' [A B]].
    exists s2'. split; eauto.
    eapply B.
  - intros. inv H0. inv H.
    inv STACKS. econstructor.
  - intros. generalize (H0 s1 (star_refl _ _ _)). intros YA.
    destruct s1.
    + right. destruct YA as [YA | YA].
      * destruct YA as [r YA]; inv YA.
      * inv H. destruct YA as [t [s'' YA]]. inv YA.
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          econstructor. econstructor. eapply exec_Inop; eauto. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          econstructor. econstructor. eapply exec_Iop; eauto.
          erewrite eval_operation_preserved; eauto.
          symmetry; eapply symbols_preserved. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          econstructor. econstructor. eapply exec_Iload; eauto.
          erewrite eval_addressing_preserved; eauto.
          symmetry; eapply symbols_preserved. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          econstructor. econstructor. eapply exec_Istore; eauto.
          erewrite eval_addressing_preserved; eauto.
          symmetry; eapply symbols_preserved. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          exploit find_function_translated'; eauto. intros [fd1 [A B]].
          econstructor. econstructor. eapply exec_Icall; eauto.
          symmetry; erewrite sig_preserved; eauto. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          exploit find_function_translated'; eauto. intros [fd1 [A B]].
          econstructor. econstructor. eapply exec_Itailcall; eauto.
          symmetry; erewrite sig_preserved; eauto.
          monadInv TRANSF'; eauto. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          econstructor. econstructor. eapply exec_Ibuiltin; eauto.
          eapply eval_builtin_args_preserved with (ge1 := tge); eauto. symmetry; eapply symbols_preserved.
          eapply external_call_symbols_preserved; eauto.
          symmetry; eapply symbols_preserved. symmetry; eapply public_preserved. symmetry; eapply varinfo_preserved. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          econstructor. econstructor. eapply exec_Icond; eauto. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          generalize (proj1 (list_nth_z_mmap _ _ _ _ _ (Integers.Int.unsigned n) EQ pc') H10). intros YA.
          unfold option_map in YA. case_eq (list_nth_z l (Integers.Int.unsigned n)); intros; rewrite H in YA; inv YA.
          econstructor. econstructor. eapply exec_Ijumptable; eauto. }
        { exploit transf_function_at_inv; eauto. intros [i [ZA ZB]].
          destruct i; simpl in ZB; monadInv ZB.
          econstructor. econstructor. eapply exec_Ireturn; eauto.
          monadInv TRANSF'; eauto. }
    + right. destruct YA as [YA | YA].
      * destruct YA as [r YA]; inv YA.
      * inv H. destruct YA as [t [s'' YA]]. inv YA.
        { destruct f0; simpl in TRANSF'; monadInv TRANSF'.
          econstructor. econstructor. econstructor; eauto. monadInv EQ; eauto. }
        { destruct f0; simpl in TRANSF'; monadInv TRANSF'.
          econstructor. econstructor. econstructor; eauto.
          eapply external_call_symbols_preserved; eauto.
          symmetry; eapply symbols_preserved. symmetry; eapply public_preserved. symmetry; eapply varinfo_preserved. }
    + destruct YA as [YA | YA].
      * inv H; left; eauto. destruct YA as [r YA]; inv YA.
        inv STACKS. eexists; econstructor; eauto.
      * inv H. destruct YA as [t [s'' YA]]. inv YA.
        inv STACKS. inv H3. right. econstructor. econstructor. econstructor; eauto.
  - intros; simpl in H0; exploit step_simulation; eauto.
    intros [s1' [A B]]. exists s1'; split; eauto.
    eapply plus_one; eauto.
Qed.

End PRESERVATION.
Generated by coq2html