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

Set Implicit Arguments.

Lemma go_back_one_acq PS PSg :
  ∀ acts lab sb mo rf
    (FIN : ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A : ConsistentAlloc lab) hmap ga V
    (HC : hist_closed sb rf V) e
    (VALID : hmap_valid lab sb rf hmap ga e)
    (INe : In e V) hFR l
    (NALLOC : lab e ≠ Aalloc l)
    (ALLOC : ∀ hf g loc,
               hFR = Hdef hf g → hf loc ≠ @HVnone PS PSg →
               ∃ c : actid, lab c = Aalloc loc ∧ c ≠ e)
    (GHOSTS: ∀ hf g loc,
               hFR = Hdef hf g → g loc ≠ None →
               ga loc ≠ Some 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 g
       (EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
            hsum (map hmap (map (hb_rf^~ e) pres_rf)) +!+ hFR =
            Hdef h g),
      let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
      ∃ h0 g0,
        hsum (map hmap (map (hb_sb e) posts_sb)) +!+
        hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR = Hdef h0 g0 ∧
        ∀ 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 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 PP QQ isrmw perm init v
    (LA : hf l = @HVra PS PSg PP QQ isrmw perm init)
    (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 hf' g' ∧
    ∃ 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 PS PSg :
  ∀ 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 g (GET: hmap edge = Hdef h g) l PP QQ isrmw perm init
    (LA: h l = @HVra PS PSg PP QQ isrmw perm init),
  ∃ cpre c hf g' PP' QQ' isrmw' perm' init',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf g' ∧
    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 PS PSg :
  ∀ 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 g (GET: hmap edge = Hdef h g) l PP QQ isrmw perm init
    (LA: h l = @HVra PS PSg PP QQ isrmw perm init),
  ∃ cpre c hf g' PP' QQ' isrmw',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf g' ∧
    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 heap_loc_allocated_atomic 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 PS PSg h g) l
    (LA: is_atomic (h l)),
  ∃ cpre c hf g',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf g' ∧
    is_atomic (hf l) ∧
    (cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)).

Lemma go_back_one_rmwacq 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 PP QQ perm init
    (LA : hf l = HVra PP QQ true perm init)
    (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 hf' g' ∧
    ∃ PP' QQ' perm' init', hf' l = @HVra PS PSg PP' QQ' true perm' init'.

Lemma heap_loc_rmwacq_allocated 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 PP QQ perm init
    (LA: h l = @HVra PS PSg PP QQ true perm init),
  ∃ cpre c hf g' PP' QQ' perm' init',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf g' ∧
    hf l = HVra PP' QQ' true perm' init'.

Lemma go_back_one_acq3 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 PP QQ perm init
    (LA : hf l = @HVra PS PSg 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' g',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = Some (hb_fst edge) ∧
    hmap edge' = Hdef hf' g' ∧
    ∃ 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 PS PSg :
  ∀ 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 g (GET: hmap edge = Hdef h g) 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 g' PP' QQ' perm' init',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf g' ∧
    (cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)) ∧
    hf l = @HVra PS PSg PP' QQ' false perm' init'.

Lemma heap_loc_ra_no_own PS PSg :
  ∀ 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 g (GET: hmap edge = Hdef h g) l PP QQ perm init (LA: h l = @HVra PS PSg PP QQ true perm init)
    h' g' (GET: hmap edge' = Hdef h' g') PP' QQ' perm' init' (LA': h' l = HVra PP' QQ' false perm' init'),
    sval (QQ' v) = Aemp ∨ sval (QQ' v) = Afalse.

Lemma wellformed PS PSg :
  ∀ 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 gw
    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 gw)
    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 gT (MAPt: hsum (map hmap T) = Hdef hT gT)
    PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
  implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).

Lemma wellformed_w PS PSg :
  ∀ 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 gw (MAPw: hmap (hb_sb wpre w) = Hdef hw gw)
    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 gT (MAPt: hsum (map hmap T) = Hdef hT gT)
    PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
  implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).

Lemma wellformed_one PS PSg :
  ∀ 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 gw
    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 gw)
    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 gT (MAPt: hmap (hb_sb rpre r) = Hdef hT gT)
    PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
  implies (sval (PW v)) (Astar (sval (QT v)) Atrue).

Lemma wellformed_one_w PS PSg :
  ∀ 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 gw
    (MAPw: hmap (hb_sb wpre w) = Hdef hw gw)
    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 gT (MAPt: hmap (hb_sb rpre r) = Hdef hT gT)
    PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
  implies (proj1_sig (PW v)) (Astar (proj1_sig (QT v)) Atrue).