Module TSOStepAuxLemmas

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

Require Import CUAST.

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

Require Import Languages.
Require Import TSOGlobSem GlobSemantics RGRels ClientSim ObjectSim.

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

Require Import FMemLemmas TSOMemLemmas.

Ltac simpls := simpl in *.
Local Transparent Mem.load Mem.alloc Mem.store Mem.free.
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.
Definition Not_lock_instr (i : instruction) :=
  match i with
  | Plock_cmpxchg _ _ => False
  | Plock_dec _ => False
  | _ => True
  end.

Inductive FLs_embed (fls :FLists.t) : tsomem -> Prop :=
  | FLs_embed_unbuffer:
      forall tm
        (Embed: forall flid,
            let fl := FLists.flist_content fls flid in
            exists fm, embed (memory tm) fl fm)
        (UNBS: forall t bi b m',
            (tso_buffers tm) t = bi :: b ->
            apply_buffer_item bi (memory tm) = Some m' ->
            FLs_embed fls (mktsomem (tupdate t b (tso_buffers tm)) m')),
        FLs_embed fls tm.

Lemma append_ls_still_nil :
  forall {A : Type} (l l' : list A),
    l = l ++ l' -> l' = nil.

Lemma list_forall2_stable :
  forall {A B : Type} al bl (P P' : A -> B -> Prop),
    (forall (a : A) (b : B), P a b -> P' a b) ->
    list_forall2 P al bl ->
    list_forall2 P' al bl.

Lemma Memperm_order''_eq_perm_eq :
  forall p1 p2,
    Memperm.perm_order'' p1 p2 ->
    Memperm.perm_order'' p2 p1 ->
    p1 = p2.

Lemma gmem_eq_mem_access_eq :
  forall m m' b ofs k,
    GMem.eq m m' ->
    (GMem.mem_access m) !! b ofs k = (GMem.mem_access m') !! b ofs k.

Lemma Memperm_order''_impl_Memperm_order' :
  forall m m' b ofs k p,
    Mem.perm_order' ((GMem.mem_access m) !! b ofs k) p ->
    Memperm.perm_order'' ((GMem.mem_access m') !! b ofs k)
                         ((GMem.mem_access m) !! b ofs k) ->
    Mem.perm_order' ((GMem.mem_access m') !! b ofs k) p.

Lemma Memperm_perm_order''_refl :
  forall p,
    Memperm.perm_order'' p p.

Lemma gmem_eq_valid_pointer_eq' :
  forall fm1 fm2,
    GMem.eq (strip fm1) (strip fm2) ->
    Mem.valid_pointer fm1 = Mem.valid_pointer fm2.

Lemma gmem_eq_valid_pointer_eq :
  forall fm1 fm2 gm1 gm2 fl,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    Mem.valid_pointer fm1 = Mem.valid_pointer fm2.

Lemma gmem_eq_load_still :
  forall m m' c b ofs v,
    GMem.eq m m' ->
    load c m b ofs = Some v ->
    exists v', load c m' b ofs = Some v'.

Lemma gmem_eq_Mem_load_still' :
  forall fm fm' c b ofs v,
    GMem.eq (strip fm) (strip fm') ->
    Mem.load c fm b ofs = Some v ->
    exists v', Mem.load c fm' b ofs = Some v'.

Lemma gmem_eq_Mem_load_still :
  forall m m' fm fm' c b ofs v fl,
    GMem.eq m m' -> embed m fl fm -> embed m' fl fm' ->
    Mem.load c fm b ofs = Some v ->
    exists v', Mem.load c fm' b ofs = Some v'.

Lemma gmem_eq_Mem_loadv_still' :
  forall fm fm' c a v,
    GMem.eq (strip fm) (strip fm') ->
    Mem.loadv c fm a = Some v ->
    exists v', Mem.loadv c fm' a = Some v'.

Lemma gmem_eq_Mem_loadv_still :
  forall m m' fm fm' c a v fl,
    GMem.eq m m' -> embed m fl fm -> embed m' fl fm' ->
    Mem.loadv c fm a = Some v ->
    exists v', Mem.loadv c fm' a = Some v'.

Lemma gmem_eq_load_same_v :
  forall m m' v v' c b ofs,
    GMem.eq m m' ->
    load c m b ofs = Some v ->
    load c m' b ofs = Some v' ->
    v = v'.

Lemma gmem_eq_Mem_load_same_v' :
  forall fm fm' v v' c b ofs,
    GMem.eq (strip fm) (strip fm') ->
    Mem.load c fm b ofs = Some v ->
    Mem.load c fm' b ofs = Some v' ->
    v = v'.

Lemma gmem_eq_Mem_load_same_v :
  forall m m' fm fm' v v' c b ofs fl,
    GMem.eq m m' -> embed m fl fm -> embed m' fl fm' ->
    Mem.load c fm b ofs = Some v ->
    Mem.load c fm' b ofs = Some v' ->
    v = v'.

Lemma gmem_eq_mem_loadv_same' :
  forall fm1 fm2 c a v1 v2,
    GMem.eq (strip fm1) (strip fm2) ->
    Mem.loadv c fm1 a = Some v1 ->
    Mem.loadv c fm2 a = Some v2 ->
    v1 = v2.
  
Lemma gmem_eq_mem_loadv_same :
  forall gm1 gm2 fm1 fm2 fl c a v1 v2,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    Mem.loadv c fm1 a = Some v1 ->
    Mem.loadv c fm2 a = Some v2 ->
    v1 = v2.

Lemma gmem_eq_Mem_store_still :
  forall gm1 gm2 fm1 fm2 fm1' fl c b ofs v,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    Mem.store c fm1 b ofs v = Some fm1' ->
    exists fm2', Mem.store c fm2 b ofs v = Some fm2'.

Lemma gmem_eq_Mem_storev_still :
  forall gm1 gm2 fm1 fm2 fm1' fl c a v,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    Mem.storev c fm1 a v = Some fm1' ->
    exists fm2', Mem.storev c fm2 a v = Some fm2'.

Lemma store_gmem_eq_stable :
  forall gm1 gm2 gm1' gm2' c b z v,
    GMem.eq gm1 gm2 ->
    store c gm1 b z v = Some gm1' ->
    store c gm2 b z v = Some gm2' ->
    GMem.eq gm1' gm2'.

Lemma gmem_eq_apply_buf_item_stable :
  forall bi gm gm' gm1,
    GMem.eq gm gm' ->
    apply_buffer_item bi gm = Some gm1 ->
    exists gm2, apply_buffer_item bi gm' = Some gm2.

Lemma apply_buf_item_after_Mem_store_original_still :
  forall bi m m' fm b ofs v c,
    apply_buffer_item bi (strip m) = Some m' ->
    Mem.store c fm b ofs v = Some m ->
    exists m'', apply_buffer_item bi (strip fm) = Some m''.
  
Lemma gmem_eq_apply_same_buf_item_still :
  forall bi gm1 gm2 gm1' gm2',
    GMem.eq gm1 gm2 ->
    apply_buffer_item bi gm1 = Some gm1' ->
    apply_buffer_item bi gm2 = Some gm2' ->
    GMem.eq gm1' gm2'.

Lemma apply_same_buf_gmem_eq_stable :
  forall bf gm1 gm2 gm1' gm2',
    GMem.eq gm1 gm2 ->
    apply_buffer bf gm1 = Some gm1' ->
    apply_buffer bf gm2 = Some gm2' ->
    GMem.eq gm1' gm2'.
  
Lemma gmem_eq_apply_same_buf_still :
  forall bf gm1 gm2 gm1',
    GMem.eq gm1 gm2 ->
    apply_buffer bf gm1 = Some gm1' ->
    exists gm2', apply_buffer bf gm2 = Some gm2'.

Lemma gmem_eq_embed_both :
  forall gm1 gm2 fl fm1,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 ->
    exists fm2, embed gm2 fl fm2 /\ Mem.nextblock fm1 = Mem.nextblock fm2.
  
Lemma gmem_eq_embed_apply_buf_still :
  forall gm1 gm2 gm1' gm2' fm1' fl bf,
    GMem.eq gm1 gm2 ->
    embed gm1' fl fm1' ->
    apply_buffer bf gm1 = Some gm1' ->
    apply_buffer bf gm2 = Some gm2' ->
    exists fm2', embed gm2' fl fm2' /\ Mem.nextblock fm1' = Mem.nextblock fm2'.

Lemma gmem_eq_weak_valid_pointer_fp_eq :
  forall fm1 fm2 b ofs,
    GMem.eq (strip fm1) (strip fm2) ->
    FMemOpFP.weak_valid_pointer_fp fm1 b ofs =
    FMemOpFP.weak_valid_pointer_fp fm2 b ofs.

Lemma gmem_eq_cmpu_bool_fp_eq :
  forall fm1 fm2 v1 v2 cmp,
    GMem.eq (strip fm1) (strip fm2) ->
    Cop_fp.cmpu_bool_fp fm1 cmp v1 v2 = Cop_fp.cmpu_bool_fp fm2 cmp v1 v2.
  
Lemma gmem_eq_ub_safe_eq:
  forall B gm gm',
    GMem.eq gm gm' ->
    unbuffer_safe (mktsomem B gm) ->
    unbuffer_safe (mktsomem B gm').

Lemma gmem_eq_embed_still :
  forall gm1 gm2 fl fm1,
    embed gm1 fl fm1 ->
    GMem.eq gm1 gm2 ->
    exists fm2, embed gm2 fl fm2 /\ Mem.nextblockid fm1 = Mem.nextblockid fm2.

Lemma gmem_eq_tsoloadv_v_eq' :
  forall bf fm1 fm2 a c v v0,
    GMem.eq (strip fm1) (strip fm2) ->
    tsoloadv c {| tbuffer := bf; fmemory := fm1 |} a = Some v ->
    tsoloadv c {| tbuffer := bf; fmemory := fm2 |} a = Some v0 ->
    v = v0.

Lemma gmem_eq_tsoloadv_v_eq :
  forall bf gm1 gm2 fm1 fm2 a c v v0 fl,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    tsoloadv c {| tbuffer := bf; fmemory := fm1 |} a = Some v ->
    tsoloadv c {| tbuffer := bf; fmemory := fm2 |} a = Some v0 ->
    v = v0.

Lemma gmem_eq_tsoloadv_v_still' :
  forall bf fm1 fm2 a c v,
    GMem.eq (strip fm1) (strip fm2) ->
    tsoloadv c {| tbuffer := bf; fmemory := fm1 |} a = Some v ->
    exists v', tsoloadv c {| tbuffer := bf; fmemory := fm2 |} a = Some v'.

Lemma gmem_eq_tsoloadv_v_still :
  forall bf gm1 gm2 fm1 fm2 a c v fl,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    tsoloadv c {| tbuffer := bf; fmemory := fm1 |} a = Some v ->
    exists v', tsoloadv c {| tbuffer := bf; fmemory := fm2 |} a = Some v'.

Lemma gmem_eq_exec_load_TSO_still :
  forall ge c buf fm1 fm2 gm1 gm2 a rs rd rs' tsofm1 fl,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    exec_load_TSO ge c {| tbuffer := buf; fmemory := fm1 |} a rs rd =
    Next rs' tsofm1 ->
    exists tsofm2, exec_load_TSO ge c {| tbuffer := buf; fmemory := fm2 |} a rs rd =
              Next rs' tsofm2.

Lemma gmem_eq_tsostorev_still':
  forall c bm1 bm2 a v tsofm1,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    tsostorev c bm1 a v = Some tsofm1 ->
    exists tsofm2, tsostorev c bm2 a v = Some tsofm2.

Lemma gmem_eq_tsostorev_still :
  forall c bf fm1 fm2 gm1 gm2 fl a v tsofm1,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    tsostorev c {| tbuffer := bf; fmemory := fm1 |} a v = Some tsofm1 ->
    exists tsofm2, tsostorev c {| tbuffer := bf; fmemory := fm2 |} a v = Some tsofm2.

Lemma gmem_eq_exec_store_TSO_still :
  forall ge c buf fm1 fm2 gm1 gm2 a r1 r2 lrs rs' tsofm1 fl,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    exec_store_TSO ge c {| tbuffer := buf; fmemory := fm1 |} a r1 r2 lrs =
    Next rs' tsofm1 ->
    exists tsofm2, exec_store_TSO ge c {| tbuffer := buf; fmemory := fm2 |} a r1 r2 lrs =
              Next rs' tsofm2.

Lemma gmem_eq_buf_eq_tsostore_stable :
  forall bm1 bm2 bm1' bm2' c b ofs v,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    tsostore c bm1 b ofs v = Some bm1' ->
    tsostore c bm2 b ofs v = Some bm2' ->
    GMem.eq (strip (fmemory bm1')) (strip (fmemory bm2')) /\
    tbuffer bm1' = tbuffer bm2'.

Lemma gmem_eq_buf_eq_tsostorev_stable :
  forall bm1 bm2 bm1' bm2' c a v,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    tsostorev c bm1 v a = Some bm1' ->
    tsostorev c bm2 v a = Some bm2' ->
    GMem.eq (strip (fmemory bm1')) (strip (fmemory bm2')) /\
    tbuffer bm1' = tbuffer bm2'.

Lemma gmem_eq_tso_valid_pointer_eq :
  forall bf fm1 fm2 gm1 gm2 fl,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    tso_valid_pointer {| tbuffer := bf; fmemory := fm1 |} =
    tso_valid_pointer {| tbuffer := bf; fmemory := fm2 |}.

Lemma gmem_eq_compare_ints_TSO_eq :
  forall x y rs bf fm1 fm2 fl gm1 gm2,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    compare_ints_TSO x y rs {| tbuffer := bf; fmemory := fm1 |} =
    compare_ints_TSO x y rs {| tbuffer := bf; fmemory := fm2 |}.

Lemma gmem_eq_tso_weak_valid_pointer_fp_eq :
  forall bf fm1 fm2 b ofs,
    GMem.eq (strip fm1) (strip fm2) ->
    tso_weak_valid_pointer_fp {| tbuffer := bf; fmemory := fm1 |} b ofs =
    tso_weak_valid_pointer_fp {| tbuffer := bf; fmemory := fm2 |} b ofs.

Lemma gmem_eq_compare_ints_TSO_fp_eq :
  forall x y bf fm1 fm2,
    GMem.eq (strip fm1) (strip fm2) ->
    compare_ints_TSO_fp x y {| tbuffer := bf; fmemory := fm1 |} =
    compare_ints_TSO_fp x y {| tbuffer := bf; fmemory := fm2 |}.

Ltac inv_next :=
  match goal with
  | H : Next _ _ = Next _ _ |- _ => inv H; subst; eauto
  end.

Ltac elim_embed :=
  match goal with
  | H : embed _ _ _ |- _ => inv H; subst
  end.

Ltac same_elim :=
  match goal with
  | H1 : ?A = _, H2 : ?A = _ |- _ =>
    rewrite H1 in H2; inv H2; tryfalse
  | _ => idtac
  end.

Ltac elim_load_eq_value_case :=
  match goal with
  | H1 : GMem.eq ?gm1 ?gm2,
         H2 : embed ?gm1 ?fl ?fm1,
              H3 : embed ?gm2 ?fl ?fm2,
                   H4 : Mem.loadv _ ?fm1 _ = Some ?v1,
                        H5 : Mem.loadv _ ?fm2 _ = Some ?v2 |- _ =>
    let H := fresh in
    lets H : H1;
    eapply gmem_eq_mem_loadv_same in H; eauto; subst; eauto; tryfalse
  end.

Ltac elim_load_eq_value_case' :=
  match goal with
  | H1 : GMem.eq (strip ?fm1) (strip ?fm2),
         H2 : Mem.loadv _ ?fm1 _ = Some ?v1,
              H3 : Mem.loadv _ ?fm2 _ = Some ?v2 |- _ =>
    let H := fresh in
    lets H : H1;
    eapply gmem_eq_mem_loadv_same' in H; eauto; subst; eauto; tryfalse
  end.

Ltac load_eq_gmem_some_none_false :=
  match goal with
  | H1 : GMem.eq ?gm1 ?gm2,
         H2 : embed ?gm1 ?fl ?fm1,
              H3 : embed ?gm2 ?fl ?fm2,
                   H4 : Mem.loadv _ ?fm1 _ = Some ?v1,
                        H5 : Mem.loadv _ ?fm2 _ = None |- _ =>
    eapply gmem_eq_Mem_loadv_still in H4; eauto; destruct H4 as [?x H4]; same_elim
  end.

Ltac load_eq_gmem_some_none_false' :=
  match goal with
  | H1 : GMem.eq (strip ?fm1) (strip ?fm2),
         H2 : Mem.loadv _ ?fm1 _ = Some ?v1,
              H3 : Mem.loadv _ ?fm2 _ = None |- _ =>
    eapply gmem_eq_Mem_loadv_still' in H2; eauto; destruct H2 as [?x H2]; same_elim
  end.

Ltac store_eq_gmem_some_none_false :=
  match goal with
  | H1 : GMem.eq ?gm1 ?gm2,
         H2 : embed ?gm1 ?fl ?fm1,
              H3 : embed ?gm2 ?fl ?fm2,
                   H4 : Mem.storev _ ?fm1 _ _ = Some ?fm1',
                        H5 : Mem.storev _ ?fm2 _ _ = None |- _ =>
    try elim_load_eq_value_case;
    eapply gmem_eq_Mem_storev_still in H4; eauto;
    destruct H4 as [?fm2' H4]; same_elim
  end.

Ltac store_eq_gmem_none_some_false :=
  match goal with
  | H1 : GMem.eq ?gm1 ?gm2,
         H2 : embed ?gm1 ?fl ?fm1,
              H3 : embed ?gm2 ?fl ?fm2,
                   H4 : Mem.storev _ ?fm1 _ _ = None,
                        H5 : Mem.storev _ ?fm2 _ _ = Some ?fm2' |- _ =>
    try elim_load_eq_value_case;
    eapply GMem.eq_sym in H1;
    eapply gmem_eq_Mem_storev_still in H5; eauto; destruct H5 as [?fm2' H5];
    same_elim
  end.

Ltac valid_pointer_eq_case :=
  match goal with
  | H1 : GMem.eq ?gm1 ?gm2,
         H2 : embed ?gm1 ?fl ?fm1,
              H3 : embed ?gm2 ?fl ?fm2,
                   H4 : context [Mem.valid_pointer ?fm1],
                        H5 : context [Mem.valid_pointer ?fm2] |- _ =>
    try elim_load_eq_value_case;
    eapply gmem_eq_valid_pointer_eq in H1; eauto;
    rewrite H1 in H4; eauto; try same_elim
  end.

Ltac valid_pointer_eq_case' :=
  match goal with
  | H1 : GMem.eq (strip ?fm1) (strip ?fm2),
         H2 : context [Mem.valid_pointer ?fm1],
              H3 : context [Mem.valid_pointer ?fm2] |- _ =>
    try elim_load_eq_value_case;
    eapply gmem_eq_valid_pointer_eq' in H1; eauto;
    rewrite H1 in H2; eauto; try same_elim
  end.

Ltac prev_process :=
  ex_match2; repeat inv_next; repeat elim_embed; eauto.

Ltac solve_load_store_valid_ptr_case :=
  ex_match2; eauto; tryfalse; inv_next;
  try solve [store_eq_gmem_none_some_false];
  try solve [store_eq_gmem_some_none_false];
  try solve [valid_pointer_eq_case];
  try solve [load_eq_gmem_some_none_false];
  try solve [elim_load_eq_value_case].

Ltac solve_tso_store_gmem_buf_eq_stable :=
  match goal with
  | H1 : GMem.eq (strip (fmemory ?bm1)) (strip (fmemory ?bm2)),
         H2 : tsostorev ?c ?bm1 ?a ?v = Some ?bm1',
              H3 : tsostorev ?c ?bm2 ?a ?v = Some ?bm2' |- _ =>
    let H := fresh in
    lets H : H1; eapply gmem_eq_buf_eq_tsostorev_stable in H; eauto;
    destruct H
  end.

Ltac solve_gmem_buf_eq_tsostorev_some_none :=
  match goal with
  | H1 : GMem.eq (strip (fmemory ?bm1)) (strip (fmemory ?bm2)),
         H2 : tbuffer ?bm1 = tbuffer ?bm2,
              H3 : tsostorev ?c ?bm1 ?a ?v = Some _,
                   H4 : tsostorev ?c ?bm2 ?a ?v = None |- _ =>
    eapply gmem_eq_tsostorev_still' in H3; eauto;
    destruct H3 as [?t H3]; rewrite H3 in H4; tryfalse
  end.

Ltac strip_mem_elim :=
  match goal with
  | H : strip _ = memory _ |- context [strip _] =>
    rewrite H; eauto
  end.

Lemma gmem_eq_tsoalloc_stable' :
  forall bf gm1 gm2 fm1 fm2 lo hi fl bm1 stk,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    tsoalloc {| tbuffer := bf; fmemory := fm1 |} lo hi (bm1, stk) ->
    exists bm2 stk', tsoalloc {| tbuffer := bf; fmemory := fm2 |} lo hi (bm2, stk') /\
                GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) /\ stk = stk' /\
                tbuffer bm1 = tbuffer bm2.

Lemma gmem_eq_tsoalloc_stable :
  forall bf gm1 gm2 fm1 fm2 lo hi fl bm1 stk,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    tsoalloc {| tbuffer := bf; fmemory := fm1 |} lo hi (bm1, stk) ->
    exists bm2, tsoalloc {| tbuffer := bf; fmemory := fm2 |} lo hi (bm2, stk) /\
           GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) /\
           tbuffer bm1 = tbuffer bm2.

Lemma gmem_eq_tsostore_stable :
  forall bm1 bm2 bm1' c b ofs v,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    tsostore c bm1 b ofs v = Some bm1' ->
    exists bm2', tsostore c bm2 b ofs v = Some bm2' /\
            GMem.eq (strip (fmemory bm1')) (strip (fmemory bm2')) /\
            tbuffer bm1' = tbuffer bm2'.

Lemma exec_load_TSO_gmem_eq_same_buf_stable :
  forall ge c bf fm1 fm2 gm1 gm2 fl a rs rd rs' tsofm1 tsofm2,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    exec_load_TSO ge c {| tbuffer := bf; fmemory := fm1 |} a rs rd =
    Next rs' tsofm1 ->
    exec_load_TSO ge c {| tbuffer := bf; fmemory := fm2 |} a rs rd =
    Next rs' tsofm2 ->
    tbuffer tsofm1 = tbuffer tsofm2 /\
    GMem.eq (strip (fmemory tsofm1)) (strip (fmemory tsofm2)).

Lemma exec_store_TSO_gmem_eq_same_buf_stable :
  forall ge c bf fm1 fm2 gm1 gm2 fl a rs rd rs' tsofm1 tsofm2 ls,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    exec_store_TSO ge c {| tbuffer := bf; fmemory := fm1 |} a rs rd ls =
    Next rs' tsofm1 ->
    exec_store_TSO ge c {| tbuffer := bf; fmemory := fm2 |} a rs rd ls =
    Next rs' tsofm2 ->
    tbuffer tsofm1 = tbuffer tsofm2 /\
    GMem.eq (strip (fmemory tsofm1)) (strip (fmemory tsofm2)).

Lemma tso_goto_label_gmem_eq_same_buf_stable :
  forall bf fm1 fm2 gm1 gm2 fl tsofm1 tsofm2 f l rs rs',
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    tso_goto_label f l rs {| tbuffer := bf; fmemory := fm1 |} = Next rs' tsofm1 ->
    tso_goto_label f l rs {| tbuffer := bf; fmemory := fm2 |} = Next rs' tsofm2 ->
    tbuffer tsofm1 = tbuffer tsofm2 /\
    GMem.eq (strip (fmemory tsofm1)) (strip (fmemory tsofm2)).

Lemma Mem_store_gmem_eq_stable :
  forall c fm1 fm2 fm1' fm2' b ofs v,
    GMem.eq (strip fm1) (strip fm2) ->
    Mem.store c fm1 b ofs v = Some fm1' ->
    Mem.store c fm2 b ofs v = Some fm2' ->
    GMem.eq (strip fm1') (strip fm2').

Lemma Mem_storev_gmem_eq_stable :
  forall fm1 fm2 c v a fm1' fm2',
    GMem.eq (strip fm1) (strip fm2) ->
    Mem.storev c fm1 a v = Some fm1' ->
    Mem.storev c fm2 a v = Some fm2' ->
    GMem.eq (strip fm1') (strip fm2').
 
Lemma exec_instr_TSO_gmem_eq_stable :
  forall ge f i rs rs' buf fm1 fm2 gm1 gm2 tsofm1 fl,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    exec_instr_TSO ge f i rs {| tbuffer := buf; fmemory := fm1 |} =
    Next rs' tsofm1 ->
    exists tsofm2, exec_instr_TSO ge f i rs {| tbuffer := buf; fmemory := fm2 |} =
              Next rs' tsofm2.

Lemma gmem_eq_exec_instr_TSO_buf_eq_stable :
  forall ge f i rs rs' bf gm1 gm2 fm1 fm2 fl tsofm1 tsofm2,
    GMem.eq gm1 gm2 -> embed gm1 fl fm1 -> embed gm2 fl fm2 ->
    exec_instr_TSO ge f i rs {| tbuffer := bf; fmemory := fm1 |} =
    Next rs' tsofm1 ->
    exec_instr_TSO ge f i rs {| tbuffer := bf; fmemory := fm2 |} =
    Next rs' tsofm2 ->
    tbuffer tsofm1 = tbuffer tsofm2 /\
    GMem.eq (strip (fmemory tsofm1)) (strip (fmemory tsofm2)).

Lemma gmem_eq_exec_instr_TSO_fp_eq :
  forall fm1 fm2 f i rs bf ge,
    GMem.eq (strip fm1) (strip fm2) ->
    exec_instr_TSO_fp ge f i rs {| tbuffer := bf; fmemory := fm1 |} =
    exec_instr_TSO_fp ge f i rs {| tbuffer := bf; fmemory := fm2 |}.

Lemma gmem_eq_eval_builtin_arg_still :
  forall ge (rs : Asm.preg -> val) sp bm1 bm2 a b,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    eval_builtin_arg ge rs sp bm1 a b ->
    eval_builtin_arg ge rs sp bm2 a b.

Lemma gmem_eq_eval_builtin_args_still :
  forall ge (rs : Asm.preg -> val) sp bm1 bm2 args vargs,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    eval_builtin_args ge rs sp bm1 args vargs ->
    eval_builtin_args ge rs sp bm2 args vargs.

Lemma gmem_eq_extcall_arg_still :
  forall rs bm1 bm2 l v,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    extcall_arg rs bm1 l v ->
    extcall_arg rs bm2 l v.

Lemma gmem_eq_extcall_arg_pair_still :
  forall rs bm1 bm2 a b,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    extcall_arg_pair rs bm1 a b ->
    extcall_arg_pair rs bm2 a b.

Lemma gmem_eq_extcall_arguments_still' :
  forall rs bm1 bm2 args vargs,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    list_forall2 (extcall_arg_pair rs bm1) args vargs ->
    list_forall2 (extcall_arg_pair rs bm2) args vargs.

Lemma gmem_eq_extcall_arguments_still :
  forall (rs : Asm.preg -> val) bm1 bm2 sg args,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    extcall_arguments rs bm1 sg args ->
    extcall_arguments rs bm2 sg args.

Lemma gmem_eq_store_args_fmem_still' :
  forall args bm1 bm2 stk bm1' tys ofs,
    GMem.eq (strip (fmemory bm1)) (strip (fmemory bm2)) ->
    tbuffer bm1 = tbuffer bm2 ->
    store_args_rec_fmem bm1 stk ofs args tys = Some bm1' ->
    exists bm2', store_args_rec_fmem bm2 stk ofs args tys = Some bm2' /\
            GMem.eq (strip (fmemory bm1')) (strip (fmemory bm2')) /\
            tbuffer bm1' = tbuffer bm2'.
  
Lemma gmem_eq_store_args_fmem_still :
  forall bm1 bm2 gm1 gm2 fl stk bm1' tys args,
    GMem.eq gm1 gm2 ->
    embed gm1 fl (fmemory bm1) -> embed gm2 fl (fmemory bm2) ->
    tbuffer bm1 = tbuffer bm2 ->
    store_args_fmem bm1 stk args tys = Some bm1' ->
    exists bm2', store_args_fmem bm2 stk args tys = Some bm2' /\
            GMem.eq (strip (fmemory bm1')) (strip (fmemory bm2')) /\
            tbuffer bm1' = tbuffer bm2'.

Lemma gmem_eq_ub_gmem_eq:
  forall B gm1 gm1' t B' gm2,
    GMem.eq gm1 gm1' ->
    unbuffer (mktsomem B gm1) t = Some (mktsomem B' gm2) ->
    exists gm2', unbuffer (mktsomem B gm1') t = Some (mktsomem B' gm2') /\
            GMem.eq gm2 gm2'.

Lemma embed_unbuffer_stable :
  forall fls tm tm' fm t n,
    FLs_embed fls tm ->
    unbuffer tm t = Some tm' ->
    embed (memory tm) (FLists.get_fl fls n) fm ->
    exists fm', embed (memory tm') (FLists.get_fl fls n) fm'.

Lemma gmem_buffer_eq_corestep_eq:
  forall ge fl c1 gm1 buf1 fp c2 gm2 buf2 gm1',
    tsostep ge fl c1 (buf1, gm1) fp c2 (buf2, gm2) ->
    GMem.eq gm1 gm1' ->
    exists gm2',
      tsostep ge fl c1 (buf1, gm1') fp c2 (buf2, gm2') /\
      GMem.eq gm2 gm2'.

Ltac inv_some :=
  match goal with
  | H : Some ?A = Some ?B |- _ => inv H
  end.

Lemma exec_load_TSO_buf_add :
  forall ge c bm a rs rd rs' bm',
    exec_load_TSO ge c bm a rs rd = Next rs' bm' ->
    exists bf, tbuffer bm' = tbuffer bm ++ bf.

Lemma exec_store_TSO_buf_add :
  forall ge c bm a rs rd ls rs' bm',
    exec_store_TSO ge c bm a rs rd ls = Next rs' bm' ->
    exists bf, tbuffer bm' = tbuffer bm ++ bf.

Lemma tso_goto_label_buf_add :
  forall f l rs bm rs' bm',
    tso_goto_label f l rs bm = Next rs' bm' ->
    exists bf, tbuffer bm' = tbuffer bm ++ bf.

Lemma exec_instr_TSO_buf_add :
  forall ge f i rs rs' bm bm',
    exec_instr_TSO ge f i rs bm = Next rs' bm' ->
    exists bf, tbuffer bm' = tbuffer bm ++ bf.

Lemma tsoalloc_buf_add :
  forall bm bm' lo hi stk,
    tsoalloc bm lo hi (bm', stk) ->
    exists bf, tbuffer bm' = tbuffer bm ++ bf.

Lemma store_args_fmem_buf_add :
  forall args bm b ofs tys bm',
    store_args_rec_fmem bm b ofs args tys = Some bm' ->
    exists bf, tbuffer bm' = tbuffer bm ++ bf.

Lemma unbuffer_remove_bf_head :
  forall tm tm' t,
    unbuffer tm t = Some tm' ->
    tso_buffers tm' t = tl (tso_buffers tm t).

Lemma tsoalloc_gm_stable :
  forall bm lo hi bm' stk,
    tsoalloc bm lo hi (bm', stk) ->
    strip (fmemory bm) = strip (fmemory bm').

Lemma exec_load_TSO_gm_stable :
  forall ge c bm a rs rd rs' bm',
    exec_load_TSO ge c bm a rs rd = Next rs' bm' ->
    strip (fmemory bm) = strip (fmemory bm').

Lemma exec_store_TSO_gm_stable :
  forall ge c bm a rs rd ls rs' bm',
    exec_store_TSO ge c bm a rs rd ls = Next rs' bm' ->
    strip (fmemory bm) = strip (fmemory bm').

Lemma tso_goto_label_gm_stable :
  forall f l rs rs' bm bm',
    tso_goto_label f l rs bm = Next rs' bm' ->
    strip (fmemory bm) = strip (fmemory bm').

Lemma exec_instr_TSO_buf_not_empty_gm_stable :
  forall ge f i rs rs' bm bm',
    tbuffer bm <> nil ->
    exec_instr_TSO ge f i rs bm = Next rs' bm' ->
    strip (fmemory bm) = strip (fmemory bm').

Lemma store_args_fmem_gm_stable :
  forall args tys bm a ofs bm',
    store_args_rec_fmem bm a ofs args tys = Some bm' ->
    strip (fmemory bm) = strip (fmemory bm').

Lemma tsoload_apply_buf_hd_still :
  forall bi b fm fm' stk ofs v v0 c,
    apply_buffer_item bi (strip fm) = Some (strip fm') ->
    tsoload c {| tbuffer := bi :: b; fmemory := fm |} stk ofs = Some v ->
    tsoload c {| tbuffer := b; fmemory := fm' |} stk ofs = Some v0 ->
    v = v0.

Lemma tsostore_apply_buf_m_eq :
  forall c bi bf fm fm' b ofs v bm bm',
    apply_buffer_item bi (strip fm) = Some (strip fm') ->
    tsostore c {| tbuffer := bi :: bf; fmemory := fm |} b ofs v = Some bm ->
    tsostore c {| tbuffer := bf; fmemory := fm' |} b ofs v = Some bm' ->
    tbuffer bm' = tl (tbuffer bm) /\ fm' = fmemory bm'.

Lemma exec_load_TSO_unbuffer_still :
  forall ge c tm tm' fm fm' t a rs rd rs' tsofm',
    unbuffer tm t = Some tm' -> strip fm = memory tm -> strip fm' = memory tm' ->
    exec_load_TSO ge c {| tbuffer := tso_buffers tm t; fmemory := fm |} a rs rd =
    Next rs' tsofm' ->
    exec_load_TSO ge c {| tbuffer := tso_buffers tm' t; fmemory := fm' |} a rs rd =
    Next rs' {| tbuffer := tl (tbuffer tsofm'); fmemory := fm' |}.

Lemma exec_store_TSO_unbuffer_still :
  forall ge c tm tm' fm fm' t a rs rd rs' tsofm' ls,
    unbuffer tm t = Some tm' -> strip fm = memory tm -> strip fm' = memory tm' ->
    exec_store_TSO ge c {| tbuffer := tso_buffers tm t; fmemory := fm |} a rs rd ls
    = Next rs' tsofm' ->
    exec_store_TSO ge c {| tbuffer := tso_buffers tm' t; fmemory := fm' |} a rs rd ls
    = Next rs' {| tbuffer := tl (tbuffer tsofm'); fmemory := fm' |}.

Lemma unbuffer_tso_valid_pointer_eq :
  forall b bi fm fm',
    apply_buffer_item bi (strip fm) = Some (strip fm') ->
    tso_valid_pointer {| tbuffer := b; fmemory := fm' |} =
    tso_valid_pointer {| tbuffer := bi :: b; fmemory := fm |}.

Lemma unbuffer_compare_ints_TSO_eq :
  forall fm fm' x y bi b rs,
    apply_buffer_item bi (strip fm) = Some (strip fm') ->
    compare_ints_TSO x y rs {| tbuffer := b; fmemory := fm' |} =
    compare_ints_TSO x y rs {| tbuffer := bi :: b; fmemory := fm |}.

Lemma unbuffer_tso_goto_label_still :
  forall f l rs rs' tm tm' fm fm' t bm,
    unbuffer tm t = Some tm' -> strip fm = memory tm -> strip fm' = memory tm' ->
    tso_goto_label f l rs {| tbuffer := tso_buffers tm t; fmemory := fm |} =
    Next rs' bm ->
    tso_goto_label f l rs {| tbuffer := tso_buffers tm' t; fmemory := fm' |} =
    Next rs' {| tbuffer := tl (tbuffer bm); fmemory := fm' |}.
  
Lemma exec_instr_TSO_unbuffer_still :
  forall ge f i rs rs' tm tm' fm fm' fl tsofm' t,
    unbuffer tm t = Some tm' ->
    embed (memory tm) fl fm -> embed (memory tm') fl fm' ->
    exec_instr_TSO ge f i rs {| tbuffer := tso_buffers tm t; fmemory := fm |} =
    Next rs' tsofm' ->
    exec_instr_TSO ge f i rs {| tbuffer := tso_buffers tm' t; fmemory := fm' |} =
    Next rs' {| tbuffer := tl (tbuffer tsofm'); fmemory := fm' |}.


Lemma unbuffer_safe_addition_original_still :
  forall tm t bf,
    unbuffer_safe (tsoupd tm t (tso_buffers tm t ++ bf) (memory tm)) ->
    unbuffer_safe tm.

Lemma unbuffer_safe_addition_multi_thread_original_still :
  forall tm tm',
    unbuffer_safe tm -> memory tm = memory tm' ->
    (forall t, exists bis, tso_buffers tm t = tso_buffers tm' t ++ bis) ->
    unbuffer_safe tm'.
  
Lemma unbuffer_safe_Mem_store_stable :
  forall tm fm m c b ofs v,
    unbuffer_safe {| tso_buffers := tso_buffers tm; memory := strip m |} ->
    strip fm = memory tm ->
    Mem.store c fm b ofs v = Some m ->
    unbuffer_safe tm.

Lemma unbuffer_upd_original_still :
  forall tm t bf tm',
    tso_buffers tm t <> nil ->
    unbuffer (tsoupd tm t (tso_buffers tm t ++ bf) (memory tm)) t = Some tm' ->
    exists tm'', unbuffer tm t = Some tm'' /\ memory tm' = memory tm'' /\
            tso_buffers tm' =
            tupdate t (tl (tso_buffers tm t ++ bf)) (tso_buffers tm'').

Lemma unbuffer_safe_unbuffer_still :
  forall tm tm' t,
    unbuffer_safe tm -> unbuffer tm t = Some tm' ->
    unbuffer_safe tm'.

Ltac unfolds_exec_load_TSO :=
  unfolds exec_load_TSO; ex_match2; simpls; inv_next; simpls.

Ltac unfolds_exec_store_TSO :=
  unfolds exec_store_TSO; ex_match2; unfolds tsostorev; ex_match2;
  unfolds tsostore; inv_some; inv_next; simpls.

Lemma unbuffer_safe_after_exec_instr_TSO_unbuffer_safe_original :
  forall ge f i tm fm rs rs' bm t,
    unbuffer_safe (tsoupd tm t (tbuffer bm) (strip (fmemory bm))) ->
    strip fm = memory tm ->
    exec_instr_TSO ge f i rs {| tbuffer := tso_buffers tm t; fmemory := fm |} =
    Next rs' bm ->
    unbuffer_safe tm.
  
Lemma unbuffer_safe_after_tsostep_unbuffer_safe_original :
  forall ge fl c fp c' buf' gm' t tm,
    tsostep ge fl c (tso_buffers tm t, memory tm) fp c' (buf', gm') ->
    unbuffer_safe (tsoupd tm t buf' gm') ->
    unbuffer_safe tm.

Lemma tso_valid_pointer_same_compare_ints_TSO_fp_eq :
  forall bm bm' x y,
    (forall b ofs, tso_valid_pointer bm b ofs = tso_valid_pointer bm' b ofs) ->
    compare_ints_TSO_fp x y bm = compare_ints_TSO_fp x y bm'.

Lemma rs_eq_fp_eq :
  forall ge f i rs bm bm',
    (forall b ofs, tso_valid_pointer bm b ofs = tso_valid_pointer bm' b ofs) ->
    Not_lock_instr i ->
    exec_instr_TSO_fp ge f i rs bm = exec_instr_TSO_fp ge f i rs bm'.

Lemma unbuffer_eval_builtin_arg_still :
  forall tm tm' fm fm' t ge a b (rs : Asm.preg -> val) sp,
    unbuffer tm t = Some tm' ->
    strip fm = memory tm -> strip fm' = memory tm' ->
    eval_builtin_arg ge rs sp {| tbuffer := tso_buffers tm t; fmemory := fm |}
                     a b ->
    eval_builtin_arg ge rs sp {| tbuffer := tso_buffers tm' t; fmemory := fm' |}
                     a b.
  
Lemma unbuffer_eval_builtin_args_still :
  forall tm tm' t fm fm' (rs : Asm.preg -> val) sp ge args vargs,
    strip fm = memory tm -> strip fm' = memory tm' ->
    unbuffer tm t = Some tm' ->
    eval_builtin_args ge rs sp {| tbuffer := tso_buffers tm t; fmemory := fm |}
                      args vargs ->
    eval_builtin_args ge rs sp {| tbuffer := tso_buffers tm' t; fmemory := fm' |}
                      args vargs.

Lemma unbuffer_extcall_arg_still :
  forall tm tm' fm fm' t a b rs,
    unbuffer tm t = Some tm' ->
    strip fm = memory tm -> strip fm' = memory tm' ->
    extcall_arg rs {| tbuffer := tso_buffers tm t; fmemory := fm |} a b ->
    extcall_arg rs {| tbuffer := tso_buffers tm' t; fmemory := fm' |} a b.

Lemma unbuffer_extcall_arg_pair_still :
  forall tm tm' fm fm' t a b rs,
    unbuffer tm t = Some tm' ->
    strip fm = memory tm -> strip fm' = memory tm' ->
    extcall_arg_pair rs {| tbuffer := tso_buffers tm t; fmemory := fm |} a b ->
    extcall_arg_pair rs {| tbuffer := tso_buffers tm' t; fmemory := fm' |} a b.

Lemma store_args_rec_fmem_apply_buf_hd_still :
  forall args bi bf fm fm' b ofs tys bm,
    apply_buffer_item bi (strip fm) = Some (strip fm') ->
    store_args_rec_fmem {| tbuffer := bi :: bf; fmemory := fm |} b ofs args tys
    = Some bm ->
    store_args_rec_fmem {| tbuffer := bf; fmemory := fm' |} b ofs args tys =
    Some {| tbuffer := tl (tbuffer bm); fmemory := fm' |}.

Lemma tso_step_buf_add :
  forall ge fl c c' gm gm' buf buf' fp,
    tsostep ge fl c (buf, gm) fp c' (buf', gm') ->
    exists buf'', buf' = buf ++ buf''.

Lemma tso_step_buf_not_empty_gm_stable :
  forall ge fl c c' gm gm' buf buf' fp,
    buf <> nil ->
    tsostep ge fl c (buf, gm) fp c' (buf', gm') ->
    gm = gm'.

Lemma tsofstep_unbuffer_still :
  forall ge c c' tm tm' fm fm' fl fp tsofm' t,
    unbuffer tm t = Some tm' -> embed (memory tm) fl fm ->
    tsofstep ge c {| tbuffer := tso_buffers tm t; fmemory := fm |} fp
             c' tsofm' ->
    embed (memory tm') fl fm' ->
    tsofstep ge c {| tbuffer := tso_buffers tm' t; fmemory := fm' |} fp
             c' {| tbuffer := (tl (tbuffer tsofm')); fmemory := fm' |}.
  
Lemma tsostep_unbuffer_still :
  forall ge fl fls c c' tm gm gm' buf buf' fp t tm' n,
    FLs_embed fls tm -> FLists.get_fl fls n = fl ->
    tso_buffers tm t = buf -> memory tm = gm ->
    tsostep ge fl c (buf, gm) fp c' (buf', gm') ->
    unbuffer tm t = Some tm' ->
    tsostep ge fl c (tso_buffers tm' t, memory tm') fp c'
            (tl buf', memory tm').
  
Lemma thrdpool_tupdate_valid_original_valid :
  forall {GE : TSOGlobEnv.t} (thdp thdp' : @TSOThrdPool.t GE) (t t' : tid) c,
    TSOThrdPool.update thdp t' c thdp' ->
    TSOThrdPool.valid_tid thdp' t ->
    TSOThrdPool.valid_tid thdp t.

Lemma thrdpool_tupdate_valid_still_valid :
  forall {GE : TSOGlobEnv.t} (thdp thdp' : @TSOThrdPool.t GE) (t t' : tid) c,
    TSOThrdPool.update thdp t' c thdp' ->
    TSOThrdPool.valid_tid thdp t ->
    TSOThrdPool.valid_tid thdp' t.

Lemma thrdpool_push_valid_original_valid :
  forall {GE : TSOGlobEnv.t} (thdp thdp' : @TSOThrdPool.t GE) (t t' : tid) c new_ix sg,
    TSOThrdPool.push thdp t' new_ix c sg = Some thdp' ->
    TSOThrdPool.valid_tid thdp' t ->
    TSOThrdPool.valid_tid thdp t.

Lemma thrdpool_pop_valid_original_valid :
  forall {GE : TSOGlobEnv.t} (thdp thdp' : @TSOThrdPool.t GE) (t t' : tid),
    TSOThrdPool.pop thdp t' = Some thdp' ->
    TSOThrdPool.valid_tid thdp' t ->
    TSOThrdPool.valid_tid thdp t.

Ltac unfold_unchanged_perm :=
  unfolds unchanged_perm;
  unfolds unchanged_validity; unfolds GMem.eq_perm;
  unfolds GMem.valid_block; unfolds GMem.perm.

Ltac unfold_belongsto :=
  unfolds belongsto; unfolds Locs.belongsto.

Ltac unfold_effects :=
  unfolds effects; do 4 unfolds Locs.union.

Lemma buf_item_unbuf_locality_1 :
  forall bi m m',
    unbuf_locality_1 bi m m'.