Module RefinesRules

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

Lemma refines_refl : forall stmt, refines stmt stmt.


Lemma refines_trans : forall stmt1 stmt2 stmt3,
  refines stmt1 stmt2 -> refines stmt2 stmt3 -> refines stmt1 stmt3.

Hint Resolve ext_trace_nil.

Hint Resolve ext_trace_app.

Inductive trace_mem_inv t P (m:mem) : list mem_event -> mem -> Prop :=
 | trace_mem_inv_nil: 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_eq2 : forall t b s1 tr s2,
  trace_mem_inv t b s1 tr s2 -> mem_trace t b s1 (rev tr) s2.

Lemma perm_gss:
  forall (d : perm_map) (perm : permission) (p : pointer),
  upd_perm d p perm p = perm.

Lemma perm_gso:
  forall (d : perm_map) (p0 : pointer) (perm : permission) (p : pointer),
    p<>p0 ->
    upd_perm d p0 perm p = d p.


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

Lemma bigstep_left_ext : forall tid ge sp st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  forall m' s' tr' m'', let (mm',ss') := st' in
    forall (SAFE: safe tid (snd mm') (fst mm')),
    st = (m',s') ->
    ext_trace tid af m'' tr' m' ->
    RefinesDefs.bigstep ge sp tid (m'',s') stmt af (tr'++tr) st'.

Lemma refines_seq : forall stmt1 stmt2 stmt1' stmt2',
  refines stmt1 stmt1' -> refines stmt2 stmt2' ->
  refines (Sseq stmt1 stmt2) (Sseq stmt1' stmt2').

Lemma while_repeat_congruence : forall body1 body2 cond args,
  refines body1 body2 ->
  refines (Swhile cond args body1) (Swhile cond args body2) .

Lemma refines_repeat_congruence : forall body1 body2 cond args,
  refines body1 body2 ->
  refines (Srepeat body1 cond args) (Srepeat body2 cond args) .

Lemma refines_remove_leak_left: forall l r1 r2 stmt,
  refines (Sseq (Leak l r1 r2) stmt) stmt.

Lemma refines_remove_leak_right: forall l r1 r2 stmt,
  refines (Sseq stmt (Leak l r1 r2)) stmt.


Lemma refines_branch_same_begin: forall stmt1 stmt2 stmt3,
  refines
     (Sbranch (Sseq stmt1 stmt2) (Sseq stmt1 stmt3))
     (Sseq stmt1 (Sbranch stmt2 stmt3)).

Lemma refines_branch_assoc2 : forall stmt1 stmt2 stmt3,
  refines (Sbranch stmt1 (Sbranch stmt2 stmt3)) (Sbranch (Sbranch stmt1 stmt2) stmt3).

Lemma Rsetmem_empty_false: forall x,
  Rset.mem x Rset.empty = false.
Hint Resolve Rsetmem_empty_false.

Lemma Rset_mem_add_false1 : forall tid t s,
  tid<> t ->
  Rset.mem tid s = false -> Rset.mem tid (Rset.add t s) = false.
Hint Resolve Rset_mem_add_false1.

Lemma Rset_mem_add_false2 : forall t tid s,
  Rset.mem tid (Rset.add t s) = false ->
  Rset.mem tid s = false.
Hint Resolve Rset_mem_add_false2.

Lemma Rset_mem_remove : forall t tid s,
  Rset.mem tid s = false ->
  Rset.mem tid (Rset.remove t s) = false.
Hint Resolve Rset_mem_remove.

Lemma Rset_mem_remove2 : forall t tid s,
  Rset.mem tid (Rset.remove t s) = false ->
  t<>tid ->
  Rset.mem tid s = false.
Hint Resolve Rset_mem_remove2.

Lemma refines_loop_aux : forall stmt stmt',
  refines stmt stmt' ->
  forall ge sp tid st stmt1 af tr st',
    bigstep ge sp tid st stmt1 af tr st' ->
    let '(m,b,rs) := st in safe tid b m ->
    let '(m',b',rs') := st' in safe tid b' m' ->
    stmt1 = Sloop stmt ->
    forall stmt2, stmt2 = Sloop stmt' ->
      RefinesDefs.bigstep ge sp tid st stmt2 af tr st'.

