Lemmas about acquire-release accesses


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 xproj1 (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 xx))
          (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' XH (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 : hbcasehb_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 xhb_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 : hbcasehb_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 : hbcasehb_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 : hbcasehb_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 : hbcasehb_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 : hbcasehb_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 Aimplies (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.

Lemmas about initialization

Lemma helper_ra_init :
   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
    (LA : hf l = HVra PP QQ isrmw true)
    (NW : ¬ is_writeL (lab (hb_fst edge)) l),
   edge' hf',
    edge_valid lab sb rf edge'
    hb_snd edge' = hb_fst edge
    hmap edge' = Hdef hf'
     PP' QQ' isrmw',
      hf' l = HVra PP' QQ' isrmw' true.
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.
    2: by rewrite <- GET; eapply In_mapI, In_mapI, qOK.
    rewrite X0 in *; clear X0; try done.
    destruct isrmw'.
    eapply hplus_ram_lD in qEQ; try edone; desc; clarify.
      assert (init'0 = true) by desf; clear qEQ2; subst.
      eapply hsum_eq_ra_initD in pEQ; eauto.
      desf; repeat (rewrite In_map in *; desf).
      by apply pOK in pEQ2; repeat (eexists; try edone); ins.
    eapply hplus_ra_lD in qEQ; try edone; desc; clarify.
    assert (init'0 = true) by desf; clear qEQ2; subst.
    eapply hsum_eq_ra_initD in pEQ; eauto.
    desf; repeat (rewrite In_map in *; desf).
    by apply pOK in pEQ2; repeat (eexists; try edone); ins.

  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_initD in qEQ; eauto.
    desf.
      unfold hupd in qEQ0; desf; desf.
      apply hplus_def_inv in pEQ'; desf.
      specialize (PLUSv l0); rewrite hupds in *; simpls.
      by desf; (hb_sb pre e); repeat (eexists; try edone).
    eapply hplus_eq_ra_initD in qEQ; eauto.
    desf.
      eapply hsum_eq_ra_initD in swsEQ; eauto; desf.
      repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
      repeat (eexists; try edone); ins; eauto.
     (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 desf; repeat eexists; try edone.
    eapply hplus_ra_rD in pEQ'; eauto; desc; clarify.
    by desf; 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 W0 in *; try done; clear init' W0.
      rewrite Z in *; destruct isrmw'.
        eapply hplus_ram_lD in UPD; eauto; desc; clarify.
        revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
        by desf; eauto.
      eapply hplus_ra_lD in UPD; eauto; desc; clarify.
      revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
      by desf; eauto.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    symmetry in UPD; rewrite hplusAC in UPD.
    destruct isrmw.
      eapply hplus_ram_lD in UPD; eauto; desc; clarify.
      revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
      by desf; eauto.
    eapply hplus_ra_lD in UPD; eauto; desc; clarify.
    revert UPD; unfold initialize, hupd; case eqP; intro; subst; try done.
    by desf; eauto.

  Case Armw.
    eapply vshift_hack in UPD.
    assert ( PP' QQ' isrmw', hi l = HVra PP' QQ' isrmw' true).
    { 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 W0 in *; try done; clear init' W0.
        rewrite Z in *; destruct isrmw'.
          eapply hplus_ram_lD in UPD; eauto; desc; clarify.
          by revert UPD; unfold initialize, hupd; desf; eauto.
        eapply hplus_ra_lD in UPD; eauto; desc; clarify.
        by revert UPD; unfold initialize, hupd; desf; eauto.
      rewrite hplusAC in UPD.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
      destruct isrmw.
        symmetry in UPD; eapply hplus_ram_lD in UPD; eauto; desc; clarify.
        by revert UPD; unfold initialize, hupd; desf; eauto.
      symmetry in UPD; eapply hplus_ra_lD in UPD; eauto; desc; clarify.
      by revert UPD; unfold initialize, hupd; desf; eauto. }
   desc.
   eapply hplus_eq_ra_initD in iEQ; eauto; desf.
     by eexists (hb_sb pre _); repeat (eexists; try edone).
   eapply hsum_eq_ra_initD 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_ra_initialized :
   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)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l PP QQ isrmw
    (LA: h l = HVra PP QQ isrmw true),
   cpre c,
    sb cpre c
    is_writeL (lab c) l
    (c = hb_fst edge happens_before lab sb rf mo c (hb_fst edge)).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  generalize (VALID _ IN).
  destruct (classic (is_writeL (lab (hb_fst edge)) l)) as [|NEQ]; eauto.
  {
    ins; red in H0; unfold unique in *; desf; ins; desf;
       pre; repeat eexists; eauto; instantiate;
      by rewrite Heq.
  }

  exploit helper_ra_init; 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.

Construction of the read_loses_perm list

Fixpoint map_pairo A B (f: A option B) l :=
  match l with
    | nilnil
    | x :: l'
      match f x with
        | Some y(x, y) :: map_pairo f l'
        | Nonemap_pairo f l'
      end
  end.

Lemma In_map_pairo A B (f : A option B) l x :
  In x (map_pairo f l) In (fst x) l f (fst x) = Some (snd x).
Proof.
  induction l; ins; try tauto.
  case_eq (f a); ins; rewrite IHl; clear IHl;
  ins; intuition; desf; ins; eauto.
Qed.

Lemma NoDup_map_fst_map_pairo A B (f : A option B) l :
  NoDup l NoDup (map (@fst _ _) (map_pairo f l)).
Proof.
  induction l; inversion 1; ins; desf; ins; eauto.
  inv H; constructor; eauto.
  rewrite In_map; intro; desf.
  rewrite In_map_pairo in *; desf.
Qed.

Lemma read_loses_perm_uniq :
   hmap lab sb rf r E v P
    (H: read_loses_perm hmap lab sb rf r E v P) P'
    (H': read_loses_perm hmap lab sb rf r E v P'),
  P = P'.
Proof.
  unfold read_loses_perm, unique in *; ins; desc.
  apply Lp2 in Lp; apply Lq2 in Lq; subst.
  rewrite Ep0, Eq0 in *; clarify.
  rewrite Gp0, Gq0 in *; clarify.
  assert (w0 = w) by (unfold ann_sw in *; des; congruence); subst.
  rewrite Ew0 in Ew; clarify.
  assert (SIM: Asim (Astar (sval (QQ' v)) (sval P)) (Astar (sval (QQ' v)) (sval P'))).
    by desf; rewrite Gw0 in *; clarify; eauto using Asim.
  clear H0 H'0.
  eapply assn_mod_eqI; eapply Asim_star_cancel in SIM.
  desf;
    try eapply (sim_assn_sem SIM) in LSEM;
    try eapply (sim_assn_sem SIM) in LSEM0; ins; desf.
Qed.

Lemma read_loses_perm1 hmap lab sb rf E res sws V :
  NoDup sws
   l,
    << NDl: NoDup (map (@fst _ _) l) >>
    << EQl: r P, In (r,P) l
               In r sws In r V
               read_loses_perm hmap lab sb rf r E res P >>
    << EQl': r P,
               In r sws In r V
               read_loses_perm hmap lab sb rf r E res P
               In (r,P) l >>.
Proof.
  eexists (map_pairo
          (fun r
             match (excluded_middle_informative
                      (! P, In r V read_loses_perm hmap lab sb rf r E res P)) with
                 | left pf
                   Some (sval (constructive_definite_description _ pf))
                 | _None
             end) sws).
  split; unfold NW.
    by apply NoDup_map_fst_map_pairo.
  split; intros.
    rewrite In_map_pairo in *; simpls; desc.
    split; try done; desf; desf; destruct e as (? & ? & ?); desc; ins.
  split; try done.
    by destruct (constructive_definite_description); ins; desf.

  rewrite In_map_pairo; ins; split; try done; desf.
  destruct e as (? & ? & M); desc; ins.
    f_equal; destruct (constructive_definite_description); ins; desf.
    by rewrite <- (M P), <- (M x0).
  eby destruct n; P; split; ins; desf; eapply read_loses_perm_uniq.
Qed.

This page has been generated by coqdoc Imprint | Data protection