blob: 049dc6b13480bf9a9673d2405de3bc14db2a9b88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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.
|
