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

Set Implicit Arguments.

Definition hbpath := list (hbcase × HeapLabel).

Definition sync_step lab (edge1 edge2 : hbcase × HeapLabel) :=
  << CONN: hb_snd (fst edge1) = Some (hb_fst (fst edge2)) >> ∧
  << STEP: (snd edge1 = HLnormal ∧ is_sb (fst edge1) ∧
           ((snd edge2 = HLnormal ∧ ¬ is_rf (fst edge2)) ∨
            (snd edge2 = HLtriangle ∧ is_sb (fst edge2) ∧ is_release_fence (lab (hb_fst (fst edge2)))) ∨
            (snd edge2 = HLnabla ∧ ¬ is_sb (fst edge2) ∧ is_release_write (lab (hb_fst (fst edge2))))))
           ∨
           (snd edge1 = HLtriangle ∧ is_sb (fst edge1) ∧
           ((snd edge2 = HLtriangle ∧ ¬ is_rf (fst edge2)) ∨
            (snd edge2 = HLnabla ∧ ¬ is_sb (fst edge2) ∧ is_write (lab (hb_fst (fst edge2)))) ∨
            (snd edge2 = HLnabla ∧ is_sink (fst edge2))))
           ∨
           (snd edge1 = HLnabla ∧
           ((snd edge2 = HLnabla ∧ ¬ is_rf (fst edge2)) ∨
            (is_rf (fst edge1) ∧ snd edge2 = HLnormal ∧ ¬ is_rf (fst edge2)
                                 ∧ is_acquire_read (lab (hb_fst (fst edge2)))) ∨
            (is_sb (fst edge1) ∧ snd edge2 = HLnormal ∧ is_sb (fst edge2)
                                 ∧ is_acquire_fence (lab (hb_fst (fst edge2)))) ∨
            (is_rf (fst edge1) ∧ snd edge2 = HLnabla ∧ ¬ is_sb (fst edge2)
                                 ∧ is_rmw (lab (hb_fst (fst edge2)))))) >>.

Definition hbpath_wf lab sb rf (path: hbpath) :=
  << SYNC: ∀ path1 path2 edge1 edge2 (DECOMP: path = path1 ++ edge1 :: edge2 :: path2),
             sync_step lab edge1 edge2 >> ∧
  << EVP : ∀ edge (IN: In edge path), edge_valid lab sb rf (fst edge) >>.

Lemma hbpath_wf_nil lab sb rf : hbpath_wf lab sb rf nil.
Proof.
  red; split; red; ins.
  symmetry in DECOMP; apply app_eq_nil in DECOMP; desf.
Qed.

Lemma hbpath_wf_one lab sb rf :
  ∀ edge, edge_valid lab sb rf (fst edge) → hbpath_wf lab sb rf (edge :: nil).
Proof.
  ins; split.
  × red; ins; exfalso.
    apply f_equal with (f := (@length _)) in DECOMP.
    rewrite app_length in DECOMP; ins.
    omega.
  × red; ins; desf.
Qed.

Lemma hbpath_wf_app lab sb rf:
  ∀ path1 path2,
    hbpath_wf lab sb rf (path1 ++ path2) → hbpath_wf lab sb rf path1 ∧ hbpath_wf lab sb rf path2.
Proof.
  ins; split; split; red; ins; try (by apply (proj2 H); find_in_list).
  eby subst; rewrite <- app_assoc, <- !app_comm_cons in H; eapply (proj1 H).
  eby subst; rewrite app_assoc in H; eapply H.
Qed.

Lemma hbpath_wf_app_l lab sb rf :
  ∀ path1 path2, hbpath_wf lab sb rf (path1 ++ path2) → hbpath_wf lab sb rf path1.
Proof.
  ins; apply hbpath_wf_app in H; desf.
Qed.

Lemma hbpath_wf_app_r lab sb rf :
  ∀ path1 path2, hbpath_wf lab sb rf (path1 ++ path2) → hbpath_wf lab sb rf path2.
Proof.
  ins; apply hbpath_wf_app in H; desf.
Qed.

Lemma hbpath_wf_cons lab sb rf:
  ∀ edge path, hbpath_wf lab sb rf (edge :: path) → hbpath_wf lab sb rf path.
Proof.
  ins.
  rewrite <- (app_nil_l path), <- app_cons in H.
  apply hbpath_wf_app in H; desf.
Qed.

