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

This page has been generated by coqdoc