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 step path ihc.

Set Implicit Arguments.

Lemma hist_closed_connect:
  ∀ lab sb rf hmap path a b V
    (CONNECT: hbpath_connects lab sb rf hmap path a b)
    (HC: hist_closed sb rf V) (IN: In b V),
  In a V.

Lemma nonatomics_strongly_connected_helper:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 hf2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2)
    l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l)),
  ∀ n, ∃ path1 path2,
    << CONNECT: hbpath_connects lab sb rf hmap (path1 ++ path2) b1 a2 ∨
                hbpath_connects lab sb rf hmap (path1 ++ path2) b2 a1 >> ∧
    << ALL: ∀ edge (IN: In edge path1) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone >> ∧
    << LEN: path2 = nil ∨ length path1 = n >>.

Lemma exists_path_with_location_throughout:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 hf2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2)
    l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l))
    (NORMAL1: HVlabeled (hf1 l) HLnormal) (NORMAL2: HVlabeled (hf2 l) HLnormal),
  ∃ path,
    << CONNECT: hbpath_connects lab sb rf hmap path b1 a2 ∨
                hbpath_connects lab sb rf hmap path b2 a1 >> ∧
    << ALL: ∀ edge (IN: In edge path) hf (MAP: hmap edge = Hdef hf), hf l ≠ HVnone >>.
Lemma nonatomics_strongly_connected:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 hf2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2)
    l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l))
    (NORMAL1: HVlabeled (hf1 l) HLnormal) (NORMAL2: HVlabeled (hf2 l) HLnormal),
  clos_refl_trans _ (happens_before lab sb rf mo) b1 a2 ∨
  clos_refl_trans _ (happens_before lab sb rf mo) b2 a1.

Theorem valid_implies_race_free :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V),
  race_free V lab sb rf mo.