Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslmodel fslassnlemmas.
Require Import fslhmap path step stepback ihc memsafe.
Require Import fslhmapa fslhmapna.
Require Import permission.
Require Import Omega.

Set Implicit Arguments.

Lemma connection_to_lvalue_forward_helper PS PSg:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b2 ≠ b1) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 g1 hf2 g2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1 g1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2 g2)
    l (ALLOCATED: hf1 l ≠ @HVnone PS PSg) (LBL: HVlabeled (hf1 l) HLnormal) (LVAL: is_lvalue (hf2 l))
    (DIRECTION: clos_refl_trans _ (happens_before_union_rf sb rf) b1 a2),
  ∀ n, ∃ path c,
    << CONNECT: hbpath_connects lab sb rf ((hb_sb a1 b1, HLnormal) :: path) a1 c >> ∧
    << HBuRF: clos_refl_trans _ (happens_before_union_rf sb rf) c a2 >> ∧
    << TRACK: tracking_path hmap path l >> ∧
    << LEN: c = a2 ∨ length path = n >>.
Proof.
  induction n.
  {
    ∃ nil, b1.
    repeat split; ins; eauto.
    right; split.
    by apply hbpath_wf_one.
    by eexists _, _; repeat split.
  }

  
  red in VALID; desc.
  desf; [by ∃ path, a2; repeat (split; try done); eauto | ].
  exploit extend_tracking_path_right; try exact CONNECT; eauto; try done.
    eby apply VLD; apply clos_refl_trans_hbUrfE in HBuRF; desf; eapply hist_closedD.
    by red; ins; desf; ins; eauto; rewrite MAP in MAP1; desf.
  ins; desf.
  destruct (classic (fst edge = hb_sb a2 b2)).
  × ∃ path, a2; repeat (split; try done); try by vauto.
    right; split.
      eby eapply connects_implies_wf.
    des_list_tail path path' edgeX; ins; eexists _, _; repeat split; ins.
    + exploit (proj1 WFP nil); ins.
      red in x0; desc; clear STEP; ins.
      by rewrite H in CONN.
    + rewrite last_app; ins.
      exploit (proj1 WFP ((hb_sb a1 b1, HLnormal) :: path')).
        by rewrite <- app_assoc.
      intro S; red in S; desc; clear STEP.
      by rewrite H in CONN.
  × ∃ (path ++ edge :: nil).
    assert (C: hb_fst (fst edge) = c).
    {
      des_list_tail path path' edgeX; ins.
      × exploit (proj1 WFP nil); ins.
        red in x0; desc; clear STEP; ins; desf.
        red in CONNECT; desf; ins; desf; ins; desf.
      × exploit (proj1 WFP ((hb_sb a1 b1, HLnormal) :: path')).
          by rewrite <- app_assoc.
        intro S; red in S; desc; clear STEP.
        red in CONNECT; desf; ins; desf.
        rewrite last_app in OMEGA; ins; desf.
    }
    assert (DEP: ¬ independent sb rf ((fst edge) :: hb_sb a2 b2 :: nil)).
    {
      exploit (hmap_defined_out (hmap := hmap) (ga := ga) CONS_RF (fst edge)); try exact C.
        eby apply VLD; apply clos_refl_trans_hbUrfE in HBuRF; desf; eapply hist_closedD.
        by apply (proj2 WFP); find_in_list.
      ins; desf.
      eapply not_independent_two; try eassumption; eauto.
      by eexists; split; eauto.
      eby apply clos_refl_trans_hbUrfE in HBuRF; desf; eapply hist_closedD.
      by apply (proj2 WFP); find_in_list.
      by eapply (TRACK0 edge); find_in_list.
      by intro N; rewrite N in LVAL.
    }
    eapply destruct_not_independent_two in DEP; eauto.
      2: by apply (proj2 WFP); find_in_list.
    desf; ins.
    + ∃ b0; repeat apply conj; try done.
      - right; split; try done.
        eexists _, _; repeat split; eauto.
        by rewrite last_app.
      - red; red; ins; eapply TRACK0; ins; eauto.
      - right; rewrite length_app; ins; omega.
    + exfalso; desf.
      clear - ACYCLIC DEP0 HBuRF EV2; eapply ACYCLIC.
      apply clos_refl_trans_hbUrfE in DEP0; apply clos_refl_trans_hbUrfE in HBuRF; desf;
        try by vauto; repeat (eapply t_trans; vauto).
Qed.

Lemma connection_to_lvalue_backwards_helper PS PSg:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 g1 hf2 g2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1 g1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2 g2)
    l (LVAL: is_lvalue (hf1 l)) (ALLOCATED: hf2 l ≠ @HVnone PS PSg) (LBL: HVlabeled (hf2 l) HLnormal)
    (DIRECTION: clos_refl_trans _ (happens_before_union_rf sb rf) b1 a2),
  ∀ n, ∃ path c,
    << CONNECT: hbpath_connects lab sb rf (path ++ (hb_sb a2 b2, HLnormal) :: nil) c b2 >> ∧
    << HBuRF: clos_refl_trans _ (happens_before_union_rf sb rf) b1 c >> ∧
    << TRACK: tracking_path hmap path l >> ∧
    << LEN: c = b1 ∨ length path = n >>.
Proof.
  induction n.
  {
    ∃ nil, a2.
    repeat split; ins; eauto.
    right; split.
    by apply hbpath_wf_one.
    by eexists _, _; repeat split.
  }

  
  desf; [by ∃ path, b1; repeat (split; try done); eauto | ].
  assert (NALLOC: lab c ≠ Aalloc l).
  {
    apply is_lvalue_implies_normal in LVAL; desf.
    exploit alloc_always_before; try exact LVAL; eauto; ins; desf.
    intro C; exploit CONS_A.
      by exact ALLOC.
      by exact C.
    ins; desf.
    apply clos_refl_trans_hbE in HB; desf; try apply hb_implies_hbUrf in HB; eapply ACYCLIC;
      apply clos_refl_trans_hbUrfE in HBuRF; desf; try by vauto; repeat (eapply t_trans; vauto).
  }
  red in VALID; desc.
  exploit extend_tracking_path_left; try exact CONNECT; eauto; try done.
    by destruct path.
    eby apply hbpath_connects_app1 in CONNECT; ins; eapply VLD, hist_closed_connect.
    by red; ins; rewrite In_app in IN; desf; eauto; ins; desf; ins; rewrite MAP in MAP2; desf.
  ins; desf.
  destruct (classic (fst edge = hb_sb a1 b1)).
  × ∃ path, b1; repeat (split; try by vauto).
    cut (c = b1); [ by ins; desf | ].
    apply hbpath_connects_app1 in CONNECT.
    destruct edge; ins; desf.
    destruct path as [ | edge1 path']; ins.
    + red in CONNECT; desf.
      exploit (proj1 WFP nil); ins.
      red in x0; desc; clear STEP; ins; desf.
    + exploit (proj1 WFP nil); ins.
      red in x0; desc; clear STEP; ins; desf.
      red in CONNECT; desf; ins; desf.
  × assert (CON: hbpath_connects lab sb rf
                 ((edge :: path) ++ (hb_sb a2 b2, HLnormal) :: nil) (hb_fst (fst edge)) b2).
    {
      right; split; try done.
      eexists _, _; repeat split; ins.
      by rewrite last_app.
    }
    ∃ (edge :: path), (hb_fst (fst edge)); repeat (apply conj).
    + by rewrite <- app_comm_cons.
    + assert (DEP: ¬ independent sb rf (hb_sb a1 b1 :: fst edge :: nil)).
      {
        apply hbpath_connects_app1 in CON.
        exploit (hmap_defined_out (hmap := hmap) (ga := ga) CONS_RF (fst edge)); try by apply eq_refl.
          eby eapply VLD, hist_closed_connect.
          by apply (proj2 WFP); find_in_list.
        ins; desf.
        eapply not_independent_two; try eassumption; eauto.
        by eexists; split; eauto.
        eby eapply hist_closed_connect.
        by apply (proj2 WFP); find_in_list.
        by intro N; rewrite N in LVAL.
        by eapply (TRACK0 edge); find_in_list.
      }
      eapply destruct_not_independent_two in DEP; eauto.
        2: by apply (proj2 WFP); find_in_list.
      desf; ins; desf.
      exfalso.
      assert (b0 = c).
      {
        clear - DEP CONNECT WFP.
        destruct path as [ | edge' path']; ins;
          red in CONNECT; desf; ins; desf; ins;
          exploit (proj1 WFP nil); ins;
          red in x0; desc; clear STEP; desf.
      }
      desf.
      clear - ACYCLIC HBuRF DEP0 EV1; eapply ACYCLIC.
      apply clos_refl_trans_hbUrfE in DEP0; apply clos_refl_trans_hbUrfE in HBuRF; desf;
        try by vauto; repeat (eapply t_trans; vauto).
    + red; red; ins; desf; eapply TRACK0; try done; find_in_list.
    + eauto.
Qed.

Lemma lvalue_before_path PS PSg:
  ∀ acts lab sb rf mo hmap
    (FIN: ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    V (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a b (IN: In a V)
    path (CONNECT: hbpath_connects lab sb rf path a b)
    l (TRACK: tracking_path hmap path l)
    edge (EV: edge_valid lab sb rf edge) (SND: hb_snd edge = Some a)
    hf g (MAP: hmap edge = @Hdef PS PSg hf g) (LVAL: is_lvalue (hf l)),
  hbpath_connects lab sb rf ((edge, HLnormal) :: path) (hb_fst edge) b ∧
  tracking_path hmap ((edge, HLnormal) :: path) l.
Proof.
  ins.
  assert (VALID' := VALID).
  red in VALID'; desc.

  assert (SB: is_sb edge).
  {
    destruct edge; ins; desf.
    eapply no_normals_on_rf; eauto.
    by eapply VLD, HC; vauto.
    by intro N; rewrite N in LVAL.
  }

  split.

  Focus 2.
    red; ins; desf; [ | eby eapply TRACK]; ins.
    rewrite MAP in *; desf.
    by apply is_lvalue_implies_normal in LVAL; desf.

  right; ins; split.

  Focus 2.
    repeat eexists.
    red in CONNECT; desf.
    apply olast_inv in TAIL; desf.
    by rewrite last_app.

  destruct path as [ | edge1 path'].
    by apply hbpath_wf_one.
  split; [ | by red; ins; desf; eapply (connects_implies_wf CONNECT); find_in_list].
  red; ins.
  destruct path1 as [ | edgeX path'']; ins; desf.
    2: eby rewrite H0 in CONNECT; eapply (connects_implies_wf CONNECT).
  assert (EV2: edge_valid lab sb rf (fst edge2)) by (eapply (connects_implies_wf CONNECT); find_in_list).
  assert (FST: hb_fst (fst edge2) = a) by (red in CONNECT; ins; desf).
  exploit (hmap_defined_out (hmap := hmap) (ga := ga) CONS_RF (fst edge2)); eauto.
  intro MAP2; desf.
  exploit (TRACK edge2); ins; eauto; desf.
  destruct edge2 as [edge2 lbl]; ins.
  destruct lbl.
  { exploit (step_back_from_normal (PS := PS) (PSg := PSg) CONS_RF edge2); eauto.
    unnw; intro DISJ; destruct DISJ as [ALLOC | SYNC].
    × destruct edge; ins; desf.
      specialize (VLD _ IN); red in VLD; rewrite ALLOC in VLD; desc.
      clear qEQ.
      rewrite ((proj2 pU) _ EV) in ×.
      rewrite MAP in pEQ; desf.
      by rewrite NALL in LVAL.
    × desc.
      assert (edge' = edge).
      {
        apply NNPP; intro NEQ; clear SYNC4.
        exploit (independent_heap_compat FIN ACYCLIC CONS_RF CONS_A HC VALID (T := edge :: edge' :: nil));
          try (by ins; desf; ins; desf; eapply HC; vauto).
          by apply NoDup_two; intro; desf.
          by eapply independent_when_sharing_second_node; eauto; unfold actid in *; congruence.
        intro SUM; ins; desf; rewrite hsum_two, MAP, SYNC1, hplus_unfold in SUM; desf; desf.
        specialize (HEAPcompat l).
        exploit hvplusDEF_with_lvalue; ins; eauto.
      }
      subst edge'.
      split; ins; try done.
      left; split; try done.
      by split; eauto.
  }
  { exploit (step_back_from_triangle (PS := PS) (PSg := PSg) CONS_RF edge2); eauto.
    unnw; intro SYNC; desc.
    assert (edge' = edge).
    {
      apply NNPP; intro NEQ; clear SYNC5.
      exploit (independent_heap_compat FIN ACYCLIC CONS_RF CONS_A HC VALID (T := edge :: edge' :: nil));
        try (by ins; desf; ins; desf; eapply HC; vauto).
        by apply NoDup_two; intro; desf.
        by eapply independent_when_sharing_second_node; eauto; unfold actid in *; congruence.
      intro SUM; ins; desf; rewrite hsum_two, MAP, SYNC1, hplus_unfold in SUM; desf; desf.
      specialize (HEAPcompat l).
      exploit hvplusDEF_with_lvalue; ins; eauto.
    }
    subst edge'.
    split; ins; try done.
    left; split; try done.
    split; try done.
    desf; eauto.
    exfalso.
    rewrite MAP in *; desf.
    by red in LVAL; desf; clear - SYNC5; ins; red in WFperm; desf;
       apply nonextendable_full_permission in PSUMdef; pplus_eq_zero.
  }

  { exploit (step_back_from_nabla (PS := PS) (PSg := PSg) CONS_RF edge2); eauto.
    unnw; intro SYNC; desc.
    assert (edge' = edge).
    {
      apply NNPP; intro NEQ; clear SYNC3.
      exploit (independent_heap_compat FIN ACYCLIC CONS_RF CONS_A HC VALID (T := edge :: edge' :: nil));
        try (by ins; desf; ins; desf; eapply HC; vauto).
        by apply NoDup_two; intro; desf.
        by eapply independent_when_sharing_second_node; eauto; unfold actid in *; congruence.
      intro SUM; ins; desf; rewrite hsum_two, MAP, SYNC1, hplus_unfold in SUM; desf; desf.
      specialize (HEAPcompat l).
      exploit hvplusDEF_with_lvalue; ins; eauto.
    }
    subst edge'.
    split; ins; try done.
    left; split; try done.
    split; try done.
    rewrite MAP in SYNC1; inv SYNC1.
    desf; try (by exfalso; red in LVAL; desf; clear - SYNC4; ins; red in WFperm; desf;
                  apply nonextendable_full_permission in PSUMdef; pplus_eq_zero).
    by eauto.
  }
Qed.

Lemma lvalue_after_path PS PSg :
  ∀ acts lab sb rf mo hmap
    (FIN: ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    V (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    hf g (MAP: hmap edge = @Hdef PS PSg hf g) l (LVAL: is_lvalue (hf l))
    a path (CONNECT: hbpath_connects lab sb rf path a (hb_fst edge))
    (TRACK: tracking_path hmap path l)
    b (SND: hb_snd edge = Some b),
  hbpath_connects lab sb rf (path ++ (edge, HLnormal) :: nil) a b ∧
  tracking_path hmap (path ++ (edge, HLnormal) :: nil) l.
Proof.
  ins.
  assert (VALID' := VALID).
  red in VALID'; desc.

  assert (SB: ¬ is_rf edge).
  {
    destruct edge; ins; desf.
    exfalso; eapply no_normals_on_rf; eauto.
    by intro N; rewrite N in LVAL.
  }

  split.

  Focus 2.
    red; ins; rewrite In_app in IN0; desf; [eby eapply TRACK | ]; ins; desf; ins.
    rewrite MAP in *; desf.
    by apply is_lvalue_implies_normal in LVAL; desf.

  right; ins; split.

  Focus 2.
    red in CONNECT; desf; ins.
      by repeat eexists; ins.
    destruct path; ins; desf.
    repeat eexists.
    by rewrite last_app.

  des_list_tail path path' edgeN.
    by apply hbpath_wf_one.
  split; [ | by red; ins; rewrite In_app in IN0; desf; ins; desf; eapply (connects_implies_wf CONNECT)].
  red; ins.
  des_list_tail path2 path'' edgeX; ins.
  Focus 2.
    rewrite !app_comm_cons, app_assoc in DECOMP.
    apply app_inj_tail in DECOMP; desf.
    rewrite DECOMP in CONNECT.
    eby eapply (connects_implies_wf CONNECT).
  rewrite <- (app_nil_l (edge2 :: nil)), app_comm_cons, app_assoc in DECOMP.
  do 2 (apply app_inj_tail in DECOMP; desf).
  assert (EV1: edge_valid lab sb rf (fst edge1)) by (eapply (connects_implies_wf CONNECT); find_in_list).
  assert (SND': hb_snd (fst edge1) = Some (hb_fst edge)).
  {
    red in CONNECT; ins; desf.
      eby exploit app_cons_not_nil; symmetry.
    destruct path1; ins; desf.
    rewrite last_app in *; desf.
  }
  exploit (hmap_defined_in (hmap := hmap) (ga := ga) CONS_RF (fst edge1)); eauto.
  intro MAP1; desf.
  exploit (TRACK edge1); ins; eauto; try find_in_list; desf.
  destruct edge1 as [edge1 lbl]; ins.
  destruct lbl.
  {
    exploit (step_from_normal (PS := PS) (PSg := PSg) CONS_RF edge1); eauto.
    intro SYNC; desc.
    split; ins; eauto 8.
  }
  { exfalso.
    exploit (step_from_triangle (PS := PS) (PSg := PSg) CONS_RF edge1); eauto.
    intro SYNC; desc.
    assert (edge2 = edge).
    {
      apply NNPP; intro NEQ; clear SYNC4.
      exploit (independent_heap_compat FIN ACYCLIC CONS_RF CONS_A HC VALID (T := edge :: edge2 :: nil));
        try (by ins; desf; ins; desf; eapply HC; vauto).
        by apply NoDup_two; intro; desf.
        by eapply independent_when_sharing_first_node; eauto; unfold actid in *; congruence.
      intro SUM; ins; desf; rewrite hsum_two, MAP, SYNC2, hplus_unfold in SUM; desf; desf.
      specialize (HEAPcompat l).
      exploit hvplusDEF_with_lvalue; ins; eauto.
    }
    by subst edge2; rewrite MAP in *; desf;
       clear - LVAL SYNC4;
       red in LVAL; desf; ins; clear Heq;
       red in WFperm; desf;
       apply nonextendable_full_permission in PSUMdef; desf;
       pplus_eq_zero.
  }

  { exploit (step_from_nabla (PS := PS) (PSg := PSg) CONS_RF edge1); eauto.
    intro SYNC; desc.
    assert (edge2 = edge).
    {
      apply NNPP; intro NEQ; clear SYNC3.
      exploit (independent_heap_compat FIN ACYCLIC CONS_RF CONS_A HC VALID (T := edge :: edge2 :: nil));
        try (by ins; desf; ins; desf; eapply HC; vauto).
        by apply NoDup_two; intro; desf.
        by eapply independent_when_sharing_first_node; eauto; unfold actid in *; congruence.
      intro SUM; ins; desf; rewrite hsum_two, MAP, SYNC1, hplus_unfold in SUM; desf; desf.
      specialize (HEAPcompat l).
      exploit hvplusDEF_with_lvalue; ins; eauto.
    }
    subst edge2; rewrite MAP in *; inv SYNC1.
    red; ins; repeat split; try done.
    by desf; eauto 12;
       clear - LVAL SYNC1 SYNC3;
       red in LVAL; desf; ins; clear Heq;
       red in WFperm; desf;
       apply nonextendable_full_permission in PSUMdef; desf;
       pplus_eq_zero.
  }
Qed.

Lemma connection_to_lvalue PS PSg:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 g1 hf2 g2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1 g1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2 g2)
    l (LVAL: is_lvalue (hf1 l)) (ALLOCATED: hf2 l ≠ @HVnone PS PSg) (LBL: HVlabeled (hf2 l) HLnormal),
  ∃ path, hbpath_wf lab sb rf ((hb_sb a1 b1, HLnormal) :: path ++ (hb_sb a2 b2, HLnormal) :: nil) ∨
               hbpath_wf lab sb rf ((hb_sb a2 b2, HLnormal) :: path ++ (hb_sb a1 b1, HLnormal) :: nil) .
Proof.
  ins.
  assert (DEP: ¬ independent sb rf (hb_sb a1 b1 :: hb_sb a2 b2 :: nil)).
  {
    eapply not_independent_two; try eassumption; eauto.
    by intro; desf.
    by intro N; rewrite N in LVAL.
  }
  eapply destruct_not_independent_two in DEP; ins; desf.

  { exploit connection_to_lvalue_backwards_helper; try eassumption.
    intro N; specialize (N DEP0 (length acts + 1)).
    ins; desf.
    { exploit lvalue_before_path; try exact CONNECT; try exact MAP1; eauto; try done.
        eby apply clos_refl_trans_hbUrfE in DEP0; desf; eapply hist_closedD.
        eby red; ins; rewrite In_app in IN; desf; ins; [eapply TRACK | desf; ins; rewrite MAP in *; desf].
      ins; desf.
      eby eexists; left; eapply connects_implies_wf.
    }
    { exfalso; eapply path_is_too_long; try exact LEN; eauto.
      eby eapply hbpath_connects_app1.
    }
  }

  { exploit connection_to_lvalue_forward_helper; try eassumption.
    intro N; specialize (N DEP0 (length acts + 1)).
    ins; desf.
    { exploit lvalue_after_path; try exact MAP1; eauto; try done.
        eby red; ins; desf; ins; [rewrite MAP in *; desf | eapply TRACK].
      ins; desf.
      eby eexists; right; eapply connects_implies_wf.
    }
    { exfalso.
      destruct path.
        by rewrite Plus.plus_comm in LEN.
      eapply path_is_too_long; try exact LEN; eauto.
      eby eapply hbpath_connects_cons.
    }
  }

  Grab Existential Variables. edone.
Qed.

Lemma atomicity_is_exclusive PS PSg (hv: HeapVal PS PSg): is_atomic hv → is_nonatomic hv → False.
Proof.
  by destruct hv.
Qed.

Lemma atomicity_is_globally_exclusive PS PSg:
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge1 (EV1: edge_valid lab sb rf edge1) (IN1: In (hb_fst edge1) V)
    hf1 g1 (MAP1: hmap edge1 = Hdef hf1 g1)
    edge2 (EV2: edge_valid lab sb rf edge2) (IN2: In (hb_fst edge2) V)
    hf2 g2 (MAP2: hmap edge2 = @Hdef PS PSg hf2 g2)
    l (AT: is_atomic (hf1 l)) (NA: is_nonatomic (hf2 l)),
  False.
Proof.
  ins.
  exploit heap_loc_allocated_atomic; try exact AT; try exact MAP1; eauto.
  intro AA; desc. clear AA3.
  exploit heap_loc_allocated_nonatomic; try exact NA; try exact MAP2; eauto.
  intro NAA; desc.
  specialize (CONS_A _ _ NAA0 _ AA0); subst.
  assert (INcpre: In cpre V) by (desf; eapply hist_closedD; eauto).
  clear NAA3.
  red in VALID; desc.
  specialize (VLD _ INcpre); red in VLD; rewrite AA0 in VLD; desc.
  rewrite <- (proj2 qU _ AA), <- (proj2 qU _ NAA) in ×.
  rewrite NAA1 in ×.
  by desf; apply hplus_gheap in qEQ; subst; rewrite hupds in ×.
Qed.

Theorem valid_implies_race_free PS PSg :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: @hmap_valids PS PSg lab sb rf hmap V),
  race_free V lab sb rf mo.
Proof.
  red; ins; assert (VALID' := VALID); red in VALID'; desf.

  × exploit valid_accessD; try exact Ab; eauto.
    intro A; desf.
    exploit valid_writeD; try exact WRI; eauto.
    intro W; desf.
      2: by exfalso; exploit valid_na_accessD; try exact NA; eauto; apply atomicity_is_exclusive.
    rewrite LOC in ×.
    exploit connection_to_lvalue; try eassumption; try solve [apply (HC a); vauto | apply (HC b); vauto].
    intro PATH; desf; exploit hb_from_path; try eassumption; simpl; eauto;
                      intro HB; apply clos_refl_trans_hbE in HB; desf;
                      solve [ by left; eapply t_trans; vauto | by left; vauto |
                              by right; eapply t_trans; vauto | by right; vauto ].
  × exploit valid_accessD; try exact Aa; eauto.
    intro A; desf.
    exploit valid_na_accessD; try exact NA; eauto.
    intro NAa.
    exploit valid_writeD; try exact WRI; eauto.
    intro W; desf; rewrite LOC in ×.
      2: by exfalso; eapply atomicity_is_globally_exclusive; try exact NAa; try exact W1; eauto;
            try done; ins; solve [apply (HC a); vauto | apply (HC b); vauto].
    assert (NEQ': b ≠ a) by (intro; desf); clear NEQ.
    exploit connection_to_lvalue; try eassumption; try solve [apply (HC a); vauto | apply (HC b); vauto].
    intro PATH; desf; exploit hb_from_path; try eassumption; simpl; eauto;
                      intro HB; apply clos_refl_trans_hbE in HB; desf;
                      solve [ by left; eapply t_trans; vauto | by left; vauto |
                              by right; eapply t_trans; vauto | by right; vauto ].
  × exploit valid_accessD; try exact Ab; eauto.
    intro A; desf.
    exploit valid_na_accessD; try exact NA; eauto.
    intro NAb.
    exploit valid_writeD; try exact WRI; eauto.
    intro W; desf; rewrite LOC in ×.
      2: by exfalso; eapply atomicity_is_globally_exclusive; try exact NAb; try exact W1; eauto;
            try done; ins; solve [apply (HC a); vauto | apply (HC b); vauto].
    exploit connection_to_lvalue; try eassumption; try solve [apply (HC a); vauto | apply (HC b); vauto].
    intro PATH; desf; exploit hb_from_path; try eassumption; simpl; eauto;
                      intro HB; apply clos_refl_trans_hbE in HB; desf;
                      solve [ by left; eapply t_trans; vauto | by left; vauto |
                              by right; eapply t_trans; vauto | by right; vauto ].
  × exploit valid_accessD; try exact Aa; eauto.
    intro A; desf.
    exploit valid_writeD; try exact WRI; eauto.
    intro W; desf.
      2: by exfalso; exploit valid_na_accessD; try exact NA; eauto; apply atomicity_is_exclusive.
    rewrite LOC in ×.
    assert (NEQ': b ≠ a) by (intro; desf); clear NEQ.
    exploit connection_to_lvalue; try eassumption; try solve [apply (HC a); vauto | apply (HC b); vauto].
    intro PATH; desf; exploit hb_from_path; try eassumption; simpl; eauto;
                      intro HB; apply clos_refl_trans_hbE in HB; desf;
                      solve [ by left; eapply t_trans; vauto | by left; vauto |
                              by right; eapply t_trans; vauto | by right; vauto ].
Qed.