Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple fsltriple2.
Require Import drf ihc initread.
Require Import GpsSepAlg.

Set Implicit Arguments.

Lemma rmw_rf_uniq :
  ∀ lab sb rf mo
    (Crf : ConsistentRF_basic lab sb rf mo)
    (Cmo : ConsistentMO lab sb rf mo)
    (Crmw : AtomicRMW lab rf mo) a wri
    (RF1 : rf a = Some wri) b
    (RF2 : rf b = Some wri) typ1 l1 v1 v1'
    (LAB1 : lab a = Armw typ1 l1 v1 v1') l2 typ2 v2 v2'
    (LAB2 : lab b = Armw typ2 l2 v2 v2'),
    a = b.
Proof.
  ins; destruct (eqP a b) as [|NEQ]; ins; exfalso.
  assert (l1 = l2); subst.
    generalize (Crf a); rewrite RF1, LAB1; ins.
    generalize (Crf b); rewrite RF2, LAB2; ins; desf.
    by destruct (lab wri); ins; desf.
  eapply Crmw in RF1; [|by rewrite LAB1].
  eapply Crmw in RF2; [|by rewrite LAB2].
  red in Cmo; desc; eapply Cmo1 in NEQ; rewrite ?LAB1, ?LAB2; try done.
  destruct RF1, RF2, NEQ; eauto.
Qed.

Lemma rmw_concurrent_readers_transfer_no_ownership PS PSg:
  ∀ fst acts lab sb rf mo sc
    (CONS : weakConsistent (fst :: acts) lab sb rf mo sc Model_hb_rf_acyclic)
    typ E E' E'' (LAB : lab fst = Armw typ E E' E'')
    prev (FST : unique (sb^~ fst) prev)
    V (V_PREV : In prev V)
    (HC : hist_closed sb rf V)
    hmap (VALID : hmap_valids_strong lab sb rf hmap V)
    (NIN : ¬ In fst V)
    hoo goo (Z : hmap (hb_sb prev fst) = Hdef hoo goo)
    PP QQ labW labR (Z0 : hoo E = @HVra PS PSg PP (fun x : val ⇒ mk_assn_mod (QQ x)) true labW labR)
    wri (RF : rf fst = Some wri)
    rfs (INrfs: ∀ x, In x rfs → rf x = Some wri),
  hsum (map hmap (map (hb_rf wri) rfs)) = hemp.
Proof.
  induction rfs; ins; desf; ins; rewrite hsum_cons, IHrfs, hplus_emp_r; eauto.
  red in VALID; desc; red in VALIDS; desc.
  destruct (classic (In a V)) as [INa | NINa].

  {
    specialize (INrfs _ (In_eq _ _)).
    red in CONS; desc.
    generalize (Crf a); rewrite INrfs; intro R; desc.
    generalize (VLD _ INa); intro VV.
    red in VV; desf; desc.
      2: by (assert (fst = a); subst; eauto using rmw_rf_uniq).
    destruct DISJ; desc; try done.
    clear TYP.
    ins; desf.
    assert (E = l).
    {
      generalize (Crf fst); rewrite RF, LAB; ins; desf.
      by destruct (lab wri); ins; desf.
    }
    subst.
    assert (rfs0 = wri :: nil) by (apply NoDup_eq_one; ins; rewrite rfsOK in *; eauto; congruence).
    subst; ins; rewrite hsum_one in ×.
    destruct FST, pU.
    eapply hplus_def_inv in pEQ'; desf.
    specialize (DEFv l); specialize (PLUSv l); rewrite hupds in *; ins.
    destruct (hz l) eqn:HZ; ins.
    × eapply heap_loc_ra_no_own with (edge' := hb_sb _ _) (h' := hf) (v:=v) (V:=V) in Z0;
        try exact PLUSv; try exact (proj1 VALID); eauto; ins; eauto with hb.
        2: by eexists; split; eauto.
      rewrite hupds in *; desf; rewrite Z0 in *; ins; desf.
      red in TRAN1; desf.
      inv TRAN0.
      rewrite TRAN1; unfold hemp; f_equal; exten.
      red in TRAN3; desf.
      ins; specialize (TRAN3 x); red in TRAN3; desf.
    × destruct isrmwflag.
      + desc; specialize (DEFv v); rewrite hupds in *; destruct DEFv as [DEFv|[DEFv ?]];
          ins; rewrite DEFv in *; ins.
        clear PLUSv; desf.
        red in TRAN1; desf.
        inv TRAN0.
        rewrite TRAN1; unfold hemp; f_equal; exten.
        red in TRAN3; desf.
        ins; specialize (TRAN3 x); red in TRAN3; desf.
     + eapply heap_loc_ra_no_own with (edge' := hb_sb _ _) (h' := hf) (v:=v) (V:=V) in Z0;
         try exact PLUSv; try exact (proj1 VALID); eauto; ins; eauto with hb.
         2: by eexists; split; eauto.
       clear PLUSv.
       assert (EF: sval P = Aemp ∨ sval P = Afalse).
         by rewrite hupds in *; desf; [apply assn_norm_star_eq_emp, proj1 in Z0 |
                                       apply assn_norm_star_eq_false in Z0; desf];
                                       destruct P as [P normP]; ins; rewrite !normP in *;
                                       desf; eauto.
       clear Z0; desf; rewrite EF in *; ins; desf.
       red in TRAN1; desf.
       inv TRAN0.
       rewrite TRAN1; unfold hemp; f_equal; exten.
       red in TRAN3; desf.
       ins; specialize (TRAN3 x); red in TRAN3; desf.
  }

  {
    eapply RESTR; eauto.
    right; split; try done.
    intro X; red in X; ins; desf.
  }
Qed.

Opaque Aexists.

Definition rmw_precondition PS PSg P l QQrel QQacq :=
  @Astar PS PSg (Arel l QQrel) (Astar (Armwacq l QQacq) (Astar (Arainit l) P)).

Definition satisfying PS PSg (phi: val → Prop) (AA: val → assn PS PSg) z :=
  if excluded_middle_informative (phi z) then AA z else Afalse.

Theorem rule_cas_ar PS PSg:
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi : val → Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AR: acquire_release_typ rmw_typ)
    (FAIL: triple (rmw_precondition P E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else RR x)),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi AA) else RR x).
