Require Import Vbase.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnlemmas fslmodel fslhmap ihc.

Set Implicit Arguments.

Lemma go_back_one_val :
  ∀ lab sb rf mo hmap edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (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 : has_value (hf l) v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
  ∃ edge´,
    edge_valid lab sb rf edge´ ∧
    hb_snd edge´ = Some (hb_fst edge) ∧
    ¬ is_writeL (lab (hb_fst edge)) l ∧
    ∃ hf´, hmap edge´ = Hdef hf´ ∧ has_value (hf´ l) v.
Proof.
  unfold hmap_valid, unique; ins; desf; desc; try destruct DISJ; desc; try clear TYP; desf.

  Case Askip.
  {
    destruct edge; ins.
    × symmetry in qEQ; assert (EQ := hplus_def_inv_l _ _ qEQ); desf; rewrite EQ in ×.
      eapply hsum_valD_weak in EQ; eauto.
        2: by repeat (rewrite In_map; eexists,; eauto); rewrite qOK.
      symmetry in qEQ; eapply hplus_val_lD_weak in qEQ; ins; desf; eauto.
      eapply hsum_eq_val_weak in pEQ; eauto; desf.
      repeat (rewrite In_map in *; desf).
      rewrite pOK in pEQ2.
      eexists (hb_sb _ _); repeat split; ins; eauto.
    × specialize (CONS_RF e´); desf; rewrite Heq in *; desf.
    × rewrite GET in qEQ; eapply hplus_val_rD_weak in qEQ; ins; desf; eauto.
      eapply hsum_eq_val_weak in pEQ; eauto; desf.
      repeat (rewrite In_map in *; desf).
      rewrite pOK in pEQ2.
      eexists (hb_sb _ _); repeat split; ins; eauto.
  }

  Case Aalloc .
  {
    destruct edge; ins; try (by red in EV; rewrite Heq in *; desf);
                        try (by specialize (CONS_RF e´); desf; 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);
                        try (by specialize (CONS_RF e´); desf; 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 by specialize (CONS_RF e´); desf; 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.
    × rewrite GET in sEQ; inv sEQ.
  }

  Case Aload .
  {
    destruct edge; ins; try by specialize (CONS_RF e´); desf; rewrite Heq in *; desf.
    × apply qU0 in EV; subst e´; rewrite GET in *; desf.
      rewrite hplusC in qEQ.
      symmetry in qEQ; eapply hplus_valD_weak in qEQ; eauto; desf.
        2: by unfold hupd in qEQ1; desf; desf.
      eapply hplus_valD_weak in qEQ; eauto; desf.
      + red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        rewrite <- has_value_sim in qEQ2; eauto.
        eapply hsum_eq_val_weak in rfsSIM; eauto; desf.
        repeat (rewrite In_map in *; desf).
        rewrite rfsOK in rfsSIM3.
        eexists (hb_rf _ _); repeat split; ins; eauto.
      + symmetry in pEQ´; eapply hplus_val_rD_weak in pEQ´; ins; desf; eauto.
        eexists (hb_sb _ _); repeat split; ins; eauto.
    × rewrite GET in sEQ; inv sEQ.
      clear - LA; unfold hupd in LA; desf; desf.
  }

  Case Astore .
  {
    destruct edge; ins; try by rewrite ?rEQ, ?sEQ in GET; inv GET.
    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; rewrite hupds in ×.
      red in LA; destruct NW; eauto.
    × eexists,; 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.
    cut (has_value (hf0 l) v).
    {
      intro V; split; [ | eby eexists,].
      intro; desf.
      rewrite qEQ, hplusA in UPD.
      symmetry in UPD; eapply hplus_ra_lD in UPD.
        2: by rewrite hupds; eauto.
      by desf;unfold initialize in UPD; desf; rewrite hupds in UPD.
    }
    {
      destruct edge; ins.
      × rewrite (qU0 _ EV), GET in ×.
        eapply hplus_val_lD_weak in UPD; ins; desf; eauto.
        clear - UPD; unfold initialize, hupd in UPD; desf; try done.
        by rewrite Heq0.
      × red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        assert (EQ := hplus_def_inv_l _ _ rfsSIM); desf; rewrite EQ in ×.
        eapply hsum_valD_weak in EQ; eauto.
          2: by repeat (rewrite In_map; eexists,; eauto); rewrite rfsOK.
        symmetry in rfsSIM; eapply hplus_val_lD_weak in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        eapply hplus_val_rD_weak in UPD; ins; desf; eauto.
        clear - UPD; unfold initialize, hupd in UPD; desf; try done.
        by rewrite Heq0.
      × red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        rewrite GET in ×.
        symmetry in rfsSIM; eapply hplus_val_rD_weak in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        eapply hplus_val_rD_weak in UPD; ins; desf; eauto.
        clear - UPD; unfold initialize, hupd in UPD; desf; try done.
        by rewrite Heq0.
    }
  }

  Case Afence.
  {
    ∃ (hb_sb pre (hb_fst edge)); ins; repeat (split; ins; desf).
    rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
    eexists,; eauto.
    destruct edge; ins; try (by red in EV; rewrite Heq in *; desf);
                        try (by specialize (CONS_RF e´); desf; rewrite Heq in *; desf).
    rewrite (qU0 _ EV), GET in ×.
    symmetry in qEQ; eapply hplus_valD_weak in qEQ; eauto; desf.
    × eapply hplus_val_lD_weak in pEQ; ins; desf; eauto.
    × eapply hplus_valD_weak in qEQ0; eauto; desf.
      + red in RELsim; desf.
        specialize (RELsim1 l).
        rewrite <- (has_value_sim _ _ _ RELsim1) in qEQ3.
        rewrite hplusAC in pEQ; eapply hplus_val_lD_weak in pEQ; ins; desf; eauto.
      + red in ACQsim; desf.
        specialize (ACQsim1 l).
        rewrite <- (has_value_sim _ _ _ ACQsim1) in qEQ3.
        rewrite <- hplusA in pEQ; eapply hplus_val_rD_weak in pEQ; ins; desf; eauto.
  }
Qed.

Lemma heap_loc_na_initialized2 :
  ∀ acts lab sb rf mo hmap V
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (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 (GET: hmap edge = Hdef h) l v (LA: has_value (h l) 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_union_rf sb rf c (hb_fst edge)) ∧
    (∀ d
      (HB1: d = hb_fst edge ∨ happens_before_union_rf sb rf d (hb_fst edge))
      (HB2: happens_before_union_rf sb rf 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; desf.
    assert (N: has_value (hf l) v).
    {
      destruct edge; ins.
      × exfalso.
        rewrite (qU0 _ EV), GET in ×.
        symmetry in qEQ; eapply hplus_ra_lD in qEQ.
          2: eby rewrite hupds.
        by desf; rewrite qEQ in ×.
      × red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        assert (EQ := hplus_def_inv_l _ _ rfsSIM); desf; rewrite EQ in ×.
        eapply hsum_valD_weak in EQ; eauto.
          2: by repeat (rewrite In_map; eexists,; eauto); rewrite rfsOK.
        symmetry in rfsSIM; eapply hplus_val_lD_weak in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        eapply hplus_val_rD_weak in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
      × red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        rewrite GET in ×.
        symmetry in rfsSIM; eapply hplus_val_rD_weak in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        eapply hplus_val_rD_weak in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
    }
    rewrite qEQ, hplusA in UPD; clear - UPD N.
    symmetry in UPD; eapply hplus_ra_lD in UPD.
      2: eby rewrite hupds.
    by desf; unfold initialize in UPD; desf; rewrite hupds in UPD.

    exfalso; destruct (hmap (hb_sb pre (hb_fst edge))); ins; desf.
    assert (N: has_value (hf l) v).
    {
      destruct edge; ins.
      × exfalso.
        rewrite (qU0 _ EV), GET in ×.
        symmetry in qEQ; eapply hplus_ra_lD in qEQ.
          2: eby rewrite hupds.
        by desf; rewrite qEQ in ×.
      × red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        assert (EQ := hplus_def_inv_l _ _ rfsSIM); desf; rewrite EQ in ×.
        eapply hsum_valD_weak in EQ; eauto.
          2: by repeat (rewrite In_map; eexists,; eauto); rewrite rfsOK.
        symmetry in rfsSIM; eapply hplus_val_lD_weak in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        eapply hplus_val_rD_weak in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
      × red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        rewrite GET in ×.
        symmetry in rfsSIM; eapply hplus_val_rD_weak in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        eapply hplus_val_rD_weak in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
    }
    rewrite qEQ, hplusA in UPD; clear - UPD N.
    symmetry in UPD; eapply hplus_ra_lD in UPD.
      2: eby rewrite hupds.
    by desf; unfold initialize in UPD; desf; rewrite hupds in UPD.
  }

  exploit go_back_one_val; 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 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.
    2: by eapply VALID; 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 sb rf (edge´ :: hb_sb pre d :: nil)).
  {
    clear IH.
    assert (∀ b, hb_snd edge = Some b → happens_before_union_rf sb rf (hb_fst edge) b)
      by (destruct edge; ins; desf; eauto with hb).
    assert (∀ b´, hb_snd edge´ = Some b´ → happens_before_union_rf sb rf (hb_fst edge´) b´)
      by (destruct edge´; ins; desf; eauto with hb).
    eapply independent_two; ins; eauto; intro; desf; 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); red in x4; desf; 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.
    2: by eapply VALID; 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 sb rf (edge´ :: hb_sb pre d :: nil)).
  {
    clear IH.
    assert (∀ b, hb_snd edge = Some b → happens_before_union_rf sb rf (hb_fst edge) b)
      by (destruct edge; ins; desf; eauto with hb).
    assert (∀ b´, hb_snd edge´ = Some b´ → happens_before_union_rf sb rf (hb_fst edge´) b´)
      by (destruct edge´; ins; desf; eauto with hb).
    eapply independent_two; ins; eauto; intro; desf; 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); red in x4; desf; ins; desf.
  by constructor; ins; intro; desf; ins; desf; eauto using t_trans, t_step.
}
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 :
  ∀ pre a b acts lab sb rf mo hmap V hf
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf 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_union_rf sb rf a b ∨ happens_before_union_rf sb rf 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 sb rf (hb_sb pre a :: hb_sb pre0 b :: nil)).
    by eapply independent_two; ins; eauto; 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.

  Grab Existential Variables. edone.
Qed.