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

Set Implicit Arguments.

Lemma go_back_one_val PS PSg :
  ∀ lab sb rf mo hmap ga edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VALID : hmap_valid lab sb rf hmap ga (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf g
    (GET : hmap edge = Hdef hf g) l v
    (LA : has_value (hf l) v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = Some (hb_fst edge) ∧
    ¬ is_writeL (lab (hb_fst edge)) l ∧
    ∃ hf' g', hmap edge' = @Hdef PS PSg hf' g' ∧ has_value (hf' l) v.

Lemma is_write_weaken typ l v : is_writeLV typ l v → is_writeL typ l.

Lemma is_write_weaken2 typ l : is_writeL typ l → is_write typ.

Lemma is_access_weaken typ l v : is_writeLV typ l v → is_access typ.

Hint Resolve is_write_weaken is_write_weaken2 is_access_weaken.

Lemma heap_loc_na_initialized2 PS PSg :
  ∀ acts lab sb rf mo hmap V
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (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)
    h g (GET: hmap edge = Hdef h g) l v (LA: has_value (h l) v),
  ∃ cpre c hf g',
    sb cpre c ∧
    is_writeLV (lab c) l v ∧
    hmap (hb_sb cpre c) = @Hdef PS PSg hf g' ∧
    is_lvalue (hf l) ∧
    (c = hb_fst edge ∨ happens_before_union_rf sb rf c (hb_fst edge)) ∧
    (∀ d
      (HB1: d = hb_fst edge ∨ happens_before_union_rf sb rf d (hb_fst edge))
      (HB2: happens_before_union_rf sb rf c d),
      ¬ is_writeL (lab d) l).

Lemma two_access_cases PS PSg :
  ∀ pre a b acts lab sb rf mo hmap V hf g
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    (INa : In a V)
    (INb : In b V)
    (SB : sb pre a) (HD: hmap (hb_sb pre a) = @Hdef PS PSg hf g) (IV: is_lvalue (hf (loc (lab a))))
    (B : is_access (lab b)) (LOC : loc (lab a) = loc (lab b)),
  a = b ∨ happens_before_union_rf sb rf a b ∨ happens_before_union_rf sb rf b a.

Lemma go_back_one_na PS PSg :
  ∀ lab sb rf mo hmap ga edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap ga (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf g
    (GET: hmap edge = Hdef hf g) l
    (LA : is_nonatomic (hf l))
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge' hf' g',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = Some (hb_fst edge) ∧
    hmap edge' = @Hdef PS PSg hf' g' ∧
    is_nonatomic (hf' l).

Lemma heap_loc_allocated_nonatomic PS PSg :
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (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)
    h g (GET: hmap edge = Hdef h g) l
    (LA: is_nonatomic (h l)),
  ∃ cpre c hf g',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = @Hdef PS PSg hf g' ∧
    is_nonatomic (hf l) ∧
    (cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)).