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

Local Open Scope string_scope.

Set Implicit Arguments.

Inductive tagged_edge :=
  | Tsb (a b : actid)
  | TsbS (a: actid)
  | Trf (a b : actid)
  | TrfS (a: actid)
  | Tesc (a b : actid)
  | TescS (σ: escrowTy) (a: actid).

Definition labeling := tagged_edge → resource.

Definition tagged_threads := list (actid × exp × resource × (nat → RProp)).

Definition te_src te :=
  match te with
    | Tsb a _
    | TsbS a
    | Trf a _
    | TrfS a
    | Tesc a _
    | TescS _ a ⇒ a
  end.

Definition te_tgt te :=
  match te with
    | Tsb _ b
    | Trf _ b
    | Tesc _ b ⇒ Some b
    | TsbS _
    | TrfS _
    | TescS _ _ ⇒ None
  end.

Definition valid_ghost r r' :=
  ∃ p g escr,
    r = Rdef p g escr ∧
    ∃ g' escr',
      r' = Rdef p g' escr' ∧
      ≪ VGG : ∀ gl gm (RG: g gl = Some gm),
               ∃ gm', g' gl = Some (existT _ (projT1 gm) gm') ∧
                           (∀ fr (SPN: salg_plus _ gm' fr = None),
                              salg_plus _ (projT2 gm) fr = None) ≫.

Notation "x ⊕ y" := (res_plus x y) (at level 55, right associativity).

Definition in_sb acts L b := rsum (map L (map (Tsb^~ b) acts)).
Definition in_rf acts L b := rsum (map L (map (Trf^~ b) acts)).
Definition in_esc acts L b := rsum (map L (map (Tesc^~ b) acts)).
Definition out_sb acts L b := L (TsbS b) ⊕ rsum (map L (map (Tsb b) acts)).
Definition out_rf acts L b := L (TrfS b) ⊕ rsum (map L (map (Trf b) acts)).
Definition out_esc acts L E b :=
  rsum (map L (map (TescS^~ b) E)) ⊕ rsum (map L (map (Tesc b) acts)).

Definition incoming acts L b :=
  in_sb acts L b ⊕ in_rf acts L b ⊕ in_esc acts L b.

Definition outgoing acts L E b :=
  out_sb acts L b ⊕ out_rf acts L b ⊕ out_esc acts L E b.

Definition valid_node IE (acts N : list actid)
           (amap : actid → act)
           (rf : actid → option actid)
           (L : labeling) (E: list escrowTy) (b: actid) :=
  ∃ r,
    ≪ VG : valid_ghost (incoming acts L b) (r ⊕ out_esc acts L E b) ≫ ∧
    ≪ GUAR: guar IE (in_sb acts L b ⊕ in_rf acts L b) r (amap b)
                  (out_sb acts L b) (out_rf acts L b) ≫ ∧
    ≪ RS : res_lt (res_strip (incoming acts L b)) r ≫ ∧
    ≪ VrfM: ∀ c (INc: In c N) (RF: rf c = Some b) (RMW: is_rmw (amap c))
                    (IACQ: is_acquire (amap c)),
             L (Trf b c) = out_rf acts L b ≫ ∧
    ≪ VrfS: (∀ c (INc: In c N) (RF: rf c = Some b) (RMW: is_rmw (amap c))
                     (IACQ: is_acquire (amap c)), False) →
             L (TrfS b) = out_rf acts L b ≫ ∧
    ≪ VrfS': res_strip (L (TrfS b)) = res_strip (out_rf acts L b) ≫.

Definition may_happens_before amap sb rf :=
  clos_refl_trans _ (fun a b ⇒ sb a b ∨ synchronizes_with amap rf a b).

Definition compat amap sb rf L :=
  ∀ E
    (NDUP: NoDup E)
    (IND: ∀ te (IN: In te E) te' (IN': In te' E) b
           (TGT: te_tgt te' = Some b)
           (HB: may_happens_before amap sb rf b (te_src te)),
       False),
  rsum (map L E) ≠ Rundef.

Definition is_atomic_writeL a loc :=
  match a with
    | Askip | Aalloc _ _ | Aload _ _ _ | Astore WATna _ _ ⇒ False
    | Astore _ l _ | Armw _ l _ _ ⇒ l = loc
  end.

Definition conform acts amap (mo : actid → actid → Prop) L N :=
  ∀ loc
    a (INa : In a N) (ATa : is_atomic_writeL (amap a) loc)
    b (INb: In b N) (Wb : is_writeL (amap b) loc) (MO: mo a b),
    prot_trans_ok (res_get (out_rf acts L a) loc)
                  (res_get (out_rf acts L b) loc).

Definition sat_exch IE σ r :=
  ∀ P Q
    (EI: interp_exch IE σ = (P, Q)),
    (P r ∨ Q r).

Definition exch_conform IE acts amap sb rf L L' EE σ :=
  ∀ edge (TGT: te_tgt edge = None)
    (ESC: res_escr (L edge) σ),
  ∃ a,
    sat_exch IE σ (L (TescS σ a)) ∧
    (may_happens_before amap sb rf a (te_src edge) ∨
     ∀ r (SE: sat_exch IE σ r)
              (IDEF: incoming acts L' a ⊕ r ≠ Rundef),
     ∃ gl, res_gget r gl ≠ None ∧
                res_gget (incoming acts L' a) gl = None ∧
                res_gget (outgoing acts L' EE a) gl ≠ None).

Definition ghost_alloc r l :=
  match r with
    | Rundef ⇒ True
    | Rdef p g e ⇒ g l ≠ None
  end.

Definition ghost_alloc_conform acts L E :=
  ∀ a (IN: In a acts) a' (IN': In a' acts) gl
    (INC: ¬ ghost_alloc (incoming acts L a) gl)
    (OUT: ghost_alloc (outgoing acts L E a) gl)
    (INC': ¬ ghost_alloc (incoming acts L a') gl)
    (OUT': ghost_alloc (outgoing acts L E a') gl),
  a = a'.

Definition label_restr acts amap (sb : relation actid) rf L E :=
  ≪ LRsb : ∀ a b, ¬ sb a b → L (Tsb a b) = res_emp ≫ ∧
  ≪ LRrf : ∀ a b, ¬ synchronizes_with amap rf a b →
             L (Trf a b) = res_emp ≫ ∧
  ≪ LResc : ∀ a b, ¬ happens_before amap sb rf a b →
             L (Tesc a b) = res_emp ≫ ∧
  ≪ LRsbS : ∀ a, ¬ In a acts → L (TsbS a) = res_emp ≫ ∧
  ≪ LRrfS : ∀ a, ¬ In a acts → L (TrfS a) = res_emp ≫ ∧
  ≪ LRescS: ∀ σ a, ¬ In a acts ∨ ¬ In σ E →
             L (TescS σ a) = res_emp ≫.

Definition gsafe IE n acts amap sb rf mo sc L E (T : tagged_threads) :=
  ≪ V : ∀ a (IN: In a acts), valid_node IE acts acts amap rf L E a ≫ ∧
  ≪ CC: compat amap sb rf L ≫ ∧
  ≪ CO: conform acts amap mo L acts ≫ ∧
  ≪ ECO: ∀ σ, exch_conform IE acts amap sb rf L L E σ ≫ ∧
  ≪ GAC: ghost_alloc_conform acts L E ≫ ∧
  ≪ SBS : ∀ a (IN: In a acts),
             L (TsbS a) =
             rsum (map (fun aerP ⇒ snd (fst aerP))
                       (filter (fun aerP ⇒ fst (fst (fst aerP)) == a) T)) ≫ ∧
  ≪ CT : ∀ aerP (IN: In aerP T), In (fst (fst (fst aerP))) acts ≫ ∧
  ≪ SAFE : ∀ a e r PP (IN: In (a, e, r, PP) T), safe IE n e PP r ≫ ∧
  ≪ CONS: Consistent acts amap sb rf mo sc ≫ ∧
  ≪ ND : NoDup acts ≫ ∧
  ≪ NDE : NoDup E ≫ ∧
  ≪ LR : label_restr acts amap sb rf L E ≫.

Lemma mhb_trans amap sb rf a b c :
  may_happens_before amap sb rf a b →
  may_happens_before amap sb rf b c →
  may_happens_before amap sb rf a c.

Lemma hb_in_ct amap sb rf sc a b :
  happens_before amap sb rf a b →
  clos_trans _ (fun a b ⇒ sb a b ∨ rf b = Some a ∨ sc a b) a b.

Lemma hb_sb amap (sb: _ → _ → Prop) rf a b :
  sb a b → happens_before amap sb rf a b.

Lemma hb_sw amap sb rf a b:
  synchronizes_with amap rf a b →
  happens_before amap sb rf a b.

Lemma hb_trans amap sb rf a b c :
  happens_before amap sb rf a b →
  happens_before amap sb rf b c →
  happens_before amap sb rf a c.

Hint Immediate hb_in_ct hb_sb hb_sw.

Lemma mhbE amap sb rf a b :
  may_happens_before amap sb rf a b ↔
  a = b ∨ happens_before amap sb rf a b.

Definition prefix_closed (sb : actid → actid → Prop) rf (N : list actid) :=
  ≪ PCsb : ∀ b (IN: In b N) a (SB: sb a b), In a N ≫ ∧
  ≪ PCrf : ∀ b (IN: In b N) a (RF: rf b = Some a), In a N ≫.

Definition pres_in (sb : actid → actid → Prop) rf b N :=
  (∀ a (SB: sb a b), In a N) ∧
  (∀ a (SB: rf b = Some a), In a N).

Lemma prefix_closed_hb amap sb rf l a b :
  prefix_closed sb rf l →
  happens_before amap sb rf a b →
  In b l →
  In a l.

Lemma pres_in_hb amap sb rf l a b :
  prefix_closed sb rf l →
  happens_before amap sb rf a b →
  pres_in sb rf b l →
  In a l.

Lemma Consistent_pres_in :
  ∀ b acts amap sb rf mo sc (CONS: Consistent (b::acts) amap sb rf mo sc),
    pres_in sb rf b acts.

Lemma Consistent_prefix_closed :
  ∀ acts amap sb rf mo sc (CONS: Consistent acts amap sb rf mo sc),
    prefix_closed sb rf acts.

Lemma Consistent_prefix_closed2 :
  ∀ b acts amap sb rf mo sc (CONS: Consistent (b :: acts) amap sb rf mo sc)
    (Nsb: ∀ x, sb b x → False)
    (Nrf: ∀ x, rf x = Some b → False),
    prefix_closed sb rf acts.

Lemma lr_ext_esc acts amap sb rf L E σ :
  label_restr acts amap sb rf L E →
  label_restr acts amap sb rf L (σ :: E).

Lemma lr_upd_sbS acts amap sb rf L E b r :
  label_restr acts amap sb rf L E → In b acts →
  label_restr acts amap sb rf (upd L (TsbS b) r) E.

Lemma lr_upd_rfS acts amap sb rf L E b r :
  label_restr acts amap sb rf L E → In b acts →
  label_restr acts amap sb rf (upd L (TrfS b) r) E.

Lemma lr_upd_escS acts amap sb rf L E σ b r :
  label_restr acts amap sb rf L E → In b acts → In σ E →
  label_restr acts amap sb rf (upd L (TescS σ b) r) E.

Lemma lr_upd_sb acts amap sb rf L E a b r :
  label_restr acts amap sb rf L E → sb a b →
  label_restr acts amap sb rf (upd L (Tsb a b) r) E.

Lemma lr_upd_rf acts amap sb rf L E a b r :
  label_restr acts amap sb rf L E → synchronizes_with amap rf a b →
  label_restr acts amap sb rf (upd L (Trf a b) r) E.

Lemma lr_upd_esc acts amap sb rf L E a b r :
  label_restr acts amap sb rf L E → happens_before amap sb rf a b →
  label_restr acts amap sb rf (upd L (Tesc a b) r) E.

Hint Resolve lr_upd_sbS lr_upd_rfS lr_upd_escS
             lr_upd_sb lr_upd_rf lr_upd_esc.

Lemma Permutation_rsum l l' : Permutation l l' → rsum l = rsum l'.

Lemma is_write_weaken typ l v : is_writeLV typ l v → is_writeL typ l.

Lemma is_access_weaken typ l v : is_writeLV typ l v → is_access typ.

Hint Resolve is_write_weaken is_access_weaken.

Definition mydecf A (f : A → Prop) x :=
  if excluded_middle_informative (f x) then true else false.

Lemma rsum_map_filter A (f : A → resource) h l :
  (∀ x, In x l → ¬ h x → f x = res_emp) →
  rsum (map f (filter (mydecf h) l)) =
  rsum (map f l).

Lemma rsum_map_map_filter A B f (g : A → B) h l :
  (∀ x, In x l → ¬ h x → f (g x) = res_emp) →
  rsum (map f (map g (filter (mydecf h) l))) =
  rsum (map f (map g l)).

Lemma no_rf_rmw_overtaken acts amap sb rf mo sc a b b_rf :
  Consistent acts amap sb rf mo sc →
  rf b = Some b_rf →
  rf a = Some b_rf →
  is_rmw (amap a) →
  happens_before amap sb rf a b →
  False.

Lemma no_rf_rmw_double acts amap sb rf mo sc a b b_rf :
  Consistent acts amap sb rf mo sc →
  rf b = Some b_rf →
  rf a = Some b_rf →
  is_rmw (amap a) →
  is_rmw (amap b) →
  a = b.

Lemma aguar_interp_prot IE r l v r_sb r_rf τ S :
  res_get r_rf l = p_at τ S →
  atomic_guar IE r l v r_sb r_rf →
  interp_prot IE τ (get_state S) v r_rf.

Lemma slist_lt_trans A (x y z: slist A) :
  slist_lt x y →
  slist_lt y z →
  slist_lt x z.

Lemma exists_immediate :
  ∀ A (r : relation A)
    (IRR: irreflexive r) (T: transitive _ r) a b
    (HAS : r a b) l
    (FIN : ∀ c, r a c → r c b → In c l),
  ∃ a', immediate r a' b ∧ (a = a' ∨ r a a').

Lemma rsum_app l l' :
  rsum (l ++ l') = rsum l ⊕ rsum l'.

Lemma in_rf_upds acts L a b r :
  NoDup acts →
  In a acts →
  in_rf acts L b = res_emp →
  in_rf acts (upd L (Trf a b) r) b = r.

Lemma no_rmw_between :
  ∀ b acts amap sb rf mo sc
    (CONS : Consistent (b :: acts) amap sb rf mo sc) typ l v
    (H : amap b = Astore typ l v) a
    (MO : immediate mo a b) c
    (IN: In c acts)
    (RF: rf c = Some a)
    (RMW: is_rmw (amap c)),
    False.

Ltac discharge_eq_emp_tac :=
 repeat first [ apply rsum_map_map_eq_empI; intros ? _; ins; desf; ins
              | apply res_plus_eq_empI ]; ins; desf; desf;
  try match goal with H: ¬ (_ ∨ _) |- _ ⇒ solve [destruct H; vauto] end.

Lemma rsum_eq_empI l :
  (∀ x, In x l → x = res_emp) → rsum l = res_emp.

Lemma Consistent_sw_in :
  ∀ acts amap sb rf mo sc (C : Consistent acts amap sb rf mo sc) a b,
  synchronizes_with amap rf a b →
  In a acts ∧ In b acts.

Lemma Consistent_hb_in :
  ∀ acts amap sb rf mo sc (C : Consistent acts amap sb rf mo sc) a b,
  happens_before amap sb rf a b →
  In a acts ∧ In b acts.

Lemma vghost_get_at :
  ∀ r1 r r'
    (VG : valid_ghost r1 (r ⊕ r'))
    (RS : res_lt (res_strip r1) r) l τ S
    (G1 : res_get r1 l = p_at τ S),
    res_get r l = p_at τ S.

Lemma vghost_get_back_at :
  ∀ r1 r r'
    (VG : valid_ghost r1 (r ⊕ r'))
    (RS : res_lt (res_strip r1) r) l τ S
    (G1 : res_get r l = p_at τ S),
    res_get r1 l = p_at τ S.

Lemma vghost_get_back :
  ∀ r1 r2 r r'
    (VG : valid_ghost (r1 ⊕ r2) (r ⊕ r')) l τ S
    (G : res_get r l = p_at τ S)
    (NBOT : res_get r1 l ≠ p_bot),
    ∃ S_pre,
      res_get r1 l = p_at τ S_pre.

Lemma vghost_get_back_uninit :
  ∀ r1 r r'
    (VG : valid_ghost r1 (r ⊕ r')) l
    (G : res_get r l = p_uninit),
  res_get r1 l = p_uninit.

Lemma res_lt_emp_l r : res_lt res_emp r.

Lemma is_atomic_write_weaken typ l : is_atomic_writeL typ l → is_writeL typ l.

Hint Immediate is_atomic_write_weaken.

Lemma prot_trans_ok_trans x y z :
  prot_trans_ok x y →
  prot_trans_ok y z →
  prot_trans_ok x z.

Lemma plus_upd_def :
  ∀ r l τ S
    (G : res_get r l = p_at τ S) r' S'
    (P : res_upd r l (p_at τ S') ⊕ r' = Rundef)
    (IMP: ∀ S'' (G' : res_get r' l = p_at τ S'')
           s' (IN': In s' (SL_list S')) (NIN': ¬ In s' (SL_list S))
           s'' (IN'': In s'' (SL_list S'')), prot_trans τ s' s'' ∨ prot_trans τ s'' s'),
  r ⊕ r' = Rundef.

Lemma get_plus_at_oneD :
  ∀ r r' l τ S s,
    res_get (res_plus r r') l = p_at τ S →
    In s (SL_list S) →
    ∃ S', (res_get r l = p_at τ S' ∨ res_get r' l = p_at τ S') ∧ In s (SL_list S').

Lemma get_rsum_at_oneD :
  ∀ rl l τ S s,
    res_get (rsum rl) l = p_at τ S →
    In s (SL_list S) →
    ∃ r S', In r rl ∧ res_get r l = p_at τ S' ∧ In s (SL_list S').

Lemma valid_ghost_refl r : r ≠ Rundef → valid_ghost r r.

Lemma rely_def IE r act r' : rely IE r act r' → r' ≠ Rundef.

Lemma filter_eq_nil A (f : A → bool) l :
  (∀ x, In x l → f x = false) → filter f l = nil.

Lemma hb_in_acts2 acts amap sb rf mo sc a b :
  Consistent acts amap sb rf mo sc →
  happens_before amap sb rf a b →
  In b acts.