Require Import Vbase Varith.
Require Import Relations Wellfounded Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas fslhmap.
Require Import ihc initread.

Set Implicit Arguments.

Lemma go_back_one_acq :
  ∀ acts lab sb mo rf
    (FIN : ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A : ConsistentAlloc lab) hmap V
    (HC : hist_closed sb rf V) e
    (VALID : hmap_valid lab sb rf hmap e)
    (INe : In e V) hFR l
    (NALLOC : lab e ≠ Aalloc l)
    (ALLOC : ∀ hf loc,
               hFR = Hdef hf → hf loc ≠ HVnone →
               ∃ c : actid, lab c = Aalloc loc ∧ c ≠ e),
   ∃ pres_sb pres_rf posts_sb posts_rf,
     NoDup pres_sb ∧
     NoDup pres_rf ∧
     NoDup posts_sb ∧
     NoDup posts_rf ∧
     (∀ x : actid, In x pres_sb ↔ sb x e) ∧
     (∀ x : actid, In x pres_rf ↔ rf e = Some x) ∧
     (∀ x : actid, In x posts_sb ↔ sb e x) ∧
     (∀ x : actid, In x posts_rf ↔ rf x = Some e) ∧
     (∀ h
       (EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
            hsum (map hmap (map (hb_rf^~ e) pres_rf)) +!+ hFR =
            Hdef h),
      let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
      ∃ h0 : val → HeapVal,
        hsum (map hmap (map (hb_sb e) posts_sb)) +!+
        hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR =
        Hdef h0 ∧
           ∀ PP´ QQ´ isrmw´ perm´ init´ (LA: h0 l = HVra PP´ QQ´ isrmw´ perm´ init´),
             hvplus_ra_ret (h l) QQ´).
Lemma go_back_one_rel :
  ∀ lab sb rf mo hmap edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET: hmap edge = Hdef hf) l PP QQ isrmw perm init v
    (LA : hf l = HVra PP QQ isrmw perm init)
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge´ hf´,
    edge_valid lab sb rf edge´ ∧
    hb_snd edge´ = Some (hb_fst edge) ∧
    hmap edge´ = Hdef hf´ ∧
    ∃ PP´ QQ´ isrmw´ perm´ init´,
      hf´ l = HVra PP´ QQ´ isrmw´ perm´ init´ ∧ implies (sval (PP v)) (sval (PP´ v)).
Lemma heap_loc_rel_allocated :
  ∀ lab sb rf mo hmap V 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 (GET: hmap edge = Hdef h) l PP QQ isrmw perm init
    (LA: h l = HVra PP QQ isrmw perm init),
  ∃ cpre c hf PP´ QQ´ isrmw´ perm´ init´,
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    hf l = HVra PP´ QQ´ isrmw´ perm´ init´ ∧
    (cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
    implies (sval (PP v)) (sval (PP´ v)).

Lemma heap_loc_rel_allocated_strong :
  ∀ lab sb rf mo hmap V 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 (GET: hmap edge = Hdef h) l PP QQ isrmw perm init
    (LA: h l = HVra PP QQ isrmw perm init),
  ∃ cpre c hf PP´ QQ´ isrmw´,
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    hf l = HVra PP´ QQ´ isrmw´ (Some HLCnormal) None ∧
    (cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
    implies (sval (PP v)) (sval (PP´ v)).

Lemma go_back_one_rmwacq :
  ∀ lab sb rf mo hmap edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET: hmap edge = Hdef hf) l PP QQ perm init
    (LA : hf l = HVra PP QQ true perm init)
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge´ hf´,
    edge_valid lab sb rf edge´ ∧
    hb_snd edge´ = Some (hb_fst edge) ∧
    hmap edge´ = Hdef hf´ ∧
    ∃ PP´ QQ´ perm´ init´, hf´ l = HVra PP´ QQ´ true perm´ init´.
Lemma heap_loc_rmwacq_allocated :
  ∀ 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 (GET: hmap edge = Hdef h) l PP QQ perm init
    (LA: h l = HVra PP QQ true perm init),
  ∃ cpre c hf PP´ QQ´ perm´ init´,
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    hf l = HVra PP´ QQ´ true perm´ init´.

Lemma go_back_one_acq3 :
  ∀ lab sb rf mo hmap edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET: hmap edge = Hdef hf) l PP QQ perm init
    (LA : hf l = HVra PP QQ false perm init) v
    (NE : sval (QQ v) ≠ Aemp)
    (NE : sval (QQ v) ≠ Afalse)
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge´ hf´,
    edge_valid lab sb rf edge´ ∧
    hb_snd edge´ = Some (hb_fst edge) ∧
    hmap edge´ = Hdef hf´ ∧
    ∃ PP´ QQ´ perm´ init´,
      hf´ l = HVra PP´ QQ´ false perm´ init´ ∧ sval (QQ´ v) ≠ Aemp ∧ sval (QQ´ v) ≠ Afalse.
