Start of match_states

1 files changed, 23 insertions, 3 deletions

diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 5cf6b368..a727155e 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -1,7 +1,7 @@
 (** Correctness proof for code duplication *)
-Require Import AST Linking Errors.
-Require Import RTL Globalenvs Smallstep.
-Require Import Duplicate.
+Require Import AST Linking Errors Globalenvs Smallstep.
+Require Import Coqlib.
+Require Import RTL Duplicate.
 
 Definition match_prog (p tp: program) :=
   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
@@ -20,6 +20,26 @@ Hypothesis TRANSL: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
+Inductive match_nodes: node -> node -> Prop :=
+  | match_node_intro: forall n, match_nodes n n
+  (* TODO - fill out the rest *)
+.
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+  | match_stackframe_intro:
+    forall res f sp pc rs f' pc'
+      (TRANSF: transf_function f = OK f')
+      (DUPLIC: match_nodes pc pc'),
+      match_stackframes (Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro:
+    forall st f sp pc rs m st' f' pc'
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: transf_function f = OK f')
+      (DUPLIC: match_nodes pc pc'),
+      match_states (State st f sp pc rs m) (State st' f' sp pc' rs m).
+
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.