Proof.
  ins; eapply triple_helper_start; ins; desf; ins; desf; try done.
  Focus 2.     exploit (FAIL (fst :: nil) (Some v') lab sb fst fst); eauto; ins; eauto.
    by repeat eexists.
    by instantiate (1 := S n) in x0; ins; desf; desf;
       exploit GUAR; clear POST RELY GUAR; try eassumption; eauto.
  clear FAIL.

  assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.

  rename h5 into hP.

  rewrite <- !hplusA in pEQ.
  rewrite hplus_hsingl_rel_rmwacq in pEQ; ins.
  rewrite hplus_init1 in pEQ; ins.

  assert (Z: ∃ hoo goo QQ labW labR, hmap (hb_sb prev fst) = Hdef hoo goo ∧
                    hoo E = HVra QQ (fun x : val ⇒ mk_assn_mod (QQacq x))
                                 true (ohlplus labW HLnormal) (ohlplus labR HLnormal)).
  {
    rewrite pEQ in *; clear -pDEF.
    rewrite hplusA in *; destruct (hP +!+ hFR); ins.
    rewrite hplus_unfold in *; desf; desf.
    specialize (HEAPcompat E); rewrite hupds in *; ins; desf; desf.
    × repeat eexists. ins.
      rewrite hupds, Heq; ins.
      f_equal; try by instantiate (1 := None).
      extensionality v; desf.
    × eexists _, _, _, permlbl, init; repeat split; try done.
      by ins; rewrite hupds, Heq.
  }
  desc.

  assert (∃ wri, << RF : rf fst = Some wri >> ∧ << WRI: is_writeLV (lab wri) E E' >>).
  {
    red in CONS; desc; assert (C := (Crf fst)); desf.
    × repeat eexists; desf; simpls; vauto.
      by rewrite SEM1 in *; ins; desf.
    × exfalso.
      red in FST; desf.
      exploit initialization_always_before; try exact Z; try exact (proj1 VALID); eauto.
         instantiate (2 := E); instantiate (1 := HLnormal).
         rewrite Z0; ins. destruct labR; ins; vauto.
         by destruct h; ins; unfold is_normal; eauto.
      ins; desf.
      eapply (C a); eauto.
        2: eby rewrite SEM1.
      clear - HB FST.
      apply clos_refl_trans_hbE in HB; desf; eauto with hb.
  }
  desc.

  assert (INwri: In wri V).
  {
    exploit HC0; eauto using In_eq; ins; desf; vauto.
    exfalso; red in CONS; desc; eapply ACYC; vauto.
  }
  
  assert (VALIDwri := VLD _ INwri).
  red in VALIDwri; destruct (lab wri) eqn: LABwri; ins; desc; subst.
  destruct DISJ; desc.

  {
    red in CONS, FST, pU; desf.
    exfalso; eapply atomicity_is_globally_exclusive; try exact (proj1 VALID);
             try (eby apply is_lvalue_implies_is_nonatomic); try exact Z; eauto; ins.
    by eapply HC; vauto.
    by rewrite Z0.
  }

  {
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfs)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
        ins; clear TYP; red in CONS; desf; ins.
        exploit wellformed_one_w; try exact (proj1 VALID); try exact H; try exact pEQ0;
                                  try exact (proj1 FST); try exact (proj1 pU); eauto.
        intro IMP; eapply (IMP V_PREV (proj1 FST)) in TRAN0; eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd h2 HLnabla); repeat split.
          by rewrite <- lupd_hplus_dist; apply lupd_eq.
          by apply lupd_label; intro U; rewrite U in *; desf.
        eexists; repeat split.
        eby apply assn_sem_assn_norm.
        by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
        by apply exact_label_hplus_dist in TRAN2; desf.
      clear - UPD TRAN0.
      symmetry in UPD; apply hplus_def_inv in UPD; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRAN0; desf.
      by rewrite e in TRAN0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
       ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { clear TYP; red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        eexists _, _, _, _; repeat (split; try edone).
          eby subst hmap'; ins.
        right; split; try done.
        ∃ rfs, hr, hF, P0, sbg, rfg.
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfs)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          clear TYP; rewrite <- rfsOK in RF.
          apply In_implies_perm in RF as [rfs' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        rewrite <- SAME, HM' in *; unnw; repeat (split; try done).
        eby eexists; split.
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        clear TYP; ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    clear TYP.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND.
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (ACQ := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct ACQ as [z ACQ]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact ACQ2; try exact pSAT8.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      by repeat (apply hplus_not_undef_l in IND; try done).
    apply NORM in pSAT8; desc.
    rename h'0 into hdrop; desf.
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                            true (Some HLCnormal) (Some HLCnormal))
               +!+ hAcq +!+ hdrop +!+ hFR )
       (hs := lupd (hN +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _ +!+ hdrop), _; split; [ | split]; try edone.
        3: eby apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        2: by rewrite (hplusC _ hFR), !(hplusAC hFR), !(hplusAC hAcq).
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hN), !(hplusAC hT) in IND.
      do 2 (apply hplus_not_undef_r in IND).
      by rewrite hplusAC.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      rename rfs0 into rfsOut.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfsOut)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfsOut; repeat (apply conj; try edone); try (eby eapply LST); try edone.
        by red in AR; desf.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hN), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC hAcq), <- hplusA.
          eapply hplus_sim_def; eauto.
          by rewrite !hplusA, !(hplusAC hN), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hN, (lupd hN HLnabla),
              (lupd hAcq HLnabla), hAcq, (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hdrop +!+ hFR).
        rewrite !hplusA, !(hplusAC hN), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA, !(hplusAC hAcq), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      × ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (NTdef: hN +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hN), (hplusAC hT), <- !hplusA in IND.
          repeat (apply hplus_not_undef_l in IND; try done).
        }
        ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj).
          2: by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
          by rewrite assn_sem_assn_norm; apply IMPrel; ins; repeat eexists.
        apply exact_label_hplus_dist in RFann2.
        apply exact_label_hplus_dist_inv; desf.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × apply Hsim_sym, lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × red in AR; desf; red; red; vauto.
      × red in AR; desf; apply exact_label_hplus_dist in RFann2; desf; red; red; vauto.
    }
  }
    
  {
    RMWin_heap.
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfsOut)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOutOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
      {
        ins; red in CONS; desf; ins.
        assert (WLV: is_writeLV (lab wri) E E') by (by rewrite LABwri).
        exploit wellformed_one; try exact WLV; try exact (proj1 VALID); try exact H; try exact DEFin;
                                   try exact (proj1 pU); eauto.
        intro IMP; eapply IMP in TRANout0; try exact (proj1 FST); eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd (h2 +!+ rfg) HLnabla); repeat split.
        × rewrite <- lupd_hplus_dist; apply lupd_eq; rewrite rOutEQ.
          + rewrite <- !hplusA; apply hplus_sim; try done.
            by apply Hsim_refl; intro U; rewrite U, !hplus_undef_r in *; congruence.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
          + rewrite <- hplusA; apply exact_label_hplus_dist_inv; try done.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
            by apply hplus_eq_gheap in ghostEQ; desf; vauto.
        × by apply lupd_label; intro U; rewrite U in *; desf.
        × eexists; repeat split.
          eby apply assn_sem_assn_norm.
          by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
          by apply exact_label_hplus_dist in TRANout2; desf.
      }
      rewrite pEQ0, !hplusA in DEFin; clear - DEFin TRANout0.
      destruct (hrel +!+ hF +!+ hsum (map hmap (map (hb_rf^~ wri) rfsIn))); ins.
      apply hplus_def_inv in DEFin; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRANout0; desf.
      by rewrite e in TRANout0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
      ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfsOut)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          rewrite <- rfsOutOK in RF.
          apply In_implies_perm in RF as [rfsOut' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        ∃ pre, post, rfsIn, rfsOut; repeat (split; try done).
          by rewrite SAME; subst hmap'; unfold mupd; desf; desf.
        ∃ P0, QQ0, hrel, hrel', hacq, hacq', ht, hF, sbg, rfg.
        Opaque assn_sem.
        rewrite <- SAME, HM' in *; unnw; repeat (apply conj; try done).
        Transparent assn_sem.
        by rewrite !map_upd_irr; ins; intro; desf.
        eby ins; split; try done; eexists; repeat (apply conj).
        eby ins; split; try done; eexists; repeat (apply conj).
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND;
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (ACQ := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct ACQ as [z ACQ]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact ACQ2; try exact pSAT8.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      by repeat (apply hplus_not_undef_l in IND; try done).
    apply NORM in pSAT8; desc.
    rename h'1 into hdrop; desf.
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                             true (Some HLCnormal) (Some HLCnormal))
                +!+ hAcq +!+ hdrop +!+ hFR )
       (hs := lupd (hN +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _ +!+ hdrop), _; split; [ | split]; try edone.
        3: eby apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        2: by rewrite (hplusC _ hFR), !(hplusAC hFR), !(hplusAC hAcq).
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hN), !(hplusAC hT) in IND.
      do 2 (apply hplus_not_undef_r in IND).
      by rewrite hplusAC.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfs)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfs; repeat (apply conj); try (eby eapply LST); try edone.
        by red in AR; desf.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hN), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC hAcq), <- hplusA.
          eapply hplus_sim_def; eauto.
          by rewrite !hplusA, !(hplusAC hN), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hN, (lupd hN HLnabla),
              (lupd hAcq HLnabla), hAcq, (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hdrop +!+ hFR).
        rewrite !hplusA, !(hplusAC hN), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA, !(hplusAC hAcq), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      × ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (NTdef: hN +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hN), (hplusAC hT), <- !hplusA in IND.
          repeat (apply hplus_not_undef_l in IND; try done).
        }
        ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj).
          2: by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
          by rewrite assn_sem_assn_norm; eapply IMPrel; try edone; ins; repeat eexists.
        apply exact_label_hplus_dist in RFann2.
        apply exact_label_hplus_dist_inv; desf.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × apply Hsim_sym, lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × red in AR; desf; red; red; vauto.
      × apply exact_label_hplus_dist in RFann2; red in AR; desf; red; red; vauto.
    }
  }

  Grab Existential Variables. all: done.
