Require Import Coqlib Maps.
Require Import AST Integers Floats Values Events Globalenvs Smallstep.

Require Import CUAST.

Require Import Footprint GMemory TSOMem FMemOpFP.
Require Import GlobDefs GAST ETrace LDSimDefs.

Require Import ASM_local AsmLang AsmTSO TSOGlobSem.
Require Import InteractionSemantics.
Require Export RGRels.

Local Notation footprint := FP.t.


Definition conflict_bi (fp: footprint) (bi: buffer_item) : Prop :=
  FP.conflict fp (bi_footprint bi).

Inductive conflictc
          (t: tid) (fp: footprint) (B: buffers): Prop :=
| Conflictc: forall bi t',
    t' <> t ->
    In bi (B t') ->
    conflict_bi fp bi ->
    conflictc t fp B.

    
Definition fpmatchc (sfp tfp: footprint): Prop := FP.subset tfp sfp.

Client module simulation

Section ClientSim.

  Variable Rc: tid -> stRel.
  Variable Gc: tid -> stRel.
  Variable Ic: stInv.

  Record clientsim_properties
         {sl: Language}
         (sG: G sl)
         (sge: Genv.t (F sl) (V sl))
         (tge: genv)
         (match_state: tid -> (core sl * gmem) -> (AsmTSO.core * tsomem) -> Prop): Prop :=
    {
      match_init:
         forall id args tc,
           AsmTSO.init_core tge id args = Some tc ->
           exists sc,
             init_core sl sG id args = Some sc /\
             (forall t sm tm,
                 Ic sm tm ->
                 sep_obj_client_block sm ->
                 match_state t (sc, sm) (tc, tm))
      ;

      match_init_none:
        forall id args,
          AsmTSO.init_core tge id args = None ->
          init_core sl sG id args = None
      ;

      match_tau:
        forall t sc sm tc tm fl b m tfp tc' b' m',
          match_state t (sc, sm) (tc, tm) ->
          tso_buffers tm t = b ->
          memory tm = m ->
          tm_alloc_not_fl tm fl t -> rel_tm_gm_vb sm tm fl t ->
          tsostep tge fl tc (b, m) tfp tc' (b', m') ->
          let tm' := (mktsomem (tupdate t b' (tso_buffers tm)) m') in
          (exists sfp sc' sm',
              step sl sG fl sc sm sfp sc' sm'
              /\ (
                (~ conflictc t tfp (tso_buffers tm)
                 /\ fpmatchc sfp tfp
                 /\ Gc t sm tm sm' tm'
                 /\ match_state t (sc', sm') (tc', tm')
                 /\ tm_alloc_not_fl tm' fl t
                 /\ rel_tm_gm_vb sm' tm' fl t)
                \/
                (conflictc t tfp (tso_buffers tm)
                 /\ fpmatchc sfp tfp)
              )
          )
          \/
          (forall FP sc'' sm'', ~ step sl sG fl sc sm FP sc'' sm'')
      ;

      match_at_external:
        forall t sc sm tc tm,
          match_state t (sc, sm) (tc, tm) ->
          AsmTSO.at_external tge tc = at_external sl sG sc
      ;
      
      match_after_external:
        forall t sc sm tc tm ores tc',
          match_state t (sc, sm) (tc, tm) ->
          AsmTSO.after_external tc ores = Some tc' ->
          exists sc', after_external sl sc ores = Some sc'
                 /\ match_state t (sc', sm) (tc', tm)
      ;

      match_after_external_none:
        forall t sc sm tc tm ores,
          match_state t (sc, sm) (tc, tm) ->
          AsmTSO.after_external tc ores = None ->
          after_external sl sc ores = None
      ;
      
      match_halted:
        forall t sc sm tc tm,
          match_state t (sc, sm) (tc, tm) ->
          AsmTSO.halt tc = halt sl sc
      ;
       
      
      match_abort:
        forall t sc sm tc tm fl m,
          match_state t (sc, sm) (tc, tm) ->
          tm_alloc_not_fl tm fl t -> rel_tm_gm_vb sm tm fl t ->
          (forall t', tso_buffers tm t' = nil) ->
          memory tm = m ->
          (forall fp tc' b' m',
              ~ (tsostep tge fl tc (nil, m) fp tc' (b', m') /\
                 exists m'', apply_buffer b' m' = Some m'')) ->
          (forall FP sc' sm', ~ step sl sG fl sc sm FP sc' sm')
          \/ (forall fm, ~ FMemory.embed m fl fm)
      ;

      match_abort_after_external:
        forall t sc sm tc tm ores,
          match_state t (sc, sm) (tc, tm) ->
          AsmTSO.after_external tc ores = None ->
          after_external sl sc ores = None
      ;

      match_rely:
        forall t sc sm tc tm sm' tm',
          match_state t (sc, sm) (tc, tm) ->
          Rc t sm tm sm' tm' ->
          sep_obj_client_block sm' ->
          match_state t (sc, sm') (tc, tm')
      ;

      match_no_entatom:
        forall t sc sm tc tm fnid sg args,
          match_state t (sc, sm) (tc, tm) ->
          at_external sl sG sc = Some (fnid, sg, args) ->
          fnid <> ent_atom
          /\ fnid <> ext_atom
      ;
          

    }.
  
End ClientSim.

Definition clientsim
           (Rc Gc: tid -> stRel) (Ic: stInv)
           (sl: Language)
           (scu: comp_unit sl)
           (tcu: AsmTSO.comp_unit) : Prop :=
  forall sge sG tge,
    init_genv sl scu sge sG ->
    AsmTSO.init_genv tcu tge ->
    genv_match _ _ sge tge ->
    exists match_state,
      clientsim_properties Rc Gc Ic sG sge tge match_state.

R/G/I for client modules

Lemma unchanged_on_sym:
  forall P gm gm',
    GMem.unchanged_on P gm gm' ->
    GMem.unchanged_on P gm' gm.

Definition buf_alloc_invalid (tm: tsomem) : Prop :=
  forall t b lo hi,
    In (BufferedAlloc b lo hi) (tso_buffers tm t) ->
    ~ GMem.valid_block (memory tm) b.

Definition buf_alloc_norep (tm: tsomem) : Prop :=
  forall t t' i j b lo hi lo' hi',
    List.nth_error (tso_buffers tm t) i = Some (BufferedAlloc b lo hi) ->
    List.nth_error (tso_buffers tm t') j = Some (BufferedAlloc b lo' hi') ->
    t = t' /\ i = j.

Record Ic (sm: gmem) (tm: tsomem) : Prop :=
  {
    Ic_ub_safe:
      unbuffer_safe tm
    ;

    Ic_no_conflict_bi:
      forall b ofs t1 t2,
        t1 <> t2 ->
        ~ obj_mem sm b ofs ->
        in_buffer (tso_buffers tm t1) b ofs ->
        in_buffer (tso_buffers tm t2) b ofs ->
        False;
      
    Ic_mem_eq:
      forall t tgm',
        apply_buffer (tso_buffers tm t) (memory tm) = Some tgm' ->
        forall b ofs,
          ~ obj_mem sm b ofs ->
          (forall t', t' <> t -> ~ in_buffer (tso_buffers tm t') b ofs) ->
          eq_on_loc b ofs sm tgm'
    ;

    Ic_buf_alloc_invalid:
      buf_alloc_invalid tm;

    Ic_buf_alloc_norep:
      buf_alloc_norep tm;
  }.

Definition Rc (t: tid) (sm: gmem) (tm: tsomem) (sm': gmem) (tm': tsomem) : Prop :=
  Ic sm tm /\ Ic sm' tm'.

Definition Gc (t: tid) (sm: gmem) (tm: tsomem) (sm': gmem) (tm': tsomem) : Prop :=
  Ic sm tm /\ Ic sm' tm'
  /\ (forall b ofs, obj_mem sm b ofs <-> obj_mem sm' b ofs)
  /\ (forall b ofs, obj_mem sm b ofs -> eq_on_loc b ofs sm sm')
  /\ memory tm = memory tm'
  /\ (exists bis, tso_buffers tm' = tupdate t (tso_buffers tm t ++ bis) (tso_buffers tm)
     /\
     (forall b ofs, in_buffer bis b ofs ->
                    (~ obj_mem sm b ofs )))
     /\ GMem.forward sm sm'.

Lemma Ic_unbuffer_safe:
  forall sm tm,
    Ic sm tm -> unbuffer_safe tm.

Lemma Ic_sta:
  forall t : tid, Sta Ic (Gc t).

Lemma Gc_implies_Rc:
  forall t t' : tid, Implies (Gc t) (Rc t').


Lemma unbuffer_safe_apply_buffer :
  forall bfs t m,
    unbuffer_safe {| tso_buffers := bfs; memory := m |} ->
    exists m', apply_buffer (bfs t) m = Some m'.

Lemma eq_on_loc_trans:
  forall b ofs m1 m2 m3,
    eq_on_loc b ofs m1 m2 ->
    eq_on_loc b ofs m2 m3 ->
    eq_on_loc b ofs m1 m3.

Lemma eq_on_loc_sym:
  forall b ofs m1 m2,
    eq_on_loc b ofs m1 m2 -> eq_on_loc b ofs m2 m1.

Lemma app_eq_length_eq_inj:
  forall A (l1 l2 l1' l2': list A),
    length l1 = length l1' ->
    l1 ++ l2 = l1' ++ l2' ->
    l2 = l2'.
  
Lemma apply_buffer_item_eq_on_loc_preserve:
  forall bi gm1 gm2 b ofs gm1' gm2',
    eq_on_loc b ofs gm1 gm2 ->
    apply_buffer_item bi gm1 = Some gm1' ->
    apply_buffer_item bi gm2 = Some gm2' ->
    eq_on_loc b ofs gm1' gm2'.
  
Lemma apply_buffer_eq_on_loc_preserve:
  forall buf gm1 gm2 b ofs gm1' gm2',
    eq_on_loc b ofs gm1 gm2 ->
    apply_buffer buf gm1 = Some gm1' ->
    apply_buffer buf gm2 = Some gm2' ->
    eq_on_loc b ofs gm1' gm2'.

Lemma apply_buffer_item_eq_on_loc_other:
  forall bi gm gm' b ofs,
    apply_buffer_item bi gm = Some gm' ->
    ~ in_buffer_item bi b ofs ->
    eq_on_loc b ofs gm gm'.

Lemma apply_buffer_eq_on_loc_other:
  forall buf gm gm' b ofs,
    apply_buffer buf gm = Some gm' ->
    ~ in_buffer buf b ofs ->
    eq_on_loc b ofs gm gm'.

Lemma Ic_buf_alloc_invalid_norep_stable:
  forall tm t tm',
    buf_alloc_invalid tm ->
    buf_alloc_norep tm ->
    unbuffer tm t = Some tm' ->
    buf_alloc_invalid tm' /\ buf_alloc_norep tm'.
          
Lemma UBSta_Ic:
  UBSta Ic.

Lemma UBImplies_Rc:
  forall t : tid, UBImplies Ic (Rc t).




Lemma nth_error_split':
  forall A (l ls:list A) i a,
    nth_error (l++ls) i = Some a ->
    nth_error l i = Some a \/ ( nth_error ls (i-(length l)) = Some a /\ (i >= length l)%nat).
Lemma nth_error_nil:
  forall A i,
    @nth_error A nil i = None.
Lemma nth_error_cons_nil:
  forall A (bi bi':A) i,
    nth_error (bi::nil) i = Some bi' ->
    i = 0%nat /\ bi = bi'.

Local Ltac Hsimpl:=
  repeat match goal with
         | H1:?a,H2:?a->?b|-_=>specialize (H2 H1)
         | H:_/\_|-_=> destruct H
         | H:exists _,_|-_=>destruct H
         end.
Local Ltac Esimpl:=
  repeat match goal with
         | H:_|-_/\_=>split
         | H:_|-exists _,_=>eexists
         end.
Local Ltac ex_match:=
  repeat match goal with
         | H: match ?x with _ => _ end = _ |- _ => destruct x eqn:?Hx; try discriminate
         end;try congruence.
Local Ltac ex_match2:=
  repeat match goal with
         | H: context[match ?x with _ => _ end] |- _ => destruct x eqn:?Hx; try discriminate
         | H: _ |- context[match ?x with _ => _ end ] => destruct x eqn:?Hx;try discriminate
         end;try congruence;try contradiction.
Local Ltac ex_match3:=
  match goal with
    H: ?x = ?y |- context [?x] => rewrite H
  end.

Ltac solve_nth_error:=
  match goal with
  | H: nth_error (?x::nil) ?y = Some ?z |- _
    => eapply nth_error_cons_nil in H;Hsimpl;subst;
      match goal with
      | H : x = z |- _ => inv H
      end
  | H: nth_error (?l++?ls) ?i = Some ?a |- _ =>
    apply nth_error_split' in H as [|[]]
  end.
Ltac esolve_nth_error:=
  repeat solve_nth_error;subst;eauto.
Lemma alloc_norep_preserve:
  forall bufs m,
    buf_alloc_norep (mktsomem bufs m)->
    forall bi,
      match bi with
      |BufferedAlloc b0 lo0 hi0 =>
       forall t b lo hi, In (BufferedAlloc b lo hi)(bufs t) -> b <> b0
      |_ => True
      end ->
      forall t m',
        buf_alloc_norep (mktsomem (tupdate t (bufs t ++ (bi::nil)) bufs) m').