Module AsmClientSim

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

Require Import CUAST.

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

Require Import ASM_local AsmLang AsmTSO TSOGlobSem.
Require Import InteractionSemantics.
Require Import RGRels ClientSim SCSemLemmas TSOSemLemmas TSOMemLemmas.

Local Notation footprint := FP.t.

Lemma strip_fl_eq_fmem_eq:
  forall fm fm',
    strip fm = strip fm' ->
    Mem.freelist fm = Mem.freelist fm' ->
    fm = fm'.

Lemma helpers_i64ext_sem_det:
  forall ef vargs vres vres',
    helpers.i64ext_sem ef vargs vres ->
    helpers.i64ext_sem ef vargs vres' ->
    vres = vres'.
          
Lemma tupdate_update_same:
  forall t bufs,
    tupdate t (bufs t) bufs = bufs.

Lemma tupdate_update_get_same:
  forall t bufs buf,
    tupdate t buf bufs t = buf.

Lemma tupdate_update2:
  forall t buf buf' bufs,
    tupdate t buf (tupdate t buf' bufs) = tupdate t buf bufs.

Lemma emp_not_conflictc:
  forall t bufs, ~ conflictc t FP.emp bufs.

Lemma conflictc_ext:
  forall fp bufs bufs' t,
    conflictc t fp bufs ->
    (forall t', t' <> t -> bufs t' = bufs' t') ->
    conflictc t fp bufs'.

Lemma conflictc_union:
  forall fp1 fp2 bufs t,
    conflictc t (FP.union fp1 fp2) bufs ->
    conflictc t fp1 bufs \/ conflictc t fp2 bufs.

Lemma conflictc_union':
  forall fp1 fp2 bufs t,
    conflictc t fp1 bufs \/ conflictc t fp2 bufs ->
    conflictc t (FP.union fp1 fp2) bufs.

Lemma store_args_fp_in_stk:
  forall stk tys,
    exists locs,
      loadframe.store_args_fp stk tys = FP.Build_t Locs.emp Locs.emp locs Locs.emp /\
      (forall b ofs, Locs.belongsto locs b ofs -> b = stk).

Lemma conflict_store_args_conflict_alloc:
  forall t stk tys bufs lo hi,
    conflictc t (loadframe.store_args_fp stk tys) bufs ->
    conflictc t (tsoalloc_fp stk lo hi) bufs.

Lemma conflict_store_conflict_alloc:
  forall chunk stk ofs lo hi bufs t,
    conflictc t (store_fp chunk stk ofs) bufs ->
    conflictc t (tsoalloc_fp stk lo hi) bufs.

Lemma Pallocframe_succeed_link_ra_inrange:
  forall ge f sz ofs_ra ofs_link rs m rs' m',
    exec_instr ge f (Pallocframe sz ofs_ra ofs_link) rs m = AsmLang.Next rs' m' ->
    (Ptrofs.unsigned ofs_ra + size_chunk Mptr <= sz /\ (align_chunk Mptr | Ptrofs.unsigned ofs_ra)) /\
    (Ptrofs.unsigned ofs_link + size_chunk Mptr <= sz /\ (align_chunk Mptr | Ptrofs.unsigned ofs_link)).

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 Gc_trans:
  forall t sm1 tm1 sm2 tm2 sm3 tm3,
    Gc t sm1 tm1 sm2 tm2 ->
    Gc t sm2 tm2 sm3 tm3 ->
    Gc t sm1 tm1 sm3 tm3.

Lemma Gc_refl:
  forall t sm tm,
    Ic sm tm ->
    Gc t sm tm sm tm.

Lemma eq_validity_eq_nextblock:
  forall fl m m' fm fm',
    (forall b n, MemAux.get_block fl n = b -> In b (GMem.validblocks m) <-> In b (GMem.validblocks m')) ->
    embed m fl fm ->
    embed m' fl fm' ->
    Mem.nextblock fm = Mem.nextblock fm'.

Lemma rel_vb_nextblock_eq:
  forall m bufs tm fl t,
    rel_tm_gm_vb (strip m) (mktsomem bufs (strip tm)) fl t ->
    (forall t', bufs t' = nil) ->
    Mem.freelist m = Mem.freelist tm ->
    Mem.freelist m = fl ->
    Mem.nextblock m = Mem.nextblock tm.
          
Record meminv (t: tid) (fl: MemAux.freelist) (sgm: gmem) (bufs: buffers) (tgm: gmem) : Prop :=
  {
    meminv_Ic: Ic sgm (mktsomem bufs tgm);
    meminv_sep: sep_obj_client_block sgm;
    meminv_rel_vb: rel_tm_gm_vb sgm (mktsomem bufs tgm) fl t;
    meminv_alloc_local: tm_alloc_not_fl (mktsomem bufs tgm) fl t;
  }.


Definition fmemop {Res: Type}: Type := mem -> FP.t -> Res -> mem -> Prop.
Definition tsofmemop {Res: Type}: Type := tsofmem -> FP.t -> Res -> tsofmem -> Prop.

Definition memops_refine {Res: Type} (opSrc: @fmemop Res) (opTgt: @tsofmemop Res) : Prop :=
  forall t fl sgm bufs tgm sfm tfm,
    meminv t fl sgm bufs tgm ->
    embed sgm fl sfm ->
    embed tgm fl tfm ->
    let tbfm := mktsofmem (bufs t) tfm in
    forall tfp tres tbfm',
      opTgt tbfm tfp tres tbfm' ->
      (exists sfp sres sfm',
          opSrc sfm sfp sres sfm' /\
          let sgm' := strip sfm' in
          let tgm' := strip (fmemory tbfm') in
          let buf' := tbuffer tbfm' in
          let bufs' := tupdate t buf' bufs in
          ((~ conflictc t tfp bufs) /\
           fpmatchc sfp tfp /\
           sres = tres /\
           meminv t fl sgm' bufs' tgm' /\
           Gc t sgm (mktsomem bufs tgm) sgm' (mktsomem bufs' tgm'))
          \/
          (conflictc t tfp bufs /\
           fpmatchc sfp tfp))
      \/
      (forall sfp sres sfm', ~ opSrc sfm sfp sres sfm').


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.

    
Lemma meminv_fl_embed_nextblockeq:
  forall m m' t fl bfs,
    meminv t fl m bfs m'->
    forall m2 fm1 fm2,
      embed m fl fm1 ->
      apply_buffer (bfs t) m' = Some m2 ->
      embed m2 fl fm2 ->
      fm1.(Mem.nextblockid) = fm2.(Mem.nextblockid).

Lemma inbuffer_split:
  forall bf1 bf2 b ofs,
    in_buffer (bf1++bf2) b ofs ->
    in_buffer bf1 b ofs \/ in_buffer bf2 b ofs.

Lemma strip_fold:
  forall fm,
    {|
      GMem.mem_contents := Mem.mem_contents fm;
      GMem.mem_access := Mem.mem_access fm;
      GMem.validblocks := Mem.validblocks fm;
      GMem.access_max := Mem.access_max fm;
      GMem.invalid_noaccess := Mem.invalid_noaccess fm;
      GMem.contents_default := Mem.contents_default fm |} = strip fm.
Lemma unbuffer_forward:
  forall tm,
    buf_alloc_invalid tm ->
    buf_alloc_norep tm ->
    forall t tm' ,
      unbuffer tm t = Some tm'->
      GMem.forward (memory tm)(memory tm').
Lemma apply_buffer_forward:
   forall tm,
    buf_alloc_invalid tm ->
    buf_alloc_norep tm ->
    forall t bf ls tm',
      tso_buffers tm t = bf++ls->
      apply_buffer bf (memory tm) = Some tm' ->
      GMem.forward (memory tm) tm'.


Lemma tsoalloc_thread_local_norep:
  forall tm lo hi tm' b,
    tsoalloc tm lo hi (tm',b) ->
    forall b' lo hi,
      In (BufferedAlloc b' lo hi) (tbuffer tm) ->
      b' <> b.
Lemma alloc_refine:
  forall lo hi,
    let opSrc := fun sfm fp stk sfm' =>
                   Mem.alloc sfm lo hi = (sfm', stk) /\ fp = alloc_fp sfm lo hi in
    let opTgt := fun tbfm fp stk tbfm' =>
                   tsoalloc tbfm lo hi (tbfm', stk) /\ fp = tsoalloc_fp stk lo hi in
    @memops_refine block opSrc opTgt.
Local Opaque Mem.alloc.

Lemma store_refine:
  forall chunk b ofs v,
    let opSrc := fun sfm fp res sfm' =>
                   Mem.store chunk sfm b ofs v = Some sfm' /\ fp = store_fp chunk b ofs in
    let opTgt := fun tbfm fp res tbfm' =>
                   tsostore chunk tbfm b ofs v = Some tbfm' /\ fp = store_fp chunk b ofs in
    @memops_refine unit opSrc opTgt.
Local Opaque Mem.store.

Lemma free_refine:
  forall b lo hi,
    let opSrc := fun sfm fp res sfm' =>
                   Mem.free sfm b lo hi = Some sfm' /\ fp = free_fp b lo hi in
    let opTgt := fun tbfm fp res tbfm' =>
                   tsofree tbfm b lo hi = Some tbfm' /\ fp = free_fp b lo hi in
    @memops_refine unit opSrc opTgt.
Local Opaque Mem.free.

Lemma load_refine:
  forall chunk b ofs,
    let opSrc := fun sfm fp v sfm' =>
                   sfm = sfm' /\ Mem.load chunk sfm b ofs = Some v /\ fp = load_fp chunk b ofs in
    let opTgt := fun tbfm fp v tbfm' =>
                   tbfm = tbfm' /\ tsoload chunk tbfm b ofs = Some v /\ fp = load_fp chunk b ofs in
    @memops_refine val opSrc opTgt.

Local Opaque Mem.load.
Lemma meminv_client_loc_forward:
  forall sfm tfm bufs t b ofs tgm',
    let fl := Mem.freelist sfm in
    let sm := strip sfm in
    let tm := strip tfm in
    Mem.freelist sfm = Mem.freelist tfm ->
    meminv t fl sm bufs tm ->
    client_mem sm b ofs ->
    apply_buffer (bufs t) tm = Some tgm' ->
    GMem.valid_block tgm' b ->
    GMem.perm sm b ofs Memperm.Cur Memperm.Nonempty ->
    GMem.perm tgm' b ofs Memperm.Cur Memperm.Nonempty.
Lemma tso_valid_pointer_matchc:
  forall tfm sm bufs t b ofs,
    meminv t (Mem.freelist sm)(strip sm) bufs (strip tfm) ->
    Mem.freelist sm = Mem.freelist tfm->
    Mem.valid_pointer sm b ofs = true ->
    forall tgm',
      apply_buffer (bufs t)(strip tfm) = Some tgm'->
      GMem.valid_block tgm' b ->
      tso_valid_pointer {|tbuffer:=bufs t;fmemory := tfm|} b ofs = true.
Lemma tso_weak_valid_pointer_matchc:
  forall tfm sm bufs t b ofs,
    meminv t (Mem.freelist sm)(strip sm) bufs (strip tfm) ->
    Mem.freelist sm = Mem.freelist tfm->
    Mem.weak_valid_pointer sm b ofs = true ->
    forall tgm',
      apply_buffer (bufs t)(strip tfm) = Some tgm'->
      GMem.valid_block tgm' b ->
      TSOAuxDefs.tso_weak_valid_pointer {|tbuffer:=bufs t;fmemory := tfm|} b ofs = true.
Lemma tso_weak_valid_pointer_fp_matchc:
  forall tfm sm bufs t b ofs,
    meminv t (Mem.freelist sm)(strip sm) bufs (strip tfm) ->
    Mem.freelist sm = Mem.freelist tfm->
    TSOAuxDefs.tso_weak_valid_pointer {|tbuffer:=bufs t;fmemory := tfm|} b ofs = true ->
    Mem.weak_valid_pointer sm b ofs = true ->
    FP.subset (tso_weak_valid_pointer_fp {|tbuffer:=bufs t;fmemory := tfm|} b ofs)(weak_valid_pointer_fp sm b ofs).
Lemma meminv_compare_ints_fp_subset:
  forall sfm tfm bufs t v1 v2,
    let fl := Mem.freelist sfm in
    let sm := strip sfm in
    let tm := strip tfm in
    Mem.freelist sfm = Mem.freelist tfm ->
    meminv t fl sm bufs tm ->
    check_compare_ints v1 v2 sfm = true ->
    check_compare_ints_TSO v1 v2 (mktsofmem (bufs t) tfm) = true ->
    FP.subset (compare_ints_TSO_fp v1 v2 (mktsofmem (bufs t) tfm))
              (compare_ints_fp v1 v2 sfm).
Lemma meminv_compare_ints_not_conflict_eq:
  forall sfm tfm bufs t v1 v2 rs,
    let fl := Mem.freelist sfm in
    let sm := strip sfm in
    let tm := strip tfm in
    Mem.freelist sfm = Mem.freelist tfm ->
    meminv t fl sm bufs tm ->
    check_compare_ints v1 v2 sfm = true ->
    check_compare_ints_TSO v1 v2 (mktsofmem (bufs t) tfm) = true ->
    ~ conflictc t (compare_ints_TSO_fp v1 v2 (mktsofmem (bufs t) tfm)) bufs ->
    compare_ints v1 v2 rs sfm = compare_ints_TSO v1 v2 rs (mktsofmem (bufs t) tfm).
Lemma meminv_extcall_arg:
  forall t fl sm tm sfm tfm rs a fp v,
    meminv t fl sm (tso_buffers tm) (memory tm) ->
    embed sm fl sfm ->
    embed (memory tm) fl tfm ->
    extcall_arg_fp rs a fp ->
    extcall_arg rs {| tbuffer := tso_buffers tm t; fmemory := tfm |} a v ->
    (exists v',
        AsmLang.extcall_arg rs sfm a v' /\
        ((~ conflictc t fp (tso_buffers tm) /\ v' = v)
         \/ conflictc t fp (tso_buffers tm)))
    \/
    (forall v', ~ AsmLang.extcall_arg rs sfm a v').
  
Lemma meminv_extcall_arg_pair:
forall t fl sm tm sfm tfm rs a fp v,
    meminv t fl sm (tso_buffers tm) (memory tm) ->
    embed sm fl sfm ->
    embed (memory tm) fl tfm ->
    extcall_arg_pair_fp rs a fp ->
    extcall_arg_pair rs {| tbuffer := tso_buffers tm t; fmemory := tfm |} a v ->
    (exists v',
        AsmLang.extcall_arg_pair rs sfm a v' /\
        ((~ conflictc t fp (tso_buffers tm) /\ v' = v)
         \/ conflictc t fp (tso_buffers tm)))
    \/
    (forall v', ~ AsmLang.extcall_arg_pair rs sfm a v').

Lemma meminv_extcall_arguments:
  forall t fl sm tm sfm tfm rs sig args fp,
    meminv t fl sm (tso_buffers tm) (memory tm) ->
    embed sm fl sfm ->
    embed (memory tm) fl tfm ->
    extcall_arguments rs (mktsofmem (tso_buffers tm t) tfm) sig args ->
    extcall_arguments_fp rs sig fp ->
    (exists args',
        AsmLang.extcall_arguments rs sfm sig args' /\
        ((~ conflictc t fp (tso_buffers tm) /\ args' = args)
         \/ conflictc t fp (tso_buffers tm)))
    \/
    (forall args', ~ AsmLang.extcall_arguments rs sfm sig args').

Lemma store_args_refine:
  forall stk args tys,
    let opSrc := fun sfm fp (x:unit) sfm' =>
                   loadframe.store_args_fmem sfm stk args tys = Some sfm' /\
                   fp = loadframe.store_args_fp stk tys in
    let opTgt := fun tbfm fp (x:unit) tbfm' =>
                   store_args_fmem tbfm stk args tys = Some tbfm' /\
                   fp = loadframe.store_args_fp stk tys in
    memops_refine opSrc opTgt.

Lemma meminv_initialize:
  forall t fl sm bufs tm sfm tfm args tys z bm1 stk tsofm',
    meminv t fl sm bufs tm ->
    embed sm fl sfm ->
    embed tm fl tfm ->
    loadframe.args_len_rec args tys = Some z ->
    tsoalloc (mktsofmem (bufs t) tfm) 0 (4 * z) (bm1, stk) ->
    store_args_fmem bm1 stk args tys = Some tsofm' ->
    let bufs' := (tupdate t (tbuffer tsofm') bufs) in
    let tm' := (strip (fmemory tsofm')) in
    (exists sfm1 sfm',
        Mem.alloc sfm 0 (4 * z) = (sfm1, stk) /\
        loadframe.store_args_fmem sfm1 stk args tys = Some sfm' /\
        (Gc t sm (mktsomem bufs tm) (strip sfm') (mktsomem bufs' tm') /\
         meminv t fl (strip sfm') bufs' tm'
         \/
         conflictc t (tsoalloc_fp stk 0 (4 * z)) bufs)
    )
    \/
    loadframe.store_args_fmem (fst (Mem.alloc sfm 0 (4 * z))) stk args tys = None.