Qed.

Theorem rule_cas_rel PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi: val → Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (REL: release_typ rmw_typ)
    (FAIL: triple (rmw_precondition P E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else (RR x))),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi (fun y ⇒ Anabla (AA y))) else RR x).
Proof.
  ins; eapply triple_helper_start; ins; desfh; ins; desfh.
  Focus 2.     exploit (FAIL (fst :: nil) (Some v') lab sb fst fst); eauto; ins; eauto.
    by repeat eexists.
    by instantiate (1 := S n) in x0; ins; desf; desf;
       exploit GUAR; clear POST RELY GUAR; try eassumption; eauto.
  clear FAIL; rewrite eqxx.

  assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.

  rename h5 into hP.

  rewrite <- !hplusA in pEQ.
  rewrite hplus_hsingl_rel_rmwacq in pEQ; ins.
  rewrite hplus_init1 in pEQ; ins.

  assert (Z: ∃ hoo goo QQ labW labR, hmap (hb_sb prev fst) = Hdef hoo goo ∧
                    hoo E = HVra QQ (fun x : val ⇒ mk_assn_mod (QQacq x))
                                 true (ohlplus labW HLnormal) (ohlplus labR HLnormal)).
  {
    rewrite pEQ in *; clear -pDEF.
    rewrite hplusA in *; destruct (hP +!+ hFR); ins.
    rewrite hplus_unfold in *; desf; desf.
    specialize (HEAPcompat E); rewrite hupds in *; ins; desf; desf.
    × repeat eexists. ins.
      rewrite hupds, Heq; ins.
      f_equal; try by instantiate (1 := None).
      extensionality v; desf.
    × eexists _, _, _, permlbl, init; repeat split; try done.
      by ins; rewrite hupds, Heq.
  }
  desc.

  assert (∃ wri, << RF : rf fst = Some wri >> ∧ << WRI: is_writeLV (lab wri) E E' >>).
  {
    red in CONS; desc; assert (C := (Crf fst)); desf.
    × repeat eexists; desf; simpls; vauto.
      by rewrite SEM1 in *; ins; desf.
    × exfalso.
      red in FST; desf.
      exploit initialization_always_before; try exact Z; try exact (proj1 VALID); eauto.
         instantiate (2 := E); instantiate (1 := HLnormal).
         rewrite Z0; ins. destruct labR; ins; vauto.
         by destruct h; ins; unfold is_normal; eauto.
      ins; desf.
      eapply (C a); eauto.
        2: eby rewrite SEM1.
      clear - HB FST.
      apply clos_refl_trans_hbE in HB; desf; eauto with hb.
  }
  desc.

  assert (INwri: In wri V).
  {
    exploit HC0; eauto using In_eq; ins; desf; vauto.
    exfalso; red in CONS; desc; eapply ACYC; vauto.
  }
  
  assert (VALIDwri := VLD _ INwri).
  red in VALIDwri; destruct (lab wri) eqn: LABwri; ins; desc; subst.
  destruct DISJ; desc.

  {
    red in CONS, FST, pU; desf.
    exfalso; eapply atomicity_is_globally_exclusive; try exact (proj1 VALID);
             try (eby apply is_lvalue_implies_is_nonatomic); try exact Z; eauto; ins.
    by eapply HC; vauto.
    by rewrite Z0.
  }

  {
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfs)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
        ins; clear TYP; red in CONS; desf; ins.
        exploit wellformed_one_w; try exact (proj1 VALID); try exact H; try exact pEQ0;
                                  try exact (proj1 FST); try exact (proj1 pU); eauto.
        intro IMP; eapply (IMP V_PREV (proj1 FST)) in TRAN0; eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd h2 HLnabla); repeat split.
          by rewrite <- lupd_hplus_dist; apply lupd_eq.
          by apply lupd_label; intro U; rewrite U in *; desf.
        eexists; repeat split.
        eby apply assn_sem_assn_norm.
        by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
        by apply exact_label_hplus_dist in TRAN2; desf.
      clear - UPD TRAN0.
      symmetry in UPD; apply hplus_def_inv in UPD; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRAN0; desf.
      by rewrite e in TRAN0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
       ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { clear TYP; red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        eexists _, _, _, _; repeat (split; try edone).
          eby subst hmap'; ins.
        right; split; try done.
        ∃ rfs, hr, hF, P0, sbg, rfg.
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfs)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          clear TYP; rewrite <- rfsOK in RF.
          apply In_implies_perm in RF as [rfs' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        rewrite <- SAME, HM' in *; unnw; repeat (split; try done).
        eby eexists; split.
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        clear TYP; ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    clear TYP.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND;
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (ACQ := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct ACQ as [z ACQ]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact ACQ2; try exact pSAT8.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      by repeat (apply hplus_not_undef_l in IND; try done).
    apply NORM in pSAT8; desc.
    rename h'0 into hdrop; desf.
    assert (ADEF: hAcq ≠ Hundef) by (intro; desf).
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                            true (Some HLCnormal) (Some HLCnormal))
               +!+ (lupd hAcq HLnabla) +!+ hdrop +!+ hFR )
       (hs := lupd (hN +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _ +!+ hdrop), (lupd hAcq HLnabla); split; [ | split].
      × apply (hplus_sim_def _ RFann1) in IND.
        rewrite !hplusA in IND; apply (hplus_sim_def _ (lupd_sim HLnabla ADEF)) in IND.
        rewrite !(hplusAC hN), !(hplusAC hT) in IND.
        do 2 (apply hplus_not_undef_r in IND).
        by rewrite hplusAC.
      × by rewrite (hplusC _ hFR), !(hplusAC hFR), !(hplusAC (lupd hAcq _)).
      × apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        split.
          by apply lupd_label.
        eexists; repeat (apply conj; try edone).
        by apply Hsim_sym, lupd_sim.
        by apply exact_label_hplus_dist in RFann2; desf.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      rename rfs0 into rfsOut.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfsOut)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfsOut; repeat (apply conj); try (eby eapply LST); try edone.
        by red in REL; desf.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hN), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC (lupd _ _)).
          eapply hplus_sim_def.
            eby eapply lupd_sim, assn_sem_def.
          rewrite <- hplusA; eapply hplus_sim_def; eauto.
          by rewrite !hplusA, !(hplusAC hN), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hN, (lupd hN HLnabla),
              (lupd hAcq HLnabla), (lupd hAcq HLnabla), (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hdrop +!+ hFR).
        rewrite !hplusA, !(hplusAC hN), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA, !(hplusAC (lupd _ _)), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      × ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (NTdef: hN +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hN), (hplusAC hT), <- !hplusA in IND.
          repeat (apply hplus_not_undef_l in IND; try done).
        }
        ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj).
          2: by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
          by rewrite assn_sem_assn_norm; eapply IMPrel; try edone; ins; repeat eexists.
        apply exact_label_hplus_dist in RFann2.
        apply exact_label_hplus_dist_inv; desf.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × by apply Hsim_refl; destruct hAcq.
      × red in REL; desf; red; red; vauto.
      × by left; apply lupd_label.
    }
  }
    
  {
    RMWin_heap.
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfsOut)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOutOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
      {
        ins; red in CONS; desf; ins.
        assert (WLV: is_writeLV (lab wri) E E') by (by rewrite LABwri).
        exploit wellformed_one; try exact WLV; try exact (proj1 VALID); try exact H; try exact DEFin;
                                   try exact (proj1 pU); eauto.
        intro IMP; eapply IMP in TRANout0; try exact (proj1 FST); eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd (h2 +!+ rfg) HLnabla); repeat split.
        × rewrite <- lupd_hplus_dist; apply lupd_eq; rewrite rOutEQ.
          + rewrite <- !hplusA; apply hplus_sim; try done.
            by apply Hsim_refl; intro U; rewrite U, !hplus_undef_r in *; congruence.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
          + rewrite <- hplusA; apply exact_label_hplus_dist_inv; try done.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
            by apply hplus_eq_gheap in ghostEQ; desf; vauto.
        × by apply lupd_label; intro U; rewrite U in *; desf.
        × eexists; repeat split.
          eby apply assn_sem_assn_norm.
          by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
          by apply exact_label_hplus_dist in TRANout2; desf.
      }
      rewrite pEQ0, !hplusA in DEFin; clear - DEFin TRANout0.
      destruct (hrel +!+ hF +!+ hsum (map hmap (map (hb_rf^~ wri) rfsIn))); ins.
      apply hplus_def_inv in DEFin; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRANout0; desf.
      by rewrite e in TRANout0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
      ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfsOut)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          rewrite <- rfsOutOK in RF.
          apply In_implies_perm in RF as [rfsOut' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        ∃ pre, post, rfsIn, rfsOut; repeat (split; try done).
          by rewrite SAME; subst hmap'; unfold mupd; desf; desf.
        ∃ P0, QQ0, hrel, hrel', hacq, hacq', ht, hF, sbg, rfg.
        Opaque assn_sem.
        rewrite <- SAME, HM' in *; unnw; repeat (apply conj; try done).
        Transparent assn_sem.
        by rewrite !map_upd_irr; ins; intro; desf.
        eby ins; split; try done; eexists; repeat (apply conj).
        eby ins; split; try done; eexists; repeat (apply conj).
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND;
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (ACQ := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct ACQ as [z ACQ]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact ACQ2; try exact pSAT8.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      by repeat (apply hplus_not_undef_l in IND; try done).
    apply NORM in pSAT8; desc.
    rename h'1 into hdrop; desf.
    assert (ADEF: hAcq ≠ Hundef) by (intro; desf).
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                            true (Some HLCnormal) (Some HLCnormal))
               +!+ (lupd hAcq HLnabla) +!+ hdrop +!+ hFR )
       (hs := lupd (hN +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _ +!+ hdrop), (lupd hAcq HLnabla); split; [ | split].
      × apply (hplus_sim_def _ RFann1) in IND.
        rewrite !hplusA in IND; apply (hplus_sim_def _ (lupd_sim HLnabla ADEF)) in IND.
        rewrite !(hplusAC hN), !(hplusAC hT) in IND.
        do 2 (apply hplus_not_undef_r in IND).
        by rewrite hplusAC.
      × by rewrite (hplusC _ hFR), !(hplusAC hFR), !(hplusAC (lupd hAcq _)).
      × apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        split.
          by apply lupd_label.
        eexists; repeat (apply conj; try edone).
        by apply Hsim_sym, lupd_sim.
        by apply exact_label_hplus_dist in RFann2; desf.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfs)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfs; repeat (apply conj); try (eby eapply LST); try edone.
        by red in REL; desf.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hN), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC (lupd _ _)).
          eapply hplus_sim_def.
            eby eapply lupd_sim, assn_sem_def.
          rewrite <- hplusA; eapply hplus_sim_def; eauto.
          by rewrite !hplusA, !(hplusAC hN), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hN, (lupd hN HLnabla),
              (lupd hAcq HLnabla), (lupd hAcq HLnabla), (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hdrop +!+ hFR).
        rewrite !hplusA, !(hplusAC hN), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA, !(hplusAC (lupd _ _)), !(hplusAC hdrop), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      × ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (NTdef: hN +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hN), (hplusAC hT), <- !hplusA in IND.
          repeat (apply hplus_not_undef_l in IND; try done).
        }
        ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj).
          2: by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
          by rewrite assn_sem_assn_norm; eapply IMPrel; try edone; ins; repeat eexists.
        apply exact_label_hplus_dist in RFann2.
        apply exact_label_hplus_dist_inv; desf.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × by apply Hsim_refl; destruct hAcq.
      × red in REL; desf; red; red; vauto.
      × by left; apply lupd_label.
    }
  }

  Grab Existential Variables. all: done.
