Require Import InteractionSemantics GlobDefs Footprint Injections GAST ETrace GlobUSim NPSemantics SimEtr GlobSim GSimDefs GDefLemmas USimDRF.

Simulation implies Refinement

Local Notation "{-| PC , T }" :=
  ({|thread_pool := thread_pool PC; cur_tid := T;gm := gm PC; atom_bit := atom_bit PC |}) (at level 70,right associativity).

Section usim_diverge.
  Variable SGE TGE:GlobEnv.t.
  Variable I:Type.
  Variable ord:I->I->Prop.
  Variable R:I->Mu->FP.t->FP.t->@ProgConfig SGE->@ProgConfig TGE->Prop.
  Hypothesis usim: GConfigUSim I ord R.
  
  
  Lemma tau_plus_star_step:
    forall ge pc fp pc',
      tau_plus np_step pc fp pc'->
      exists fp1 fp2 pc1,
        tau_star np_step pc fp1 pc1 /\
        @np_step ge pc1 tau fp2 pc' /\
        FP.union fp1 fp2 = fp.
  Lemma usim_Sdiverge_inva:
    forall i mu fpS fpT spc tpc,
      R i mu fpS fpT spc tpc->
      Sdiverge TGE tpc->
      exists tpc1 fpT1 tpc2 fpT2 o,
          (o = tau \/ o = sw) /\
          tau_star np_step tpc fpT1 tpc1 /\
          np_step tpc1 o fpT2 tpc2 /\ Sdiverge TGE tpc2 /\
          exists spc1 fpS1 spc2 fpS2,
            tau_star np_step spc fpS1 spc1 /\
            np_step spc1 o fpS2 spc2 /\
            exists i' fpS' fpT',
              R i' mu fpS' fpT' spc2 tpc2.


  Lemma tau_star_cons_Sdiverge:
    forall ge pc fp pc',
      tau_star np_step pc fp pc'->
      Sdiverge ge pc'->
      Sdiverge ge pc.

  Lemma tau_star_cons_step_non_evt_plus:
    forall ge pc fp pc' fp' pc'' o,
      o = tau \/ o = sw ->
      tau_star (@np_step ge) pc fp pc'->
      np_step pc' o fp' pc''->
      non_evt_plus np_step pc (FP.union fp fp') pc''.
  Lemma usim_Sdiverge_preserve:
    forall i mu fpS fpT spc tpc,
      R i mu fpS fpT spc tpc->
      Sdiverge TGE tpc->
      Sdiverge SGE spc.

  Lemma tau_star_non_evt_star{ge}:
    forall (step:@ProgConfig ge->glabel->FP.t->@ProgConfig ge->Prop) pc fp pc',
      tau_star step pc fp pc'->
      non_evt_star step pc fp pc'.

  
  Lemma non_evt_star_cons{ge}:
    forall (step:@ProgConfig ge->glabel->FP.t->@ProgConfig ge->Prop) s s' s'' fp fp',
      non_evt_star step s fp s' ->
      non_evt_star step s' fp' s'' ->
      non_evt_star step s (FP.union fp fp')s''.
  Inductive non_evt_starN {State:Type}:(State->glabel->FP.t->State->Prop)->nat->State->FP.t->State->Prop:=
  | ne_star_refl: forall step s,
      @non_evt_starN State step 0 s FP.emp s
  | ne_star_step: forall step n s1 fp1 s2 fp2 s3,
      step s1 tau fp1 s2 \/ step s1 sw fp1 s2 ->
      @non_evt_starN State step n s2 fp2 s3 ->
      non_evt_starN step (S n)s1 (FP.union fp1 fp2) s3.
  Lemma non_evt_star_N_equiv{State:Type}:
    forall step s fp s',
      @non_evt_star State step s fp s' <-> exists n,non_evt_starN step n s fp s'.
  Ltac ccut H :=
    match type of H with
    | ?A -> ?B => enough(B);[clear H|apply H]
    end.

  Lemma usim_refine_done:
    forall j i mu fpS fpT spc tpc,
        R i mu fpS fpT spc tpc->
        forall fpT1 tpc1,
          non_evt_starN np_step j tpc fpT1 tpc1->
          final_state tpc1->
          SEtr SGE spc Behav_done.

  Lemma usim_refine_abort:
    forall j i mu fpS fpT spc tpc,
        R i mu fpS fpT spc tpc->
        forall fpT1 tpc1,
          non_evt_starN np_step j tpc fpT1 tpc1->
          np_abort tpc1->
          SEtr SGE spc Behav_abort.


  Lemma usim_refine_cons:
    forall j i mu fpS fpT spc tpc,
      R i mu fpS fpT spc tpc->
      forall fpT1 tpc1 v tpc2,
        non_evt_starN np_step j tpc fpT1 tpc1->
        np_step tpc1 (evt v) FP.emp tpc2->
        exists k fpS1 spc1 spc2,
          non_evt_star np_step spc fpS1 spc1 /\
          np_step spc1 (evt v) FP.emp spc2 /\
          R k mu FP.emp FP.emp spc2 tpc2.
  Lemma usim_refine:
      forall i mu fpS fpT spc tpc,
        R i mu fpS fpT spc tpc->
        forall b,
          SEtr TGE tpc b->
          SEtr SGE spc b.
End usim_diverge.

Main result: upward simulation implies NP-refinement

Theorem USim_Refine:
  forall NL (L: @langs NL) (sprog tprog: prog L),
    GlobUSim sprog tprog ->
    np_prog_refine sprog tprog.

Lemma np_safe_config_cons:
  forall ge pc l fp pc',
    star np_step pc l fp pc'->
    @np_safe_config ge pc->
    np_safe_config pc'.
Lemma np_safe_config_safe_state:
  forall ge pc,
    @np_safe_config ge pc <->
    safe_state np_step np_abort pc.
Inductive starN {ge}: nat -> @ProgConfig ge->list glabel ->FP.t->@ProgConfig ge ->Prop:=
  | star0:forall s,starN 0 s nil FP.emp s
  | star_step':forall i s1 e fp1 s2 l fp2 s3,
      np_step s1 e fp1 s2->
      starN i s2 l fp2 s3->
      starN (S i) s1 (cons e l) (FP.union fp1 fp2) s3.
Lemma star_starN_equiv:
    forall ge pc pc' l fp,
      star (@np_step ge) pc l fp pc' <-> exists i,starN i pc l fp pc'.
Lemma USim_Safe_config':
  forall sge tge I ord match_state,
    @GConfigUSim sge tge I ord match_state->
    forall i mu fpS fpT spc tpc,
    match_state i mu fpS fpT spc tpc->
    safe_state np_step np_abort tpc.
Lemma USim_Safe_Config:
  forall NL L sprog tprog,
    @GlobUSim NL L sprog tprog->
    forall mu sgm sge spc tgm tge tpc,
      InitRel mu sge tge sgm tgm->
      init_config sprog sgm sge spc spc.(cur_tid)->
      init_config tprog tgm tge tpc tpc.(cur_tid)->
      spc.(cur_tid) = tpc.(cur_tid)->
      np_safe_config tpc.