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

Set Implicit Arguments.

Hint Unfold imm_happens_before.

Lemma hupds A h l (y : A) : hupd h l y l = y.

Lemma hist_closed_trans :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: clos_refl_trans _ sb a b) (IN: In b V), In a V.

Lemma hist_closedD :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: happens_before_union_rf sb rf a b) (IN: In b V), In a V.

Lemma happens_before_trans lab sb rf mo a b c :
  happens_before lab sb rf mo a b →
  happens_before lab sb rf mo b c →
  happens_before lab sb rf mo a c.

Lemma happens_before_union_rf_trans sb rf a b c :
  happens_before_union_rf sb rf a b →
  happens_before_union_rf sb rf b c →
  happens_before_union_rf sb rf a c.

Lemma happens_before_sb lab (sb : relation actid) rf mo a b :
  sb a b → happens_before lab sb rf mo a b.

Lemma happens_before_sw lab sb rf mo a b :
  synchronizes_with lab sb rf mo a b → happens_before lab sb rf mo a b.

Lemma happens_before_union_rf_sb (sb : relation actid) rf a b :
  sb a b → happens_before_union_rf sb rf a b.

Lemma happens_before_union_rf_rf (sb : relation actid) rf a b :
  rf b = Some a → happens_before_union_rf sb rf a b.

Lemma clos_trans_hbE :
  ∀ lab sb rf mo a b (HB: clos_trans actid (happens_before lab sb rf mo) a b),
    happens_before lab sb rf mo a b.

Lemma clos_trans_hbUrfE :
  ∀ sb rf a b (HB: clos_trans actid (happens_before_union_rf sb rf) a b),
    happens_before_union_rf sb rf a b.

Hint Immediate clos_trans_hbE : hb.
Hint Immediate clos_trans_hbUrfE : hb.

Hint Resolve
  happens_before_sb happens_before_sw happens_before_union_rf_sb happens_before_union_rf_rf
  happens_before_trans happens_before_union_rf_trans t_step hist_closedD : hb.

Lemma count_implies :
  ∀ (T: eqType) (f1 f2 : T → bool) (IMP : ∀ x, f1 x → f2 x) l,
  count f1 l ≤ count f2 l.

Lemma hasP' :
  ∀ (T : eqType) (a : pred T) (l : list_predType T),
    reflect (∃ x : T, In x l ∧ a x) (has a l).

Lemma clos_refl_transE X rel a b :
    clos_refl_trans X rel a b ↔ a = b ∨ clos_trans X rel a b.

Lemma clos_refl_trans_hbE :
  ∀ lab sb rf mo a b,
    clos_refl_trans actid (happens_before lab sb rf mo) a b →
    happens_before lab sb rf mo a b ∨ a = b.

Lemma clos_refl_trans_hbUrfE :
  ∀ sb rf a b,
    clos_refl_trans actid (happens_before_union_rf sb rf) a b →
    happens_before_union_rf sb rf a b ∨ a = b.

Lemma release_seq_implies_hbUrf lab sb rf mo a b:
  release_seq lab sb rf mo a b →
  clos_refl_trans _ (happens_before_union_rf sb rf) a b.

Lemma hb_implies_hbUrf lab sb rf mo a b:
  happens_before lab sb rf mo a b → happens_before_union_rf sb rf a b.

Lemma helper_perm_filter_post :
  ∀ e T,
    ∃ posts_sb posts_rf,
      Permutation T (filter (fun x : hbcase ⇒ (hb_fst x != e) || (x == hb_sink e)) T ++
                     map (hb_sb e) posts_sb ++
                     map (hb_rf e) posts_rf).

Lemma helper_filter_decide_sink: ∀ a T (ND: NoDup T),
      Permutation (filter (fun x : hbcase ⇒ (hb_fst x != a) || (x == hb_sink a)) T)
        (if excluded_middle_informative (In (hb_sink a) T)
          then hb_sink a :: (filter (fun x : hbcase ⇒ hb_fst x != a) T)
          else (filter (fun x : hbcase ⇒ hb_fst x != a) T)).

Lemma has_rf_succs acts lab sb rf mo (a: actid) :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ (rfs: list actid),
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf x = Some a >>.

Lemma has_rf_pres acts lab sb rf mo a :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ rfs,
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf a = Some x >>.

Definition wf_ltof A (f : A → nat) :
  well_founded (fun x y ⇒ f x < f y).

Lemma In_implies_perm A (x : A) l (IN: In x l) :
  ∃ l', Permutation l (x :: l').

