Module RefinesUtils

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

Lemma cons'_app : forall B A (x:B*list A) l1 l2,
  (x:::l1)++l2 = x:::(l1++l2).
Hint Resolve cons'_app.

Module Env.
Section ge.
Variable ge : genv.
Variable sp: option pointer.

Definition state : Type := (mem * buffer * INJECT.state)%type.

Definition cast t (mb:mem*buffer) : tsomem :=
  let (m,b) := mb in
    TSOMEM m (upd (fun _ => nil) t b).

Inductive intra_step t : state -> thread_event -> state -> Prop :=
| intra_step_not_mem: forall st st' m e
  (ST:INJECT.step ge sp st e st')
  (IS_not_mem:forall e', e <> TEtso e'),
  intra_step t (m, st) e (m, st')
| intra_step_mem: forall m st st' m' e'
  (ST:INJECT.step ge sp st (TEtso e') st')
  (ES:tso_step t (cast t m) e' (cast t m')),
  intra_step t (m, st) (TEtso e') (m', st')
| intra_step_unbuf: forall m st m' bi
  (ES:tso_step t (cast t m) (TSOunbuf bi) (cast t m')),
  intra_step t (m, st) (TEtso (TSOunbuf bi)) (m', st).

Inductive atomic_intra_step t : (mem * INJECT.state) -> thread_event -> (mem * INJECT.state) -> Prop :=
| atomic_intra_step_not_mem: forall st st' m e
  (ST:INJECT.step ge sp st e st')
  (IS_not_mem:forall e', e <> TEtso e'),
  atomic_intra_step t (m, st) e (m, st')
| atomic_intra_step_mem: forall m st st' m' e'
  (ST:INJECT.step ge sp st (TEtso (TSOmem e')) st')
  (AIS1:forall ap ib a v, e' = MEread ap ib a v -> ib = false)
  (AIS2:forall r p v a, e' = MErmw r p v a -> False)
  (ES:mem_step t m e' m'),
  atomic_intra_step t (m, st) (TEato e') (m', st').

Inductive atrace t : (mem * INJECT.state) -> list thread_event -> (mem * INJECT.state) -> Prop :=
| atrace_nil : forall s, atrace t s nil s
| atrace_cons : forall s0 m st e m' st' l
   (AT1:atomic_intra_step t (m, st) e (m', st'))
   (AT2:atrace t s0 l (m,st))
   (AT5:forall ev, e<>TEend ev),
   atrace t s0 (e::l) (m',st').

Inductive atrace_inv t : (mem * INJECT.state) -> list thread_event -> (mem * INJECT.state) -> Prop :=
| atrace_inv_nil : forall s, atrace_inv t s nil s
| atrace_inv_cons : forall s0 m st e m' st' l
   (AT1:atomic_intra_step t (m', st') e (m, st))
   (AT2:atrace_inv t (m,st) l s0)
   (AT3:forall ev, e<>TEend ev),
   atrace_inv t (m',st') (e::l) s0.

Inductive step t : state -> option (thread_id * ext_event) -> state -> Prop :=
  | step_env_mem: forall t' m st e m' b
      (ES0:t<>t')
      (ES:mem_trace t' (safe t b) m e m'),
    step t (m, b, st) (Some (t',e)) (m', b, st)
  | step_intra: forall st st' e
      (ST:intra_step t st e st')
      (ST1:forall e', e <> TEend e')
      (ST2:e<>TEtso TSObeginatomic),
    step t st None st'
  | step_intra_atomic: forall st1 m2 s2 m3 s3 st4 f l
      (ST1:intra_step t st1 (TEtso TSObeginatomic) (m2,nil,s2))
      (ST0:atrace t (m2,s2) l (m3,s3))
      (ST2:intra_step t (m3,nil,s3) (TEtso (TSOendatomic f)) st4),
    step t st1 None st4.

Inductive trace t (s0:state) : list (thread_id * ext_event) -> state -> Prop :=
| trace_nil : trace t s0 nil s0
| trace_cons1 : forall tr s1 e s2
  (HT1: trace t s0 tr s1)
  (HT2: step t s1 (Some e) s2),
  trace t s0 (e:::tr) s2
| trace_cons2 : forall tr s1 s2
  (HT1: trace t s0 tr s1)
  (HT2: step t s1 None s2),
  trace t s0 tr s2.

Inductive trace_inv t : state -> list (thread_id * ext_event) -> state -> Prop :=
| trace_inv_nil : forall s0, trace_inv t s0 nil s0
| trace_inv_cons1 : forall tr s1 e s2 s3
  (HT1: trace_inv t s2 tr s3)
  (HT2: step t s1 (Some e) s2),
  trace_inv t s1 (e:::tr) s3
| trace_inv_cons2 : forall tr s1 s2 s3
  (HT1: trace_inv t s2 tr s3)
  (HT2: step t s1 None s2),
  trace_inv t s1 tr s3.

Lemma trace_inv_eq1_1 : forall t s1 tr s2,
  trace_inv t s1 tr s2 -> forall e s3,
  step t s2 (Some e) s3 -> trace_inv t s1 (tr++ (e:::nil)) s3.

Lemma trace_inv_eq1_2 : forall t s1 tr s2,
  trace_inv t s1 tr s2 -> forall s3,
  step t s2 None s3 -> trace_inv t s1 tr s3.

Lemma trace_inv_eq1 : forall t s1 tr s2,
  trace t s1 tr s2 -> trace_inv t s1 (rev tr) s2.

Lemma trace_inv_eq2_1 : forall t s1 tr s2,
  trace t s1 tr s2 -> forall e s0,
  step t s0 (Some e) s1 -> trace t s0 (tr++ (e:::nil)) s2.

Lemma trace_inv_eq2_2 : forall t s1 tr s2,
  trace t s1 tr s2 -> forall s0,
  step t s0 None s1 -> trace t s0 tr s2.

Lemma trace_inv_eq2 : forall t s1 tr s2,
  trace_inv t s1 tr s2 -> trace t s1 (rev tr) s2.

Lemma trace_inv_eq : forall t s1 tr s2,
  trace_inv t s1 tr s2 <-> trace t s1 (rev tr) s2.

End ge.


End Env.

Inductive ext_trace_inv tid : atomic_flag -> (mem*buffer) -> list (thread_id*ext_event) -> (mem*buffer) -> Prop :=
| ext_trace_inv_nil : forall m b af
  (SAFE: safe tid b m),
  ext_trace_inv tid af (m,b) nil (m,b)
| ext_trace_inv_mem: forall t m1 e m2 l m3 b2 b1
  (ET1: t <> tid)
  (SAFE: safe tid b2 m3),
  mem_trace t (safe tid b2) m2 e m3 ->
  ext_trace_inv tid Interleaved (m1,b1) l (m2,b2) ->
  ext_trace_inv tid Interleaved (m1,b1) ((t,e):::l) (m3,b2)
| ext_trace_unbuf: forall m1 b1 m2 b2 l m3 b3,
  unbuffer tid (m2,b2) (m3,b3) ->
  ext_trace_inv tid Interleaved (m1,b1) l (m2,b2) ->
  ext_trace_inv tid Interleaved (m1,b1) l (m3,b3).

Lemma ext_trace_inv_eq1_1 : forall t af s1 tr s2,
  ext_trace t af s1 tr s2 -> af = Interleaved ->
  let (m2,b2) := s2 in
    forall t' e m3, t'<>t ->
      (safe t b2 m3) ->
      mem_trace t' (safe t b2) m2 e m3 -> ext_trace t Interleaved s1 (tr++ ((t',e):::nil)) (m3,b2).

Lemma ext_trace_inv_eq1_2 : forall t af s1 tr s2,
  ext_trace t af s1 tr s2 -> af = Interleaved ->
  let (m2,b2) := s2 in
    forall b3 m3,
      unbuffer t (m2,b2) (m3,b3) -> ext_trace t Interleaved s1 tr (m3,b3).

Lemma ext_trace_inv_eq1 : forall t af s1 tr s2,
  ext_trace_inv t af s1 tr s2 -> ext_trace t af s1 (rev tr) s2.

Lemma ext_trace_inv_eq2_1 : forall t af s1 tr s2,
  ext_trace_inv t af s1 tr s2 -> af = Interleaved ->
  let (m1,b1) := s1 in
    forall t' e m0, t'<>t ->
      (safe t b1 m0) ->
      mem_trace t' (safe t b1) m0 e m1 -> ext_trace_inv t Interleaved (m0,b1) (tr++ ((t',e):::nil)) s2.

Lemma ext_trace_inv_eq2_2 : forall t af s1 tr s2,
  ext_trace_inv t af s1 tr s2 -> af = Interleaved ->
  let (m1,b1) := s1 in
    forall m0 b0,
      unbuffer t (m0,b0) (m1,b1) -> ext_trace_inv t Interleaved (m0,b0) tr s2.

Lemma ext_trace_inv_eq2 : forall t af s1 tr s2,
  ext_trace t af s1 tr s2 -> ext_trace_inv t af s1 (rev tr) s2.

Lemma unbuffer_env_step: forall ge sp tid mb mb' st,
  unbuffer tid mb mb' ->
  Env.step ge sp tid (mb, st) None (mb', st).


Lemma ext_trace_inv_env_trace: forall ge sp tid af m l m',
  ext_trace_inv tid af m l m' -> forall m0 st0 st l',
  Env.trace ge sp tid (m0,st0) l' (m,st) ->
  Env.trace ge sp tid (m0,st0) (l++l') (m',st).

Lemma ext_trace_env_trace: forall ge sp tid af m l m',
  ext_trace tid af m l m' -> forall m0 st0 st l',
  Env.trace ge sp tid (m0,st0) l' (m,st) ->
  Env.trace ge sp tid (m0,st0) (rev l++l') (m',st).

Hint Resolve ext_trace_nil.

Lemma bigstep_simpl : forall tid ge sp m b r stmt2' af tr m' b' r',
  Bigstep.bigstep ge sp tid (m,b,r) stmt2' af tr (m',b',r') ->
  safe tid b m -> safe tid b' m' ->
  bigstep ge sp tid (m,b,r) stmt2' af tr (m',b',r').

Lemma ext_trace_app: forall t af m l1 m1,
  ext_trace t af m l1 m1 ->
  forall l2 m2,
    ext_trace t af m1 l2 m2 ->
    ext_trace t af m (l1++l2) m2.
Hint Resolve ext_trace_app.