Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 permission fslassn fslassnsem fslmodel fslassnlemmas.

Set Implicit Arguments.

Hint Unfold imm_happens_before.

Lemma hupds A h l (y : A) : hupd h l y l = y.
Proof. unfold hupd; desf; congruence. Qed.

Lemma hist_closed_trans :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: clos_refl_trans _ sb a b) (IN: In b V), In a V.
Proof. induction 2; ins; eauto using hc_edge. Qed.

Lemma hist_closedD :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: happens_before_union_rf sb rf a b) (IN: In b V), In a V.
Proof. induction 2; ins; unfold imm_happens_before in *; desf; eauto using hc_edge. Qed.

Lemma happens_before_trans lab sb rf mo a b c :
  happens_before lab sb rf mo a b →
  happens_before lab sb rf mo b c →
  happens_before lab sb rf mo a c.
Proof. apply t_trans. Qed.

Lemma happens_before_union_rf_trans sb rf a b c :
  happens_before_union_rf sb rf a b →
  happens_before_union_rf sb rf b c →
  happens_before_union_rf sb rf a c.
Proof. apply t_trans. Qed.

Lemma happens_before_sb lab (sb : relation actid) rf mo a b :
  sb a b → happens_before lab sb rf mo a b.
Proof. ins; apply t_step; auto. Qed.

Lemma happens_before_sw lab sb rf mo a b :
  synchronizes_with lab sb rf mo a b → happens_before lab sb rf mo a b.
Proof. ins; apply t_step; auto. Qed.

Lemma happens_before_union_rf_sb (sb : relation actid) rf a b :
  sb a b → happens_before_union_rf sb rf a b.
Proof. ins; apply t_step; vauto. Qed.

Lemma happens_before_union_rf_rf (sb : relation actid) rf a b :
  rf b = Some a → happens_before_union_rf sb rf a b.
Proof. ins; apply t_step; vauto. Qed.

Lemma clos_trans_hbE :
  ∀ lab sb rf mo a b (HB: clos_trans actid (happens_before lab sb rf mo) a b),
    happens_before lab sb rf mo a b.
Proof.
  induction 1; vauto.
Qed.

Lemma clos_trans_hbUrfE :
  ∀ sb rf a b (HB: clos_trans actid (happens_before_union_rf sb rf) a b),
    happens_before_union_rf sb rf a b.
Proof.
  induction 1; vauto.
Qed.

Hint Immediate clos_trans_hbE : hb.
Hint Immediate clos_trans_hbUrfE : hb.

Hint Resolve
  happens_before_sb happens_before_sw happens_before_union_rf_sb happens_before_union_rf_rf
  happens_before_trans happens_before_union_rf_trans t_step hist_closedD : hb.

Lemma count_implies :
  ∀ (T: eqType) (f1 f2 : T → bool) (IMP : ∀ x, f1 x → f2 x) l,
  count f1 l ≤ count f2 l.
Proof.
  induction l; ins; desf; eauto.
  by rewrite IMP in Heq0.
Qed.

Lemma hasP' :
  ∀ (T : eqType) (a : pred T) (l : list_predType T),
    reflect (∃ x : T, In x l ∧ a x) (has a l).
Proof.
  ins; case hasP; intro H; constructor; try red; intros; destruct H; desf.
    by apply/inP in H; eauto.
  by ∃ x; try apply/inP; eauto.
Qed.

Lemma clos_refl_transE X rel a b :
    clos_refl_trans X rel a b ↔ a = b ∨ clos_trans X rel a b.
Proof.
  split; ins; desf; try induction H; desf; eauto using clos_refl_trans, clos_trans.
Qed.

Lemma clos_refl_trans_hbE :
  ∀ lab sb rf mo a b,
    clos_refl_trans actid (happens_before lab sb rf mo) a b →
    happens_before lab sb rf mo a b ∨ a = b.
Proof.
  unfold happens_before; induction 1; desf; vauto.
Qed.

Lemma clos_refl_trans_hbUrfE :
  ∀ sb rf a b,
    clos_refl_trans actid (happens_before_union_rf sb rf) a b →
    happens_before_union_rf sb rf a b ∨ a = b.
