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.

Local Open Scope string_scope.

Set Implicit Arguments.

Definition pre_write_prot_equiv IE acts amap (mo : relation actid) L b r_pre r' :=
  match amap b with
    | Aalloc l n ⇒
          ∀ loc, l ≤ loc ≤ l + n → res_get r' loc = p_bot
    | Astore typ l _ ⇒
        ∀ (ISREL: is_release_wtyp typ) τ S,
          res_get r_pre l ≠ p_bot →
          res_get r' l = p_at τ S →
          ∃ a,
            ≪ INa : In a acts ≫ ∧
            ≪ MO : immediate mo a b ≫ ∧
            ≪ Wa : is_writeL (amap a) l ≫ ∧
          ∃ v_env,
            (∃ Sxxx, res_get (out_rf (b::acts) L a) l = p_at τ Sxxx ∧
                          slist_lt S Sxxx) ∧
            env_move IE r_pre l v_env (out_rf (b::acts) L a)
    | Armw typ l _ _ ⇒
        ∀ (ISACQ: is_acquire_utyp typ) (ISREL: is_release_utyp typ) τ S,
          res_get r_pre l = p_at τ S →
          ∃ Su,
            res_get r' l = p_at τ Su ∧ get_state S = get_state Su
    | _ ⇒ True
  end.

Lemma pwpe :
  ∀ 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
    (RELY : rely IE (in_sb (b :: acts) L b) (amap b)
      (in_sb (b :: acts) L b ⊕ in_rf (b :: acts) L b))
    EE r
    (V : ∀ a : actid, 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)))
    (CO : conform (b :: acts) amap mo L acts)
    (VG : valid_ghost (incoming (b :: acts) L b)
      (r ⊕ out_esc (b :: acts) L EE b))
  (RS : res_lt (res_strip (incoming (b :: acts) L b)) r)
  (NDE: NoDup EE)
  (LR : label_restr (b :: acts) amap sb rf L EE),
   pre_write_prot_equiv IE acts amap mo L b
     (in_sb (b :: acts) L b ⊕ in_rf (b :: acts) L b) (incoming (b :: acts) L b).

Lemma wpe :
  ∀ IE b acts amap mo L r_pre r r' r'',
    pre_write_prot_equiv IE acts amap mo L b r_pre r →
    valid_ghost r (r' ⊕ r'') →
    res_lt (res_strip r) r' →
    write_prot_equiv IE (amap b) r_pre r'.