Auxiliary lemmas for the soundness proof


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.

Various helper lemmas


Hint Unfold imm_happens_before.

Lemma hupds A h l (y : A) : hupd h l y l = y.
Proof. unfold hupd; desf; congruence. Qed.

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.
Proof. induction 2; ins; eauto using hc_edge. Qed.

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.
Proof. induction 2; ins; unfold imm_happens_before in *; desf; eauto using hc_edge. Qed.

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.
Proof. apply t_trans. Qed.

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.
Proof. apply t_trans. Qed.

Lemma happens_before_sb lab (sb : relation actid) rf mo a b :
  sb a b happens_before lab sb rf mo a b.
Proof. ins; apply t_step; auto. Qed.

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.
Proof. ins; apply t_step; auto. Qed.

Lemma happens_before_union_rf_sb (sb : relation actid) rf a b :
  sb a b happens_before_union_rf sb rf a b.
Proof. ins; apply t_step; vauto. Qed.

Lemma happens_before_union_rf_rf (sb : relation actid) rf a b :
  rf b = Some a happens_before_union_rf sb rf a b.
Proof. ins; apply t_step; vauto. Qed.

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.
Proof.
  induction 1; vauto.
Qed.

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.
Proof.
  induction 1; vauto.
Qed.

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.
Proof.
  induction l; ins; desf; eauto.
  by rewrite IMP in Heq0.
Qed.

Lemma hasP' :
   (T : eqType) (a : pred T) (l : list_predType T),
    reflect ( x : T, In x l a x) (has a l).
Proof.
  ins; case hasP; intro H; constructor; try red; intros; destruct H; desf.
    by apply/inP in H; eauto.
  by x; try apply/inP; eauto.
Qed.

Lemma clos_refl_transE X rel a b :
    clos_refl_trans X rel a b a = b clos_trans X rel a b.
Proof.
  split; ins; desf; try induction H; desf; eauto using clos_refl_trans, clos_trans.
Qed.

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.
Proof.
  unfold happens_before; induction 1; desf; vauto.
Qed.

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.
Proof.
  induction 1; desf; vauto.
Qed.

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.
Proof.
  induction 1; vauto.
    by apply rt_step; vauto.
  by eapply rt_trans, rt_step; vauto.
Qed.

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.
Proof.
  ins; induction H; eauto with hb.
  red in H; desf; vauto.
  red in H; desf.
  × eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H1; desf; vauto.
    eapply happens_before_union_rf_trans; vauto.
  × apply clos_refl_transE in H1; eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H2; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
  × apply clos_refl_transE in H1; eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H2; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
  × apply clos_refl_transE in H1; apply clos_refl_transE in H2;
    eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H3; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
