Module AuxLDSim

Require Import Coqlib Globalenvs Values AST.
Require Import Blockset Footprint GMemory MemAux MemClosures
        InteractionSemantics Injections LDSimDefs LDSim ReachClose.

Auxilliary ldsim definition: with reach-close, we are able to give a RGSim-like simulation

Record config_ldsim_aux {sl tl: Language}
       (index: Type)
       (index_order: index -> index -> Prop)
       (sfl tfl: freelist)
       (sG: G sl)
       (tG: G tl)
       (sge: Genv.t (F sl) (V sl))
       (tge: Genv.t (F tl) (V tl))
       (match_state: bool -> index -> Mu -> FP.t -> FP.t ->
                     ((core sl) * gmem) -> ((core tl) * gmem) -> Prop): Prop :=
  {
    index_wf: well_founded index_order;
    
    wd_mu: forall b i mu Hfp Lfp Hc Lc,
        match_state b i mu Hfp Lfp Hc Lc ->
        Bset.inject (inj mu) (SharedSrc mu) (SharedTgt mu) /\
        no_overlap sfl (SharedSrc mu) /\
        no_overlap tfl (SharedTgt mu)
    ;

    match_mu_ge: forall b i mu Hfp Lfp Hc Lc,
      match_state b i mu Hfp Lfp Hc Lc ->
      ge_init_inj mu sge tge
    ;
      

    match_HG: forall b i mu Hfp Lfp Hcore Hm Lcore Lm,
        match_state b i mu Hfp Lfp (Hcore, Hm) (Lcore, Lm) ->
        HG sfl mu Hfp Hm;

    match_init: forall mu id argSrc argTgt score,
        ge_init_inj mu sge tge ->
        G_args (SharedSrc mu) argSrc ->
        arg_rel (inj mu) argSrc argTgt ->
        init_core sl sG id argSrc = Some score ->
        exists tcore,
          init_core tl tG id argTgt = Some tcore /\
          (forall sm tm,
              init_gmem sl sge sm ->
              init_gmem tl tge tm ->
              local_init_rel mu sfl sm tfl tm ->
              forall sm' tm',
                HLRely sfl tfl mu sm sm' tm tm' ->
                exists i, match_state true i mu FP.emp FP.emp (score, sm') (tcore, tm'))
    ;
    
    match_tau_step: forall i mu Hfp Lfp Hcore Hm Lcore Lm Hfp' Hcore' Hm',
        match_state true i mu Hfp Lfp (Hcore, Hm) (Lcore, Lm) ->
        (step sl) sG sfl Hcore Hm Hfp' Hcore' Hm' ->
        (
          (exists i',
              index_order i' i /\
              match_state true i' mu (FP.union Hfp Hfp') Lfp (Hcore', Hm') (Lcore, Lm))
          \/
          (exists i' Lfp' Lcore' Lm',
              plus (step tl tG tfl) Lcore Lm Lfp' Lcore' Lm' /\
              LfpG' tfl mu (FP.union Hfp Hfp') (FP.union Lfp Lfp') /\
              match_state true i' mu (FP.union Hfp Hfp') (FP.union Lfp Lfp') (Hcore', Hm') (Lcore', Lm'))
        )
    ;

    match_at_external: forall i mu Hfp Lfp Hcore Hm Lcore Lm f sg argSrc,
        match_state true i mu Hfp Lfp (Hcore, Hm) (Lcore, Lm) ->
        (at_external sl) sG Hcore = Some (f, sg, argSrc) ->
        G_args (SharedSrc mu) argSrc /\
        exists i' argTgt,
          (at_external tl) tG Lcore = Some (f, sg, argTgt) /\
          arg_rel (inj mu) argSrc argTgt /\
          LG' tfl mu Hfp Hm Lfp Lm /\
          match_state false i' mu FP.emp FP.emp (Hcore, Hm) (Lcore, Lm)
    ;
    
    match_after_external: forall i mu Hcore Hm Lcore Lm oresSrc Hcore' oresTgt,
        match_state false i mu FP.emp FP.emp (Hcore, Hm) (Lcore, Lm) ->
        G_oarg (SharedSrc mu) oresSrc ->
        (after_external sl) Hcore oresSrc = Some Hcore' ->
        ores_rel (inj mu) oresSrc oresTgt ->
        exists Lcore',
          (after_external tl) Lcore oresTgt = Some Lcore' /\
          (forall Hm' Lm', HLRely sfl tfl mu Hm Hm' Lm Lm' ->
                      exists i', match_state true i' mu FP.emp FP.emp (Hcore', Hm') (Lcore', Lm'))
    ;

    match_halt: forall i mu Hfp Lfp Hcore Hm Lcore Lm resSrc,
        match_state true i mu Hfp Lfp (Hcore, Hm) (Lcore, Lm) ->
        (halt sl) Hcore = Some resSrc ->
        G_arg (SharedSrc mu) resSrc /\
        exists resTgt,
          (halt tl) Lcore = Some resTgt /\
          res_rel (inj mu) resSrc resTgt /\
          LG' tfl mu Hfp Hm Lfp Lm
  }.

Lemma config_rc_ldsim_ldsimaux:
  forall sl tl index index_order sfl tfl sG tG sge tge R I,
    @config_ldsim sl tl index index_order sfl tfl sG tG sge tge R ->
    rc_inv sG sge I ->
    wd sl ->
    exists R', config_ldsim_aux index index_order sfl tfl sG tG sge tge R'.

Definition ldsim_aux {sl tl: Language}
           (su: comp_unit sl) (tu: comp_unit tl) : Prop :=
  forall sG sge tG tge sfl tfl,
    init_genv sl su sge sG ->
    init_genv tl tu tge tG ->
    Genv.genv_next sge = Genv.genv_next tge ->
    exists index index_order match_state,
      config_ldsim_aux index index_order sfl tfl sG tG sge tge match_state.

Theorem ldsim_rc_ldsim_aux:
  forall (sl tl: Language) (su: comp_unit sl) (tu: comp_unit tl),
    ldsim su tu ->
    wd sl ->
    reach_close su ->
    ldsim_aux su tu.