Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 permission fslassn fslassnsem fslmodel fslassnlemmas fslhmap.
Require Import GpsSepAlg.

Set Implicit Arguments.

Lemma only_alloc_allocates PS PSg:
  ∀ lab sb rf mo hmap ga edge h g l
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap ga (hb_fst edge))
    (EV : edge_valid lab sb rf edge)
    (HM : hmap edge = Hdef h g)
    (ALL: h l ≠ @HVnone PS PSg)
    (NAb: ∀ x h g, sb x (hb_fst edge) →
                      hmap (hb_sb x (hb_fst edge)) = Hdef h g → h l = @HVnone PS PSg)
    (NAr: ∀ x h g, rf (hb_fst edge) = Some x →
                      hmap (hb_rf x (hb_fst edge)) = Hdef h g → h l = @HVnone PS PSg),
    lab (hb_fst edge) = Aalloc l.
Proof.
  ins; unfold hmap_valid, unique in VAL.
  desf; try first [progress f_equal|exfalso]; desc;
   try (destruct DISJ; desc); try clear TYP;
   destruct edge; ins; desf;
   try (by red in EV; rewrite Heq in EV; desc);
   try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf);
   try (by rewrite HM in sEQ; inv sEQ);
   try (eapply qU0 in EV; desf);
   try (by rewrite HM in *; desf; unfold hupd in *; desf; desf;
           exploit NAb; eauto).

  {
    assert (X: In e' posts) by (by apply qOK).
    eapply In_split in X; desf; rewrite !map_app, hsum_app in *;
    ins; rewrite hsum_cons, HM in ×.
    rewrite hdef_alt in DEF; desf.
    assert (hf l ≠ HVnone).
    {
      intro; symmetry in DEF.
      eapply hplus_nalloc in DEF; eauto; desf.
      eapply hplus_nalloc in DEF; eauto; desf.
      eapply hplus_nalloc in DEF4; eauto; desf.
    }
    rewrite DEF in EQ.
    eapply hplus_alloc in EQ; eauto; desf.
    eapply hsum_alloc in EQ; eauto; desf; eauto.
    eby repeat (rewrite In_map in *; desf); exploit NAb; try eapply pOK.
  }

  {
    rewrite HM in ×.
    rewrite hdef_alt in DEF; desf.
    rewrite DEF in EQ.
    symmetry in DEF; eapply hplus_preserves_alloc_r in DEF; eauto.
    eapply hplus_alloc in EQ; eauto; desf.
    eapply hsum_alloc in EQ; eauto; desf; eauto.
    eby repeat (rewrite In_map in *; desf); exploit NAb; try eapply pOK.
  }

  {
    rewrite HM in qEQ.
    symmetry in qEQ; eapply hplus_alloc in qEQ; eauto; desf.
    unfold hupd in qEQ0; desf; desf.
    exploit NAb; eauto; ins.
  }

  {
    rewrite HM in qEQ.
    symmetry in qEQ; eapply hplus_alloc in qEQ; eauto; desf.
    unfold hupd in qEQ0; desf; desf.
    exploit NAb; eauto; ins.
  }

  {
    rewrite qEQ in ×.
    eapply hplus_alloc in HM; eauto; desf.
    exploit NAb; eauto; ins.
  }


  {
    rewrite qEQ in ×.
    eapply hplus_alloc in HM; eauto; desf.
    × unfold hupd in HM0; desf; subst; try done.
      clear ALL; exploit NAb; eauto; ins.
      symmetry in pEQ'; eapply hplus_nalloc in pEQ'; eauto; desf.
      by rewrite hupds in ×.
    × eapply hplus_alloc in HM; eauto; desf.
      + eapply hsum_alloc_sim in rfsSIM; eauto; desc.
        repeat (rewrite In_map in *; desf).
        by eapply rfsOK in rfsSIM2; eauto.
      + eapply hplus_alloc in HM; eauto; desf.
        by symmetry in pEQ'; eapply hplus_preserves_alloc_r in pEQ'; eauto.
  }

  {
    symmetry in pEQ'; eapply hplus_preserves_alloc_l in pEQ'; eauto.
    rewrite sEQ in HM; inv HM.
    clear - ALL; unfold hupd in *; desf; desf.
  }

  {
    rewrite qEQ in HM; eapply hplus_alloc in HM; eauto; desf.
    unfold hupd in HM0; desf; desf; exploit NAb; eauto.
    by intro N; rewrite N in ×.
  }


  {
    by rewrite rEQ in HM; unfold hemp in *; desf.
  }

  {
    specialize (NAb pre).
    destruct (hmap (hb_sb pre e)); desf.
    specialize (NAb _ _ pU eq_refl).
    cut (initialize hf l0 l ≠ HVnone).
      by rewrite <- initialize_alloc; ins.
    rewrite qEQ in HM.
    apply hplus_eq_gheap in ghostEQ; desf.
    eapply hplus_alloc in HM; eauto; desf.
      by eapply hplus_preserves_alloc_l in UPD; eauto.
    eapply hplus_alloc in HM; eauto; desf.
    by rewrite hplusAC in UPD; eapply hplus_preserves_alloc_l in UPD; eauto.
  }

  {
    specialize (NAb pre);
    destruct (hmap (hb_sb pre e)); desf;
    specialize (NAb _ _ pU eq_refl).
    cut (initialize hf l0 l ≠ HVnone).
      by rewrite <- initialize_alloc; ins.
    red in rfsSIM; desf.
    destruct hr; apply hplus_eq_gheap in ghostEQ; desf.
    symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
    rewrite <- hplusA in UPD; eapply hplus_preserves_alloc_r in UPD; eauto.
    intro N.
    specialize (rfsSIM1 l); rewrite N in rfsSIM1; red in rfsSIM1; desf.
    symmetry in rfsSIM; eapply hplus_nalloc in rfsSIM; eauto; desf.
    symmetry in rfsSIM; eapply hsum_nalloc_all with (h := Hdef h g) in rfsSIM; eauto; desf.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
  }

  {
    rewrite HM in ×.
    specialize (NAb pre);
    destruct (hmap (hb_sb pre e)); desf;
    specialize (NAb _ _ pU eq_refl).
    cut (initialize hf l0 l ≠ HVnone).
      by rewrite <- initialize_alloc; ins.
    red in rfsSIM; desf.
    destruct hr; apply hplus_eq_gheap in ghostEQ; desf.
    symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
    rewrite <- hplusA in UPD; eapply hplus_preserves_alloc_r in UPD; eauto.
    intro N.
    specialize (rfsSIM1 l); rewrite N in rfsSIM1; red in rfsSIM1; desf.
    symmetry in rfsSIM; eapply hplus_nalloc in rfsSIM; eauto; desf.
  }

  {
    RMWin_def.
    rewrite HM in ×.
    symmetry in qEQ; eapply hplus_alloc in qEQ; eauto; desf.
    × unfold hupd in qEQ0; desf; desf.
      apply hplus_not_undef_l, hdef_alt in DEFin; desf.
      exploit (NAb pre); eauto; ins.
      rewrite DEFin in pEQ.
      eapply hplus_nalloc in pEQ; eauto; desf.
      by rewrite hupds in ×.
    × eapply hplus_alloc in qEQ; eauto; desf.
      + eapply Hsim_alloc in ACQsim; eauto; desf.
        red in TRANin; desf.
        rewrite TRANin in ×.
        symmetry in TRANin; eapply hplus_preserves_alloc_l in TRANin; eauto.
        eapply hsum_alloc in rInEQ; eauto; desf.
        repeat (rewrite In_map in *; desf).
        rewrite rfsInOK in ×.
        exploit NAr; eauto.
      + apply hplus_eq_gheap in ghostEQ; desf.
        eapply hplus_alloc in qEQ; eauto; desf.
        rewrite <- !hplusA in pEQ.
        apply hplus_not_undef_l, hdef_alt in DEFin; desf; rewrite DEFin in ×.
        eapply hplus_preserves_alloc_r in pEQ; eauto.
  }

  {
    RMWin_def.
    apply hplus_not_undef_r in DEF.
    assert (R := hplus_not_undef_l _ DEF).
    rewrite hdef_alt in DEF, R; desf.
    red in TRANout; desf.
    rewrite <- hplusA, TRANout, DEF in rOutEQ.
    rewrite R in DEF.
    eapply hsum_preserves_alloc in R; eauto.
      2: by repeat (rewrite In_map; eexists; split; eauto); apply rfsOutOK.
    symmetry in DEF; eapply hplus_preserves_alloc_l in DEF; eauto.
    apply hplus_eq_gheap in ghostEQ; desf.
    symmetry in rOutEQ; eapply hplus_alloc in rOutEQ; eauto; desf.
    eapply hplus_alloc in TRANout; eauto; desf.
    × eapply Hsim_alloc in RELsim; eauto; desf.
      apply hplus_not_undef_l, hdef_alt in DEFin; desf.
      rewrite hplusAC, DEFin in pEQ.
      eapply hplus_preserves_alloc_l in pEQ; eauto.
    × red in TRANin; desf.
      rewrite TRANin in ×.
      symmetry in TRANin; eapply hplus_preserves_alloc_r in TRANin; eauto.
      eapply hsum_alloc in rInEQ; eauto; desf.
      repeat (rewrite In_map in *; desf).
      rewrite rfsInOK in ×.
      exploit NAr; eauto.
  }
 
  {
    RMWin_def.
    rewrite HM in ×.
    apply hplus_not_undef_r, hdef_alt in DEF.
    red in TRANout; desf.
    rewrite <- hplusA, TRANout, DEF in rOutEQ.
    symmetry in DEF; eapply hplus_preserves_alloc_r in DEF; eauto.
    apply hplus_eq_gheap in ghostEQ; desf.
    symmetry in rOutEQ; eapply hplus_alloc in rOutEQ; eauto; desf.
    eapply hplus_alloc in TRANout; eauto; desf.
    × eapply Hsim_alloc in RELsim; eauto; desf.
      apply hplus_not_undef_l, hdef_alt in DEFin; desf.
      rewrite hplusAC, DEFin in pEQ.
      eapply hplus_preserves_alloc_l in pEQ; eauto.
    × red in TRANin; desf.
      rewrite TRANin in ×.
      symmetry in TRANin; eapply hplus_preserves_alloc_r in TRANin; eauto.
      eapply hsum_alloc in rInEQ; eauto; desf.
      repeat (rewrite In_map in *; desf).
      rewrite rfsInOK in ×.
      exploit NAr; eauto.
  }

  {
    assert (pD: hmap (hb_sb pre e) ≠ Hundef).
    {
      rewrite qEQ, <- !hplusA in DEF; apply hplus_not_undef_l in DEF; rewrite hplusA in DEF.
      cut (Hsim (hF +!+ hrel' +!+ hacq') (hF +!+ hrel +!+ hacq)).
        by rewrite pEQ; intros H ?; red in H; desf; congruence.
      apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in *).
        by apply Hsim_refl; intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in ×.
      by apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in *); apply Hsim_sym.
    }
    specialize (NAb pre);
    destruct (hmap (hb_sb pre e)); desf;
    specialize (NAb _ _ pU eq_refl).
    rewrite HM in ×.
    symmetry in qEQ; eapply hplus_alloc in qEQ; eauto; desf.
      by eapply hplus_preserves_alloc_l in pEQ; eauto.
    eapply hplus_alloc in qEQ; eauto; desf.
    × eapply Hsim_alloc in RELsim; eauto; desf.
      rewrite hplusAC in pEQ; eapply hplus_preserves_alloc_l in pEQ; eauto.
    × eapply hplus_alloc in qEQ; eauto; desf.
      eapply Hsim_alloc in ACQsim; eauto; desf.
      rewrite <- hplusA in pEQ; eapply hplus_preserves_alloc_r in pEQ; eauto.
  }
