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

Set Implicit Arguments.

Lemma step_from_normal PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV: edge_valid lab sb rf edge1) b (B: hb_snd edge1 = Some b)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga b) hf1 g1 (MAP: hmap edge1 = Hdef hf1 g1)
    l (ALL: hf1 l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf1 l) HLnormal),
  is_sb edge1 ∧
  ∃ edge2 hf2 g2, hb_snd edge1 = Some (hb_fst edge2) ∧ edge_valid lab sb rf edge2 ∧
                       hmap edge2 = Hdef hf2 g2 ∧ hf2 l ≠ @HVnone PS PSg ∧
                       (HVlabeled (hf2 l) HLnormal ∧ ¬ is_rf edge2 ∨
                        HVlabeled (hf2 l) HLtriangle ∧ is_sb edge2 ∧ is_release_fence (lab (hb_fst edge2)) ∨
                        HVlabeled (hf2 l) HLnabla ∧ ¬ is_sb edge2 ∧ is_release_write (lab (hb_fst edge2))).

Lemma step_from_triangle PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV: edge_valid lab sb rf edge1) b (B: hb_snd edge1 = Some b)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga b) hf1 g1 (MAP: hmap edge1 = Hdef hf1 g1)
    l (ALL: hf1 l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf1 l) HLtriangle),
  is_sb edge1 ∧
  ∃ edge2 hf2 g2, hb_snd edge1 = Some (hb_fst edge2) ∧ edge_valid lab sb rf edge2 ∧
                    hmap edge2 = Hdef hf2 g2 ∧ hf2 l ≠ @HVnone PS PSg ∧
                    (HVlabeled (hf2 l) HLtriangle ∧ ¬ is_rf edge2 ∨
                     HVlabeled (hf2 l) HLnabla ∧ ¬ is_sb edge2 ∧ is_write (lab (hb_fst edge2)) ∨
                     HVlabeled (hf2 l) HLnabla ∧ is_sink edge2).

Lemma step_from_nabla PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV: edge_valid lab sb rf edge1) b (B: hb_snd edge1 = Some b)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga b) hf1 g1 (MAP: hmap edge1 = Hdef hf1 g1)
    l (ALL: hf1 l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf1 l) HLnabla),
  ∃ edge2 hf2 g2, hb_snd edge1 = Some (hb_fst edge2) ∧ edge_valid lab sb rf edge2 ∧
                       hmap edge2 = Hdef hf2 g2 ∧ hf2 l ≠ @HVnone PS PSg ∧
  (HVlabeled (hf2 l) HLnabla ∧ ¬ is_rf edge2 ∨
   is_rf edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ ¬ is_rf edge2 ∧ is_acquire_read (lab (hb_fst edge2)) ∨
   is_sb edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ is_sb edge2 ∧ is_acquire_fence (lab (hb_fst edge2)) ∨
   is_rf edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ ¬ is_sb edge2 ∧ is_rmw (lab (hb_fst edge2))).

Lemma take_sync_step 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)) b (B: hb_snd (fst edge) = Some b)
    (VALID: hmap_valid lab sb rf hmap ga b) hf g (MAP: hmap (fst edge) = Hdef hf g)
    l (LAB: HVlabeled (hf l) (snd edge)) (ALL: hf l ≠ @HVnone PS PSg),
  ∃ 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_right 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 b) l (TRACK: tracking_path hmap path l),
  ∃ edge, << WFP: hbpath_wf lab sb rf (path ++ edge :: nil) >> ∧
               << TRACK: tracking_path hmap (path ++ edge :: nil) l >>.