Lemma store_args_succeed_tso:
  forall args tys z m stk m' tfm,
    loadframe.args_len_rec args tys = Some z ->
    loadframe.store_args_fmem m stk args tys = Some m' ->
    exists tfm',
      store_args_fmem (buffer_insert {| tbuffer := nil; fmemory := tfm |}
                                     (BufferedAlloc (Mem.nextblock tfm) 0 (4 * z)))
                      (Mem.nextblock tfm) args tys = Some tfm'
      /\ exists m'', apply_buffer (tbuffer tfm') (strip (fmemory tfm')) = Some m''.

Lemma meminv_load_refine':
  forall sm tm fl sfm bufs t chunk b ofs v,
    embed sm fl sfm ->
    (forall t', bufs t' = nil) ->
    meminv t fl sm bufs tm ->
    Mem.load chunk sfm b ofs = Some v ->
    load chunk tm b ofs = Some v.

Lemma meminv_store_refine':
  forall sm tm fl sfm tfm bufs t chunk b ofs v sfm',
    embed sm fl sfm ->
    embed tm fl tfm ->
    (forall t', bufs t' = nil) ->
    meminv t fl sm bufs tm ->
    Mem.store chunk sfm b ofs v = Some sfm' ->
    exists buf, tsostore chunk (mktsofmem (bufs t) tfm) b ofs v = Some (mktsofmem buf tfm) /\
           exists tm', apply_buffer buf tm = Some tm'.

