Module TSOGlobUSim

From mathcomp.ssreflect Require Import fintype.
Require Import Coqlib Maps.
Require Import AST Integers Floats Values Events Globalenvs Smallstep.
Require Import Locations Stacklayout Conventions.

Require Import Asm.

Require Import CUAST FMemOpFP ValFP Op_fp String val_casted helpers.

Require Import Footprint GMemory FMemory TSOMem.
Require Import GAST GlobDefs ETrace Blockset.
Require Import loadframe.

Require Import ASM_local.
Require Import AsmLang.
Require Import AsmTSO.

Require Import Coq.Lists.Streams.

Require Import TSOGlobSem GlobSemantics.

Local Notation footprint := FP.t.
Local Notation empfp := FP.emp.

Record TSOGConfigUSim
       {sge: GlobEnv.t}
       {tge: TSOGlobEnv.t}
       (match_state: @ProgConfig sge -> @TSOProgConfig tge -> Prop) : Prop :=
  {
    match_taustep:
      forall spc tpc,
        match_state spc tpc ->
        forall tpc' fpT',
          tso_globstep tpc tau fpT' tpc' ->
          exists spc' fpS',
            tau_star glob_step spc fpS' spc'
            /\
            (match_state spc' tpc'
             \/
             GlobSemantics.abort spc')
    ;

    match_swstep:
      forall spc tpc,
        match_state spc tpc ->
        forall tpc',
          tso_globstep tpc sw empfp tpc' ->
          exists spc',
            glob_step spc ETrace.sw empfp spc'
            /\ match_state spc' tpc'
    ;

    match_unbufferstep:
      forall spc tpc,
        match_state spc tpc ->
        forall t' tpc',
          tso_globstep tpc (ub t') empfp tpc' ->
          match_state spc tpc'
    ;

    match_eventstep:
      forall spc tpc,
        match_state spc tpc ->
        forall v tpc',
          tso_globstep tpc (evt v) empfp tpc' ->
          exists spc',
            glob_step spc (ETrace.evt v) empfp spc'
            /\ match_state spc' tpc'
    ;

    match_final:
      forall spc tpc,
        match_state spc tpc ->
        final_state tpc ->
        GlobDefs.final_state spc
    ;

    match_abort:
      forall spc tpc,
        match_state spc tpc ->
        TSOGlobSem.abort tpc ->
        exists spc' fpS,
          tau_star glob_step spc fpS spc' /\
          GlobSemantics.abort spc'
    ;
    
  }.


Definition TSOGlobUSim {NL: nat} {L: @langs NL}
           (pSC: prog L)
           (pTSO: tsoprog) : Prop :=
  forall sgm sge spc t tgm tge tpc,
    tso_sc_initRel sge tge sgm tgm ->
    init_config pSC sgm sge spc t ->
    ~ DRF.star_race_config spc ->
    safe_state glob_step abort spc ->
    tso_initconfig pTSO tgm tge tpc t ->
    exists match_state,
      TSOGConfigUSim match_state /\
      match_state spc tpc.



Lemma tau_star_non_evt_star_app:
  forall state step (pc: state) fp pc' fp' pc'',
    tau_star step pc fp pc' ->
    non_evt_star step pc' fp' pc'' ->
    non_evt_star step pc (FP.union fp fp') pc''.

Lemma tau_star_star_step:
  forall state step (pc: state) fp pc',
    tau_star step pc fp pc' ->
    exists ll, star step pc ll fp pc'.

Lemma non_evt_star_star_step:
  forall state step (pc: state) fp pc',
    non_evt_star step pc fp pc' ->
    exists ll, star step pc ll fp pc'.

Lemma star_star_app:
  forall state step (pc: state) l1 fp pc' l2 fp' pc'',
    star step pc l1 fp pc' ->
    star step pc' l2 fp' pc'' ->
    star step pc (l1 ++ l2) (FP.union fp fp') pc''.

Lemma non_evt_star_sim:
  forall SGE TGE (spc: @ProgConfig SGE) (tpc: @TSOProgConfig TGE) match_state fp tpc',
    non_evt_star tso_etrstep tpc fp tpc' ->
    TSOGConfigUSim match_state ->
    match_state spc tpc ->
    ~ DRF.star_race_config spc ->
    safe_state glob_step abort spc ->
    exists fpS spc', non_evt_star glob_step spc fpS spc' /\ match_state spc' tpc'.
         
Theorem tso_globusim_refinement:
  forall NL L (pSC: @prog NL L) pTSO,
    TSOGlobUSim pSC pTSO ->
    tso_refine_sc pSC pTSO.