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

Set Implicit Arguments.

Lemma go_back_one_val :
  ∀ lab sb rf hmap edge
    (VALID : hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET : hmap edge = Hdef hf) l v
    (LA : hf l = HVval v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = hb_fst edge ∧
    ¬ is_writeL (lab (hb_fst edge)) l ∧
    ∃ hf', hmap edge' = Hdef hf' ∧
                hf' l = HVval v.
Proof.
  unfold hmap_valid, unique; ins; desf; desf.
  Case Askip.
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (hf' l = HVval v).
      symmetry in VAL'; eapply hplus_val_lD; eauto.
      intros; eapply hsum_valD; eauto.
      repeat (eapply In_map; repeat (eexists; try edone)).
      by apply qOK.
    assert (hf0 l = HVval v).
      by eapply vshift_val with (l := l) in qEQ; rewrite H in ×.
    clear qEQ LA.
    eapply hsum_eq_val in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    by eapply pOK in pEQ2; eexists (hb_sb _ _); ins; eauto 6.

  Case Aalloc .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    by unfold hupd in *; ins; desf; vauto.

  Case Aalloc .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    by unfold hupd in *; ins; desf; vauto.

  Case Aload .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.

  Case Aload .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    rewrite hplusC in qEQ.
    symmetry in qEQ; eapply hplus_valD in qEQ; eauto; desf.
    2: by unfold hupd in qEQ1; desf; desf.
    eapply hplus_valD in qEQ; eauto; desf.
    {
      eapply hsum_eq_val in swsEQ; eauto; desf.
      repeat (rewrite In_map in *; desf).
      eapply swsOK in swsEQ2.
      eexists (hb_sw _ e); repeat (split; try edone); vauto.
    }
    ∃ (hb_sb pre e); repeat split; ins.
    destruct (hmap (hb_sb pre e)); ins.
      eexists; split; ins; instantiate; ins; clarify.
      rewrite hplusC, hplus_unfold in *; desf.
      by rewrite qEQ2; ins; desf.

  Case Astore .
    destruct edge; ins.
      by rewrite wEQ in GET; unfold hemp in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    intro; desf; destruct NW; split; ins; unfold hupd in *; desf; congruence.
    eexists; split; try edone.
    by unfold hupd in *; ins; desf; vauto; exfalso; eauto.

  Case Astore .
    ∃ (hb_sb pre (hb_fst edge)); ins; do 2 (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (N: hf' l = HVval v).
    { eapply hplus_val_rD; eauto; ins.
      destruct edge; ins.
        eapply hplus_val_rD; eauto; clear h'' H; ins.
        eapply hplus_val_lD; eauto; clear h'' H; ins.
        eapply hsum_valD; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOK.
      eapply hplus_val_lD; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    assert (N': hf0 l = HVval v).
      eapply vshift_val with (l := l) in UPD; rewrite N in *; try done.
      unfold initialize, hupd in *; desf; congruence.
    split; eauto; []; intro; desf.
    apply hplus_def_inv in VAL'; desf.
    generalize (PLUSv l); rewrite N; unfold hupd; desf; ins; desf.

  Case Armw.
    ins.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (N: hf' l = HVval v).
    { rewrite hplusC, !hplusA, <- hplusA in VAL'; eapply hplus_val_lD; eauto; ins.
      destruct edge; ins.
        eapply hplus_val_rD; eauto; clear h'' H; ins.
        eapply hsum_valD; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOutOK.
      eapply hplus_val_lD; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    assert (N': hi l = HVval v).
      by eapply vshift_val with (l := l) in UPD; rewrite N in ×.
    assert (l0 ≠ l).
      intro; eapply hplus_ra_lD in VAL'; eauto using hupds; desf; congruence.

    eapply hplus_valD in iEQ; eauto; desf.
      eexists (hb_sb pre _); repeat split; ins.
      rewrite pEQ; eexists; split; ins; instantiate; ins; clarify; congruence.
    eapply hsum_eq_val in iEQ0; eauto; desf.
    repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
    eexists (hb_sw _ _); repeat (split; try edone); vauto.
Qed.

Lemma heap_loc_na_initialized2 :
  ∀ 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 v (LA: h l = HVval v),
  ∃ cpre c hf,
    sb cpre c ∧
    is_writeLV (lab c) l v ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    is_val (hf l) ∧
    (c = hb_fst edge ∨ happens_before lab sb rf mo c (hb_fst edge)) ∧
    (∀ d
      (HB1: d = hb_fst edge ∨ happens_before lab sb rf mo d (hb_fst edge))
      (HB2: happens_before lab sb rf mo c d),
      ¬ is_writeL (lab d) l).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  generalize (VALID _ IN).
  destruct (classic (is_writeLV (lab (hb_fst edge)) l v)) as [|NEQ]; eauto.
  {
    ins; red in H0; unfold unique in *; desf; ins; desf.
      ∃ pre; repeat eexists; try eapply H2; eauto.
        by rewrite Heq.
      by red; ins; desf; eauto with hb.

    exfalso; destruct (hmap (hb_sb pre (hb_fst edge))); ins.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (N: hf' l = HVval v).
    { eapply hplus_val_rD; eauto; ins.
      destruct edge; ins.
        eapply hplus_val_rD; eauto; clear h'' H; ins.
        eapply hplus_val_lD; eauto; clear h'' H; ins.
        eapply hsum_valD; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOK.
      eapply hplus_val_lD; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    
    apply hplus_def_inv in VAL'; desf.
    generalize (PLUSv l); rewrite hupds in *; ins; desf; congruence.

    exfalso; destruct (hmap (hb_sb pre (hb_fst edge))); ins.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (N: hf' l = HVval v).
    { rewrite hplusC, !hplusA, <- hplusA in VAL'; eapply hplus_val_lD; eauto; ins.
      destruct edge; ins.
        eapply hplus_val_rD; eauto; clear h'' H; ins.
        eapply hsum_valD; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOutOK.
      eapply hplus_val_lD; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    apply hplus_def_inv in VAL'; desf.
    generalize (PLUSv l); rewrite hupds in *; ins; desf; congruence.
  }

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

{
  intro M; eapply x10, M; eauto.
  assert (N: is_access (lab d)) by (clear - M; destruct (lab d); ins).
  eapply valid_accessD in N; eauto using hist_closedD; desf.
  replace (loc (lab d)) with l in × by (clear - M; destruct (lab d); ins; desf).
  clear M; apply NNPP; intro M; apply not_or_and in M; desc.
  assert (IND : independent lab sb rf mo (edge' :: hb_sb pre d :: nil)).
    assert (happens_before lab sb rf mo (hb_fst edge) (hb_snd edge))
      by (destruct edge; ins; eauto with hb).
    assert (happens_before lab sb rf mo (hb_fst edge') (hb_snd edge'))
      by (destruct edge'; ins; eauto with hb).
    apply independent_two; ins; eauto; intro; desf; rewrite x1 in *;
    eauto 6 with hb.
  eapply independent_heap_compat in IND; eauto;
    try (by ins; desf; ins; desf; eauto with hb).
    desf; ins; rewrite hsum_two, N0, x3, hplus_unfold in IND; desf.
    by specialize (h1 l); rewrite x4 in *; ins; desf.
  by constructor; ins; intro; desf; ins; desf; eauto using t_trans, t_step.
}

{
  intro M; eapply x10, M; eauto.
  assert (N: is_access (lab d)) by (clear - M; destruct (lab d); ins).
  eapply valid_accessD in N; eauto using hist_closedD; desf.
  replace (loc (lab d)) with l in × by (clear - M; destruct (lab d); ins; desf).
  clear M; apply NNPP; intro M; apply not_or_and in M; desc.
  assert (IND : independent lab sb rf mo (edge' :: hb_sb pre d :: nil)).
    assert (happens_before lab sb rf mo (hb_fst edge) (hb_snd edge))
      by (destruct edge; ins; eauto with hb).
    assert (happens_before lab sb rf mo (hb_fst edge') (hb_snd edge'))
      by (destruct edge'; ins; eauto with hb).
    apply independent_two; ins; eauto; intro; desf; rewrite x1 in *;
    eauto 6 using t_step, t_trans with hb.
  eapply independent_heap_compat in IND; eauto;
    try (by ins; desf; ins; desf; eauto with hb).
    desf; ins; rewrite hsum_two, N0, x3, hplus_unfold in IND; desf.
    by specialize (h1 l); rewrite x4 in *; ins; desf.
  by constructor; ins; intro; desf; ins; desf; eauto using t_trans, t_step.
}
Qed.

Lemma hc_edge_hb mt lab sb rf mo a b :
  happens_before lab sb rf mo a b →
  clos_trans _ (hc_edge mt lab sb rf mo) a b.
Proof.
  induction 1; unfold imm_happens_before in *; desf;
  eauto using hc_edge, clos_trans.
Qed.

Lemma heap_loc_na_initialized :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (IRR: IrreflexiveHB lab sb rf mo)
    (ACYCLIC: acyclic (hc_edge mt 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 v (LA: h l = HVval v),
  ∃ cpre c hf,
    sb cpre c ∧
    is_writeLV (lab c) l v ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    is_val (hf l) ∧
    (c = hb_fst edge ∨ happens_before lab sb rf mo c (hb_fst edge)) ∧
    
    (∀ d
      (HB1: clos_refl_trans _ (hc_edge mt lab sb rf mo) d (hb_fst edge))
      (HB2: clos_trans _ (hc_edge mt lab sb rf mo) c d),
      ¬ is_writeL (lab d) l).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  generalize (VALID _ IN).
  destruct (classic (is_writeLV (lab (hb_fst edge)) l v)) as [|NEQ]; eauto.
  {
    ins; red in H0; unfold unique in *; desf; ins; desf.
      ∃ pre; repeat eexists; try eapply H2; eauto using clos_refl_trans.
        by rewrite Heq.
      by red; ins; rewrite clos_refl_transE in *; desf; eauto using t_trans.

    exfalso; destruct (hmap (hb_sb pre (hb_fst edge))); ins.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (N: hf' l = HVval v).
    { eapply hplus_val_rD; eauto; ins.
      destruct edge; ins.
        eapply hplus_val_rD; eauto; clear h'' H; ins.
        eapply hplus_val_lD; eauto; clear h'' H; ins.
        eapply hsum_valD; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOK.
      eapply hplus_val_lD; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    apply hplus_def_inv in VAL'; desf.
    generalize (PLUSv l); rewrite hupds in *; ins; desf; congruence.
    exfalso; destruct (hmap (hb_sb pre (hb_fst edge))); ins.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (N: hf' l = HVval v).
    { rewrite hplusC, !hplusA, <- hplusA in VAL'; eapply hplus_val_lD; eauto; ins.
      destruct edge; ins.
        eapply hplus_val_rD; eauto; clear h'' H; ins.
        eapply hsum_valD; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOutOK.
      eapply hplus_val_lD; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    apply hplus_def_inv in VAL'; desf.
    generalize (PLUSv l); rewrite hupds in *; ins; desf; congruence.
  }

  exploit go_back_one_val; 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; desc; repeat eexists; eauto with hb; ins; desc.
    by desf; eauto with hb.
{
  rewrite clos_refl_transE in HB1; destruct HB1 as [HB1|HB1]; clarify.
  intro M; eapply x10, M; eauto.
  assert (N: is_access (lab d)) by (clear - M; destruct (lab d); ins).
  eapply valid_accessD in N; try eapply VALID; desc.
  2: by clear -HB1 HC IN; induction HB1; eauto.
  replace (loc (lab d)) with l in × by (clear - M; destruct (lab d); ins; desf).
  clear M; rewrite clos_refl_transE; apply NNPP; intro M; apply not_or_and in M; desc.
  assert (IND : independent lab sb rf mo (edge' :: hb_sb pre d :: nil)).
    assert (happens_before lab sb rf mo (hb_fst edge) (hb_snd edge))
      by (destruct edge; ins; eauto with hb).
    assert (happens_before lab sb rf mo (hb_fst edge') (hb_snd edge'))
      by (destruct edge'; ins; eauto with hb).
    apply independent_two; ins; eauto; intro; desf; rewrite x1 in *;
    eauto 6 using hc_edge_hb, hc_edge, clos_trans with hb.
  eapply independent_heap_compat in IND; eauto;
    try (by ins; desf; ins; desf; eauto using hc_edge_hb, hc_edge with hb).
    desf; ins; rewrite hsum_two, N0, x3, hplus_unfold in IND; desf;
    by specialize (h1 l); rewrite x4 in *; ins; desf.
  by constructor; ins; intros [X|X]; clarify; simpls; clarify; eauto.

  clear x9; ins; desf; ins; eauto using hist_closedD.
  assert (clos_trans actid (hc_edge mt lab sb rf mo) a (hb_fst edge)).
    by eauto using hc_edge, clos_trans.
  by clear -H0 HC IN; induction H0; eauto.
}
Qed.

Lemma is_write_weaken typ l v : is_writeLV typ l v → is_writeL typ l.
Proof. destruct typ; ins; desf. Qed.

Lemma is_access_weaken typ l v : is_writeLV typ l v → is_access typ.
Proof. destruct typ; ins; desf. Qed.

Hint Resolve is_write_weaken is_access_weaken.

Lemma two_access_cases :
  ∀ mt pre a b acts lab sb rf mo hmap V hf
    (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)
    (INa : In a V)
    (INb : In b V)
    (SB : sb pre a) (HD: hmap (hb_sb pre a) = Hdef hf) (IV: is_val (hf (loc (lab a))))
    (B : is_access (lab b)) (LOC : loc (lab a) = loc (lab b)),
  a = b ∨ happens_before lab sb rf mo a b ∨ happens_before lab sb rf mo b a.
Proof.
  ins.
  eapply valid_accessD in B; eauto; desf.
  apply NNPP; intro X; apply not_or_and in X; desc; apply not_or_and in X0; desc.
  rewrite LOC in ×.
  assert (IND: independent lab sb rf mo (hb_sb pre a :: hb_sb pre0 b :: nil)).
    by apply independent_two; ins; intro; desf; eauto with hb.
  eapply independent_heap_compat in IND; eauto;
    try (by ins; desf; ins; desf; eauto with hb).
    desf; ins; rewrite hsum_two, HD, B0, hplus_unfold in IND; desf.
    by specialize (h0 (loc (lab b))); unfold is_val in *; desf; ins; desf.
  by constructor; ins; intro; desf; ins; desf; eauto using t_trans, t_step.
Qed.

Lemma hb_prev :
  ∀ lab sb rf mo a p n,
    happens_before lab sb rf mo a n →
    (∀ x, sb x n → x = p) →
    (∀ x, synchronizes_with lab sb rf mo x n → x = p) →
    a = p ∨ happens_before lab sb rf mo a p.
Proof.
  ins; apply clos_trans_tn1_iff in H.
  destruct H; destruct H; try rewrite ?(H0 _ H), ?(H1 _ H) in *; eauto;
    by right; apply clos_tn1_trans.
Qed.

Lemma go_back_one_na :
  ∀ lab sb rf hmap edge
    (VALID : hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET : hmap edge = Hdef hf) l
    (LA : is_val (hf l))
    (NW: lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = hb_fst edge ∧
    ∃ hf', hmap edge' = Hdef hf' ∧
                is_val (hf' l).
Proof.
  unfold hmap_valid, unique; ins; desf; desf.
  Case Askip.
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (is_val (hf' l)).
      eapply hplus_has_val_l; eauto.
      ins; eapply hsum_has_val; eauto.
      repeat (eapply In_map; repeat (eexists; try edone)).
      by apply qOK.
    assert (is_val (hf0 l)).
      by eapply vshift_val with (l := l) in qEQ; congruence.
    clear qEQ LA.
    eapply hsum_is_val in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    by eapply pOK in pEQ2; eexists (hb_sb _ _); ins; eauto 6.

  Case Aalloc .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    by unfold hupd in *; ins; desf; vauto.

  Case Aalloc .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    by unfold hupd in *; ins; desf; vauto.

  Case Aload .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.

  Case Aload .
    destruct edge; ins; try by red in EV; rewrite Heq in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    rewrite hplusC in qEQ.
    symmetry in qEQ; eapply hplus_is_val in qEQ; eauto; desf.
    2: by unfold hupd in qEQ1; desf; desf.
    eapply hplus_is_val in qEQ; eauto; desf.
      eapply hsum_is_val in swsEQ; eauto; desf.
      repeat (rewrite In_map in *; desf); rewrite swsOK in ×.
      by eexists (hb_sw _ _); ins; eauto 6.
    ∃ (hb_sb pre e); repeat split; ins.
    destruct (hmap (hb_sb pre e)); ins.
      eexists; split; ins; instantiate; ins; clarify.
      rewrite hplusC, hplus_unfold in *; desf.
      by destruct (hf3 l); ins; desf.

  Case Astore .
    destruct edge; ins.
      by rewrite wEQ in GET; unfold hemp in *; desf.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    eexists; split; try edone.
    by unfold hupd in *; ins; desf; vauto; exfalso; eauto.

  Case Astore .
    ∃ (hb_sb pre (hb_fst edge)); ins; do 2 (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    repeat (eexists; try edone).
    assert (N: is_val (hf' l)).
    { eapply hplus_has_val_r; eauto; ins.
      destruct edge; ins.
        eapply hplus_has_val_r; eauto; clear h'' H; ins.
        eapply hplus_has_val_l; eauto; clear h'' H; ins.
        eapply hsum_has_val; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOK.
      eapply hplus_has_val_l; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    eapply vshift_val with (l := l) in UPD; try congruence.
    rewrite UPD in *; unfold initialize, hupd in *; desf; congruence.

  Case Armw.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    assert (N: is_val (hf' l)).
    { rewrite hplusC, !hplusA, <- hplusA in VAL'; eapply hplus_has_val_l; eauto; ins.
      destruct edge; ins.
        eapply hplus_has_val_r; eauto; clear h'' H; ins.
        eapply hsum_has_val; eauto.
        repeat (eapply In_map; repeat (eexists; try edone)).
        by apply swsOutOK.
      eapply hplus_has_val_l; eauto; clear h'' H; ins.
      apply qU0 in EV; subst e'; rewrite GET in *; desf.
    }
    assert (l0 ≠ l).
      by intro; eapply hplus_ra_lD in VAL'; eauto using hupds; desf; rewrite VAL' in ×.

    eapply vshift_val with (l := l) in UPD; try congruence.
    rewrite UPD in *; unfold initialize, hupd in *; desf.
    eapply hplus_is_val in iEQ; eauto; desf; desf.
      eexists (hb_sb pre _); repeat split; ins.
      rewrite pEQ; eexists; split; ins; instantiate; ins; congruence.
    eapply hsum_is_val in iEQ0; eauto; desf.
    repeat (rewrite In_map in *; desf); rewrite swsInOK in ×.
    eexists (hb_sw _ _); repeat (split; try edone); vauto.
Qed.

Lemma heap_loc_na_allocated :
  ∀ 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 (LA: is_val (h l)),
  ∃ cpre c hf,
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = Hdef hf ∧
    hf l = HVuval ∧
    (cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.

  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
  {
     generalize (VALID _ IN).
     clear IH; unfold hmap_valid; desf; ins; desc.
     destruct edge; ins.
       by destruct EV; rewrite Heq in ×.
     eapply qU in EV; subst; rewrite GET in *; desf;
       rewrite hupds in *; desf.
     destruct qU; eauto 10 using hupds.
  }

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