Lemma refines_loop : forall stmt stmt',
  refines stmt stmt' ->
  refines (Sloop stmt) (Sloop stmt').

Lemma refines_if : forall cond args stmt1 stmt1' stmt2 stmt2',
  refines stmt1 stmt1' ->
  refines stmt2 stmt2' ->
  refines (Sifthenelse cond args stmt1 stmt2) (Sifthenelse cond args stmt1' stmt2').

Lemma refines_if1 : forall cond args stmt1 stmt1' stmt2,
  refines stmt1 stmt1' ->
  refines (Sifthenelse cond args stmt1 stmt2) (Sifthenelse cond args stmt1' stmt2).

Lemma refines_if2 : forall cond args stmt1 stmt2 stmt2',
  refines stmt2 stmt2' ->
  refines (Sifthenelse cond args stmt1 stmt2) (Sifthenelse cond args stmt1 stmt2').

Lemma no_atomic_in_statement_dec: forall stmt,
  no_atomic_in_statement stmt = true ->
  INJECT.no_atomic_in_statement stmt.

Require Import Relation_Operators.
Require Import Operators_Properties.

Lemma ext_trace_prefix: forall t af mb1 tr mb2,
  ext_trace t af mb1 tr mb2 ->
  let (m1,b1) := mb1 in
  let (m2,b2) := mb2 in
      exists l', b1 = b2 ++ l'.

Lemma star_unbuffer_safe_aux : forall t mb mb0,
  star (unbuffer t) mb mb0 ->
  safe t (snd mb) (fst mb) ->
  safe t (snd mb0) (fst mb0).

Lemma star_unbuffer_safe : forall t m b m0 b0,
  star (unbuffer t) (m, b) (m0, b0) ->
  safe t b m ->
  safe t b0 m0.
Hint Resolve star_unbuffer_safe.

Lemma star_unbuffer_ext_trace_aux: forall t mb mb',
  star (unbuffer t) mb mb' ->
  let (m',b') := mb in safe t b' m' ->
    ext_trace t Interleaved mb nil mb'.

Lemma star_unbuffer_ext_trace: forall t m b m' b',
  star (unbuffer t) (m,b) (m',b') ->
  safe t b m ->
  ext_trace t Interleaved (m,b) nil (m',b').

Lemma refines_atomic : forall b stmt stmt',
  refines stmt stmt' ->
  no_atomic_in_statement stmt' = true ->
  refines (Satomic b stmt) (Satomic b stmt').

Fixpoint uses (stmt:statement) : Rset.t :=
  match stmt with
    | Sfence _
    | Sabort _ _ _
    | Sfreeperm
    | Sskip
    | Srelease
    | Leak _ _ _ => Rset.empty
    | Sreturn arg => Rset.add_list arg Rset.empty
    | Sassume _ args
    | Sload _ _ args _
    | Satomicmem _ _ args _
    | Sop _ args _
    | Srequestperm _ _ args
    | Sstore _ _ _ args _ => Rset.add_list args Rset.empty
    | Sseq stmt1 stmt2
    | Sbranch stmt1 stmt2 => Rset.union (uses stmt1) (uses stmt2)
    | Sifthenelse _ args stmt1 stmt2 =>
      Rset.add_list args (Rset.union (uses stmt1) (uses stmt2))
    | Swhile _ args body
    | Srepeat body _ args => Rset.add_list args (uses body)
    | Sloop s => uses s
    | Satomic _ body => uses body
  end
.


Lemma mem_add1: forall x,
  Rset.mem x (Rset.add x Rset.empty) = true.

Lemma mem_union_left: forall x s1 s2,
  Rset.mem x s1 -> Rset.mem x (Rset.union s1 s2).

Lemma mem_union_right: forall x s1 s2,
  Rset.mem x s2 -> Rset.mem x (Rset.union s1 s2).

Lemma mem_union_case: forall x s1 s2,
  Rset.mem x (Rset.union s1 s2) ->
  Rset.mem x s1 \/ Rset.mem x s2.

Lemma case_bool: forall b, ~b = true -> b = false.

Lemma no_def_no_change: forall tid ge sp st stmt af l st',
  bigstep ge sp tid st stmt af l st' ->
  let (m,rs) := st in
  match st' with
    | (m',SIntra rs') =>
      forall x,
        Rset.mem x (defs stmt) = false -> rs x = rs' x
    | _ => True
  end.


Lemma eq_args: forall (rs rs':INJECT.regset) args,
  (forall x, In x args -> rs x = rs' x) ->
  map rs args = map rs' args.

Lemma orb_true_left: forall b,
  b || true = true.
Hint Resolve orb_true_left.

Lemma abrupt_correct: forall tid ge sp st stmt af tr st',
  bigstep ge sp tid st stmt af tr st' ->
  (forall m' rs', st' <> (m',SIntra rs')) ->
  abrupt stmt = true.

Lemma refines_swap_assert : forall stmt cond args,
  negb (abrupt stmt) ->
  forallb (fun r => negb (Rset.mem r (defs stmt))) args ->
  refines (Sseq stmt (Sassume cond args)) (Sseq (Sassume cond args) stmt).

Require Import Relation_Operators.
Require Import Operators_Properties.

Lemma ext_trace_empty: forall t af mb tr mb',
  ext_trace t af mb tr mb' ->
  (snd mb) = nil ->
  tr = nil ->
  mb = mb'.

Lemma no_store_ext_trace: forall tid ge sp st stmt af l st',
  bigstep ge sp tid st stmt af l st' ->
  let '(m,b,rs) := st in
  safe tid b m ->
  match st' with
    | (m',b',SIntra rs') =>
      safe tid b' m' ->
      store stmt = false -> ext_trace tid af (m,b) l (m',b')
    | _ => True
  end.

Lemma refines_atomic' : forall b stmt stmt',
  refines_in_atomic stmt stmt' ->
  no_atomic_in_statement stmt' = true ->
  refines (Satomic b stmt) (Satomic b stmt').

Lemma refines_in_atomic_refl : forall stmt, refines_in_atomic stmt stmt.

Lemma refines_in_atomic_trans : forall stmt1 stmt2 stmt3,
  refines_in_atomic stmt1 stmt2 -> refines_in_atomic stmt2 stmt3 -> refines_in_atomic stmt1 stmt3.

Lemma refines_in_atomic_seq : forall stmt1 stmt2 stmt1' stmt2',
  refines_in_atomic stmt1 stmt1' -> refines_in_atomic stmt2 stmt2' ->
  refines_in_atomic (Sseq stmt1 stmt2) (Sseq stmt1' stmt2').

Lemma refines_in_atomic_seq_left : forall stmt1 stmt2 stmt1',
  refines_in_atomic stmt1 stmt1' ->
  refines_in_atomic (Sseq stmt1 stmt2) (Sseq stmt1' stmt2).

Lemma refines_in_atomic_seq_right : forall stmt1 stmt2 stmt2',
  refines_in_atomic stmt2 stmt2' ->
  refines_in_atomic (Sseq stmt1 stmt2) (Sseq stmt1 stmt2').

Lemma ext: forall (rs rs0:INJECT.regset),
  (forall x : positive, rs x = rs0 x) -> rs=rs0.

Lemma mem_empty: forall x,
  Rset.mem x Rset.empty = false.

Lemma not_mem_add1 : forall x y s,
  Rset.mem x s = false ->
  x<>y ->
  Rset.mem x (Rset.add y s) = false.

Lemma not_mem_add2 : forall x y s,
  Rset.mem x (Rset.add y s) = false ->
  Rset.mem x s = false.

Lemma not_mem_add3 : forall x y s,
  Rset.mem x (Rset.add y s) = false -> x<>y.

Lemma not_mem_remove1 : forall x y s,
  Rset.mem x s = false ->
  Rset.mem x (Rset.remove y s) = false.

Lemma not_mem_remove2 : forall x s,
  Rset.mem x (Rset.remove x s) = false.

Lemma not_mem_remove3 : forall x y s,
  Rset.mem x (Rset.remove y s) = false ->
  x=y \/ Rset.mem x s = false.

Lemma not_mem_remove_list1 : forall x y s,
  Rset.mem x s = false ->
  Rset.mem x (Rset.remove_list y s) = false.

Lemma not_mem_remove_list2 : forall x y s,
  In x y ->
  Rset.mem x (Rset.remove_list y s) = false.

Lemma not_mem_remove_list3 : forall x y s,
  Rset.mem x (Rset.remove_list y s) = false ->
  (In x y) \/ Rset.mem x s = false.

Lemma not_mem_inter1 : forall x s1 s2,
  Rset.mem x s1 = false ->
  Rset.mem x (Rset.inter s1 s2) = false.

Lemma not_mem_inter2 : forall x s1 s2,
  Rset.mem x s2 = false ->
  Rset.mem x (Rset.inter s1 s2) = false.

Lemma not_mem_inter3 : forall x s1 s2,
  Rset.mem x (Rset.inter s1 s2) = false ->
  Rset.mem x s1 = false \/
  Rset.mem x s2 = false.

Hint Resolve
  not_mem_add2
  not_mem_add3
  not_mem_inter2
  not_mem_inter1
  not_mem_remove2
  not_mem_remove1
  not_mem_remove_list2
  not_mem_remove_list1
  not_mem_add1
   mem_empty.


Lemma bigstep_and_dead: forall ge sp tid st stmt af l st',
  bigstep ge sp tid st stmt af l st' ->
  let (m,rs) := st in
  let (m',s') := st' in
    forall rs0 s,
      (forall x, Rset.mem x (dead_in stmt s) = false ->
        rs x = rs0 x) ->
      match s' with
        | SIntra rs' =>
          exists rs0',
            (forall x, Rset.mem x s = false -> rs' x = rs0' x)
            /\ bigstep ge sp tid (m,rs0) stmt af l (m',SIntra rs0')
        | _ => bigstep ge sp tid (m,rs0) stmt af l st'
      end.

Lemma rbigstep_left_ext : forall tid ge sp st' stmt af tr m' s',
  RefinesDefs.bigstep ge sp tid (m',s') stmt af tr st' ->
  forall tr' m'',
  ext_trace tid af m'' tr' m' ->
  RefinesDefs.bigstep ge sp tid (m'',s') stmt af (tr'++tr) st'.

Lemma refines_dead_code : forall stmt1 stmt2,
  abrupt stmt1 = false ->
  store stmt1 = false ->
  Rset.forallb (fun r => Rset.mem r (dead_in stmt2 Rset.empty)) (defs stmt1) = true ->
  refines (Sseq stmt1 stmt2) stmt2.

Lemma refines_dead_code_return : forall stmt1 args,
  abrupt stmt1 = false ->
  store stmt1 = false ->
  Rset.forallb (fun r => forallb (fun arg => negb (Peqb r arg)) args) (defs stmt1) = true ->
  refines (Sseq stmt1 (Sreturn args)) (Sreturn args).

Lemma refines_seq_assoc1 : forall stmt1 stmt2 stmt3,
  refines (Sseq stmt1 (Sseq stmt2 stmt3))
          (Sseq (Sseq stmt1 stmt2) stmt3).

Lemma refines_seq_assoc2 : forall stmt1 stmt2 stmt3,
  refines (Sseq (Sseq stmt1 stmt2) stmt3)
          (Sseq stmt1 (Sseq stmt2 stmt3)).

Lemma refines_loop_one_aux :
  forall ge sp tid st s0 s1 af tr st',
    bigstep ge sp tid st (Sseq s0 (Sseq (Sloop s0) s1)) af tr st' ->
    bigstep ge sp tid st (Sseq (Sloop s0) s1) af tr st'.

Lemma refines_skip_aux :
  forall ge sp tid st s af tr st',
    bigstep ge sp tid st (Sseq s Sskip) af tr st' ->
    bigstep ge sp tid st s af tr st'.

Lemma refines_loop_parenthesis_aux : forall ge sp tid st S af tr st',
  bigstep ge sp tid st S af tr st' ->
  forall s1 s2,
    S = Sloop (Sseq s1 s2) ->
    bigstep ge sp tid st (Sbranch (Sseq s1 (Sseq (Sloop (Sseq s2 s1)) s2)) Sskip) af tr st'.

Lemma refines_while_aux: forall ge sp tid st S af tr st',
  bigstep ge sp tid st S af tr st' ->
  forall cond args body,
    S = Swhile cond args body ->
  let '((m',b'),s') := st' in
    safe tid b' m' ->
   bigstep ge sp tid st
     (Sseq (Sloop (Sseq (Sassume cond args) body))
        (Sassume (negate_condition cond) args)) af tr st'.

Lemma refines_while : forall body cond args,
  refines (Swhile cond args body)
          (Sseq
            (Sloop (Sseq (Sassume cond args) body))
            (Sassume (negate_condition cond) args)).

Lemma refines_while_inv_aux: forall ge sp tid st S af tr st',
  bigstep ge sp tid st S af tr st' ->
  forall cond args body,
    S = Sloop (Sseq (Sassume cond args) body) ->
    match st' with
      | (m',SIntra s') =>
        bigstep ge sp tid (m',s') (Sassume (negate_condition cond) args) af nil st' ->
        bigstep ge sp tid st (Swhile cond args body) af tr st'
      | _ => bigstep ge sp tid st (Swhile cond args body) af tr st'
    end.

Lemma refines_while_inv : forall body cond args,
  refines (Sseq
            (Sloop (Sseq (Sassume cond args) body))
            (Sassume (negate_condition cond) args))
          (Swhile cond args body).

Lemma Peqb_false {x y} :
  negb (Peqb x y) -> x <> y.

Lemma not_undef : forall {X v} {a b:X},
    v <> Vundef ->
    (if Val.eq_dec v Vundef then a else b) = b.

Lemma ext_trace_from_empty_buffer': forall t mb af tr mb',
  ext_trace t af mb tr mb' ->
  snd mb = empty_buffer -> snd mb' = empty_buffer.

Lemma ext_trace_from_empty_buffer: forall t m af tr m' b',
  ext_trace t af (m,empty_buffer) tr (m',b') -> b' = empty_buffer.

Hint Constructors ext_trace.

Lemma refines_cas_fail_stronger : forall r ptr new old dst,
  refines
  (Sseq
    (Satomicmem r Op.AScas (ptr::new::old::nil) dst)
    (Sassume (Op.Ccomp Cne) (dst::old::nil)))
  (Satomic true
    (Sseq
      (if r then
        (Sseq (Sload Global (Op.Aindexed Int.zero) (ptr::nil) dst) Srelease)
       else
          (Sload Global (Op.Aindexed Int.zero) (ptr::nil) dst))
      (Sassume (Op.Ccomp Cne) (dst::old::nil)))).


Lemma refines_cas_success : forall r ptr new old dst,
  negb (Peqb dst old) ->
  negb (Peqb dst new) ->
  negb (Peqb ptr dst) ->
  refines
  (Sseq
    (Satomicmem r Op.AScas (ptr::new::old::nil) dst)
    (Sassume (Op.Ccomp Ceq) (dst::old::nil)))
  (Satomic true
    (Sseq
      (Sload Global (Op.Aindexed Int.zero) (ptr::nil) dst)
      (Sseq
        (Sassume (Op.Ccomp Ceq) (dst::old::nil))
        (Sstore r Global (Op.Aindexed Int.zero) (ptr::nil) new)))).


Lemma refines_seq_left : forall stmt1 stmt2 stmt1',
  refines stmt1 stmt1' ->
  refines (Sseq stmt1 stmt2) (Sseq stmt1' stmt2).

Lemma refines_seq_right : forall stmt1 stmt2 stmt2',
  refines stmt2 stmt2' ->
  refines (Sseq stmt1 stmt2) (Sseq stmt1 stmt2').

Lemma refines_if_with_branch : forall cond args ifso ifnot,
  refines (Sifthenelse cond args ifso ifnot)
          (Sbranch
            (Sseq (Sassume cond args) ifso)
            (Sseq (Sassume (negate_condition cond) args) ifnot)).

Lemma refines_seq_branch : forall stmt1 stmt2 stmt3,
  refines
    (Sseq stmt1 (Sbranch stmt2 stmt3))
    (Sbranch (Sseq stmt1 stmt2) (Sseq stmt1 stmt3)).

Lemma refines_branch_seq : forall stmt1 stmt2 stmt3,
  refines
    (Sseq (Sbranch stmt1 stmt2) stmt3)
    (Sbranch (Sseq stmt1 stmt3) (Sseq stmt2 stmt3)).

Lemma refines_branch : forall stmt1 stmt2 stmt1' stmt2',
  refines stmt1 stmt1' -> refines stmt2 stmt2' ->
  refines (Sbranch stmt1 stmt2) (Sbranch stmt1' stmt2').

Lemma seq_seq : forall ge sp tid st s1 s3 s4 af tr st',
  bigstep ge sp tid st (Sseq s1 (Sseq s3 s4)) af tr st' ->
  bigstep ge sp tid st (Sseq (Sseq s1 s3) s4) af tr st'.

Lemma seq_seq_1 : forall ge sp tid st s1 s3 s4 af tr st',
  bigstep ge sp tid st (Sseq (Sseq s1 s3) s4) af tr st' ->
  bigstep ge sp tid st (Sseq s1 (Sseq s3 s4)) af tr st'.

Lemma unroll_once : forall ge sp tid st s af tr st',
  bigstep ge sp tid st (Sseq s (Sloop s)) af tr st' ->
  bigstep ge sp tid st (Sloop s) af tr st'.

Lemma unroll_once_1 : forall ge sp tid st s' s af tr st',
  bigstep ge sp tid st (Sseq (Sseq s (Sloop s)) s') af tr st' ->
  bigstep ge sp tid st (Sseq (Sloop s) s') af tr st'.

Lemma neg_neg_cond : forall cond,
  negate_condition (negate_condition cond) = cond.

Lemma refines_repeat : forall body cond args,
  refines (Srepeat body cond args)
          (Sseq
            (Sloop (Sseq body (Sassume (negate_condition cond) args)))
            (Sseq body (Sassume cond args))).

Lemma refines_branch_left : forall stmt1 stmt2 stmt1',
  refines stmt1 stmt1' ->
  refines (Sbranch stmt1 stmt2) (Sbranch stmt1' stmt2).

Lemma refines_branch_right : forall stmt1 stmt2 stmt2',
  refines stmt2 stmt2' ->
  refines (Sbranch stmt1 stmt2) (Sbranch stmt1 stmt2').

Lemma refines_branch_assoc : forall stmt1 stmt2 stmt3,
  refines (Sbranch (Sbranch stmt1 stmt2) stmt3) (Sbranch stmt1 (Sbranch stmt2 stmt3)).

Lemma refines_skip_stmt : forall stmt,
  refines (Sseq Sskip stmt) stmt.

Lemma refines_stmt_skipstmt : forall stmt,
  refines stmt (Sseq Sskip stmt).

Lemma refines_stmt_skip : forall stmt,
  refines (Sseq stmt Sskip) stmt.

Lemma refines_atomic_abort : forall r e,
  refines
    (Sseq (Sfence true) (Sabort Interleaved r e))
    (Satomic true (Sseq Srelease (Sabort Atomic r e))).