blob: 5cf6b36872f0b84c477fbfd24b983466cd577b9b (
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
|
(** Correctness proof for code duplication *)
Require Import AST Linking Errors.
Require Import RTL Globalenvs Smallstep.
Require Import Duplicate.
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 ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Theorem transf_program_correct:
forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
(* TODO *)
Admitted.
End PRESERVATION.
|
