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

Local Open Scope string_scope.

Set Implicit Arguments.

Definition pre_write_prot_equiv 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 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
    (RELY : rely (in_sb (b :: acts) L b) (amap b)
      (in_sb (b :: acts) L b ⊕ in_rf (b :: acts) L b))
    I r
    (V : ∀ a : actid, In a acts → valid_node (b :: acts) (b::acts) amap rf L a)
    (CC : compat amap sb rf (upd L (TescS b) (L (TescS b) ⊕ r)))
    (CO : conform (b :: acts) amap mo L acts)
    (VG : valid_ghost (incoming (b :: acts) L b)
      (r ⊕ out_esc (b :: acts) L b ⊕ L (TcondS b)) I)
  (RS : res_lt (res_strip (incoming (b :: acts) L b)) r)
  (LR : label_restr (b :: acts) amap sb rf L),
   pre_write_prot_equiv acts amap mo L b
     (in_sb (b :: acts) L b ⊕ in_rf (b :: acts) L b) (incoming (b :: acts) L b).

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

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
    (V : ∀ a (IN: In a acts), valid_node (b::acts) (b::acts) amap rf L a)
    (CO: conform (b::acts) amap mo L acts) r'
    (CC: compat amap sb rf (upd L (TescS b) (L (TescS 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)
    (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 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 (TescS 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' I
    (VG : valid_ghost r1 (r ⊕ r') I) l τ S
    (G : res_get r l = p_at τ S),
    ∃ S_pre,
      res_get r1 l = p_at τ S_pre.

Lemma guar_sidecond :
  ∀ r l v r_sb r_rf
    (G : atomic_guar r l v r_sb r_rf)
    acts L b I
    (VG : valid_ghost (incoming acts L b)
           (r ⊕ out_esc acts L b ⊕ L (TcondS b)) I)
    (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'),
    slist_lt S' S.

Lemma guar_sidecond2 :
  ∀ r l v r_sb r_rf
    (G : atomic_guar r l v r_sb r_rf)
    acts L b I
    (VG : valid_ghost (incoming acts L b)
           (r ⊕ out_esc acts L b ⊕ L (TcondS b)) I)
    (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 (TcondS b)) l = p_at τ S'),
    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
    (V : ∀ a, In a acts → valid_node (b :: acts) M amap rf L a) r
    (CC : compat amap sb rf (upd L (TsbS b) r))
    (CO : conform (b :: acts) amap mo L acts) I
    (VG : valid_ghost (incoming (b :: acts) L b)
                      (r ⊕ out_esc (b :: acts) L b ⊕ L (TcondS b)) I)
    (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)
    τ 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 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' I l :
  valid_ghost r1 (r ⊕ r') I →
  res_get r1 l = p_bot →
  res_get r l = p_bot.

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) r_pre r_sb r_rf
    (G: guar 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 r_pre_sb (amap b) r_pre)
    (V : ∀ a (IN: In a acts), valid_node (b::acts) (b::acts) amap rf L a)
    (CC: compat amap sb rf (upd L (TescS b) (L (TescS b) ⊕ r)))
    (CO: conform (b::acts) amap mo L acts) I
    (VG: valid_ghost (incoming (b::acts) L b)
                     (r ⊕ out_esc (b::acts) L b ⊕ L (TcondS b)) I)
    (VI : ∀ σ r (GIN: In (σ, r) I),
            ∃ P P', interp_escr σ = (P, P') ∧ P' r)
    (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)
    (VES: res_lt (rsum (map snd (filter (escr_ffun L (b::acts)) I))) (L (TescS b)))
    (LR : label_restr (b :: acts) amap sb rf L)
    (WPE: pre_write_prot_equiv acts amap mo L b r_pre (incoming (b::acts) L b)),
  ∃ L',
    ≪ V : ∀ a (IN: In a (b::acts)), valid_node (b::acts) (b::acts) amap rf L' a ≫ ∧
    ≪ CC: compat amap sb rf L' ≫ ∧
    ≪ CO: conform (b::acts) amap mo L' (b :: acts) ≫ ∧
    ≪ 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' ≫.

Lemma prepare_step :
  ∀ b acts amap sb rf mo sc
    (CONS: Consistent (b :: acts) amap sb rf mo sc)
    (NIN : ¬ In b acts)
    (ND : NoDup (b :: acts)) a
    (SB : sb a b) amap_old sb_old rf_old mo_old sc_old
    (OCON: Consistent acts amap_old sb_old rf_old mo_old sc_old) L
    (LR : label_restr acts amap_old sb_old rf_old L) r r_rem
    (LAB : L (TsbS a) = r ⊕ r_rem)
    (V : ∀ a, In a acts → valid_node acts acts amap_old rf_old L a)
    (CC : compat amap_old sb_old rf_old L)
    (CO : conform acts amap_old mo_old L acts)
    (Ea : ∀ x, In x acts → amap x = amap_old x)
    (Esb : ∀ x y, sb x y ↔ sb_old x y ∨ x = a ∧ y = b)
    (Erf : ∀ x, x ≠ b → rf x = rf_old x)
    (Emo : ∀ x, x ≠ b → ∀ y, y ≠ b → (mo x y ↔ mo_old x y))
    (Esc : ∀ x, x ≠ b → ∀ y, y ≠ b → (sc x y ↔ sc_old x y)),
  ∃ L',
    ≪ V : ∀ a, In a acts → valid_node (b :: acts) acts amap rf L' a ≫ ∧
    ≪ CC : compat amap sb rf L' ≫ ∧
    ≪ CO : conform (b :: acts) amap mo L' acts ≫ ∧
    ≪ LAB : L' (TsbS a) = r_rem ≫ ∧
    ≪ LSB : in_sb (b :: acts) L' b = r ≫ ∧
    ≪ LR : label_restr (b :: acts) amap sb rf L' ≫ ∧
    ≪ Irf : in_rf (b :: acts) L' b = res_emp ≫ ∧
    ≪ Iesc: in_esc (b :: acts) L' b = res_emp ≫ ∧
    ≪ Isb : ∀ a', a' ≠ a → L' (Tsb a' b) = res_emp ≫ ∧
    ≪ O : outgoing (b :: acts) L' b = res_emp ≫ ∧
    ≪ LEQ : ∀ a', a' ≠ a → L' (TsbS a') = L (TsbS a') ≫ ∧
    ≪ PC : prefix_closed sb rf acts ≫.