From 5b67f8284c3a98581f4da9b065a738fc534480c4 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 15:56:44 +0200 Subject: archi pour la verif du scheduler --- scheduling/BTL_Schedulerproof.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) (limited to 'scheduling/BTL_Schedulerproof.v') 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. -- cgit