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

Set Implicit Arguments.

Lemma location_does_not_vanish:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge) b (SND: hb_snd edge = Some b)
    hmap (VALID: hmap_valid lab sb rf hmap b) hf (MAP: hmap edge = Hdef hf)
    l (ALL: hf l ≠ HVnone),
  ∃ edge´, << EV´: edge_valid lab sb rf edge´ >> ∧ << CON: b = hb_fst edge´ >> ∧
                ∃ hf´, << MAP´: hmap edge´ = Hdef hf´ >> ∧ << ALL´: hf´ l ≠ HVnone >>.
Lemma na_propagates_forward:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV1: edge_valid lab sb rf edge1)
    edge2 (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA: is_nonatomic (hf1 l)) (ALL: hf2 l ≠ HVnone),
  is_nonatomic (hf2 l).
Lemma na_propagates_back:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV1: edge_valid lab sb rf edge1)
    edge2 (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (ALL: hf1 l ≠ HVnone) (NA: is_nonatomic (hf2 l)),
  is_nonatomic (hf1 l).
Lemma no_triangle_after_nabla:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 (EV1: edge_valid lab sb rf edge1) edge2 (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (NA2: is_nonatomic (hf2 l)) (LAB1: HVlabeled (hf1 l) HLnabla),
  ¬ HVlabeled (hf2 l) HLtriangle.
Lemma step_from_normal:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (LAB: HVlabeled (hf1 l) HLnormal) (ALL: hf2 l ≠ HVnone),
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnormal ∧ is_sb edge2) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLtriangle ∧ is_sb edge2 ∧ is_release_fence (lab (hb_fst edge2))) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ is_rf edge2 ∧ is_release_write (lab (hb_fst edge2))) ∨
  is_sink edge2.
Lemma step_from_nabla:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (LAB: HVlabeled (hf1 l) HLnabla) (ALL: hf2 l ≠ HVnone),
  (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))).
Lemma step_from_triangle:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    (CON: hb_snd edge1 = Some (hb_fst edge2))
    hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge2))
    hf1 (MAP1: hmap edge1 = Hdef hf1) hf2 (MAP2: hmap edge2 = Hdef hf2)
    l (NA1: is_nonatomic (hf1 l)) (LAB: HVlabeled (hf1 l) HLtriangle) (ALL: hf2 l ≠ HVnone),
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLtriangle ∧ ¬ is_rf edge2) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ is_rf edge2 ∧ is_write (lab (hb_fst edge2))) ∨
  (is_sb edge1 ∧ HVlabeled (hf2 l) HLnabla ∧ is_sink edge2).