Module SimulationByRefines

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 Utils.
Require Import RTLinject.
Require Import TSOmachine.
Require Import Classical.
Require Import Relations.
Require Import INJECT.
Require Import Permissions Emem MemoryMachine TSOMemoryMachine
 RTLinject RefinesDefs RefinesUtils AllRefinesRulesAux.

Lemma safe_True: forall tid b m, safe tid b m.
Hint Resolve safe_True.

Section backwardsim_from_RTLinject_smallstep.

Variable ge : genv.

Inductive atrace_inv t : (tsomem * intra_state)%type -> list thread_event -> (tsomem * intra_state)%type -> Prop :=
| atrace_inv_nil : forall s, atrace_inv t s nil s
| atrace_inv_cons : forall s0 m st e m' st' l
   (AT1:intra_step ge t (m, st) e s0)
   (AT2:atrace_inv t s0 l (m', st'))
   (AT3:e<>TEtso TSObeginatomic)
   (AT4:forall f, e<>TEtso (TSOendatomic f))
   (AT5:forall ev, e<>TEend ev),
   atrace_inv t (m,st) (l++e::nil) (m',st').



Inductive trace_inv : RTLinject.state -> list (thread_id * list thread_event) -> RTLinject.state -> Prop :=
| trace_inv_nil : forall s0, trace_inv s0 nil s0
| trace_inv_cons : forall tr s1 e s2 s3
  (HT1: trace_inv s2 tr s3)
  (HT2: astep ge s1 e s2),
  trace_inv s1 (tr++e::nil) s3.

Lemma trace_inv_eq1: forall s1 tr s2,
  trace_inv s1 tr s2 -> forall e s3,
  astep ge s2 e s3 -> trace_inv s1 (e::tr) s3.

Lemma trace_inv_eq2: forall s1 tr s2,
  trace ge s1 tr s2 -> forall e s0,
  astep ge s0 e s1 -> trace ge s0 (tr++e::nil) s2.

Lemma trace_inv_eq: forall s1 tr s2,
  trace ge s1 tr s2 <-> trace_inv s1 tr s2.

Lemma trace_step_right : forall s1 tr s2,
  trace ge s1 tr s2 -> forall s0 e,
  astep ge s0 e s1 ->
  trace ge s0 (tr++e::nil) s2.

Lemma trace_app_inv : forall tr1 s1 tr2 s2,
  trace ge s1 (tr1++tr2) s2 ->
  exists s, trace ge s1 tr2 s /\ trace ge s tr1 s2.

Lemma trace_app : forall s2 tr1 s3,
  trace ge s2 tr1 s3 ->
  forall tr2 s1,
  trace ge s1 tr2 s2 ->
  trace ge s1 (tr1++tr2) s3.

Definition filter_not_tid {A:Type} tid (l:list (thread_id * A)) : list (thread_id * A) :=
  filter (fun tid_e => negb (peq tid (fst tid_e))) l.
  
Lemma filter_not_tid_app : forall A tid (l1 l2:list (thread_id*A)),
  filter_not_tid tid (l1++l2) = (filter_not_tid tid l1)++(filter_not_tid tid l2).

Lemma In_filter : forall A f (l:list A) x,
  In x (filter f l) -> f x = true /\ In x l.

Lemma f_true_In_filter : forall A f (l:list A) x,
  f x = true -> In x l -> In x (filter f l).

Lemma filter_id : forall A (f:A->bool) (l:list A),
  (forall x, In x l -> f x = true) ->
  filter f l = l.

Lemma filter_nil : forall A (f:A->bool) (l:list A),
  (forall x, In x l -> f x = false) ->
  filter f l = nil.

Lemma filter_filter : forall A f (l:list A),
  filter f (filter f l) = filter f l.

Lemma app_eq_nil: forall A (l1 l2:list A),
  l1 ++ l2 = nil -> l1 = nil /\ l2 = nil.

