Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import Omega List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper GpsWPE.

Local Open Scope string_scope.

Set Implicit Arguments.

Lemma conform_suff_immediate :
  ∀ b acts amap sb rf mo sc
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI: pres_in sb rf b acts) L IE EE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L EE a)
    (CO: conform (b::acts) amap mo L acts) r'
    (CC: compat amap sb rf (upd L (TsbS b) (L (TsbS b) ⊕ r')))
    (NIN: ¬ In b acts) loc
    (Orf: rsum (map L (map (Trf b) (b::acts))) = res_emp)
    (LR : label_restr (b :: acts) amap sb rf L EE)
    (ND': NoDup EE)
    (LOC: is_atomic_writeL (amap b) loc)
    (HPL: res_get (incoming (b :: acts) L b) loc ≠ p_bot)
    (G : res_get r' loc ≠ p_bot) vb rsb r
    (MAG : atomic_guar IE r' loc vb rsb r)
    (PREV: ∀ a (IMM: immediate mo a b) (IN: In a acts)
      (AW: is_atomic_writeL (amap a) loc),
      prot_trans_ok (res_get (out_rf (b::acts) L a) loc) (res_get r loc))
    (GIMP: ∀ τ S
      (G1: res_get r loc = p_at τ S) S'
      (G2: res_get (L (TsbS b)) loc = p_at τ S'),
      slist_lt S' S),
  conform (b::acts) amap mo (upd L (TrfS b) r) (b::acts).

Lemma vghost_get_back_at2 :
  ∀ r1 r r'
    (VG : valid_ghost r1 (r ⊕ r')) l τ S
    (G : res_get r l = p_at τ S),
    ∃ S_pre,
      res_get r1 l = p_at τ S_pre.

Lemma guar_sidecond :
  ∀ IE r l v r_sb r_rf
    (G : atomic_guar IE r l v r_sb r_rf)
    acts L b EE
    (VG : valid_ghost (incoming acts L b)
           (r ⊕ out_esc acts L EE b))
    (RS : res_lt (res_strip (incoming acts L b)) r) τ S
    (G1 : res_get r_rf l = p_at τ S) S' σ
    (G2 : res_get (L (TescS σ b)) l = p_at τ S')
    (IN : In σ EE)
    (ND : NoDup EE),
    slist_lt S' S.

Lemma res_lt_rf_in acts a b L :
  In a acts →
  NoDup acts →
  res_lt (L (Trf a b)) (incoming acts L b).

Lemma compat_atom_write :
  ∀ b acts amap sb rf mo sc
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (PC: prefix_closed sb rf acts)
    (ND: NoDup (b::acts)) l
    (AW: is_atomic_writeL (amap b) l) M L IE EE
    (V : ∀ a, In a acts → valid_node IE (b :: acts) M amap rf L EE a) r
    (CC : compat amap sb rf (upd L (TsbS b) r))
    (CO : conform (b :: acts) amap mo L acts)
    (VG : valid_ghost (incoming (b :: acts) L b)
                      (r ⊕ out_esc (b :: acts) L EE b))
    (Orf : L (TrfS b) = res_emp)
    (Orf0 : rsum (map L (map (Trf b) (b::acts))) = res_emp)
    (Osb : L (TsbS b) = res_emp)
    (Osb0 : rsum (map L (map (Tsb b) (b::acts))) = res_emp)
    (LR : label_restr (b :: acts) amap sb rf L EE)
    (ND': NoDup EE)
    τ s S' r_sb r_rf
    (REQ : r_sb ⊕ r_rf = res_upd r l (p_at τ S'))
    (Gsb : res_get r_sb l = p_at τ S')
    (Grf : res_get r_rf l = p_at τ S')
    S (GET : res_get r l = p_at τ S)
    v (AG : atomic_guar IE r l v r_sb r_rf)
    (LT: res_lt (res_strip (incoming (b :: acts) L b)) r)
    (LAST : ∀ s0, In s0 (SL_list S) → prot_trans τ s0 s)
    (SEQ : ∀ s0, In s0 (SL_list S') ↔ s0 = s ∨ In s0 (SL_list S))
    (CO' : conform (b :: acts) amap mo (upd L (TrfS b) r_rf) (b :: acts)),
    compat amap sb rf (upd L (TsbS b) (res_upd r l (p_at τ S'))).

Lemma vghost_get_bot r1 r r' l :
  valid_ghost r1 (r ⊕ r') →
  res_get r1 l = p_bot →
  res_get r l = p_bot.

Lemma res_escr_atomic_guar IE r l v r_sb r_rf σ :
  atomic_guar IE r l v r_sb r_rf →
  r ≠ Rundef →
  res_escr r_sb σ ∨ res_escr r_rf σ →
  res_escr r σ.


Lemma guar_step :
  ∀ b acts (NIN: ¬ In b acts) amap sb rf mo sc r
    (CONS: Consistent (b :: acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI: pres_in sb rf b acts) IE r_pre r_sb r_rf
    (G: guar IE r_pre r (amap b) r_sb r_rf) L
    (RPRE: r_pre = in_sb (b::acts) L b ⊕ in_rf (b::acts) L b) r_pre_sb
    (RELY: rely IE r_pre_sb (amap b) r_pre) EE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L EE a)
    (CC: compat amap sb rf (upd L (TsbS b) (L (TsbS b) ⊕ r)))
    (ECO: ∀ σ,
            exch_conform IE (b::acts) amap sb rf
                         (upd L (TsbS b) (L (TsbS b) ⊕ r))
                         (upd L (TsbS b) (L (TsbS b) ⊕ r)) EE σ)
    (CO: conform (b::acts) amap mo L acts)
    (GAC: ghost_alloc_conform (b::acts)
                (upd L (TsbS b) (L (TsbS b) ⊕ r)) EE)
    (VG: valid_ghost (incoming (b::acts) L b)
                     (r ⊕ out_esc (b::acts) L EE b))
    
    (Orf: out_rf (b::acts) L b = res_emp)
    (Osb: out_sb (b::acts) L b = res_emp)
    (RS: res_lt (res_strip (incoming (b::acts) L b)) r)
    
    (LR : label_restr (b :: acts) amap sb rf L EE)
    (ND': NoDup EE)
    (WPE: pre_write_prot_equiv IE acts amap mo L b r_pre (incoming (b::acts) L b)),
  ∃ L',
    ≪ V : ∀ a (IN: In a (b::acts)), valid_node IE (b::acts) (b::acts) amap rf L' EE a ≫ ∧
    ≪ CC: compat amap sb rf L' ≫ ∧
    ≪ ECO: ∀ σ, exch_conform IE (b::acts) amap sb rf L' L' EE σ ≫ ∧
    ≪ CO: conform (b::acts) amap mo L' (b :: acts) ≫ ∧
    ≪ GAC: ghost_alloc_conform (b::acts) L' EE ≫ ∧
    ≪ EsbS: ∀ a, a ≠ b → L' (TsbS a) = L (TsbS a) ≫ ∧
    ≪ EsbS': L' (TsbS b) = r_sb ≫ ∧
    ≪ LR : label_restr (b :: acts) amap sb rf L' EE ≫.