Lemma Val_and_result:
  forall v1 v2,
    Val.and v1 v2 = Vundef \/ exists n, Val.and v1 v2 = Vint n.

Lemma meminv_free_refine':
  forall sm bufs tm t fl sfm b lo hi sfm',
    embed sm fl sfm ->
    meminv t fl sm bufs tm ->
    (forall t', bufs t' = nil) ->
    Mem.free sfm b lo hi = Some sfm' ->
    exists tm', apply_buffer (BufferedFree b lo hi :: nil) tm = Some tm'.

Lemma meminv_extcall_arg':
  forall t fl sm tm sfm tfm rs a arg,
    meminv t fl sm (tso_buffers tm) (memory tm) ->
    embed sm fl sfm ->
    embed (memory tm) fl tfm ->
    (forall t', (tso_buffers tm) t' = nil) ->
    AsmLang.extcall_arg rs sfm a arg ->
    extcall_arg rs (mktsofmem (tso_buffers tm t) tfm) a arg.

Lemma meminv_extcall_arg_pair':
  forall t fl sm tm sfm tfm rs l arg,
    meminv t fl sm (tso_buffers tm) (memory tm) ->
    embed sm fl sfm ->
    embed (memory tm) fl tfm ->
    (forall t', (tso_buffers tm) t' = nil) ->
    AsmLang.extcall_arg_pair rs sfm l arg ->
    extcall_arg_pair rs (mktsofmem (tso_buffers tm t) tfm) l arg.

