Module RTLpathproof

Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL Linking.
Require Import RTLpath.

Definition match_prog (p: RTLpath.program) (tp: RTL.program) :=
match_program (fun ctx f tf => tf = fundef_RTL f) eq p tp.

Lemma transf_program_match:
forall p, match_prog p (transf_program p).

Proof.

intros. eapply match_transform_program; eauto.
Qed.

Lemma match_program_transf:
forall p tp, match_prog p tp -> transf_program p = tp.

Proof.

  intros p tp H. inversion_clear H. inv H1.
  destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *.
  subst. unfold transf_program. unfold transform_program. simpl.
  apply program_equals; simpl; auto.
  induction H0; simpl; auto.
  rewrite IHlist_forall2. apply cons_extract.
  destruct a1 as [ida gda]. destruct b1 as [idb gdb].
  simpl in *.
  inv H. inv H2.
  - simpl in *. subst. auto.
  - simpl in *. subst. inv H. auto.
Qed.

Section PRESERVATION.

Variable prog: RTLpath.program.
Variable tprog: RTL.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Theorem transf_program_correct:
forward_simulation (RTLpath.semantics prog) (RTL.semantics tprog).

Proof.

pose proof (match_program_transf prog tprog TRANSF) as TR. subst.
eapply RTLpath_correct.
Qed.

End PRESERVATION.