Lemma Permutation_count A l l' (P : Permutation (A:=A) l l') f :
  count f l = count f l'.

Lemma count_eq_0: ∀ A f (lst: list A), count f lst = 0 ↔ ∀ x (IN: In x lst), ¬ f x.

Lemma Permutation_hmap_valids PS PSg :
  ∀ l l' (P : Permutation l l') lab sb rf hmap,
    @hmap_valids PS PSg lab sb rf hmap l →
    hmap_valids lab sb rf hmap l'.

Lemma Permutation_hmap_valids_strong PS PSg:
  ∀ l l' (P : Permutation l l') lab sb rf hmap,
    @hmap_valids_strong PS PSg lab sb rf hmap l →
    hmap_valids_strong lab sb rf hmap l'.

Lemma Permutation_hist_closed :
  ∀ l l' (P : Permutation l l') sb rf,
    hist_closed sb rf l →
    hist_closed sb rf l'.

Lemma Consistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : Consistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    Consistent acts' lab sb rf mo sc mt.

Lemma weakConsistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.

Lemma weakConsistent_Permutation :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: Permutation acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.

Lemma Permutation_flatten A l l' (P : Permutation l l') :
  Permutation (A:=A) (flatten l) (flatten l').

Lemma AcyclicStrong_implies_IrreflexiveHBuRF:
  ∀ lab sb rf mo, AcyclicStrong lab sb rf mo → IrreflexiveHBuRF sb rf.

Hint Resolve AcyclicStrong_implies_IrreflexiveHBuRF.

Definition is_pred A (rel : A → A → Prop) B a :=
  has (fun b ⇒ mydec (clos_refl_trans A rel a b)) B.

Definition depth_metric A (rel: A → A → Prop) V a :=
  count (is_pred rel a) V.

Lemma clos_transK T (rel: relation T) x y :
  clos_trans _ (clos_trans _ rel) x y →
  clos_trans _ rel x y.

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b → a = b ∨ clos_trans T rel a b.

Lemma depth_lt (rel : relation actid) V A B
  (HB : ∀ a, In a A → ¬ In a B →
        ∃ b, In b B ∧ rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: ∀ a, In a A → ¬ clos_trans _ rel b a)
  (SUB: ∀ b, In b B → In b V) :
  depth_metric rel V A < depth_metric rel V B.

Lemma edge_depth_ind lab sb rf V
  (ACYCLIC: IrreflexiveHBuRF sb rf)
  (HC: hist_closed sb rf V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge' (EV : edge_valid lab sb rf edge')
            (LT: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)),
      P edge')
    (EV : edge_valid lab sb rf edge)
    (IN : In (hb_fst edge) V),
    P edge) →
  ∀ edge (EV : edge_valid lab sb rf edge), In (hb_fst edge) V → P edge.

Fixpoint find_max A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f curr ≤ f x then find_max x f xs else find_max curr f xs
  end.

Lemma find_max_range :
  ∀ A (curr: A) f l,
    In (find_max curr f l) (curr :: l).

Lemma find_max_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f x ≤ f (find_max curr f l).

Lemma get_deepest :
  ∀ sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
         V (HC: hist_closed sb rf V)
         T (NNIL: T ≠ nil)
         (INCL: ∀ edge (IN: In edge T), In (hb_fst edge) V),
  ∃ edge,
    << IN: In edge T >> ∧
    << INe: In (hb_fst edge) V >> ∧
    << DEEP: ∀ edge' (IN': In edge' T)
                 (HB': happens_before_union_rf sb rf (hb_fst edge) (hb_fst edge')),
               False >>.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f x ≤ f curr then find_min x f xs else find_min curr f xs
  end.

Lemma find_min_range :
  ∀ A (curr: A) f l,
    In (find_min curr f l) (curr :: l).

Lemma find_min_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f (find_min curr f l) ≤ f x.

Lemma get_shallow :
  ∀ lab sb rf mo (ACYCLIC: AcyclicStrong lab sb rf mo)
         V (HC: hist_closed sb rf V)
         T (HC': hist_closed sb rf (V ++ T)) (NNIL: T ≠ nil),
  ∃ e,
    << IN: In e T >> ∧
    << HC: hist_closed sb rf (e :: V) >>.

Lemma no_normals_on_rf PS PSg :
  ∀ lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap ga a)
    hfr gr (MAP: hmap (hb_rf a b) = Hdef hfr gr) l (ALL: hfr l ≠ @HVnone PS PSg)
    (NORMAL: HVlabeled (hfr l) HLnormal),
  False.

