Module TailcallproofC
Let SEGETGT: senv_genv_compat skenv_link tge. Proof. eapply SkEnv.senv_genv_compat; et. Qed.
Theorem sim_modsem: ModSemPair.sim msp.
Proof.
End SIMMODSEM.
Section SIMMOD.
Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Definition mp: ModPair.t := ModPair.mk (RTLC.module prog) (RTLC.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.
esplits;
eauto.
rewrite sig_preserved;
et.
+
clarify.
left.
esplits;
eauto.
-
ii.
inv SIMSKENVLINK.
eapply sim_modsem;
eauto.
Qed.
End SIMMOD.