Lemma meminv_extcall_arguments':
  forall t fl sm tm sfm tfm rs sig args,
    meminv t fl sm (tso_buffers tm) (memory tm) ->
    embed sm fl sfm ->
    embed (memory tm) fl tfm ->
    (forall t', (tso_buffers tm) t' = nil) ->
    AsmLang.extcall_arguments rs sfm sig args ->
    extcall_arguments rs (mktsofmem (tso_buffers tm t) tfm) sig args.

Lemma meminv_valid_pointer_refine':
  forall sm bufs tm t fl sfm tfm b ofs,
    embed sm fl sfm ->
    embed tm fl tfm ->
    meminv t fl sm bufs tm ->
    (forall t', bufs t' = nil) ->
    Mem.valid_pointer sfm b ofs = true ->
    tso_valid_pointer (mktsofmem (bufs t) tfm) b ofs = true.

Lemma meminv_cmpu_bool_Some_refine':
  forall sm bufs tm t fl sfm tfm c v1 v2 b,
    embed sm fl sfm ->
    embed tm fl tfm ->
    meminv t fl sm bufs tm ->
    (forall t', bufs t' = nil) ->
    Val.cmpu_bool (Mem.valid_pointer sfm) c v1 v2 = Some b ->
    exists b', Val.cmpu_bool (tso_valid_pointer (mktsofmem (bufs t) tfm)) c v1 v2 = Some b'.