Qed.

Theorem rule_cas_acq PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi : val → Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (ACQ: acquire_typ rmw_typ)
    (FAIL: triple (rmw_precondition (Atriangle P) E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else (RR x))),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi AA) else RR x).
Proof.
  ins; eapply triple_helper_start; ins; desf; ins; desf; try done.
  Focus 2.     exploit (FAIL (fst :: nil) (Some v') lab sb fst fst); eauto; ins; eauto.
    by repeat (eexists; try edone).
    by instantiate (1 := S n) in x0; ins; desf; desf;
       exploit GUAR; clear POST RELY GUAR; try eassumption; eauto.
  clear FAIL.

  assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.

  rename h5 into hP.

  rewrite <- !hplusA in pEQ.
  rewrite hplus_hsingl_rel_rmwacq in pEQ; ins.
  rewrite hplus_init1 in pEQ; ins.

  assert (Z: ∃ hoo goo QQ labW labR, hmap (hb_sb prev fst) = Hdef hoo goo ∧
                    hoo E = HVra QQ (fun x : val ⇒ mk_assn_mod (QQacq x))
                                 true (ohlplus labW HLnormal) (ohlplus labR HLnormal)).
  {
    rewrite pEQ in *; clear -pDEF.
    rewrite hplusA in *; destruct (hP +!+ hFR); ins.
    rewrite hplus_unfold in *; desf; desf.
    specialize (HEAPcompat E); rewrite hupds in *; ins; desf; desf.
    × repeat eexists. ins.
      rewrite hupds, Heq; ins.
      f_equal; try by instantiate (1 := None).
      extensionality v; desf.
    × eexists _, _, _, permlbl, init; repeat split; try done.
      by ins; rewrite hupds, Heq.
  }
  desc.

  assert (∃ wri, << RF : rf fst = Some wri >> ∧ << WRI: is_writeLV (lab wri) E E' >>).
  {
    red in CONS; desc; assert (C := (Crf fst)); desf.
    × repeat eexists; desf; simpls; vauto.
      by rewrite SEM1 in *; ins; desf.
    × exfalso.
      red in FST; desf.
      exploit initialization_always_before; try exact Z; try exact (proj1 VALID); eauto.
         instantiate (2 := E); instantiate (1 := HLnormal).
         rewrite Z0; ins. destruct labR; ins; vauto.
         by destruct h; ins; unfold is_normal; eauto.
      ins; desf.
      eapply (C a); eauto.
        2: eby rewrite SEM1.
      clear - HB FST.
      apply clos_refl_trans_hbE in HB; desf; eauto with hb.
  }
  desc.

  assert (INwri: In wri V).
  {
    exploit HC0; eauto using In_eq; ins; desf; vauto.
    exfalso; red in CONS; desc; eapply ACYC; vauto.
  }
  
  assert (VALIDwri := VLD _ INwri).
  red in VALIDwri; destruct (lab wri) eqn: LABwri; ins; desc; subst.
  destruct DISJ; desc.

  {
    red in CONS, FST, pU; desf.
    exfalso; eapply atomicity_is_globally_exclusive; try exact (proj1 VALID);
             try (eby apply is_lvalue_implies_is_nonatomic); try exact Z; eauto; ins.
    by eapply HC; vauto.
    by rewrite Z0.
  }

  {
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfs)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
        ins; clear TYP; red in CONS; desf; ins.
        exploit wellformed_one_w; try exact (proj1 VALID); try exact H; try exact pEQ0;
                                  try exact (proj1 FST); try exact (proj1 pU); eauto.
        intro IMP; eapply (IMP V_PREV (proj1 FST)) in TRAN0; eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd h2 HLnabla); repeat split.
          by rewrite <- lupd_hplus_dist; apply lupd_eq.
          by apply lupd_label; intro U; rewrite U in *; desf.
        eexists; repeat split.
        eby apply assn_sem_assn_norm.
        by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
        by apply exact_label_hplus_dist in TRAN2; desf.
      clear - UPD TRAN0.
      symmetry in UPD; apply hplus_def_inv in UPD; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRAN0; desf.
      by rewrite e in TRAN0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
       ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { clear TYP; red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        eexists _, _, _, _; repeat (split; try edone).
          eby subst hmap'; ins.
        right; split; try done.
        ∃ rfs, hr, hF, P0, sbg, rfg.
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfs)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          clear TYP; rewrite <- rfsOK in RF.
          apply In_implies_perm in RF as [rfs' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        rewrite <- SAME, HM' in *; unnw; repeat (split; try done).
        eby eexists; split.
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        clear TYP; ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    clear TYP.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND;
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (A := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct A as [z A]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    assert (ADEF: hAcq ≠ Hundef) by (intro; desf).
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact A2; try exact pSAT9.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      do 3 apply hplus_not_undef_l in IND.
      eby eapply hplus_sim_def.
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                            true (Some HLCnormal) (Some HLCnormal))
               +!+ hAcq +!+ hFR )
       (hs := lupd (hP +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _), _; split; [ | split]; try edone.
        3: eby apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        2: by rewrite hplusC, hplusA.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA , !(hplusAC hP), !(hplusAC hT) in IND.
      do 2 (apply hplus_not_undef_r in IND).
      by rewrite hplusAC.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      rename rfs0 into rfsOut.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfsOut)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfsOut; repeat (apply conj); try (eby eapply LST); try edone.
        by red in ACQ; desf.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hP), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC hAcq).
          rewrite <- hplusA; eapply hplus_sim_def; eauto.
          by rewrite !(hplusAC hP), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hP, (lupd hP HLnabla),
              (lupd hAcq HLnabla), hAcq, (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hFR).
        rewrite !hplusA, !(hplusAC hP), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA.
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      × ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (PTdef: hP +!+ hT ≠ Hundef ∧ h' +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
          do 3 apply hplus_not_undef_l in IND; split; try done.
          eby eapply hplus_sim_def.
        }
        desc; ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        ∃ (h' +!+ hT); repeat (apply conj).
        by rewrite assn_sem_assn_norm; eapply IMPrel; try edone; ins; repeat eexists.
        by rewrite <- lupd_hplus_dist; apply lupd_sim2, hplus_sim; try done; apply Hsim_refl;
           intro; desf; rewrite hplus_undef_r in ×.
        by apply exact_label_hplus_dist in RFann2; desf; apply exact_label_hplus_dist_inv.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × by apply Hsim_sym, lupd_sim; destruct hAcq.
      × red; red; vauto.
      × apply exact_label_hplus_dist in RFann2; red in ACQ; desf; red; red; vauto.
    }
  }
    
  {
    RMWin_heap.
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfsOut)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOutOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
      {
        ins; red in CONS; desf; ins.
        assert (WLV: is_writeLV (lab wri) E E') by (by rewrite LABwri).
        exploit wellformed_one; try exact WLV; try exact (proj1 VALID); try exact H; try exact DEFin;
                                   try exact (proj1 pU); eauto.
        intro IMP; eapply IMP in TRANout0; try exact (proj1 FST); eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd (h2 +!+ rfg) HLnabla); repeat split.
        × rewrite <- lupd_hplus_dist; apply lupd_eq; rewrite rOutEQ.
          + rewrite <- !hplusA; apply hplus_sim; try done.
            by apply Hsim_refl; intro U; rewrite U, !hplus_undef_r in *; congruence.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
          + rewrite <- hplusA; apply exact_label_hplus_dist_inv; try done.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
            by apply hplus_eq_gheap in ghostEQ; desf; vauto.
        × by apply lupd_label; intro U; rewrite U in *; desf.
        × eexists; repeat split.
          eby apply assn_sem_assn_norm.
          by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
          by apply exact_label_hplus_dist in TRANout2; desf.
      }
      rewrite pEQ0, !hplusA in DEFin; clear - DEFin TRANout0.
      destruct (hrel +!+ hF +!+ hsum (map hmap (map (hb_rf^~ wri) rfsIn))); ins.
      apply hplus_def_inv in DEFin; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRANout0; desf.
      by rewrite e in TRANout0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
      ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfsOut)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          rewrite <- rfsOutOK in RF.
          apply In_implies_perm in RF as [rfsOut' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        ∃ pre, post, rfsIn, rfsOut; repeat (split; try done).
          by rewrite SAME; subst hmap'; unfold mupd; desf; desf.
        ∃ P0, QQ0, hrel, hrel', hacq, hacq', ht, hF, sbg, rfg.
        Opaque assn_sem.
        rewrite <- SAME, HM' in *; unnw; repeat (apply conj; try done).
        Transparent assn_sem.
        by rewrite !map_upd_irr; ins; intro; desf.
        eby ins; split; try done; eexists; repeat (apply conj).
        eby ins; split; try done; eexists; repeat (apply conj).
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND;
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (A := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct A as [z A]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    assert (ADEF: hAcq ≠ Hundef) by (intro; desf).
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact A2; try exact pSAT9.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      do 3 apply hplus_not_undef_l in IND.
      eby eapply hplus_sim_def.
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                            true (Some HLCnormal) (Some HLCnormal))
               +!+ hAcq +!+ hFR )
       (hs := lupd (hP +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _), _; split; [ | split]; try edone.
        3: eby apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        2: by rewrite hplusC, hplusA.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA , !(hplusAC hP), !(hplusAC hT) in IND.
      do 2 (apply hplus_not_undef_r in IND).
      by rewrite hplusAC.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfs)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfs; repeat (apply conj); try (eby eapply LST); try edone.
        by red in ACQ; desf.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hP), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC hAcq).
          rewrite <- hplusA; eapply hplus_sim_def; eauto.
          by rewrite !(hplusAC hP), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hP, (lupd hP HLnabla),
              (lupd hAcq HLnabla), hAcq, (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hFR).
        rewrite !hplusA, !(hplusAC hP), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA.
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      ×ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (PTdef: hP +!+ hT ≠ Hundef ∧ h' +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
          do 3 apply hplus_not_undef_l in IND; split; try done.
          eby eapply hplus_sim_def.
        }
        desc; ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        ∃ (h' +!+ hT); repeat (apply conj).
        by rewrite assn_sem_assn_norm; eapply IMPrel; try edone; ins; repeat eexists.
        by rewrite <- lupd_hplus_dist; apply lupd_sim2, hplus_sim; try done; apply Hsim_refl;
           intro; desf; rewrite hplus_undef_r in ×.
        by apply exact_label_hplus_dist in RFann2; desf; apply exact_label_hplus_dist_inv.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × by apply Hsim_sym, lupd_sim; destruct hAcq.
      × red; red; vauto.
      × apply exact_label_hplus_dist in RFann2; red in ACQ; desf; red; red; vauto.
    }
  }

  Grab Existential Variables. all: done.
