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

Set Implicit Arguments.

Lemma step_back_from_normalR:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeledR (hf l) HLnormal),
  << STORE: is_writeL (lab (hb_fst edge)) l >> ∨
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧ << SB: ¬ is_rf edge >> ∧
                   (<< SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnormal >> ∨
                    << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_fence (lab (hb_fst edge)) >> ∨
                    << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∧
                                              << ACQ: is_acquire_read (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e´); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    right.
    symmetry in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    rewrite D in ×.
    symmetry in D; eapply hsum_preserves_Rlabel in D; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply qOK.
    symmetry in qEQ; eapply hplus_preserves_Rlabel in qEQ; eauto; desfh.
    assert (pEQ´ := pEQ).
    symmetry in pEQ; eapply hsum_preserves_Rlabel_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    right.
    symmetry in qEQ; rewrite hplusC in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    symmetry in qEQ; eapply hplus_preserves_Rlabel in qEQ; eauto; desfh.
    symmetry in pEQ; eapply hsum_preserves_Rlabel_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    right.
    rewrite pEQ in qEQ; inv qEQ.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    right; revert TYP.
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × unfold hupd in qEQ0; desfh; desfh.
      symmetry in pEQ´; eapply hplus_preserves_Rlabel in pEQ´; rewrite ?hupds; try by eauto.
      desfh; eexists (hb_sb _ e), _; repeat split; ins; eauto.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      + red in TRAN; desfh.
        rewrite TRAN in ×.
        red in rfsSIM; desfh.
        specialize (rfsSIM1 l).
        rewrite HVsim_sym in rfsSIM1; eapply Rlabel_sim in rfsSIM1; eauto; desfh.
        specialize (TRAN3 l).
        exploit (Rlabel_is_consistent_with_exact_label (hf2 l)); eauto; intro; desfh.
        symmetry in TRAN; eapply hsum_preserves_Rlabel_inv in TRAN; eauto; desfh.
        repeat (rewrite In_map in *; desfh).
        eexists (hb_rf _ e), _; ins; repeat split; eauto.
          by apply rfsOK.
        repeat right; repeat split; desfh.
        - red in TYP; desfh; specialize (TYP0 l).
          by exploit Rlabel_is_consistent_with_exact_label; eauto.
        - desf.
      + symmetry in pEQ´; rewrite hplusC in pEQ´; eapply hplus_preserves_Rlabel in pEQ´; eauto; desfh.
        eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    right; clear TYP.
    assert (l0 = l) by (unfold hupd in LAB; desfh; desfh).
    symmetry in pEQ´; eapply hplus_preserves_Rlabel in pEQ´; rewrite ?hupds; simpls; desfh.
      2: by instantiate (1 := HLnormal); vauto.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    unfold hupd in *; desfh; desfh; eauto.
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    destruct (classic (l = l0)); eauto.
    right; clear TYP.
    eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    unfold initialize, hupd in UPD; desfh.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    rewrite TRAN in ×.
    assert (R := hplus_def_inv_l _ _ TRAN); desf.
    rewrite R in ×.
    symmetry in R; eapply hsum_preserves_Rlabel in R; eauto; desf.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply rfsOK.
    symmetry in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desf.
    specialize (TRAN3 l).
    by exploit Rlabel_is_consistent_with_exact_label; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desf.
    specialize (TRAN3 l).
    by exploit Rlabel_is_consistent_with_exact_label; eauto.
  }

  {
    rewrite hdef_alt in DEF; desfh.
    rewrite DEF in ×.
    right; eexists (hb_sb _ e), _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_Rlabel in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso; red in RELlabel´; desf.
      specialize (RELlabel´0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
    × red in ACQsim; desfh.
      specialize (ACQsim1 l).
      rewrite HVsim_sym in ACQsim1.
      eapply Rlabel_sim in ACQsim1; eauto; desfh.
      red in ACQlabel; desfh.
      specialize (ACQlabel0 l).
      exploit Rlabel_is_consistent_with_exact_label; eauto; ins; desfh.
      rewrite <- hplusA, hplusC in pEQ.
      eapply hplus_preserves_Rlabel in pEQ; try eassumption; intuition.
      right; left; intuition; desf; intuition.
      inv H; intuition.
  }
Qed.

Lemma step_back_from_nablaR:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeledR (hf l) HLnabla),
  (<< STORE: is_writeL (lab (hb_fst edge)) l >> ∧
   << REL: is_release_write (lab (hb_fst edge)) >> ∧
   << RF: ¬ is_sb edge >>) ∨
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧
                   (<< SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∨
                    << SB: ¬ is_rf edge >> ∧ << RF´: is_rf edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnabla >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLtriangle >> ∨
                    << RF: ¬ is_sb edge >> ∧ << SB´: is_sb edge´ >> ∧ << LAB´: HVlabeledR (hf´ l) HLnormal >> ∧
                                              << REL: is_release_write (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e´); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    right.
    symmetry in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    rewrite D in ×.
    symmetry in D; eapply hsum_preserves_Rlabel in D; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply qOK.
    symmetry in qEQ; eapply hplus_preserves_Rlabel in qEQ; eauto; desfh.
    assert (pEQ´ := pEQ).
    symmetry in pEQ; eapply hsum_preserves_Rlabel_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    right.
    symmetry in qEQ; rewrite hplusC in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    symmetry in qEQ; eapply hplus_preserves_Rlabel in qEQ; eauto; desfh.
    symmetry in pEQ; eapply hsum_preserves_Rlabel_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    right; eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
      ins; unfold is_nabla in LAB; desf.
  }

  {
    right.
    rewrite pEQ in qEQ; inv qEQ.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    right; revert TYP.
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso.
      unfold hupd in qEQ0; desf; ins; desfh.
      unfold is_nabla in qEQ0; desf.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      + red in TRAN; desfh.
        rewrite TRAN in ×.
        red in rfsSIM; desfh.
        specialize (rfsSIM1 l).
        rewrite HVsim_sym in rfsSIM1; eapply Rlabel_sim in rfsSIM1; eauto; desfh.
        specialize (TRAN3 l).
        exploit (Rlabel_is_consistent_with_exact_label (hf2 l)); eauto; intro; desfh.
        symmetry in TRAN; eapply hsum_preserves_Rlabel_inv in TRAN; eauto; desfh.
        repeat (rewrite In_map in *; desfh).
        eexists (hb_rf _ e), _; ins; repeat split; eauto 6.
        by apply rfsOK.
      + symmetry in pEQ´; rewrite hplusC in pEQ´; eapply hplus_preserves_Rlabel in pEQ´; eauto; desfh.
        eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    exfalso.
    unfold hupd in *; desf; desf; eauto; ins; unfold is_nabla in LAB; desf.
  }

  {
    right.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    unfold hupd in LAB; desfh; desfh; eauto.
  }

  {
    right; clear TYP.
    eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    left; intuition.
    by eapply initialize_not_normalR; eauto.
  }

  {
    red in TRAN; desfh.
    rewrite TRAN in ×.
    assert (R := hplus_def_inv_l _ _ TRAN); desfh.
    rewrite R in ×.
    symmetry in R; eapply hsum_preserves_Rlabel in R; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply rfsOK.
    symmetry in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desfh.
    red in rfsSIM; desfh.
    specialize (rfsSIM1 l).
    eapply Rlabel_sim in rfsSIM1; eauto; desfh.
    assert (UPDcopy := UPD).
    rewrite hplusC in UPD; eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    ins; desfh.
    × right; eexists (hb_sb _ e), _; do 3 (split; eauto); ins.
      red in TYP; desfh.
      specialize (TYP0 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desfh.
      right; right; left; intuition.
      by eapply initialize_not_normalR; eauto.
    × red in TYP1; desfh.
      specialize (TYP2 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desfh.
      destruct (classic (l0 = l)); desfh.
      + left; desf; intuition.
      + right; eexists (hb_sb _ e), _; do 3 (split; eauto); ins.
        unfold initialize, hupd in UPD; ins; desfh.
        repeat right; desf; intuition.
  }

  {
    red in TRAN; desfh.
    rewrite TRAN in ×.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desfh.
    red in rfsSIM; desfh.
    specialize (rfsSIM1 l).
    eapply Rlabel_sim in rfsSIM1; eauto; desfh.
    assert (UPDcopy := UPD).
    rewrite hplusC in UPD; eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    ins; desfh.
    × right; eexists (hb_sb _ e), _; do 3 (split; eauto); ins.
      red in TYP; desfh.
      specialize (TYP0 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desfh.
      right; right; left; intuition.
      by eapply initialize_not_normalR; eauto.
    × red in TYP1; desfh.
      specialize (TYP2 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desfh.
      destruct (classic (l = l0)).
      + left; desf; intuition.
      + right; eexists (hb_sb _ e), _; do 3 (split; eauto); ins.
        unfold initialize, hupd in UPD; ins; desfh.
        repeat right; desf; intuition.
  }

  {
    rewrite hdef_alt in DEF; desfh.
    rewrite DEF in ×.
    right; eexists (hb_sb _ e), _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_Rlabel in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso; red in RELlabel´; desf.
      specialize (RELlabel´0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
    × exfalso; red in ACQlabel´; desf.
      specialize (ACQlabel´0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
  }
Qed.

Lemma step_back_from_triangleR:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (LAB: HVlabeledR (hf l) HLtriangle),
  ∃ edge´ hf´, << CON: hb_snd edge´ = Some (hb_fst edge) >> ∧ << EV´: edge_valid lab sb rf edge´ >> ∧
                    << MAP´: hmap edge´ = Hdef hf´ >> ∧
                    << SB: ¬ is_rf edge >> ∧ << SB´: is_sb edge´ >> ∧
                   (<< LAB´: HVlabeledR (hf´ l) HLtriangle >> ∨
                    << LAB´: HVlabeledR (hf´ l) HLnormal >> ∧ << REL: is_release_fence (lab (hb_fst edge)) >>).
Proof.
  ins; unnw.
  unfold hmap_valid, unique in VALID.
  desfh; desc; try (destruct DISJ; desc); destruct edge; ins; try revert TYP; desfh;
    try (by red in EV; rewrite Heq in EV);
    try (by specialize (CONS_RF e´); desfh; desfh; rewrite Heq in *; desfh);
    rewrite ?(qU0 _ EV), ?MAP in *; desfh;
    try (by inv sEQ);
    try (by rewrite rEQ in MAP; inv MAP).

  {
    symmetry in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    rewrite D in ×.
    symmetry in D; eapply hsum_preserves_Rlabel in D; eauto; desfh.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply qOK.
    symmetry in qEQ; eapply hplus_preserves_Rlabel in qEQ; eauto; desfh.
    assert (pEQ´ := pEQ).
    symmetry in pEQ; eapply hsum_preserves_Rlabel_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    symmetry in qEQ; rewrite hplusC in qEQ; assert (D := (hplus_def_inv_l _ _ qEQ)); desfh.
    symmetry in qEQ; eapply hplus_preserves_Rlabel in qEQ; eauto; desfh.
    symmetry in pEQ; eapply hsum_preserves_Rlabel_inv in pEQ; eauto; desf.
    repeat (rewrite In_map in *; desf).
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    by apply pOK.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto; unfold hupd in *; desf; desf; eauto;
      ins; unfold is_triangle in LAB; desf.
  }

  {
    rewrite pEQ in qEQ; inv qEQ.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × exfalso.
      unfold hupd in qEQ0; desf; ins; desfh.
      unfold is_triangle in qEQ0; desf.
    × eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      + ins; exfalso.
        assert (L: ∃ lbl, HlabeledExact (Hdef hf´0) lbl ∧ lbl ≠ HLtriangle) by (by desf; eexists,; eauto).
        clear TYP; desf.
        red in L; desf.
        specialize (L1 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desf.
      + symmetry in pEQ´; rewrite hplusC in pEQ´; eapply hplus_preserves_Rlabel in pEQ´; eauto; desfh.
        eexists (hb_sb _ e), _; repeat split; ins; eauto.
  }

  {
    exfalso.
    unfold hupd in *; desf; desf; eauto; ins; unfold is_triangle in LAB; desf.
  }

  {
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    unfold hupd in LAB; desf; desf; eauto.
  }

  {
    eapply hplus_preserves_Rlabel in UPD; eauto; desfh.
    eexists (hb_sb _ e), _; repeat split; ins; eauto.
    clear TYP; left; intuition.
    by eapply initialize_not_normalR; eauto.
  }

  {
    exfalso.
    red in TRAN; desfh.
    assert (R := hplus_def_inv_l _ _ TRAN); desf.
    rewrite R in ×.
    symmetry in R; eapply hsum_preserves_Rlabel in R; eauto; desf.
      2: by rewrite <- MAP; repeat (rewrite In_map; eexists,; eauto); apply rfsOK.
    symmetry in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desf.
    specialize (TRAN3 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desf.
  }

  {
    exfalso.
    red in TRAN; desfh.
    symmetry in TRAN; rewrite hplusC in TRAN; eapply hplus_preserves_Rlabel in TRAN; eauto; desf.
    specialize (TRAN3 l); exploit Rlabel_is_consistent_with_exact_label; eauto; intro; desf.
  }

  {
    rewrite hdef_alt in DEF; desfh.
    rewrite DEF in ×.
    eexists (hb_sb _ e), _; do 3 (split; eauto).
    symmetry in qEQ; eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
      by eapply hplus_preserves_Rlabel in pEQ; eauto; desfh; ins; intuition.
    eapply hplus_preserves_Rlabel_inv in qEQ; eauto; desfh.
    × red in RELsim; desfh.
      specialize (RELsim1 l).
      apply HVsim_sym in RELsim1; eapply Rlabel_sim in qEQ1; eauto; desfh.
      red in RELlabel; desfh.
      specialize (RELlabel0 l); exploit Rlabel_is_consistent_with_exact_label; eauto; desfh.
      rewrite hplusAC in pEQ; eapply hplus_preserves_Rlabel in pEQ; eauto; ins; desfh; intuition.
      right; split; try done; desf; intuition.
      inv H; intuition.
    × exfalso; red in ACQlabel´; desf.
      specialize (ACQlabel´0 l).
      by exploit Rlabel_is_consistent_with_exact_label; eauto.
 }
Qed.