Lemma filter_cons_inv : forall A f (l l2:list A) x,
  filter f l = x :: l2 ->
  exists l1', exists l2',
    l=l1'++x::l2' /\
    (forall y, In y l1' -> f y = false) /\
    l2 = filter f l2'.

Lemma filter_app_inv : forall A f (l l1 l2:list A),
  filter f l = l1++l2 ->
  exists l1', exists l2',
    l=l1'++l2' /\
    l1 = filter f l1' /\
    l2 = filter f l2'.

Lemma filter_not_tid_cons: forall A tid tid' (e:A) tr,
  tid <> tid' ->
  filter_not_tid tid ((tid', e)::tr) = (tid',e) :: filter_not_tid tid tr.

Lemma In_filter_not_tid_iff: forall A tid tid' (e:A) tr,
  tid <> tid' ->
  (In (tid', e) tr <-> In (tid',e) (filter_not_tid tid tr)).

Lemma filter_not_tid_app_cons : forall A (e:A) tid tid' tr1 tr2 tr,
  tid <> tid' ->
  filter_not_tid tid tr = filter_not_tid tid (tr1 ++ (tid', e) :: tr2) ->
  exists tr1', exists tr2',
    tr = tr1' ++ (tid', e) :: tr2' /\
    filter_not_tid tid tr1 = filter_not_tid tid tr1' /\
    filter_not_tid tid tr2 = filter_not_tid tid tr2'.

Lemma filter_not_tid_app_cons_eq : forall A (e:A) tid tr,
  filter_not_tid tid (tr ++ (tid, e) :: nil) = filter_not_tid tid tr.

  

Lemma filter_fullevent_list_nil : forall l,
  (forall e, ~ In (TEext e) l) ->
  filter_fullevent_list l = nil.

Lemma filter_not_tid_eq_filter_fullevent : forall tid tr,
  (forall e l, In (tid,l) tr -> ~ In (TEext e) l) ->
  filter_fullevent tr = filter_fullevent (filter_not_tid tid tr).

Variable wf_state: RTLinject.state -> Prop.


Definition almost_high_trace (s1: RTLinject.state) (tr: list (thread_id * list thread_event)) (s2:RTLinject.state) : Prop :=
  trace ge s1 tr s2 /\
  forall id tr1 tr2,
    tr = tr1++(id,TEbegin BeginLow::nil)::tr2 ->
    (forall ev' l, In (id,l) tr1 -> ~ In (TEend ev') l) /\ forall k, In (id,TEbegin k::nil) tr2 -> k = BeginHigh.

Definition refines_smallstep (stmt1 stmt2:statement) : Prop :=
  forall ge sp t m rs tr st stf e,
    Env.trace ge sp t (m,NormalState rs stmt1 Kend) tr st ->
    Env.intra_step ge sp t st (TEend e) stf ->
    exists st',
      Env.trace ge sp t (m,NormalState rs stmt2 Kend) tr st' /\
      Env.intra_step ge sp t st' (TEend e) stf.

Definition ge_correct_wrt_refines (refines:statement->statement->Prop) (ge:genv) : Prop :=
  forall b f,
    Genv.find_funct_ptr ge b = Some (Internal f) ->
    forall pc inj args dst s,
      (fn_code f)!pc = Some (Iinject inj args dst s) ->
      refines inj.(ic_stmt_low) inj.(ic_stmt_high).

Lemma atrace_no_end: forall tid l m s' m' s'',
  atrace ge tid (m, s') l (m', s'') ->
  forall k, ~ In (TEend k) l.

Lemma rtl_step_injected_state: forall s e s',
  rtli_step ge s e s' ->
  inject_state s -> inject_state s' \/ (exists ev, e = TEend ev).

Lemma trace_with_two_begins_aux : forall s1 s2 tr,
  trace ge s1 tr s2 ->
  (forall tr1 id k tr2,
    tr = tr1 ++ (id, TEbegin k::nil) :: tr2 ->
    (forall ev' l, In (id, l) tr1 -> ~ In (TEend ev') l) ->
    let '(tso, st) := s2 in
      match st!id with
        | Some s => inject_state s
        | None => false
      end).

Lemma atrace_keep_inject_state: forall t l m' s s'' m,
  inject_state s ->
  atrace ge t (m, s) l (m', s'') ->
  inject_state s''.

Lemma atrace_no_begin: forall tid s l m s' m' s'',
  rtli_step ge s (TEtso TSObeginatomic) s' ->
  atrace ge tid (m, s') l (m', s'') ->
  forall k, ~ In (TEbegin k) l.

Lemma trace_with_two_begins : forall tr1 s1 s2 tr,
  trace ge s1 tr s2 ->
  (forall id k tr2,
    tr = tr1 ++ (id, TEbegin k::nil) :: tr2 ->
    (forall ev' l, In (id, l) tr1 -> ~ In (TEend ev') l) ->
    forall k' l, In (id,l) tr1 -> ~ In (TEbegin k') l).

Lemma filter_not_tid_eq_In : forall tid tid' (x:list thread_event) tr1 tr2,
  filter_not_tid tid tr1 = filter_not_tid tid tr2 ->
  tid <> tid' ->
  In (tid',x) tr1 -> In (tid',x) tr2.
Hint Resolve filter_not_tid_eq_In.

Lemma atrace_no_ext: forall tid l m s' m' s'',
  inject_state s' ->
  atrace ge tid (m, s') l (m', s'') ->
  forall k, ~ In (TEext k) l.

Lemma trace_with_pending_begin_no_ext : forall tr1 s1 s2 tr,
  trace ge s1 tr s2 ->
  (forall id k tr2,
    tr = tr1 ++ (id, TEbegin k :: nil) :: tr2 ->
    (forall ev' l, In (id, l) tr1 -> ~ In (TEend ev') l) ->
   forall k' l, In (id,l) tr1 -> ~ In (TEext k') l).


Variable refines_implies_trace_transformation1: forall st1 tr1 tid tr2 st2 ev,
    wf_state st1 ->
    trace ge st1 ((tid,TEend ev::nil)::tr1++(tid, TEbegin BeginLow::nil)::tr2) st2 ->
    (forall ev' l, In (tid,l) tr1 -> ~ In (TEend ev') l) ->
    exists tr1',
      trace ge st1 ((tid,TEend ev::nil)::tr1'++(tid, TEbegin BeginHigh::nil)::tr2) st2 /\
      (forall ev' l, In (tid,l) tr1'-> ~ In (TEend ev') l) /\
      filter_not_tid tid tr1 = filter_not_tid tid tr1'.

Lemma almost_high_trace_and_one_step : forall s1 tr s2 e s3,
  wf_state s1 ->
  almost_high_trace s1 tr s2 ->
  astep ge s2 e s3 ->
  exists tr',
    almost_high_trace s1 tr' s3 /\ filter_fullevent tr' = filter_fullevent (e::tr).

Lemma low_code_in_inject_state : forall s1 tr s2,
  trace ge s1 tr s2 ->
  forall id tr1 tr2,
    tr = tr1++(id,TEbegin BeginLow::nil)::tr2 ->
    (forall ev' l, In (id,l) tr1 -> ~ In (TEend ev') l) ->
    exists s, (snd s2)!id = Some s /\ inject_state s.

Lemma refines_implies_almost_backwardsim: forall s1 tr s2,
  wf_state s1 ->
  trace ge s1 tr s2 ->
  exists tr',
    almost_high_trace s1 tr' s2 /\ filter_fullevent tr' = filter_fullevent tr.

Lemma refines_implies_backwardsim': forall st1 tr st2,
  wf_state st1 ->
  low_trace ge st1 tr st2 ->
  (forall tid s, (snd st2)!tid = Some s -> inject_state s = false) ->
  exists tr',
    high_trace ge st1 tr' st2 /\ filter_fullevent tr' = filter_fullevent tr.

End backwardsim_from_RTLinject_smallstep.





Module simulation1.
Section simulation1.
Variable ge : genv.
Variable sp: option pointer.
Variable tid: thread_id.


