blob: 3811b1704ac880aae6f238dc7a691fe8fc265a47 (
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
30
31
32
33
|
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.
Inductive match_states (s1 s2: BTL.state): Prop :=. (* STUB *)
Theorem transf_program_correct:
forward_simulation (fsem prog) (fsem tprog).
Proof.
eapply forward_simulation_step with match_states. (* lock-step with respect to match_states *)
Admitted.
End PRESERVATION.
|
