aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL_Schedulerproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling/BTL_Schedulerproof.v')
-rw-r--r--scheduling/BTL_Schedulerproof.v29
1 files changed, 29 insertions, 0 deletions
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index e69de29b..049dc6b1 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -0,0 +1,29 @@
+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).
+Admitted.
+
+End PRESERVATION.