diff options
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 1221 |
1 files changed, 1221 insertions, 0 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v new file mode 100644 index 00000000..a601d5d5 --- /dev/null +++ b/backend/CSE3proof.v @@ -0,0 +1,1221 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(* +Replace available expressions by the register containing their value. + +Proofs. + +David Monniaux, CNRS, VERIMAG + *) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE3 CSE3analysis CSE3analysisproof. +Require Import RTLtyping. + +Section PARAMS. + Variable params : cse3params. + +Definition param_match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => param_transf_fundef params f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, param_transf_program params p = OK tp -> param_match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSF: param_match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Section SOUNDNESS. +Variable sp : val. +Variable ctx : eq_context. + +Definition sem_rel_b (rel : RB.t) (rs : regset) (m : mem) := + match rel with + | None => False + | Some rel => sem_rel (ctx:=ctx) (genv:=ge) (sp:=sp) rel rs m + end. + +Lemma forward_move_b_sound : + forall rel rs m x, + (sem_rel_b rel rs m) -> + rs # (forward_move_b (ctx := ctx) rel x) = rs # x. +Proof. + destruct rel as [rel | ]; simpl; intros. + 2: contradiction. + eapply forward_move_sound; eauto. + Qed. + + Lemma forward_move_l_b_sound : + forall rel rs m x, + (sem_rel_b rel rs m) -> + rs ## (forward_move_l_b (ctx := ctx) rel x) = rs ## x. + Proof. + destruct rel as [rel | ]; simpl; intros. + 2: contradiction. + eapply forward_move_l_sound; eauto. + Qed. + + Definition fmap_sem (fmap : PMap.t RB.t) (pc : node) (rs : regset) (m : mem) := + sem_rel_b (PMap.get pc fmap) rs m. + + Lemma subst_arg_ok: + forall invariants, + forall pc, + forall rs, + forall m, + forall arg, + forall (SEM : fmap_sem invariants pc rs m), + rs # (subst_arg (ctx:=ctx) invariants pc arg) = rs # arg. + Proof. + intros. + apply forward_move_b_sound with (m:=m). + assumption. + Qed. + + Lemma subst_args_ok: + forall invariants, + forall pc, + forall rs, + forall m, + forall args, + forall (SEM : fmap_sem invariants pc rs m), + rs ## (subst_args (ctx:=ctx) invariants pc args) = rs ## args. + Proof. + intros. + apply forward_move_l_b_sound with (m:=m). + assumption. + Qed. +End SOUNDNESS. + +Lemma functions_translated: + forall (v: val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ param_transf_fundef params f = OK tf. +Proof. + apply (Genv.find_funct_transf_partial TRANSF). +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: RTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ param_transf_fundef params f = OK tf. +Proof. + apply (Genv.find_funct_ptr_transf_partial TRANSF). +Qed. + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof. + apply (Genv.find_symbol_match TRANSF). +Qed. + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof. + apply (Genv.senv_match TRANSF). +Qed. + +Lemma sig_preserved: + forall f tf, param_transf_fundef params f = OK tf -> funsig tf = funsig f. +Proof. + destruct f; simpl; intros. + - monadInv H. + monadInv EQ. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ1. + reflexivity. + - monadInv H. + reflexivity. +Qed. + +Lemma stacksize_preserved: + forall f tf, param_transf_function params f = OK tf -> fn_stacksize tf = fn_stacksize f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma params_preserved: + forall f tf, param_transf_function params f = OK tf -> fn_params tf = fn_params f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma entrypoint_preserved: + forall f tf, param_transf_function params f = OK tf -> fn_entrypoint tf = fn_entrypoint f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma sig_preserved2: + forall f tf, param_transf_function params f = OK tf -> fn_sig tf = fn_sig f. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + reflexivity. +Qed. + +Lemma transf_function_is_typable: + forall f tf, param_transf_function params f = OK tf -> + exists tenv, type_function f = OK tenv. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + exists x. + assumption. +Qed. +Lemma transf_function_invariants_inductive: + forall f tf tenv, param_transf_function params f = OK tf -> + type_function f = OK tenv -> + check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f)))) + f tenv (fst (preanalysis tenv f)) = true. +Proof. + unfold transf_function; destruct f; simpl; intros. + monadInv H. + replace x with tenv in * by congruence. + clear x. + destruct preanalysis as [invariants hints]. + destruct check_inductiveness; trivial; discriminate. +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 /\ param_transf_fundef params 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. + +Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop := + | match_stackframes_nil: forall sg, + sg.(sig_res) = Tint -> + match_stackframes nil nil sg + | match_stackframes_cons: + forall res f sp pc rs s tf ts sg tenv + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: param_transf_function params f = OK tf) + (WTF: type_function f = OK tenv) + (WTRS: wt_regset tenv rs) + (WTRES: tenv res = proj_sig_res sg) + (REL: forall m vres, + sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) + ((fst (preanalysis tenv f))#pc) (rs#res <- vres) m), + + match_stackframes + (Stackframe res f sp pc rs :: s) + (Stackframe res tf sp pc rs :: ts) + sg. + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s f sp pc rs m ts tf tenv + (STACKS: match_stackframes s ts (fn_sig tf)) + (FUN: param_transf_function params f = OK tf) + (WTF: type_function f = OK tenv) + (WTRS: wt_regset tenv rs) + (REL: sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) ((fst (preanalysis tenv f))#pc) rs m), + match_states (State s f sp pc rs m) + (State ts tf sp pc rs m) + | match_states_call: + forall s f args m ts tf + (STACKS: match_stackframes s ts (funsig tf)) + (FUN: param_transf_fundef params f = OK tf) + (WTARGS: Val.has_type_list args (sig_args (funsig tf))), + match_states (Callstate s f args m) + (Callstate ts tf args m) + | match_states_return: + forall s res m ts sg + (STACKS: match_stackframes s ts sg) + (WTRES: Val.has_type res (proj_sig_res sg)), + match_states (Returnstate s res m) + (Returnstate ts res m). + +Lemma match_stackframes_change_sig: + forall s ts sg sg', + match_stackframes s ts sg -> + sg'.(sig_res) = sg.(sig_res) -> + match_stackframes s ts sg'. +Proof. + intros. inv H. + constructor. congruence. + econstructor; eauto. + unfold proj_sig_res in *. rewrite H0; auto. +Qed. + +Lemma transf_function_at: + forall f tf pc tenv instr + (TF : param_transf_function params f = OK tf) + (TYPE : type_function f = OK tenv) + (PC : (fn_code f) ! pc = Some instr), + (fn_code tf) ! pc = Some (param_transf_instr + (ctx := (context_from_hints (snd (preanalysis tenv f)))) + params (fst (preanalysis tenv f)) + pc instr). +Proof. + intros. + unfold transf_function in TF. + monadInv TF. + replace x with tenv in * by congruence. + clear EQ. + destruct (preanalysis tenv f) as [invariants hints]. + destruct check_inductiveness. + 2: discriminate. + inv EQ0. + simpl. + rewrite PTree.gmap. + rewrite PC. + reflexivity. +Qed. + +Ltac TR_AT := erewrite transf_function_at by eauto. + +Hint Resolve wt_instrs type_function_correct : wt. + +Lemma wt_undef : + forall tenv rs dst, + wt_regset tenv rs -> + wt_regset tenv rs # dst <- Vundef. +Proof. + unfold wt_regset. + intros. + destruct (peq r dst). + { subst dst. + rewrite Regmap.gss. + constructor. + } + rewrite Regmap.gso by congruence. + auto. +Qed. + +Lemma rel_ge: + forall inv inv' + (GE : RELATION.ge inv' inv) + ctx sp rs m + (REL: sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) inv rs m), + sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) inv' rs m. +Proof. + unfold sem_rel, RELATION.ge. + intros. + apply (REL i); trivial. + eapply HashedSet.PSet.is_subset_spec1; eassumption. +Qed. + +Hint Resolve rel_ge : cse3. + +Lemma relb_ge: + forall inv inv' + (GE : RB.ge inv' inv) + ctx sp rs m + (REL: sem_rel_b sp ctx inv rs m), + sem_rel_b sp ctx inv' rs m. +Proof. + intros. + destruct inv; cbn in *. + 2: contradiction. + destruct inv'; cbn in *. + 2: assumption. + eapply rel_ge; eassumption. +Qed. + +Hint Resolve relb_ge : cse3. + +Lemma sem_rhs_sop : + forall sp op rs args m v, + eval_operation ge sp op rs ## args m = Some v -> + sem_rhs (genv:=ge) (sp:=sp) (SOp op) args rs m v. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sop : cse3. + +Lemma sem_rhs_sload : + forall sp chunk addr rs args m a v, + eval_addressing ge sp addr rs ## args = Some a -> + Mem.loadv chunk m a = Some v -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m v. +Proof. + intros. simpl. + rewrite H. rewrite H0. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload : cse3. + +Lemma sem_rhs_sload_notrap1 : + forall sp chunk addr rs args m, + eval_addressing ge sp addr rs ## args = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap1 : cse3. + +Lemma sem_rhs_sload_notrap2 : + forall sp chunk addr rs args m a, + eval_addressing ge sp addr rs ## args = Some a -> + Mem.loadv chunk m a = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. rewrite H0. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap2 : cse3. + +Lemma sem_rel_top: + forall ctx sp rs m, sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) RELATION.top rs m. +Proof. + unfold sem_rel, RELATION.top. + intros. + rewrite HashedSet.PSet.gempty in *. + discriminate. +Qed. + +Hint Resolve sem_rel_top : cse3. + +Lemma sem_rel_b_top: + forall ctx sp rs m, sem_rel_b sp ctx (Some RELATION.top) rs m. +Proof. + intros. simpl. + apply sem_rel_top. +Qed. + +Hint Resolve sem_rel_b_top : cse3. + +(* +Ltac IND_STEP := + match goal with + REW: (fn_code ?fn) ! ?mpc = Some ?minstr + |- + sem_rel_b ?sp (context_from_hints (snd (preanalysis ?tenv ?fn))) ((fst (preanalysis ?tenv ?fn)) # ?mpc') ?rs ?m => + assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv fn)))) fn tenv (fst (preanalysis tenv fn))) as IND by + (apply checked_is_inductive_allstep; + eapply transf_function_invariants_inductive; eassumption); + unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND; + specialize IND with (pc:=mpc) (pc':=mpc') (instr:=minstr); + simpl in IND; + rewrite REW in IND; + simpl in IND; + destruct ((fst (preanalysis tenv fn)) # mpc') as [zinv' | ]; + destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ]; + simpl in *; + intuition; + eapply rel_ge; eauto with cse3 (* ; for printing + idtac mpc mpc' fn minstr *) + end. + *) + +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. + all: try set (ctx := (context_from_hints (snd (preanalysis tenv f)))) in *. + all: try set (invs := (fst (preanalysis tenv f))) in *. + - (* Inop *) + exists (State ts tf sp pc' rs m). split. + + apply exec_Inop; auto. + TR_AT. reflexivity. + + econstructor; eauto. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + unfold sem_rel_b. + apply (rel_ge inv_pc inv_pc'); auto. + (* END INVARIANT *) + + - (* Iop *) + exists (State ts tf sp pc' (rs # res <- v) m). split. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity. + unfold param_transf_instr, find_op_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct (if (negb params.(cse3_operations) || (negb (params.(cse3_trivial_ops))) && (is_trivial_op op)) + then None + else + rhs_find pc (SOp op) + (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND. + ** destruct (negb params.(cse3_operations) || ((negb (params.(cse3_trivial_ops))) && (is_trivial_op op))). discriminate. + apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iop with (op := op) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)). + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_operation_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iop with (op := op) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)). + TR_AT. + { subst instr'. + rewrite if_same in H1. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_operation_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * eapply wt_exec_Iop with (f:=f); try eassumption. + eauto with wt. + * + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) + - (* Iload *) + exists (State ts tf sp pc' (rs # dst <- v) m). split. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite H1 in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * eapply wt_exec_Iload with (f:=f); try eassumption. + eauto with wt. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) + + - (* Iload notrap1 *) + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * apply wt_undef; assumption. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) + + - (* Iload notrap2 *) + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + * destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite H0 in FIND_SOUND. (* ADDR *) + rewrite H1 in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload_notrap2 with (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + * apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + + econstructor; eauto. + * apply wt_undef; assumption. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) + + - (* Istore *) + exists (State ts tf sp pc' rs m'). split. + + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)) + (src := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc src)) ; try eassumption. + * TR_AT. reflexivity. + * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved. + eassumption. + * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. + assumption. + + econstructor; eauto. + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply store_sound with (a0:=a) (m0:=m); unfold ctx; eauto with cse3. + (* END INVARIANT *) + + - (* Icall *) + destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. + econstructor. split. + + eapply exec_Icall; try eassumption. + * TR_AT. reflexivity. + * apply sig_preserved; auto. + + rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + assert (wt_instr f tenv (Icall (funsig fd) ros args res pc')) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * econstructor; eauto. + ** rewrite sig_preserved with (f:=fd); assumption. + ** intros. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + (* END INVARIANT *) + { apply kill_reg_sound; unfold ctx; eauto with cse3. + eapply kill_mem_sound; unfold ctx; eauto with cse3. } + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H7. + apply wt_regset_list; auto. + - (* Itailcall *) + destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. + econstructor. split. + + eapply exec_Itailcall; try eassumption. + * TR_AT. reflexivity. + * apply sig_preserved; auto. + * rewrite stacksize_preserved with (f:=f); eauto. + + rewrite subst_args_ok with (m:=m) (sp := (Vptr stk Ptrofs.zero)) by trivial. + assert (wt_instr f tenv (Itailcall (funsig fd) ros args)) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * rewrite sig_preserved with (f:=fd) by trivial. + inv STACKS. + ** econstructor; eauto. + rewrite H7. + rewrite <- sig_preserved2 with (tf:=tf) by trivial. + assumption. + ** econstructor; eauto. + unfold proj_sig_res in *. + rewrite H7. + rewrite WTRES. + rewrite sig_preserved2 with (f:=f) by trivial. + reflexivity. + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H6. + apply wt_regset_list; auto. + - (* Ibuiltin *) + econstructor. split. + + eapply exec_Ibuiltin; try eassumption. + * TR_AT. reflexivity. + * eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + * eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + econstructor; eauto. + * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. + * (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + (* END INVARIANT *) + + apply kill_builtin_res_sound; unfold ctx; eauto with cse3. + eapply external_call_sound; unfold ctx; eauto with cse3. + + - (* Icond *) + destruct (find_cond_in_fmap (ctx := ctx) params invs pc cond args) as [bfound | ] eqn:FIND_COND. + + econstructor; split. + * eapply exec_Inop; try eassumption. + TR_AT. unfold param_transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. + * replace bfound with b. + { econstructor; eauto. + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + rewrite andb_true_iff in IND_step_me. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me as [IND_so [IND_not ZOT]]. + clear ZOT. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + + destruct b. + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. + (* END INVARIANT *) + } + unfold sem_rel_b in REL. + destruct (invs # pc) as [rel | ] eqn:FIND_REL. + 2: contradiction. + pose proof (is_condition_present_sound pc rel cond args rs m REL) as COND_PRESENT_TRUE. + pose proof (is_condition_present_sound pc rel (negate_condition cond) args rs m REL) as COND_PRESENT_FALSE. + rewrite eval_negate_condition in COND_PRESENT_FALSE. + unfold find_cond_in_fmap in FIND_COND. + change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND. + rewrite FIND_REL in FIND_COND. + destruct (params.(cse3_conditions)). + 2: discriminate. + destruct (is_condition_present pc rel cond args). + { rewrite COND_PRESENT_TRUE in H0 by trivial. + congruence. + } + destruct (is_condition_present pc rel (negate_condition cond) args). + { destruct (eval_condition cond rs ## args m) as [b0 | ]. + 2: discriminate. + inv H0. + cbn in COND_PRESENT_FALSE. + intuition. + inv H0. + inv FIND_COND. + destruct b; trivial; cbn in H2; discriminate. + } + clear COND_PRESENT_TRUE COND_PRESENT_FALSE. + pose proof (is_condition_present_sound pc rel cond (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_TRUE. + pose proof (is_condition_present_sound pc rel (negate_condition cond) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_FALSE. + rewrite eval_negate_condition in COND_PRESENT_FALSE. + + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_TRUE. + { rewrite COND_PRESENT_TRUE in H0 by trivial. + congruence. + } + unfold fmap_sem. + unfold sem_rel_b. + fold invs. + rewrite FIND_REL. + exact REL. + } + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_FALSE. + { destruct (eval_condition cond rs ## args m) as [b0 | ]. + 2: discriminate. + inv H0. + cbn in COND_PRESENT_FALSE. + intuition. + inv H0. + inv FIND_COND. + destruct b; trivial; cbn in H2; discriminate. + } + unfold fmap_sem. + unfold sem_rel_b. + fold invs. + rewrite FIND_REL. + exact REL. + } + discriminate. + + econstructor; split. + * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. + ** TR_AT. unfold param_transf_instr. fold invs. fold ctx. + rewrite FIND_COND. + reflexivity. + ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + eassumption. + ** reflexivity. + * econstructor; eauto. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + rewrite andb_true_iff in IND_step_me. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me as [IND_so [IND_not ZOT]]. + clear ZOT. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + + destruct b. + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. + (* END INVARIANT *) + + - (* Ijumptable *) + econstructor. split. + + eapply exec_Ijumptable with (arg := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)); try eassumption. + * TR_AT. reflexivity. + * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. + assumption. + + econstructor; eauto. + + (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + rewrite forallb_forall in IND_step_me. + assert (RB.ge (invs # pc') (Some inv_pc)) as GE. + { + apply relb_leb_correct. + specialize IND_step_me with (pc', Some inv_pc). + apply IND_step_me. + apply (in_map (fun pc'0 : node => (pc'0, Some inv_pc))). + eapply list_nth_z_in. + eassumption. + } + destruct (invs # pc'); cbn in *. + 2: contradiction. + eapply rel_ge; eauto. + (* END INVARIANT *) + + - (* Ireturn *) + destruct or as [arg | ]. + -- econstructor. split. + + eapply exec_Ireturn with (or := Some (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)). + * TR_AT. reflexivity. + * rewrite stacksize_preserved with (f:=f); eauto. + + simpl. + rewrite subst_arg_ok with (sp:=(Vptr stk Ptrofs.zero)) (m:=m) by trivial. + econstructor; eauto. + apply type_function_correct in WTF. + apply wt_instrs with (pc:=pc) (instr:=(Ireturn (Some arg))) in WTF. + 2: assumption. + inv WTF. + rewrite sig_preserved2 with (f:=f) by assumption. + rewrite <- H3. + unfold wt_regset in WTRS. + apply WTRS. + -- econstructor. split. + + eapply exec_Ireturn; try eassumption. + * TR_AT; reflexivity. + * rewrite stacksize_preserved with (f:=f); eauto. + + econstructor; eauto. + simpl. trivial. + - (* Callstate internal *) + monadInv FUN. + rename x into tf. + destruct (transf_function_is_typable f tf EQ) as [tenv TENV]. + econstructor; split. + + apply exec_function_internal. + rewrite stacksize_preserved with (f:=f); eauto. + + rewrite params_preserved with (tf:=tf) (f:=f) by assumption. + rewrite entrypoint_preserved with (tf:=tf) (f:=f) by assumption. + econstructor; eauto. + * apply type_function_correct in TENV. + inv TENV. + simpl in WTARGS. + rewrite sig_preserved2 with (f:=f) in WTARGS by assumption. + apply wt_init_regs. + rewrite <- wt_params in WTARGS. + assumption. + * assert ((check_inductiveness f tenv (fst (preanalysis tenv f)))=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + clear IND_step. + apply RB.beq_correct in IND_entry. + unfold RB.eq in *. + destruct ((fst (preanalysis tenv f)) # (fn_entrypoint f)). + 2: contradiction. + cbn. + rewrite <- IND_entry. + apply sem_rel_top. + + - (* external *) + simpl in FUN. + inv FUN. + econstructor. split. + + eapply exec_function_external. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + econstructor; eauto. + eapply external_call_well_typed; eauto. + - (* return *) + inv STACKS. + econstructor. split. + + eapply exec_return. + + econstructor; eauto. + apply wt_regset_assign; trivial. + rewrite WTRES0. + exact WTRES. +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. inversion H. + exploit function_ptr_translated; eauto. + intros (tf & A & B). + exists (Callstate nil tf nil m0); split. + - econstructor; eauto. + + eapply (Genv.init_mem_match TRANSF); eauto. + + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main; eauto. + + rewrite <- H3. eapply sig_preserved; eauto. + - constructor; trivial. + + constructor. rewrite sig_preserved with (f:=f) by assumption. + rewrite H3. reflexivity. + + rewrite sig_preserved with (f:=f) by assumption. + rewrite H3. reflexivity. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> final_state S1 r -> 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. + - apply senv_preserved. + - eexact transf_initial_states. + - eexact transf_final_states. + - intros. eapply step_simulation; eauto. +Qed. + +End PRESERVATION. +End PARAMS. + +Definition match_prog := param_match_prog (cmdline_params tt). |