Library compcertx.backend.TailcallproofX

Require compcert.backend.Tailcallproof.
Require RTLX.
Require SmallstepX.

Import Coqlib.
Import Errors.
Import AST.
Import Values.
Import Memory.
Import Events.
Import SmallstepX.
Import Globalenvs.
Import Tailcall.
Export Tailcallproof.

Section WITHCONFIG.
Context `{compiler_config: CompilerConfiguration}.

Variable prog: RTL.program.
Let tprog := transf_program prog.
Let ge : RTL.genv := Genv.globalenv prog.
Let tge: RTL.genv := Genv.globalenv tprog.

Lemma transf_initial_states:
  ∀ i init_m sg args,
  ∀ S, RTLX.initial_state prog i init_m sg args S →
  ∃ R, RTLX.initial_state tprog i init_m sg args R ∧ match_states S R.
Proof.
  intros. inv H.
  exploit funct_ptr_translated; eauto. intros.
  ∃ (RTL.Callstate nil (transf_fundef f) args init_m); split.
  econstructor; eauto.
  unfold tprog. erewrite symbols_preserved; eauto.
  symmetry. eapply sig_preserved; eauto.
  econstructor.
  econstructor.
  exact (val_lessdef_refl _).
  apply Mem.extends_refl.
Qed.

Lemma transf_final_states:
  ∀ sg,
  ∀ st1 st2 r,
  match_states st1 st2 → RTLX.final_state sg st1 r →
  final_state_with_extends (RTLX.final_state sg) st2 r.
Proof.
  intros. inv H0. inv H.
  inv H3.
  econstructor; eauto.
  constructor.
Qed.

Theorem transf_program_correct:
  ∀ init_m args,
  ∀ i sg,
  forward_simulation
    (semantics_as_c (RTLX.csemantics prog i init_m) sg args)
    (semantics_with_extends (semantics_as_c (RTLX.csemantics tprog i init_m) sg args)).
Proof.
  intros.
  eapply forward_simulation_opt with (measure := measure); eauto.
  apply symbols_preserved.
  apply transf_initial_states.
  apply transf_final_states.
  apply transf_step_correct.
  eauto with typeclass_instances.
Qed.

End WITHCONFIG.