blob: 20eded970a6c9f0e80bd8d860b849da764e87942 (
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
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.
|