Lemma no_normals_on_rf2 PS PSg :
  ∀ lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap ga b)
    hfr gr (MAP: hmap (hb_rf a b) = Hdef hfr gr) l (ALL: hfr l ≠ @HVnone PS PSg)
    (NORMAL: HVlabeled (hfr l) HLnormal),
  False.

Lemma triangles_never_on_rf PS PSg:
∀ edge lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (ALL: hf l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge ∨ is_sink edge.

Lemma triangles_never_on_rf2 PS PSg:
∀ edge lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap
    (VALID: ∃ b, hb_snd edge = Some b ∧ hmap_valid lab sb rf hmap ga b)
    hf g (MAP: hmap edge = Hdef hf g) l (ALL: hf l ≠ @HVnone PS PSg) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge.

Lemma FenceInDEF PS PSg:
  ∀ hmap pre post e hF hrel hrel' hacq hacq' gnew
    (DEF: hmap (hb_sb e post) ≠ @Hundef PS PSg)
    (pEQ: hmap (hb_sb pre e) = hF +!+ hrel +!+ hacq)
    (qEQ: hmap (hb_sb e post) = hF +!+ hrel' +!+ hacq' +!+ gheap _ _ gnew)
    (RELsim: Hsim hrel hrel')
    (ACQsim: Hsim hacq hacq'),
  ∃ hf g, hmap (hb_sb pre e) = Hdef hf g.

Lemma RMWinDEF PS PSg:
  ∀ hmap pre e post rfsIn rfsOut l hrel hrel' hacq hacq' ht hF P QQ v' sbg rfg
    (DEF: hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfsOut))
          +!+ hmap (hb_sink e) ≠ @Hundef PS PSg)
    (pEQ: hmap (hb_sb pre e) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                +!+ hrel +!+ hF )
    (qEQ: hmap (hb_sb e post) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                +!+ hacq' +!+ hF +!+ sbg)
    (rInEQ: hsum (map hmap (map (hb_rf^~ e) rfsIn)) = hacq +!+ ht)
    (rOutEQ: hsum (map hmap (map (hb_rf e) rfsOut)) +!+ hmap (hb_sink e) = hrel' +!+ ht +!+ rfg)
    (RELsim: Hsim hrel hrel') (ACQsim: Hsim hacq hacq'),
  ∃ hf g, hmap (hb_sb pre e) +!+ hsum (map hmap (map (hb_rf^~ e) rfsIn)) = Hdef hf g.

Ltac RMWin_def := exploit RMWinDEF; try eassumption; rewrite <- hdef_alt; intro DEFin; [].

Ltac RMWin_heap := exploit RMWinDEF; try eassumption; intro DEFin; desc; [].

Lemma valid_accessD PS PSg:
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Aa : is_access (lab a)),
  ∃ pre hf g,
    sb pre a ∧ hmap (hb_sb pre a) = Hdef hf g
    ∧ hf (loc (lab a)) ≠ @HVnone PS PSg ∧ HVlabeled (hf (loc (lab a))) HLnormal.

Lemma valid_na_accessD PS PSg :
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (NA : is_na (lab a)) pre
         (SB : sb pre a) hf g
         (HM : hmap (hb_sb pre a) = @Hdef PS PSg hf g),
  is_nonatomic (hf (loc (lab a))).

Lemma valid_readD PS PSg :
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Ra : is_read (lab a)),
  ∃ pre hf g,
    sb pre a ∧ hmap (hb_sb pre a) = @Hdef PS PSg hf g
    ∧ HVlabeledR (hf (loc (lab a))) HLnormal.

Lemma valid_writeD PS PSg :
  ∀ lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Wa : is_write (lab a)),
  ∃ pre hf g,
    sb pre a ∧ hmap (hb_sb pre a) = @Hdef PS PSg hf g ∧
    (is_lvalue (hf (loc (lab a))) ∨ is_atomic (hf (loc (lab a)))).

Lemma hmap_defined_in PS PSg:
  ∀ lab sb rf hmap mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge b (VALID: hmap_valid lab sb rf hmap ga b)
    (EV: edge_valid lab sb rf edge)
    (IN: hb_snd edge = Some b),
  ∃ hf g, hmap edge = @Hdef PS PSg hf g.

Lemma hmap_defined_out PS PSg:
  ∀ lab sb rf hmap ga mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge a (VALID: hmap_valid lab sb rf hmap ga a)
    (EV: edge_valid lab sb rf edge)
    (IN: hb_fst edge = a),
  ∃ hf g, hmap edge = @Hdef PS PSg hf g.