Lemma extend_path_right :
  ∀ lab sb rf path (WFP: hbpath_wf lab sb rf path)
    edge (LAST: olast path = Some edge) edge' (VALID: edge_valid lab sb rf (fst edge'))
    (SYNC: sync_step lab edge edge'),
  hbpath_wf lab sb rf (path ++ edge' :: nil).
Proof.
  ins.
  apply olast_inv in LAST; desf.
  split; [ | by red; ins; rewrite In_app in IN; desf; ins; desf; apply (proj2 WFP)].
  red; ins.
  des_list_tail path2 path2' edgeX.
  × rewrite <- (app_nil_l (edge2 :: nil)), app_comm_cons, app_assoc in DECOMP.
    apply app_inj_tail in DECOMP; desf.
    apply app_inj_tail in DECOMP; desf.
  × rewrite <- (app_nil_l (edgeX :: nil)), !app_comm_cons, !app_assoc in DECOMP.
    apply app_inj_tail in DECOMP; desf.
    rewrite DECOMP, app_nil_r in WFP.
    eby eapply (proj1 WFP).
Qed.

Lemma extend_path_left :
  ∀ lab sb rf path (WFP: hbpath_wf lab sb rf path)
    edge (FIRST: ohead path = Some edge) edge' (VALID: edge_valid lab sb rf (fst edge'))
    (SYNC: sync_step lab edge' edge),
  hbpath_wf lab sb rf (edge' :: path).
Proof.
  ins.
  destruct path as [ | edge1 path']; ins.
  split; [ | red; ins; desf; apply (proj2 WFP); find_in_list].
  red; ins.
  destruct path1 as [ | edgeX path'']; ins; desf.
  eby rewrite H0 in WFP; eapply WFP.
Qed.

Lemma sink_is_always_last lab sb rf:
  ∀ path edge (WF: hbpath_wf lab sb rf (path ++ edge :: nil)),
    ¬ ∃ edge', In edge' path ∧ is_sink (fst edge').
Proof.
  ins; intro; desf.
  apply In_split in H; desf.
  destruct l2; [rewrite <- app_assoc, <- app_comm_cons, app_nil_l in WF | apply hbpath_wf_app in WF; desf];
    exploit (proj1 WF l1); ins; eauto; unfold sync_step in *; desc; destruct (fst edge'); ins.
Qed.

Lemma inside_path_normals_are_on_sb_edges :
  ∀ lab sb rf path edgeN (WFP: hbpath_wf lab sb rf (path ++ edgeN :: nil))
    edge (IN: In edge path) (LAB: snd edge = HLnormal),
  is_sb (fst edge).
Proof.
  ins.
  cut (∃ edge', sync_step lab edge edge').
    by unfold sync_step; ins; desf; try congruence.
  apply In_split in IN; desf.
  destruct l2.
  × rewrite <- app_assoc, <- app_comm_cons, app_nil_l in WFP.
    eby eexists; eapply (proj1 WFP).
  × apply hbpath_wf_app_l in WFP.
    eby eexists; eapply (proj1 WFP).
Qed.

Lemma inside_path_triangles_are_on_sb_edges :
  ∀ lab sb rf path edgeN (WFP: hbpath_wf lab sb rf (path ++ edgeN :: nil))
    edge (IN: In edge path) (LAB: snd edge = HLtriangle),
  is_sb (fst edge).
Proof.
  ins.
  cut (∃ edge', sync_step lab edge edge').
    by unfold sync_step; ins; desf; try congruence.
  apply In_split in IN; desf.
  destruct l2.
  × rewrite <- app_assoc, <- app_comm_cons, app_nil_l in WFP.
    eby eexists; eapply (proj1 WFP).
  × apply hbpath_wf_app_l in WFP.
    eby eexists; eapply (proj1 WFP).
Qed.

Lemma structure_of_nonnormal_path:
  ∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
    path (PV: hbpath_wf lab sb rf path)
    (LAB: ∀ edge (IN: In edge path), snd edge ≠ HLnormal),
  ∃ path1 path2, << DECOMP: path = path1 ++ path2 >> ∧
    << LAB1: ∀ edge (IN: In edge path1), snd edge = HLtriangle >> ∧
    << LAB2: ∀ edge (IN: In edge path2), snd edge = HLnabla >>.
Proof.
  induction path as [ | edge1 path']; ins.
    by ∃ nil, nil; unnw; repeat split; ins.
  exploit IHpath'; eauto; ins; clear IHpath'; desf.
    eby eapply hbpath_wf_cons.

  case_eq (snd edge1) as LABedge1.
    by exfalso; apply (LAB edge1); eauto.

  {
    ∃ (edge1 :: path1), path2; unnw; repeat split; ins; desf.
    eby eapply LAB1.
  }

  {
    ∃ nil, (edge1 :: path1 ++ path2); unnw; repeat split; ins; desf.
    rewrite In_app in IN; desf.
      2: eby eapply LAB2.
    exfalso.
    destruct path1 as [ | edge2 path1']; ins; clear IN.
    specialize (LAB1 _ (or_introl eq_refl)).
    exploit (proj1 PV nil); ins; eauto.
    red in x0; desf; congruence.
  }
Qed.

Lemma structure_of_nabla_path:
  ∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
    path (PV: hbpath_wf lab sb rf path) (SINK: ∀ edge (IN: In edge path), ¬ is_sink (fst edge))
    (LAB: ∀ edge (IN: In edge path), snd edge = HLnabla),
  ∃ pathRF pathSB,
    << DECOMP: path = pathRF ++ pathSB >> ∧
    << SB: ∀ edge (IN: In edge pathSB), is_sb (fst edge) >> ∧
    << RF: ∀ edge (IN: In edge pathRF), is_rf (fst edge) >>.
Proof.
  induction path as [ | edge1 path'].
    by ins; ∃ nil, nil; unnw; ins.
  ins.
  exploit (IHpath' (hbpath_wf_cons PV)).
    by ins; eapply SINK; eauto.
    by ins; eapply LAB; eauto.
  ins; desf.
  exploit (LAB edge1); ins; eauto; desf.

  case_eq (fst edge1) as E1.

  {
    cut (pathRF = nil).
    { ins; subst.
      ∃ nil; ins; eexists; repeat split; eauto.
      red; ins; desf.
      by rewrite E1.
      by apply SB.
    }
    destruct pathRF as [ | edgeRF pathRF']; ins; exfalso.
    exploit (RF edgeRF); ins; eauto.
    exploit (proj1 PV nil); ins; eauto.
    red in x2; desf; try congruence.
    by apply (SINK edgeRF); eauto; destruct (fst edgeRF).
    by rewrite E1 in STEP0.
  }

  {
    rewrite app_comm_cons; eexists _, _; repeat split; eauto.
    red; ins; desf.
    by rewrite E1.
    by apply RF.
  }
  
  
  by exfalso; eapply SINK; eauto; instantiate; rewrite E1.
Qed.

Lemma structure_of_normal_to_normal_transition:
  ∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
    path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
    (NORMALfst: snd edge1 = HLnormal) (NORMALlst: snd edgeN = HLnormal)
    (MID: ∀ edge (IN: In edge path), snd edge ≠ HLnormal),
    path = nil ∨
    ∃ pathTRIANGLE edgeRF pathRMW pathNABLA,
      << DECOMP: path = pathTRIANGLE ++ edgeRF :: pathRMW ++ pathNABLA >> ∧
      << TRIANGLE: ∀ edge (IN: In edge pathTRIANGLE), snd edge = HLtriangle >> ∧
      << NABLA: ∀ edge (IN: In edge (edgeRF :: pathRMW ++ pathNABLA)), snd edge = HLnabla >> ∧
      << SB: ∀ edge (IN: In edge (pathTRIANGLE ++ pathNABLA)), is_sb (fst edge) >> ∧
      << RF: ∀ edge (IN: In edge (edgeRF :: pathRMW)), is_rf (fst edge) >> ∧
      << RMW: ∀ edge (IN: In edge pathRMW), is_rmw (lab (hb_fst (fst edge))) >>.
Proof.
  ins.
  exploit (structure_of_nonnormal_path ACYCLIC CONS_RF (hbpath_wf_app_l _ _ (hbpath_wf_cons WFP))); try done.

  ins; desf.

  destruct (classic (path1 ++ path2 = nil)) as [N|N]; [by left | right].

  assert (∃ edgeRF path2', << P2: path2 = edgeRF :: path2' >> ∧ << RFE: is_rf (fst edgeRF) >>).
  {
    destruct path2 as [ | edgeRF path2'].
    {
      exfalso.
      rewrite <- app_assoc in *; ins.
      des_list_tail path1 path1' edgeX; ins.
      rewrite <- app_assoc in *; ins.
      exploit (proj1 WFP (edge1 :: path1')); ins; eauto.
      red in x0; desf; try congruence; exploit (LAB1 edgeX); try find_in_list; ins; congruence.
    }

    {
      eexists _, _; split; eauto; unfold NW.
      assert (SINK: ¬ is_sink (fst edgeRF)).
      {
        rewrite <- (app_nil_l (_ :: nil)), app_comm_cons, app_assoc in WFP.
        apply sink_is_always_last in WFP.
        intro S; destruct WFP.
        eexists; split; eauto; find_in_list.
      }
      des_list_tail path1 path1' edgeX; ins.
      × exploit (proj1 WFP nil); ins; eauto.
        red in x0; desf; try congruence; try (exploit (LAB2 edgeRF); eauto; ins; congruence).
        by destruct (fst edgeRF); ins.
      × rewrite <- !app_assoc, !app_cons in *; ins.
        exploit (proj1 WFP (edge1 :: path1')); ins; eauto.
        red in x0; desf; try congruence;
          try (exploit (LAB2 edgeRF); eauto; ins; congruence);
          try (by destruct (fst edgeRF); ins).
        exploit (LAB1 edgeX); try find_in_list; ins; congruence.
    }
  }
  desf.

  exploit (structure_of_nabla_path ACYCLIC CONS_RF
             (hbpath_wf_cons (hbpath_wf_app_r _ _ (hbpath_wf_app_l _ _ (hbpath_wf_cons WFP))))).
  { ins.
    rewrite <- (app_nil_l (_ :: nil)), app_comm_cons, app_assoc in WFP.
    apply sink_is_always_last in WFP.
    intro SINK; destruct WFP.
    eexists; split; eauto; find_in_list.
  }
    by ins; apply (LAB2 edge); find_in_list.

  ins; desf.

  assert (RMW: ∀ edge (IN: In edge pathRF), is_rmw (lab (hb_fst (fst edge)))).
  {
    ins.
    apply hbpath_wf_cons, hbpath_wf_app_l, hbpath_wf_app_r in WFP.
    rewrite app_comm_cons in WFP.
    apply hbpath_wf_app_l in WFP.
    exploit (LAB2 edgeRF); eauto; []; intro rfLABEL.
    apply In_split in IN; desf.
    exploit (RF edge); try find_in_list; []; intro RFedge.
    des_list_tail l1 path edgeX; ins.
    × exploit (proj1 WFP nil); ins; eauto.
      red in x0; desf; try congruence.
      by destruct (fst edgeRF).
    × rewrite <- app_assoc in WFP; ins.
      exploit (LAB2 edgeX); eauto; try find_in_list; []; intro LABELx.
      exploit (proj1 WFP (edgeRF :: path)); ins; eauto.
      red in x0; desf; try congruence.
      exploit (RF edgeX); try find_in_list.
      by ins; destruct (fst edgeX).
  }

  ∃ path1, edgeRF, pathRF, pathSB; repeat split; red; ins.
  × rewrite In_app in IN; desf; try by apply SB.
    exploit (LAB1 edge); try find_in_list; []; intro edgeTRIANLGE.
    rewrite app_comm_cons in WFP.
    apply In_split in IN; desf.
    eapply inside_path_triangles_are_on_sb_edges; eauto.
    find_in_list.
  × by desf; apply RF.
Qed.

Lemma sb_from_path:
  ∀ lab sb rf path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
    (pSB: ∀ edge (IN: In edge path), is_sb (fst edge)),
  ∀ a (SND: hb_snd (fst edge1) = Some a), clos_refl_trans _ sb a (hb_fst (fst edgeN)).
Proof.
  induction path as [ | edge path]; ins.
  × exploit ((proj1 WFP) nil); ins; eauto.
    red in x0; desc; vauto.
  × exploit ((proj2 WFP) edge); ins; eauto.
    exploit (pSB edge); eauto; ins.
    case_eq (fst edge) as E; ins.
    exploit ((proj1 WFP) nil); ins; eauto.
    red in x2; desc; clear STEP.
    apply hbpath_wf_cons in WFP.
    exploit IHpath; try eassumption.
      by eauto.
      by rewrite E.
    desf; ins; eapply rt_trans; try eassumption.
    rewrite E; vauto.
Qed.

Lemma release_seq_from_path:
  ∀ lab sb rf mo w r path edgeN lbl
    (PV: hbpath_wf lab sb rf ((hb_rf w r, lbl) :: path ++ edgeN :: nil))
    (RMWr: is_rmw (lab r))
    (RMWn: is_rmw (lab (hb_fst (fst edgeN))))
    (PATH: ∀ edge (IN: In edge path), << RMW: is_rmw (lab (hb_fst (fst edge))) >> ∧
                                           << RF: is_rf (fst edge) >>),
  release_seq lab sb rf mo w (hb_fst (fst edgeN)).
Proof.
  induction path using (well_founded_induction (well_founded_ltof _ (@length _))).
  rename H into IH.
  des_list_tail path path' edgeX; ins.

  {
    exploit (proj1 PV nil); ins; desf.
    red in x0; desc; clear STEP; ins; desf.
    exploit (proj2 PV ((hb_rf w (hb_fst (fst edgeN))), lbl)); ins; eauto.
    eapply RS_rmw; eauto.
    by apply RS_refl.
  }

  {
    rewrite <- app_assoc in PV; ins.
    exploit (proj1 PV ((hb_rf w r, lbl) :: path')); ins.
    red in x0; desc; clear STEP.
    exploit (proj2 PV edgeX); ins; try find_in_list.
    exploit (PATH edgeX); ins; try find_in_list; desf.
    red in RF; desf; ins; desf.
    eapply RS_rmw; eauto.
    rewrite <- (app_nil_l (_ :: nil)), !app_comm_cons, app_assoc in PV.
    apply hbpath_wf_app_l in PV; ins.
    apply IH in PV; ins.
    by rewrite Heq in ×.
    by red; rewrite length_app; ins; omega.
    by apply PATH; find_in_list.
    by apply PATH; find_in_list.
  }
Qed.

Lemma hb_from_path_simple:
  ∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
    path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
    (NORMALfst: snd edge1 = HLnormal) (NORMALlst: snd edgeN = HLnormal)
    (MID: ∀ edge (IN: In edge path), snd edge ≠ HLnormal),
  ∀ b (SND: hb_snd (fst edge1) = Some b),
    clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst (fst edgeN)).
Proof.
  ins; exploit structure_of_normal_to_normal_transition; eauto; ins; desf; ins.

  {
    exploit (proj1 WFP nil); ins; eauto.
    red in x0; desc; clear STEP; desf.
    by apply rt_refl.
  }
    
    
  apply rt_step, t_step; right.
  rewrite <- app_assoc, <- app_comm_cons, <- app_assoc in WFP.

  exploit (proj2 WFP edgeRF); try find_in_list; []; intro READ.
  exploit (RF edgeRF); eauto; []; destruct edgeRF as [eRF lbl]; destruct eRF as [w r | w r | w]; ins; desf.

  des_list_tail pathRMW pathRMW' lastRF; ins.
  {
    assert (endSBseq: clos_refl_trans actid sb r (hb_fst (fst edgeN))).     {
      eapply sb_from_path; ins.       by apply hbpath_wf_cons, hbpath_wf_app_r in WFP; exact WFP.
      by apply SB; find_in_list.
      done.
    }
    destruct pathTRIANGLE as [ | edge2 pT]; ins.     {
      exploit (proj1 WFP nil); ins; eauto.
      red in x1; desf; try congruence.
      des_list_tail pathNABLA pN edgeX; ins.       {
        exploit (proj1 WFP (edge1 :: nil)); ins; eauto.
        red in x1; desf; try congruence.
        left.         ins; desf.
        repeat split; try done.
        ∃ b; split; vauto.
      }
      {
        rewrite <- app_assoc in WFP; ins.
        exploit (NABLA edgeX); try find_in_list; []; intro NABLAx.
        exploit (SB edgeX); try find_in_list; []; intro SBx.
        exploit (proj1 WFP (edge1 :: (hb_rf b r, lbl) :: pN)); ins; eauto.
        red in x1; desf; try congruence; try by destruct (fst edgeX).
        right; left.         ins; desf.
        repeat split; try done.
        eexists _, _; repeat split; try eassumption.
        by apply RS_refl.
      }
    }
    {
      exploit (TRIANGLE edge2); try find_in_list; []; intro TRIANGLE2.
      exploit (SB edge2); try find_in_list; []; intro SB2.
      assert (startSBseq: clos_refl_trans actid sb (hb_fst (fst edge2)) w).
      {
        exploit sb_from_path; ins.
        by rewrite <- (app_nil_l (_ ++ _ :: nil)), !app_comm_cons, app_assoc in WFP;
           apply hbpath_wf_app_l in WFP; rewrite <- app_comm_cons in WFP; exact WFP.
        by apply SB; ins; desf; find_in_list.
        by eapply (proj1 WFP nil); ins.
        done.
      }
      exploit (proj1 WFP nil); ins; eauto.
      red in x1; desf; try congruence.
      des_list_tail pathNABLA pN edgeX; ins.       {
        exploit (proj1 WFP (edge1 :: edge2 :: pT)); ins; eauto.
        red in x1; desf; try congruence.
        right; right; left.         ins; desf.
        repeat split; try done.
        eexists _, _; repeat split; try eassumption.
        by apply RS_refl.
      }
      {
        rewrite <- app_assoc in WFP; ins.
        exploit (NABLA edgeX); try find_in_list; []; intro NABLAx.
        exploit (SB edgeX); try find_in_list; []; intro SBx.
        exploit (proj1 WFP (edge1 :: edge2 :: pT ++ (hb_rf w r, lbl) :: pN)); ins.
          by rewrite <- app_assoc; ins.
        red in x1; desf; try congruence; try by destruct (fst edgeX).
        repeat right.         ins; desf.
        repeat split; try done.
        eexists _, _, _; repeat split; try eassumption.
        by apply RS_refl.
      }
    }
  }

  {
    rewrite <- app_assoc in WFP; ins.
    exploit (NABLA lastRF); try find_in_list; []; intro NABLArf'.
    exploit (RF lastRF); try find_in_list; [].
    exploit (proj2 WFP lastRF); try find_in_list; []; intro READ'.
    destruct lastRF as [lRF lbl']; destruct lRF as [w' r' | w' r' | w']; ins.
    assert (RELSEQ: release_seq lab sb rf mo w w').
    {
      apply hbpath_wf_cons, hbpath_wf_app_r in WFP.
      exploit release_seq_from_path.
      × rewrite <- (app_nil_l (_ ++ _ :: nil)), !app_comm_cons, app_assoc in WFP.
        apply hbpath_wf_app_l in WFP; ins.
        exact WFP.
      × destruct pathRMW' as [ | edgeX pathRMW']; ins.
        + exploit (proj1 WFP nil); ins; desf.
          exploit (RMW (hb_rf w' r', HLnabla)); ins; eauto.
          red in x2; desc; clear STEP; ins; desf.
        + exploit (proj1 WFP nil); ins; desf.
          exploit (RMW edgeX); ins; eauto.
          red in x2; desc; clear STEP; ins; desf.
      × apply RMW; find_in_list.
      × ins; split; [apply RMW | apply RF]; find_in_list.
      × eby ins.
    }
    
    assert (endSBseq: clos_refl_trans actid sb r' (hb_fst (fst edgeN))).     {
      eapply sb_from_path; ins.       do 2 apply hbpath_wf_cons, hbpath_wf_app_r in WFP; exact WFP.
      by apply SB; find_in_list.
      done.
    }
    destruct pathTRIANGLE as [ | edge2 pT]; ins.     {
      exploit (proj1 WFP nil); ins; eauto.
      red in x2; desf; try congruence.
      des_list_tail pathNABLA pN edgeX; ins.       {
        exploit (proj1 WFP (edge1 :: (hb_rf b r, lbl) :: pathRMW')); ins; eauto.
        red in x2; desf; try congruence.
        left.         ins; desf.
        repeat split; try done.
        eby eexists.
      }
      {
        rewrite <- app_assoc in WFP; ins.
        exploit (NABLA edgeX); try find_in_list; []; intro NABLAx.
        exploit (SB edgeX); try find_in_list; []; intro SBx.
        exploit (proj1 WFP (edge1 :: (hb_rf b r, lbl) :: pathRMW' ++ (hb_rf w' r', HLnabla) :: pN)); ins.
          by rewrite <- app_assoc; ins.
        red in x2; desf; try congruence; try by destruct (fst edgeX).
        right; left.         ins; desf.
        repeat split; try done.
        eexists _, _; repeat split; eassumption.
      }
    }
    {
      exploit (TRIANGLE edge2); try find_in_list; []; intro TRIANGLE2.
      exploit (SB edge2); try find_in_list; []; intro SB2.
      assert (startSBseq: clos_refl_trans actid sb (hb_fst (fst edge2)) w).
      {
        exploit sb_from_path; ins.
          by rewrite <- (app_nil_l (_ ++ _ :: _ ++ _ :: nil)), !app_comm_cons, app_assoc in WFP;
             apply hbpath_wf_app_l in WFP; rewrite <- app_comm_cons in WFP; exact WFP.
          by apply SB; ins; desf; find_in_list.
          by eapply (proj1 WFP nil); ins.
          done.
      }
      exploit (proj1 WFP nil); ins; eauto.
      red in x2; desf; try congruence.
      des_list_tail pathNABLA pN edgeX; ins.       {
        exploit (proj1 WFP (edge1 :: edge2 :: pT ++ (hb_rf w r, lbl) :: pathRMW')); ins.
          by rewrite <- app_assoc; ins.
        red in x2; desf; try congruence.
        right; right; left.         ins; desf.
        repeat split; try done.
        eexists _, _; repeat split; eassumption.
      }
      {
        rewrite <- app_assoc in WFP; ins.
        exploit (NABLA edgeX); try find_in_list; []; intro NABLAx.
        exploit (SB edgeX); try find_in_list; []; intro SBx.
        exploit (proj1 WFP (edge1 :: edge2 :: pT ++ (hb_rf w r, lbl) :: pathRMW'
                                                 ++ (hb_rf w' r', HLnabla) :: pN)); ins.
          by do 2 (rewrite <- !app_assoc; ins).
        red in x2; desf; try congruence; try by destruct (fst edgeX).
        repeat right.         ins; desf.
        repeat split; try done.
        eexists _, _, _; repeat split; eassumption.
      }
    }
  }
Qed.

Lemma hb_from_path:
  ∀ lab sb rf mo (ACYCLIC: IrreflexiveHBuRF sb rf) (CONS_RF: ConsistentRF_basic lab sb rf mo)
    path edge1 edgeN (WFP: hbpath_wf lab sb rf (edge1 :: path ++ edgeN :: nil))
    (NORMALfst: snd edge1 = HLnormal) (NORMALlst: snd edgeN = HLnormal),
  ∀ b (SND1: hb_snd (fst edge1) = Some b),
    clos_refl_trans _ (happens_before lab sb rf mo) b (hb_fst (fst edgeN)).
Proof.
  induction path using (well_founded_induction (well_founded_ltof _ (@length _))).
  rename H into IH.

  destruct path as [ | edge2 path']; ins.

  {
    exploit ((proj1 WFP) nil nil edge1 edgeN); ins; desf.
    red in x0; desc; clear STEP; desf; apply rt_refl.
  }


  exploit ((proj1 WFP) nil); ins.
  red in x0; desc; clear STEP.

  assert (C: ∃ c, hb_snd (fst edge2) = Some c).
  {
    clear - WFP.
    apply hbpath_wf_cons in WFP.
    destruct path'; ins; exploit (proj1 WFP nil); ins; red in x0; desc; clear STEP; eauto.
  }
  desf.

  destruct (classic (snd edge2 = HLnormal)).

  {
    apply rt_trans with (y := c).
    × apply rt_step, t_step; left.
      rewrite !app_comm_cons in WFP.
      exploit inside_path_normals_are_on_sb_edges; eauto; try find_in_list.
      intro SB; red in SB; desf; ins; desf.
      exploit (proj2 WFP edge2); try find_in_list.
      by rewrite Heq; ins.
    × eapply (IH path'); try (eby eapply hbpath_wf_cons); eauto; try edone; ins.
  }

  {
    exploit (first_exists (path' ++ edgeN :: nil) (fun edge ⇒ snd edge = HLnormal)).
      by ∃ edgeN; intuition.
    intro EX; desf.
    rename a' into edgei; rename l1 into path1.
    des_list_tail l2 path2 edgeN'.
    × clear IH.
      apply app_inj_tail in EX; desf.
      rewrite app_comm_cons in WFP.
      exploit (hb_from_path_simple ACYCLIC CONS_RF); eauto; ins; desf.
      by apply EX1.
    × rewrite EX in ×.
      rewrite !app_comm_cons, !app_assoc in EX.
      apply app_inj_tail in EX; desf.
      exploit (proj2 WFP edgei); try find_in_list.
      intro EVi.
      case_eq (fst edgei) as I; ins; desf.
      Focus 2.         exfalso.
        exploit inside_path_normals_are_on_sb_edges; try exact EX0.
          by rewrite !app_comm_cons, app_assoc in WFP; exact WFP.
          by find_in_list.
        by rewrite I; ins.
      Focus 2.         exfalso; destruct edgei; ins; desf; clear - WFP.
        do 2 apply hbpath_wf_cons in WFP.
        by destruct path2; ins; exploit (proj1 WFP path1); ins; red in x0; desc.
      apply rt_trans with (y := e').
      apply rt_trans with (y := e).
      + rewrite <- (app_nil_l path2), !app_comm_cons, !app_assoc in WFP.
        do 2 apply hbpath_wf_app_l in WFP.
        rewrite <- app_comm_cons in WFP.
        assert (E: e = (hb_fst (fst edgei))) by (by rewrite I); rewrite E.
        eapply (hb_from_path_simple _ _ _ edgei (edge1 := edge1)); eauto.
        by ins; desf; apply EX1.
      + apply rt_step, t_step; vauto.
      + do 2 apply hbpath_wf_cons in WFP; apply hbpath_wf_app_r in WFP.
        eapply (IH _ _ _ _ WFP); eauto.
        by rewrite I.
  }

  Grab Existential Variables. all: try done.
  by red; ins; rewrite length_app; ins; omega.
Qed.

Definition hbpath_connects lab sb rf path a b :=
  << EMPTY: path = nil ∧ a = b >> ∨
  << WFP: hbpath_wf lab sb rf path >> ∧
  ∃ alpha omega, << HEAD: ohead path = some alpha >> ∧ << ALPHA: hb_fst (fst alpha) = a >> ∧
                      << TAIL: olast path = some omega >> ∧ << OMEGA: hb_snd (fst omega) = Some b >>.

Lemma connects_implies_wf:
  ∀ lab sb rf path a b, hbpath_connects lab sb rf path a b → hbpath_wf lab sb rf path.
Proof.
  ins; red in H; desf.
  by apply hbpath_wf_nil.
Qed.

Lemma hbpath_connects_app1:
  ∀ lab sb rf path1 path2 edge a b
    (CONNECT: hbpath_connects lab sb rf (path1 ++ edge :: path2) a b),
  hbpath_connects lab sb rf path1 a (hb_fst (fst edge)).
Proof.
  unfold hbpath_connects; ins; desf.
    by exploit app_cons_not_nil; eauto.
  destruct path1; ins; desf; eauto.
  right; split.
    eby rewrite app_comm_cons in WFP; eapply hbpath_wf_app_l.
  ∃ alpha.
  des_list_tail path1 path edge'; ins.
  × ∃ alpha; repeat split.
    eby eapply (proj1 WFP nil).
  × rewrite !app_comm_cons, <- !app_assoc in *; ins.
    ∃ edge'; repeat split.
    by rewrite last_app.
    eby apply hbpath_wf_cons in WFP; eapply (proj1 WFP).
Qed.

Lemma hbpath_connects_app2:
  ∀ lab sb rf path1 path2 edge a b
    (CONNECT: hbpath_connects lab sb rf (path1 ++ edge :: path2) a b),
  hbpath_connects lab sb rf (edge :: path2) (hb_fst (fst edge)) b.
Proof.
  ins; red.
  right; split.
    by apply connects_implies_wf, hbpath_wf_app in CONNECT; desc.
  red in CONNECT; ins; desf.
    by exploit app_cons_not_nil; eauto; ins.
  eexists _, _; repeat split; eauto.
  destruct path1; ins; desf.
  by rewrite last_app in OMEGA.
Qed.

Lemma hbpath_connects_cons:
  ∀ lab sb rf edge1 edge2 path a b
    (CONNECT: hbpath_connects lab sb rf (edge1 :: edge2 :: path) a b),
  hbpath_connects lab sb rf (edge2 :: path) (hb_fst (fst edge2)) b.
Proof.
  eby ins; rewrite <- (app_nil_l (_ :: path)), app_comm_cons in CONNECT; eapply hbpath_connects_app2.
Qed.

Lemma connects_implies_no_sink:
  ∀ lab sb rf path a b,
    hbpath_connects lab sb rf path a b → ∀ edge (IN: In edge path), ¬ is_sink (fst edge).
Proof.
  ins.
  red in H; desf.
  apply olast_inv in TAIL; desf.
  rewrite In_app in IN; desf.
  by intro; eapply sink_is_always_last; eauto.
  by ins; desf; unfold is_sink; desf.
Qed.

Lemma connect_implies_hbUrf:
  ∀ lab sb rf path a b (CONNECT: hbpath_connects lab sb rf path a b),
  clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Proof.
  induction path as [ | edge path]; ins.
    by red in CONNECT; desf; vauto.
  red in CONNECT; ins; desf.
  exploit (proj2 WFP alpha); ins; eauto.
  destruct path as [ | edge' path]; ins.
  × apply rt_step, t_step.
    destruct (fst alpha); ins; desf; vauto.
  × apply rt_trans with (y := (hb_fst (fst edge'))).
    + exploit (proj1 WFP nil); ins; eauto.
      red in x1; desc; clear STEP.
      apply rt_step, t_step.
      destruct (fst alpha); ins; desf; vauto.
    + apply IHpath.
      red; ins.
      right; split.
        eby eapply hbpath_wf_cons.
      eexists _, _; repeat split; eauto.
Qed.

Lemma connect_implies_hbUrf_strong:
  ∀ lab sb rf path a b (CONNECT: hbpath_connects lab sb rf path a b),
  path ≠ nil → happens_before_union_rf sb rf a b.
Proof.
  ins.
  destruct path as [ | edge path]; desf.
  exploit (proj2 (connects_implies_wf CONNECT) edge); ins; try find_in_list.
  assert (¬ is_sink (fst edge)).
    by intro; destruct edge; ins; exploit connects_implies_no_sink; eauto; find_in_list.
  destruct path as [ | edge' path]; desf.
    by red in CONNECT; ins; desf; destruct (fst alpha); ins; vauto.
  exploit (proj1 (connects_implies_wf CONNECT) nil); ins; eauto.
  assert (a = hb_fst (fst edge)).
    by red in CONNECT; ins; desf.
  red in x1; desc; clear STEP.
  eapply hbpath_connects_cons, connect_implies_hbUrf, clos_refl_transE in CONNECT; desf.
    by destruct (fst edge); ins; vauto.
  apply clos_trans_hbUrfE in CONNECT.
  eapply t_trans; eauto.
  by destruct (fst edge); ins; vauto.
Qed.

Lemma hist_closed_connect:
  ∀ lab sb rf path a b V
    (CONNECT: hbpath_connects lab sb rf path a b)
    (HC: hist_closed sb rf V) (IN: In b V),
  In a V.
Proof.
  ins.
  apply connect_implies_hbUrf, clos_refl_trans_hbUrfE in CONNECT; desf.
  eby eapply hist_closedD.
Qed.

Lemma path_is_too_long :
  ∀ acts lab sb rf mo path a b
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONNECT: hbpath_connects lab sb rf path a b)
    (LEN: length path = length acts + 1),
  False.
Proof.
  ins.
  assert (∃ path1 edge1 path2 edge2 path3,
                 << DECOMP: path = path1 ++ edge1 :: path2 ++ edge2 :: path3 >> ∧
                 << EQ: hb_fst (fst edge1) = hb_fst (fst edge2) >>).
  {
    remember (map hb_fst (map (@fst _ _) path)) as nodes.
    assert (SUBSET: ∀ e (IN: In e nodes), In e acts).
    {
      subst nodes; ins.
      repeat (rewrite In_map in *; desf).
      exploit (proj2 (connects_implies_wf CONNECT) x0); ins.
      assert (¬ is_sink (fst x0)) by (eby eapply connects_implies_no_sink).
      destruct (fst x0); ins.
      by exploit (proj2 FIN); eauto; ins; desf.
      by specialize (CONS_RF e'); desf; desf; apply (proj1 FIN); intro S; rewrite S in ×.
    }
    exploit (not_NoDup_split (l := nodes)).
      eapply too_long_implies_not_NoDup; eauto.
      by subst nodes; rewrite !length_map, LEN; rewrite Plus.plus_comm.
    intro DECOMP; desf.
    apply map_eq_app in DECOMP; desf.
    apply map_eq_app in DECOMP; desf.
    apply map_eq_cons in DECOMP1; desf.
    apply map_eq_cons in DECOMP1; desf.
    apply map_eq_app in DECOMP2; desf.
    apply map_eq_app in DECOMP2; desf.
    apply map_eq_cons in DECOMP1; desf.
    apply map_eq_cons in DECOMP1; desf.
    repeat eexists.
    by symmetry.
  }
  desf.
  apply hbpath_connects_app2 in CONNECT.
  rewrite app_comm_cons in CONNECT; apply hbpath_connects_app1 in CONNECT.
  apply connect_implies_hbUrf_strong in CONNECT; ins.
  eby rewrite EQ in CONNECT; eapply ACYCLIC.
Qed.

Definition tracking_path PS PSg hmap (path : hbpath) l :=
 ∀ edge (IN: In edge path) hf g (MAP: hmap (fst edge) = Hdef hf g),
   << ALL: hf l ≠ @HVnone PS PSg >> ∧ << LAB: HVlabeled (hf l) (snd edge) >>.