begin scheduler BTL proof

2 files changed, 142 insertions, 5 deletions

diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index ec83b3c1..8240c861 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -37,6 +37,7 @@ Record match_function (f1 f2: BTL.function): Prop := {
   preserv_fnparams: fn_params f1 = fn_params f2;
   preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2;
   preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2;
+  (*exists_entrypoint: exists ibf, (fn_code f1)!(fn_entrypoint f1) = Some ibf;*)
   (* preserv_inputs: equiv_input_regs f1 f2; TODO: a-t-on besoin de ça ? *)
   symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 ->
                     exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2);
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 3811b170..f186581f 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -1,7 +1,7 @@
 Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
-Require Import Coqlib Maps Events Errors Op.
+Require Import Coqlib Maps Events Errors Op OptionMonad.
 Require Import RTL BTL BTL_SEtheory.
-Require Import BTL_Scheduler.
+Require Import BTLmatchRTL BTL_Scheduler.
 
 Definition match_prog (p tp: program) :=
   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
@@ -22,12 +22,148 @@ Hypothesis TRANSL: match_prog prog tprog.
 Let pge := Genv.globalenv prog.
 Let tpge := Genv.globalenv tprog.
 
-Inductive match_states (s1 s2: BTL.state): Prop :=. (* STUB *)
+Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s.
+Proof.
+  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
+Qed.
+
+Lemma senv_preserved:
+  Senv.equiv pge tpge.
+Proof.
+  eapply (Genv.senv_match TRANSL).
+Qed.
+
+(* TODO gourdinl move this to BTL_Scheduler.v? *)
+Inductive match_fundef: fundef -> fundef -> Prop :=
+  | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: stackframe -> stackframe -> Prop :=
+  | match_stackframe_intro 
+      res f sp pc rs f'
+      (TRANSF: match_function f f')
+      : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_intro 
+      st f sp pc rs m st' f'
+      (*(ENTRY: (fn_code f) ! pc = Some ibf)*)
+      (STACKS: list_forall2 match_stackframes st st')
+      (TRANSF: match_function f f')
+      : match_states (State st f sp pc rs m) (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) (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) (Returnstate st' v m)
+   .
+
+Lemma transf_function_correct f f':
+  transf_function f = OK f' -> match_function f f'.
+Proof.
+  unfold transf_function. intros H. monadInv H.
+  econstructor; eauto. eapply check_symbolic_simu_correct; eauto.
+Qed.
+
+Lemma transf_fundef_correct f f':
+  transf_fundef f = OK f' -> match_fundef f f'.
+Proof.
+Admitted.
+
+Lemma function_ptr_preserved:
+  forall v f,
+  Genv.find_funct_ptr pge v = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf.
+Proof.
+  intros.
+  exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
+Qed.
+
+Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = funsig f.
+Proof.
+  intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
+  symmetry; erewrite preserv_fnsig; eauto.
+Qed.
+
+Theorem transf_initial_states:
+  forall s1, initial_state prog s1 ->
+  exists s2, initial_state tprog s2 /\ match_states s1 s2.
+Proof.
+  intros. inv H.
+  exploit function_ptr_preserved; eauto. intros (tf & FIND &  TRANSF).
+  eexists. split.
+  - econstructor; eauto.
+    + intros; apply (Genv.init_mem_match TRANSL); eauto.
+    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
+      symmetry. eapply match_program_main. eauto.
+    + erewrite function_sig_translated; eauto.
+  - constructor; eauto.
+    + constructor.
+    + apply transf_fundef_correct; auto.
+Qed.
+
+Lemma transf_final_states s1 s2 r:
+  match_states s1 s2 -> final_state s1 r -> final_state s2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Lemma iblock_step_simulation stk1 stk2 f f' sp rs m ibf t s1 pc
+  (STEP : iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s1)
+  (ENTRY : (fn_code f) ! pc = Some ibf)
+  (STACKS : list_forall2 match_stackframes stk1 stk2)
+  (TRANSF : match_function f f')
+  :exists s2 : state,
+    (fn_code f') ! pc = Some ibf /\
+    iblock_step tr_inputs tpge stk2 f' sp rs m ibf.(entry) t s2 /\
+    match_states s1 s2.
+Admitted.
+
+Local Hint Constructors step: core.
+
+Theorem step_simulation s1 s1' t s2
+  (STEP: step tr_inputs pge s1 t s1')
+  (MS: match_states s1 s2)
+  :exists s2',
+    step tr_inputs tpge s2 t s2'
+  /\ match_states s1' s2'.
+Proof.
+  destruct STEP as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; inv MS.
+  - (* iblock *)
+    simplify_someHyps. intros ENTRY.
+    exploit iblock_step_simulation; eauto.
+    intros (s2 & ENTRY2 & STEP2 & MS2). 
+    eexists; split; eauto.
+  - (* function internal *)
+    inversion TRANSF as [xf tf MF |]; subst.
+    eexists; split.
+    + econstructor. erewrite <- preserv_fnstacksize; eauto.
+    + erewrite preserv_fnparams; eauto.
+      erewrite preserv_entrypoint; eauto.
+      econstructor; eauto. 
+  - (* function external *)
+    inv TRANSF. eexists; split; econstructor; eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  - (* return *)
+    inv STACKS. destruct b1 as [res' f' sp' pc' rs'].
+    eexists; split.
+    + econstructor.
+    + inv H1. econstructor; eauto.
+Qed.
 
 Theorem transf_program_correct:
   forward_simulation (fsem prog) (fsem tprog).
 Proof.
-  eapply forward_simulation_step with match_states. (* lock-step with respect to match_states *)
-Admitted.
+  eapply forward_simulation_step with match_states; simpl; eauto. (* lock-step with respect to match_states *)
+  - eapply senv_preserved.
+  - eapply transf_initial_states.
+  - eapply transf_final_states.
+  - intros; eapply step_simulation; eauto.
+Qed.
 
 End PRESERVATION.