Helper lemmas for initialized reads


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 ); 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 ); 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 ); 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.

This page has been generated by coqdoc