Require Import Vbase.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 rslassn rslassnlemmas rslmodel rslhmap.

Set Implicit Arguments.

Lemma go_back_one_val :
  ∀ lab sb rf hmap edge
    (VALID : hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET : hmap edge = Hdef hf) l v
    (LA : hf l = HVval v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = hb_fst edge ∧
    ¬ is_writeL (lab (hb_fst edge)) l ∧
    ∃ hf', hmap edge' = Hdef hf' ∧
                hf' l = HVval v.

Lemma heap_loc_na_initialized2 :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l v (LA: h l = HVval v),
  ∃ cpre c hf,
    sb cpre c ∧
    is_writeLV (lab c) l v ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    is_val (hf l) ∧
    (c = hb_fst edge ∨ happens_before lab sb rf mo c (hb_fst edge)) ∧
    (∀ d
      (HB1: d = hb_fst edge ∨ happens_before lab sb rf mo d (hb_fst edge))
      (HB2: happens_before lab sb rf mo c d),
      ¬ is_writeL (lab d) l).
Lemma hc_edge_hb mt lab sb rf mo a b :
  happens_before lab sb rf mo a b →
  clos_trans _ (hc_edge mt lab sb rf mo) a b.

Lemma heap_loc_na_initialized :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (IRR: IrreflexiveHB lab sb rf mo)
    (ACYCLIC: acyclic (hc_edge mt lab sb rf mo))
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l v (LA: h l = HVval v),
  ∃ cpre c hf,
    sb cpre c ∧
    is_writeLV (lab c) l v ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    is_val (hf l) ∧
    (c = hb_fst edge ∨ happens_before lab sb rf mo c (hb_fst edge)) ∧
    
    (∀ d
      (HB1: clos_refl_trans _ (hc_edge mt lab sb rf mo) d (hb_fst edge))
      (HB2: clos_trans _ (hc_edge mt lab sb rf mo) c d),
      ¬ is_writeL (lab d) l).
Lemma is_write_weaken typ l v : is_writeLV typ l v → is_writeL typ l.

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

Hint Resolve is_write_weaken is_access_weaken.

Lemma two_access_cases :
  ∀ mt pre a b acts lab sb rf mo hmap V hf
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo 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 hf) (IV: is_val (hf (loc (lab a))))
    (B : is_access (lab b)) (LOC : loc (lab a) = loc (lab b)),
  a = b ∨ happens_before lab sb rf mo a b ∨ happens_before lab sb rf mo b a.

Lemma hb_prev :
  ∀ lab sb rf mo a p n,
    happens_before lab sb rf mo a n →
    (∀ x, sb x n → x = p) →
    (∀ x, synchronizes_with lab sb rf mo x n → x = p) →
    a = p ∨ happens_before lab sb rf mo a p.

Lemma go_back_one_na :
  ∀ lab sb rf hmap edge
    (VALID : hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET : hmap edge = Hdef hf) l
    (LA : is_val (hf l))
    (NW: lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = hb_fst edge ∧
    ∃ hf', hmap edge' = Hdef hf' ∧
                is_val (hf' l).

Lemma heap_loc_na_allocated :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l (LA: is_val (h l)),
  ∃ cpre c hf,
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    hf l = HVuval ∧
    (cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)).