Module RefinesRules2

Require Import Utf8 Coqlib.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Libtactics.
Require Import INJECT.
Require Import Classical.
Require Import Utils.
Require Import Emem Permissions MemoryMachine TSOMemoryMachine RefinesDefs RefinesUtils.
Require Import RefinesRules AllRefinesRulesAux.

Import Bigstep.

Lemma atomic_empty' : forall stmt ge sp tid st st' l af,
  bigstep ge sp tid st stmt af l st' ->
  af = Atomic →
  snd (fst st) = empty_buffer →
  snd (fst st') = empty_buffer.
Corollary atomic_empty : forall stmt ge sp tid m m' b rs rs' l,
  bigstep ge sp tid (m, empty_buffer, rs) stmt Atomic l (m', b, rs') ->
  b = empty_buffer.


  Definition release_before_load t' d' a s : perm_map :=
    fun x =>
      if Ptr.eq_dec x a then
        match d' a with
          | FrozenBy q => FrozenBy (if Rset.mem t' s then q else Rset.remove t' q)
          | HiddenBy _ => empty_perm
        end
      else d' x.
  Lemma release_case {t t' d a d' s} :
    t <> t' ->
    d a = FrozenBy s ->
    release t (upd_perm d a (FrozenBy (Rset.add t' s))) d' ->
    release t d (release_before_load t' d' a s).

    Lemma release_case' {t t' d a d' s} :
    t <> t' ->
    d a = FrozenBy s ->
    release t (upd_perm d a (FrozenBy (Rset.add t' s))) d' ->
      upd_read_perm_set (release_before_load t' d' a s) a t' d'.

Lemma pfrup t d r a s t' :
  d a = FrozenBy s ->
  range_has_store_perm t (upd_perm d a (FrozenBy (Rset.add t' s))) r ->
  range_has_store_perm t d r.

Ltac ptr :=
  match goal with
    | [H : context [Ptr.eq_dec ?a ?b ] |- _ ] => destruct (Ptr.eq_dec a b);[subst|]
    | [|- context [Ptr.eq_dec ?a ?b ] ] => destruct (Ptr.eq_dec a b);[subst|]
  end.

Lemma localread_leftmover_mem_step: forall t m2 e m3,
  mem_step t m2 e m3 ->
  forall t' a v inbuf,
    t <> t' ->
    mem_step t' m2 (MEread Local inbuf a v) m2 ->
    mem_step t' m3 (MEread Local inbuf a v) m3.

  Lemma pfruh t d r a t' :
    d a = empty_perm \/ d a = HiddenBy t' ->
    range_has_store_perm t (upd_perm d a (HiddenBy t')) r ->
    range_has_store_perm t d r.

Lemma localstore_leftmover_mem_step: forall t m2 e m3,
  mem_step t m2 e m3 ->
  forall t' m1 a v,
    t <> t' ->
    mem_step t' m1 (MEwrite false Local a v) m2 ->
    exists m',
      mem_step t m1 e m' /\ mem_step t' m' (MEwrite false Local a v) m3.

Inductive trace_mem_inv t P (m:mem) : list mem_event -> mem -> Prop :=
 | trace_mem_inv_nil: forall (TM: P m), trace_mem_inv t P m nil m
 | trace_mem_inv_cons: forall l m' e m''
   (TM1: trace_mem_inv t P m' l m'')
   (TM2: mem_step t m e m')
   (TM3: P m),
   trace_mem_inv t P m (e::l) m''.

Lemma trace_mem_inv_eq1_1 : forall t P s1 tr s2,
  trace_mem_inv t P s1 tr s2 -> forall e s3,
  P s3 ->
  mem_step t s2 e s3 -> trace_mem_inv t P s1 (tr++ (e::nil)) s3.

Lemma trace_mem_inv_eq1 : forall t b s1 tr s2,
  mem_trace t b s1 tr s2 -> trace_mem_inv t b s1 (rev tr) s2.

Lemma trace_mem_inv_eq2_1 : forall t P s1 tr s2,
  mem_trace t P s1 tr s2 -> forall e s0,
  P s0 ->
  mem_step t s0 e s1 -> mem_trace t P s0 (tr++ (e::nil)) s2.

Lemma trace_mem_inv_safe_snd: forall t t' b s1 tr s2,
  trace_mem_inv t' (safe t b) s1 tr s2 -> safe t b s2.
Hint Resolve trace_mem_inv_safe_snd.

Lemma trace_mem_inv_safe_fst: forall t t' b s1 tr s2,
  trace_mem_inv t' (safe t b) s1 tr s2 -> safe t b s1.
Hint Resolve trace_mem_inv_safe_fst.

Lemma trace_mem_inv_eq2 : forall t b s1 tr s2,
  trace_mem_inv t b s1 tr s2 -> mem_trace t b s1 (rev tr) s2.

Lemma localread_leftmover_trace_mem: forall t t' b m2 l m3,
  trace_mem_inv t' b m2 l m3 ->
  forall a v inbuf, t<>t' ->
    mem_step t m2 (MEread Local inbuf a v) m2 ->
    mem_step t m3 (MEread Local inbuf a v) m3.

Lemma localwrite_leftmover_mem_trace: forall t b t' m2 l m3,
  trace_mem_inv t' (safe t b) m2 l m3 ->
  forall m1 a v , t<>t' ->
    safe t b m1 ->
    mem_step t m1 (MEwrite false Local a v) m2 ->
    exists m',
      trace_mem_inv t' (safe t b) m1 l m' /\ mem_step t m' (MEwrite false Local a v) m3.

Lemma perm_step_readable_perm: forall t d1 d2 p t' e,
      readable_perm d1 p t ->
      perm_step t' d1 e d2 ->
      t <> t' ->
      readable_perm d2 p t.


Lemma unbuffer_n_readable_perm: forall t N m1 b1 b1' m1_flushed d1,
  unbuffer_n t (m1,b1) N (MEM m1_flushed d1, b1') ->
  forall p t' e m2,
      readable_perm d1 p t ->
      mem_step t' m1 e m2 ->
      t <> t' ->
      forall m2_flushed d2,
          unbuffer_n t (m2,b1) N (MEM m2_flushed d2, b1') ->
          readable_perm d2 p t.

Require Import LocalLoad.

Lemma frms' t n :
  ∀ b m1 m1f,
    unbuffer_n' t (m1,b) n (m1f, empty_buffer) →
    ∀ inbuf a v,
      mem_step t m1f (MEread Local inbuf a v) m1f →
      ∀ m2,
        le t m1 m2 →
        ∀ m2f,
          unbuffer_n' t (m2,b) n (m2f, empty_buffer) →
          mem_step t m2f (MEread Local inbuf a v) m2f.

Lemma flush_read_mem_step: forall t b m1 m1_flushed,
  flush t b m1 m1_flushed ->
  forall inbuf a v t' e m2,
    mem_step t m1_flushed (MEread Local inbuf a v) m1_flushed ->
    mem_step t' m1 e m2 ->
    t <> t' ->
    forall m2_flushed,
      flush t b m2 m2_flushed ->
      mem_step t m2_flushed (MEread Local inbuf a v) m2_flushed.

Require Import Relation_Operators.
Require Import Operators_Properties.

Lemma flush_read_unbuffer: forall t b m1 m1_flushed,
  flush t b m1 m1_flushed ->
  forall inbuf a v b' m2,
    mem_step t m1_flushed (MEread Local inbuf a v) m1_flushed ->
    unbuffer t (m1,b) (m2,b') ->
    forall m2_flushed,
      flush t b' m2 m2_flushed ->
      mem_step t m2_flushed (MEread Local inbuf a v) m2_flushed.

Lemma mem_trace_safe_snd: forall t t' b s1 tr s2,
  mem_trace t' (safe t b) s1 tr s2 -> safe t b s2.
Hint Resolve mem_trace_safe_snd.

Lemma mem_remove : forall t t' s,
  Rset.mem t' (Rset.remove t s) = if peq t' t then false else Rset.mem t' s.

Lemma mem_trace_readable_perm : forall a t' t P m1 e m2,
  mem_trace t P m1 e m2 ->
  readable_perm m1 a t' -> t<>t' ->
  readable_perm m2 a t'.


Lemma addr_in_buf_app' {p b} :
  addr_in_buf p b →
  ∀ b', addr_in_buf p (b ++ b').

Lemma ext_trace_read_mem_step: forall a v st af M1 tr M2,
  ext_trace st af M1 tr M2 ->
  af = Interleaved ->
  let (m'0, b'0) := M1 in
    let (m'1, b) := M2 in
      b=nil ->
      (∀ x k, ¬ In (FBufItem x k) b'0) →
      (if addr_in_buf a b'0
        then
          buf_load a b'0 = Some v
          ∧ wf_val v ∧ wf_ptr a ∧ readable_perm m'0 a st
        else mem_step st m'0 (MEread Local false a v) m'0) ->
 mem_step st m'1 (MEread Local false a v) m'1.

Lemma refines_localload: forall addr args dst f stmt,
  refines
  (Sseq
    (Sload Local addr args dst)
    (Satomic f stmt))
  (Satomic f
    (Sseq
      (Sload Local addr args dst)
      stmt)).


Lemma mem_trace_mon: forall t P1 m1 l m2,
   mem_trace t P1 m1 l m2 ->
   forall P2,
     (forall m, P1 m -> P2 m) ->
     mem_trace t P2 m1 l m2.

Lemma ext_trace_push_item: forall t af mb1 tr mb2,
  ext_trace t af mb1 tr mb2 ->
  forall m1 m2 bi b1 b2,
    mb1 = (m1,push_item bi b1) ->
    mb2 = (m2,b2) ->
    (b2 = empty_buffer /\ exists m1', exists m2', exists e,
      buf_step t m1' bi e m2' /\
      exists tr1, exists tr2,
        tr = tr1 ++ tr2 /\
        ext_trace t af (m1,b1) tr1 (m1',empty_buffer) /\
        ext_trace t af (m2',empty_buffer) tr2 (m2,empty_buffer))
    \/
    (exists b2', b2 = push_item bi b2' /\
      ext_trace t af (m1,b1) tr (m2,b2')).

Lemma ext_trace_write_mem_step: forall t af mb1 tr mb2,
  ext_trace t af mb1 tr mb2 ->
  let (m1,b1) := mb1 in
  let (m2,b2) := mb2 in
  forall a v m0,
    b1 = empty_buffer ->
    mem_step t m0 (MEwrite false Local a v) m1 ->
    exists m',
      ext_trace t af (m0,b1) tr (m',b2) /\
      mem_step t m' (MEwrite false Local a v) m2.

Lemma ext_trace_hidden_perm_inv: forall tid af mb tr mb',
  ext_trace tid af mb tr mb' ->
  let '(m,_) := mb in
  let '(m',_) := mb' in
    forall a, m.(perms) a = HiddenBy tid -> m'.(perms) a = HiddenBy tid.

Lemma refines_localstore_aux ge sp tid m b rs addr args dst f stmt af tr m' b' s' :
  bigstep ge sp tid (m, b, rs)
          (Sseq (Sstore false Local addr args dst) (Satomic f stmt))
          af tr (m', b', s') →
   bigstep ge sp tid (m, b, rs)
           (Satomic f (Sseq (Sstore false Local addr args dst) stmt))
           af tr (m', b', s').

Lemma refines_localstore: forall addr args dst f stmt,
  refines
  (Sseq
    (Sstore false Local addr args dst)
    (Satomic f stmt))
  (Satomic f
    (Sseq
      (Sstore false Local addr args dst)
      stmt)).

Lemma local_before_abort_bigstep:
  forall tid ge sp st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  local_before_abort stmt = true ->
  let '(m,b,rs) := st in
  let '(m',b',s') := st' in
    safe tid b m ->
    safe tid b' m' ->
    ext_trace tid af (m,b) tr (m',b').

Lemma local_before_abort_last:
  forall ge sp tid st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  local_before_abort stmt = true ->
  let (m',s') := st' in
  match s' with
    | SReturn _ => False
    | SAbort => False
    | _ => True
  end.


Lemma refines_stmt_abort: forall stmt af e r,
  local_before_abort stmt = true ->
  refines (Sseq stmt (Sabort af r e)) (Sabort af r e).

Lemma refines_abort_stmt: forall stmt af r e,
  refines (Sseq (Sabort af r e) stmt) (Sabort af r e).

Lemma refines_loop_branch_abort_aux: forall tid ge sp st S af tr st',
  bigstep ge sp tid st S af tr st' -> forall e stmt af0 r,
  S = Sloop (Sbranch (Sabort af0 r e) stmt) ->
  let '(m,b,rs) := st in
  let '(m',b',s') := st' in
    safe tid b m ->
    safe tid b' m' ->
  bigstep ge sp tid st (Sbranch (Sseq (Sloop stmt) (Sabort af0 r e)) (Sloop stmt)) af tr st'.

Lemma refines_loop_branch_abort: forall af r e stmt,
  refines
    (Sloop (Sbranch (Sabort af r e) stmt))
    (Sbranch (Sseq (Sloop stmt) (Sabort af r e)) (Sloop stmt)).


Lemma refines_branch_dup: forall stmt1 stmt2,
  refines
    (Sbranch stmt1 (Sbranch stmt1 stmt2))
    (Sbranch stmt1 stmt2).

Lemma left_mover_bigstep:
  forall tid ge sp st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  forall (R1:no_atomic_in_statement stmt=true),
  left_mover stmt = true -> forall m'' b'' tr',
  let '(m',b',s') := st' in
  let '(m,b,s) := st in
    ext_trace tid af (m',b') tr' (m'',b'') ->
    exists m0,
      ext_trace tid af (m,b) (tr++tr') (m0,b'') /\
      bigstep ge sp tid (m0,b'',s) stmt Atomic nil (m'',b'',s') /\
      ( b=b').

Lemma left_mover_abort_last:
  forall ge sp tid st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  left_mover stmt = true ->
  let (m',s') := st' in
  match s' with
    | SReturn _ => False
    | SAbort => False
    | _ => True
  end.

Lemma refines_left_mover : forall stmt1 f stmt2,
  left_mover stmt1 = true ->
  no_atomic_in_statement stmt1 = true ->
  no_atomic_in_statement stmt2 = true ->
  refines
    (Sseq stmt1 (Satomic f stmt2))
    (Satomic f (Sseq stmt1 stmt2)).





  
Lemma left_mover_strong_abort_last:
  forall ge sp tid st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  left_mover_strong stmt = true ->
  let '(m', _,s') := st' in
  match s' with
    | SReturn _ => False
    | _ => True
  end.

Lemma no_atomic_in_left_move_conv s :
  no_atomic_in_statement (left_move_conv s) = no_atomic_in_statement s.

Lemma refines_strong_left_mover ge sp tid st S af tr st' :
  bigstep ge sp tid st S af tr st' →
  left_mover_strong S = true →
  no_atomic_in_statement S = true →
  match st' with
    | (m', b', SIntra rs') =>
      ∀ f S' tr',
      ∀ m'' b'' s'',
     no_atomic_in_statement S' = true →
     safe tid b'' m'' →
     bigstep ge sp tid (m', b', rs') (Satomic f S') af tr' (m'', b'', s'') →
     bigstep ge sp tid st (Satomic f (Sseq (left_move_conv S) S')) af (tr ++ tr') (m'', b'', s'')
    | (_, SReturn _) => False
    | (m', b', SAbort) =>
      ∀ f S',
        no_atomic_in_statement S' = true →
        safe tid b' m' →
        bigstep ge sp tid st (Satomic f (Sseq (left_move_conv S) S')) af tr (m', b', SAbort)
  end.


Lemma refines_left_mover_strong : forall stmt1 f stmt2,
  left_mover_strong stmt1 = true ->
  no_atomic_in_statement stmt1 = true ->
  no_atomic_in_statement stmt2 = true ->
  refines
    (Sseq stmt1 (Satomic f stmt2))
    (Satomic f (Sseq (left_move_conv stmt1) stmt2)).

Lemma right_mover_bigstep:
  forall tid ge sp st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  no_atomic_in_statement stmt = true ->
  right_mover stmt = true ->
  let '(m',b',s') := st' in
  let '(m,b,s) := st in
    m = m' /\ b = b' /\ tr = nil /\
      bigstep ge sp tid (m,b,s) stmt Atomic tr (m,b,s').

Lemma refines_right_mover : forall stmt1 f stmt2,
  right_mover stmt2 = true ->
  no_atomic_in_statement stmt1 ->
  no_atomic_in_statement stmt2 ->
  refines
    (Sseq (Satomic f stmt1) stmt2)
    (Satomic f (Sseq stmt1 stmt2)).


Lemma refines_if_atomic : forall cond args f stmt1 stmt2,
  no_atomic_in_statement stmt1 ->
  no_atomic_in_statement stmt2 ->
  refines
    (Sifthenelse cond args (Satomic f stmt1) (Satomic f stmt2))
    (Satomic f (Sifthenelse cond args stmt1 stmt2)).

Lemma refines_fence_load: forall f af addr args dst,
  refines
    (Sseq (Sfence false) (Sload af addr args dst))
    (Satomic f (Sload af addr args dst)).