diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
commit | 73a83b969dbb6f4c419ebdcc663f463509b6d6e3 (patch) | |
tree | 259852cd3272f2f31a09d75ac24e31ec1aaa8d9e /scheduling/RTLpathproof.v | |
parent | 3570ba2827908b280315c922ba7e43289f6d802a (diff) | |
parent | 035a1a9f4b636206acbae4506c5fc4ef322de0c1 (diff) | |
download | compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.tar.gz compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.zip |
Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3
Diffstat (limited to 'scheduling/RTLpathproof.v')
-rw-r--r-- | scheduling/RTLpathproof.v | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/scheduling/RTLpathproof.v b/scheduling/RTLpathproof.v new file mode 100644 index 00000000..20eded97 --- /dev/null +++ b/scheduling/RTLpathproof.v @@ -0,0 +1,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. + + |