Module RefinesDefs

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 Permissions Emem MemoryMachine TSOMemoryMachine.

Definition cons' {A B:Type} (x:B*list A) (l:list (B* (list A))) : list (B *(list A)) :=
  match snd x with
    | nil => l
    | _ => x::l
  end.

Infix ":::" := cons' (at level 60, right associativity).

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

Inductive rstate :=
| SAbort
| SReturn (v: list val)
| SIntra (r:INJECT.regset).

Definition ext_event : Type := list mem_event.

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

Module Bigstep.
Section bigstep.

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


Inductive bigstep: state -> statement -> atomic_flag -> list (thread_id*ext_event) -> (mem*buffer*rstate) -> Prop :=
  | exec_skip: forall m b rs af,
      bigstep (m,b,rs) Sskip af nil (m,b,SIntra rs)

  | exec_fence: forall m m' b l rs (r:bool) m'',
      ext_trace tid Interleaved (m,b) l (m',nil) ->
      (if r then mem_step tid m' (MEperm PErelease) m'' else m'=m'') ->
      bigstep (m,b,rs) (Sfence r) Interleaved l (m'',nil,SIntra rs)

  | exec_leak: forall m b rs l arg out af,
      bigstep (m,b,rs) (Leak l arg out) af nil (m,b,SIntra rs)

  | exec_atomic_block: forall m b l m' rs body fence rs'' m''',
      ext_trace tid Interleaved (m,b) l (m',nil) ->
      no_atomic_in_statement body ->
      bigstep (m',empty_buffer,rs) body Atomic nil (m''',empty_buffer,rs'') ->
      bigstep (m,b,rs) (Satomic fence body) Interleaved l (m''',empty_buffer,rs'')

  | exec_op: forall m b rs v op args res rs' af,
      eval_operation ge sp op (map rs args) = Some v ->
      rs' = (rs##res <- v) ->
      bigstep (m,b,rs) (Sop op args res) af nil (m,b,SIntra rs')

  | exec_freeperm: forall m rs m' b b' l af,
      ext_trace tid af (m,b) l (m',b') ->
      mem_step tid m' (MEperm PEfreeperm) m' ->
      bigstep (m,b,rs) Sfreeperm af l (m',b',SIntra rs)

  | exec_release: forall m rs m' l m'' b b' af,
      ext_trace tid af (m,b) l (m',b') ->
      mem_step tid m' (MEperm PErelease) m'' ->
      bigstep (m,b,rs) Srelease af l (m'',b',SIntra rs)

  | exec_request: forall m rs m' l m'' rp addr args a b b' af,
      ext_trace tid af (m,b) l (m',b') ->
      eval_addressing ge sp addr (map rs args) = Some (Vptr a) ->
      mem_step tid m' (MEperm (PErequest rp a)) m'' ->
      bigstep (m,b,rs) (Srequestperm rp addr args) af l (m'',b',SIntra rs)

  | exec_load: forall ap m rs a v addr args res rs' m' l b b' af,
      ext_trace tid af (m,b) l (m',b') ->
      (if addr_in_buf a b'
       then buf_load a b' = Some v
           ∧ wf_val v ∧ wf_ptr a
           ∧ match ap with
               | Global => ∀ t', m'.(perms) a = HiddenBy t' → tid = t'
               | Local => readable_perm m' a tid
             end
       else mem_step tid m' (MEread ap false a v) m') ->
      (∀ x k, ¬ In (FBufItem x k) b') →
      rs' = (rs##res <- v) ->
      eval_addressing ge sp addr (map rs args) = Some (Vptr a) ->
      Val.has_type v Tint ->
      bigstep (m,b,rs) (Sload ap addr args res) af l (m',b',SIntra rs')

  | exec_store_interleaved: forall rs a v addr args src m m' m'' l ap b b' b'' (r:bool) (ESWF1: wf_val v)
      (ESWF2: wf_ptr a)
      (HTv: Val.has_type (rs src) Tint),
      ext_trace tid Interleaved (m,b) l (m',b') ->
      (if r then mem_step tid m' (MEperm PErelease) m'' else m'=m'') ->
      eval_addressing ge sp addr (map rs args) = Some (Vptr a) ->
      v = (rs src) ->
      b'' = push_item (WBufItem a v) b' ->
      check_perm_store tid m' ap a ->
      safe tid b'' m' ->
      bigstep (m,b,rs) (Sstore r ap addr args src) Interleaved l (m'',b'',SIntra rs)

  | exec_store_atomic: forall rs a v addr args src m ap b m' r
      (HTv: wf_val (rs src)),
      eval_addressing ge sp addr (map rs args) = Some (Vptr a) ->
      v = (rs src) ->
      mem_step tid m (MEwrite r ap a v) m' ->
      b = empty_buffer ->
      bigstep (m,b,rs) (Sstore r ap addr args src) Atomic nil (m',b,SIntra rs)

  | exec_atomic: forall op args res v rs rs' lab m m' m'' l release b,
      ext_trace tid Interleaved (m,b) l (m',empty_buffer) ->
      mem_step tid m' lab m'' ->
      atomic_statement_mem_event release op (map rs args) v lab ->
      rs' = (rs##res <- v) ->
      Val.has_type v Tint ->
      bigstep (m,b,rs) (Satomicmem release op args res) Interleaved l (m'',empty_buffer,SIntra rs')

  | exec_if_true: forall rs cond args ifso ifnot l st m b af,
      eval_condition cond (map rs args) = Some true ->
      bigstep (m,b,rs) ifso af l st ->
      bigstep (m,b,rs) (Sifthenelse cond args ifso ifnot) af l st

  | exec_if_false: forall rs cond args ifso ifnot l st m b af,
      eval_condition cond (map rs args) = Some false ->
      bigstep (m,b,rs) ifnot af l st ->
      bigstep (m,b,rs) (Sifthenelse cond args ifso ifnot) af l st

  | exec_while_true: forall rs cond args body m m' rs' st'' l1 l2 b b' af,
      eval_condition cond (map rs args) = Some true ->
      bigstep (m,b,rs) body af l1 (m',b',SIntra rs') ->
      bigstep (m',b',rs') (Swhile cond args body) af l2 st'' ->
      safe tid b' m' ->
      bigstep (m,b,rs) (Swhile cond args body) af (l1++l2) st''

  | exec_while_true_abrupt: forall rs cond args body m st l b af,
      eval_condition cond (map rs args) = Some true ->
      bigstep (m,b,rs) body af l st ->
      (forall m' rs', st <> (m',SIntra rs')) ->
      bigstep (m,b,rs) (Swhile cond args body) af l st

  | exec_while_false: forall rs cond args body m b af,
      eval_condition cond (map rs args) = Some false ->
      bigstep (m,b,rs) (Swhile cond args body) af nil (m,b,SIntra rs)

  | exec_repeat: forall cond args body st l st' af,
      bigstep st (Sseq body (Swhile (Op.negate_condition cond) args body)) af l st' ->
      bigstep st (Srepeat body cond args) af l st'

  | exec_seq st m' rs' stmt1 stmt2 l1 l2 st' b' af
      :
      bigstep st stmt1 af l1 (m',b',SIntra rs') ->
      bigstep (m',b',rs') stmt2 af l2 st' ->
      safe tid b' m' ->
      bigstep st (Sseq stmt1 stmt2) af (l1++l2) st'

  | exec_seq_abrupt st stmt1 stmt2 l st' af
      :
      bigstep st stmt1 af l st' ->
      (forall m' rs', st' <> (m',SIntra rs')) ->
      bigstep st (Sseq stmt1 stmt2) af l st'

  | exec_return m rs res b af
      :
      bigstep (m,b,rs) (Sreturn res) af nil (m,b,SReturn (map rs res))

  | exec_abort rs m e b af (r:bool)
      : bigstep (m,b,rs) (Sabort af r e) af nil (m,b,SAbort)

  | exec_assert_true rs cond args m b af
      : eval_condition cond (map rs args) = Some true ->
      bigstep (m,b,rs) (Sassume cond args) af nil (m,b,SIntra rs)

  | exec_branch_left s1 s2 st l st' af
      :
      bigstep st s1 af l st' ->
      bigstep st (Sbranch s1 s2) af l st'

  | exec_branch_right s1 s2 st l st' af
      :
      bigstep st s2 af l st' ->
      bigstep st (Sbranch s1 s2) af l st'

  | exec_loop_end m rs s b af
      :
      bigstep (m,b,rs) (Sloop s) af nil (m,b,SIntra rs)

  | exec_loop_next st s tr1 m rs tr2 st' b af
      :
      bigstep st s af tr1 (m,b,SIntra rs) ->
      bigstep (m,b,rs) (Sloop s) af tr2 st' ->
      safe tid b m ->
      bigstep st (Sloop s) af (tr1++tr2) st'

  | exec_loop_next_abrupt st s st' l af
      :
      bigstep st s af l st' ->
      (forall m' rs', st' <> (m',SIntra rs')) ->
      bigstep st (Sloop s) af l st'.

End bigstep.

End Bigstep.

Inductive bigstep ge sp tid: state -> statement -> atomic_flag -> list (thread_id*ext_event) -> mem*buffer*rstate -> Prop :=
  | bigstep_def: forall m rs stmt af tr m' s' tr' m'' b b' b''
    (SAFE: safe tid b m),
    Bigstep.bigstep ge sp tid (m,b,rs) stmt af tr (m',b',s') ->
    ext_trace tid af (m',b') tr' (m'',b'') ->
    bigstep ge sp tid (m,b,rs) stmt af (tr++tr') (m'',b'',s').


Definition refines (stmt1 stmt2:statement) : Prop :=
  forall ge sp tid af tr st st',
    bigstep ge sp st tid stmt1 af tr st' ->
    bigstep ge sp st tid stmt2 af tr st'.



Lemma ext_trace_safe_left_aux: forall tid af mb tr mb',
  ext_trace tid af mb tr mb' -> safe tid (snd mb) (fst mb).

Lemma ext_trace_safe_left: forall tid af m b tr m' b',
  ext_trace tid af (m,b) tr (m',b') -> safe tid b m.
Hint Resolve ext_trace_safe_left.

Lemma ext_trace_safe_right_aux: forall tid af mb tr mb',
  ext_trace tid af mb tr mb' -> safe tid (snd mb') (fst mb').

Lemma ext_trace_safe_right: forall tid af m b tr m' b',
  ext_trace tid af (m,b) tr (m',b') -> safe tid b' m'.
Hint Resolve ext_trace_safe_right.