Qed.

Theorem rule_cas_rlx PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi : val → Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AT: rmw_typ ≠ ATna)
    (FAIL: triple (rmw_precondition (Atriangle P) E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else (RR x))),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi (fun y ⇒ Anabla (AA y))) else RR x).
Proof.
  ins; eapply triple_helper_start; ins; desfh; ins; desfh.
  Focus 2.     exploit (FAIL (fst :: nil) (Some v') lab sb fst fst); eauto; ins; eauto.
    by repeat (eexists; try edone).
    by instantiate (1 := S n) in x0; ins; desf; desf;
       exploit GUAR; clear POST RELY GUAR; try eassumption; eauto.
  clear FAIL; rewrite eqxx.

  assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.

  rename h5 into hP.

  rewrite <- !hplusA in pEQ.
  rewrite hplus_hsingl_rel_rmwacq in pEQ; ins.
  rewrite hplus_init1 in pEQ; ins.

  assert (Z: ∃ hoo goo QQ labW labR, hmap (hb_sb prev fst) = Hdef hoo goo ∧
                    hoo E = HVra QQ (fun x : val ⇒ mk_assn_mod (QQacq x))
                                 true (ohlplus labW HLnormal) (ohlplus labR HLnormal)).
  {
    rewrite pEQ in *; clear -pDEF.
    rewrite hplusA in *; destruct (hP +!+ hFR); ins.
    rewrite hplus_unfold in *; desf; desf.
    specialize (HEAPcompat E); rewrite hupds in *; ins; desf; desf.
    × repeat eexists. ins.
      rewrite hupds, Heq; ins.
      f_equal; try by instantiate (1 := None).
      extensionality v; desf.
    × eexists _, _, _, permlbl, init; repeat split; try done.
      by ins; rewrite hupds, Heq.
  }
  desc.

  assert (∃ wri, << RF : rf fst = Some wri >> ∧ << WRI: is_writeLV (lab wri) E E' >>).
  {
    red in CONS; desc; assert (C := (Crf fst)); desf.
    × repeat eexists; desf; simpls; vauto.
      by rewrite SEM1 in *; ins; desf.
    × exfalso.
      red in FST; desf.
      exploit initialization_always_before; try exact Z; try exact (proj1 VALID); eauto.
         instantiate (2 := E); instantiate (1 := HLnormal).
         rewrite Z0; ins. destruct labR; ins; vauto.
         by destruct h; ins; unfold is_normal; eauto.
      ins; desf.
      eapply (C a); eauto.
        2: eby rewrite SEM1.
      clear - HB FST.
      apply clos_refl_trans_hbE in HB; desf; eauto with hb.
  }
  desc.

  assert (INwri: In wri V).
  {
    exploit HC0; eauto using In_eq; ins; desf; vauto.
    exfalso; red in CONS; desc; eapply ACYC; vauto.
  }
  
  assert (VALIDwri := VLD _ INwri).
  red in VALIDwri; destruct (lab wri) eqn: LABwri; ins; desc; subst.
  destruct DISJ; desc.

  {
    red in CONS, FST, pU; desf.
    exfalso; eapply atomicity_is_globally_exclusive; try exact (proj1 VALID);
             try (eby apply is_lvalue_implies_is_nonatomic); try exact Z; eauto; ins.
    by eapply HC; vauto.
    by rewrite Z0.
  }

  {
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfs)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
        ins; clear TYP; red in CONS; desf; ins.
        exploit wellformed_one_w; try exact (proj1 VALID); try exact H; try exact pEQ0;
                                  try exact (proj1 FST); try exact (proj1 pU); eauto.
        intro IMP; eapply (IMP V_PREV (proj1 FST)) in TRAN0; eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd h2 HLnabla); repeat split.
          by rewrite <- lupd_hplus_dist; apply lupd_eq.
          by apply lupd_label; intro U; rewrite U in *; desf.
        eexists; repeat split.
        eby apply assn_sem_assn_norm.
        by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
        by apply exact_label_hplus_dist in TRAN2; desf.
      clear - UPD TRAN0.
      symmetry in UPD; apply hplus_def_inv in UPD; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRAN0; desf.
      by rewrite e in TRAN0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
       ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { clear TYP; red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        eexists _, _, _, _; repeat (split; try edone).
          eby subst hmap'; ins.
        right; split; try done.
        ∃ rfs, hr, hF, P0, sbg, rfg.
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfs)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          clear TYP; rewrite <- rfsOK in RF.
          apply In_implies_perm in RF as [rfs' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        rewrite <- SAME, HM' in *; unnw; repeat (split; try done).
        eby eexists; split.
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        clear TYP; ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    clear TYP.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND;
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (ACQ := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct ACQ as [z ACQ]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    assert (ADEF: hAcq ≠ Hundef) by (intro; desf).
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact ACQ2; try exact pSAT9.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      do 3 apply hplus_not_undef_l in IND.
      eby eapply hplus_sim_def.
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                            true (Some HLCnormal) (Some HLCnormal))
               +!+ (lupd hAcq HLnabla) +!+ hFR )
       (hs := lupd (hP +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _), (lupd hAcq HLnabla); split; [ | split].
      × apply (hplus_sim_def _ RFann1) in IND.
        rewrite !hplusA in IND; apply (hplus_sim_def _ (lupd_sim HLnabla ADEF)) in IND.
        rewrite !(hplusAC hP), !(hplusAC hT) in IND.
        do 2 (apply hplus_not_undef_r in IND).
        by rewrite hplusAC.
      × by rewrite (hplusAC (lupd hAcq _)), (hplusC _ hFR).
      × apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        split.
          by apply lupd_label.
        eexists; repeat (apply conj; try edone).
        by apply Hsim_sym, lupd_sim.
        by apply exact_label_hplus_dist in RFann2; desf.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      rename rfs0 into rfsOut.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfsOut)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfsOut; repeat (apply conj); try (eby eapply LST); try edone.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hP), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC (lupd _ _)).
          eapply hplus_sim_def.
            eby eapply lupd_sim, assn_sem_def.
          rewrite <- hplusA; eapply hplus_sim_def; eauto.
          by rewrite !(hplusAC hP), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hP, (lupd hP HLnabla),
              (lupd hAcq HLnabla), (lupd hAcq HLnabla), (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hFR).
        rewrite !hplusA, !(hplusAC hP), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA.
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      × ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (PTdef: hP +!+ hT ≠ Hundef ∧ h' +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
          do 3 apply hplus_not_undef_l in IND; split; try done.
          eby eapply hplus_sim_def.
        }
        desc; ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        ∃ (h' +!+ hT); repeat (apply conj).
        by rewrite assn_sem_assn_norm; apply IMPrel; ins; repeat eexists.
        by rewrite <- lupd_hplus_dist; apply lupd_sim2, hplus_sim; try done; apply Hsim_refl;
           intro; desf; rewrite hplus_undef_r in ×.
        by apply exact_label_hplus_dist in RFann2; desf; apply exact_label_hplus_dist_inv.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × by apply Hsim_refl; destruct hAcq.
      × red; red; vauto.
      × by left; apply lupd_label; destruct hAcq.
    }
  }
    
  {
    RMWin_heap.
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfsOut)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOutOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
      {
        ins; red in CONS; desf; ins.
        assert (WLV: is_writeLV (lab wri) E E') by (by rewrite LABwri).
        exploit wellformed_one; try exact WLV; try exact (proj1 VALID); try exact H; try exact DEFin;
                                   try exact (proj1 pU); eauto.
        intro IMP; eapply IMP in TRANout0; try exact (proj1 FST); eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd (h2 +!+ rfg) HLnabla); repeat split.
        × rewrite <- lupd_hplus_dist; apply lupd_eq; rewrite rOutEQ.
          + rewrite <- !hplusA; apply hplus_sim; try done.
            by apply Hsim_refl; intro U; rewrite U, !hplus_undef_r in *; congruence.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
          + rewrite <- hplusA; apply exact_label_hplus_dist_inv; try done.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
            by apply hplus_eq_gheap in ghostEQ; desf; vauto.
        × by apply lupd_label; intro U; rewrite U in *; desf.
        × eexists; repeat split.
          eby apply assn_sem_assn_norm.
          by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
          by apply exact_label_hplus_dist in TRANout2; desf.
      }
      rewrite pEQ0, !hplusA in DEFin; clear - DEFin TRANout0.
      destruct (hrel +!+ hF +!+ hsum (map hmap (map (hb_rf^~ wri) rfsIn))); ins.
      apply hplus_def_inv in DEFin; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRANout0; desf.
      by rewrite e in TRANout0.
    }
    red in CONS; desc.
    remember (mupd (mupd hmap (hb_rf wri fst) hA) (hb_sink wri) hR) as hmap' eqn:HM'.
    assert (VAL'': ∀ e, In e V → hmap_valid lab sb rf hmap' (ga_clear ga fst) e).
    {
      ins; destruct (eqP e wri).
      × subst e; red; rewrite LABwri.
        ∃ gnew; split.
          { red; ins; split.
            by intro X; apply NG in X; unfold ga_clear; desf.
            by ins; apply NG; unfold ga_clear in *; desf.
          }
        assert(SAME: hsum (map hmap' (map (hb_rf wri) rfsOut)) +!+ hmap' (hb_sink wri) = hmap (hb_sink wri)).
        {
          rewrite <- rfsOutOK in RF.
          apply In_implies_perm in RF as [rfsOut' PERM].
          rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
          rewrite !hsum_cons.
          rewrite HM', !map_upd_irr; ins.
            2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
          unfold mupd; desf; desf.
          rewrite (hsum_perm (map_perm _ (map_perm _ PERM))) in RFempty; ins.
          rewrite hsum_cons, hplus_eq_emp in RFempty; desc.
          by rewrite RFempty0, !hplus_emp_r.
        }
        ∃ pre, post, rfsIn, rfsOut; repeat (split; try done).
          by rewrite SAME; subst hmap'; unfold mupd; desf; desf.
        ∃ P0, QQ0, hrel, hrel', hacq, hacq', ht, hF, sbg, rfg.
        Opaque assn_sem.
        rewrite <- SAME, HM' in *; unnw; repeat (apply conj; try done).
        Transparent assn_sem.
        by rewrite !map_upd_irr; ins; intro; desf.
        eby ins; split; try done; eexists; repeat (apply conj).
        eby ins; split; try done; eexists; repeat (apply conj).
      × subst hmap'; eapply hmap_irr_change_valid.
          by apply VLD.
          by apply ga_clear_agrees; congruence.
        ins; unfold mupd; desf; desf; ins; desf.
    }
    assert (VAL': hmap_valids lab sb rf hmap' V).
      by eexists; split; try exact VAL''; eauto using ga_clear_fin.
    assert (IND: independent sb rf (hb_rf wri fst :: hb_sb prev fst :: nil)).
      by desc; eapply independent_when_sharing_second_node; ins; eauto; exact (proj1 FST).
    eapply independent_heap_compat with (V:=V) in IND; try exact VAL'; eauto; ins; red in FST; desf; desf.
      2: by constructor; ins; intro; desf; desf.
    pattern g0 in IND; apply ex_intro in IND;
    pattern h in IND; apply ex_intro in IND; rewrite <- hdef_alt in IND.
    rewrite hsum_two in IND; unfold mupd in IND; desf; desf.
    rewrite pEQ, !hplusA in IND.
    ins; desf.
    assert (ACQ := proj1 (assn_sem_exists _ _) (IMPacq _ RFann0)).
    destruct ACQ as [z ACQ]; ins; desf.
    rename h1 into hAcq; rename h2 into hT.
    specialize (IMPrel z); unfold satisfying in IMPrel; desf.
    assert (ADEF: hAcq ≠ Hundef) by (intro; desf).
    Focus 2.
      exploit IMPrel; ins.
      eexists _, _; repeat split; try exact ACQ2; try exact pSAT9.
      apply (hplus_sim_def _ RFann1) in IND.
      rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
      do 3 apply hplus_not_undef_l in IND.
      eby eapply hplus_sim_def.
    eapply safe_final4a with
       (h := hsingl _ _ E (HVra (fun x ⇒ mk_assn_mod (QQrel x)) (fun x ⇒ mk_assn_mod (QQacq x))
                            true (Some HLCnormal) (Some HLCnormal))
               +!+ (lupd hAcq HLnabla) +!+ hFR )
       (hs := lupd (hP +!+ hT) HLnabla )
       (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    {
      eexists (hsingl _ _ E _), (lupd hAcq HLnabla); split; [ | split].
      × apply (hplus_sim_def _ RFann1) in IND.
        rewrite !hplusA in IND; apply (hplus_sim_def _ (lupd_sim HLnabla ADEF)) in IND.
        rewrite !(hplusAC hP), !(hplusAC hT) in IND.
        do 2 (apply hplus_not_undef_r in IND).
        by rewrite hplusAC.
      × by rewrite (hplusAC (lupd hAcq _)), (hplusC _ hFR).
      × apply assn_sem_exists; ∃ z; unfold satisfying; des_if.
        split.
          by apply lupd_label.
        eexists; repeat (apply conj; try edone).
        by apply Hsim_sym, lupd_sim.
        by apply exact_label_hplus_dist in RFann2; desf.
    }
    {
      red; rewrite SEM1.
      ∃ gres_emp; split.
        by unfold ga_clear; split; ins; desf.
      assert (RFS := has_rf_succs fst FIN Crf); desf.
      assert (RFempty': hsum (map hmap (map (hb_rf fst) rfs)) = hemp).
        by apply hsum_eq_emp; ins; repeat (rewrite In_map in *; desf); eapply VALID; eauto.
      eexists _, _, (wri :: nil), rfs; repeat (apply conj); try (eby eapply LST); try edone.
        by split; ins; desf; eauto.
        { rewrite !map_upd_irr; ins; try congruence.
          rewrite RFempty', hplus_emp_l.
          unfold mupd; ins; desf; desf.
          rewrite hplusC.
          eapply hplus_sim_def.
          { apply lupd_sim.
            eapply hplus_sim_def in IND; try exact RFann1.
            rewrite !hplusA, hplusAC, !(hplusAC hP), <- hplusA in IND.
            eby eapply hplus_not_undef_l.
          }
          rewrite !hplusA, hplusAC, !(hplusAC (lupd _ _)).
          eapply hplus_sim_def.
            eby eapply lupd_sim, assn_sem_def.
          rewrite <- hplusA; eapply hplus_sim_def; eauto.
          by rewrite !(hplusAC hP), hplusAC in IND.
        }
      eexists (mk_assn_mod (QQrel E'')), (fun x ⇒ mk_assn_mod (QQacq x)), hP, (lupd hP HLnabla),
              (lupd hAcq HLnabla), (lupd hAcq HLnabla), (lupd hT HLnabla), _, hemp, hemp.
      Opaque assn_sem.
      repeat (apply conj).
      Transparent assn_sem.
      × unfold mupd; ins; desf; desf. rewrite pEQ.
        instantiate (1 := hsingl _ _ E (HVra (fun x : val ⇒ mk_assn_mod (QQrel x))
                                             (fun x : val ⇒ mk_assn_mod (QQacq x))
                                             true (Some HLCnormal) (Some HLCnormal))
                          +!+ hFR).
        rewrite !hplusA, !(hplusAC hP), !(hplusC _ hFR), !(hplusAC hFR).
        red; repeat f_equal. rewrite hplus_hsingl.
        by clear; f_equal; exten; ins; unfold hupd; desf; desf; f_equal; exten; ins; desf; desf.
        by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
      × unfold mupd; ins; desf; desf.
        by rewrite hsum_one, <- lupd_hplus_dist; apply lupd_eq.
      × unfold mupd; ins; desf; desf.
        rewrite hplus_emp_r, (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl.
          2: by split; ins; vauto; red; unfold hupd; desf; desf; ins; eauto.
        clear; ins; rewrite !hplusA.
        red; repeat f_equal; ins; exten; ins; unfold hupd; desf; desf.
      × rewrite hplus_emp_r, !map_upd_irr; ins.
          2: by intro; desf.
        unfold mupd; ins; desf; desf.
        by rewrite RFempty', hplus_emp_l, lupd_hplus_dist.
      × by rewrite hplus_emp_r.
      × ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        eexists; repeat (apply conj); rewrite ?assn_sem_assn_norm; try edone.
        by rewrite <- lupd_hplus_dist; apply Hsim_sym, lupd_sim.
      × assert (PTdef: hP +!+ hT ≠ Hundef ∧ h' +!+ hT ≠ Hundef).
        {
          apply (hplus_sim_def _ RFann1) in IND.
          rewrite !hplusA, !(hplusAC hP), (hplusAC hT), <- !hplusA in IND.
          do 3 apply hplus_not_undef_l in IND; split; try done.
          eby eapply hplus_sim_def.
        }
        desc; ins; split.
          by rewrite <- lupd_hplus_dist; apply lupd_label.
        ∃ (h' +!+ hT); repeat (apply conj).
        by rewrite assn_sem_assn_norm; apply IMPrel; ins; repeat eexists.
        by rewrite <- lupd_hplus_dist; apply lupd_sim2, hplus_sim; try done; apply Hsim_refl;
           intro; desf; rewrite hplus_undef_r in ×.
        by apply exact_label_hplus_dist in RFann2; desf; apply exact_label_hplus_dist_inv.
      × apply lupd_sim.
        by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      × by apply Hsim_refl; destruct hAcq.
      × red; red; vauto.
      × by left; apply lupd_label; destruct hAcq.
    }
  }

  Grab Existential Variables. all: done.
Qed.

Theorem rule_cas_shortcut PS PSg:
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq RR
    (UNSAT: implies (Astar (QQacq E') P) Afalse)
    (FAIL: triple (rmw_precondition P E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else RR x)),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Afalse else RR x).
Proof.
  ins; eapply triple_helper_start; ins; desfh; ins; desfh.
  Focus 2.     exploit (FAIL (fst :: nil) (Some v') lab sb fst fst); eauto; ins; eauto.
    by repeat eexists.
    by instantiate (1 := S n) in x0; ins; desf; desf;
       exploit GUAR; clear POST RELY GUAR; try eassumption; eauto.
  clear FAIL; exfalso.

  assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.

  rename h5 into hP.

  rewrite <- !hplusA in pEQ.
  rewrite hplus_hsingl_rel_rmwacq in pEQ; ins.
  rewrite hplus_init1 in pEQ; ins.

  assert (Z: ∃ hoo goo QQ labW labR, hmap (hb_sb prev fst) = Hdef hoo goo ∧
                    hoo E = HVra QQ (fun x : val ⇒ mk_assn_mod (QQacq x))
                                 true (ohlplus labW HLnormal) (ohlplus labR HLnormal)).
  {
    rewrite pEQ in *; clear -pDEF.
    rewrite hplusA in *; destruct (hP +!+ hFR); ins.
    rewrite hplus_unfold in *; desf; desf.
    specialize (HEAPcompat E); rewrite hupds in *; ins; desf; desf.
    × repeat eexists. ins.
      rewrite hupds, Heq; ins.
      f_equal; try by instantiate (1 := None).
      extensionality v; desf.
    × eexists _, _, _, permlbl, init; repeat split; try done.
      by ins; rewrite hupds, Heq.
  }
  desc.

  assert (∃ wri, << RF : rf fst = Some wri >> ∧ << WRI: is_writeLV (lab wri) E E' >>).
  {
    red in CONS; desc; assert (C := (Crf fst)); desf.
    × repeat eexists; desf; simpls; vauto.
      by rewrite SEM1 in *; ins; desf.
    × exfalso.
      red in FST; desf.
      exploit initialization_always_before; try exact Z; try exact (proj1 VALID); eauto.
         instantiate (2 := E); instantiate (1 := HLnormal).
         rewrite Z0; ins. destruct labR; ins; vauto.
         by destruct h; ins; unfold is_normal; eauto.
      ins; desf.
      eapply (C a); eauto.
        2: eby rewrite SEM1.
      clear - HB FST.
      apply clos_refl_trans_hbE in HB; desf; eauto with hb.
  }
  desc.

  assert (INwri: In wri V).
  {
    exploit HC0; eauto using In_eq; ins; desf; vauto.
    exfalso; red in CONS; desc; eapply ACYC; vauto.
  }
  

  assert (VALIDwri := VLD _ INwri).
  red in VALIDwri; destruct (lab wri) eqn: LABwri; ins; desc; subst.
  destruct DISJ; desc.

  {
    red in CONS, FST, pU; desf.
    exfalso; eapply atomicity_is_globally_exclusive; try exact (proj1 VALID);
             try (eby apply is_lvalue_implies_is_nonatomic); try exact Z; eauto; ins.
    by eapply HC; vauto.
    by rewrite Z0.
  }

  {
    clear TYP.
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfs)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
        ins; red in CONS; desf; ins.
        exploit wellformed_one_w; try exact (proj1 VALID); try exact H; try exact pEQ0;
                                  try exact (proj1 FST); try exact (proj1 pU); eauto.
        intro I; eapply (I V_PREV (proj1 FST)) in TRAN0; eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd h2 HLnabla); repeat split.
          by rewrite <- lupd_hplus_dist; apply lupd_eq.
          by apply lupd_label; intro U; rewrite U in *; desf.
        eexists; repeat split.
        eby apply assn_sem_assn_norm.
        by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
        by apply exact_label_hplus_dist in TRAN2; desf.
      clear - UPD TRAN0.
      symmetry in UPD; apply hplus_def_inv in UPD; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRAN0; desf.
      by rewrite e in TRAN0.
    }
    red in CONS; ins; desc.
    assert (IND: independent sb rf (hb_sb prev fst :: hb_sink wri :: nil)).
    {
      apply independent_two with (lab := lab); ins; eauto.
        by red in FST; desf.
        by red; rewrite LABwri.
        by intro; desf.
        2: by intro; desf.
      intro; desf.
      destruct NIN; eapply hist_closedD; eauto.
    }
    red in VALID; desc.
    eapply independent_heap_compat with (V := V) in IND; rewrite <- ?hdef_alt in IND; ins; desf; eauto.
      2: by constructor; ins; intro; desf; desf.
      2: exact (proj1 FST).
      2: red; desf.
    rewrite hsum_two, pEQ, WRIsinkDECOMP, !hplusA in IND.
    exploit UNSAT; ins.
    eexists _, _; repeat split.
      2: edone.
      2: edone.
    rewrite !(hplusAC hP), !(hplusAC hA), <- hplusA in IND.
    apply hplus_not_undef_l in IND.
    eby eapply hplus_sim_def.
  }
    
  {
    RMWin_heap.
    assert (RFempty: hsum (map hmap (map (hb_rf wri) rfsOut)) = hemp).
      by eapply rmw_concurrent_readers_transfer_no_ownership, rfsOutOK; eauto.
    rewrite RFempty, hplus_emp_l in ×.
    assert (∃ hA hR, << WRIsinkDECOMP: hmap (hb_sink wri) = hA +!+ hR >> ∧
                          << RFann: assn_sem (Anabla (QQacq E')) hA >>).
    {
      cut (∃ RelP AcqP isrmw labW labR, hf E = HVra RelP AcqP isrmw labW labR ∧ RelP E' = P0).
      {
        ins; red in CONS; desf; ins.
        assert (WLV: is_writeLV (lab wri) E E') by (by rewrite LABwri).
        exploit wellformed_one; try exact WLV; try exact (proj1 VALID); try exact H; try exact DEFin;
                                   try exact (proj1 pU); eauto.
        intro IMP; eapply IMP in TRANout0; try exact (proj1 FST); eauto; ins; desf.
        ∃ (lupd h1 HLnabla), (lupd (h2 +!+ rfg) HLnabla); repeat split.
        × rewrite <- lupd_hplus_dist; apply lupd_eq; rewrite rOutEQ.
          + rewrite <- !hplusA; apply hplus_sim; try done.
            by apply Hsim_refl; intro U; rewrite U, !hplus_undef_r in *; congruence.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
          + rewrite <- hplusA; apply exact_label_hplus_dist_inv; try done.
            by rewrite hplusA; intro U; rewrite rOutEQ, U, hplus_undef_r in DEF.
            by apply hplus_eq_gheap in ghostEQ; desf; vauto.
        × by apply lupd_label; intro U; rewrite U in *; desf.
        × eexists; repeat split.
          eby apply assn_sem_assn_norm.
          by apply Hsim_sym, lupd_sim; intro U; rewrite U in *; desf.
          by apply exact_label_hplus_dist in TRANout2; desf.
      }
      rewrite pEQ0, !hplusA in DEFin; clear - DEFin TRANout0.
      destruct (hrel +!+ hF +!+ hsum (map hmap (map (hb_rf^~ wri) rfsIn))); ins.
      apply hplus_def_inv in DEFin; desf.
      specialize (DEFv E); specialize (PLUSv E); unfold initialize in PLUSv; rewrite !hupds in *; ins.
      destruct (hf E), (hz E); ins; inv PLUSv; repeat eexists; eauto; instantiate; ins; rewrite hupds; try done.
      clear - TRANout0; desf.
      by rewrite e in TRANout0.
    }
    red in CONS; desc.
    assert (IND: independent sb rf (hb_sb prev fst :: hb_sink wri :: nil)).
    {
      apply independent_two with (lab := lab); ins; eauto.
        by red in FST; desf.
        by red; rewrite LABwri.
        by intro; desf.
        2: by intro; desf.
      intro; desf.
      destruct NIN; eapply hist_closedD; eauto.
    }
    red in VALID; desc.
    eapply independent_heap_compat with (V := V) in IND; rewrite <- ?hdef_alt in IND; ins; desf; eauto.
      2: by constructor; ins; intro; desf; desf.
      2: exact (proj1 FST).
      2: red; desf.
    rewrite hsum_two, pEQ, WRIsinkDECOMP, !hplusA in IND.
    exploit UNSAT; ins.
    eexists _, _; repeat split.
      2: edone.
      2: edone.
    rewrite !(hplusAC hP), !(hplusAC hA), <- hplusA in IND.
    apply hplus_not_undef_l in IND.
    eby eapply hplus_sim_def.
  }
Qed.