Fixpoint filter_mem (tr:list thread_event) : list mem_event :=
  match tr with
    | nil => nil
    | e::tr =>
      match e with
        | TEtso (TSOunbuf e) => e::(filter_mem tr)
        | TEtso (TSOmem (MEwrite true ap p _)) => (MEperm PErelease)::(MEperm (PEcheck_store ap p))::(filter_mem tr)
        | TEtso (TSOmem (MEwrite false ap p _)) => (MEperm (PEcheck_store ap p))::(filter_mem tr)
        | TEtso (TSOmem (MEread ap false p v)) => (MEread ap false p v)::(filter_mem tr)
        | TEtso (TSOmem (MEread ap true p _)) => (MEperm (PEcheck_load ap p))::(filter_mem tr)
        | TEtso (TSOmem (MErmw r p v i)) => (MErmw r p v i)::(filter_mem tr)
        | TEtso (TSOmem (MEperm pe)) => (MEperm pe)::(filter_mem tr)
        | TEato e => e::(filter_mem tr)
        | _ => filter_mem tr
      end
  end.

Inductive match_state : RTLinject.state -> Env.state -> Prop :=
| R_def1: forall ts m st stack c pc rs regs
    (R1: ts!tid = Some (RIInjectState stack c sp pc rs regs st)),
    match_state (m, ts) (m.(shared_mem),m.(buffers)tid,st).

