Require Import Vbase Varith.
Require Import Relations Wellfounded Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 rslassn rslmodel rslassnlemmas rslhmap.

Set Implicit Arguments.

Lemma hplus_eq_ra_rmwD h h1 h2 l PP QQ init :
  hplus h1 h2 = Hdef h →
  h l = HVra PP QQ true init →
  ∃ hf PP' QQ' init',
    (h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' true init'.
Proof.
  ins; eapply hplus_def_inv in H; desf.
  specialize (DEFv l); rewrite PLUSv in *; clear PLUSv.
  red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
    repeat eexists; try edone; eauto.
Qed.

Lemma hsum_eq_ra_rmwD:
  ∀ h' hs l PP QQ init,
  hsum hs = Hdef h' →
  h' l = HVra PP QQ true init →
  ∃ h'' PP' QQ' init', In (Hdef h'') hs ∧ h'' l = HVra PP' QQ' true init'.
Proof.
  intros until 0; induction[h' PP QQ init] hs; ins; [by inv H|].
  rewrite hsum_cons in *; eapply hplus_eq_ra_rmwD in H; eauto.
  desf; eauto 8; exploit IHhs; eauto; ins; desf; eauto 8.
Qed.

Lemma hplus_eq_ra_ownD h h1 h2 l PP QQ init v :
  hplus h1 h2 = Hdef h →
  h l = HVra PP QQ false init →
  sval (QQ v) ≠ Aemp →
  sval (QQ v) ≠ Afalse →
  ∃ hf PP' QQ' init',
    (h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' false init'
    ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
  ins; eapply hplus_def_inv in H; desf.
  specialize (DEFv l); rewrite PLUSv in *; clear PLUSv.
  red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
    try solve [repeat (eexists; try eassumption); eauto].
  case_eq (sval (QQ0 v)); ins;
    try solve [clear Heq0; repeat (eexists; try eassumption); eauto;
               instantiate; congruence].
    case_eq (sval (QQ1 v)); ins;
    try solve [clear Heq; repeat (eexists; try eassumption); eauto;
               instantiate; congruence].
    by rewrite H, H0, assn_norm_star_false in ×.
    by rewrite H, H0, assn_norm_star_emp_r in ×.

  clear Heq; repeat (eexists; try eassumption); eauto.
  by intro H0; apply H1; rewrite H, H0, assn_norm_star_emp, assn_norm_emp.
  by intro H0; apply H2; rewrite H, H0, assn_norm_star_emp.
Qed.

Lemma hsum_eq_ra_ownD:
  ∀ h' hs l PP QQ init v,
  hsum hs = Hdef h' →
  h' l = HVra PP QQ false init →
  sval (QQ v) ≠ Aemp →
  sval (QQ v) ≠ Afalse →
  ∃ h'' PP' QQ' init',
    In (Hdef h'') hs ∧ h'' l = HVra PP' QQ' false init'
    ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
  intros until 0; induction[h' PP QQ init] hs; ins; [by inv H|].
  rewrite hsum_cons in *; eapply hplus_eq_ra_ownD in H; eauto.
  desf; eauto 10; exploit IHhs; eauto; ins; desf; eauto 12.
Qed.

Lemma hplus_ra_own_l h h1 h2 l PP QQ init v :
  hplus (Hdef h1) h2 = Hdef h →
  h1 l = HVra PP QQ false init →
  sval (QQ v) ≠ Aemp →
  sval (QQ v) ≠ Afalse →
  ∃ PP' QQ' init',
    h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
  ins; eapply hplus_def_inv in H; desf.
  specialize (DEFv l); rewrite PLUSv in *; clear PLUSv;
  red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
    try solve [repeat eexists; eauto].
    by exfalso; destruct (DEFv v); desf.
  repeat eexists; ins; intro; [
    apply assn_norm_star_eq_emp in H |
    apply assn_norm_star_eq_false in H ]; desf; auto;
    eapply H1; destruct (QQ v); ins; congruence.
Qed.

Lemma hplus_ra_own_r h h1 h2 l PP QQ init v :
  hplus h1 (Hdef h2) = Hdef h →
  h2 l = HVra PP QQ false init →
  sval (QQ v) ≠ Aemp →
  sval (QQ v) ≠ Afalse →
  ∃ PP' QQ' init',
    h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof. by rewrite hplusC; apply hplus_ra_own_l. Qed.

Lemma hsum_has_ra_own h hs hf l PP QQ init v :
  hsum hs = Hdef h →
  In (Hdef hf) hs →
  hf l = HVra PP QQ false init →
  sval (QQ v) ≠ Aemp →
  sval (QQ v) ≠ Afalse →
  ∃ PP' QQ' init',
    h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
  induction[h PP QQ init] hs; ins.
  rewrite hsum_cons in *; desf.
    eapply hplus_ra_own_l; eauto.
  exploit hplus_def_inv; eauto; ins; desf.
  exploit IHhs; eauto; intro; desf.
  rewrite x1 in *; eapply hplus_ra_own_r; eauto.
Qed.

Lemma go_back_one_acq :
  ∀ mt acts lab sb mo rf
    (FIN : ExecutionFinite acts lab sb)
    (CONS_A : ConsistentAlloc lab) hmap V
    (HC : hist_closed mt lab sb rf mo V) e
    (VALID : hmap_valid lab sb rf hmap e)
    (INe : In e V) hFR l
    (NALLOC : lab e ≠ Aalloc l)
    (ALLOC : ∀ hf loc,
               hFR = Hdef hf → hf loc ≠ HVnone →
               ∃ c : actid, lab c = Aalloc loc ∧ c ≠ e),
   ∃ pres_sb pres_sw posts_sb posts_sw,
     NoDup pres_sb ∧
     NoDup pres_sw ∧
     NoDup posts_sb ∧
     NoDup posts_sw ∧
     (∀ x : actid, In x pres_sb ↔ sb x e) ∧
     (∀ x : actid, In x pres_sw ↔ ann_sw lab rf x e) ∧
     (∀ x : actid, In x posts_sb ↔ sb e x) ∧
     (∀ x : actid, In x posts_sw ↔ ann_sw lab rf e x) ∧
     (∀ h
       (EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
            hsum (map hmap (map (hb_sw^~ e) pres_sw)) +!+ hFR =
            Hdef h),
      ∃ h0 : val → HeapVal,
        hsum (map hmap (map (hb_sb e) posts_sb)) +!+
        hsum (map hmap (map (hb_sw e) posts_sw)) +!+ hFR =
        Hdef h0 ∧
           ∀ PP' QQ' isrmw' init' (LA: h0 l = HVra PP' QQ' isrmw' init'),
             hvplus_ra2_ret (h l) QQ').
Proof.
  unfold hmap_valid, unique; ins; desf; desf.

  Case Askip.
    ∃ pres, nil, posts, nil; repeat (split; ins).
        by red in H; desf; rewrite Heq in ×.
      by red in H; desf; rewrite Heq in ×.
    eapply vshift_hack in qEQ.
    rewrite pEQ, qEQ, hplusA, hplusAC, hplusC in EQ.
    eapply hplus_def_inv in EQ; desf.
    repeat (eexists; try edone).
    eby rewrite PLUSv; intros; eapply hvplus_ra2.

  Case Aalloc.
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    by red in H; desf; rewrite Heq in ×.
    rewrite pEQ, qEQ in *; destruct hFR; ins.
    rewrite hplus_unfold in *; desf; vauto.
      eexists; split; ins; instantiate; ins.
      unfold hupd in LA; desf; desf; repeat (eexists; try edone).
      by rewrite LA; eexists; vauto.
    destruct n; intro l'; specialize (h0 l').
    unfold hupd in *; desf; desf.
    specialize (ALLOC _ l0 eq_refl).
    destruct (hf0 l0); desf; destruct ALLOC; desf;
    by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.

  Case Aalloc .
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    by red in H; desf; rewrite Heq in ×.
    rewrite pEQ, qEQ in *; destruct hFR; ins.
    rewrite hplus_unfold in *; desf; vauto.
      eexists; split; ins; instantiate; ins.
      unfold hupd in LA; desf; desf; repeat (eexists; try edone).
      by rewrite LA; eexists; vauto.
    destruct n; intro l'; specialize (h0 l').
    unfold hupd in *; desf; desf.
    specialize (ALLOC _ l0 eq_refl).
    destruct (hf0 l0); desf; destruct ALLOC; desf;
    by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.

  Case Aload .
    pose proof (has_sw_pres rf e FIN); desc.
    ∃ (pre :: nil), sws, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one in *; eauto.

    by red in H; desf; rewrite Heq in ×.
     rewrite qEQ, hsum_nil, hplus_emp_l;
        rewrite (hplusC _ hFR), <- hplusA in EQ.
     exploit hplus_def_inv; try eapply EQ; ins; desf.
     eexists; split; try edone; ins.
     rewrite PLUSv; eapply hvplus_ra2; eauto.

  Case Aload .
    ∃ (pre :: nil), sws, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    rewrite pEQ, swsEQ, <- pEQ', hplusA, (hplusAC _ hF),
            <- hplus_init1 with (init := true), hplusA,
            <- (hplusA _ hF), <- (hplusA _ (hplus _ hF)), <- qEQ, hplusC in EQ.
    eapply hplus_def_inv in EQ; ins; desf.
    repeat (eexists; try edone).
    intros; rewrite PLUSv; eapply hvplus_ra2; eauto.

  Case Astore .
    pose proof (has_sw_succs rf e FIN); desc.
    ∃ (pre :: nil), nil, (post :: nil), sws; ins; repeat (split; ins; desf);
      rewrite ?hsum_one in *; eauto.
      by red in H; desf; rewrite Heq in ×.
    assert (M: hsum (map hmap (map (hb_sw e) sws)) = hemp).
      generalize (fun x ⇒ proj1 (INsws x)); clear - wEQ.
      by induction sws; ins; rewrite hsum_cons, IHsws, hplus_emp_r; eauto.
    rewrite M; rewrite hsum_nil, pEQ, qEQ in ×.
    exploit (hdef_upd_alloc2); eauto.
    instantiate (1 := v); intro A; desf.
    repeat (eexists; try edone); intros.
    rewrite <- A0, LA; [by eexists; vauto|].
    by intro; subst; desf; clear - A LA;
       eapply hplus_raD in A; eauto; desc;
       clear N R; unfold hupd in *; desf; desf.

  Case Astore .
    ∃ (pre :: nil), nil, (post :: nil), sws; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    rewrite pEQ in ×.
    eapply vshift_hack in UPD.
    assert (∃ RR QQ isrmw init, hf l0 = HVra RR QQ isrmw init).
      clear - UPD; symmetry in UPD; eapply hplus_def_inv in UPD; desf.
      specialize (DEFv l0); eapply hvplus_ra2 in DEFv; eauto using hupds.
      rewrite <- PLUSv in DEFv; clear - DEFv.
      by unfold initialize in *; rewrite hupds in *; desf; eauto.
    desf.

    exploit (hplus_init_def2 _ l0 _ EQ); [congruence|intro X].
    generalize X; intro Z.
    rewrite UPD in X.
    rewrite !hplusA, !(hplusAC hsink), <- hplusA, hplusC in X.
    generalize X; intro Y.
    eapply hplus_def_inv in X; desf.
    repeat (eexists; try edone).
    ins; cut (hvplus_ra2_ret (initialize h l0 l) QQ').
      by clear; unfold initialize, hupd; desf; try rewrite Heq0.
    by rewrite PLUSv; eapply hvplus_ra2; eauto.

  Case Armw.
    ∃ (pre :: nil), swsIn, (post :: nil), swsOut; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    rewrite pEQ in ×.
    eapply vshift_hack in UPD.
    assert (∃ RR QQ isrmw init, hi l0 = HVra RR QQ isrmw init).
      clear - UPD; symmetry in UPD; eapply hplus_def_inv in UPD; desf.
      specialize (DEFv l0); eapply hvplus_ra2 in DEFv; eauto using hupds.
      rewrite <- PLUSv in DEFv; clear - DEFv.
      by destruct (hi l0); eauto.
    desf.

    rewrite <- hplusA, iEQ, UPD, !hplusA, !(hplusAC hsink), <- hplusA, hplusC in EQ.
    eapply hplus_def_inv in EQ; desc.
    eexists; split; try edone; ins.
    by rewrite PLUSv; eapply hvplus_ra2; eauto.
Qed.

Lemma go_back_one_acq2 :
  ∀ acts lab sb rf
    (FIN : ExecutionFinite acts lab sb)
    
    (CONS_A : ConsistentAlloc lab) hmap a
    (VALID : hmap_valid lab sb rf hmap a)
    hFR typ l v pre post sws
    (LL: lab a = Aload typ l v)
    (Lp: unique (sb^~ a) pre)
    (Lq: unique (sb a) post)
    (LwND: NoDup sws)
    (LwOK: ∀ x, In x sws ↔ ann_sw lab rf x a)
    hp hq hw PP QQ PP' QQ'
    (Ep: hmap (hb_sb pre a) = Hdef hp)
    (Eq: hmap (hb_sb a post) = Hdef hq)
    (Ew: hsum (map hmap (map (hb_sw^~ a) sws)) = Hdef hw)
    (Gp: hp l = HVra PP QQ false true)
    (Gq: hq l = HVra PP' QQ' false true) Q
    (NF: ¬ Asim Q Afalse)
    (L: << Gw : hw l = HVnone >> ∧
        << ASIM: Asim (sval (QQ v)) (Astar (sval (QQ' v)) Q) >>
     ∨ ∃ Pw' Qw' initw',
        << Gw : hw l = HVra Pw' Qw' false initw' >> ∧
        << ASIM: Asim (Astar (sval (QQ v)) (sval (Qw' v))) (Astar (sval (QQ' v)) Q) >>)
    (ALLOC : ∀ hf loc,
               hFR = Hdef hf →
               hf loc ≠ HVnone → ∃ c : actid, lab c = Aalloc loc ∧ c ≠ a) h
    (EQ: hmap (hb_sb pre a) +!+
         hsum (map hmap (map (hb_sw^~ a) sws)) +!+ hFR =
         Hdef h),
  ∃ h0 : val → HeapVal,
    hmap (hb_sb a post) +!+ hFR =
    Hdef h0 ∧
      ∀ PP' QQ' isrmw' (LA: h0 l = HVra PP' QQ' isrmw' true),
        ∃ PP0 QQ0, h l = HVra PP0 QQ0 isrmw' true ∧
        Asim (sval (QQ0 v)) (Astar (sval (QQ' v)) Q).
Proof.
  intros; unfold hmap_valid, unique in VALID; ins; rewrite LL in *; desc.
  eapply Lp in pU; eapply Lq in qU; subst pre0 post0; clear pU0 qU0.
  rewrite pEQ in *; clarify.
  destruct DISJ; desc.
     rewrite qEQ; rewrite (hplusC _ hFR), <- hplusA in EQ.
     exploit hplus_def_inv; try eapply EQ; ins; desc.
     eexists; split; try edone; ins.
     exfalso; eapply hplus_raD in x0; eauto; clear L; desf; congruence.

    assert (PRM: Permutation sws0 sws).
      by apply NoDup_Permutation; ins; rewrite swsOK, LwOK.
    assert (Hdef hw0 = Hdef hw); clarify.
      by rewrite <- swsEQ, <- Ew,
         (hsum_perm (Permutation_map _ (Permutation_map _ PRM))).

    simpls; rewrite Ew in *; clarify.
    rewrite <- pEQ', hplusA, (hplusAC _ hF),
            <- hplus_init1 with (init := true), hplusA,
            <- (hplusA _ hF), <- (hplusA _ (hplus _ hF)), <- qEQ, hplusC in EQ.
    eapply hplus_def_inv in EQ; ins; desc.
    eexists; split; try edone; ins.
    rewrite PLUSv, LA in *; rename DEFv into DDD; specialize (DDD l); clear PLUSv; desc; clarify.
    rewrite hupds, qEQ in ×.
    eapply hplus_def_inv in EQ; desc; clarify.
    rewrite EQ, PLUSv in *; desc; clarify.
    eapply hplus_def_inv in EQ; desc; clarify.
specialize (DEFv0 l); specialize (DEFv l).
rewrite PLUSv0 in ×.
    eapply hplus_def_inv in pEQ'; desc; clarify.
    specialize (DEFv1 l).
    rewrite hupds, PLUSv1 in *; clear hp PLUSv1 PLUSv hq PLUSv0 qEQ pEQ qD.
    eapply hplus_def_inv in EQ0; desc; clarify.
    simpl; do 2 eexists; split;f_equal; ins; auto using orbF.
    destruct isrmw'.
    { cut (Asim Aemp Q).
        by clear; intros H; eapply Asim_trans, Asim_star, H;
           eauto using Asim.
      specialize (DEFv2 l); rewrite PLUSv in *; des; rewrite Gw in *; ins;
      rewrite !hupds in *; ins; desf; rewrite hupds in *; ins; clarify; ins;
        desf; ins; desc; specialize (DDD v); rewrite hupds in *;
        red in DDD; ins; desf; rewrite ?DDD1 in *; ins; rewrite <- DDD in *; Asim_simpl_asm ASIM; try apply Asim1 in ASIM; desf; eauto using Asim.
      eapply Asim_trans in ASIM; [|eapply Asim_starC]; apply Asim1 in ASIM; desf; eauto using Asim.
    }
    specialize (DEFv2 l); rewrite PLUSv in *; des; rewrite Gw in *; ins;
    destruct (hz2 l); ins; clarify; ins; rewrite hupds in *; ins;
    destruct (hz l); ins; clarify; rewrite hupds in *;

    rewrite ?assn_norm_emp, ?Asim_norm_l, ?Asim_norm_r in *; simpls;
      Asim_simpl_asm ASIM; instantiate; Asim_simpl.

    by eauto using Asim.
    by eauto using Asim.
    by apply Asim_rem2; eauto using Asim.
    by eauto using Asim.
    by apply Asim_rem2; eauto using Asim.
    by eauto using Asim.
    by apply Asim_rem2; eauto using Asim.
Qed.

Lemma go_back_one_rel :
  ∀ lab sb rf hmap edge
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET: hmap edge = Hdef hf) l PP QQ isrmw init v
    (LA : hf l = HVra PP QQ isrmw init)
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge' hf',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = hb_fst edge ∧
    hmap edge' = Hdef hf' ∧
    ∃ PP' QQ' isrmw' init',
      hf' l = HVra PP' QQ' isrmw' init' ∧
      (∀ h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h).
Proof.
  unfold hmap_valid, unique; ins; desf; desf.
  Case Askip.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    eapply vshift_hack in qEQ.
    symmetry in qEQ.
    assert (X := hplus_def_inv _ _ qEQ); desf; rewrite X in ×.
    eapply hsum_raD in X; eauto; desf; desf.
    2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
    destruct isrmw'.
      eapply hplus_ram_lD in qEQ; try edone; desc; clear qEQ2; desf.
      eapply hsum_eq_raD with (v:=v) in pEQ; eauto.
      desf; repeat (rewrite In_map in *; desf); eapply pOK in pEQ3.
      by repeat (eexists; try edone); ins; apply pEQ1, qEQ0, X2.
    eapply hplus_ra_lD in qEQ; try edone; desc; clear qEQ2; desf.
    eapply hsum_eq_raD with (v:=v) in pEQ; eauto.
    desf; repeat (rewrite In_map in *; desf); eapply pOK in pEQ3.
    by repeat (eexists; try edone); ins; apply pEQ1, qEQ0, X2.

  Case Aalloc.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in *; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aalloc.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in *; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aload .
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    rewrite pEQ in *; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aload .
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    symmetry in qEQ; eapply hplus_eq_raD with (v:=v) in qEQ; eauto.
    desf.
      unfold hupd in qEQ0; desf; desf.
      ∃ (hb_sb pre e); eapply hplus_def_inv in pEQ'; desf.
      specialize (PLUSv l0); rewrite hupds in *; simpls.
      by desf; repeat (eexists; try edone); ins; try eapply qEQ1 in H.
    eapply hplus_eq_raD with (v:=v) in qEQ; eauto.
    desf.
      eapply hsum_eq_raD with (v:=v) in swsEQ; eauto; desc.
      repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
      repeat (eexists; try edone); ins; eauto.
      generalize (qEQ1 h), (qEQ3 h), (swsEQ1 h); clear - H; tauto.
    ∃ (hb_sb pre e); destruct (hmap (hb_sb pre e)); try done.
    eexists; repeat split; ins.
    destruct isrmw'0.
      eapply hplus_ram_rD in pEQ'; eauto; desc; clarify.
      by repeat eexists; try edone; intros; apply pEQ'0, qEQ3, qEQ1.
    eapply hplus_ra_rD in pEQ'; eauto; desc; clarify.
    by repeat eexists; try edone; intros; apply pEQ'0, qEQ3, qEQ1.

  Case Astore .
    destruct edge; ins; subst; try (by rewrite wEQ in GET; try done; inv GET); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in LA; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Astore .
    ∃ (hb_sb pre (hb_fst edge)); destruct (hmap (hb_sb pre (hb_fst edge))); try done.
    eexists; repeat split; ins.
    eapply vshift_hack in UPD.
    destruct edge; ins.
      symmetry in UPD.
      rewrite !(hplusAC (hsum _)) in UPD.
      exploit hplus_def_inv_l; eauto; intro Z; desf.
      exploit hsum_raD; eauto; [|intro W; desf].
        by rewrite <- GET; eapply In_mapI, In_mapI, swsOK.
      destruct isrmw'.
        rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
        eapply initialize_eq_raD in UPD; desc.
        by repeat eexists; try edone; intros; apply UPD0; eauto.
      rewrite Z in *; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
      eapply initialize_eq_raD in UPD; desc.
      by repeat eexists; try edone; intros; apply UPD0; eauto.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    destruct isrmw.
      symmetry in UPD; rewrite hplusAC in UPD.
      eapply hplus_ram_lD in UPD; eauto; desc; clarify.
      eapply initialize_eq_raD in UPD; desc.
      by repeat eexists; try edone; intros; apply UPD0; eauto.
    symmetry in UPD; rewrite hplusAC in UPD.
    eapply hplus_ra_lD in UPD; eauto; desc; clarify.
    eapply initialize_eq_raD in UPD; desc.
    by repeat eexists; try edone; intros; apply UPD0; eauto.

  Case Armw.
    eapply vshift_hack in UPD.
    assert (X: ∃ PP' QQ' isrmw' init',
              hi l = HVra PP' QQ' isrmw' init' ∧
              (∀ h0, assn_sem (sval (PP v)) h0 → assn_sem (sval (PP' v)) h0)).
    {
    destruct edge; ins.
      rewrite !(hplusAC (hsum _)) in UPD.
      symmetry in UPD; exploit hplus_def_inv_l; eauto.
      intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
        by rewrite <- GET; eapply In_mapI, In_mapI, swsOutOK.
      destruct isrmw'.
        rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
        by repeat eexists; try edone; intros; apply UPD0; eauto.
      rewrite Z in *; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
      by repeat eexists; try edone; intros; apply UPD0; eauto.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    rewrite hplusAC in UPD.
    destruct isrmw.
      symmetry in UPD; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
      by repeat eexists; try edone; intros; apply UPD0; eauto.
    symmetry in UPD; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
    by repeat eexists; try edone; intros; apply UPD0; eauto.
    }
    desc.
    eapply hplus_eq_raD with (v:=v) in iEQ; eauto; desf.
      eexists (hb_sb pre _), _; ins; repeat (split; try edone); ins; eauto.
      by repeat eexists; try edone; intros; apply iEQ1; auto.
    eapply hsum_eq_raD with (v:=v) in iEQ; eauto; desf.
    repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
    eexists (hb_sw _ _); ins; repeat (eexists; try edone); ins; eauto.
    generalize (iEQ1 h), (iEQ3 h), (X0 h); clear - H; tauto.
Qed.

Lemma heap_loc_rel_allocated :
  ∀ mt lab sb rf mo hmap V v
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l PP QQ isrmw init
    (LA: h l = HVra PP QQ isrmw init),
  ∃ cpre c hf PP' QQ' isrmw' init',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    hf l = HVra PP' QQ' isrmw' init' ∧
    (cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)) ∧
    (∀ h, assn_sem (proj1_sig (PP v)) h → assn_sem (proj1_sig (PP' v)) h).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  generalize (VALID _ IN).
  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
  {
     ins; destruct edge; ins; try (by red in EV; rewrite H in *; desf); [].
     repeat (eexists; try edone); vauto.
  }
  intros; exploit go_back_one_rel; eauto; ins; desf.

  assert (HB: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)).
    by destruct edge'; ins; subst; eauto with hb.
  exploit (IH edge'); eauto.
  intro; desf; repeat eexists; eauto with hb; ins; desf; eauto.
Qed.

Lemma go_back_one_rmwacq :
  ∀ lab sb rf hmap edge
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET: hmap edge = Hdef hf) l PP QQ init
    (LA : hf l = HVra PP QQ true init)
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge' hf',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = hb_fst edge ∧
    hmap edge' = Hdef hf' ∧
    ∃ PP' QQ' init', hf' l = HVra PP' QQ' true init'.
Proof.
  unfold hmap_valid, unique; ins; desf; desf.
  Case Askip.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    eapply vshift_hack in qEQ.
    symmetry in qEQ.
    assert (X := hplus_def_inv _ _ qEQ); desf; rewrite X in ×.
    eapply hsum_raD in X; eauto; desf; desf.
    2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
    rewrite X1 in *; ins.
    eapply hplus_ram_lD in qEQ; try edone; desc; clear qEQ2; desf.
    eapply hsum_eq_ra_rmwD in pEQ; eauto.
    desf; repeat (rewrite In_map in *; desf); rewrite pOK in ×.
    by repeat (eexists; try edone).

  Case Aalloc.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in *; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aalloc.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in *; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aload .
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    rewrite pEQ in *; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aload .
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    symmetry in qEQ; eapply hplus_eq_ra_rmwD in qEQ; eauto.
    desf; [by unfold hupd in qEQ0; desf; desf|].
    eapply hplus_eq_ra_rmwD in qEQ; eauto.
    desf.
      eapply hsum_eq_ra_rmwD in swsEQ; eauto; desc.
      repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
      by repeat (eexists; try edone); ins; eauto.
    ∃ (hb_sb pre e); destruct (hmap (hb_sb pre e)); try done.
    eexists; repeat split; ins.
    eapply hplus_ram_rD in pEQ'; eauto; desc; clarify.
    by repeat eexists; try edone.

  Case Astore .
    destruct edge; ins; subst; try (by rewrite wEQ in GET; try done; inv GET); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in LA; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Astore .
    ∃ (hb_sb pre (hb_fst edge)); destruct (hmap (hb_sb pre (hb_fst edge))); try done.
    eexists; repeat split; ins.
    eapply vshift_hack in UPD.
    destruct edge; ins.
      rewrite !(hplusAC (hsum _)) in UPD.
      symmetry in UPD; exploit hplus_def_inv_l; eauto.
      intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
        by rewrite <- GET; eapply In_mapI, In_mapI, swsOK.
      rewrite W1 in *; ins.
      rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
      eapply initialize_eq_raD in UPD; desc.
      by repeat eexists; try edone.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    symmetry in UPD; rewrite hplusAC in UPD.
    eapply hplus_ram_lD in UPD; eauto; desc; clarify.
    eapply initialize_eq_raD in UPD; desc.
    by repeat eexists; try edone; intros; apply UPD0; eauto.

  Case Armw.
    eapply vshift_hack in UPD.
    assert (X: ∃ PP' QQ' init', hi l = HVra PP' QQ' true init').
    {
    destruct edge; ins.
      rewrite !(hplusAC (hsum _)) in UPD.
      symmetry in UPD; exploit hplus_def_inv_l; eauto.
      intro Z; desf; exploit hsum_raD; eauto; [|intro W; desf].
        by rewrite <- GET; eapply In_mapI, In_mapI, swsOutOK.
      rewrite W1 in *; ins.
      rewrite Z in *; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
      by repeat eexists; try edone.
    rewrite hplusAC in UPD.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    symmetry in UPD; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
    by repeat eexists; try edone.
    }
    desc.
    eapply hplus_eq_ra_rmwD in iEQ; eauto; desf.
      by eexists (hb_sb pre _), _; ins; repeat (split; try edone); ins; eauto.
    eapply hsum_eq_ra_rmwD in iEQ; eauto; desf.
    repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
    by eexists (hb_sw _ _); ins; repeat (eexists; try edone); ins; eauto.
Qed.

Lemma heap_loc_rmwacq_allocated :
  ∀ mt lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l PP QQ init
    (LA: h l = HVra PP QQ true init),
  ∃ cpre c hf PP' QQ' init',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    hf l = HVra PP' QQ' true init'.
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  generalize (VALID _ IN).
  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
  {
     ins; destruct edge; ins; try (by red in EV; rewrite H in *; desf); [].
     repeat (eexists; try edone); vauto.
  }
  intros; exploit go_back_one_rmwacq; eauto; ins; desf.

  assert (HB: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)).
    by destruct edge'; ins; subst; eauto with hb.
  exploit (IH edge'); eauto.
Qed.

Lemma go_back_one_acq3 :
  ∀ lab sb rf hmap edge
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET: hmap edge = Hdef hf) l PP QQ init
    (LA : hf l = HVra PP QQ false init) v
    (NE : sval (QQ v) ≠ Aemp)
    (NE : sval (QQ v) ≠ Afalse)
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge' hf',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = hb_fst edge ∧
    hmap edge' = Hdef hf' ∧
    ∃ PP' QQ' init',
      hf' l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
  unfold hmap_valid, unique; ins; desf; desf.
  Case Askip.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    eapply vshift_hack in qEQ.
    symmetry in qEQ.
    assert (X := hplus_def_inv _ _ qEQ); desf; rewrite X in ×.
    eapply hsum_has_ra_own in X; eauto; desf; desf.
    2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
    eapply hplus_ra_own_l in qEQ; try edone; desc.
    eapply hsum_eq_ra_ownD with (v:=v) in pEQ; eauto.
    desf; repeat (rewrite In_map in *; desf); rewrite pOK in ×.
    by repeat (eexists; try edone); eauto.

  Case Aalloc.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in *; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aalloc.
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in *; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aload .
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    rewrite pEQ in *; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Aload .
    destruct edge; ins; subst; try (by red in EV; rewrite Heq in *; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    rewrite hplusAC in qEQ.
    symmetry in qEQ; eapply hplus_eq_ra_ownD in qEQ; eauto.
    desf.
      eapply hsum_eq_ra_ownD in swsEQ; eauto; desc.
      repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
      by repeat (eexists; try edone); ins; eauto.
    eexists (hb_sb pre e), _; repeat split; eauto.
    eapply hplus_eq_ra_ownD in qEQ; eauto; desf.
      by unfold hupd in qEQ3; desf; desf; ins.
    by eapply hplus_ra_own_r in pEQ'; eauto.

  Case Astore .
    destruct edge; ins; subst; try (by rewrite wEQ in GET; try done; inv GET); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    unfold hupd in LA; desf; desf.
    by ∃ (hb_sb pre e); repeat (eexists; try edone).

  Case Astore .
    ∃ (hb_sb pre (hb_fst edge)); destruct (hmap (hb_sb pre (hb_fst edge))); try done.
    eexists; repeat split; ins.
    eapply vshift_hack in UPD.
    destruct edge; ins.
      rewrite !(hplusAC (hsum _)) in UPD.
      symmetry in UPD; exploit hplus_def_inv_l; eauto.
      intro Z; desf; exploit hsum_has_ra_own; eauto; [|intro W; desf].
        by rewrite <- GET; eapply In_mapI, In_mapI, swsOK.
      rewrite Z in *; eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
      eapply initialize_eq_raD in UPD; desc.
      by repeat (eexists; try edone).
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    symmetry in UPD; rewrite hplusAC in UPD.
    eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
    eapply initialize_eq_raD in UPD; desc.
    by repeat (eexists; try edone).

  Case Armw.
    eapply vshift_hack in UPD.
    assert (X: ∃ PP' QQ' init',
                 hi l = HVra PP' QQ' false init' ∧
                 sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse).
    {
    destruct edge; ins.
      rewrite !(hplusAC (hsum _)) in UPD.
      symmetry in UPD; exploit hplus_def_inv_l; eauto.
      intro Z; desf; exploit hsum_has_ra_own; eauto; [|intro W; desf].
        by rewrite <- GET; eapply In_mapI, In_mapI, swsOutOK.
      by rewrite Z in *; eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
    rewrite hplusAC in UPD.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    by symmetry in UPD; eapply hplus_ra_own_l in UPD; eauto; desc; clarify.
    }
    desc.
    eapply hplus_eq_ra_ownD with (v := v) in iEQ; eauto; desf.
      by eexists (hb_sb pre _); ins; repeat (eexists; try edone).
    eapply hsum_eq_ra_ownD in iEQ; eauto; desf.
    repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
    by eexists (hb_sw _ _); ins; repeat (eexists; try edone).
Qed.

Lemma heap_loc_ra_own_allocated :
  ∀ mt lab sb rf mo hmap V v
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l PP QQ init
    (LA: h l = HVra PP QQ false init)
    (ALL: sval (QQ v) ≠ Aemp)
    (NF: sval (QQ v) ≠ Afalse),
  ∃ cpre c hf PP' QQ' init',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    (cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)) ∧
    hf l = HVra PP' QQ' false init'.
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  generalize (VALID _ IN).
  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
  {
     ins; destruct edge; ins; try (by red in EV; rewrite H in *; desf); [].
     repeat (eexists; try edone); vauto.
  }
  intros; exploit go_back_one_acq3; eauto; ins; desc.

  assert (HB: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)).
    by destruct edge'; ins; subst; eauto with hb.

  exploit (IH edge'); ins; desf; repeat (eexists; try edone); eauto with hb.
Qed.

Lemma heap_loc_ra_no_own :
  ∀ mt lab sb rf mo hmap V v
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    edge' (EV: edge_valid lab sb rf edge') (IN': In (hb_fst edge') V)
    h (GET: hmap edge = Hdef h) l PP QQ init (LA: h l = HVra PP QQ true init)
    h' (GET: hmap edge' = Hdef h') PP' QQ' init' (LA': h' l = HVra PP' QQ' false init'),
    sval (QQ' v) = Aemp ∨ sval (QQ' v) = Afalse.
Proof.
  intros; apply NNPP; intro.
  eapply heap_loc_ra_own_allocated with (edge:=edge') in LA'; eauto.
  eapply heap_loc_rmwacq_allocated with (edge:=edge) in LA; eauto.
  desc; pose proof (CONS_A _ _ LA0 _ LA'0); subst; desc.
  assert (INN: In cpre0 V) by (desf; eauto with hb); clear LA'2.
  eapply VALID in INN; red in INN; desf; desc.
  eapply qU in LA; eapply qU in LA'; congruence.
Qed.

Lemma hb_helper1 lab sb rf mo e e' a :
  unique (sb e) e' →
  (∀ x, ¬ synchronizes_with lab sb rf mo e x) →
  happens_before lab sb rf mo e a →
  happens_before lab sb rf mo e' a ∨ e' = a.
Proof.
  unfold happens_before; intros.
  apply clos_trans_t1n in H1.
  inv H1; red in H2; desf; try apply H in H2; try apply H0 in H2;
  vauto; eauto using clos_t1n_trans.
Qed.

Lemma helper_acyclic_last :
  ∀ A (r: A → A → Prop)
    (ACYCL: acyclic r) e i
    (MHB: clos_refl_trans _ r e i) R,
  ∃ b,
    << PRM: In b (i :: R) >> ∧
    << BEFORE: clos_refl_trans _ r e b >> ∧
    << NAFTER: ∀ c, In c (i :: R) → ¬ clos_trans _ r b c >>.
Proof.
  unfold not; induction R; ins; unfold NW.
    by repeat eexists; eauto; ins; desf; subst; eauto using t_step, clos_refl_trans.
  desc; destruct (classic (clos_trans _ r b a)).
    ∃ a; repeat split; eauto.
      by clear -BEFORE H; rewrite clos_refl_transE in *; desf; eauto using clos_trans.
    by intros ? [IN|[IN|IN]] HB; subst; eauto using clos_trans.
  ∃ b; repeat split; try tauto.
  by intros ? [IN|[IN|IN]] HB; subst; eauto using clos_trans.
Qed.

Lemma helper_hb_last :
  ∀ A lab sb rf mo
    (ACYCL: IrreflexiveHB lab sb rf mo) b (Q: A) R (IN: In (b, Q) R) e
    (MHB: e = b ∨ happens_before lab sb rf mo e b),
   ∃ b Q,
     << PRM: In (b, Q) R >> ∧
     << BEFORE: e = b ∨ happens_before lab sb rf mo e b >> ∧
     << NAFTER: ∀ b' Q',
                  In (b', Q') R →
                  ¬ happens_before lab sb rf mo b b' >>.
Proof.
  intros; desc.
  eapply In_implies_perm in IN; desc.
  assert (MHB': clos_refl_trans actid (imm_happens_before lab sb rf mo) e b).
    by clear -MHB; desf; [|induction MHB]; eauto using clos_refl_trans.
  pose proof (helper_acyclic_last ACYCL MHB' (map (@fst _ _) l')).
  ins; desc.
  assert (∃ Q, In (b0, Q) R).
    destruct PRM; subst.
    ∃ Q; apply (Permutation_in _ (Permutation_sym IN)), In_eq.
    apply In_map in H; destruct H as [[? Q'] [? ?]].
    ∃ Q'; apply (Permutation_in _ (Permutation_sym IN)); vauto.
  desc; ∃ b0, Q0; repeat split; try edone.
    by eapply clos_refl_transE in BEFORE; destruct BEFORE; vauto.
  red; ins; eapply NAFTER.
  apply (Permutation_in _ IN) in H0; ins; rewrite In_map in ×.
  clear - H0; desf; vauto.
Qed.

Definition RTrel A lab sb rf mo V RT RT' :=
  length (A:=A) (fst RT) < length (A:=A) (fst RT') ∨
  length (fst RT) = length (fst RT') ∧
  depth_metric (happens_before lab sb rf mo) V (map hb_fst (snd RT)) <
  depth_metric (happens_before lab sb rf mo) V (map hb_fst (snd RT')).

Definition RTrelWF A lab sb rf mo V :
  well_founded (RTrel (A:=A) lab sb rf mo V).
Proof.
  red; intros [a b].
  remember (existT (fun _ ⇒ list hbcase) (length a) b) as c; revert a b Heqc.
  induction c using
    (well_founded_ind
       (wf_lexprod _ _ _ _
          (wf_ltof (fun x ⇒ x))
          (fun _ ⇒ wf_ltof (fun x ⇒
             depth_metric (happens_before lab sb rf mo) V (map hb_fst x))))).
  intros; desf; constructor; intros [m n] R; eapply H; ins.
  red in R; desf; ins; try rewrite R in *; vauto.
Qed.

Definition read_loses_perm hmap lab sb rf a l v (Q: assn_mod) :=
  ∃ typ apre apost w,
    << LL: lab a = Aload typ l v >> ∧
    << Lp: unique (sb^~ a) apre >> ∧
    << Lq: unique (sb a) apost >> ∧
    << Lw: ann_sw lab rf w a >> ∧
    ∃ hp hq hw PP QQ PP' QQ',
    << Ep: hmap (hb_sb apre a) = Hdef hp >> ∧
    << Eq: hmap (hb_sb a apost) = Hdef hq >> ∧
    << Ew: hmap (hb_sw w a) = Hdef hw >> ∧
    << Gp: hp l = HVra PP QQ false true >> ∧
    << Gq: hq l = HVra PP' QQ' false true >> ∧
    << PREC: precise (sval Q) >> ∧
    << LSEM: assn_sem (sval Q) (Hdef hw) >> ∧
    ( << Gw : hw l = HVnone >> ∧
       << ASIM: Asim (sval (QQ v)) (Astar (sval (QQ' v)) (sval Q)) >>
    ∨ ∃ Pw' Qw' initw',
       << Gw : hw l = HVra Pw' Qw' false initw' >> ∧
       << ASIM: Asim (Astar (sval (QQ v)) (sval (Qw' v))) (Astar (sval (QQ' v)) (sval Q)) >>).

Definition ssnd (x : actid × assn_mod) := sval (snd x).

Lemma wellformed_only_reads_helper :
  ∀ (goal : assn_mod → Prop) mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    T (NDt: NoDup T)
      (ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
      (TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
    (R: list (actid × assn_mod))
      (NDr: NoDup (map (@fst _ _) R))
      (SR: ∀ a Q (IN: In (a, Q) R), In a V) l v
      (DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
    (NHB: ∀ a (INt: In a T) b Q (INr: In (b,Q) R),
            hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b)
    (INDEP: independent lab sb rf mo T)
    hT (MAPt: hsum (map hmap T) = Hdef hT)
    PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT)
    (PROVE:
       ∀ h h' PP' QQ' isrmw' init'
              (ALLOC: ∀ a apost (SB: sb a apost) (A: lab a = Aalloc l) h''
                             (D: hmap (hb_sb a apost) = Hdef h''), h'' l = h' l)
              (VS: vshift (Hdef h) (Hdef h'))
              (G : h l = HVuval ∨ ∃ isrmw QQ, h l = HVra QQ QQ isrmw false)
              (G': h' l = HVra PP' QQ' isrmw' init'),
       ∃ FRAME, goal (mk_assn_mod (Astar (sval (QQ' v)) FRAME))),
  ∃ FRAME, goal (mk_assn_mod (Astar (sval (QT v)) (foldr Astar (map ssnd R) FRAME))).
Proof.
  intros until R; revert NDt ST TT.
  remember (R, T) as RT; revert R T HeqRT.
  induction RT using (well_founded_ind (RTrelWF lab sb rf mo V)).
  specialize (fun R' T' X ⇒ H (R',T') X _ _ eq_refl).
  ins; desf.

  exploit (get_deepest ACYCLIC HC (T:=T)); try done.
    by intro; subst; clear - HT MAPt; inv MAPt.
  intro; desc.

  destruct (classic (∃ b Q, In (b, Q) R ∧
               (hb_fst edge = b ∨ happens_before lab sb rf mo (hb_fst edge) b))).
  {
  
    desc.
    pose proof (helper_hb_last ACYCLIC _ _ H0 H1).
    clear b Q H0 H1; desc.

    assert (LP := DEL _ _ PRM); red in LP; desc.
    eapply In_implies_perm in PRM; desc.
    destruct BEFORE as [BEFORE|BEFORE]; subst.

  {
    pose proof (get_pres ACYCLIC HC _ NDt IN ST TT DEEP INDEP); ins; desc.
    clear METR.
    ins.

    assert (METR': RTrel lab sb rf mo V (l', map (hb_sb^~ (hb_fst edge)) pres_sb ++
           map (hb_sw^~ (hb_fst edge)) pres_sw ++
           filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)
                       (R, T)).
      by left; simpl; rewrite (Permutation_length PRM); ins.
    specialize (H _ _ METR' ND' INCL' EVS').

    assert (ALLOC: ∀ hf loc,
            hsum (map hmap (filter (fun x ⇒ hb_fst x != hb_fst edge) T)) = Hdef hf →
            hf loc ≠ HVnone →
            ∃ c, lab c = Aalloc loc ∧ c ≠ hb_fst edge).
      intros ? ? U NEQ; eapply hsum_alloc in U; eauto; desc.
      rewrite In_map in *; desc; rewrite In_filter in *; desc.
      exploit heap_loc_allocated; eauto; try (by destruct x; ins; eauto).
      destruct (eqP (hb_fst x) (hb_fst edge)); ins; desc; eexists; split; eauto; intro; desc.
      subst; desf; congruence.

    assert (∃ hT',
             hsum
               (map hmap
                    (map (hb_sb^~ (hb_fst edge)) pres_sb ++
                     map (hb_sw^~ (hb_fst edge)) pres_sw ++
                     filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)) =
             Hdef hT' ∧
             ∃ PT' QT' isrmwT' initT',
               hT' l = HVra PT' QT' isrmwT' initT' ∧
               Asim (sval (QT' v)) (Astar (sval (QT v)) (sval Q))).
    {
      clear H; exploit independent_heap_compat; eauto;
      try solve [by intros ? ? X; eapply INCL' in X|
                 by intros ? ? X; eapply EVS' in X].
      intros [hhh M]; simpls; eexists; split; try edone.
      rewrite !map_app, !hsum_app in ×.
      clear METR' IND' EVS' ND' INCL'.

      assert (IN' := IN).
      eapply TT in IN'; destruct edge; ins;
        [by red in IN'; rewrite LL in IN'; desc|].
      eapply Lq in IN'; subst.

      assert (J: Permutation T (hb_sb e e' :: filter (fun x : hbcase ⇒ hb_fst x != e) T)).
        eapply NoDup_Permutation; eauto.
        constructor; eauto using NoDup_filter.
          by rewrite In_filter; simpl; rewrite eqxx; intro; desc.
        clear LP0; split; ins; rewrite In_filter in *; desf; eauto.
        case (eqP (hb_fst x) e); eauto.
        left; eapply TT in H; destruct x; ins; subst;
          [by red in H; rewrite LL in H; desc|].
        by eapply Lq in H; subst.
      clear IN.

      assert (pres_sb = apre :: nil).
        destruct Lp as [Lp Lp'].
        destruct pres_sb as [|aa pres_sb]; ins; [by eapply Pb in Lp|].
        (assert (apre = aa) by eapply Lp', Pb, In_eq); subst aa; f_equal.
        destruct pres_sb; ins; inv NDb; destruct H1; left; symmetry.
        by eapply Lp', Pb; vauto.
      subst; ins; rewrite hsum_one, Ep in ×.

      revert MAPt; rewrite (hsum_perm (map_perm _ J)); simpl.
      rewrite hsum_cons, Eq; intro.

      assert (P: pres_sw = w :: nil).
        by apply NoDup_eq_one; clear - NDw Pw Lw; ins;
           rewrite Pw in *; unfold ann_sw in *; desf.

      rewrite <- Ep in M.
      subst; simpls; rewrite hsum_one in ×.
      exploit (go_back_one_acq2 (rf:=rf) FIN CONS_A hmap); try eapply LwND; eauto;
          simpls; rewrite ?hsum_one; try edone.
        by intro G; eapply sim_assn_sem in LSEM; [|apply Asim_sym, G].
      intro K; desc.
      rewrite Eq, MAPt in K; clarify.
      eapply hplus_ra_lD in MAPt; eauto; desc; rewrite MAPt in *; desc; clarify.
      assert (initT = true) by desf; subst; clear MAPt2.
      specialize (K0 _ _ _ eq_refl); desc; rewrite K0.
      do 4 eexists; try edone.
    }

    clear ND' INCL' EVS' METR' hT MAPt HT; desc.
    cut (∃ FRAME,
     goal
       (mk_assn_mod
          (Astar (sval (QT' v)) (foldr Astar (List.map ssnd l') FRAME)))).
      clear -H2 PRM; intro M; desc.
      ∃ FRAME; erewrite AsimD; [eapply M|].
      eapply Asim_trans.
        by eapply (Asim_star (Asim_refl _)), (foldr_star_perm2 (Permutation_map _ PRM)).
      eapply Asim_trans.
        by simpl; eapply Asim_sym, Asim_starA.
      by eapply Asim_star, Asim_refl; eapply Asim_sym, H2.

    eapply H; eauto.

      by eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr; inv NDr.
      eby ins; eapply SR, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
      eby ins; eapply DEL, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].

    { clear LP0; intros; rewrite !In_app, !In_map, In_filter in *; desf; ins; eauto.
      3: eapply NHB; eauto;
         eby ins; eapply Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
      × split.
        by intro; subst;
           eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
           inv NDr; destruct H5; rewrite In_map; vauto.
        eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
      × split.
        by intro; subst;
           eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
           inv NDr; destruct H5; rewrite In_map; vauto.
        eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
    }
  }

  assert (METR': RTrel lab sb rf mo V (l', hb_sb apre b :: hb_sw w b :: T) (R, T)).
    by left; simpl; rewrite (Permutation_length PRM); ins.
  specialize (H _ _ METR').

  assert (ND': NoDup (hb_sb apre b :: hb_sw w b :: T)).
    clear LP0; constructor; try constructor; ins;
      intro X; desf; eapply NHB in X.
    2: by ins; eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
    by ins; desf.
    2: by ins; eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
    by ins; desf.

  assert (INDEP': independent lab sb rf mo (hb_sb apre b :: hb_sw w b :: T)).
  { clear LP0 H; destruct Lp, Lq.
    red; ins; destruct IN1 as [|[|]], IN2 as [|[|]];
    desc; subst; ins; try rewrite LwOK in *; eauto;
      try solve[by desf; eauto with hb].

    eapply NHB in H3.
    2: by eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
    by desf; eauto with hb.
    eapply NHB in H3.
    2: by eapply Permutation_in, In_eq; eapply (Permutation_sym PRM).
    by desf; eauto with hb.
  }
  clear INDEP.

  assert (INCL' : ∀ edge0,
                    In edge0 (hb_sb apre b :: hb_sw w b :: T) →
                    In (hb_fst edge0) V).
    assert (In b V).
      by ins; eapply SR, Permutation_in, In_eq; eapply (Permutation_sym PRM).
    by destruct Lp; clear LP0; ins; desf; ins; try rewrite LwOK in *;
       eauto using hist_closedD with hb.

  assert (EV' : ∀ edge0,
                    In edge0 (hb_sb apre b :: hb_sw w b :: T) →
                  edge_valid lab sb rf edge0).
    by destruct Lp; ins; clear BEFORE LP0; desf; ins; eauto.

  assert (∃ hT',
            hsum (hmap (hb_sb apre b) :: hmap (hb_sw w b) :: map hmap T) = Hdef hT' ∧
            ∃ PT' QT' isrmwT' initT',
              hT' l = HVra PT' QT' isrmwT' initT' ∧
              ∃ R,
              Asim (sval (QT' v)) (Astar (sval (QT v)) (Astar (sval Q) R))).
  { clear H; exploit independent_heap_compat; eauto;
    try solve [by intros ? ? X; eapply INCL' in X|
               by intros ? ? X; eapply EV' in X].
    intros [hhh L]; simpls; eexists; split; try edone.
    rewrite !hsum_cons, MAPt, Ep, Ew in L; desc.
    revert HT LP0 Gp L; clear; do 2 (rewrite hplus_unfold; desf).
    specialize (h l); specialize (h0 l).
    intros; desc; clarify; rewrite Gp, HT in *; simpls.
    destruct (hw l); ins; desf; do 5 eexists; try edone;
    ins; ∃ (sval (QQ' v)); Asim_simpl; desf; try solve [exfalso; eauto];
    (eapply Asim_sym, Asim_trans, Asim_sym in ASIM; [|apply Asim_starC]);
    (eapply Asim_trans; [|repeat first [exact ASIM|apply Asim_star|idtac]; try apply Asim_refl]); eauto using Asim.

   by destruct (h0 v); ins; desc; rewrite H, ?H0; eauto using Asim.

   by destruct (h v), (h0 v); ins; desc; rewrite H, H0, ?H1, ?H2; eauto using Asim.
  }

  clear hT HT MAPt; desc.
  cut (∃ FRAME,
   goal
     (mk_assn_mod
        (Astar (sval (QT' v)) (foldr Astar (List.map ssnd l') FRAME)))).
    clear -H2 PRM; intro M; desc.
    ∃ (Astar R0 FRAME); erewrite AsimD; [eapply M|].
    eapply Asim_trans.
      by eapply (Asim_star (Asim_refl _)), (foldr_star_perm2 (Permutation_map _ PRM)).
    eapply Asim_trans.
      by simpl; eapply Asim_sym, Asim_starA.
    eapply Asim_trans, Asim_star, Asim_refl; [|apply Asim_sym, H2].
    apply (Asim_trans (Asim_starA _ _ _)).
    eapply Asim_trans, Asim_sym, Asim_starA.
    apply Asim_star; [apply Asim_refl|].
    eapply Asim_trans, Asim_sym, Asim_starA.
    apply Asim_star, Asim_foldr_pull; apply Asim_refl.

  eapply H; eauto.
  × by eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr; inv NDr.
  × eby ins; eapply SR, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
  × eby ins; eapply DEL, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].

  × ins; eauto using Permutation_in, Permutation_map.

    destruct INt as [|[INt|INt]]; desc; subst; ins.
    3: eby eapply NHB, Permutation_in, In_cons; [|eapply (Permutation_sym PRM)|].
    split.
      by intro; subst;
         eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
         inv NDr; destruct H5; rewrite In_map; vauto.
    eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].

    split.
      by intro; subst;
         eapply (Permutation_NoDup (Permutation_map _ PRM)) in NDr;
         inv NDr; destruct H5; rewrite In_map; vauto.
    eby eapply NAFTER, Permutation_in, In_cons; [eapply (Permutation_sym PRM)|].
}

 
  pose proof (get_pres ACYCLIC HC _ NDt IN ST TT DEEP INDEP); desf.
  simpls; desf.

  assert (NHB': ∀ a,
       In a
         (map (hb_sb^~ (hb_fst edge)) pres_sb ++
          map (hb_sw^~ (hb_fst edge)) pres_sw ++
          filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T) →
       ∀ b Q,
       In (b, Q) R →
       hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b).
  { clear - H0 NHB; intros.
    rewrite !In_app, !In_map, In_filter in *; desf; ins; eauto;
    split; intro; desf; destruct H0; eauto. }

  specialize (H R (map (hb_sb^~ (hb_fst edge)) pres_sb ++
                   map (hb_sw^~ (hb_fst edge)) pres_sw ++
                   filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)
                (or_intror (conj eq_refl METR)) ND' INCL' EVS'
                NDr SR _ _ DEL NHB' IND').
  clear NHB'.

  exploit independent_heap_compat; try apply IND'; eauto;
    try solve [by intros ? ? X; eapply INCL' in X|by intros ? ? X; eapply EVS' in X].
  intro M; desf; rewrite M in ×.
  specialize (H _ eq_refl).
  clear IND' EVS' INCL' METR ND'.

  assert (J := helper_perm_filter_post (hb_fst edge) T); desf.
  revert MAPt.
  rewrite (hsum_perm (map_perm _ J)).
  rewrite !map_app, !hsum_app in ×.
  rewrite hplusC, hplusA; ins.
  assert (ALLOC: ∀ hf loc,
            hsum (map hmap (filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T)) = Hdef hf →
            hf loc ≠ HVnone →
            ∃ c, lab c = Aalloc loc ∧ c ≠ hb_fst edge).
     intros ? ? U NEQ; eapply hsum_alloc in U; eauto; desf.
     rewrite In_map in *; desf.
     rewrite In_filter in *; desf.
     exploit heap_loc_allocated; eauto; try (by destruct x; ins; eauto).
     destruct (eqP (hb_fst x) (hb_fst edge)); ins; desf; eexists; split; eauto; intro; desf.
     by apply clos_refl_trans_hbE in x0; desf; try congruence; eapply DEEP; eauto with hb.
  clear INDEP.

  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [EQ|NEQ].
  {
    clear H.
    destruct posts_sw; ins.
    2: by exploit TT;
          [by eapply Permutation_in, In_appI2, In_appI2, In_eq;
              apply Permutation_sym, J|];
          simpl; unfold ann_sw; rewrite EQ; ins; desf.
    generalize (VALID _ (ST _ IN)); unfold hmap_valid; rewrite EQ.
    generalize IN as IN'.
    intros; desc; eapply TT in IN'; destruct edge; simpls;
     [by red in IN'; rewrite EQ in *; desf|].
    eapply qU in IN'; subst.
    assert (posts_sb = e' :: nil).
    { eapply (Permutation_in _ J) in IN.
      rewrite !In_app, In_map, In_filter, eqxx in *; ins.
      clear qEQ; desf.
      eapply (Permutation_NoDup J), nodup_append_right, nodup_append_left in NDt.
      destruct (In_implies_perm _ _ IN0) as [l' Pl'].
      cut (l' = nil).
        symmetry in Pl'; eapply In_split in IN0; desf.
        eapply Permutation_cons_app_inv in Pl'.
        intros; subst; eapply Permutation_nil in Pl'.
        by destruct l1; ins; destruct l2; ins.
      apply (Permutation_NoDup (Permutation_map _ Pl')) in NDt.
      ins; inv NDt.
      destruct l' as [|e'' ?]; ins.
      clear H3.
      assert (e' ≠ e'') by (intro; subst; eauto).
      destruct H.
      exploit TT.
      eapply (Permutation_in _ (Permutation_sym J)), In_appI2, In_appI1, In_mapI.
      eapply (Permutation_in _ (Permutation_sym Pl')), In_cons, In_eq.
      eapply qU.
    }
    subst; ins; rewrite hsum_nil, hsum_one, hplus_emp_l in ×.
    assert (R = nil).
    {
      specialize (NHB _ IN).
      destruct R as [|[]]; ins; []; exfalso.
      specialize (SR _ _ (In_eq _ _)).
      specialize (DEL _ _ (In_eq _ _)); red in DEL; desc; clear DEL0.
      specialize (NHB _ _ (In_eq _ _)); desc.
      assert (∃ hf', hmap (hb_sb e e') = Hdef hf' ∧ hf' l ≠ HVnone).
        by clear -qEQ; desf; repeat eexists; try edone; rewrite hupds.
      desc; clear qEQ IN.
      exploit (heap_loc_allocated ACYCLIC HC VALID (hb_sb a apost));
          try eapply Lq; simpl; eauto.
         instantiate (1:=l); congruence.
      intro M'; desc.
      assert (c = e) by (eapply CONS_A; rewrite ?EQ, ?M'; ins); subst.
      eapply clos_refl_trans_hbE in M'0; desf; try congruence.
      desf; eauto using t_step with hb; try congruence.
      eapply (@hb_helper1 lab sb rf) with (a := a) in qU;
        try edone; desf; eauto with hb.
      by unfold synchronizes_with; rewrite M'; red; ins; desf.
    }
    subst; ins.

    clear - PROVE CONS_A qU qEQ MAPt ALLOC EQ HT.
    eapply hplus_def_inv in MAPt; desc; subst; rewrite MAPt in ×.
    assert (N: hT l = hy l).
      desf; rewrite PLUSv, hupds; simpls; desf;
      exfalso; assert (XXX: hz l ≠ HVnone) by congruence;
      destruct (ALLOC _ _ MAPt0 XXX) as (c & Ac & []);
      by eapply CONS_A; rewrite ?EQ, ?Ac.
    eapply PROVE; eauto using vshift_refl.
      intros; assert (a = e) by (eapply CONS_A; rewrite ?EQ, ?A; done); subst.
      eapply qU in SB; congruence.
    by desf; rewrite hupds in *; desf; eauto.
  }

  exploit go_back_one_acq; try eapply NEQ; eauto.
  intro K; desf.
  exploit (NoDup_Permutation K NDb); [by intro; rewrite Pb|].
  exploit (NoDup_Permutation K0 NDw); [by intro; rewrite Pw|].
  clear Pb Pw; intros Pb Pw.
  rewrite (hsum_perm (map_perm _ (map_perm _ Pb))) in K7.
  rewrite (hsum_perm (map_perm _ (map_perm _ Pw))) in K7.
  specialize (K7 _ M); desf.

  destruct (@perm_from_subset _ posts_sb0 posts_sb) as [rb Psb].
    by eapply (Permutation_NoDup J) in NDt; rewrite !nodup_app in NDt;
       desf; eauto using NoDup_mapD.
    by symmetry in J; intros; apply K5, (TT (hb_sb _ _)), (Permutation_in _ J),
                                    In_appI2, In_appI1, In_mapI.

  destruct (@perm_from_subset _ posts_sw0 posts_sw) as [rw Psw].
    by eapply (Permutation_NoDup J) in NDt; rewrite !nodup_app in NDt;
       desf; eauto using NoDup_mapD.
    by symmetry in J; intros; apply K6, (TT (hb_sw _ _)), (Permutation_in _ J),
                                    In_appI2, In_appI2, In_mapI.

  rewrite (hsum_perm (map_perm _ (map_perm _ Psb))) in K7.
  rewrite (hsum_perm (map_perm _ (map_perm _ Psw))) in K7.
  rewrite !map_app, !hsum_app, !hplusA in K7.
  rewrite !(hplusAC (hsum (map hmap (map (hb_sb _) rb)))) in K7.
  rewrite !(hplusAC (hsum (map hmap (map (hb_sw _) rw)))) in K7.
  unfold actid in *; rewrite MAPt, <- hplusA, hplusC in K7.

  eapply hplus_def_inv in K7; desf.
  eapply hvplus_ra2 in HT; eauto.
  rewrite <- PLUSv in HT; red in HT; desf.
  specialize (K8 _ _ _ _ eq_refl); red in K8; desf.
  specialize (H _ _ _ _ eq_refl PROVE); desf.
  specialize (HT v); desf.
  specialize (K8 v); desf.

  ∃ (Astar (Astar QR QR0) FRAME).
  clear -H HT K8; erewrite AsimD; [edone|].
  eapply Asim_trans.
    by apply Asim_star, Asim_foldr_pull; apply Asim_refl.
  eapply Asim_trans, (Asim_star (Asim_sym K8)), Asim_refl.
  eapply Asim_trans, (Asim_star (Asim_star (Asim_sym HT) (Asim_refl _))), Asim_refl.
  eapply Asim_trans, Asim_sym, Asim_starA.
  eapply Asim_trans, Asim_sym, Asim_starA.
  apply Asim_star, Asim_starA; apply Asim_refl.
Qed.

Lemma wellformed :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    wpre w (INw: In w V)
    l v (LAB: is_writeLV (lab w) l v)
    (SBw: sb wpre w) hw
    sww (swwOK: ∀ x, In x sww ↔ ann_sw lab rf x w) (swwND: NoDup sww)
    (MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_sw^~ w) sww)) = Hdef hw)
    PW QW isrmwW initW
    (HW: hw l = HVra PW QW isrmwW initW)
    (R: list (actid × assn_mod))
      (NDr: NoDup (map (@fst _ _) R))
      (SR: ∀ a Q (IN: In (a, Q) R), In a V)
      (TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
      (DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
    T (NDt: NoDup T)
      (ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
      (TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
    (INDEP: independent lab sb rf mo T)
    (NHB: ∀ a (INt: In a T) b Q (INr: In (b,Q) R),
            hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b)
    hT (MAPt: hsum (map hmap T) = Hdef hT)
    PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
  implies (proj1_sig (PW v))
          (Astar (proj1_sig (QT v))
                 (foldr Astar (map ssnd R) Atrue)).
Proof.
  intros.
  assert (N: ∃ cpre c hf PP' QQ' isrmw' init',
            sb cpre c ∧
            lab cpre = Aalloc l ∧
            hmap (hb_sb cpre c) = Hdef hf ∧
            hf l = HVra PP' QQ' isrmw' init' ∧
            happens_before lab sb rf mo cpre w ∧
            (∀ h, assn_sem (sval (PW v)) h → assn_sem (sval (PP' v)) h)).
    eapply hplus_eq_raD with (v:=v) in MAPw; eauto; desf.
      exploit (heap_loc_rel_allocated v ACYCLIC CONS_A HC VALID
                                    (hb_sb wpre w) SBw); ins; eauto with hb.
      by desc; repeat (eexists; try edone); ins; desf; eauto with hb; apply x5, MAPw1.
    eapply hsum_eq_raD with (v:=v) in MAPw; eauto; desc; clarify.
    repeat (rewrite In_map in *; desc); clarify; rewrite swwOK in ×.
    exploit (heap_loc_rel_allocated v ACYCLIC CONS_A HC VALID
                                    (hb_sw _ w) MAPw5); ins; eauto with hb.
    by desc; repeat (eexists; try edone); ins; desf; eauto with hb; apply x6, MAPw3, MAPw1.
  desc; intros.
  assert (In cpre V) by (eauto with hb).
  clear SBw INw MAPw HW.
  edestruct (wellformed_only_reads_helper (fun A ⇒ implies (sval (PW v)) (sval A)));
    eauto.
    intros; eapply vshift_hack in VS; desf; rewrite G in *; desf.
    erewrite ALLOC in N2; eauto; []; desf.
    ∃ Aemp; red; ins.
    eapply sim_assn_sem, N4; eauto; Asim_simpl; vauto.
  simpls.
  red; intros.
  eapply sim_assn_sem; [apply Asim_star, Asim_foldr_simpl; apply Asim_refl|].
  apply H0 in H1.
  eapply sim_assn_sem in H1; [|apply Asim_assn_norm].
  eapply sim_assn_sem in H1;
    [|apply Asim_star, Asim_sym, Asim_foldr_simpl; apply Asim_refl].
  clear -H1; simpls; desf; repeat eexists; try edone.
  by intro; desf; destruct h0; ins.
Qed.

Lemma wellformed_one :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    wpre w (INw: In w V)
    l v (LAB: is_writeLV (lab w) l v)
    (SBw: sb wpre w) hw
    sww (swwOK: ∀ x, In x sww ↔ ann_sw lab rf x w) (swwND: NoDup sww)
    (MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_sw^~ w) sww)) = Hdef hw)
    PW QW isrmwW initW
    (HW: hw l = HVra PW QW isrmwW initW)
    rpre r (ST: In rpre V) (TT: sb rpre r)
    (NIN: ¬ In r V)
    (R: list (actid × assn_mod))
      (NDr: NoDup (map (@fst _ _) R))
      (SR: ∀ a Q (IN: In (a, Q) R), In a V)
      (TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
      (DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
    hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
    PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
  implies (proj1_sig (PW v))
          (Astar (proj1_sig (QT v))
                 (foldr Astar (map ssnd R) Atrue)).
Proof.
  intros; eapply wellformed with (w := w) (T := hb_sb rpre r :: nil);
  eauto; ins; desf.
  × by red; ins; desf; ins; desf; eauto using t_step with hb.
  × by split; intro; desf; eauto using hist_closedD.
  × by rewrite hsum_one.
Qed.

Lemma wellformed_one_w :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    wpre w (INw: In w V)
    typ l v (LAB: lab w = Astore typ l v)
    (SBw: sb wpre w) hw
    (MAPw: hmap (hb_sb wpre w) = Hdef hw)
    PW QW isrmwW initW
    (HW: hw l = HVra PW QW isrmwW initW)
    rpre r (ST: In rpre V) (TT: sb rpre r)
    (NIN: ¬ In r V)
    (R: list (actid × assn_mod))
      (NDr: NoDup (map (@fst _ _) R))
      (SR: ∀ a Q (IN: In (a, Q) R), In a V)
      (TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
      (DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
    hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
    PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
  implies (proj1_sig (PW v))
          (Astar (proj1_sig (QT v))
                 (foldr Astar (map ssnd R) Atrue)).
Proof.
  intros; eapply wellformed_one with (w := w) (sww := nil); eauto;
    instantiate; ins; unfold ann_sw; try rewrite LAB; ins; try split; ins; desf.
  by rewrite hsum_nil, hplus_emp_r.
Qed.