Qed.

Lemma heap_loc_allocated PS PSg :
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf )
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h g (GET: hmap edge = Hdef h g) l (LA: h l ≠ @HVnone PS PSg),
  ∃ c,
    lab c = Aalloc l ∧
    clos_refl_trans _ (happens_before_union_rf sb rf) c (hb_fst edge).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  red in VALID; desc.
  specialize (VLD _ IN).
  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ].
    by eauto using clos_refl_trans.
  cut (∃ edge' h' g',
         edge_valid lab sb rf edge' ∧
         hb_snd edge' = Some (hb_fst edge) ∧
         hmap edge' = Hdef h' g' ∧
         h' l ≠ HVnone).
    by intro; desf; exploit (IH edge'); eauto;
       [|intro; desf; repeat eexists; try edone];
       destruct edge'; ins; vauto; eauto using clos_refl_trans with hb.
  clear IH.
  apply NNPP; intro; destruct NEQ.
  eapply only_alloc_allocates; eauto.
    by ins; apply NNPP; intro; destruct H; eexists (hb_sb x _); ins; vauto.
  by ins; apply NNPP; intro; destruct H; eexists (hb_rf x _); ins; vauto.
Qed.

Definition independent sb rf T :=
  ∀ edge1 (IN1: In edge1 T) edge2 (IN2: In edge2 T)
      (HB: ∃ e, hb_snd edge1 = Some e ∧
           (e = hb_fst edge2 ∨ happens_before_union_rf sb rf e (hb_fst edge2))),
    False.

Lemma new_ghosts_are_ok PS PSg:
  ∀ h h' g hfs gs
    (DEF: h +!+ gheap _ _ g ≠ @Hundef PS PSg ) (DEF': h +!+ h' = Hdef hfs gs)
    (GHOSTS: ∀ hf' g' loc, h' = Hdef hf' g' → g' loc ≠ None → g loc = None),
  h +!+ gheap _ _ g +!+ h' = Hdef hfs (gres_plus_total g gs).
Proof.
  ins.
  destruct h as [ | hf gg]; destruct h' as [ | hf' gg']; ins.
  rewrite <- hplusA.
  rewrite hplus_unfold in *; desf; desf.
  assert (F: (fun v : val ⇒ hvplus (hf v) HVnone) = hf) by (by exten; ins; rewrite hvplusC).
  rewrite F; clear F.
  rewrite hplus_unfold; desf; desf.
  × f_equal; rewrite (gres_plus_totalC gg).
    apply gres_plus_totalA; try by rewrite (gres_plusC gg) in ×.
    rewrite gres_plus_gres_plus_totalA; try by rewrite (gres_plusC gg) in ×.
    by rewrite (gres_plus_totalC g).
  × destruct n; split; try done.
    unfold gres_plus; des_eqrefl; try done.
    unfold lift_plus in EQ; desf.
    destruct n; ins.
    unfold olift_plus; desf.
    exploit GHOSTS; eauto.
      by instantiate (1 := x); congruence.
      clear DEF GHOSTS; intro N.
      unfold gres_plus_total in Heq; desf.
      assert (GX: g0 x = gg x).
      {
        clear - Heq2 N.
        rewrite gres_plusC in ×.
        unfold gres_plus in ×. des_eqrefl; try done.
        desf.
        destruct gg; ins.
        unfold lift_plus in EQ; desf.
        destruct (lift_plus_helper (fun x0 : nat ⇒ olift_plus (plift_plus salg salg_plus) (g x0) (gres_fun x0)) n)
          as [g' EQ]; ins.
        specialize (EQ x); rewrite N in EQ; ins; desf.
      }
    rewrite GX in *; clear GX.
    destruct s as [A m]; destruct s0 as [A' m'].
    ins; desf; ins.
    + unfold gres_plus in GHOSTcompat; des_eqrefl; try done.
      clear GHOSTcompat; unfold lift_plus in EQ; desf.
      specialize (n x); rewrite Heq, Heq0 in n.
      ins; desf.
      rewrite <- eq_rect_eq in ×.
      congruence.
    + unfold gres_plus in GHOSTcompat; des_eqrefl; try done.
      clear GHOSTcompat; unfold lift_plus in EQ; desf.
      specialize (n0 x); rewrite Heq, Heq0 in n0.
      ins; desf.
Qed.

Lemma hsingl_with_ghosts_is_ok PS PSg:
  ∀ l hv h g hfs gs (DEF: h +!+ gheap _ _ g ≠ @Hundef PS PSg) (DEF': hsingl _ _ l hv +!+ h = Hdef hfs gs),
  hsingl _ _ l hv +!+ h +!+ gheap _ _ g = Hdef hfs (gres_plus_total g gs).
Proof.
  ins; destruct h as [ | hf gg]; ins.
  rewrite hplusAC, hplus_unfold; desf; desf.
    Focus 2.
    destruct n; unnw; split; ins.
    by apply hvplusDEFC.
    by rewrite gres_plusC, gres_plus_emp_r.
  rewrite hplus_unfold in *; desf; desf.
  × f_equal.
      2: by rewrite !gres_plus_total_emp_l, gres_plus_totalC.
    exten; ins. rewrite hvplusC; try done.
    unfold hupd; desf; desf.
    rewrite (hvplusC hv); ins.
    by apply hvplusDEFC.
  × destruct n; unnw; split; ins.
    by rewrite hvplusC; ins; apply hvplusDEFC.
    by rewrite gres_plus_total_emp_l.
Qed.

Lemma go_back_one PS PSg :
  ∀ acts lab sb rf mo ga
    (FIN: ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A : ConsistentAlloc lab) hmap e
    (VALID : hmap_valid lab sb rf hmap ga e) hFR
    (ALLOC : ∀ hf g loc,
               hFR = Hdef hf g → hf loc ≠ @HVnone PS PSg →
               ∃ c, lab c = Aalloc loc ∧ c ≠ e)
    (GHOSTS: ∀ hf g loc,
               hFR = Hdef hf g → g loc ≠ None →
               ga loc ≠ Some e),
  ∃ pres_sb pres_rf posts_sb posts_rf,
    NoDup pres_sb ∧
    NoDup pres_rf ∧
    NoDup posts_sb ∧
    NoDup posts_rf ∧
    (∀ x : actid, In x pres_sb ↔ sb x e) ∧
    (∀ x : actid, In x pres_rf ↔ rf e = Some x) ∧
    (∀ x : actid, In x posts_sb ↔ sb e x) ∧
    (∀ x : actid, In x posts_rf ↔ rf x = Some e) ∧
    (∀ h g
      (EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
           hsum (map hmap (map (hb_rf^~ e) pres_rf)) +!+ hFR =
           Hdef h g),
     let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
     ∃ h0 g0,
       hsum (map hmap (map (hb_sb e) posts_sb)) +!+
       hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR =
       Hdef h0 g0).
Proof.

  unfold hmap_valid; ins; desc.

  assert (GHOSTS': ∀ hf' g' loc, hFR = Hdef hf' g' → g' loc ≠ None → gnew loc = None).
  {
    ins.
    eapply GHOSTS in H0; eauto.
    apply NNPP; intro C; destruct H0.
    by apply NG.
  }

  unfold unique in *; ins; desf; desc; try (destruct DISJ; desc); try clear TYP;
    try (by red in a; rewrite Heq in a);
    try (by destruct n; red; rewrite Heq).

  Case Askip.
  {
    ∃ pres, nil, posts, nil; repeat (split; ins).
    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.
    rewrite hsum_nil, hplus_emp_l in ×.
    rewrite <- hplusA, <- EQ, hplusA.
    eexists _, _; apply new_ghosts_are_ok; eauto; congruence.
  }


  Case Aload .
  {
    pose proof (has_rf_pres e FIN CONS_RF); desc.
    ∃ (pre :: nil), rfs, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one in *; eauto.

    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.

    rewrite sEQ, qEQ, hsum_nil, !hplus_emp_l.
    rewrite hplusAC in EQ; apply hplus_def_inv_r in EQ; desf.
    rewrite hplusA.
    eexists _, _; apply new_ghosts_are_ok; eauto; congruence.
  }

  Case Aload .
  {
    ∃ (pre :: nil), rfs, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.

    rewrite sEQ in ×.
    rewrite qEQ, !hplusA; do 4 rewrite (hplusAC (hsingl _ _ _ _));
    rewrite <- hplusA, hplus_init1, !(hplusAC hr); ins.
    rewrite pEQ, <- pEQ', hplusA, !(hplusAC (hsum _)) in EQ.
    eapply hplus_sim_def_strong in EQ; try eassumption; desf.
    eexists _, _.
    do 2 rewrite <- hplusA; eapply new_ghosts_are_ok; rewrite ?hplusA; try edone.
    rewrite hplusAC, <- (hplusA hr).
    rewrite <- !hplusA in EQ; apply hplus_def_inv_l in EQ; desf; rewrite !hplusA, hplusAC in EQ.
    rewrite hdef_alt; eexists _, _.
    apply hsingl_with_ghosts_is_ok; try edone.
    by rewrite hplusA; intro U; rewrite U, ?hplus_undef_l, hplus_undef_r in ×.
  }


  Case Astore .
  {
    pose proof (has_rf_succs e FIN CONS_RF); desc.
    ∃ (pre :: nil), nil, (post :: nil), rfs; ins; repeat (split; ins; desf);
      rewrite ?sEQ, ?hsum_one, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.

    assert (M: hsum (map hmap (map (hb_rf e) rfs)) = hemp).
    {
      generalize (fun x ⇒ proj1 (INrfs x)); clear - rEQ.
      by induction rfs; ins; rewrite hsum_cons, IHrfs, hplus_emp_r; eauto.
    }
    rewrite M, hplus_emp_l in ×.
    rewrite pEQ, qEQ in ×.
    exploit hdef_upd_alloc; eauto; ins; desf.
    eby eexists _, _; rewrite hplusA; apply new_ghosts_are_ok.
  }

  Case Astore .
  {
    ∃ (pre :: nil), nil, (post :: nil), rfs; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.

    rewrite pEQ in EQ.
    apply hplus_init_def with (l := l) in EQ.
    rewrite UPD, !hplusA in EQ.
    rewrite hplusAC in EQ.
    rewrite <- hdef_alt, <- (hplusA _ _ hFR), hplusAC.
    rewrite Hsim_sym in rfsSIM; eapply hplus_sim_def; eauto.
    rewrite qEQ, !hplusA, !(hplusAC hF), (hplusAC (hsingl _ _ _ _)), <- hplusA, <- hplusA.
    rewrite hdef_alt, (hplusAC hr) in EQ; desf.
    rewrite <- (hplusA rfg), (hplusC rfg), ghostEQ, hdef_alt.
    eexists _, _; apply new_ghosts_are_ok; rewrite ?hplusA; try edone.
    rewrite qEQ, hplusC in DEF; eapply hplus_sim_def in DEF.
      2: eby apply Hsim_sym.
    rewrite !hplusA, <- !(hplusAC rfg), (hplusC rfg), ghostEQ in DEF.
    by rewrite !(hplusAC hr), (hplusAC (hsingl _ _ _ _)).
  }

  Case Armw.
  {
    ∃ (pre :: nil), rfsIn, (post :: nil), rfsOut; repeat (split; ins; desc); eauto; try by desf.
    rewrite hsum_one in ×.
    rewrite pEQ, rInEQ, !hplusA in EQ.
    rewrite qEQ, <- (hplusA _ _ hFR), rOutEQ, !hplusA.
    pattern g in EQ; apply ex_intro in EQ;
    pattern h in EQ; apply ex_intro in EQ; rewrite <- hdef_alt in EQ.
    rewrite hplusAC in EQ; eapply hplus_sim_def in EQ; eauto.
    rewrite !(hplusAC hacq) in EQ; eapply hplus_sim_def in EQ; eauto.
    apply hdef_alt; rewrite !(hplusAC hrel'), !(hplusAC hacq'); rewrite (hplusAC ht).
    rewrite hdef_alt in EQ; desf.
    rewrite <- (hplusA sbg), ghostEQ, hdef_alt; eexists _, _.
    do 4 rewrite <- hplusA; apply new_ghosts_are_ok; rewrite ?hplusA; try edone.
    by rewrite qEQ, rOutEQ, !hplusA, <- !(hplusAC sbg), ghostEQ, !(hplusAC hrel'), !(hplusAC hacq') in DEF.
  }

  Case Aalloc.
  {
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desc);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto; clear n;
      try (by desf);
      try (by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf);
      try (by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf).
    desf; rewrite pEQ, qEQ, hplusA in *; destruct hFR; ins;
    eexists _, _; apply new_ghosts_are_ok; try edone;
    rewrite hplus_unfold in *; desf; desf; vauto;
    destruct n; split; try done;
    intro l'; specialize (HEAPcompat l');
    unfold hupd in *; desf; desf;
    specialize (ALLOC _ _ l eq_refl);
    destruct (hf0 l); desf; destruct ALLOC; desf;
    by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.
  }

  Case Afence.
  {
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.
    rewrite pEQ, qEQ, !hplusA in ×.
    rewrite hplusAC in EQ; eapply hplus_sim_def_strong in EQ; eauto; desf.
    rewrite !(hplusAC hacq) in EQ; eapply hplus_sim_def_strong in EQ; eauto; desf.
    rewrite hplusAC, !(hplusAC hacq'), <- hplusA, <- hplusA.
    eexists _, _; apply new_ghosts_are_ok; rewrite ?hplusA; try edone.
    by rewrite hplusAC, !(hplusAC hacq') in DEF.
  }
Qed.

Lemma step_back_ghost PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (GALL: g l ≠ None),
  << GA: ga l = Some (hb_fst edge) >> ∨
  ∃ edge' hf' g', << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
                       << EV': edge_valid lab sb rf edge' >> ∧
                       << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
                       << GALL': g' l ≠ None >>.
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desf; desc; try (destruct DISJ; desc); destruct edge; ins; try clear TYP; desf;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e'); desf; desf; rewrite Heq in *; desf);
    rewrite ?(qU0 _ EV), ?MAP in *; desf;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP);
    try solve[ symmetry in qEQ; eapply hplus_galloc in qEQ; eauto; desf; try (by left; apply NG);
               right; eexists (hb_sb _ e), _, _; ins; repeat split; eauto].

  {
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    assert (D := (hplus_def_inv_l _ _ DEF)); desf.
    rewrite D in ×.
    eapply hsum_preserves_galloc with (hf' := hf) (g' := g) in D; eauto.
      2: by repeat (rewrite In_map; eexists; split; try edone); apply qOK.
    symmetry in DEF; eapply hplus_preserves_galloc_l in DEF; eauto.
    eapply hplus_galloc in EQ; eauto; desf; try (by left; apply NG).
    right.
    eapply hsum_galloc in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
    by apply pOK.
  }

  {
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    symmetry in DEF; eapply hplus_preserves_galloc_r in DEF; eauto.
    eapply hplus_galloc in EQ; eauto; desf; try (by left; apply NG).
    right.
    eapply hsum_galloc in EQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
    by apply pOK.
  }

  {
    symmetry in qEQ; eapply hplus_galloc in qEQ; eauto; desf.
    eapply hplus_galloc in qEQ; eauto; desf.
    × right.
      red in rfsSIM; desf.
      eapply hsum_galloc in rfsSIM; eauto; desf.
      repeat (rewrite In_map in *; desf).
      eexists (hb_rf _ e), _, _; ins; repeat split; eauto.
      by apply rfsOK.
    × eapply hplus_galloc in qEQ; eauto; desf; try (by left; apply NG).
      right.
      symmetry in pEQ'; eapply hplus_preserves_galloc_r in pEQ'; eauto.
      eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
  }

  {
    symmetry in qEQ; eapply hplus_galloc in qEQ; eauto; desf.
    eapply hplus_galloc in qEQ; eauto; desf.
    × right.
      eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
      rewrite hplusAC in UPD; eapply hplus_preserves_galloc_l in UPD; eauto.
    × left.
      apply NG.
      eapply hplus_preserves_galloc_l; eauto.
  }

  {
    red in rfsSIM; desf.
    assert (D := hplus_def_inv_l _ _ rfsSIM); desf; rewrite D in ×.
    eapply hsum_preserves_galloc with (hf' := hf) (g' := g) in D; eauto.
      2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
    symmetry in rfsSIM; eapply hplus_preserves_galloc_l in rfsSIM; eauto.
    eapply hplus_galloc in rfsSIM0; eauto; desf.
      right; eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
      by rewrite <- hplusA in UPD; eapply hplus_preserves_galloc_r in UPD; eauto.
    left; apply NG.
    eapply hplus_preserves_galloc_r; eauto.
  }
  
  {
    red in rfsSIM; desf.
    symmetry in rfsSIM; eapply hplus_preserves_galloc_r in rfsSIM; eauto.
    eapply hplus_galloc in rfsSIM0; eauto; desf.
      right; eexists (hb_sb _ e), _, _; split; ins; repeat split; eauto.
      by rewrite <- hplusA in UPD; eapply hplus_preserves_galloc_r in UPD; eauto.
    left; apply NG.
    eapply hplus_preserves_galloc_r; eauto.
  }

  {
    exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desf.
    symmetry in qEQ; eapply hplus_galloc in qEQ; eauto; desf.
    eapply hplus_galloc in qEQ; eauto; desf.
    × right.
      red in ACQsim; desf.
      eapply hplus_def_inv_r in D; desf; rewrite D in ×.
      eapply hplus_preserves_galloc_l in rInEQ; eauto.
      eapply hsum_galloc in D; eauto; desf.
      repeat (rewrite In_map in *; desf).
      eexists (hb_rf _ e), _, _; ins; repeat split; eauto.
      by apply rfsInOK.
    × eapply hplus_galloc in qEQ; eauto; desf; try (by left; apply NG).
      + right.
        eapply hplus_def_inv_l in D; desf; rewrite D in ×.
        eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
        rewrite <- hplusA in pEQ; eapply hplus_preserves_galloc_r in pEQ; eauto.
      + left; apply NG.
        eapply hplus_preserves_galloc_l; eauto.
  }

  {
    exploit RMWinDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desf.
    apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
    assert (R := hplus_def_inv_l _ _ DEF); desf; rewrite R in ×.
    eapply hsum_preserves_galloc with (hf' := hf) (g' := g) in R; eauto.
      2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
    symmetry in DEF; eapply hplus_preserves_galloc_l in DEF; eauto.
    symmetry in rOutEQ; eapply hplus_galloc in rOutEQ; eauto; desf.
    × red in RELsim; desf.
      eapply hplus_def_inv_l in D; desf; rewrite D in ×.
      right; eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
      rewrite <- hplusAC in pEQ; eapply hplus_preserves_galloc_l in pEQ; eauto.
    × eapply hplus_galloc in rOutEQ; eauto; desf.
      + eapply hplus_def_inv_r in D; desf; rewrite D in ×.
        eapply hplus_preserves_galloc_r in rInEQ; eauto.
        eapply hsum_galloc in D; eauto; desf.
        repeat (rewrite In_map in *; desf).
        right; eexists (hb_rf _ e), _, _; ins; repeat split; eauto.
        by apply rfsInOK.
      + left; apply NG.
        eapply hplus_preserves_galloc_r; eauto.
  }

  {
    exploit RMWinDEF; try exact pEQ; try eassumption; try (eby rewrite <- MAP in *); intro D; desf.
    apply hplus_not_undef_r, hdef_alt in DEF; desf; rewrite DEF in ×.
    symmetry in DEF; eapply hplus_preserves_galloc_r in DEF; eauto.
    symmetry in rOutEQ; eapply hplus_galloc in rOutEQ; eauto; desf.
    × red in RELsim; desf.
      eapply hplus_def_inv_l in D; desf; rewrite D in ×.
      right; eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
      rewrite <- hplusAC in pEQ; eapply hplus_preserves_galloc_l in pEQ; eauto.
    × eapply hplus_galloc in rOutEQ; eauto; desf.
      + eapply hplus_def_inv_r in D; desf; rewrite D in ×.
        eapply hplus_preserves_galloc_r in rInEQ; eauto.
        eapply hsum_galloc in D; eauto; desf.
        repeat (rewrite In_map in *; desf).
        right; eexists (hb_rf _ e), _, _; ins; repeat split; eauto.
        by apply rfsInOK.
      + left; apply NG.
        eapply hplus_preserves_galloc_r; eauto.
  }

  {
    exploit FenceInDEF; try eassumption; try (eby rewrite <- MAP in *); intro D; desf; rewrite D in ×.
    symmetry in qEQ; eapply hplus_galloc in qEQ; eauto; desf.
    × right.
      eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
      eby eapply hplus_preserves_galloc_l in pEQ.
    × eapply hplus_galloc in qEQ; eauto; desf.
      + right.
        eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
        red in RELsim; desf.
        eby rewrite hplusAC in pEQ; eapply hplus_preserves_galloc_l in pEQ.
      + eapply hplus_galloc in qEQ; eauto; desf; try (by left; apply NG).
        right.
        eexists (hb_sb _ e), _, _; ins; repeat split; eauto.
        red in ACQsim; desf.
        eby rewrite <- hplusA in pEQ; eapply hplus_preserves_galloc_r in pEQ.
  }
Qed.

Lemma ghost_allocated PS PSg :
  ∀ lab sb rf mo hmap ga V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: ∀ e : actid, In e V → hmap_valid lab sb rf hmap ga e)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h g (GET: hmap edge = @Hdef PS PSg h g) l
    (GL: g l ≠ None),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    ga l = Some (hb_fst edge') ∧
    (edge' = edge ∨ happens_before_union_rf sb rf (hb_fst edge') (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 (ga l = Some (hb_fst edge))) as [GA|NGA]; eauto.
  ins; exploit step_back_ghost; eauto; ins; desf.
  assert (HB: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)).
    by destruct edge'; ins; desf; eauto with hb.
  exploit (IH edge'); eauto.
  intro; desf; repeat eexists; eauto using implies_trans with hb ; ins; desf; eauto.
Qed.

Lemma get_pres_aux :
  ∀ sb rf V a
    (HC : hist_closed sb rf V)
    (IN : In a V),
   ∃ pres_sb pres_rf,
     << NDb : NoDup pres_sb >> ∧
     << NDr : NoDup pres_rf >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x a >> ∧
     << Pr : ∀ x, In x pres_rf ↔ rf a = Some x >>.
Proof.
  intros; unfold NW.
  ∃ (undup (filter (fun x ⇒ mydec (sb x a)) V)),
         (undup (filter (fun x ⇒ mydec (rf a = Some x)) V)).
  do 2 (split; [by apply/uniqP; apply undup_uniq|]); split;
  ins; rewrite (In_mem_eq (mem_undup (T:=Vbase.nat_eqType) _)), In_filter;
  unfold mydec; desf; split; ins; desf; eauto using hist_closedD with hb.
Qed.

Lemma get_pres :
  ∀ lab sb rf V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (HC : hist_closed sb rf V) edge T
    (ND : NoDup T)
    (IN : In edge T)
    (INCL : ∀ edge, In edge T → In (hb_fst edge) V)
    (EVS : ∀ edge, In edge T → edge_valid lab sb rf edge)
    (DEEP : ∀ edge', In edge' T →
              happens_before_union_rf sb rf (hb_fst edge) (hb_fst edge') → False)
    (IND: independent sb rf T),
   ∃ pres_sb pres_rf,
     let res := map (fun x ⇒ hb_sb x (hb_fst edge)) pres_sb ++
                map (fun x ⇒ hb_rf x (hb_fst edge)) pres_rf ++
                filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T in
     << NDb : NoDup pres_sb >> ∧
     << NDr : NoDup pres_rf >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x (hb_fst edge) >> ∧
     << Pr : ∀ x, In x pres_rf ↔ rf (hb_fst edge) = Some x >> ∧
     << ND' : NoDup res >> ∧
     << METR: (depth_metric (happens_before_union_rf sb rf) V (map hb_fst res) <
               depth_metric (happens_before_union_rf sb rf) V (map hb_fst T) : Prop) >> ∧
     << INCL': ∀ edge, In edge res → In (hb_fst edge) V >> ∧
     << EVS' : ∀ edge, In edge res → edge_valid lab sb rf edge >> ∧
     << IND' : independent sb rf res >>.
Proof.
  intros; exploit get_pres_aux; eauto; intro; desf.
  ∃ pres_sb, pres_rf; unfold NW;
  repeat (split; try done).

  by rewrite !nodup_app; intuition; try (apply nodup_map; try done; congruence);
     red; ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     apply (IND _ IN2 _ IN); eexists; split; vauto.

  {
    apply depth_lt with (hb_fst edge);
    eauto using In_mapI.
      by ins; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
         rewrite ?Pr, ?Pb in *; eauto using In_mapI with hb; exfalso; eauto.

     intro; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
         rewrite ?Pr, ?Pb in *; eauto using In_mapI with hb.
     by destruct (eqP (hb_fst x) (hb_fst edge)).

     red; ins; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
     rewrite ?Pr, ?Pb in *; eauto with hb.

     by ins; rewrite In_map in *; desf; eauto.
  }

  by ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pr, ?Pb in *; eauto with hb.

  by ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pr, ?Pb in *; eauto.

  {
    red; ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pw, ?Pb in *; try (injection HB; ins); subst; eauto with hb;
     try (revert IN0; case eqP; ins; congruence);
     try (apply (IND _ IN1 _ IN); eexists; split; eauto; right; vauto).
     × apply Pr in IN0; eapply ACYCLIC; vauto.
     × apply Pr in IN0; eapply ACYCLIC; vauto.
     × apply Pr in IN0; vauto.
     × apply happens_before_union_rf_trans with (b := x); vauto.
     × apply Pr in IN0; eapply ACYCLIC,happens_before_union_rf_trans; vauto.
     × apply Pr in IN0; eapply ACYCLIC,happens_before_union_rf_trans; vauto.
     × apply Pr in IN0; apply happens_before_union_rf_trans with (b := x); vauto.
  }
Qed.

Theorem independent_heap_compat PS PSg :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab) hmap V
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    T (ND: NoDup T)
      (SSB: ∀ a b (IN: In (hb_sb a b) T), In a V)
      (SSW: ∀ a b (IN: In (hb_rf a b) T), In a V)
      (Ssink: ∀ a (IN: In (hb_sink a) T), In a V)
      (TSB: ∀ a b (IN: In (hb_sb a b) T), sb a b)
      (TSW: ∀ a b (IN: In (hb_rf a b) T), rf b = Some a)
      (Tsink: ∀ a (IN: In (hb_sink a) T), ann_sink lab a)
    (INDEP: independent sb rf T),
    ∃ h g, hsum (map hmap T) = @Hdef PS PSg h g.
Proof.
  intros until T; induction T using
    (well_founded_ind (wf_ltof
       (fun T ⇒ depth_metric (happens_before_union_rf sb rf) V (map hb_fst T)))).
  case_eq (depth_metric (happens_before_union_rf sb rf) V (map hb_fst T)); ins.
  {
    clear H.
    destruct T; unfold depth_metric in *; ins; vauto.
    assert (IN: In (hb_fst h) V) by (destruct h; ins; eauto).
    eapply In_implies_perm in IN; desf.
    rewrite (Permutation_count IN) in H0; ins; desf.
    unfold is_pred, mydec in Heq; ins; desf.
    exfalso; eauto using rt_refl.
  }
  exploit (get_deepest ACYCLIC HC (T:=T)).
    by intro; subst; clear - H0; induction V; ins.
    by destruct edge; ins; eauto.
  intro; clear n H0; desc.

  exploit get_pres; eauto; try (by intros []; ins; eauto).
  ins; desf.

  destruct (H _ METR ND'); ins; eauto;
    try solve [by apply INCL' in IN0|by apply EVS' in IN0].
  clear H METR ND'.
  remember (hb_fst edge) as e; clear edge IN Heqe.

  rewrite !map_app, !hsum_app in ×.

  cut (∃ posts_sb posts_rf,
           NoDup posts_sb ∧ NoDup posts_rf ∧
           (∀ x, In x posts_sb ↔ sb e x) ∧
           (∀ x, In x posts_rf ↔ rf x = Some e) ∧
       ∃ h0 g0,
         hsum (map hmap (filter (fun x ⇒ (hb_fst x != e) || (x == hb_sink e)) T)) +!+
         hsum (map hmap (map (hb_sb e) posts_sb)) +!+
         hsum (map hmap (map (hb_rf e) posts_rf)) = Hdef h0 g0).
    intros; desf.
    assert (M := helper_perm_filter_post e T); desf.
    rewrite (hsum_perm (map_perm _ M)).
    destruct (@perm_from_subset _ posts_sb posts_sb0) as [? Psb].
      by eapply (Permutation_NoDup M) in ND; rewrite !nodup_app in ND;
         desf; eauto using NoDup_mapD.
      by symmetry in M; intros; apply H2, TSB, (Permutation_in _ M), In_appI2, In_appI1, In_mapI.

    destruct (@perm_from_subset _ posts_rf posts_rf0) as [? Prf].
      by eapply (Permutation_NoDup M) in ND; rewrite !nodup_app in ND;
         desf; eauto using NoDup_mapD.
      by symmetry in M; intros; apply H3, TSW, (Permutation_in _ M), In_appI2, In_appI2, In_mapI.

    rewrite (hsum_perm (map_perm _ (map_perm _ Psb))) in H4.
    rewrite (hsum_perm (map_perm _ (map_perm _ Prf))) in H4.

    eapply hplus_def_inv_l with (hf := h0) (g := g0); rewrite <- H4.
    rewrite !map_app, !hsum_app, !hplusA.
    f_equal; f_equal.
    by symmetry; rewrite hplusAC; f_equal.

  assert (ALLOC: ∀ hf g loc,
            hsum (map hmap (filter (fun x ⇒ hb_fst x != e) T)) = Hdef hf g →
            hf loc ≠ HVnone →
            ∃ c, lab c = Aalloc loc ∧ c ≠ e).
  {
    intros; eapply hsum_alloc in H; eauto; desf.
    rewrite In_map in *; desf.
    rewrite In_filter in *; desf.
    exploit heap_loc_allocated; eauto; try (by destruct x0; ins; eauto).
    destruct (eqP (hb_fst x0) e); ins; desf; eexists; split; eauto; intro; desf.
    by eapply clos_refl_trans_hbUrfE in x1; desf; eapply DEEP; eauto.
  }

  red in VALID; desc.

  assert (GHOSTS: ∀ hf g loc,
            hsum (map hmap (filter (fun x ⇒ hb_fst x != e) T)) = Hdef hf g →
            g loc ≠ None → ga loc ≠ Some e).
  {
    intros ? gg ? SUM ALL GALL.
    eapply hsum_galloc in SUM; eauto; desf.
    rewrite In_map in SUM; desf.
    rewrite In_filter in SUM1; desf.
    exploit ghost_allocated; eauto; try by intuition.
    intro C; desf.
    eby eapply neq_contra.
    eby eapply DEEP.
  }

  ins; exploit go_back_one; eauto; []; intro K; desc.
  exploit (NoDup_Permutation K NDb); [by intro; rewrite Pb|].
  exploit (NoDup_Permutation K0 NDr); [by intro; rewrite Pr|].
  clear Pb Pr; intros Pb Pr.
  rewrite (hsum_perm (map_perm _ (map_perm _ Pb))) in K7.
  rewrite (hsum_perm (map_perm _ (map_perm _ Pr))) in K7.
  edestruct K7; ins; eauto.
  ∃ posts_sb, posts_rf; repeat (split; ins).
  rewrite (hsum_perm ((map_perm _ (helper_filter_decide_sink _ ND)))).
  desf.
  by simpls; rewrite hsum_cons; rewrite hplusC, !hplusA; eexists; eauto.
  by specialize (Tsink _ i).
  eby rewrite !(hplusAC (hmap (hb_sink e))) in H; apply hplus_def_inv_r in H; desf;
      rewrite hplusC, hplusA; eexists _, _.
  eby rewrite hplus_emp_l in H; rewrite hplusC, hplusA; eexists _, _.
Qed.