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.

Set Implicit Arguments.


Lemma step_back_from_normalR PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeledR (hf l) HLnormal),
  << STORE: is_writeL (lab (hb_fst edge)) l >> ∨
  ∃ edge' hf' g', << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
                       << EV': edge_valid lab sb rf edge' >> ∧
                       << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
                       << SB: ¬ is_rf edge >> ∧
                     (<< SB': is_sb edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnormal >> ∨
                      << SB': is_sb edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnabla >> ∧
                                                << ACQ: is_acquire_fence (lab (hb_fst edge)) >> ∨
                      << RF': is_rf edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnabla >> ∧
                                                << ACQ: is_acquire_read (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.

  assert (notRF: ¬ is_rf edge).
  {
    destruct edge; ins.
    exploit no_normals_on_rf; eauto; ins; desf.
      2: eby eapply Rlabel_implies_label.
    by intro N; rewrite N in LAB.
  }


  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e'); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    right.
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    assert (D := hplus_def_inv_l _ _ DEF); desf; rewrite D in ×.
    symmetry in D; eapply hsum_preserves_Rlabel in D; eauto; desfh.
      2: by repeat (rewrite In_map; eexists; split; eauto); apply qOK.
    symmetry in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in EQ; eauto; desf.
    symmetry in EQ; eapply hsum_preserves_Rlabel_inv in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    right.
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in EQ; eauto; desf.
    symmetry in EQ; eapply hsum_preserves_Rlabel_inv in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    apply hplus_gheap in qEQ.
    right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    apply hplus_gheap in qEQ.
    right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    right.
    rewrite pEQ in qEQ; apply hplus_gheap in qEQ.
    eexists (hb_sb _ e), _, _; repeat split; red in IV; ins; desf; eauto.
  }

  {
    right; revert TYP.
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × unfold hupd in qEQ0; desfh; desfh.
      symmetry in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; rewrite ?hupds; try by eauto.
      desfh; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      + red in TRAN; desfh.
        rewrite TRAN in ×.
        red in rfsSIM; desfh.
        specialize (rfsSIM1 l).
        rewrite HVsim_sym in rfsSIM1; eapply Rlabel_sim in rfsSIM1; eauto; desfh.
        specialize (TRAN3 l).
        exploit (Rlabel_is_consistent_with_exact_label (hf2 l)); eauto; intro; desfh.
        symmetry in TRAN; eapply hsum_preserves_Rlabel_inv in TRAN; eauto; desfh.
        repeat (rewrite In_map in *; desfh).
        eexists (hb_rf _ e), _, _; ins; repeat split; eauto.
          by apply rfsOK.
        repeat right; repeat split; desfh.
        - red in TYP; desfh.
          by exploit Rlabel_is_consistent_with_exact_label; try exact (TYP0 l); eauto.
        - desf.
      + eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
        symmetry in pEQ'; rewrite hplusC in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; eauto; desfh.
        eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    right; clear TYP.
    assert (l0 = l) by (unfold hupd in LAB; desfh; desfh).
    symmetry in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; rewrite ?hupds; simpls; desfh.
      2: by instantiate (1 := HLnormal); vauto.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    apply hplus_gheap in qEQ; desfh.
    unfold hupd in *; desfh; desfh; eauto.
    right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    destruct (classic (l = l0)); eauto.
    right; clear TYP.
    symmetry in UPD; rewrite <- hplusA in UPD, qEQ.
    assert (D := hplus_def_inv_l _ _ UPD); desfh; rewrite D in ×.
    apply hplus_eq_gheap in ghostEQ; desfh.
    apply hplus_gheap in qEQ; desfh.
    symmetry in UPD; eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    unfold initialize, hupd in UPD; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desf.
    specialize (TRAN3 l).
    by exploit Rlabel_is_consistent_with_exact_label; eauto.
  }

  {
    exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by left; unfold hupd in qEQ0; desfh.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × eapply Rlabel_hsim in ACQsim; eauto; desfh.
      rewrite <- rInEQ in TRANin.
      apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in ×.
      eapply hplus_preserves_Rlabel in rInEQ; eauto.
      exploit Rlabel_is_consistent_with_exact_label_spec; try exact rInEQ; eauto.
      ins; subst.
      symmetry in D; eapply hsum_preserves_Rlabel_inv in D; eauto; desfh.
      repeat (rewrite In_map in *; desfh).
      right; eexists (hb_rf _ _), _, _; repeat split; ins; eauto.
        by apply rfsInOK.
      repeat right; repeat split; try done.
      red in ACQlabel; desfh; try by desf.
      by exploit Rlabel_is_consistent_with_exact_label_spec; try exact ACQlabel; eauto.
    × apply hplus_eq_gheap in ghostEQ; desfh.
      eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
      right; eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
      rewrite hplusC, hplusA, hplusAC in pEQ.
      eapply hplus_preserves_Rlabel in pEQ; eauto.
  }

  {
    exfalso.
    apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
    rewrite hplusC in DEF; symmetry in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desf.
    apply hplus_eq_gheap in ghostEQ; desf.
    rewrite <- hplusA in rOutEQ; symmetry in rOutEQ.
    eapply hplus_preserves_Rlabel_inv in rOutEQ; eauto; desf.
    by rewrite rOutEQ in *; exploit Rlabel_is_consistent_with_exact_label_spec; eauto.
  }

  {
    exploit FenceInDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desfh; rewrite D in ×.
    right; eexists (hb_sb _ e), _, _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_Rlabel in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso; red in RELlabel'; desf.
      specialize (RELlabel'0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      red in ACQsim; desfh.
      specialize (ACQsim1 l).
      rewrite HVsim_sym in ACQsim1.
      eapply Rlabel_sim in ACQsim1; eauto; desfh.
      red in ACQlabel; desfh.
      exploit Rlabel_is_consistent_with_exact_label; try exact (ACQlabel0 l); eauto; ins; desfh.
      rewrite <- hplusA, hplusC in pEQ.
      eapply hplus_preserves_Rlabel in pEQ; try eassumption; repeat split; try done.
      right; left; repeat split; try done; desf.
      exploit REL; try done.
      intro H; inv H.
  }
Qed.

Lemma step_back_from_triangleR PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeledR (hf l) HLtriangle),
  ∃ edge' hf' g',
    << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
    << EV': edge_valid lab sb rf edge' >> ∧
    << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
    << SB: ¬ is_rf edge >> ∧
    << SB': is_sb edge' >> ∧
   (<< LAB': HVlabeledR (hf' l) HLtriangle >> ∨
    << LAB': HVlabeledR (hf' l) HLnormal >> ∧ << REL: is_release_fence (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.

  assert (notRF: ¬ is_rf edge).
  {
    destruct edge; ins.
    exploit triangles_never_on_rf; eauto; ins; desf; try edone.
      2: eby eapply Rlabel_implies_label.
    by intro N; rewrite N in LAB.
  }

  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e'); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

   {
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    assert (D := hplus_def_inv_l _ _ DEF); desf; rewrite D in ×.
    symmetry in D; eapply hsum_preserves_Rlabel in D; eauto; desfh.
      2: by repeat (rewrite In_map; eexists; split; eauto); apply qOK.
    symmetry in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in EQ; eauto; desf.
    symmetry in EQ; eapply hsum_preserves_Rlabel_inv in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in EQ; eauto; desf.
    symmetry in EQ; eapply hsum_preserves_Rlabel_inv in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    apply hplus_gheap in qEQ; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    apply hplus_gheap in qEQ; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
      ins; unfold is_triangle in LAB; desf.
  }

  {
    rewrite pEQ in qEQ; apply hplus_gheap in qEQ; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso.
      unfold hupd in qEQ0; desf; ins; desfh.
      unfold is_triangle in qEQ0; desf.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      + ins; exfalso.
        assert (L: ∃ lbl, HlabeledExact (Hdef hf'0 g'0 ) lbl ∧ lbl ≠ HLtriangle).
          by desf; eexists; split; eauto.
        clear TYP; desf.
        red in L; desf.
        specialize (L1 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desf.
      + eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
        symmetry in pEQ'; rewrite hplusC in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; eauto; desfh.
        eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    exfalso.
    unfold hupd in *; desf; desf; eauto; ins; unfold is_triangle in LAB; desf.
  }

  {
    apply hplus_gheap in qEQ; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    unfold hupd, lvalue in LAB; desf; desf; ins; eauto.
  }

  {
    symmetry in UPD; rewrite <- hplusA in UPD, qEQ.
    assert (D := hplus_def_inv_l _ _ UPD); desfh; rewrite D in ×.
    apply hplus_eq_gheap in ghostEQ; desfh.
    apply hplus_gheap in qEQ; desfh.
    symmetry in UPD; eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    clear TYP; left; repeat split; try done.
    by eapply initialize_not_normalR; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desf.
    specialize (TRAN3 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desf.
  }

  {
    exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by unfold hupd in qEQ0; desfh; desfh; ins; unfold is_triangle in *; desfh.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by red in ACQlabel; desfh; exploit Rlabel_is_consistent_with_exact_label_spec; try exact qEQ1; eauto.
    apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
    eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
    apply hplus_eq_gheap in ghostEQ; desfh.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    rewrite hplusC, hplusA, hplusAC in pEQ.
    eapply hplus_preserves_Rlabel in pEQ; eauto.
  }

  {
    exfalso.
    apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
    rewrite hplusC in DEF; symmetry in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desf.
    apply hplus_eq_gheap in ghostEQ; desf.
    rewrite <- hplusA in rOutEQ; symmetry in rOutEQ.
    eapply hplus_preserves_Rlabel_inv in rOutEQ; eauto; desf.
    by rewrite rOutEQ in *; exploit Rlabel_is_consistent_with_exact_label_spec; eauto.
  }

  {
    exploit FenceInDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desfh; rewrite D in ×.
    eexists (hb_sb _ e), _, _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_Rlabel in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × red in RELsim; desfh.
      specialize (RELsim1 l).
      apply HVsim_sym in RELsim1; eapply Rlabel_sim in qEQ1; eauto; desfh.
      red in RELlabel; desfh.
      specialize (RELlabel0 l); exploit Rlabel_is_consistent_with_exact_label; eauto; desfh.
      rewrite hplusAC in pEQ; eapply hplus_preserves_Rlabel in pEQ; eauto; ins; desfh; repeat split; try done.
      right; repeat split; try done; desf.
      exploit ACQ; try done.
      intro H; inv H.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      exfalso; red in ACQlabel'; desf.
      specialize (ACQlabel'0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
  }
Qed.

Lemma step_back_from_nablaR PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeledR (hf l) HLnabla),
  (<< STORE: is_writeL (lab (hb_fst edge)) l >> ∧
   << REL: is_release_write (lab (hb_fst edge)) >> ∧
   << RF: ¬ is_sb edge >>) ∨
  ∃ edge' hf' g',
    << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
    << EV': edge_valid lab sb rf edge' >> ∧
    << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
   (<< SB: ¬ is_rf edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnabla >> ∨
    << SB: ¬ is_rf edge >> ∧ << RF': is_rf edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnabla >> ∨
    << RF: ¬ is_sb edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeledR (hf' l) HLtriangle >> ∨
    << RF: ¬ is_sb edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnormal >> ∧
                              << REL: is_release_write (lab (hb_fst edge)) >> ∨
    << RF: ¬ is_sb edge >> ∧ << RF': is_rf edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnabla >> ∧
                              << RMW: is_rmw (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e'); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    right.
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    assert (D := hplus_def_inv_l _ _ DEF); desf; rewrite D in ×.
    symmetry in D; eapply hsum_preserves_Rlabel in D; eauto; desfh.
      2: by repeat (rewrite In_map; eexists; split; eauto); apply qOK.
    symmetry in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in EQ; eauto; desf.
    symmetry in EQ; eapply hsum_preserves_Rlabel_inv in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    right.
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in EQ; eauto; desf.
    symmetry in EQ; eapply hsum_preserves_Rlabel_inv in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    apply hplus_gheap in qEQ; desfh.
    right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    apply hplus_gheap in qEQ; desfh.
    right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
      ins; unfold is_nabla in LAB; desf.
  }

  {
    right.
    rewrite pEQ in qEQ; apply hplus_gheap in qEQ; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    right; revert TYP.
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso.
      unfold hupd in qEQ0; desf; ins; desfh.
      unfold is_nabla in qEQ0; desf.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      + red in TRAN; desfh.
        rewrite TRAN in ×.
        red in rfsSIM; desfh.
        specialize (rfsSIM1 l).
        rewrite HVsim_sym in rfsSIM1; eapply Rlabel_sim in rfsSIM1; eauto; desfh.
        specialize (TRAN3 l).
        exploit (Rlabel_is_consistent_with_exact_label (hf2 l)); eauto; intro; desfh.
        symmetry in TRAN; eapply hsum_preserves_Rlabel_inv in TRAN; eauto; desfh.
        repeat (rewrite In_map in *; desfh).
        eexists (hb_rf _ e), _, _; ins; repeat split; eauto 6.
        by apply rfsOK.
      + eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
        symmetry in pEQ'; rewrite hplusC in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; eauto; desfh.
        eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
  }

  {
    exfalso.
    unfold hupd in *; desf; desf; eauto; ins; unfold is_nabla in LAB; desf.
  }

  {
    right.
    apply hplus_gheap in qEQ; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    unfold hupd, lvalue in LAB; desfh; desfh; ins; eauto.
  }

  {
    symmetry in UPD; rewrite <- hplusA in UPD, qEQ.
    assert (D := hplus_def_inv_l _ _ UPD); desfh; rewrite D in ×.
    apply hplus_eq_gheap in ghostEQ; desfh.
    apply hplus_gheap in qEQ; desfh.
    symmetry in UPD; right; clear TYP.
    eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
    left; repeat split; try done.
    by eapply initialize_not_normalR; eauto.
  }

  {
    red in TRAN; desfh.
    rewrite TRAN in ×.
    assert (R := hplus_def_inv_l _ _ TRAN); desfh.
    rewrite R in ×.
    symmetry in R; eapply hsum_preserves_Rlabel in R; eauto; desfh.
      2: by repeat (rewrite In_map; eexists; split; eauto); apply rfsOK.
    symmetry in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desfh.
    rewrite Hsim_sym in rfsSIM; eapply Rlabel_hsim in rfsSIM; eauto; desfh.
    apply hplus_eq_gheap in ghostEQ; desfh.
    eapply hplus_preserves_Rlabel_inv in rfsSIM; eauto; desfh.
    assert (UPDcopy := UPD).
    rewrite <- hplusA, hplusC in UPD; eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    ins; desfh.
    × right; eexists (hb_sb _ e), _, _; do 3 (split; eauto); ins.
      red in TYP; desfh.
      exploit Rlabel_is_consistent_with_exact_label; try exact (TYP0 l); eauto; intro; desfh.
      right; right; left; repeat split; try done.
      by eapply initialize_not_normalR; eauto.
    × red in TYP1; desfh.
      exploit Rlabel_is_consistent_with_exact_label; try exact (TYP2 l); eauto; intro; desfh.
      destruct (classic (l0 = l)); desfh.
      + by left; desf; repeat split.
      + right; eexists (hb_sb _ e), _, _; do 3 (split; eauto); ins.
        unfold initialize, hupd in UPD; ins; desfh.
        by do 3 right; left; desf; repeat split.
  }

  {
    red in TRAN; desfh.
    rewrite TRAN in ×.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desfh.
    rewrite Hsim_sym in rfsSIM; eapply Rlabel_hsim in rfsSIM; eauto; desfh.
    apply hplus_eq_gheap in ghostEQ; desfh.
    eapply hplus_preserves_Rlabel_inv in rfsSIM; eauto; desfh.
    assert (UPDcopy := UPD).
    rewrite <- hplusA, hplusC in UPD; eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    ins; desfh.
    × right; eexists (hb_sb _ e), _, _; do 3 (split; eauto); ins.
      red in TYP; desfh.
      exploit Rlabel_is_consistent_with_exact_label; try exact (TYP0 l); eauto; intro; desfh.
      right; right; left; repeat split; try done.
      by eapply initialize_not_normalR; eauto.
    × red in TYP1; desfh.
      exploit Rlabel_is_consistent_with_exact_label; try exact (TYP2 l); eauto; intro; desfh.
      destruct (classic (l = l0)).
      + by left; desf; repeat split.
      + right; eexists (hb_sb _ e), _, _; do 3 (split; eauto); ins.
        unfold initialize, hupd in UPD; ins; desfh.
        by do 3 right; left; desf; repeat split.
  }

  {
    exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by unfold hupd in qEQ0; desfh; desfh; ins; unfold is_nabla in qEQ0; desfh.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × eapply Rlabel_hsim in ACQsim; eauto; desfh.
      apply exact_label_hplus_dist in TRANin; desfh.
      exploit Rlabel_is_consistent_with_exact_label_spec; try exact ACQsim1; eauto.
      ins; subst.
      apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in ×.
      eapply hplus_preserves_Rlabel in rInEQ; eauto; desfh.
      symmetry in D; eapply hsum_preserves_Rlabel_inv in D; eauto; desfh.
      repeat (rewrite In_map in *; desfh).
      right; eexists (hb_rf _ _), _, _; repeat split; eauto; ins.
        by apply rfsInOK.
      by right; left; repeat split.
    × apply hplus_eq_gheap in ghostEQ; desfh.
      eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
      rewrite hplusC, hplusA, hplusAC in pEQ.
      eapply hplus_preserves_Rlabel in pEQ; eauto; desfh.
      right; eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
  }

  {
    exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); rewrite <- hdef_alt; intro D; desfh.
    red in TRANout; desfh; rewrite <- hplusA, TRANout in rOutEQ.
    apply hplus_not_undef_r, hdef_alt in DEF; desfh; rewrite DEF in ×.
    assert (R := hplus_def_inv_l _ _ DEF); desfh; rewrite R in ×.
    symmetry in R; eapply hsum_preserves_Rlabel in R; eauto; desfh.
      2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
    symmetry in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    apply hplus_eq_gheap in ghostEQ; desfh.
    symmetry in rOutEQ; eapply hplus_preserves_Rlabel_inv in rOutEQ; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in TRANout; eauto; desfh.
    × eapply Rlabel_hsim in RELsim; eauto; desfh.
      apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
      rewrite hplusAC in pEQ; eapply hplus_preserves_Rlabel in pEQ; eauto; desfh.
      red in RELlabel; desfh; exploit Rlabel_is_consistent_with_exact_label_spec;
                                      try exact RELsim0; eauto; ins; subst lbl'.
      + right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
        right; right; left; eauto.
      + right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
        do 3 right; left; repeat split; desf.
    × apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in ×.
      rewrite hplusC in rInEQ; eapply hplus_preserves_Rlabel in rInEQ; eauto; desfh.
      symmetry in D; eapply hsum_preserves_Rlabel_inv in D; eauto; desfh.
      repeat (rewrite In_map in *; desfh).
      right; eexists (hb_rf _ _), _, _; repeat split; eauto; ins.
        by apply rfsInOK.
      by repeat right; repeat split.
  }

  {
    exploit RMWinDEF; try exact pEQ; try eassumption; try (eby rewrite <- MAP in *);
      rewrite <- hdef_alt; intro D; desfh.
    red in TRANout; desfh; rewrite <- hplusA, TRANout in rOutEQ.
    apply hplus_not_undef_r, hdef_alt in DEF; desfh; rewrite DEF in ×.
    symmetry in DEF; rewrite hplusC in DEF; eapply hplus_preserves_Rlabel in DEF; eauto; desfh.
    apply hplus_eq_gheap in ghostEQ; desfh.
    symmetry in rOutEQ; rewrite hplusC in rOutEQ; eapply hplus_preserves_Rlabel_inv in rOutEQ; eauto; desfh.
    eapply hplus_preserves_Rlabel_inv in TRANout; eauto; desfh.
    × eapply Rlabel_hsim in RELsim; eauto; desfh.
      apply hplus_not_undef_l, hdef_alt in D; desfh; rewrite D in ×.
      rewrite hplusAC in pEQ; eapply hplus_preserves_Rlabel in pEQ; eauto; desfh.
      red in RELlabel; desfh; exploit Rlabel_is_consistent_with_exact_label_spec;
                                      try exact RELsim0; eauto; ins; subst lbl'.
      + right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
        right; right; left; eauto.
      + right; eexists (hb_sb _ e), _, _; repeat split; ins; eauto.
        do 3 right; left; repeat split; desf.
    × apply hplus_not_undef_r, hdef_alt in D; desfh; rewrite D in ×.
      rewrite hplusC in rInEQ; eapply hplus_preserves_Rlabel in rInEQ; eauto; desfh.
      symmetry in D; eapply hsum_preserves_Rlabel_inv in D; eauto; desfh.
      repeat (rewrite In_map in *; desfh).
      right; eexists (hb_rf _ _), _, _; repeat split; eauto; ins.
        by apply rfsInOK.
      by repeat right; repeat split.
  }

  {
    exploit FenceInDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desfh; rewrite D in ×.
    right; eexists (hb_sb _ e), _, _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_Rlabel in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso; red in RELlabel'; desf.
      specialize (RELlabel'0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      exfalso; red in ACQlabel'; desf.
      specialize (ACQlabel'0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
  }
Qed.