Section MatchStateSim.

  Variable (cu : Asm_comp_unit).
  Hypothesis (HNODUPGD: nodup_gd_ident (cu_defs cu) = true).
  Hypothesis (HNODUPEF: (nodup_ef (cu_defs cu)) = true).
  Variable (sge : Genv.t fundef unit).
  Variable (tge : Genv.t fundef unit).
  Hypothesis (HSINITGE : init_genv AsmLang cu sge sge).
  Hypothesis (HTINITGE : AsmTSO.init_genv cu tge).
  Hypothesis (HGEMATCH : genv_match _ _ sge tge).

  Lemma symbols_preserved:
    forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol sge s.

  Lemma find_def_find_symbol:
    forall b gd, Genv.find_def sge b = Some gd -> exists s, Genv.find_symbol sge s = Some b.

  Lemma find_def_find_symbol':
    forall b gd, Genv.find_def tge b = Some gd -> exists s, Genv.find_symbol tge s = Some b.

  Lemma find_def_eq:
    forall b, Genv.find_def sge b = Genv.find_def tge b.
    
  Lemma senv_preserved:
    Senv.equiv sge tge.
  
  Lemma function_ptr_eq:
    forall b, Genv.find_funct_ptr sge b = Genv.find_funct_ptr tge b.

  Lemma symbol_address_eq:
    forall id ofs,
      Genv.symbol_address tge id ofs = Genv.symbol_address sge id ofs.

  Lemma eval_addrmode32_eq:
    forall a rs,
      eval_addrmode32 tge a rs = eval_addrmode32 sge a rs.

  Lemma eval_addrmode64_eq:
    forall a rs,
      eval_addrmode64 tge a rs = eval_addrmode64 sge a rs.

  Lemma eval_addrmode_eq:
    forall a rs,
      eval_addrmode tge a rs = eval_addrmode sge a rs.

  Lemma senv_symbol_address_eq:
    forall id ofs, Senv.symbol_address sge id ofs = Senv.symbol_address tge id ofs.

  Lemma eval_builtin_arg_fp_eq:
    forall (rs: Asm.preg -> val) sp arg fp,
      MemOpFP.eval_builtin_arg_fp sge rs sp arg fp <->
      MemOpFP.eval_builtin_arg_fp tge rs sp arg fp.
  
  Lemma genv_match_eval_builtin_args_fp:
    forall (rs: Asm.preg -> val) sp args fp,
      MemOpFP.eval_builtin_args_fp sge rs sp args fp <->
      MemOpFP.eval_builtin_args_fp tge rs sp args fp.

  Lemma meminv_eval_builtin_arg:
    forall t sm bufs tm fl sfm tfm (rs: Asm.preg -> val) sp arg v fp,
      meminv t fl sm bufs tm ->
      embed sm fl sfm ->
      embed tm fl tfm ->
      eval_builtin_arg tge rs sp (mktsofmem (bufs t) tfm) arg v ->
      MemOpFP.eval_builtin_arg_fp tge rs sp arg fp ->
      (exists v', AsmLang.eval_builtin_arg sge rs sp sfm arg v' /\
             ((~ conflictc t fp bufs /\ v' = v)
              \/ conflictc t fp bufs))
      \/
      (forall v', ~ AsmLang.eval_builtin_arg sge rs sp sfm arg v').
  
  Lemma meminv_eval_builtin_args:
    forall t sm bufs tm fl sfm tfm (rs: Asm.preg -> val) sp args vargs fp,
      meminv t fl sm bufs tm ->
      embed sm fl sfm ->
      embed tm fl tfm ->
      eval_builtin_args tge rs sp (mktsofmem (bufs t) tfm) args vargs ->
      MemOpFP.eval_builtin_args_fp tge rs sp args fp ->
      (exists vargs', AsmLang.eval_builtin_args sge rs sp sfm args vargs' /\
                 ((~ conflictc t fp bufs /\ vargs = vargs')
                  \/ conflictc t fp bufs))
      \/
      (forall vargs', ~ AsmLang.eval_builtin_args sge rs sp sfm args vargs').

  Lemma meminv_eval_builtin_arg':
    forall t sm bufs tm fl sfm tfm (rs: Asm.preg -> val) sp arg v,
      meminv t fl sm bufs tm ->
      (forall t', bufs t' = nil) ->
      embed sm fl sfm ->
      embed tm fl tfm ->
      AsmLang.eval_builtin_arg sge rs sp sfm arg v ->
      eval_builtin_arg tge rs sp (mktsofmem (bufs t) tfm) arg v.
    
  Lemma meminv_eval_builtin_args':
    forall t sm bufs tm fl sfm tfm (rs: Asm.preg -> val) sp args vargs,
      meminv t fl sm bufs tm ->
      (forall t', bufs t' = nil) ->
      embed sm fl sfm ->
      embed tm fl tfm ->
      AsmLang.eval_builtin_args sge rs sp sfm args vargs ->
      eval_builtin_args tge rs sp (mktsofmem (bufs t) tfm) args vargs.
            
  Lemma invert_symbol_from_string_eq:
    forall name, invert_symbol_from_string tge name = invert_symbol_from_string sge name.
  
  Ltac simpl_hypos:=
  match goal with
  | [H1: ?x = _, H2: ?x = _ |- _] => rewrite H1 in H2; inv H2; simpl in *; simpl_hypos
  | [H1: context[Genv.find_funct_ptr sge _], H2: context[Genv.find_funct_ptr tge _] |- _ ]
    => rewrite function_ptr_eq in H1; simpl in *; simpl_hypos
  | _ => idtac
  end.

  
  Record match_state (t: tid) (scm: core AsmLang * gmem) (tcm: core AsmLang * tsomem) : Prop :=
    {
      match_sep_obj_clt: sep_obj_client_block (snd scm);
      match_core: fst scm = fst tcm;
      match_mem: Ic (snd scm) (snd tcm);
    }.

  Local Hint Resolve FP.subset_refl FP.subset_emp.
  
  Lemma meminv_exec_instr_eq:
    forall t sfm bufs (tfm: Mem.mem) f i rs rs' tsofm' tfp,
      let fl := Mem.freelist sfm in
      let sgm := strip sfm in
      let tgm := mktsomem bufs (strip tfm) in
      Mem.freelist sfm = Mem.freelist tfm ->
      meminv t fl sgm bufs (strip tfm) ->
      exec_instr_TSO tge f i rs (mktsofmem (bufs t) tfm) = Next rs' tsofm' ->
      exec_instr_TSO_fp tge f i rs (mktsofmem (bufs t) tfm) = tfp ->
      (exists srs' sfp sfm',
          exec_instr sge f i rs sfm = AsmLang.Next srs' sfm' /\
          exec_instr_fp sge f i rs sfm = sfp /\
          ((~ conflictc t tfp bufs) /\
           srs' = rs' /\
           fpmatchc sfp tfp /\
           meminv t fl (strip sfm') (tupdate t (tbuffer tsofm') bufs) (strip (fmemory tsofm')) /\
           Gc t sgm tgm
              (strip sfm') (mktsomem (tupdate t (tbuffer tsofm') bufs) (strip (fmemory tsofm')))
           \/
           (conflictc t tfp bufs /\
            fpmatchc sfp tfp)
          )
      )
      \/
      exec_instr sge f i rs sfm = AsmLang.Stuck.
    
  Lemma meminv_exec_instr_eq':
    forall f i rs sm bufs tm t fl sfm rs' sfm' tfm,
      embed sm fl sfm ->
      embed tm fl tfm ->
      meminv t fl sm bufs tm ->
      (forall t', bufs t' = nil) ->
      exec_instr sge f i rs sfm = AsmLang.Next rs' sfm' ->
      not_alloc_instr i ->
      exists rs'' b',
        exec_instr_TSO tge f i rs (mktsofmem (bufs t) tfm) = Next rs'' (mktsofmem b' tfm) /\
        exists tm', apply_buffer b' tm = Some tm'.

  


  Lemma match_state_clientsim_properties:
    @clientsim_properties Rc Gc Ic AsmLang sge sge tge match_state.
    
End MatchStateSim.

Theorem clientsim_hold:
  forall cu
    (HNODUPGD: nodup_gd_ident (cu_defs cu) = true)
    (HNODUPEF: (nodup_ef (cu_defs cu)) = true),
    clientsim Rc Gc Ic AsmLang cu cu.