Qed.

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).
Proof.
  induction T as [|hb T']; ins; desc.
     by nil, nil.
  case eqP; ins; subst; [|eby do 2 eexists; eapply Permutation_cons].
  destruct hb; ins.
  × (e' :: posts_sb), posts_rf; simpl.
    by apply Permutation_cons_app.
  × posts_sb, (e' :: posts_rf); simpl.
    by rewrite <- appA in *; apply Permutation_cons_app.
  × desf; [ posts_sb, posts_rf | done].
    by rewrite <- app_comm_cons; apply Permutation_cons.
Qed.

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 : hbcasehb_fst x != a) T)
          else (filter (fun x : hbcasehb_fst x != a) T)).
    Proof.
      ins; induction T as [ | edge T']; simpls; desf; apply nodup_cons in ND; desf;
      solve [
        eapply (Permutation_cons eq_refl) in IHT'; ins; eapply perm_trans; eauto; apply perm_swap
        |
        apply perm_skip; apply IHT'; done
        |
        destruct n; right; done
        |
        destruct n; left; done
        |
        destruct Heq; left; done
        |
        destruct Heq; right; done
        |
        apply IHT'; done
      ].
    Qed.

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 >>.
Proof.
   (undup (filter (fun xmydec (rf x = Some a)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=Vbase.nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H, H0; desf.
  by generalize (CLOlab x), (H0 x); rewrite H1 in *; destruct (lab x); ins; desf; vauto; eapply H.
Qed.

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 >>.
Proof.
   (undup (filter (fun xmydec (rf a = Some x)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=Vbase.nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H, H0; desf.
  by generalize (CLOlab x), (H0 a); rewrite H1 in *; destruct (lab x); ins; desf; vauto; eapply H.
Qed.

Definition wf_ltof A (f : A nat) :
  well_founded (fun x yf x < f y).
Proof.
  by apply Wf_nat.well_founded_lt_compat with f; intros x y; case ltP.
Qed.

A few lemmas about Permutations

Lemma In_implies_perm A (x : A) l (IN: In x l) :
   l', Permutation l (x :: l').
Proof.
  induction l; ins; desf; eauto.
  destruct IHl; eauto using Permutation.
Qed.

Lemma Permutation_count A l l' (P : Permutation (A:=A) l l') f :
  count f l = count f l'.
Proof.
  induction P; ins; desf; congruence.
Qed.

Lemma count_eq_0: A f (lst: list A), count f lst = 0 x (IN: In x lst), ¬ f x.
Proof.
  split; ins.
  × intro.
    apply In_implies_perm in IN; desf.
    apply Permutation_count with (f := f) in IN.
    rewrite IN in H.
    rewrite <- (app_nil_l l') , <- app_cons, count_app in H.
    by simpls; desf.
  × induction lst as [ | h tl]; simpls; desf.
    by exfalso; exploit (H h); vauto.
    by apply IHtl; ins; apply H; vauto.
Qed.

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'.
Proof.
  unfold hmap_valids; ins; desf.
  eexists; split.
  eby eexists.
  by red; ins; apply VLD, Permutation_in with (l := l'); [eapply Permutation_sym | ].
Qed.

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'.
Proof.
  red; ins; split; red; red in H; desf; ins.
    eby eapply Permutation_hmap_valids.
  apply (RESTR e); try done.
  eby intro; destruct NIN; eapply Permutation_in.
  desf; [left | right; split]; try done.
  intro SB; destruct H0.
  eby unfold is_sb_out in *; split; desf; eapply Permutation_in.
Qed.

Lemma Permutation_hist_closed :
   l l' (P : Permutation l l') sb rf,
    hist_closed sb rf l
    hist_closed sb rf l'.
Proof.
  red; ins; eapply H in HB.
    by apply (Permutation_in _ P) in HB.
  by eapply Permutation_in, IN; eauto using Permutation_sym.
Qed.

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.
Proof.
  unfold Consistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

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.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

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.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins.
    by apply (Permutation_in _ EQ), CLOlab.
  by apply CLOsb in H; desf; split; apply (Permutation_in _ EQ).
Qed.

Lemma Permutation_flatten A l l' (P : Permutation l l') :
  Permutation (A:=A) (flatten l) (flatten l').
Proof.
  induction P; ins; rewrite ?flatten_cons, <- ?appA;
  eauto using Permutation, Permutation_app, Permutation_app_comm.
Qed.

Lemma AcyclicStrong_implies_IrreflexiveHBuRF:
   lab sb rf mo, AcyclicStrong lab sb rf mo IrreflexiveHBuRF sb rf.
Proof.
  ins.
  do 2 red; ins.
  eapply H; instantiate (1 := x).
  red in H0.
  revert H0; generalize x at 1 3; intros y H0.
  induction H0; eauto using clos_trans.
  destruct H0; eauto using t_step with hb.
Qed.

Hint Resolve AcyclicStrong_implies_IrreflexiveHBuRF.

Depth metric


Definition is_pred A (rel : A A Prop) B a :=
  has (fun bmydec (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.
Proof. induction 1; eauto using clos_trans. Qed.

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b a = b clos_trans T rel a b.
Proof. induction 1; desf; eauto using clos_trans. Qed.

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.
Proof.
  unfold depth_metric; ins.
  assert (IMP: x, is_pred rel A x is_pred rel B x).
    clear -HB; unfold is_pred, mydec; ins; desf.
    apply/@hasP'; apply/@hasP' in H; destruct H; desf.
    destruct (inP x0 B); [by x0; ins; desf|].
    eapply HB in H; desf; eexists _; split; try edone; desf.
    by exfalso; eauto using rt_trans, rt_step.
  assert (P1: is_pred rel B b).
    unfold is_pred, mydec; desf.
    eapply In_split in IN; desf.
    rewrite has_app; ins; desf; clarsimp.
    by destruct n; vauto.
  assert (P2: is_pred rel A b = false).
    clear -NHB NIN; apply/hasP'; unfold mydec; intro; desf; eauto.
    by apply clos_refl_transD in c; unfold not in *; desf; eauto.
  assert (IN' : In b V) by eauto.
  eapply In_split in IN'; desf; rewrite !count_app; ins.
  ins; rewrite P1, P2, addnS, ltnS.
  eauto using len_add, count_implies.
Qed.

A useful induction principle for happens-before graphs.

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.
Proof.
  intros until edge.
  generalize (S (depth_metric (happens_before_union_rf sb rf) V (hb_fst edge :: nil))),
             (ltnSn (depth_metric (happens_before_union_rf sb rf) V (hb_fst edge :: nil))).
  intro n'.
  revert edge; induction n'; ins.
  eapply H; ins; eapply IHn'; ins; eauto.
  2: by clear -HC LT H1; induction LT; unfold imm_happens_before in *; desf;
        eauto with hb.
  eapply ltn_len_trans, H0.
  eapply depth_lt; ins; desf; eauto; instantiate; rewrite addn0 in *;
    intro; desf; [rewrite H2 in *|]; eauto using t_step, t_trans, clos_trans_hbUrfE.
Qed.

Fixpoint find_max A (curr : A) f l :=
  match l with
    | nilcurr
    | 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).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_max_greatest :
   A (x curr: A) f l (IN: In x (curr :: l)),
    f x f (find_max curr f l).
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

Given a non-empty set of edges, T, there is always an edge whose source node does not happen before any of the sources of the other edges.

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 >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (happens_before_union_rf sb rf) V (hb_fst x :: nil)).

  assert (IN:= find_max_range h f T).
  eexists _; split; unfold NW; repeat split; eauto; ins.
  assert (D := find_max_greatest f IN'); ins.
  specialize (INCL _ IN'); clear IN IN'; subst f.
  erewrite lenE, depth_lt in D; ins; desf; try intro; desf.
    by (hb_fst edge'); split; vauto.
    by left; reflexivity.
    by rewrite H in *; eauto using t_step.
    by eauto using t_step, t_trans, clos_trans_hbUrfE.
Qed.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nilcurr
    | 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).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_min_greatest :
   A (x curr: A) f l (IN: In x (curr :: l)),
    f (find_min curr f l) f x.
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

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) >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (hc_edge sb rf) (V ++ a :: T) (x :: nil)).

  assert (IN:= find_min_range a f T).

  eexists; split; unfold NW; repeat split; eauto; ins.
  red; ins; destruct IN0; eauto; subst.
  generalize HB; eapply HC' in HB; eauto.
  2: by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
  rewrite In_app in HB; destruct HB as [|H]; vauto; intro.
  eapply find_min_greatest with (f:=f) in H.
  exfalso; clear IN.
  rewrite lenE in H; apply/negP in H; destruct H.
  eapply depth_lt; eauto using In_eq; ins; desf.
    by destruct HB; eauto using hc_edge with hb .
    by intro; desf; destruct HB; desf; eauto 8 with hb.
    intro H.
    assert (X: clos_trans actid (hc_edge sb rf) a0 a0) by eauto using clos_trans.
    apply (ACYCLIC a0); revert X; clear;
    generalize a0 at 1 3; induction 1; eauto using clos_trans;
    by destruct H; desf; auto with hb.
  assert (IN:= find_min_range a f T).
  by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
Qed.

Some lemmas about validly annotated nodes

RF-edges carry only HLnabla labels

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.
Proof.
  ins; red in VALID; desf; try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      red in TRAN; desf.
      generalize (hplus_def_inv _ _ TRAN); intro D; desf.
      rewrite D, D0 in ×.
      symmetry in D; eapply hsum_preserves_label in D; desf; eauto.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      symmetry in TRAN; eapply hplus_preserves_label in TRAN; desf; eauto.
      clear - TRAN4 TRAN TRAN3.
      specialize (TRAN3 l); destruct (hf0 l); desf; red in TRAN3; desf; ins; desf; red in TRAN4; desf.
    }
  }

  {
    desf; ins; desf.
    exploit (@exact_label_hplus_dist_inv _ _ (hrel' +!+ ht) rfg); try eassumption.
      eby rewrite hplusA, <- rOutEQ; eapply hplus_not_undef_r.
      by apply hplus_eq_gheap in ghostEQ; desf; vauto.
    rewrite hplusA, <- rOutEQ; intro L.
    apply exact_label_hplus_dist in L; desf.
    apply exact_label_hsum_dist with (h := Hdef hfr gr) in L.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOutOK.
    rewrite <- label_exact_hdef in L.
    specialize (L l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

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.
Proof.
  ins; red in VALID; desf; try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      apply exact_label_hsum_dist with (h := Hdef hfr gr) in TRAN.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      red in TRAN; desf.
      clear - TRAN3 ALL NORMAL.
      specialize (TRAN3 l); destruct (hf0 l); ins; try congruence;
        by desf; desf; red in NORMAL; desf.
    }
  }

  {
    desf; ins; desf.
    rewrite <- rInEQ in TRANin.
    apply exact_label_hsum_dist with (h := Hdef hfr gr) in TRANin.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsInOK.
    rewrite <- label_exact_hdef in TRANin.
    specialize (TRANin l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

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.
Proof.
  ins; apply NNPP; intro.
  apply not_or_and in H.
  destruct edge; ins; desf.
  ins; red in VALID; desf; try (by specialize (CONS_RF e'); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      red in TRAN; desf.
      generalize (hplus_def_inv _ _ TRAN); intro D; desf.
      rewrite D, D0 in ×.
      symmetry in D; eapply hsum_preserves_label in D; desf; eauto.
        2: by do 2 (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      symmetry in TRAN; eapply hplus_preserves_label in TRAN; desf; eauto.
      clear - TRAN4 TRAN TRAN3.
      specialize (TRAN3 l); destruct (hf1 l); desf; red in TRAN3; desf; ins; desf; red in TRAN4; desf.
    }
  }
  
  {
    desf; ins; desf.
    exploit (@exact_label_hplus_dist_inv _ _ (hrel' +!+ ht) rfg); try eassumption.
      eby rewrite hplusA, <- rOutEQ; eapply hplus_not_undef_r.
      by apply hplus_eq_gheap in ghostEQ; desf; vauto.
    rewrite hplusA, <- rOutEQ; intro L.
    apply exact_label_hplus_dist in L; desf.
    apply exact_label_hsum_dist with (h := Hdef hf g) in L.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOutOK.
    rewrite <- label_exact_hdef in L.
    specialize (L l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

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.
Proof.
  ins; desf.
  apply NNPP; intro RF.
  destruct edge; ins; desf.
  ins; red in VALID0; desf; try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
    {
      desf; rewrite rEQ in MAP; inv MAP.
    }
    {
      desc; clear TYP; ins; desf.
      apply exact_label_hsum_dist with (h := Hdef hf g) in TRAN.
        2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      rewrite <- label_exact_hdef in TRAN.
      specialize (TRAN l).
      exploit label_is_consistent_with_exact_label; eauto; ins.
    }
  }
  
  {
    desf; ins; desf.
    rewrite <- rInEQ in TRANin.
    apply exact_label_hsum_dist with (h := Hdef hf g) in TRANin.
      2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsInOK.
    rewrite <- label_exact_hdef in TRANin.
    specialize (TRANin l).
    exploit label_is_consistent_with_exact_label; eauto; ins.
  }
Qed.

The heap on the incoming edge of a fence node is defined.

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.
Proof.
  ins; rewrite <- hdef_alt; rewrite pEQ, qEQ in ×.
  rewrite hplusAC; eapply hplus_sim_def.
    eby apply Hsim_sym.
  rewrite <- hplusA, hplusC; eapply hplus_sim_def.
    eby apply Hsim_sym.
  rewrite hplusAC, <- hplusA, hplusC, <- hplusA.
  by intro U; rewrite <- !hplusA, U, hplus_undef_l in DEF.
Qed.

Heaps on the incoming edges of an RMW node are compatible.

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.
Proof.
  ins; rewrite <- hdef_alt.
  rewrite qEQ, rOutEQ, !hplusA, !(hplusAC sbg), (hplusC _ rfg), !(hplusAC rfg) in DEF.
  do 2 apply hplus_not_undef_r in DEF.
  rewrite pEQ, rInEQ.
  rewrite hplusC in DEF.
  rewrite !hplusA, hplusC.
  eapply hplus_sim_def; eauto.
  rewrite !(hplusAC hacq), (hplusAC _ hrel).
  apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in *).
    by apply Hsim_sym.
  apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in *).
    by apply Hsim_refl; intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in ×.
  apply hplus_sim; try (by intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in *).
    by apply Hsim_sym.
  by apply Hsim_refl; intro U; rewrite U, ?hplus_undef_r, ?hplus_undef_l in ×.
Qed.

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

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

Every validly annotated memory access contains the accessed location in the domain of the heap of its incoming sb-edge.

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.
Proof.
  ins.
  red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    red in IV; desf; desf.
    by eexists _, _, _; repeat split; eauto; ins; instantiate; rewrite Heq0.
  }

  {
    symmetry in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; eauto; rewrite ? hupds; ins.
      eexists _, _, _; repeat split; eauto; ins.
      by intro N; rewrite N in ×.
      eby apply Rlabel_implies_label.
    vauto.
  }

  {
    eexists _, _, _; repeat split; eauto; ins.
    by intro N; rewrite N in ×.
  }

  {
    symmetry in UPD; eapply hplus_ra_lD in UPD; desf.
      3: eby rewrite hupds.
    × apply initialize_eq_raD in UPD; desf.
      eexists _, _, _; repeat split; eauto; ins; try congruence.
      rewrite UPD; ins; desf; vauto.
    × apply initialize_eq_raD in UPD; desf.
      eexists _, _, _; repeat split; eauto; ins; try congruence.
      rewrite UPD; ins; desf; unfold is_normal; tauto.
  }

  {
    RMWin_def.
    apply hplus_not_undef_l, hdef_alt in DEFin; ins; desf.
    rewrite DEFin in ×.
    repeat eexists; eauto.
    by eapply hplus_preserves_alloc_l in pEQ; rewrite ?hupds.
    by eapply hplus_preserves_label in pEQ; rewrite ?hupds; ins; desf; vauto.
  }
Qed.

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))).
Proof.
  unfold hmap_valid, unique; ins; desf; desf; ins; apply pU0 in SB; desf;
  rewrite pEQ in HM; desf; eauto.
Qed.

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.
Proof.
  ins.
  red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    eexists _, _, _; repeat split; eauto; ins.
    red; desf; ins; desf.
  }

  {
    eexists _, _, _; repeat split; eauto; ins.
    symmetry in pEQ'; eapply hplus_preserves_Rlabel in pEQ'; eauto.
    rewrite hupds; ins.
    vauto.
  }
  
  {
    RMWin_def.
    apply hplus_not_undef_l, hdef_alt in DEFin; ins; desf.
    rewrite DEFin in ×.
    repeat eexists; eauto.
    by eapply hplus_preserves_Rlabel in pEQ; rewrite ?hupds; ins; desf; vauto.
  }
Qed.

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)))).
Proof.
  ins; red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    eexists _, _, _; repeat split; eauto; ins.
  }

  {
    eexists _, _, _; repeat split; eauto; ins.
    right; clear - UPD.
    apply initialize_is_atomic with (l := l).
    eapply hplus_has_atomic_l.
      eby symmetry in UPD.
    by ins; desf; rewrite hupds.
  }
  
  {
    RMWin_def.
    apply hplus_not_undef_l, hdef_alt in DEFin; ins; desf.
    rewrite DEFin in ×.
    repeat eexists; eauto.
    right; clear - pEQ.
    eapply hplus_has_atomic_l.
      eby symmetry in pEQ.
    by ins; desf; rewrite hupds.
  }
Qed.

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.
Proof.
  ins; red in VALID; red in EV; desf; ins; desc; try destruct DISJ; desc; try clear TYP;
    try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf);
    inv IN; rewrite ?(proj2 pU _ EV) in *;
    try (eby eexists _, _).

  {
    rewrite <- EQ in DEF.
    apply hplus_not_undef_l, hdef_alt in DEF; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply pOK.
  }

 
  {
    RMWin_def.
    by apply hplus_not_undef_l, hdef_alt in DEFin.
  }

  {
    rewrite qEQ, (hplusC _ (gheap _ _ _)), !(hplusAC (gheap _ _ _)) in DEF.
    apply hplus_not_undef_r in DEF.
    rewrite pEQ, <- hdef_alt.
    rewrite hplusC; rewrite hplusC in DEF.
    eapply hplus_sim_def; eauto.
    eapply hplus_sim; solve [by apply Hsim_sym | by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in *].
  }
  
  {
    eby eexists _, _; rewrite rEQ.
  }
  
  {
    red in TRAN; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
  }

  {
    RMWin_def.
    apply hplus_not_undef_r, hdef_alt in DEFin; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsInOK.
  }
