Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import Omega List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas GpsLogic.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.
Require Import GpsPrep GpsRely GpsGhost GpsWPE GpsGuar.

Local Open Scope string_scope.

Set Implicit Arguments.

Definition erase (x : actid × exp × resource × (nat → RProp)) :=
   let '(a, e, r, QQ) := x in (a, e).

Theorem gsafe_pres :
  ∀ IE n mc L EE T mc',
    gsafe IE (n + 1) (Macts mc) (Mamap mc) (Msb mc) (Mrf mc) (Mmo mc) (Msc mc) L EE T →
    map erase T = Mtmap mc →
    mc_step mc mc' →
    ∃ L' EE' T',
      gsafe IE n (Macts mc') (Mamap mc') (Msb mc') (Mrf mc') (Mmo mc') (Msc mc') L' EE' T' ∧
      map erase T' = Mtmap mc' ∧
      ∃ rem, map (fun x ⇒ snd x) T' = map (fun x ⇒ snd x) T ++ rem.

Lemma gsafe_memsafe IE n acts amap sb rf mo sc L EE T :
  gsafe IE n acts amap sb rf mo sc L EE T →
  mem_safe acts amap sb rf.

Lemma compat_inc2 :
  ∀ acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a b
    (NEQ : a ≠ b)
    (NHB : ¬ happens_before amap sb rf a b)
    (NHB': ¬ happens_before amap sb rf b a),
  incoming acts L a ⊕ incoming acts L b ≠ Rundef.

Lemma gsafe_racefree IE n acts amap sb rf mo sc L EE T :
  gsafe IE n acts amap sb rf mo sc L EE T →
  race_free acts amap sb rf.

Lemma gsafe_rinit IE n acts amap sb rf mo sc L EE T :
  gsafe IE n acts amap sb rf mo sc L EE T →
  initialized_reads acts amap rf.

Lemma Consistent_ext_skip :
  ∀ acts amap sb rf mo sc
    (CONS : Consistent acts amap sb rf mo sc)
    a' (INa : In a' acts)
    b' (NIN : ¬ In b' acts),
  Consistent (b' :: acts) amap (fun a b ⇒ sb a b ∨ a = a' ∧ b = b') rf mo sc.

Lemma gsafe_final_sat :
  ∀ IE acts amap sb rf mo sc
    (CONS' : Consistent acts amap sb rf mo sc) L' EE
    (V : ∀ a, In a acts → valid_node IE acts acts amap rf L' EE a)
    (CC : compat amap sb rf L')
    (CO : conform acts amap mo L' acts)
    (ECO: ∀ σ, exch_conform IE acts amap sb rf L' L' EE σ) a r r_rem
    (GAC : ghost_alloc_conform acts L' EE)
    (SBS : L' (TsbS a) = r ⊕ r_rem)
    (CT : In a acts) QQ
    (END : ghost_move IE r QQ)
    (ND : NoDup acts)
    (NDE : NoDup EE)
    (LR : label_restr acts amap sb rf L' EE),
  ∃ r, QQ r.

Theorem adequacy :
  ∀ IE e QQ (T: triple IE Rtrue e QQ) e' acts amap sb rf mo sc,
    cexecutions e e' acts amap sb rf mo sc →
    mem_safe acts amap sb rf ∧
    race_free acts amap sb rf ∧
    initialized_reads acts amap rf ∧
    ∀ v, e' = Evalue v → ∃ r, (QQ v) r.