Module AllRefinesRules

Require Import
  Utf8 Coqlib Op Integers Maps
  Utils INJECT RTLinject
  Common Errors Traces RTLinjectlow Asm MIRcompiler
  RefinesDefs AllRefinesRulesAux.


Module Type REFINE.

  Parameter refines : statement → statement → Prop.

  Parameter 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.

  Parameter rtlinject_compiler_correctness :
    forall sort fe1 fi2 fe2 bi p p' (HBI: ok_bi bi),
      transf_rtlinject_program sort fe1 fi2 fe2 bi p = OK p' →
      forall trace,
        safe_program p →
        tfin trace →
        prog_traces x86_sem p' nil trace →
        low_traces p trace.

  Parameter refines_refl: forall stmt,
    refines stmt stmt.
  Parameter refines_trans : forall stmt1 stmt2 stmt3,
    refines stmt1 stmt2 → refines stmt2 stmt3 → refines stmt1 stmt3.


  Parameter refines_seq : forall stmt1 stmt2 stmt1' stmt2',
    refines stmt1 stmt1' → refines stmt2 stmt2' →
    refines (Sseq stmt1 stmt2) (Sseq stmt1' stmt2').
  Parameter refines_seq_assoc1 : forall stmt1 stmt2 stmt3,
    refines (Sseq stmt1 (Sseq stmt2 stmt3))
            (Sseq (Sseq stmt1 stmt2) stmt3).
  Parameter refines_seq_assoc2 : forall stmt1 stmt2 stmt3,
    refines (Sseq (Sseq stmt1 stmt2) stmt3)
            (Sseq stmt1 (Sseq stmt2 stmt3)).

  Parameter refines_stmt_skip : forall stmt,
    refines (Sseq stmt Sskip) stmt.
  Parameter refines_skip_stmt : forall stmt,
    refines (Sseq Sskip stmt) stmt.

  Parameter while_repeat_congruence : forall body1 body2 cond args,
    refines body1 body2 →
    refines (Swhile cond args body1) (Swhile cond args body2).
  Parameter refines_repeat_congruence : forall body1 body2 cond args,
    refines body1 body2 →
    refines (Srepeat body1 cond args) (Srepeat body2 cond args) .
  Parameter refines_loop : forall stmt stmt',
    refines stmt stmt' →
    refines (Sloop stmt) (Sloop stmt').
  Parameter refines_while : forall body cond args,
    refines (Swhile cond args body)
            (Sseq
              (Sloop (Sseq (Sassume cond args) body))
              (Sassume (negate_condition cond) args)).
  Parameter refines_while_inv : forall body cond args,
    refines (Sseq
              (Sloop (Sseq (Sassume cond args) body))
              (Sassume (negate_condition cond) args))
            (Swhile cond args body).
  Parameter 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))).

  Parameter 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').
  Parameter refines_if1 : forall cond args stmt1 stmt1' stmt2,
    refines stmt1 stmt1' →
    refines (Sifthenelse cond args stmt1 stmt2) (Sifthenelse cond args stmt1' stmt2).
  Parameter refines_if2 : forall cond args stmt1 stmt2 stmt2',
    refines stmt2 stmt2' →
    refines (Sifthenelse cond args stmt1 stmt2) (Sifthenelse cond args stmt1 stmt2').
  Parameter refines_branch_same_begin: forall stmt1 stmt2 stmt3,
    refines
       (Sbranch (Sseq stmt1 stmt2) (Sseq stmt1 stmt3))
       (Sseq stmt1 (Sbranch stmt2 stmt3)).
  Parameter refines_branch_assoc2 : forall stmt1 stmt2 stmt3,
    refines (Sbranch stmt1 (Sbranch stmt2 stmt3)) (Sbranch (Sbranch stmt1 stmt2) stmt3).
  Parameter 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)).


  Parameter 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)))).
  Parameter 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)))).
  Parameter refines_seq_branch : forall stmt1 stmt2 stmt3,
    refines
      (Sseq stmt1 (Sbranch stmt2 stmt3))
      (Sbranch (Sseq stmt1 stmt2) (Sseq stmt1 stmt3)).
  Parameter refines_branch_seq : forall stmt1 stmt2 stmt3,
    refines
      (Sseq (Sbranch stmt1 stmt2) stmt3)
      (Sbranch (Sseq stmt1 stmt3) (Sseq stmt2 stmt3)).
  Parameter refines_branch : forall stmt1 stmt2 stmt1' stmt2',
    refines stmt1 stmt1' → refines stmt2 stmt2' →
    refines (Sbranch stmt1 stmt2) (Sbranch stmt1' stmt2').
  Parameter refines_branch_left : forall stmt1 stmt2 stmt1',
    refines stmt1 stmt1' →
    refines (Sbranch stmt1 stmt2) (Sbranch stmt1' stmt2).
  Parameter refines_branch_right : forall stmt1 stmt2 stmt2',
    refines stmt2 stmt2' →
    refines (Sbranch stmt1 stmt2) (Sbranch stmt1 stmt2').
  Parameter refines_branch_assoc : forall stmt1 stmt2 stmt3,
    refines (Sbranch (Sbranch stmt1 stmt2) stmt3) (Sbranch stmt1 (Sbranch stmt2 stmt3)).
  Parameter refines_branch_dup: forall stmt1 stmt2,
    refines
      (Sbranch stmt1 (Sbranch stmt1 stmt2))
      (Sbranch stmt1 stmt2).

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

  Parameter refines_atomic : forall b stmt stmt',
    refines stmt stmt' →
    no_atomic_in_statement stmt' →
    refines (Satomic b stmt) (Satomic b stmt').
  Parameter refines_atomic' : forall b stmt stmt',
    refines_in_atomic stmt stmt' →
    no_atomic_in_statement stmt' →
    refines (Satomic b stmt) (Satomic b stmt').

  Parameter 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).

  Parameter 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) →
    refines (Sseq stmt1 stmt2) stmt2.
  Parameter 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) →
    refines (Sseq stmt1 (Sreturn args)) (Sreturn args).

  Parameter 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)).

  Parameter refines_stmt_abort: forall stmt af e r,
    local_before_abort stmt →
    refines (Sseq stmt (Sabort af r e)) (Sabort af r e).
  Parameter refines_abort_stmt: forall stmt af r e,
    refines (Sseq (Sabort af r e) stmt) (Sabort af r e).
  Parameter 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)).

  Parameter refines_left_mover : forall stmt1 f stmt2,
    left_mover stmt1 →
    no_atomic_in_statement stmt1 →
    no_atomic_in_statement stmt2 →
    refines
      (Sseq stmt1 (Satomic f stmt2))
      (Satomic f (Sseq stmt1 stmt2)).
  Parameter refines_left_mover_strong : forall stmt1 f stmt2,
    left_mover_strong stmt1 →
    no_atomic_in_statement stmt1 →
    no_atomic_in_statement stmt2 →
    refines
      (Sseq stmt1 (Satomic f stmt2))
      (Satomic f (Sseq (left_move_conv stmt1) stmt2)).
  Parameter 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)).
  Parameter 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)).
  Parameter 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)).
  Parameter refines_elim_fence: refines (Sfence false) Sskip.

  Parameter refines_request: forall addr args ap stmt f,
    refines
      (Sseq
        (Srequestperm ap addr args)
        (Satomic f stmt))
      (Satomic f
        (Sseq (Srequestperm ap addr args) stmt)).
  Parameter refines_promotes_fence: forall f r,
    refines (Sfence r) (Satomic f (if r then Srelease else Sskip)).
  Parameter refines_store_fence: forall f r af addr args dst,
    refines
      (Sseq (Sstore false af addr args dst) (Sfence r))
      (Satomic f (Sstore r af addr args dst)).
  Parameter refines_remove_freeperm_right: forall stmt,
    refines (Sseq stmt Sfreeperm) stmt.
  Parameter refines_remove_perm: forall stmt,
    release_point stmt →
    refines (Sseq Sfreeperm stmt) (Sseq (remove_perm stmt) Sfreeperm).

