Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import RTL Op Registers OptionMonad BTL.

Require Import Errors Linking BTLtoRTL.


(*****************************)
(* Put this in an other file *)

Require Import Linking.

Lemma transf_function_correct f f':
  transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
Proof.
  unfold transf_function; unfold bind. repeat autodestruct.
  intros H _ _ X. inversion X; subst; clear X.
  eexists; eapply verify_function_correct; simpl; eauto.
Qed.

Lemma transf_fundef_correct f f':
  transf_fundef f = OK f' -> match_fundef f f'.
Proof.
  intros TRANSF; destruct f; simpl; monadInv TRANSF.
  + exploit transf_function_correct; eauto.
    intros (dupmap & MATCH_F).
    eapply match_Internal; eauto.
  + eapply match_External.
Qed.

Definition match_prog (p: program) (tp: RTL.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 RTL_SIMULATES_BTL.

Variable prog: program.
Variable tprog: RTL.program.

Hypothesis TRANSL: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.

Lemma senv_preserved: Senv.equiv ge tge.
Proof.
  eapply (Genv.senv_match TRANSL).
Qed.

Lemma functions_translated (v: val) (f: fundef):
  Genv.find_funct ge v = Some f ->
  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog.
Proof.
  intros. exploit (Genv.find_funct_match TRANSL); eauto.
  intros (cu & tf & A & B & C).
  repeat eexists; intuition eauto.
  + unfold incl; auto.
  + eapply linkorder_refl.
Qed.

Lemma function_ptr_translated v f:
  Genv.find_funct_ptr ge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tge 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 -> RTL.funsig tf = funsig f.
Proof.
  intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
  erewrite preserv_fnsig; eauto.
Qed.

Lemma transf_initial_states s1:
  initial_state prog s1 ->
  exists s2, RTL.initial_state tprog s2 /\ match_states s1 s2.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
  eexists. split.
  - econstructor; eauto.
    + eapply (Genv.init_mem_transf_partial 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 -> RTL.final_state s2 r.
Proof.
  intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Inductive iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg: state -> trace -> bool -> option final -> option node -> Prop :=
  | ibis_synced ib rs1 m1 opc pc1
      (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 None)
      (HOPC: opc = Some pc1)
      (MIB : match_iblock dupmap cfg true pc0 ib opc)
      : iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg (State stack f sp pc0 rs0 m0) E0 true None opc
  | ibis_stutter ib rs1 m1 fin ofin s t
      (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
      (HFIN: ofin = Some fin)
      (MIB : match_iblock dupmap cfg false pc0 ib None)
      (FS : final_step ge stack f sp rs1 m1 fin t s)
      : iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg s t false ofin None.

Lemma iblock_step_simulation
 sp dupmap stack stack' f f' rs0 m0 ofin pc0 opc t s isfst
 (STACKS: list_forall2 match_stackframes stack stack')
 (TRANSF: match_function dupmap f f')
 (*(IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin)*)
 (*(MIB : match_iblock dupmap cfg' isfst pc0 ib opc)*)
 (*(FS : final_step ge stack f sp rs1 m1 fin t s)*)
(*FNC : (fn_code f) ! pc = Some ib*)
 (IBGEN: iblock_istep_gen sp dupmap stack f rs0 m0 pc0 (RTL.fn_code f') s t isfst ofin opc)
 :exists s', (if isfst then plus RTL.step else star RTL.step) tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
Proof.
  (* TODO: généraliser ce lemme pour pouvoir le prouver par induction sur IBIS:
       => il faut en particulier généraliser l'hypothèse MIB qui relie le iblock_istep ib en cours d'exécution.
          avec le code RTL à partir de pc0. 
       => ici, le "isfst" a déjà été généralisé: quand il vaut "false", ça veut dire qu'on a le droit de faire du "stuttering" côté RTL.
       => il reste à comprendre comment généraliser le "None" en "opc"
          ainsi que l'hypothese OFIN pour autoriser le cas "ofin=None" (nécessaire pour l'induction).
          Idée: si "ofin = None" alors il y a un pc1 tq "opc = Some pc1" qui permet d'exécuter la suite du bloc...

    Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"...
  *)
  (* XXX keep IBIS, MIB, and FS ? *)
  induction IBGEN.
  - inv IBIS.
    + inv MIB.
      eexists. split. apply plus_one.
      eapply exec_Inop; eauto.
      econstructor; eauto.
      try_simplify_someHyps.
      admit.
    + admit.
    + admit.
    + admit.
    + admit.
    + admit.
  - admit.
  (* induction IBIS.
  - (* exec_final *) 
    try_simplify_someHyps. (* TODO: introduire un lemme pour ce cas specifique ? *)
    admit.
  - (* exec_nop *)
    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
  - (* exec_op *)
    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
  - (* exec_load_TRAP *)
    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
  - (* exec_load_store *)
    try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *)
  - (* exec_seq_stop *)
    try_simplify_someHyps.
    inv MIB.
    eapply IHIBIS; eauto.
    (* TODO: c'est ici qu'on voit que l'hypothèse MIB est trop restrictive actuellement 
       normalement, l'hypothèse d'induction IHIBIS devrait permettre de conclure quasi-directement ici.
    *)
    admit.
  - (* exec_seq_continue *)
    (* TODO: ici l'hypothèse d'induction IHIBIS1 n'est pas utilisable à cause de OFIN trop restrictive *)
    try_simplify_someHyps.
    inv MIB.
    admit.
  - (* exec_cond *)
    try_simplify_someHyps.
    inv MIB.
     admit.*)
Admitted.

Theorem plus_simulation s1 t s1':
  step ge s1 t s1' ->
  forall s2 (MS: match_states s1 s2),
  exists s2',
     plus RTL.step tge s2 t s2'
  /\ match_states s1' s2'.
Proof.
  destruct 1; intros; inv MS.
  - eapply dupmap_correct in DUPLIC; eauto.
    destruct DUPLIC as (ib' & FNC & MIB).
    try_simplify_someHyps. destruct STEP as (rs' & m' & fin & IBIS & FS).
    admit.
    (*intros; exploit iblock_step_simulation; eauto.*)
  (* exec_function_internal *)
  - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split.
    + eapply plus_one. apply RTL.exec_function_internal.
      erewrite <- preserv_fnstacksize; eauto.
    + erewrite <- preserv_fnparams; eauto.
      eapply match_states_intro; eauto.
      apply dupmap_entrypoint. assumption.
  (* exec_function_external *)
  - inversion TRANSF as [|]; subst. eexists. split.
    + eapply plus_one. econstructor.
      eapply external_call_symbols_preserved; eauto. apply senv_preserved.
    + constructor. assumption.
  (* exec_return *)
  - inversion STACKS as [|a1 al b1 bl H1 HL]; subst.
    destruct b1 as [res' f' sp' pc' rs'].
    eexists. split.
    + eapply plus_one. constructor.
    + inv H1. econstructor; eauto.
(*Qed.*)
Admitted.

Theorem transf_program_correct:
  forward_simulation (semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_plus with match_states.
  - eapply senv_preserved.
  - eapply transf_initial_states.
  - eapply transf_final_states.
  - eapply plus_simulation.
Qed.

End RTL_SIMULATES_BTL.