Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
Require Import Coqlib Maps Events Errors Op.
Require Import RTL BTL BTL_SEtheory.
Require Import BTL_Scheduler.

Definition match_prog (p tp: program) :=
  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
  intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.

Hypothesis TRANSL: match_prog prog tprog.

Let pge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.

Theorem transf_program_correct:
  forward_simulation (fsem prog) (fsem tprog).
Proof.
  eapply forward_simulation_step with equiv_state. (* lock-step with respect to equiv_states *)
Admitted.

End PRESERVATION.