End REFINE.

Require RefinesDefs RefinesRules RefinesRules2 RefinesRules3 SimulationByRefines.

Module Refines : REFINE.

  Definition refines := RefinesDefs.refines.

  Definition refines_refl := RefinesRules.refines_refl.
  Definition refines_trans := RefinesRules.refines_trans.

  Definition refines_seq := RefinesRules.refines_seq.
  Definition refines_seq_assoc1 := RefinesRules.refines_seq_assoc1.
  Definition refines_seq_assoc2 := RefinesRules.refines_seq_assoc2.

  Definition refines_stmt_skip := RefinesRules.refines_stmt_skip.
  Definition refines_skip_stmt := RefinesRules.refines_skip_stmt.

  Definition while_repeat_congruence := RefinesRules.while_repeat_congruence.
  Definition refines_repeat_congruence := RefinesRules.refines_repeat_congruence.

  Definition refines_loop := RefinesRules.refines_loop.
  Definition refines_while := RefinesRules.refines_while.
  Definition refines_while_inv := RefinesRules.refines_while_inv.
  Definition refines_repeat := RefinesRules.refines_repeat.

  Definition refines_if := RefinesRules.refines_if.
  Definition refines_if1 := RefinesRules.refines_if1.
  Definition refines_if2 := RefinesRules.refines_if2.
  Definition refines_branch_same_begin := RefinesRules.refines_branch_same_begin.
  Definition refines_branch_assoc2 := RefinesRules.refines_branch_assoc2.
  Definition refines_if_with_branch := RefinesRules.refines_if_with_branch.
  Definition refines_seq_branch := RefinesRules.refines_seq_branch.
  Definition refines_branch_seq := RefinesRules.refines_branch_seq.
  Definition refines_branch := RefinesRules.refines_branch.
  Definition refines_branch_left := RefinesRules.refines_branch_left.
  Definition refines_branch_right := RefinesRules.refines_branch_right.
  Definition refines_branch_assoc := RefinesRules.refines_branch_assoc.
  Definition refines_branch_dup := RefinesRules2.refines_branch_dup.

  Definition refines_remove_leak_left := RefinesRules.refines_remove_leak_left.
  Definition refines_remove_leak_right := RefinesRules.refines_remove_leak_right.

  Definition refines_atomic := RefinesRules.refines_atomic.
  Definition refines_atomic' := RefinesRules.refines_atomic'.
  Definition refines_swap_assert := RefinesRules.refines_swap_assert.
  Definition refines_dead_code := RefinesRules.refines_dead_code.
  Definition refines_dead_code_return := RefinesRules.refines_dead_code_return.

  Definition refines_localstore := RefinesRules2.refines_localstore.
  Definition refines_stmt_abort := RefinesRules2.refines_stmt_abort.
  Definition refines_abort_stmt := RefinesRules2.refines_abort_stmt.
  Definition refines_loop_branch_abort := RefinesRules2.refines_loop_branch_abort.

  Definition refines_left_mover := RefinesRules2.refines_left_mover.
  Definition refines_left_mover_strong := RefinesRules2.refines_left_mover_strong.
  Definition refines_right_mover := RefinesRules2.refines_right_mover.
  Definition refines_if_atomic := RefinesRules2.refines_if_atomic.
  Definition refines_fence_load := RefinesRules2.refines_fence_load.
  Definition refines_request := RefinesRules3.refines_request.
  Definition refines_promotes_fence := RefinesRules3.refines_promotes_fence.
  Definition refines_store_fence := RefinesRules3.refines_store_fence.
  Definition refines_remove_perm := RefinesRules3.refines_remove_perm.
  Definition refines_remove_freeperm_right := RefinesRules3.refines_remove_freeperm_right.
  Definition refines_elim_fence := RefinesRules3.refines_elim_fence.

  Definition refines_cas_fail_stronger := RefinesRules.refines_cas_fail_stronger.
  Definition refines_cas_success := RefinesRules.refines_cas_success.

  Definition refines_implies_backwardsim := SimulationByRefines.refines_implies_backwardsim.

  Definition rtlinject_compiler_correctness := MIRcompiler.rtlinject_compiler_correctness.

End Refines.