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

Set Implicit Arguments.


Lemma step_back_from_normalR PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeledR (hf l) HLnormal),
  << STORE: is_writeL (lab (hb_fst edge)) l >> ∨
  ∃ edge' hf' g', << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
                       << EV': edge_valid lab sb rf edge' >> ∧
                       << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
                       << 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_triangleR PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (LAB: HVlabeledR (hf l) HLtriangle),
  ∃ edge' hf' g',
    << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
    << EV': edge_valid lab sb rf edge' >> ∧
    << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
    << 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)) >>).

Lemma step_back_from_nablaR PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) 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' g',
    << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
    << EV': edge_valid lab sb rf edge' >> ∧
    << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
   (<< 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)) >> ∨
    << RF: ¬ is_sb edge >> ∧ << RF': is_rf edge' >> ∧ << LAB': HVlabeledR (hf' l) HLnabla >> ∧
                              << RMW: is_rmw (lab (hb_fst edge)) >>).