Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslmodel fslassnlemmas.
Require Import fslhmap stepback.

Set Implicit Arguments.

Lemma alloc_always_before PS PSg:
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    hf g (MAP: hmap edge = Hdef hf g) l (ALL: hf l ≠ @HVnone PS PSg)
    lbl (LAB: HVlabeled (hf l) lbl),
  ∃ a, << ALLOC: lab a = Aalloc l >> ∧
    ((<< LBL: lbl = HLnormal >> ∧ << HB: clos_refl_trans _ (happens_before lab sb rf mo) a (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLtriangle >> ∧ ∃ b, << REL: is_release_fence (lab b) >> ∧
                                               << HB: happens_before lab sb rf mo a b >> ∧
                                               << SB: clos_refl_trans _ sb b (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << SB: ¬ is_rf edge >>
                                  ∧ ∃ b b' c, << REL: is_release_write (lab b) >> ∧
                                                    << HB: happens_before lab sb rf mo a b >> ∧
                                                    << RSQ: release_seq lab sb rf mo b b' >> ∧
                                                    << RF: rf c = Some b' >> ∧
                                                    << SB: clos_refl_trans _ sb c (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << SB: ¬ is_rf edge >>
                                  ∧ ∃ b c c' d, << REL: is_release_fence (lab b) >> ∧
                                                      << HB: happens_before lab sb rf mo a b >> ∧
                                                      << SB1: clos_trans _ sb b c >> ∧
                                                      << RSQ: release_seq lab sb rf mo c c' >> ∧
                                                      << RF: rf d = Some c' >> ∧
                                                      << SB2: clos_refl_trans _ sb d (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << RF: ¬ is_sb edge >>
                                  ∧ ∃ b, << REL: is_release_write (lab b) >> ∧
                                               << HB: happens_before lab sb rf mo a b >> ∧
                                               << RSQ: release_seq lab sb rf mo b (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << RF: ¬ is_sb edge >> ∧
                                     ∃ b c, << REL: is_release_fence (lab b) >> ∧
                                                 << HB: happens_before lab sb rf mo a b >> ∧
                                                 << SB: clos_trans _ sb b c >> ∧
                                                 << RSQ: release_seq lab sb rf mo c (hb_fst edge) >>)).

Theorem valid_implies_mem_safe PS PSg :
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: @hmap_valids PS PSg lab sb rf hmap V),
  mem_safe V lab sb rf mo.