Proof.
  induction 1; desf; vauto.
Qed.

Lemma release_seq_implies_hbUrf lab sb rf mo a b:
  release_seq lab sb rf mo a b →
  clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Proof.
  induction 1; vauto.
    by apply rt_step; vauto.
  by eapply rt_trans, rt_step; vauto.
Qed.

Lemma hb_implies_hbUrf lab sb rf mo a b:
  happens_before lab sb rf mo a b → happens_before_union_rf sb rf a b.
Proof.
  ins; induction H; eauto with hb.
  red in H; desf; vauto.
  red in H; desf.
  × eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H1; desf; vauto.
    eapply happens_before_union_rf_trans; vauto.
  × apply clos_refl_transE in H1; eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H2; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
  × apply clos_refl_transE in H1; eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H2; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
  × apply clos_refl_transE in H1; apply clos_refl_transE in H2;
    eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H3; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
Qed.

Lemma helper_perm_filter_post :
  ∀ e T,
    ∃ posts_sb posts_rf,
      Permutation T (filter (fun x : hbcase ⇒ (hb_fst x != e) || (x == hb_sink e)) T ++
                     map (hb_sb e) posts_sb ++
                     map (hb_rf e) posts_rf).
Proof.
  induction T as [|hb T']; ins; desc.
     by ∃ nil, nil.
  case eqP; ins; subst; [|eby do 2 eexists; eapply Permutation_cons].
  destruct hb; ins.
  × ∃ (e' :: posts_sb), posts_rf; simpl.
    by apply Permutation_cons_app.
  × ∃ posts_sb, (e' :: posts_rf); simpl.
    by rewrite <- appA in *; apply Permutation_cons_app.
  × desf; [∃ posts_sb, posts_rf | done].
    by rewrite <- app_comm_cons; apply Permutation_cons.
Qed.

Lemma helper_filter_decide_sink: ∀ a T (ND: NoDup T),
      Permutation (filter (fun x : hbcase ⇒ (hb_fst x != a) || (x == hb_sink a)) T)
        (if excluded_middle_informative (In (hb_sink a) T)
          then hb_sink a :: (filter (fun x : hbcase ⇒ hb_fst x != a) T)
          else (filter (fun x : hbcase ⇒ hb_fst x != a) T)).
    Proof.
      ins; induction T as [ | edge T']; simpls; desf; apply nodup_cons in ND; desf;
      solve [
        eapply (Permutation_cons eq_refl) in IHT'; ins; eapply perm_trans; eauto; apply perm_swap
        |
        apply perm_skip; apply IHT'; done
        |
        destruct n; right; done
        |
        destruct n; left; done
        |
        destruct Heq; left; done
        |
        destruct Heq; right; done
        |
        apply IHT'; done
      ].
    Qed.

Lemma has_rf_succs acts lab sb rf mo (a: actid) :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ (rfs: list actid),
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf x = Some a >>.
Proof.
  ∃ (undup (filter (fun x ⇒ mydec (rf x = Some a)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=Vbase.nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H, H0; desf.
  by generalize (CLOlab x), (H0 x); rewrite H1 in *; destruct (lab x); ins; desf; vauto; eapply H.
Qed.

Lemma has_rf_pres acts lab sb rf mo a :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ rfs,
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf a = Some x >>.
Proof.
  ∃ (undup (filter (fun x ⇒ mydec (rf a = Some x)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=Vbase.nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H, H0; desf.
  by generalize (CLOlab x), (H0 a); rewrite H1 in *; destruct (lab x); ins; desf; vauto; eapply H.
Qed.

Definition wf_ltof A (f : A → nat) :
  well_founded (fun x y ⇒ f x < f y).
Proof.
  by apply Wf_nat.well_founded_lt_compat with f; intros x y; case ltP.
Qed.

Lemma In_implies_perm A (x : A) l (IN: In x l) :
  ∃ l', Permutation l (x :: l').
Proof.
  induction l; ins; desf; eauto.
  destruct IHl; eauto using Permutation.
Qed.

Lemma Permutation_count A l l' (P : Permutation (A:=A) l l') f :
  count f l = count f l'.
Proof.
  induction P; ins; desf; congruence.
Qed.

Lemma count_eq_0: ∀ A f (lst: list A), count f lst = 0 ↔ ∀ x (IN: In x lst), ¬ f x.
Proof.
  split; ins.
  × intro.
    apply In_implies_perm in IN; desf.
    apply Permutation_count with (f := f) in IN.
    rewrite IN in H.
    rewrite <- (app_nil_l l') , <- app_cons, count_app in H.
    by simpls; desf.
  × induction lst as [ | h tl]; simpls; desf.
    by exfalso; exploit (H h); vauto.
    by apply IHtl; ins; apply H; vauto.
Qed.

Lemma Permutation_hmap_valids PS PSg :
  ∀ l l' (P : Permutation l l') lab sb rf hmap,
    @hmap_valids PS PSg lab sb rf hmap l →
    hmap_valids lab sb rf hmap l'.
Proof.
  unfold hmap_valids; ins; desf.
  eexists; split.
  eby eexists.
  by red; ins; apply VLD, Permutation_in with (l := l'); [eapply Permutation_sym | ].
Qed.

Lemma Permutation_hmap_valids_strong PS PSg:
  ∀ l l' (P : Permutation l l') lab sb rf hmap,
    @hmap_valids_strong PS PSg lab sb rf hmap l →
    hmap_valids_strong lab sb rf hmap l'.
Proof.
  red; ins; split; red; red in H; desf; ins.
    eby eapply Permutation_hmap_valids.
  apply (RESTR e); try done.
  eby intro; destruct NIN; eapply Permutation_in.
  desf; [left | right; split]; try done.
  intro SB; destruct H0.
  eby unfold is_sb_out in *; split; desf; eapply Permutation_in.
Qed.

Lemma Permutation_hist_closed :
  ∀ l l' (P : Permutation l l') sb rf,
    hist_closed sb rf l →
    hist_closed sb rf l'.
Proof.
  red; ins; eapply H in HB.
    by apply (Permutation_in _ P) in HB.
  by eapply Permutation_in, IN; eauto using Permutation_sym.
Qed.

Lemma Consistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : Consistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    Consistent acts' lab sb rf mo sc mt.
Proof.
  unfold Consistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

Lemma weakConsistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

Lemma weakConsistent_Permutation :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: Permutation acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins.
    by apply (Permutation_in _ EQ), CLOlab.
  by apply CLOsb in H; desf; split; apply (Permutation_in _ EQ).
Qed.

Lemma Permutation_flatten A l l' (P : Permutation l l') :
  Permutation (A:=A) (flatten l) (flatten l').
Proof.
  induction P; ins; rewrite ?flatten_cons, <- ?appA;
  eauto using Permutation, Permutation_app, Permutation_app_comm.
Qed.

Lemma AcyclicStrong_implies_IrreflexiveHBuRF:
  ∀ lab sb rf mo, AcyclicStrong lab sb rf mo → IrreflexiveHBuRF sb rf.
Proof.
  ins.
  do 2 red; ins.
  eapply H; instantiate (1 := x).
  red in H0.
  revert H0; generalize x at 1 3; intros y H0.
  induction H0; eauto using clos_trans.
  destruct H0; eauto using t_step with hb.
Qed.

Hint Resolve AcyclicStrong_implies_IrreflexiveHBuRF.

Definition is_pred A (rel : A → A → Prop) B a :=
  has (fun b ⇒ mydec (clos_refl_trans A rel a b)) B.

Definition depth_metric A (rel: A → A → Prop) V a :=
  count (is_pred rel a) V.

Lemma clos_transK T (rel: relation T) x y :
  clos_trans _ (clos_trans _ rel) x y →
  clos_trans _ rel x y.
Proof. induction 1; eauto using clos_trans. Qed.

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b → a = b ∨ clos_trans T rel a b.
Proof. induction 1; desf; eauto using clos_trans. Qed.

Lemma depth_lt (rel : relation actid) V A B
  (HB : ∀ a, In a A → ¬ In a B →
        ∃ b, In b B ∧ rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: ∀ a, In a A → ¬ clos_trans _ rel b a)
  (SUB: ∀ b, In b B → In b V) :
  depth_metric rel V A < depth_metric rel V B.
Proof.
  unfold depth_metric; ins.
  assert (IMP: ∀ x, is_pred rel A x → is_pred rel B x).
    clear -HB; unfold is_pred, mydec; ins; desf.
    apply/@hasP'; apply/@hasP' in H; destruct H; desf.
    destruct (inP x0 B); [by ∃ x0; ins; desf|].
    eapply HB in H; desf; eexists _; split; try edone; desf.
    by exfalso; eauto using rt_trans, rt_step.
  assert (P1: is_pred rel B b).
    unfold is_pred, mydec; desf.
    eapply In_split in IN; desf.
    rewrite has_app; ins; desf; clarsimp.
    by destruct n; vauto.
  assert (P2: is_pred rel A b = false).
    clear -NHB NIN; apply/hasP'; unfold mydec; intro; desf; eauto.
    by apply clos_refl_transD in c; unfold not in *; desf; eauto.
  assert (IN' : In b V) by eauto.
  eapply In_split in IN'; desf; rewrite !count_app; ins.
  ins; rewrite P1, P2, addnS, ltnS.
  eauto using len_add, count_implies.
Qed.

Lemma edge_depth_ind lab sb rf V
  (ACYCLIC: IrreflexiveHBuRF sb rf)
  (HC: hist_closed sb rf V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge' (EV : edge_valid lab sb rf edge')
            (LT: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)),
      P edge')
    (EV : edge_valid lab sb rf edge)
    (IN : In (hb_fst edge) V),
    P edge) →
  ∀ edge (EV : edge_valid lab sb rf edge), In (hb_fst edge) V → P edge.
Proof.
  intros until edge.
  generalize (S (depth_metric (happens_before_union_rf sb rf) V (hb_fst edge :: nil))),
             (ltnSn (depth_metric (happens_before_union_rf sb rf) V (hb_fst edge :: nil))).
  intro n'.
  revert edge; induction n'; ins.
  eapply H; ins; eapply IHn'; ins; eauto.
  2: by clear -HC LT H1; induction LT; unfold imm_happens_before in *; desf;
        eauto with hb.
  eapply ltn_len_trans, H0.
  eapply depth_lt; ins; desf; eauto; instantiate; rewrite addn0 in *;
    intro; desf; [rewrite H2 in *|]; eauto using t_step, t_trans, clos_trans_hbUrfE.
Qed.

Fixpoint find_max A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f curr ≤ f x then find_max x f xs else find_max curr f xs
  end.

Lemma find_max_range :
  ∀ A (curr: A) f l,
    In (find_max curr f l) (curr :: l).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_max_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f x ≤ f (find_max curr f l).
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

Lemma get_deepest :
  ∀ sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
         V (HC: hist_closed sb rf V)
         T (NNIL: T ≠ nil)
         (INCL: ∀ edge (IN: In edge T), In (hb_fst edge) V),
  ∃ edge,
    << IN: In edge T >> ∧
    << INe: In (hb_fst edge) V >> ∧
    << DEEP: ∀ edge' (IN': In edge' T)
                 (HB': happens_before_union_rf sb rf (hb_fst edge) (hb_fst edge')),
               False >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (happens_before_union_rf sb rf) V (hb_fst x :: nil)).

  assert (IN:= find_max_range h f T).
  eexists _; split; unfold NW; repeat split; eauto; ins.
  assert (D := find_max_greatest f IN'); ins.
  specialize (INCL _ IN'); clear IN IN'; subst f.
  erewrite lenE, depth_lt in D; ins; desf; try intro; desf.
    by ∃ (hb_fst edge'); split; vauto.
    by left; reflexivity.
    by rewrite H in *; eauto using t_step.
    by eauto using t_step, t_trans, clos_trans_hbUrfE.
Qed.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f x ≤ f curr then find_min x f xs else find_min curr f xs
  end.

Lemma find_min_range :
  ∀ A (curr: A) f l,
    In (find_min curr f l) (curr :: l).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_min_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f (find_min curr f l) ≤ f x.
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

Lemma get_shallow :
  ∀ lab sb rf mo (ACYCLIC: AcyclicStrong lab sb rf mo)
         V (HC: hist_closed sb rf V)
         T (HC': hist_closed sb rf (V ++ T)) (NNIL: T ≠ nil),
  ∃ e,
    << IN: In e T >> ∧
    << HC: hist_closed sb rf (e :: V) >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (hc_edge sb rf) (V ++ a :: T) (x :: nil)).

  assert (IN:= find_min_range a f T).

  eexists; split; unfold NW; repeat split; eauto; ins.
  red; ins; destruct IN0; eauto; subst.
  generalize HB; eapply HC' in HB; eauto.
  2: by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
  rewrite In_app in HB; destruct HB as [|H]; vauto; intro.
  eapply find_min_greatest with (f:=f) in H.
  exfalso; clear IN.
  rewrite lenE in H; apply/negP in H; destruct H.
  eapply depth_lt; eauto using In_eq; ins; desf.
    by destruct HB; eauto using hc_edge with hb .
    by intro; desf; destruct HB; desf; eauto 8 with hb.
    intro H.
    assert (X: clos_trans actid (hc_edge sb rf) a0 a0) by eauto using clos_trans.
    apply (ACYCLIC a0); revert X; clear;
    generalize a0 at 1 3; induction 1; eauto using clos_trans;
    by destruct H; desf; auto with hb.
  assert (IN:= find_min_range a f T).
  by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
Qed.

Lemma no_normals_on_rf PS PSg :
  ∀ lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap ga a)
    hfr gr (MAP: hmap (hb_rf a b) = Hdef hfr gr) l (ALL: hfr l ≠ @HVnone PS PSg)
    (NORMAL: HVlabeled (hfr l) HLnormal),
  False.
Proof.
  ins; red in VALID; desf; try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      red in TRAN; desf.
      generalize (hplus_def_inv _ _ TRAN); intro D; desf.
      rewrite D, D0 in ×.
      symmetry in D; eapply hsum_preserves_label in D; desf; eauto.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      symmetry in TRAN; eapply hplus_preserves_label in TRAN; desf; eauto.
      clear - TRAN4 TRAN TRAN3.
      specialize (TRAN3 l); destruct (hf0 l); desf; red in TRAN3; desf; ins; desf; red in TRAN4; desf.
    }
  }

  {
    desf; ins; desf.
    exploit (@exact_label_hplus_dist_inv _ _ (hrel' +!+ ht) rfg); try eassumption.
      eby rewrite hplusA, <- rOutEQ; eapply hplus_not_undef_r.
      by apply hplus_eq_gheap in ghostEQ; desf; vauto.
    rewrite hplusA, <- rOutEQ; intro L.
    apply exact_label_hplus_dist in L; desf.
    apply exact_label_hsum_dist with (h := Hdef hfr gr) in L.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOutOK.
    rewrite <- label_exact_hdef in L.
    specialize (L l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

Lemma no_normals_on_rf2 PS PSg :
  ∀ lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap ga b)
    hfr gr (MAP: hmap (hb_rf a b) = Hdef hfr gr) l (ALL: hfr l ≠ @HVnone PS PSg)
    (NORMAL: HVlabeled (hfr l) HLnormal),
  False.
Proof.
  ins; red in VALID; desf; try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      apply exact_label_hsum_dist with (h := Hdef hfr gr) in TRAN.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      red in TRAN; desf.
      clear - TRAN3 ALL NORMAL.
      specialize (TRAN3 l); destruct (hf0 l); ins; try congruence;
        by desf; desf; red in NORMAL; desf.
    }
  }

  {
    desf; ins; desf.
    rewrite <- rInEQ in TRANin.
    apply exact_label_hsum_dist with (h := Hdef hfr gr) in TRANin.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsInOK.
    rewrite <- label_exact_hdef in TRANin.
    specialize (TRANin l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

Lemma triangles_never_on_rf PS PSg:
∀ edge lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (ALL: hf l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge ∨ is_sink edge.
Proof.
  ins; apply NNPP; intro.
  apply not_or_and in H.
  destruct edge; ins; desf.
  ins; red in VALID; desf; try (by specialize (CONS_RF e'); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      red in TRAN; desf.
      generalize (hplus_def_inv _ _ TRAN); intro D; desf.
      rewrite D, D0 in ×.
      symmetry in D; eapply hsum_preserves_label in D; desf; eauto.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      symmetry in TRAN; eapply hplus_preserves_label in TRAN; desf; eauto.
      clear - TRAN4 TRAN TRAN3.
      specialize (TRAN3 l); destruct (hf1 l); desf; red in TRAN3; desf; ins; desf; red in TRAN4; desf.
    }
  }
  
  {
    desf; ins; desf.
    exploit (@exact_label_hplus_dist_inv _ _ (hrel' +!+ ht) rfg); try eassumption.
      eby rewrite hplusA, <- rOutEQ; eapply hplus_not_undef_r.
      by apply hplus_eq_gheap in ghostEQ; desf; vauto.
    rewrite hplusA, <- rOutEQ; intro L.
    apply exact_label_hplus_dist in L; desf.
    apply exact_label_hsum_dist with (h := Hdef hf g) in L.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOutOK.
    rewrite <- label_exact_hdef in L.
    specialize (L l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

Lemma triangles_never_on_rf2 PS PSg:
∀ edge lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap
    (VALID: ∃ b, hb_snd edge = Some b ∧ hmap_valid lab sb rf hmap ga b)
    hf g (MAP: hmap edge = Hdef hf g) l (ALL: hf l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge.
Proof.
  ins; desf.
  apply NNPP; intro RF.
  destruct edge; ins; desf.
  ins; red in VALID0; desf; try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      apply exact_label_hsum_dist with (h := Hdef hf g) in TRAN.
        2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      rewrite <- label_exact_hdef in TRAN.
      specialize (TRAN l).
      exploit label_is_consistent_with_exact_label; eauto; ins.
    }
  }
  
  {
    desf; ins; desf.
    rewrite <- rInEQ in TRANin.
    apply exact_label_hsum_dist with (h := Hdef hf g) in TRANin.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsInOK.
    rewrite <- label_exact_hdef in TRANin.
    specialize (TRANin l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

Lemma FenceInDEF PS PSg:
  ∀ hmap pre post e hF hrel hrel' hacq hacq' gnew
    (DEF: hmap (hb_sb e post) ≠ @Hundef PS PSg)
    (pEQ: hmap (hb_sb pre e) = hF +!+ hrel +!+ hacq)
    (qEQ: hmap (hb_sb e post) = hF +!+ hrel' +!+ hacq' +!+ gheap _ _ gnew)
    (RELsim: Hsim hrel hrel')
    (ACQsim: Hsim hacq hacq'),
  ∃ hf g, hmap (hb_sb pre e) = Hdef hf g.
Proof.
  ins; rewrite <- hdef_alt; rewrite pEQ, qEQ in ×.
  rewrite hplusAC; eapply hplus_sim_def.
    eby apply Hsim_sym.
  rewrite <- hplusA, hplusC; eapply hplus_sim_def.
    eby apply Hsim_sym.
  rewrite hplusAC, <- hplusA, hplusC, <- hplusA.
  by intro U; rewrite <- !hplusA, U, hplus_undef_l in DEF.
Qed.

Lemma RMWinDEF PS PSg:
  ∀ hmap pre e post rfsIn rfsOut l hrel hrel' hacq hacq' ht hF P QQ v' sbg rfg
    (DEF: hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfsOut))
          +!+ hmap (hb_sink e) ≠ @Hundef PS PSg)
    (pEQ: hmap (hb_sb pre e) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                +!+ hrel +!+ hF )
    (qEQ: hmap (hb_sb e post) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                +!+ hacq' +!+ hF +!+ sbg)
    (rInEQ: hsum (map hmap (map (hb_rf^~ e) rfsIn)) = hacq +!+ ht)
    (rOutEQ: hsum (map hmap (map (hb_rf e) rfsOut)) +!+ hmap (hb_sink e) = hrel' +!+ ht +!+ rfg)
    (RELsim: Hsim hrel hrel') (ACQsim: Hsim hacq hacq'),
  ∃ hf g, hmap (hb_sb pre e) +!+ hsum (map hmap (map (hb_rf^~ e) rfsIn)) = Hdef hf g.
Proof.
  ins; rewrite <- hdef_alt.
  rewrite qEQ, rOutEQ, !hplusA, !(hplusAC sbg), (hplusC _ rfg), !(hplusAC rfg) in DEF.
  do 2 apply hplus_not_undef_r in DEF.
  rewrite pEQ, rInEQ.
  rewrite hplusC in DEF.
  rewrite !hplusA, hplusC.
  eapply hplus_sim_def; eauto.
  rewrite !(hplusAC hacq), (hplusAC _ hrel).
  apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in *).
    by apply Hsim_sym.
  apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in *).
    by apply Hsim_refl; intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in ×.
  apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in *).
    by apply Hsim_sym.
  by apply Hsim_refl; intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in ×.
Qed.

Ltac RMWin_def := exploit RMWinDEF; try eassumption; rewrite <- hdef_alt; intro DEFin; [].

Ltac RMWin_heap := exploit RMWinDEF; try eassumption; intro DEFin; desc; [].

Lemma valid_accessD PS PSg:
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Aa : is_access (lab a)),
  ∃ pre hf g,
    sb pre a ∧ hmap (hb_sb pre a) = Hdef hf g
    ∧ hf (loc (lab a)) ≠ @HVnone PS PSg ∧ HVlabeled (hf (loc (lab a))) HLnormal.
Proof.
  ins.
  red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    red in IV; desf; desf.
    by eexists _, _, _; repeat split; eauto; ins; instantiate; rewrite Heq0.
  }

  {
    symmetry in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; eauto; rewrite ? hupds; ins.
      eexists _, _, _; repeat split; eauto; ins.
      by intro N; rewrite N in ×.
      eby apply Rlabel_implies_label.
    vauto.
  }

  {
    eexists _, _, _; repeat split; eauto; ins.
    by intro N; rewrite N in ×.
  }

  {
    symmetry in UPD; eapply hplus_ra_lD in UPD; desf.
      3: eby rewrite hupds.
    × apply initialize_eq_raD in UPD; desf.
      eexists _, _, _; repeat split; eauto; ins; try congruence.
      rewrite UPD; ins; desf; vauto.
    × apply initialize_eq_raD in UPD; desf.
      eexists _, _, _; repeat split; eauto; ins; try congruence.
      rewrite UPD; ins; desf; unfold is_normal; tauto.
  }

  {
    RMWin_def.
    apply hplus_not_undef_l, hdef_alt in DEFin; ins; desf.
    rewrite DEFin in ×.
    repeat eexists; eauto.
    by eapply hplus_preserves_alloc_l in pEQ; rewrite ?hupds.
    by eapply hplus_preserves_label in pEQ; rewrite ?hupds; ins; desf; vauto.
  }
Qed.

Lemma valid_na_accessD PS PSg :
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (NA : is_na (lab a)) pre
         (SB : sb pre a) hf g
         (HM : hmap (hb_sb pre a) = @Hdef PS PSg hf g),
  is_nonatomic (hf (loc (lab a))).
Proof.
  unfold hmap_valid, unique; ins; desf; desf; ins; apply pU0 in SB; desf;
  rewrite pEQ in HM; desf; eauto.
Qed.

Lemma valid_readD PS PSg :
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Ra : is_read (lab a)),
  ∃ pre hf g,
    sb pre a ∧ hmap (hb_sb pre a) = @Hdef PS PSg hf g
    ∧ HVlabeledR (hf (loc (lab a))) HLnormal.
Proof.
  ins.
  red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    eexists _, _, _; repeat split; eauto; ins.
    red; desf; ins; desf.
  }

  {
    eexists _, _, _; repeat split; eauto; ins.
    symmetry in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; eauto.
    rewrite hupds; ins.
    vauto.
  }
  
  {
    RMWin_def.
    apply hplus_not_undef_l, hdef_alt in DEFin; ins; desf.
    rewrite DEFin in ×.
    repeat eexists; eauto.
    by eapply hplus_preserves_Rlabel in pEQ; rewrite ?hupds; ins; desf; vauto.
  }
Qed.

Lemma valid_writeD PS PSg :
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Wa : is_write (lab a)),
  ∃ pre hf g,
    sb pre a ∧ hmap (hb_sb pre a) = @Hdef PS PSg hf g ∧
    (is_lvalue (hf (loc (lab a))) ∨ is_atomic (hf (loc (lab a)))).
Proof.
  ins; red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    eexists _, _, _; repeat split; eauto; ins.
  }

  {
    eexists _, _, _; repeat split; eauto; ins.
    right; clear - UPD.
    apply initialize_is_atomic with (l := l).
    eapply hplus_has_atomic_l.
      eby symmetry in UPD.
    by ins; desf; rewrite hupds.
  }
  
  {
    RMWin_def.
    apply hplus_not_undef_l, hdef_alt in DEFin; ins; desf.
    rewrite DEFin in ×.
    repeat eexists; eauto.
    right; clear - pEQ.
    eapply hplus_has_atomic_l.
      eby symmetry in pEQ.
    by ins; desf; rewrite hupds.
  }
Qed.

Lemma hmap_defined_in PS PSg:
  ∀ lab sb rf hmap mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge b (VALID: hmap_valid lab sb rf hmap ga b)
    (EV: edge_valid lab sb rf edge)
    (IN: hb_snd edge = Some b),
  ∃ hf g, hmap edge = @Hdef PS PSg hf g.
Proof.
  ins; red in VALID; red in EV; desf; ins; desc; try destruct DISJ; desc; try clear TYP;
    try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf);
    inv IN; rewrite ?(proj2 pU _ EV) in *;
    try (eby eexists _, _).

  {
    rewrite <- EQ in DEF.
    apply hplus_not_undef_l, hdef_alt in DEF; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply pOK.
  }

 
  {
    RMWin_def.
    by apply hplus_not_undef_l, hdef_alt in DEFin.
  }

  {
    rewrite qEQ, (hplusC _ (gheap _ _ _)), !(hplusAC (gheap _ _ _)) in DEF.
    apply hplus_not_undef_r in DEF.
    rewrite pEQ, <- hdef_alt.
    rewrite hplusC; rewrite hplusC in DEF.
    eapply hplus_sim_def; eauto.
    eapply hplus_sim; solve [by apply Hsim_sym | by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in *].
  }
  
  {
    eby eexists _, _; rewrite rEQ.
  }
  
  {
    red in TRAN; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
  }

  {
    RMWin_def.
    apply hplus_not_undef_r, hdef_alt in DEFin; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsInOK.
  }
Qed.

Lemma hmap_defined_out PS PSg:
  ∀ lab sb rf hmap ga mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge a (VALID: hmap_valid lab sb rf hmap ga a)
    (EV: edge_valid lab sb rf edge)
    (IN: hb_fst edge = a),
  ∃ hf g, hmap edge = @Hdef PS PSg hf g.
Proof.
  ins; red in VALID; red in EV; desf; ins; desc; try destruct DISJ; desc; try clear TYP;
    try (by specialize (CONS_RF e'); desf; rewrite Heq in CONS_RF; desf);
    try (by red in EV; rewrite Heq in EV);
    rewrite ?(proj2 qU _ EV) in *; try (eby desf; eexists _, _); try (by apply hdef_alt).

  {
    clear - DEF qOK EV; apply hplus_not_undef_l, hdef_alt in DEF; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply qOK.
  }

  {
    eby eapply hdef_alt, hplus_not_undef_l.
  }

  {
    eby eapply hdef_alt, hplus_not_undef_l.
  }

  {
    eby eexists _, _; rewrite rEQ.
  }

  {
    red in TRAN; desf.
    apply hplus_def_inv_l in TRAN; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
  }

  {
    rewrite hplusAC, hdef_alt in DEF; desf; apply hplus_def_inv_l in DEF; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
  }

  {
    apply hplus_not_undef_r, hdef_alt in DEF; desf.
  }

  {
    red in TRAN; desf.
    by apply hplus_def_inv_r in TRAN.
  }

  {
    eby rewrite <- hplusA, hdef_alt in DEF; desf; eapply hplus_def_inv_r.
  }
Qed.