Lemma heap_loc_ra_own_allocated :
  ∀ lab sb rf mo hmap V 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 (GET: hmap edge = Hdef h) l PP QQ perm init
    (LA: h l = HVra PP QQ false perm init)
    (ALL: sval (QQ v) ≠ Aemp)
    (NF: sval (QQ v) ≠ Afalse),
  ∃ cpre c hf PP´ QQ´ perm´ init´,
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    (cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
    hf l = HVra PP´ QQ´ false perm´ init´.

Lemma heap_loc_ra_no_own :
  ∀ lab sb rf mo hmap V 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)
    edge´ (EV: edge_valid lab sb rf edge´) (IN´: In (hb_fst edge´) V)
    h (GET: hmap edge = Hdef h) l PP QQ perm init (LA: h l = HVra PP QQ true perm init)
    h´ (GET: hmap edge´ = Hdef h´) PP´ QQ´ perm´ init´ (LA´: h´ l = HVra PP´ QQ´ false perm´ init´),
    sval (QQ´ v) = Aemp ∨ sval (QQ´ v) = Afalse.

Lemma wellformed :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (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)
    wpre w (INw: In w V)
    l v (LAB: is_writeLV (lab w) l v)
    (SBw: sb wpre w) hw
    rfw (rfwOK: ∀ x, In x rfw ↔ rf w = Some x) (rfwND: NoDup rfw)
    (MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_rf^~ w) rfw)) = Hdef hw)
    PW QW isrmwW permW initW
    (HW: hw l = HVra PW QW isrmwW permW initW)
    T (NDt: NoDup T)
      (ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
      (TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
    (INDEP: independent sb rf T)
    hT (MAPt: hsum (map hmap T) = Hdef hT)
    PT QT isrmwT permT initT (HT: hT l = HVra PT QT isrmwT permT initT),
  implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).
Lemma wellformed_w :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (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)
    wpre w (INw: In w V)
    typ l v (LAB: lab w = Astore typ l v)
    (SBw: sb wpre w) hw (MAPw: hmap (hb_sb wpre w) = Hdef hw)
    PW QW isrmwW permW initW
    (HW: hw l = HVra PW QW isrmwW permW initW)
    T (NDt: NoDup T)
      (ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
      (TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
    (INDEP: independent sb rf T)
    hT (MAPt: hsum (map hmap T) = Hdef hT)
    PT QT isrmwT permT initT (HT: hT l = HVra PT QT isrmwT permT initT),
  implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).

Lemma wellformed_one :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (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)
    wpre w (INw: In w V)
    l v (LAB: is_writeLV (lab w) l v)
    (SBw: sb wpre w) hw
    rfw (rfwOK: ∀ x, In x rfw ↔ rf w = Some x) (rfwND: NoDup rfw)
    (MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_rf^~ w) rfw)) = Hdef hw)
    PW QW isrmwW permW initW
    (HW: hw l = HVra PW QW isrmwW permW initW)
    rpre r (ST: In rpre V) (TT: sb rpre r)
    (NIN: ¬ In r V)
    hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
    PT QT isrmwT permT initT (HT: hT l = HVra PT QT isrmwT permT initT),
  implies (sval (PW v)) (Astar (sval (QT v)) Atrue).

Lemma wellformed_one_w :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (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)
    wpre w (INw: In w V)
    typ l v (LAB: lab w = Astore typ l v)
    (SBw: sb wpre w) hw
    (MAPw: hmap (hb_sb wpre w) = Hdef hw)
    PW QW isrmwW permW initW
    (HW: hw l = HVra PW QW isrmwW permW initW)
    rpre r (ST: In rpre V) (TT: sb rpre r)
    (NIN: ¬ In r V)
    hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
    PT QT isrmwT permT initT (HT: hT l = HVra PT QT isrmwT permT initT),
  implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).