Fixpoint proj_trace (tr:list (thread_id*list thread_event)) : list (thread_id*list mem_event) :=
  match tr with
    | nil => nil
    | (tid',e)::tr =>
      if peq tid tid'
        then proj_trace tr
        else (tid',filter_mem e):::(proj_trace tr)
  end.

Lemma proj_trace_app : forall tr1 tr2,
  proj_trace (tr1 ++ tr2) = (proj_trace tr1)++(proj_trace tr2).

Ltac clean_eq_some :=
  match goal with
    | h1: ?X = Some _, h2: ?X = Some _ |- _ => rewrite h2 in h1; inversion h1; subst; clear h1
  end.

Lemma upd_upd_s `{X: Type} `{EqDec X} {Y} (f: X → Y) p v' v:
  (upd (upd f p v') p v) = upd f p v.

Lemma tso_step_cast: forall t (m:tsomem) e m',
  tso_step t m e m' ->
  (forall tid', e <> INJECT.TSOstart tid') ->
  tso_step t (Env.cast t (m.(shared_mem), buffers m t)) e (Env.cast t (m'.(shared_mem), buffers m' t)).

Lemma atrace_inthemiddle: forall t stack c sp pc regs rs l m' s'' m is2,
  atrace ge t (m, RIInjectState stack c sp pc rs regs is2) l (m', s'') ->
  exists is, s'' = (RIInjectState stack c sp pc rs regs is)
    /\ Env.atrace ge sp t (m,is2) l (m',is).

Lemma atrace_trace_mem b : forall t sp l m is m' is',
  Env.atrace ge sp t (m, is) l (m', is') ->
    mem_trace t (safe tid b) m (filter_mem l) m'.

Lemma tso_step_unbuf_mem_step: forall t m e m',
  tso_step t m (TSOunbuf e) m' ->
  mem_step t m e m'.


Lemma simul: forall st1 st2 st1' e,
  astep ge st1 e st2 ->
  match_state st1 st1' ->
    (exists e', e = (tid, (TEend e')::nil))
    \/
    (match_state st2 st1' /\ fst e = tid)
    \/
    exists st2',
      match_state st2 st2' /\
      exists e', Env.step ge sp tid st1' e' st2' /\
        match e' with
          | None => fst e = tid
          | Some e' => tid<>(fst e) /\ snd e' = filter_mem (snd e) /\ fst e = fst e'
        end.

Lemma trace_simul: forall st0 tr st1,
  trace ge st0 tr st1 ->
  (forall ev', ~ In (tid,(TEend ev')::nil) tr) -> forall st0',
  match_state st0 st0' ->
  exists st1',
    Env.trace ge sp tid st0' (proj_trace tr) st1' /\
    match_state st1 st1'.

Inductive match_state2 : RTLinject.state -> Env.state -> RTLinject.state -> list (thread_id*ext_event) -> Env.state -> Prop :=
| R2_def: forall ts1 ts2 st2 st tr m1 m2 st1 regs rs pc c stack b1 b2
    (R2: ts2!tid = Some (RIInjectState stack c sp pc rs regs st2))
    (R3: forall tid', tid <> tid' -> ts1!tid'=ts2!tid')
    (R4: ts1!tid = Some (RIInjectState stack c sp pc rs regs st1))
    (R6: Env.trace ge sp tid (m2,b2 tid,st2) tr st)
    (R7: forall tid', tid <> tid' -> b1 tid' = b2 tid'),
    match_state2 (TSOMEM m1 b1, ts1) (m2,b2 tid,st2) (TSOMEM m2 b2, ts2) tr st.

Lemma rev_cons' : forall B A (x:B*list A) l,
  rev (x:::l) = (rev l)++x:::nil.

Lemma proj_trace_rev: forall tr,
  proj_trace (rev tr) = rev (proj_trace tr).

Lemma proj_trace_app_cons : forall tr ev,
  (proj_trace tr ++ ev:::nil) = (rev (ev:::(proj_trace (rev tr)))).

Lemma exists_atrace: forall t stack c sp pc rs regs,
  forall l S S' m m' st st',
    S = RIInjectState stack c sp pc rs regs st ->
    S' = RIInjectState stack c sp pc rs regs st' ->
    Env.atrace ge sp t (m, st) l (m', st') ->
    atrace ge t (m,S) l (m',S').

Lemma exists_astep: forall stack c sp pc rs st4 m st f m4 ts ts' regs,
  ts!tid = Some (RIInjectState stack c sp pc rs regs st) ->
  ts' = ts!tid <- (RIInjectState stack c sp pc rs regs st4) ->
  forall st2 l st3 b,
    b tid = nil ->
    Env.atrace ge sp tid (m,st2) l (m4,st3) ->
    Env.intra_step ge sp tid (m, nil, st) (TEtso TSObeginatomic) (m,nil,st2) ->
    Env.intra_step ge sp tid (m4,nil,st3) (TEtso (TSOendatomic f)) (m4, nil, st4) ->
    astep ge (TSOMEM m b,ts) (tid,l) (TSOMEM m4 b,ts').

Lemma Env_atrace_no_end: forall ge sp t st1 tr st2,
  Env.atrace ge sp t st1 tr st2 ->
  forall ev, ~ In (TEend ev) tr.

Lemma upd_comm {X: Type} `{EqDec X} {Y: Type} {t t'} {f: X → Y} {x x'} :
  t' ≠ t →
  upd (upd f t x) t' x' = upd (upd f t' x') t x.

Lemma tso_step_o : forall bufs m tid tid' b ev m' bufs',
  tid <> tid' ->
  ev ≠ TSOstart tid →
  tso_step tid' (TSOMEM m bufs) ev (TSOMEM m' bufs') ->
  tso_step tid' (TSOMEM m (upd bufs tid b)) ev (TSOMEM m' (upd bufs' tid b)).

Lemma tso_step_same_buf : forall bufs m tid tid' ev m' bufs',
  tid <> tid' ->
  (forall newtid, ev <> (TSOstart newtid)) ->
  tso_step tid' (TSOMEM m bufs) ev (TSOMEM m' bufs') ->
  bufs tid = bufs' tid.

Lemma upd_upd {X Y} `{EqDec X} {f: X → Y} {x} :
  upd f x (f x) = f.

Lemma upd_inv {X Y} `{EqDec X} {f: X → Y} {x y y'} :
  upd f x y = upd f x y' → y = y'.

Lemma tso_step_cast2: forall t m e m' b b' bufs,
  tso_step t (Env.cast t (m, b)) e (Env.cast t (m', b')) ->
  bufs t = b ->
  (forall newtid, e <> (TSOstart newtid)) ->
  tso_step t (TSOMEM m bufs) e (TSOMEM m' (upd bufs t b')).

Lemma ptree_set_same: forall A (m:PTree.t A) x v,
  m!x = Some v ->
  m ! x <- v = m.

Lemma env_step_none: forall ts tid stack c sp pc rs regs s1 s2 m1 b1 m2 b2 b,
  ts ! tid = Some (RIInjectState stack c sp pc rs regs s1) ->
  b1 = b tid ->
  Env.step ge sp tid (m1,b1,s1) None (m2,b2,s2) ->
  exists l,
    astep ge (TSOMEM m1 b,ts) (tid,l)
      (TSOMEM m2 (upd b tid b2),ts!tid <- (RIInjectState stack c sp pc rs regs s2)) /\
    (forall ev, ~ In (TEend ev) l).

Lemma proj_trace_false: forall tid0 e tr,
  tid <> tid0 ->
  proj_trace ((tid0,e)::tr) = (tid0,filter_mem e):::proj_trace tr.


Lemma atrace_filter_mem: forall tid' st e st',
  atrace ge tid' st e st' ->
  filter_mem e = nil -> forall m0,
  atrace ge tid' (m0, snd st) e (m0, snd st').



Lemma Trace_inv_eq: forall ge sp t s1 tr s2,
  Env.trace_inv ge sp t s1 (rev tr) s2 <-> Env.trace ge sp t s1 tr s2.

Lemma proj_trace_app_cons' : forall tr ev,
  (proj_trace (tr ++ ev:::nil)) = (rev (proj_trace (ev:::nil) ++ (proj_trace (rev tr)))).

Lemma buf_step_mem_step: forall t m bi e m',
  buf_step t m bi e m' -> mem_step t m e m'.

Lemma simul3': forall tid' S2 TR st,
  tid' <> tid ->
  Env.trace_inv ge sp tid S2 TR st ->
  forall tr e m2 b1 m1 ts1 b2 st2 st3 regs rs pc c stack ts2,
  S2 = (m2, b2 tid, st2) ->
  TR = ((tid', e) :: proj_trace tr) ->
  ts2 ! tid = Some (RIInjectState stack c sp pc rs regs st2) ->
  (∀tid' : positive, tid ≠ tid' → ts1 ! tid' = ts2 ! tid') ->
  (ts1 ! tid = Some (RIInjectState stack c sp pc rs regs st3)) ->
  (∀tid' : positive, tid ≠ tid' → b1 tid' = b2 tid') ->
  exists stt1', exists st1', exists stt1'',
    match_state2 (TSOMEM m1 b1,ts1) stt1'' st1' (proj_trace (rev tr)) st /\
    Env.trace ge sp tid (m2,b2 tid,st2) nil stt1' /\
    Env.step ge sp tid stt1' (Some (tid', e)) stt1''.


Lemma simul3: forall st0 tid' e stt1 st1 tr st,
  tid' <> tid ->
  match_state2 st0 stt1 st1 (proj_trace tr++(tid',e)::nil) st ->
  exists stt1', exists st1', exists stt1'',
    match_state2 st0 stt1'' st1' (proj_trace tr) st /\
    Env.trace ge sp tid stt1 nil stt1' /\
    Env.step ge sp tid stt1' (Some (tid', e)) stt1''.

Lemma atrace_filter_mem_nil: forall e,
  filter_mem e = nil ->
  forall tid' m s m' s', atrace ge tid' (m, s) e (m', s') ->
    forall m0, atrace ge tid' (m0, s) e (m0, s').


Lemma env_trace_nil: forall S1 tr S2,
  Env.trace_inv ge sp tid S1 tr S2 ->
  forall ts stack c pc rs regs s1 s2 m1 b1 m2 b2 b,
    tr = nil ->
    S1 = (m1,b1,s1) ->
    S2 = (m2,b2,s2) ->
    ts ! tid = Some (RIInjectState stack c sp pc rs regs s1) ->
    b1 = b tid ->
    exists tr,
      trace_inv ge (TSOMEM m1 b,ts) tr
      (TSOMEM m2 (upd b tid b2),ts!tid <- (RIInjectState stack c sp pc rs regs s2)) /\
      proj_trace tr = nil /\
      filter_not_tid tid tr = nil /\
      ∀ev : end_event, ∀l : list thread_event, In (tid, l) tr → ¬In (TEend ev) l.

Lemma atrace_mem_trace_atrace: forall P tid' e m1 m1' s s' m2 m2',
  atrace ge tid' (m1, s) e (m1', s') ->
  mem_trace tid' P m2 (filter_mem e) m2' ->
  atrace ge tid' (m2, s) e (m2', s').

Lemma simul2: forall st1 tid' e st2 stt1' stt1 tr st,
  (snd st1)!tid<>None ->
  astep ge st1 (tid',e) st2 ->
  tid' <> tid ->
  match_state2 st1 stt1' stt1 (proj_trace (tr++(tid',e)::nil)) st ->
    exists stt2, exists stt2', exists tr',
      match_state2 st2 stt2' stt2 (proj_trace tr) st /\
      trace ge stt1 ((tid',e)::tr') stt2 /\
      proj_trace tr' = nil /\
      filter_not_tid tid tr' = nil /\
      (forall ev l, In (tid,l) tr' -> ~ In (TEend ev) l).


Lemma astep_none_none: forall m1 ts1 e m2 ts2,
   astep ge (m1,ts1) e (m2,ts2) ->
   ts1 ! tid <> None ->
   ts2 ! tid <> None \/ e = (tid, TEexit :: nil).
  

Lemma simul1: forall st1 e st2 stt1' stt1 tr st,
  astep ge st1 (tid,e) st2 ->
  (forall ev, e <> (TEend ev::nil)) ->
  match_state2 st1 stt1' stt1 (proj_trace tr) st->
  match_state2 st2 stt1' stt1 (proj_trace tr) st.

Lemma trace_keep_tid_inject_state: forall st0 tr st1,
  trace ge st0 tr st1 -> forall s,
  (snd st0)!tid = Some s -> inject_state s ->
  (forall ev, ~ In (tid,TEend ev::nil) tr) ->
  exists s, (snd st1)!tid = Some s /\ inject_state s.

Lemma trace_simul_final_aux: forall st0 tr st1,
  trace ge st0 tr st1 -> forall tr0 st2 s st0' st
  (Hs: exists s, (snd st0)!tid = Some s /\ inject_state s),
  (forall ev, ~ In (tid,TEend ev::nil) tr) ->
  trace_inv ge st1 tr0 st2 ->
  match_state2 st0 s st0' (proj_trace (tr0++tr)) st ->
  exists st1', exists tr', exists s',
    trace ge st0' tr' st1' /\
    match_state2 st1 s' st1' (proj_trace tr0) st /\
    proj_trace tr = proj_trace tr' /\
    filter_not_tid tid tr = filter_not_tid tid tr' /\
    (forall ev l, In (tid,l) tr' -> ~ In (TEend ev) l).

Lemma trace_simul_final: forall st1 tr st2,
  trace ge st1 tr st2 -> forall s st1' st,
  (exists s, (snd st1)!tid = Some s /\ inject_state s) ->
  (forall ev, ~ In (tid,TEend ev::nil) tr) ->
  match_state2 st1 s st1' (proj_trace tr) st ->
  exists st2', exists tr', exists s',
    trace ge st1' tr' st2' /\
    match_state2 st2 s' st2' nil st /\
    proj_trace tr = proj_trace tr' /\
    filter_not_tid tid tr = filter_not_tid tid tr' /\
    (forall ev l, In (tid,l) tr' -> ~ In (TEend ev) l).

End simulation1.

Lemma wf_state_invariant_rtl_step: forall refines ge,
  ge_correct_wrt_refines refines ge ->
  forall s e s',
    rtli_step ge s e s' ->
    wf_intra_state refines s ->
    wf_intra_state refines s'.

Lemma wf_state_invariant_astep: forall refines ge,
  ge_correct_wrt_refines refines ge ->
  forall st1 e st2,
    wf_istate refines st1 ->
    astep ge st1 e st2 ->
    wf_istate refines st2.

Lemma wf_state_invariant_trace: forall refines ge,
  ge_correct_wrt_refines refines ge ->
  forall st1 tr st2,
    trace ge st1 tr st2 ->
    wf_istate refines st1 ->
    wf_istate refines st2.

Lemma atrace_not_TEend : forall ge tid st1 tr st2,
  atrace ge tid st1 tr st2 ->
  forall ev, ~ In (TEend ev) tr.

Lemma refines_implies_trace_transformation1: forall ge st1,
  ge_correct_wrt_refines refines_smallstep ge ->
  wf_istate refines_smallstep st1 ->
  forall tr1 tid tr2 st2 ev,
    trace ge st1 ((tid,TEend ev::nil)::tr1++(tid, TEbegin BeginLow::nil)::tr2) st2 ->
    (forall ev' l, In (tid,l) tr1 -> ~ In (TEend ev') l) ->
    exists tr1',
      trace ge st1 ((tid,TEend ev::nil)::tr1'++(tid, TEbegin BeginHigh::nil)::tr2) st2 /\
      (forall ev' l, In (tid,l) tr1'-> ~ In (TEend ev') l) /\
      filter_not_tid tid tr1 = filter_not_tid tid tr1'.
  
End simulation1.

Section equiv_big_small.

Context {fundef: Type}.
Variable ge: genv.
Variable sp: option pointer.
Variable tid: thread_id.


Lemma env_trace_inv_app: forall ge sp s1 l1 s2,
  Env.trace_inv ge sp tid s1 l1 s2 -> forall s3 l2,
  Env.trace_inv ge sp tid s2 l2 s3 ->
  Env.trace_inv ge sp tid s1 (l1++l2) s3.

Lemma env_atrace_inv_app: forall ge sp s1 l1 s2,
  Env.atrace_inv ge sp tid s1 l1 s2 -> forall s3 l2,
  Env.atrace_inv ge sp tid s2 l2 s3 ->
  Env.atrace_inv ge sp tid s1 (l1++l2) s3.

Lemma env_trace_inv_nothing_from_return: forall st1 l st2,
  Env.trace_inv ge sp tid st1 l st2 -> forall m m' rs' stmt k,
    st1 = (m, ReturnState) ->
    st2 = (m', NormalState rs' stmt k) -> False.

Lemma env_atrace_inv_nothing_from_return: forall st1 l st2,
  Env.atrace_inv ge sp tid st1 l st2 -> forall m m' rs' stmt k,
    st1 = (m, ReturnState) ->
    st2 = (m', NormalState rs' stmt k) -> False.

Fixpoint app_cont (k1 k2:continuation) : continuation :=
  match k1 with
    | Kstmt s k1 => Kstmt s (app_cont k1 k2)
    | Kendatomic b k1 => Kendatomic b (app_cont k1 k2)
    | Kend => k2
  end.

Lemma in_atomic_app : forall k1 k2 f k,
  in_atomic k1 = Some (f,k) ->
    in_atomic (app_cont k1 k2) = Some (f,app_cont k k2).

Lemma in_atomic_app' : forall k1 k2,
  in_atomic k1 = None ->
  in_atomic (app_cont k1 k2) = in_atomic k2.

Lemma env_atrace_incr_cont : forall st1 l st2,
  Env.atrace ge sp tid st1 l st2 -> forall m1 m2 rs1 rs2 body1 body2 k1 k2 k,
 st1 = (m1, NormalState rs1 body1 k1) ->
 st2 = (m2, NormalState rs2 body2 k2) ->

 Env.atrace ge sp tid
   (m1, NormalState rs1 body1 (app_cont k1 k)) l
   (m2, NormalState rs2 body2 (app_cont k2 k)).

Lemma env_atrace_inv_incr_cont : forall st1 l st2,
  Env.atrace_inv ge sp tid st1 l st2 -> forall m1 m2 rs1 rs2 body1 body2 k1 k2 k,
 st1 = (m1, NormalState rs1 body1 k1) ->
 st2 = (m2, NormalState rs2 body2 k2) ->
 Env.atrace_inv ge sp tid
   (m1, NormalState rs1 body1 (app_cont k1 k)) l
   (m2, NormalState rs2 body2 (app_cont k2 k)).


Lemma env_trace_inv_incr_cont: forall st1 l st2,
Env.trace_inv ge sp tid st1 l st2 -> forall k m1 rs1 body1 k1 m2 rs2 body2 k2,
 st1 = (m1, NormalState rs1 body1 k1) ->
 st2 = (m2, NormalState rs2 body2 k2) ->

 Env.trace_inv ge sp tid
   (m1, NormalState rs1 body1 (app_cont k1 k)) l
   (m2, NormalState rs2 body2 (app_cont k2 k)).


Lemma exec_trace_nil_aux : forall af m l m',
  ext_trace tid af m l m' -> snd m = nil -> l = nil -> m=m'.

Lemma exec_trace_nil : forall af m m',
  ext_trace tid af (m,nil) nil m' -> m'=(m,nil).

Lemma ext_trace_keep_empty_buffer : forall a st tr st',
  ext_trace tid a st tr st' ->
  snd st = nil -> snd st' = nil.

Lemma bigstep_keep_empty_buffer_aux : forall st stmt a tr st',
  Bigstep.bigstep ge sp tid st stmt a tr st' ->
  tr = nil ->
  a = Atomic ->
  no_atomic_in_statement stmt ->
  let '(m,b,rs) := st in
  let '(m',b',rs') := st' in
  b = nil -> b'=nil.

Lemma bigstep_keep_empty_buffer : forall m rs stmt m' b' rs',
  Bigstep.bigstep ge sp tid (m,nil,rs) stmt Atomic nil (m',b',rs') ->
  no_atomic_in_statement stmt ->
  b'=nil.

Lemma bigstep_implies_atrace : forall st stmt a tr st',
  Bigstep.bigstep ge sp tid st stmt a tr st' ->
  tr = nil ->
  a = Atomic ->
  no_atomic_in_statement stmt ->
  let '(m,b,rs) := st in
  b = nil ->
    match st' with
      | (m',b',SIntra rs') => exists l,
        Env.atrace_inv ge sp tid (m,NormalState rs stmt Kend) l (m',NormalState rs' Sskip Kend)
      | (m',b',SAbort) => exists l, exists rs', exists r, exists e, exists k',
        Env.atrace_inv ge sp tid (m,NormalState rs stmt Kend) l (m',NormalState rs' (Sabort Atomic r e) k') /\ in_atomic k' = None
      | (m',b',SReturn v) => exists l, exists st',
        Env.atrace_inv ge sp tid (m,NormalState rs stmt Kend) l (m',st') /\
        INJECT.step ge sp st' (TEend (ReturnEvent v)) ReturnState
    end.


Fixpoint no_atomic_in_continuation (k:continuation) : Prop :=
  match k with
    | Kend => True
    | Kstmt s k => no_atomic_in_statement s /\ no_atomic_in_continuation k
    | Kendatomic _ _ => False
  end.

Lemma no_atomic_in_continuation_in_atomic: forall k1,
  no_atomic_in_continuation k1 ->
  in_atomic k1 = None.

Definition no_atomic_in_state (s:INJECT.state) : Prop :=
  match s with
    | ReturnState => True
    | NormalState rs stmt k => no_atomic_in_statement stmt /\ no_atomic_in_continuation k
  end.

Lemma env_atrace_no_atomic: forall ge sp st1 l st2,
  Env.atrace_inv ge sp tid st1 l st2 ->
  no_atomic_in_state (snd st1) ->
  no_atomic_in_state (snd st2).

Lemma ext_trace_env_trace_inv: forall a m l m',
  ext_trace tid a m l m' -> forall m0 st0 st,
  Env.trace_inv ge sp tid (m', st) nil (m0,st0) ->
  Env.trace_inv ge sp tid (m, st) l (m0,st0).


Lemma env_atrace_inv_eq1_aux: forall t S l s0,
  Env.atrace ge sp t S l s0 -> forall e m' st',
  let (m, st) := S in
  (forall ev : end_event, e <> TEend ev) ->
  Env.atomic_intra_step ge sp t (m', st') e (m, st) ->
  Env.atrace ge sp t (m', st') (l ++ e::nil) s0.

Lemma env_atrace_inv_eq1:
  forall t st l st',
    Env.atrace_inv ge sp t st l st' -> Env.atrace ge sp t st (rev l) st'.

Lemma env_atrace_inv_eq2_aux: forall t S l s0,
  Env.atrace_inv ge sp t s0 l S -> forall e m' st',
  let (m, st) := S in
  (forall ev : end_event, e <> TEend ev) ->
  Env.atomic_intra_step ge sp t (m, st) e (m', st') ->
  Env.atrace_inv ge sp t s0 (l++e::nil) (m', st').

Lemma env_atrace_inv_eq2:
  forall t st l st',
    Env.atrace ge sp t st l st' -> Env.atrace_inv ge sp t st (rev l) st'.

Lemma no_atomic_in_statement1: forall stmt,
  INJECT.no_atomic_in_statement stmt ->
  no_atomic_in_statement stmt.
Hint Resolve no_atomic_in_statement1.

Lemma bigstep_implies_smallstep_aux : forall st stmt a tr st',
  Bigstep.bigstep ge sp tid st stmt a tr st' ->
  a = Interleaved ->
  let (m,rs) := st in
    match st' with
      | (m',SIntra rs') => Env.trace_inv ge sp tid (m,NormalState rs stmt Kend) tr (m',NormalState rs' Sskip Kend)
      | (m',SAbort) => exists st',
        Env.trace_inv ge sp tid (m,NormalState rs stmt Kend) tr (m',st') /\
        INJECT.step ge sp st' (TEend FailEvent) ReturnState
      | (m',SReturn v) => exists st',
        Env.trace_inv ge sp tid (m,NormalState rs stmt Kend) tr (m',st') /\
        INJECT.step ge sp st' (TEend (ReturnEvent v)) ReturnState
    end.


Definition bigstep_with_small_step ge sp tid m rs stmt tr m' e:=
    exists st, Env.trace ge sp tid (m,NormalState rs stmt Kend) tr st
      /\ Env.intra_step ge sp tid st (TEend e) (m',ReturnState).

Lemma refines_smallstep_def2 : forall stmt1 stmt2,
  refines_smallstep stmt1 stmt2 <->
  (forall ge sp tid m rs tr m' e,
    bigstep_with_small_step ge sp tid m rs stmt1 tr m' e ->
    bigstep_with_small_step ge sp tid m rs stmt2 tr m' e).

Definition end_event_of_rstate (s:rstate) : end_event :=
  match s with
    | SReturn v => ReturnEvent v
    | SAbort => FailEvent
    | SIntra _ => ReturnVoid
  end.

Lemma bigstep_implies_smallstep : forall m rs stmt tr m' s',
  bigstep ge sp tid (m,rs) stmt Interleaved tr (m',s') ->
  bigstep_with_small_step ge sp tid m rs stmt (rev tr) m' (end_event_of_rstate s').

Lemma bigstep_left_ext : forall tid ge sp st stmt af tr st',
  Bigstep.bigstep ge sp tid st stmt af tr st' ->
  af = Interleaved ->
  forall m' b' s' tr' m'', st = (m',b',s') ->
    safe tid (snd (fst st')) (fst (fst st')) ->
    ext_trace tid Interleaved m'' tr' (m',b') ->
    bigstep ge sp tid (m'',s') stmt Interleaved (tr'++tr) st'.

Lemma bigstep_left_ext' : forall tid ge sp m' b' s' stmt tr st',
  bigstep ge sp tid (m',b',s') stmt Interleaved tr st' ->
  forall tr' m'',
    ext_trace tid Interleaved m'' tr' (m',b') ->
    bigstep ge sp tid (m'',s') stmt Interleaved (tr'++tr) st'.

Inductive bigstep_with_cont :
  (mem*buffer*rstate) -> continuation -> list (thread_id * ext_event) -> (mem*buffer*rstate) -> Prop :=
  | bigstep_with_cont_abrupt_in_atomic: forall k s m st' tr stmt,
    (forall rs, s <> SIntra rs) ->
    bigstep_with_cont (m,s) k tr st' ->
    bigstep_with_cont (m,s) (Kstmt stmt k) tr st'

  | bigstep_with_cont_end: forall m1 m2 s tr,
    ext_trace tid Interleaved m1 tr m2 ->
    bigstep_with_cont (m1,s) Kend tr (m2,s)

  | bigstep_with_cont_stmt: forall stmt tr tr' st' k tr'' m b rs st'',
    bigstep ge sp tid (m,b,rs) stmt Interleaved tr st' ->
    bigstep_with_cont st' k tr' st'' ->
    tr''= tr++tr' ->
    bigstep_with_cont (m,b,SIntra rs) (Kstmt stmt k) tr'' st''

  | bigstep_with_cont_enda: forall st tr st' f k,
    bigstep_with_cont st k tr st' ->
    bigstep_with_cont st (Kendatomic f k) tr st'
.

Lemma bigstep_with_cont_ext: forall m2s k tr st',
    bigstep_with_cont m2s k tr st' -> forall m1 l,
    let (m2,s) := m2s in
    ext_trace tid Interleaved m1 l m2 ->
    bigstep_with_cont (m1,s) k (l++tr) st'.

Lemma bigstep_with_cont_abrupt_prop: forall st k tr st',
    bigstep_with_cont st k tr st' ->
    let '(m,b,s) := st in
    let (m',s') := st' in
      (forall rs, s <> SIntra rs) ->
      safe tid b m ->
      ext_trace tid Interleaved (m,b) tr m' /\ s'=s.

Lemma bigstep_with_cont_end_prop: forall st k tr st',
    bigstep_with_cont st k tr st' ->
    let '(m,b,s) := st in
    let (m',s') := st' in k = Kend ->
      safe tid b m ->
      ext_trace tid Interleaved (m,b) tr m' /\ s'=s.


Hint Constructors bigstep_with_cont.



Lemma bigstep_with_cont_abort_nil : forall k m b,
  safe tid b m ->
  bigstep_with_cont (m, b, SAbort) k nil (m, b, SAbort).
Hint Resolve bigstep_with_cont_abort_nil.

Lemma bigstep_with_cont_return_nil : forall k m b v,
  safe tid b m ->
  bigstep_with_cont (m, b, SReturn v) k nil (m, b, SReturn v).
Hint Resolve bigstep_with_cont_return_nil.

Lemma atrace_same_in_atomic: forall st1 l st2,
  Env.atrace ge sp tid st1 l st2 ->
  match st1, st2 with
    | (_, NormalState _ _ k1),(_, NormalState _ _ k2) => in_atomic k1 = in_atomic k2
    | _ , _ => True
  end.

Lemma in_atomic_bigstep_with_cont_abrupt: forall cont f k tr m' s' m s,
  in_atomic cont = Some (f, k) ->
  (forall rs, s <> SIntra rs) ->
  bigstep_with_cont (m, s) k tr (m',s') ->
  bigstep_with_cont (m, s) cont tr (m',s').


Lemma mem_trace_safe_last: forall t' tid b2 m1 e1 m2,
  mem_trace t' (safe tid b2) m1 e1 m2 -> safe tid b2 m2.
Hint Resolve mem_trace_safe_last.


Lemma bigstep_with_cont_stmt2 : forall m b rs stmt st' k tr st'',
 bigstep ge sp tid (m, b, rs) stmt Interleaved nil st' ->
 bigstep_with_cont st' k tr st'' ->
 bigstep_with_cont (m, b, SIntra rs) (Kstmt stmt k) tr st''.

Lemma bigstep_with_cont_skip : forall m2 rs0 tr0 st' cont tr' m3 s'',
  bigstep ge sp tid (m2, rs0) Sskip Interleaved tr0 st' ->
  bigstep_with_cont st' cont tr' (m3, s'') ->
  bigstep_with_cont (m2, SIntra rs0) cont (tr0 ++ tr') (m3, s'').

Lemma upd_buff_eq: forall (buff1 buff2:positive->buffer) tid b1 b2,
  upd buff1 tid b1 = upd buff2 tid b2 -> b1 = b2.

Fixpoint cont2stmt (k:continuation) : statement :=
  match k with
    | Kstmt s k => Sseq s (cont2stmt k)
    | Kendatomic _ _ => Sskip
    | Kend => Sskip
  end.

Inductive end_of_atomic_state (rs:regset) : statement -> rstate -> Prop :=
| end_of_atomic_state_normal : end_of_atomic_state rs Sskip (SIntra rs)
| end_of_atomic_state_return : forall res, end_of_atomic_state rs (Sreturn res) (SReturn (map rs res))
| end_of_atomic_state_abort : forall r e, end_of_atomic_state rs (Sabort Interleaved r e) SAbort.

Lemma smallstep_implies_bigstep_atomic : forall st tr st',
  Env.atrace_inv ge sp tid st tr st' ->
  let (m',s') := st' in
  let '(m,s) := st in
    forall f stf,
    Env.intra_step ge sp tid (m', nil, s') (TEtso (TSOendatomic f)) stf ->
    match s with
      | NormalState rs stmt k =>
        match snd stf with
          | NormalState rs' stmt' _ =>
            exists s'',
            Bigstep.bigstep ge sp tid ((m,nil), rs) (Sseq stmt (cont2stmt k)) Atomic nil (m', nil, s'') /\
            end_of_atomic_state rs' stmt' s''
          | _ => False
        end
      | _ => False
    end.


Lemma smallstep_implies_bigstep_aux : forall st tr st',
  Env.trace_inv ge sp tid st tr st' ->
  let (m',s') := st' in
  let '(m,b,s) := st in
    forall e stf,
    Env.intra_step ge sp tid (m', s') (TEend e) stf ->
    safe tid b m ->
    match s with
      | NormalState rs stmt k =>
        in_atomic k = None ->
        exists s'',
          bigstep_with_cont (m,b, SIntra rs) (Kstmt stmt k) tr (m', s'') /\
          e = end_event_of_rstate s''
      | _ => False
    end.


Lemma smallstep_implies_bigstep : forall m b rs stmt tr m' e,
  bigstep_with_small_step ge sp tid (m,b) rs stmt (rev tr) m' e ->
  safe tid b m ->
  exists s', e = end_event_of_rstate s' /\
    bigstep ge sp tid (m,b,rs) stmt Interleaved tr (m',s').

End equiv_big_small.

Lemma refines_implies_refines_smallstep: forall stmt1 stmt2,
  refines stmt1 stmt2 ->
  refines_smallstep stmt1 stmt2.

Section WEAKEN.
  Context {P Q: statement → statement → Prop}.
  Hypothesis W: ∀ s1 s2, P s1 s2 → Q s1 s2.

  Lemma wf_c_weak c : wf_c P c → wf_c Q c.

  Lemma wf_stack_weak stk : wf_stack P stk → wf_stack Q stk.

  Lemma wf_intra_state_weak s : wf_intra_state P s → wf_intra_state Q s.

  Lemma wf_istate_weak s : wf_istate P s → wf_istate Q s.

  Lemma ge_correct_wrt_weak ge : ge_correct_wrt_refines P ge → ge_correct_wrt_refines Q ge.

End WEAKEN.


Lemma refines_implies_backwardsim_smallstep:
    ∀ ge st1 tr st2,
      ge_correct_wrt_refines refines_smallstep ge →
      wf_istate refines_smallstep st1 ->
      low_trace ge st1 tr st2 ->
      (∀ tid s, (snd st2)!tid = Some s -> inject_state s = false) ->
      ∃ tr',
        high_trace ge st1 tr' st2 ∧ filter_fullevent tr' = filter_fullevent tr.

Theorem refines_implies_backwardsim:
    ∀ ge st1 tr st2,
      ge_correct_wrt_refines refines ge →
      wf_istate refines st1 ->
      low_trace ge st1 tr st2 ->
      (∀ tid s, (snd st2)!tid = Some s -> inject_state s = false) ->
      ∃ tr',
        high_trace ge st1 tr' st2 ∧ filter_fullevent tr' = filter_fullevent tr.