Stubs for Duplicate pass

1 files changed, 29 insertions, 0 deletions

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