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 (sigma: 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 sigma r :=
  ∀ P Q
    (EI: interp_exch IE sigma = (P, Q)),
    (P r ∨ Q r).

Definition exch_conform IE acts amap sb rf L L' EE sigma :=
  ∀ edge (TGT: te_tgt edge = None)
    (ESC: res_escr (L edge) sigma),
  ∃ a,
    sat_exch IE sigma (L (TescS sigma a)) ∧
    (may_happens_before amap sb rf a (te_src edge) ∨
     ∀ r (SE: sat_exch IE sigma 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: ∀ sigma a, ¬ In a acts ∨ ¬ In sigma E →
             L (TescS sigma 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: ∀ sigma, exch_conform IE acts amap sb rf L L E sigma >> ∧
  << 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.
Proof.
  unfold may_happens_before; eauto using rt_trans.
Qed.

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.
Proof.
  induction 1 as [? ? [|[]]|]; eauto using clos_trans.
Qed.

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

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

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.
Proof.
  unfold happens_before; eauto using t_trans.
Qed.

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.
Proof.
  unfold may_happens_before, happens_before, imm_happens_before; split; ins; desf; eauto;
  try induction H; desf; eauto using clos_trans, clos_refl_trans.
Qed.

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.
Proof.
  induction 2; eauto.
  unfold imm_happens_before, synchronizes_with, prefix_closed in *; desf; eauto.
Qed.

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.
Proof.
  ins; apply clos_trans_tn1 in H0; destruct H0;
    [|eapply prefix_closed_hb; eauto; try eby eapply clos_tn1_trans];
    unfold imm_happens_before, synchronizes_with, pres_in in *; desf; eauto.
Qed.

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.
Proof.
  red; unfold NW; ins; red in CONS; desf; split; ins.
    destruct (proj1 (proj2 FIN _ _ SB)); ins; desf; edestruct ACYC; vauto.
  specialize (Crf b); rewrite SB in *; desf.
  assert (X: In a (b::acts)) by (by apply (proj1 FIN); intro X; rewrite X in *).
  destruct X; desf; edestruct ACYC; eauto using t_step.
Qed.

Lemma Consistent_prefix_closed :
  ∀ acts amap sb rf mo sc (CONS: Consistent acts amap sb rf mo sc),
    prefix_closed sb rf acts.
Proof.
  red; unfold NW; ins; red in CONS; desf; split; ins.
    by apply (proj2 FIN) in SB; desf.
  specialize (Crf b); rewrite RF in *; desf.
  by apply (proj1 FIN); intro X; rewrite X in ×.
Qed.

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.
Proof.
  ins; apply Consistent_prefix_closed in CONS.
  red; unfold NW; ins; red in CONS; desf; split; ins.
    by edestruct PCsb; eauto; desf; exfalso; eauto.
  by edestruct PCrf; eauto; desf; exfalso; eauto.
Qed.

Lemma lr_ext_esc acts amap sb rf L E sigma :
  label_restr acts amap sb rf L E →
  label_restr acts amap sb rf L (sigma :: E).
Proof.
  destruct 1; desf; repeat split; unfold NW, upd; ins; desf; auto.
  apply LRescS; tauto.
Qed.

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.
Proof.
  destruct 1; desf; repeat split; unfold NW, upd; ins; desf; auto.
Qed.

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.
Proof.
  destruct 1; desf; repeat split; unfold NW, upd; ins; desf; auto.
Qed.

Lemma lr_upd_escS acts amap sb rf L E sigma b r :
  label_restr acts amap sb rf L E → In b acts → In sigma E →
  label_restr acts amap sb rf (upd L (TescS sigma b) r) E.
Proof.
  destruct 1; desf; repeat split; unfold NW, upd; ins; desf; auto.
Qed.

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.
Proof.
  destruct 1; desf; repeat split; unfold NW, upd; ins; desf; auto.
Qed.

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.
Proof.
  destruct 1; desf; repeat split; unfold NW, upd; ins; desf; auto.
Qed.

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.
Proof.
  destruct 1; desf; repeat split; unfold NW, upd; ins; desf; auto.
Qed.

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'.
Proof.
  induction 1; ins; try congruence; apply res_plusAC.
Qed.

Lemma is_write_weaken typ l v : is_writeLV typ l v → is_writeL typ l.
Proof. destruct typ; ins; desf. Qed.

Lemma is_access_weaken typ l v : is_writeLV typ l v → is_access typ.
Proof. destruct typ; ins; desf. Qed.

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).
Proof.
  induction l; ins; desf; ins; f_equal; eauto.
  rewrite H, res_plus_emp_l; eauto.
  unfold mydecf in *; desf.
Qed.

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)).
Proof.
  induction l; ins; desf; ins; f_equal; eauto.
  rewrite H, res_plus_emp_l; eauto.
  unfold mydecf in *; desf.
Qed.

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.
Proof.
  unfold Consistent; ins; desc.
  edestruct Crmw as [MO _]; eauto.
  generalize (Crf b), (Crf a); rewrite H0, H1; ins; desc.
  eapply Cwr in H0; eauto.
  destruct (amap b_rf); ins; destruct (amap a); ins; destruct (amap b); ins; desf.
Qed.

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.
Proof.
  unfold Consistent; ins; desc.
  edestruct Crmw with (a := a) as [MO _]; eauto.
  edestruct Crmw with (a := b) as [MO' _]; eauto.
  generalize (Crf b), (Crf a); rewrite H0, H1; ins; desc.
  assert (l0 = l) by (destruct (amap b_rf); ins; desf); subst.
  apply NNPP; intro N; eapply Cmo with (l:=l) in N; desf; try eapply Crmw in N; eauto.
    by destruct (amap a); ins; desf.
    by destruct (amap b); ins; desf.
Qed.

Lemma aguar_interp_prot IE r l v r_sb r_rf tau S :
  res_get r_rf l = p_at tau S →
  atomic_guar IE r l v r_sb r_rf →
  interp_prot IE tau (get_state S) v r_rf.
Proof.
  unfold atomic_guar; ins; desf; rewrite H in *; desf;
  replace (get_state S') with s; try done.
    by unfold get_state; destruct S'; ins; subst; ins.

  assert (IN := proj2 (SEQ s) (in_eq _ _)).
  assert (A: ∀ x, In x (SL_list S') → prot_trans tau0 x s).
    ins; apply SEQ in H0; desf; eauto using prot_trans_refl.
  clear - IN A.
  unfold get_state; des_eqrefl; [exfalso|]; ins.
    by destruct S'; ins; destruct (exists_last SL_nemp) as (? & ? & ?); subst;
       rewrite rev_app_distr in ×.
  destruct S'; ins.
  assert (∃ l, SL_list = l ++ p :: nil).
    revert x EQ; clear; induction SL_list using rev_ind; ins.
    by rewrite rev_app_distr in *; ins; desf; vauto.
  desf.
  rewrite in_app_iff in *; ins; desf.
   exploit Sorted_app_end_inv; eauto; ins.
  eapply prot_trans_ord; eauto using in_or_app, in_eq.
Qed.

Lemma slist_lt_trans A (x y z: slist A) :
  slist_lt x y →
  slist_lt y z →
  slist_lt x z.
Proof.
  unfold slist_lt; ins; desf.
  edestruct H as (? & ? & ?); eauto.
  edestruct H0 as (? & ? & ?); eauto using prot_trans_trans.
Qed.

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').
Proof.
  induction[a HAS] l; ins.
    ∃ a; repeat split; eauto.
  destruct (classic (r a b ∧ r a0 a)); desf; eauto.
    destruct (IHl a) as [a' ?]; ins; desf; eauto.
    by destruct (FIN c); desf; eauto; exfalso; eauto.
  eapply (IHl a0); eauto; ins.
  by destruct (FIN c); desf; destruct H.
Qed.

Lemma rsum_app l l' :
  rsum (l ++ l') = rsum l +!+ rsum l'.
Proof.
  induction l; simpl rsum; rewrite ?res_plus_emp_l, ?res_plusA; congruence.
Qed.

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.
Proof.
  unfold in_rf; intros ND H.
  eapply In_NoDup_Permutation in H; desf.
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ H))); simpl; rupd.
  rewrite map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  by intro X; apply res_plus_eq_empD, proj2 in X; rewrite X, res_plus_emp_r.
Qed.

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.
Proof.
  ins.
  red in CONS; desf.
  exploit Crmw; eauto.
  unfold immediate in *; ins; desf.
  specialize (Crf c); rewrite RF in *; desf.
  red in Cmo; desf.
  destruct (eqP b c); desf; [by rewrite H in *|].
  specialize (Cmo _ _ MO); desf; rewrite H in *; ins; desf.
  assert (l1 = l0) by (destruct (amap a); ins; desf); subst.
  specialize (Cmo1 l0 b); ins; rewrite H in *; destruct (Cmo1 eq_refl c); eauto.
  by destruct (amap c); ins; desf.
Qed.

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.
Proof.
  induction l; ins; rewrite (H a), res_plus_emp_l; eauto.
Qed.

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.
Proof.
  by destruct 2 as [_[??]]; split; apply (proj1 (proj1 C)); intro X; rewrite X in ×.
Qed.

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.
Proof.
  split; induction H; eauto; unfold imm_happens_before in *; desf;
  try eapply (proj2 (proj1 C)) in H;
  try eapply (Consistent_sw_in C) in H; desf.
Qed.

Lemma vghost_get_at :
  ∀ r1 r r'
    (VG : valid_ghost r1 (r +!+ r'))
    (RS : res_lt (res_strip r1) r) l tau S
    (G1 : res_get r1 l = p_at tau S),
    res_get r l = p_at tau S.
Proof.
  ins; red in VG; desf; red in RS; desf; ins; desf; ins; desf.
  inv_lplus l; rewrite G1 in *; desf; ins; desf.
  rewrite <- H0 in *; f_equal.
  ins; desf.
  apply slist_eq2; ins.
  by split; [clear Heq4|clear Heq5]; unfold mk_slist in *; desf; ins;
     rewrite in_undup_iff, In_sort, in_app_iff; desf; eauto.
Qed.

Lemma vghost_get_back_at :
  ∀ r1 r r'
    (VG : valid_ghost r1 (r +!+ r'))
    (RS : res_lt (res_strip r1) r) l tau S
    (G1 : res_get r l = p_at tau S),
    res_get r1 l = p_at tau S.
Proof.
  ins; red in VG; desf; red in RS; desf; ins; desf; ins; desf.
  inv_lplus l; rewrite G1 in *; desf; ins; desf.
  rewrite <- H0 in *; f_equal.
  ins; desf.
  apply slist_eq2; ins.
  by split; [clear Heq4|clear Heq5]; unfold mk_slist in *; desf; ins;
     rewrite in_undup_iff, In_sort, in_app_iff; desf; eauto.
Qed.

Lemma vghost_get_back :
  ∀ r1 r2 r r'
    (VG : valid_ghost (r1 +!+ r2) (r +!+ r')) l tau S
    (G : res_get r l = p_at tau S)
    (NBOT : res_get r1 l ≠ p_bot),
    ∃ S_pre,
      res_get r1 l = p_at tau S_pre.
Proof.
  ins; red in VG; desf.
  destruct r1, r; ins; desf; ins; desf.
  inv_lplus l; rewrite G in *; destruct (pmap l); ins; desf;
  rewrite <- H0 in *; desf; eauto.
Qed.

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.
Proof.
  ins; red in VG; desf.
  destruct r; ins; desf; ins; desf.
  inv_lplus l; rewrite G in *; ins; desf.
Qed.

Lemma res_lt_emp_l r : res_lt res_emp r.
Proof. by ∃ r; apply res_plus_emp_l. Qed.

Lemma is_atomic_write_weaken typ l : is_atomic_writeL typ l → is_writeL typ l.
Proof. destruct typ; ins; desf. Qed.

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.
Proof.
  destruct x; ins; desf; desf; ins; desf; eauto using slist_lt_trans.
Qed.

Lemma plus_upd_def :
  ∀ r l tau S
    (G : res_get r l = p_at tau S) r' S'
    (P : res_upd r l (p_at tau S') +!+ r' = Rundef)
    (IMP: ∀ S'' (G' : res_get r' l = p_at tau S'')
           s' (IN': In s' (SL_list S')) (NIN': ¬ In s' (SL_list S))
           s'' (IN'': In s'' (SL_list S'')), prot_trans tau s' s'' ∨ prot_trans tau s'' s'),
  r +!+ r' = Rundef.
Proof.
  ins; destruct r; ins; desf.
  eapply lift_plus_none_inv in Heq1; desc; inv_lplus l0.
  desf; desf; rewrite G in *; ins; desf.
  unfold mk_slist in *; desf; destruct n; clear H0; desf.
  split; ins.
   by destruct S' as [[]].
  specialize (IMP _ eq_refl); clear Heq0 Heq2 G.
  destruct s, S', S; ins.

  rewrite in_app_iff in *; desf; eauto using in_or_app;
    try solve [eapply Sorted_total; try exact H; unfold reflexive; eauto using prot_trans_refl].
    destruct (classic (In y SL_list1)); eauto 8 using in_or_app.
    exploit IMP; eauto; tauto.
  destruct (classic (In x SL_list1)); eauto 8 using in_or_app.
Qed.

Lemma get_plus_at_oneD :
  ∀ r r' l tau S s,
    res_get (res_plus r r') l = p_at tau S →
    In s (SL_list S) →
    ∃ S', (res_get r l = p_at tau S' ∨ res_get r' l = p_at tau S') ∧ In s (SL_list S').
Proof.
  destruct r, r'; ins; desf; ins.
  inv_lplus l; unfold prot_plus in *; rewrite H in *; desf; desf; eauto.
  unfold mk_slist in *; desf; ins.
  rewrite in_undup_iff, In_sort, in_app_iff in *; desf; eauto.
Qed.

Lemma get_rsum_at_oneD :
  ∀ rl l tau S s,
    res_get (rsum rl) l = p_at tau S →
    In s (SL_list S) →
    ∃ r S', In r rl ∧ res_get r l = p_at tau S' ∧ In s (SL_list S').
Proof.
  induction rl; ins.
  eapply get_plus_at_oneD in H; eauto; desf; eauto 8.
  exploit IHrl; eauto; intro; desf; eauto 8.
Qed.

Lemma valid_ghost_refl r : r ≠ Rundef → valid_ghost r r.
Proof.
  red; destruct r; ins; repeat eexists; ins; desf; eauto.
  destruct gm; ins.
Qed.

Lemma rely_def IE r act r' : rely IE r act r' → r' ≠ Rundef.
Proof.
  destruct act; ins; desf; desf.
Qed.

Lemma filter_eq_nil A (f : A → bool) l :
  (∀ x, In x l → f x = false) → filter f l = nil.
Proof.
  induction l; ins; rewrite H; eauto.
Qed.

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.
Proof.
  induction 2 as [? ? [|[? ?]]|]; eauto; red in H; desc.
    by apply (proj2 FIN), proj2 in H0.
  by apply (proj1 FIN); intro X; rewrite X in ×.
Qed.