From 863b65cc49fb49ad203694cac36e3cbd4f45dab7 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 3 Sep 2019 17:34:02 +0200 Subject: Stubs for Duplicate pass --- backend/Duplicateproof.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 backend/Duplicateproof.v (limited to 'backend/Duplicateproof.v') diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v new file mode 100644 index 00000000..5cf6b368 --- /dev/null +++ b/backend/Duplicateproof.v @@ -0,0 +1,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. \ No newline at end of file -- cgit