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

Set Implicit Arguments.

Lemma step_back_from_normal 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: HVlabeled (hf l) HLnormal) (ALL: hf l ≠ @HVnone PS PSg),
  << ALLOC: lab (hb_fst edge) = Aalloc l >> ∨
  ∃ edge' hf' g', << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
                       << EV': edge_valid lab sb rf edge' >> ∧
                       << MAP': hmap edge' = Hdef hf' g' >> ∧
                       << ALL': hf' l ≠ @HVnone PS PSg >> ∧
                       << SB: ¬ is_rf edge >> ∧
                      (<< SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnormal >> ∨
                       << SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∧
                                                 << ACQ: is_acquire_fence (lab (hb_fst edge)) >> ∧
                                                 << reallySB: is_sb edge >> ∨
                       << RF': is_rf edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∧
                                                 << ACQ: is_acquire_read (lab (hb_fst edge)) >>).

Lemma step_back_from_nabla 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: HVlabeled (hf l) HLnabla) (ALL: hf l ≠ @HVnone PS PSg),
  ∃ edge' hf' g',
    << CON: hb_snd edge' = Some (hb_fst edge) >> ∧ << EV': edge_valid lab sb rf edge' >> ∧
    << MAP': hmap edge' = Hdef hf' g' >> ∧ << ALL': hf' l ≠ @HVnone PS PSg >> ∧
   (<< SB: ¬ is_rf edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∨
    << SB: ¬ is_rf edge >> ∧ << RF': is_rf edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∨
    << RF: ¬ is_sb edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLtriangle >> ∨
    << RF: ¬ is_sb edge >> ∧ << SB': is_sb edge' >> ∧ << LAB': HVlabeled (hf' l) HLnormal >> ∧
                              << REL: is_release_write (lab (hb_fst edge)) >> ∨
    << RF: ¬ is_sb edge >> ∧ << RF': is_rf edge' >> ∧ << LAB': HVlabeled (hf' l) HLnabla >> ∧
                              << RMW: is_rmw (lab (hb_fst edge)) >>).

Lemma step_back_from_triangle 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: HVlabeled (hf l) HLtriangle) (ALL: hf l ≠ @HVnone PS PSg),
  ∃ edge' hf' g',
    << CON: hb_snd edge' = Some (hb_fst edge) >> ∧ << EV': edge_valid lab sb rf edge' >> ∧
    << MAP': hmap edge' = Hdef hf' g' >> ∧ << ALL': hf' l ≠ @HVnone PS PSg >> ∧
    << SB: ¬ is_rf edge >> ∧ << SB': is_sb edge' >> ∧
   (<< LAB': HVlabeled (hf' l) HLtriangle >> ∨
    << LAB': HVlabeled (hf' l) HLnormal >> ∧ << REL: is_release_fence (lab (hb_fst edge)) >>
                                           ∧ << reallySB: is_sb edge >>).

Lemma take_sync_step_back PS PSg:
  ∀ lab sb rf mo hmap ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf (fst edge)) (VALID: hmap_valid lab sb rf hmap ga (hb_fst (fst edge)))
    hf g (MAP: hmap (fst edge) = Hdef hf g) l (LAB: HVlabeled (hf l) (snd edge)) (ALL: hf l ≠ @HVnone PS PSg)
    (NALL: lab (hb_fst (fst edge)) ≠ Aalloc l),
  ∃ edge' hf' g', << VALID: edge_valid lab sb rf (fst edge') >> ∧
                       << MAP': hmap (fst edge') = Hdef hf' g' >> ∧
                       << ALL': hf' l ≠ @HVnone PS PSg >> ∧
                       << LAB': HVlabeled (hf' l) (snd edge') >> ∧
                       << SYNC: sync_step lab edge' edge >>.

Lemma extend_tracking_path_left PS PSg :
  ∀ lab sb rf mo hmap ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    path (NEMP: path ≠ nil) a b (CON: hbpath_connects lab sb rf path a b)
    (VALID: @hmap_valid PS PSg lab sb rf hmap ga a) l (TRACK: tracking_path hmap path l)
    (NALL: lab a ≠ Aalloc l),
  ∃ edge, << WFP: hbpath_wf lab sb rf (edge :: path) >> ∧
               << TRACK: tracking_path hmap (edge :: path) l >>.