Qed.

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.
Proof.
  ins; red in VALID; red in EV; desf; ins; desc; try destruct DISJ; desc; try clear TYP;
    try (by specialize (CONS_RF e'); desf; rewrite Heq in CONS_RF; desf);
    try (by red in EV; rewrite Heq in EV);
    rewrite ?(proj2 qU _ EV) in *; try (eby desf; eexists _, _); try (by apply hdef_alt).

  {
    clear - DEF qOK EV; apply hplus_not_undef_l, hdef_alt in DEF; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply qOK.
  }

  {
    eby eapply hdef_alt, hplus_not_undef_l.
  }

  {
    eby eapply hdef_alt, hplus_not_undef_l.
  }

  {
    eby eexists _, _; rewrite rEQ.
  }

  {
    red in TRAN; desf.
    apply hplus_def_inv_l in TRAN; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsOK.
  }

  {
    rewrite hplusAC, hdef_alt in DEF; desf; apply hplus_def_inv_l in DEF; desf.
    eapply hsum_def_inv; eauto.
    by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
  }

  {
    apply hplus_not_undef_r, hdef_alt in DEF; desf.
  }

  {
    red in TRAN; desf.
    by apply hplus_def_inv_r in TRAN.
  }

  {
    eby rewrite <- hplusA, hdef_alt in DEF; desf; eapply hplus_def_inv_r.
  }
Qed.

This page has been generated by coqdoc