1 files changed, 50 insertions, 0 deletions
diff --git a/scheduling/RTLpathproof.v b/scheduling/RTLpathproof.v
new file mode 100644
index 00000000..20eded97
--- /dev/null
+++ b/scheduling/RTLpathproof.v
@@ -0,0 +1,50 @@
+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.
+
+