Module SelectionproofC
Let SEGETGT: senv_genv_compat skenv_link tge. Proof. eapply SkEnv.senv_genv_compat; et. Qed.
Inductive match_states_at: Cminor.state -> CminorSel.state -> SimMem.t -> SimMem.t -> Prop :=
| match_states_at_intro
fptr sg vs k m st_tgt sm_at sm_arg
(ATEXT: Genv.find_funct ge fptr = None):
match_states_at (Cminor.Callstate fptr sg vs k m) st_tgt sm_at sm_arg.
Theorem sim_modsem: ModSemPair.sim msp.
Proof.
End SIMMODSEM.
Section SIMMOD.
Variable prog: Cminor.program.
Variable tprog: CminorSel.program.
Hypothesis TRANSL: match_prog prog tprog.
Definition mp: ModPair.t := ModPair.mk (CminorC.module prog) (CminorSelC.module tprog) tt.
Theorem sim_mod: ModPair.sim mp.
Proof.
econs;
ss.
-
r.
eapply Sk.match_program_eq;
eauto.
ii.
destruct f1;
ss.
+
clarify.
right.
unfold bind in MATCH.
inv MATCH.
des.
unfold sel_fundef in *.
ss.
unfold bind in *.
des_ifs.
esplits;
eauto.
unfold sel_function,
bind in *.
des_ifs.
+
clarify.
left.
rr in MATCH.
des.
ss.
clarify.
esplits;
eauto.
-
ii.
inv SIMSKENVLINK.
eapply sim_modsem;
eauto.
Qed.
End SIMMOD.