start RTL -> BTL

1 files changed, 50 insertions, 0 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 3944e756..08a77ae4 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -6,6 +6,56 @@ Require Import Errors Linking BTLtoRTL.
 
 Require Import Linking.
 
+Record match_function dupmap f f': Prop := {
+  dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f');
+  dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f');
+  preserv_fnsig: fn_sig f = RTL.fn_sig f';
+  preserv_fnparams: fn_params f = RTL.fn_params f';
+  preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f'
+}.
+
+Inductive match_fundef: fundef -> RTL.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc = Some pc')
+      : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
+
+Inductive match_states: state -> RTL.state -> Prop :=
+  | match_states_intro 
+      dupmap st f sp pc rs m st' f' pc'
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc = Some pc')
+      : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m)
+  | match_states_call
+      st st' f f' args m
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_fundef f f')
+      : match_states (Callstate st f args m) (RTL.Callstate st' f' args m)
+  | match_states_return
+      st st' v m
+      (STACKS: list_forall2 match_stackframes st st')
+      : match_states (Returnstate st v m) (RTL.Returnstate st' v m)
+   .
+
+Lemma verify_function_correct dupmap f f' tt:
+  verify_function dupmap f f' = OK tt ->
+  fn_sig f = RTL.fn_sig f' ->
+  fn_params f = RTL.fn_params f' ->
+  fn_stacksize f = RTL.fn_stacksize f' ->
+  match_function dupmap f f'.
+Proof.
+  unfold verify_function; intro VERIF. monadInv VERIF.
+  constructor; eauto.
+  - eapply verify_cfg_correct; eauto.
+  - eapply verify_is_copy_correct; eauto.
+Qed.
+
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
 Proof.