Require Import Omega.
Require Import Vbase Arith Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas GpsGlobal.

Remove Hints plus_n_O mult_n_O.
Hint Immediate plus_n_O mult_n_O.

Local Open Scope string_scope.

Set Implicit Arguments.

C.3.1. Visibility


Definition is_pred A (rel : A A Prop) B a :=
   b, In b B clos_refl_trans A rel a b.

Definition depth_metric A (rel: A A Prop) V acts :=
  length (filter (mydecf (is_pred rel acts)) V).

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 clos_trans_hbE :
   lab sb rf a b (HB: clos_trans actid (happens_before lab sb rf) a b),
    happens_before lab sb rf a b.
Proof. induction 1; vauto. Qed.

Lemma length_filter_imp :
   A (f g : A Prop) (IMP : x, f x g x) l,
    length (filter (mydecf f) l)
    length (filter (mydecf g) l).
Proof.
  unfold mydecf; induction l; ins; desf; ins; eauto; try omega.
  destruct n; eauto.
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, mydecf; ins; desf.
    destruct (classic (In b B)); eauto.
    by exploit HB; eauto; ins; desf; eauto using clos_refl_trans.
  assert (P1: is_pred rel B b).
    by unfold is_pred; desf; eauto using clos_refl_trans.
  assert (P2: ¬ is_pred rel A b).
    clear -NHB NIN; unfold is_pred; intro; desf.
    by apply clos_refl_transD in H0; unfold not in *; desf; eauto.
  assert (IN' : In b V) by eauto.
  eapply In_split in IN'; desf; rewrite !filter_app, !app_length; ins.
  unfold mydecf at 2 6; desf; ins.
  generalize (length_filter_imp _ _ IMP l1), (length_filter_imp _ _ IMP l2).
  ins; omega.
Qed.

A useful induction principle for happens-before graphs.

Lemma edge_depth_ind lab sb rf V
  (IRR : irreflexive (happens_before lab sb rf) )
  (HC: prefix_closed sb rf V) (P : tagged_edge Prop) :
  ( edge
    (IH: edge'
            (LT: happens_before lab sb rf (te_src edge') (te_src edge)),
      P edge')
    (IN : In (te_src edge) V),
    P edge)
   edge, In (te_src edge) V P edge.
Proof.
  intros until edge.
  generalize (S (depth_metric (happens_before lab sb rf) V (te_src edge :: nil))),
      (lt_n_Sn (depth_metric (happens_before lab sb rf) V (te_src edge :: nil))).
  intro n'.
  revert edge; induction n'; ins; try omega.
  eapply H; ins; eapply IHn'; ins; eauto using prefix_closed_hb.
  eapply lt_le_trans, lt_n_Sm_le, H0.
  eapply depth_lt; ins; desf; eauto; instantiate;
    intro; desf; [rewrite H2 in *|]; eauto using t_step, t_trans, clos_trans_hbE.
Qed.

Visibility of allocation


Lemma res_get_plus_alloc r r' l :
  res_get (res_plus r r') l p_bot
  res_get r l p_bot res_get r' l p_bot.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto.
  right; congruence.
Qed.

Lemma res_get_rsum_alloc rl l :
  res_get (rsum rl) l p_bot
   r, In r rl res_get r l p_bot.
Proof.
  induction rl; ins; eapply res_get_plus_alloc in H; desf; eauto.
  specialize (IHrl H); desf; eauto.
Qed.

Lemma incoming_allocated :
   acts L b l (IN: res_get (incoming acts L b) l p_bot),
     te, te_tgt te = Some b res_get (L te) l p_bot.
Proof.
  ins; repeat first [apply res_get_plus_alloc in IN; desf|
                     apply res_get_rsum_alloc in IN; desf];
  repeat (rewrite in_map_iff in *; desf); eexists; split; eauto; ins.
Qed.

Lemma res_get_plus_bot r r' (D: res_plus r r' Rundef) l :
  res_get (res_plus r r') l = p_bot res_get r l = p_bot res_get r' l = p_bot.
Proof.
  split; ins; desf.
  2: by apply NNPP; intro X; apply res_get_plus_alloc in X; desf.
  destruct r, r'; ins; desf; ins; inv_lplus l; unfold prot_plus in *;
    desf; split; congruence.
Qed.

Lemma res_get_rsum_bot rl (D: rsum rl Rundef) l :
  res_get (rsum rl) l = p_bot r, In r rl res_get r l = p_bot.
Proof.
  induction rl; ins.
  rewrite res_get_plus_bot, IHrl; ins.
  2: by destruct a; ins; desf.
  clear; intuition; desf.
Qed.

Lemma guar_allocated :
   IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l
    (GET: res_get r l = p_bot)
    (NA: ¬ l' n, act = Aalloc l' n l' l l' + n),
    r_sb +!+ r_rf Rundef
    res_get r_sb l = p_bot
    res_get r_rf l = p_bot.
Proof.
  destruct act; ins; desf; desf; ins; rewrite ?res_plus_emp_r; try done.

  by destruct r; ins; repeat split; try done; desf; desf; destruct NA;
     eauto 10.

  by repeat split; try done; intro X; rewrite X in *; ins.
  by repeat split; try done; intro X; rewrite X in *; ins.

  repeat split; try done; try (by destruct r).
  unfold res_upd; desf; ins; case eqnP; ins; desf; congruence.

  repeat split; try done; try (by destruct r).
  unfold res_upd; desf; ins; case eqnP; ins; desf; congruence.

  unfold atomic_guar in *; desf; destruct (eqP l0 l); desf; try congruence;
  by split; try eapply res_get_plus_bot; ins; rewrite REQ;
     destruct r; ins; desf; desf.

  unfold atomic_guar in *; desf; destruct (eqP l0 l); desf; try congruence;
  by split; try eapply res_get_plus_bot; ins; rewrite REQ;
     destruct r; ins; desf; desf.
Qed.

Lemma outgoing_allocated :
    IE acts M amap rf L E edge
     (V: valid_node IE acts M amap rf L E (te_src edge)) l
     (G: res_get (L edge) l p_bot)
     (IN: b, te_tgt edge = Some b In b acts)
     (IN': sigma a, edge = TescS sigma a In sigma E)
     (NA: ¬ l' n, amap (te_src edge) = Aalloc l' n l' l l' + n),
   res_get (incoming acts L (te_src edge)) l p_bot.
Proof.
  ins; red in V; desf.
  cut (res_get (r +!+ out_esc acts L E (te_src edge)) l p_bot).
    by clear - VG; red in VG; desf; rewrite VG, VG0.
  clear - GUAR VG G NA IN IN'.
  red in VG; desf.
  intro X; unfold out_esc in *; rewrite !res_get_plus_bot, res_get_rsum_bot in *;
    desf; try (by intro M; rewrite M, ?res_plus_undef in *).
  eapply guar_allocated in GUAR; desf; eauto.
  unfold out_rf, out_sb in *; rewrite !res_get_plus_bot, res_get_rsum_bot in *;
    desf; try (by intro M; rewrite M, ?res_plus_undef in *).
  destruct edge; ins; destruct G; eauto using in_map.
  eapply X0, in_map, in_map_iff; eauto.
Qed.

Lemma nemp_of_get_at r l tau S : res_get r l = p_at tau S r res_emp.
Proof.
  red; ins; desf.
Qed.

Lemma nemp_of_get_nbot r l : res_get r l p_bot r res_emp.
Proof.
  red; ins; desf.
Qed.

Hint Resolve nemp_of_get_at nemp_of_get_nbot.

Lemma prefix_closed_pres_in sb rf N a :
  prefix_closed sb rf N
  In a N
  pres_in sb rf a N.
Proof.
  unfold prefix_closed, pres_in; ins; desf; eauto.
Qed.

Lemma hb_one :
   acts amap sb rf L E
    (LR : label_restr acts amap sb rf L E) te b,
  te_tgt te = Some b
  L te res_emp
  happens_before amap sb rf (te_src te) b.
Proof.
  ins; apply NNPP; intro; destruct te, H0; ins; desf;
    apply LR; intro; destruct H1; eauto.
Qed.

Lemma lab_src_in_acts :
   acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (LR : label_restr acts amap sb rf L E) te
    (G : L te res_emp),
  In (te_src te) acts.
Proof.
  ins; apply NNPP; intro X.
  assert (Y: L te = res_emp); [|by rewrite Y in *].
  destruct te; ins; eapply LR; eauto; intro HB;
  destruct X; eapply proj1, Consistent_hb_in; eauto.
Qed.

Lemma lab_tgt_in_acts :
   acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (LR : label_restr acts amap sb rf L E) te
    (G : L te res_emp) b
    (T : te_tgt te = Some b),
  In b acts.
Proof.
  ins; apply NNPP; intro X.
  assert (Y: L te = res_emp); [|by rewrite Y in *].
  destruct te; ins; eapply LR; eauto; intro HB; desf;
  destruct X; eapply proj2, Consistent_hb_in; eauto.
Qed.

Lemma visible_allocation_one :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) te l
    (G: res_get (L te) l p_bot) (X: In (te_src te) N),
   a l' n, may_happens_before amap sb rf a (te_src te)
            amap a = Aalloc l' n
            l' l l' + n.
Proof.
  intros; revert G; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te X; ins.
  destruct (classic ( l' n, amap (te_src edge) = Aalloc l' n l' l l' + n)).
    desf; repeat eexists; eauto; apply mhbE; eauto.
  assert (K:=G).
  eapply outgoing_allocated, incoming_allocated in K; eauto using lab_tgt_in_acts; desf.
  exploit IH; try eexact K0; ins; desf; eauto; eauto using hb_one.
    by repeat eexists; eauto; eapply mhb_trans, mhbE; eauto using hb_one.
  by ins; apply NNPP; intro; red in LR; desf; rewrite LRescS in G; vauto.
Qed.

Lemma visible_allocation :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) b (IN: pres_in sb rf b N) l
    (G: res_get (incoming acts L b) l p_bot),
   a l' n, happens_before amap sb rf a b
            amap a = Aalloc l' n
            l' l l' + n.
Proof.
  ins; eapply incoming_allocated in G; desf.
  assert (X: In (te_src te) N).
    eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  exploit visible_allocation_one; eauto; intro; desf.
  repeat eexists; eauto.
  rewrite mhbE in *; desf; eauto using hb_trans, hb_one.
Qed.

Visibility of non-atomic assertions


Definition is_na r l v := k, res_get r l = p_na k v.

Lemma res_get_plus_naE r r' l k v :
  res_get (res_plus r r') l = p_na k v
   k, res_get r l = p_na k v res_get r' l = p_na k v.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto;
    try solve [ k0; left; congruence | k; right; congruence].
Qed.

Lemma res_get_rsum_naE rl l k v :
  res_get (rsum rl) l = p_na k v
   r k, In r rl res_get r l = p_na k v.
Proof.
  induction[k] rl; ins; eapply res_get_plus_naE in H; desf; eauto.
  specialize (IHrl _ H); desf; eauto.
Qed.

Lemma is_na_plusE r r' l v :
  is_na (res_plus r r') l v is_na r l v is_na r' l v.
Proof.
  unfold is_na; ins; desf; eapply res_get_plus_naE in H; desf; eauto.
Qed.

Lemma is_na_rsumE rl l v :
  is_na (rsum rl) l v r, In r rl is_na r l v.
Proof.
  induction rl; ins; [red in H|eapply is_na_plusE in H]; desf; eauto.
  specialize (IHrl H); desf; eauto.
Qed.

Lemma incoming_na :
   acts L b l v (IN: is_na (incoming acts L b) l v),
     te, te_tgt te = Some b is_na (L te) l v.
Proof.
  ins; repeat first [apply is_na_plusE in IN; desf|
                     apply is_na_rsumE in IN; desf];
  repeat (rewrite in_map_iff in *; desf); eexists; split; eauto; ins.
Qed.

Lemma is_na_plus r r' (D: res_plus r r' Rundef) l v :
  is_na (res_plus r r') l v
  is_na r l v is_na r' l v.
Proof.
  split; ins; desf; eauto using is_na_plusE;
  unfold is_na in *; desf;
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; desf;
  try rewrite H in *; eauto.
Qed.

Lemma is_na_rsum rl (D: rsum rl Rundef) l v :
  is_na (rsum rl) l v r, In r rl is_na r l v.
Proof.
  induction rl; ins; rewrite ?is_na_plus, ?IHrl; try split; ins; desf; eauto.
    by red in H; desf.
  by destruct a; ins; desf.
Qed.

Lemma guar_na_sb :
   IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l v
    (GET: is_na r_sb l v)
    (NW: ¬ is_writeLV act l v),
    is_na r l v.
Proof.
  destruct act; ins; desf; desf; ins; rewrite ?res_plus_emp_r; try done.

  by unfold is_na in *; desf; destruct r; ins; desf; vauto.
  by unfold is_na in *; desf; destruct r; ins; desf; desf; desf; vauto; destruct NW; desf.
  by unfold is_na in *; desf; destruct r; ins; desf; desf; desf; vauto; destruct NW; desf.

  unfold is_na, atomic_guar in *; desf;
  assert (REQ':= REQ);
  eapply (f_equal (fun fres_get f l0)) in REQ'; destruct r; ins;
  destruct (eqnP l0 l); desf; try congruence;
  destruct r_sb; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.

  unfold is_na, atomic_guar in *; desf;
  assert (REQ':= REQ);
  eapply (f_equal (fun fres_get f l0)) in REQ'; destruct r; ins;
  destruct (eqnP l0 l); desf; try congruence;
  destruct r_sb; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.
Qed.

Lemma guar_na_rf :
   IE r_pre r act r_sb r_rf
    (GUAR : guar IE r_pre r act r_sb r_rf) l v
    (GET: is_na r_rf l v)
    (NW: ¬ is_writeLV act l v),
    is_na r l v.
Proof.
  unfold is_na; destruct act; ins; desf; desf; ins; rewrite ?res_plus_emp_r; try done.

  unfold atomic_guar in *; desf; rewrite res_plusC in *;
  assert (REQ':= REQ);
  eapply (f_equal (fun fres_get f l0)) in REQ'; destruct r; ins; desf; try congruence;
  destruct r_rf; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.

  unfold atomic_guar in *; desf; rewrite res_plusC in *;
  assert (REQ':= REQ);
  eapply (f_equal (fun fres_get f l0)) in REQ'; destruct r; ins; desf; try congruence;
  destruct r_rf; ins; desf; inv_lplus l0; try rewrite GET in *; ins; desf; try congruence;
  eauto using eq_trans.
Qed.

Lemma guar_def :
   IE (r_pre r : resource) (act : act) (r_sb r_rf : resource),
  guar IE r_pre r act r_sb r_rf
  r_sb Rundef r_rf Rundef.
Proof.
  destruct act; ins; desf; desf; try red in AG; desf;
    try (by destruct r; ins);
    try (by destruct r_sb, r_rf).
Qed.

Lemma outgoing_na :
    IE acts M amap rf L E edge
     (V: valid_node IE acts M amap rf L E (te_src edge)) l v
     (G: is_na (L edge) l v)
     (IN: b, te_tgt edge = Some b In b acts)
     (IN': sigma a, edge = TescS sigma a In sigma E)
     (NW: ¬ is_writeLV (amap (te_src edge)) l v),
   is_na (incoming acts L (te_src edge)) l v.
Proof.
  ins; red in V; desf.
  cut (is_na (r +!+ out_esc acts L E (te_src edge)) l v).
    by clear - VG; red in VG; desf; rewrite VG, VG0.
  clear - GUAR VG G NW IN IN'.
  red in VG; desf; unfold out_esc in *;
  rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × ).
  destruct edge; ins; eauto 10 using in_map.
    eapply guar_na_sb in GUAR; eauto; unfold out_sb in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    eapply guar_na_sb in GUAR; eauto; unfold out_sb in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    eapply guar_na_rf in GUAR; eauto; unfold out_rf in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    eapply guar_na_rf in GUAR; eauto; unfold out_rf in *; eapply guar_def in GUAR; desc;
    rewrite !is_na_plus, is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.

    right; right;
    rewrite is_na_rsum; try (by intro Z; rewrite Z, ?res_plus_undef in × );
    eauto 7 using in_map.
Qed.

Lemma res_get_plus_na_or_bot r r' l v :
  is_na r l v res_get r l = p_bot
  is_na r' l v res_get r' l = p_bot
  is_na (r +!+ r') l v res_get (r +!+ r') l = p_bot.
Proof.
  unfold is_na; ins; destruct r, r'; ins; desf; ins; inv_lplus l;
  rewrite ?H, ?H0 in *; ins; desf; desf; eauto.
Qed.

Lemma res_get_rsum_na_or_bot rl l v :
  ( r, In r rl is_na r l v res_get r l = p_bot)
  is_na (rsum rl) l v res_get (rsum rl) l = p_bot.
Proof.
  induction rl; ins; try eapply res_get_plus_na_or_bot; eauto.
Qed.

Lemma compat_def2 :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) L E
    (LR : label_restr acts amap sb rf L E)
    (CC : compat amap sb rf L) edge
    (NE : L edge res_emp) edge'
    (NE': L edge' res_emp)
    (NEQ : edge edge')
    (NHB : b (TGT: te_tgt edge = Some b)
             (MHB: may_happens_before amap sb rf b (te_src edge')), False)
    (NHB': b (TGT: te_tgt edge' = Some b)
             (MHB: may_happens_before amap sb rf b (te_src edge)), False)
    (DEF : L edge +!+ L edge' = Rundef),
  False.
Proof.
  ins; apply (CC (edge :: edge' :: nil)); ins; rewrite ?res_plus_emp_r;
  desf; desf; eauto; try (by constructor; vauto; intro; ins; desf);
  eapply hb_one in TGT; eauto; rewrite mhbE in *; desf;
  red in CONS; desc; edestruct ACYC; eauto using hb_trans, hb_in_ct.
Qed.

Lemma hb_irr :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) a
    (HB: happens_before amap sb rf a a),
    False.
Proof.
  unfold Consistent; ins; desf.
  eapply (ACYC a); revert HB; generalize a at 1 3; induction 1; vauto.
  unfold imm_happens_before, synchronizes_with in *; desf; eauto using clos_trans.
Qed.

Lemma compat_inc :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a,
  incoming acts L a Rundef.
Proof.
  red; ins.
  apply (CC (map (Tsb^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
             ++ map (Trf^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
             ++ map (Tesc^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts))).
    rewrite !nodup_app; repeat apply conj;
    try eapply nodup_map; try eapply nodup_filter; ins; try congruence;
    by unfold disjoint; intro; rewrite ?in_app_iff, !in_map_iff; ins; desf.

    by ins; rewrite !in_app_iff, !in_map_iff in *; desf; rewrite in_filter_iff in *; ins; desf;
       rewrite mhbE in *; desf; unfold mydecf in *; desf; eapply hb_irr; eauto 2 using hb_trans.

  by ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins; apply LR; eauto.
Qed.

Lemma compat_inc_sink :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a b,
  a = b
  happens_before amap sb rf a b
  L (TsbS b) +!+ incoming acts L a Rundef.
Proof.
  ins.
  apply NNPP; intro X.
  apply not_or_and in X; desf.
  apply not_or_and in X0; desf.
  apply NNPP in X1.
  apply (CC (TsbS b :: map (Tsb^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
                     ++ map (Trf^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
                     ++ map (Tesc^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts))).
    constructor; [by rewrite !in_app_iff, !in_map_iff; intro; desf|].
    rewrite !nodup_app; repeat apply conj;
    try eapply nodup_map; try eapply nodup_filter; ins; try congruence;
    by unfold disjoint; intro; rewrite ?in_app_iff, !in_map_iff; ins; desf.

    by ins; rewrite !in_app_iff, !in_map_iff in *; desf; rewrite in_filter_iff in *; ins; desf;
       rewrite mhbE in *; desf; unfold mydecf in *; desf; eapply hb_irr; eauto using hb_trans.

  ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins; apply LR; eauto.
Qed.

Lemma compat_inc_nonsink :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND : NoDup acts) L
    (CC : compat amap sb rf L) E
    (LR : label_restr acts amap sb rf L E) a edge b
    (E : te_tgt edge = Some b),
  may_happens_before amap sb rf a (te_src edge)
  may_happens_before amap sb rf b a
  L edge +!+ incoming acts L a Rundef.
Proof.
  ins.
  rewrite !mhbE.
  apply NNPP; intro X.
  apply not_or_and in X; desf.
  apply not_or_and in X; desf.
  apply not_or_and in X0; desf.
  apply not_or_and in X0; desf.
  apply NNPP in X2.
  destruct (classic (L edge = res_emp)) as [EMP|NEMP].
    by rewrite EMP, res_plus_emp_l in *; eapply compat_inc in X2; eauto.
  eapply hb_one in NEMP; eauto.
  apply (CC (edge :: map (Tsb^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
                     ++ map (Trf^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts)
                     ++ map (Tesc^~ a) (filter (mydecf (happens_before amap sb rf^~ a)) acts))).
    constructor; [by rewrite !in_app_iff, !in_map_iff; intro; desf; ins; desf|].
    rewrite !nodup_app; repeat apply conj;
    try eapply nodup_map; try eapply nodup_filter; ins; try congruence;
    by unfold disjoint; intro; rewrite ?in_app_iff, !in_map_iff; ins; desf.

    by ins; rewrite !in_app_iff, !in_map_iff in *; desf; desf; try rewrite in_filter_iff in *; ins; desf;
       rewrite mhbE in *; desf; unfold mydecf in *; desf;
       try solve [eauto 3 using hb_trans | eapply hb_irr; eauto 3 using hb_trans].

  by ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins; apply LR; eauto.
Qed.

Definition writeL_pre x :=
  match x with
    | p_botFalse
    | p_na k vk = pe_full
    | _True
  end.

Lemma is_writeL_inc IE acts M amap rf a l L E :
  is_writeL (amap a) l
  valid_node IE acts M amap rf L E a
  writeL_pre (res_get (incoming acts L a) l).
Proof.
  unfold valid_node; ins; desf.
  red in GUAR; red in VG; desf; desf; try red in AG; desf; rewrite VG; ins; desf;
  by destruct r; ins; desf; inv_lplus l; red; unfold prot_plus in *; desf; desf.
Qed.

Lemma is_writeL_in IE acts M amap rf a l L E :
  is_writeL (amap a) l
  valid_node IE acts M amap rf L E a
   edge', te_tgt edge' = Some a res_get (L edge') l p_bot.
Proof.
  unfold valid_node; ins; desf.
  apply (incoming_allocated acts).
  cut (res_get r l p_bot).
    red; ins; red in VG; desf; rewrite VG in *; ins.
    destruct r; ins; desf.
    by inv_lplus l; rewrite H1 in *; unfold prot_plus in *; desf.
  destruct (amap a); ins; desf; unfold atomic_guar in *; desf;
  try congruence.
Qed.

Lemma res_plus_is_na_writeL_pre r r' l v :
  is_na r l v
  writeL_pre (res_get r' l)
  r +!+ r' = Rundef.
Proof.
  unfold is_na; ins; desf; destruct r, r'; ins; desf.
  inv_lplus l; unfold prot_plus in *; desf; ins; desf.
  destruct k; ins.
Qed.

Lemma visible_na_one :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) te
    (IN : In (te_src te) N) b
    (T : te_tgt te = Some b) l v
    (G : is_na (L te) l v),
   a,
    << HB : happens_before amap sb rf a b >>
    << WRI: is_writeLV (amap a) l v >>
    << OTH: a' (W: is_writeL (amap a') l) (N: In a' N)
              (HB1: ¬ may_happens_before amap sb rf b a'),
              may_happens_before amap sb rf a' a >>.
Proof.
  ins; desf.
  assert (MHB: may_happens_before amap sb rf b b) by vauto.
  assert (OTH: a' (W: is_writeL (amap a') l) (N: In a' N)
              (HB1: happens_before amap sb rf a' b),
              happens_before amap sb rf a' b).
    by ins; rewrite mhbE; eauto.

  revert MHB OTH; generalize b at 2 3.
  revert b G T; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te IN; ins; unfold NW.
  destruct (classic (is_writeL (amap (te_src edge)) l)).
    desf; repeat eexists; eauto.
    by red in G; desf; eapply hb_one; eauto; intro X; rewrite X in ×.
  { clear IH.
    assert ( edge', te_src edge' = te_src edge
                          is_na (L edge') l v
                          res_get (L edge') l = p_bot).
      ins; destruct (classic (edge = edge')); desf; vauto.
      apply NNPP; intro; apply (CC (edge :: edge' :: nil)).
        by constructor; vauto; ins; intro; desf.
      by red in G; desc; ins; desf; desf;
         try eapply hb_one in T; eauto; try (by intro Z; rewrite Z in *; ins);
         try eapply hb_one in TGT; eauto; try (by intro Z; rewrite Z in *; ins);
         try rewrite H0 in *;
         red in CONS; desc; rewrite mhbE in *; desf; edestruct ACYC;
         eauto using hb_trans, hb_in_ct.
      ins; rewrite res_plus_emp_r.
      destruct (L edge); ins; desf; ins; destruct H2.
      inv_lplus l; unfold is_na, prot_plus in *; ins; desf; vauto.
    assert (is_na (out_sb acts L (te_src edge)) l v
            res_get (out_sb acts L (te_src edge)) l = p_bot).
      eapply res_get_plus_na_or_bot; eauto.
      eapply res_get_rsum_na_or_bot; eauto.
      by intros; repeat (rewrite in_map_iff in *; desf); eauto.
    specialize (V _ IN); red in V; desf; red in GUAR; desf; ins; subst; split; ins;
    unfold is_na, atomic_guar in *; desf;
    rewrite ?GUAR0, ?Gsb in *; ins; rewrite ?res_get_upds in *; desf;
      try (by intro Z; rewrite Z in × ).
  }
  {
    ins; clear IH.
    eapply is_writeL_inc in W; eauto.
    eapply compat_inc_nonsink with (a:=a') in T; eauto; desf.
    by destruct T; eauto using res_plus_is_na_writeL_pre.
  }

  assert (K:=G); red in G; desc.
  eapply outgoing_na, incoming_na in K; eauto; desf.
  2: by ins; eapply lab_tgt_in_acts; eauto; intro Z; rewrite Z in ×.
  assert (K':=K); eapply IH in K'; clear IH; desf; eauto.
  2: by red in K0; desc; eapply hb_one; eauto; intro X; rewrite X in ×.
  2: by eapply mhbE; eauto.
  repeat eexists; eauto.
  eapply hb_trans; eauto.
  by eapply hb_one; eauto; intro X; rewrite X in ×.

  ins; destruct (classic (may_happens_before amap sb rf (te_src edge) a')); eauto.

  ins; apply NNPP; intro X.
  assert (J := is_writeL_inc _ W (V _ N0)); desf.

  eapply compat_inc_nonsink with (a:=a') in T; eauto.
   desf; eauto.
     by rewrite mhbE in *; desf; eauto using hb_irr, hb_trans.
  by destruct T; eapply res_plus_is_na_writeL_pre; vauto.

  by ins; apply NNPP; intro; red in LR; desf; rewrite LRescS in G; vauto.
Qed.

Lemma visible_na :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc) (ND: NoDup acts) L E
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l v
    (G : is_na (incoming acts L b) l v),
   a,
    << HB : happens_before amap sb rf a b >>
    << WRI: is_writeLV (amap a) l v >>
    << OTH: a' (W: is_writeL (amap a') l) (N: In a' N)
              (NMHB: ¬ may_happens_before amap sb rf b a'),
              may_happens_before amap sb rf a' a >>.
Proof.
  ins; unfold NW; eapply incoming_na in G; desf; eauto.
  assert (X: In (te_src te) N).
    red in G0; desc; eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  eapply visible_na_one; eauto.
Qed.

Visibility of uninitialized locations


Lemma res_get_plus_uninitE r r' l :
  res_get (res_plus r r') l = p_uninit
  res_get r l = p_uninit res_get r' l = p_uninit.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto;
  try (left; congruence); right; congruence.
Qed.

Lemma res_get_rsum_uninitE rl l :
  res_get (rsum rl) l = p_uninit
   r, In r rl res_get r l = p_uninit.
Proof.
  induction rl; ins; eapply res_get_plus_uninitE in H; desf; eauto.
  specialize (IHrl H); desf; eauto.
Qed.

Lemma res_get_plus_uninit r r' (D: res_plus r r' Rundef) l :
  res_get (res_plus r r') l = p_uninit
  res_get r l = p_uninit res_get r' l = p_uninit.
Proof.
  destruct r; ins; desf; ins; inv_lplus l; unfold prot_plus in *; desf; vauto;
  split; ins; desf;
    try solve [left; congruence | right; congruence | congruence].
Qed.

Lemma res_get_rsum_uninit rl (D: rsum rl Rundef) l :
  res_get (rsum rl) l = p_uninit
   r, In r rl res_get r l = p_uninit.
Proof.
  induction rl; ins; rewrite ?res_get_plus_uninit, ?IHrl; try split; ins; desf; eauto.
  by destruct a; ins; desf.
Qed.

Lemma incoming_uninit :
   acts L b l (IN: res_get (incoming acts L b) l = p_uninit),
     te, te_tgt te = Some b res_get (L te) l = p_uninit.
Proof.
  ins; repeat first [apply res_get_plus_uninitE in IN; desf|
                     apply res_get_rsum_uninitE in IN; desf];
  repeat (rewrite in_map_iff in *; desf); eexists; split; eauto; ins.
Qed.

Lemma mhb_hb_trans:
   (amap : actid act) (sb : actid actid Prop)
    (rf : actid option actid) (a b c : actid),
  may_happens_before amap sb rf a b
  happens_before amap sb rf b c happens_before amap sb rf a c.
Proof.
  ins; rewrite mhbE in *; desf; eauto using hb_trans.
Qed.

Lemma helper_out_def :
   a acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts)
    (ND': NoDup E)
    (CC: compat amap sb rf L)
    (LR : label_restr acts amap sb rf L E),
  outgoing acts L E a Rundef.
Proof.
  ins; intro; eapply (CC (TrfS a :: TsbS a ::
      map (Tsb a) (filter (mydecf (happens_before amap sb rf a)) (acts)) ++
      map (Trf a) (filter (mydecf (happens_before amap sb rf a)) (acts)) ++
      map (TescS^~ a) E ++
      map (Tesc a) (filter (mydecf (happens_before amap sb rf a)) (acts)))).
      repeat constructor; try by rewrite ?in_cons_iff, ?in_app_iff, ?in_map_iff; intro; desf.
      rewrite !nodup_app; intuition; try eapply nodup_map; eauto; ins; try congruence;
      unfold disjoint; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; eauto using nodup_filter.
    red in CONS; desf; ins.
    assert (te_src te = a); subst; [|clear IN].
      by clear -IN; ins; desf; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; ins; desf.
    by ins; desf; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; ins; desf;
       rewrite ?filter_In in *; desf; unfold mydecf in *; desf;
       edestruct ACYC; eauto using mhb_hb_trans, hb_in_ct.
  unfold outgoing, out_sb, out_rf, out_esc in H;
  rewrite !res_plusA, !(res_plusAC (L (TrfS _))) in H.
  by ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins;
     apply LR; intro; desf; eauto.
Qed.

Lemma outgoing_uninit :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) edge l
    (GG : res_get (L edge) l = p_uninit),
  res_get (outgoing acts L E (te_src edge)) l = p_uninit.
Proof.
  ins; assert (DEF := helper_out_def (te_src edge) CONS ND ND' CC LR).
  unfold outgoing, out_esc, out_rf, out_sb in ×.
  rewrite !res_get_plus_uninit, !res_get_rsum_uninit;
    try (by intro X; rewrite X, ?res_plus_undef in *).
  assert ( b, te_tgt edge = Some b In b acts).
    by apply (lab_tgt_in_acts CONS LR); ins; intro X; rewrite X in *; ins.
  assert (IN': sigma a, edge = TescS sigma a In sigma E).
    by ins; apply NNPP; intro; red in LR; desf; rewrite LRescS in GG; vauto.
  by destruct edge; ins; eauto 10 using in_map.
Qed.

Lemma vnode_uninit :
   acts M amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) IE edge
    (V: valid_node IE acts M amap rf L E (te_src edge)) l
    (GG : res_get (L edge) l = p_uninit)
    (NA : ¬ l' n, amap (te_src edge) = Aalloc l' n
                         l' l l' + n),
  res_get (incoming acts L (te_src edge)) l = p_uninit.
Proof.
  unfold valid_node; ins; desf.
  cut (res_get (r +!+ out_esc acts L E (te_src edge)) l = p_uninit).
    by clear - VG; red in VG; desc; rewrite VG, VG0.
  rewrite res_get_plus_uninit; [|red in VG; desf; congruence].
  clear VG VrfM VrfS VrfS' RS.
  eapply outgoing_uninit in GG; eauto.
  unfold outgoing in GG; rewrite <- res_plusA in GG.
  apply res_get_plus_uninitE in GG; desf; eauto; left.
  red in GUAR; desf; desf;
    rewrite ?GUAR, ?GUAR0, ?GUAR1, ?res_plus_emp_r in *; ins.

  by destruct r; ins; desf; desf; edestruct NA; eauto 8.
  by destruct r; ins; desf.
  by destruct r; ins; desf.
  by red in AG; desf; rewrite REQ in *; destruct r; ins; desf.
  by red in AG; desf; rewrite REQ in *; destruct r; ins; desf.
Qed.

Lemma is_writeL_out :
   acts M amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) L E (ND': NoDup E)
    (LR : label_restr acts amap sb rf L E)
    (CC: compat amap sb rf L) edge l
    (GG: res_get (L edge) l = p_uninit)
    (W : is_writeL (amap (te_src edge)) l) IE
    (V : valid_node IE acts M amap rf L E (te_src edge)),
  False.
Proof.
  ins; eapply outgoing_uninit in GG; eauto.
  remember (te_src edge) as b; clear edge Heqb.
  red in V; desf.
  unfold outgoing in GG; rewrite <- res_plusA in GG.
  apply res_get_plus_uninitE in GG; desf.

  red in GUAR; desf; desf;
  rewrite ?GUAR, ?GUAR0, ?GUAR1, ?res_plus_emp_r in *; ins; desf.

  by rewrite res_get_upds in *; desf; intro; desf.
  by rewrite res_get_upds in *; desf; intro; desf.
  by red in AG; desf; rewrite REQ, res_get_upds in GG; desf; intro; desf.
  by red in AG; desf; rewrite REQ, res_get_upds in GG; desf; intro; desf.

  assert (GG': res_get r l = p_bot); [|clear GG].
    red in VG; desf; destruct r; ins; desf.
    by inv_lplus l; ins; rewrite GG in *; destruct (pmap l); ins.

  red in GUAR; desf; desf;
  rewrite ?GUAR, ?GUAR0, ?GUAR1, ?res_plus_emp_r in *; ins; desf; try congruence.
  red in AG; desf; congruence.
Qed.

Lemma visible_uninit2 :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l
    (IN: res_get (incoming acts L b) l = p_uninit) a
    (W: is_writeL (amap a) l)
    (PI': pres_in sb rf a N)
    (J : res_get (incoming acts L a) l p_bot),
    may_happens_before amap sb rf b a.
Proof.
  ins.
  eapply incoming_uninit in IN; desf.
  apply incoming_allocated in J; destruct J as (edge' & J); desf.
  assert (X: In (te_src te) N).
    clear PI'; eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  assert (X': In (te_src edge') N).
    clear PI; eapply pres_in_hb; eauto.
    by eapply hb_one; eauto.
  clear PI PI'; revert b IN IN0; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te X; ins.
  destruct (classic ( l' n, amap (te_src edge) = Aalloc l' n l' l l' + n)).
  {
    exploit visible_allocation_one; eauto.
    intro K; desf.
      assert (C:=CONS); red in C; desc.
      pose proof (Ca _ _ _ H _ _ _ K0); desf; try (exfalso; omega).
      rewrite K0 in H; desf.
    apply NNPP; intro T.
    eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.
      by intro Z; rewrite Z in *; desf; destruct T; apply mhbE; auto.

      ins; rewrite TGT in *; desf.
      by eapply T, mhb_trans, mhbE; eauto using hb_one.

      ins; rewrite TGT in *; desf.
      eapply hb_one in TGT; eauto.
      by rewrite mhbE in *; desf; try rewrite K in *;
         edestruct ACYC; eapply hb_in_ct; eauto using hb_trans.

      destruct (L edge), (L edge'); ins; desf.
      by inv_lplus l; rewrite IN1 in *; ins; desf.
  }

  assert (IN': res_get (incoming acts L (te_src edge)) l = p_uninit).
    by eapply vnode_uninit; eauto.
  eapply incoming_uninit in IN'; desf.
  exploit (IH te); clear IH; eauto.
    by eapply hb_one; eauto; intro Z; rewrite Z in ×.
  intro; apply NNPP; intro T.
  destruct (classic (te = edge')); desf.
    by eapply is_writeL_out with (edge := edge); eauto.
  destruct (classic (edge = edge')); desf.
    by apply T, mhbE; eauto.

  destruct (classic (happens_before amap sb rf (te_src edge') (te_src edge))).
  {
    eapply (compat_def2 CONS LR CC) with (edge := te) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.

      ins; rewrite TGT in *; desf.
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans.

      ins; rewrite TGT in *; desf.
      eapply hb_one in IN'; eauto; try (by intro Z; rewrite Z in *; ins).
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans, mhb_trans.

    destruct (L te), (L edge'); ins; desf.
    by inv_lplus l; unfold prot_plus in *; ins; desf.
  }

  eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
    by intro Z; rewrite Z in *; desf.

    ins; rewrite TGT in *; desf.
    by eapply T, mhb_trans, mhbE; eauto using hb_one.

    ins; rewrite TGT in *; desf.
    eapply hb_one in TGT; eauto.
    by rewrite mhbE in MHB; desf; eauto using hb_trans.

  destruct (L edge), (L edge'); ins; desf.
  by inv_lplus l; unfold prot_plus in *; ins; desf.
Qed.

Lemma visible_uninit :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND' : NoDup E) L
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (CC: compat amap sb rf L)
    (PC: prefix_closed sb rf N) b (PI: pres_in sb rf b N) l
    (IN: res_get (incoming acts L b) l = p_uninit) a
    (W: is_writeL (amap a) l) (INa: In a N),
    may_happens_before amap sb rf b a.
Proof.
  ins.
  eapply incoming_uninit in IN; desf.
  assert (X: In (te_src te) N).
    eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  clear PI; revert b IN IN0; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te X; ins.
  destruct (classic ( l' n, amap (te_src edge) = Aalloc l' n l' l l' + n)).
  {
    assert (J := is_writeL_in _ W (V _ INa)); desf.
    exploit visible_allocation_one; eauto.
      by eapply prefix_closed_hb; eauto using hb_one.
    intro K; desf.
      assert (C:=CONS); red in C; desc.
      pose proof (Ca _ _ _ H _ _ _ K0); desf; try (exfalso; omega).
      rewrite K0 in H; desf.
    apply NNPP; intro T.
    eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.
      by intro Z; rewrite Z in *; desf; destruct T; apply mhbE; auto.

      ins; rewrite TGT in *; desf.
      by eapply T, mhb_trans, mhbE; eauto using hb_one.

      ins; rewrite TGT in *; desf.
      eapply hb_one in TGT; eauto.
      by rewrite mhbE in *; desf; try rewrite K in *;
         edestruct ACYC; eapply hb_in_ct; eauto using hb_trans.

      destruct (L edge), (L edge'); ins; desf.
      by inv_lplus l; rewrite IN1 in *; ins; desf.
  }

  assert (IN': res_get (incoming acts L (te_src edge)) l = p_uninit).
    by eapply vnode_uninit; eauto.
  eapply incoming_uninit in IN'; desf.
  exploit (IH te); clear IH; eauto.
    by eapply hb_one; eauto; intro Z; rewrite Z in ×.
  intro; apply NNPP; intro T.
  assert (J := is_writeL_in _ W (V _ INa)); desf.
  destruct (classic (te = edge')); desf.
    by eapply is_writeL_out with (edge := edge); eauto.
  destruct (classic (edge = edge')); desf.
    by apply T, mhbE; eauto.

  destruct (classic (happens_before amap sb rf (te_src edge') (te_src edge))).
  {
    eapply (compat_def2 CONS LR CC) with (edge := te) (edge' := edge'); eauto.
      by intro Z; rewrite Z in *; desf.

      ins; rewrite TGT in *; desf.
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans.

      ins; rewrite TGT in *; desf.
      eapply hb_one in IN'; eauto; try (by intro Z; rewrite Z in *; ins).
      by red in CONS; desc; eapply ACYC, hb_in_ct; eauto using mhb_hb_trans, mhb_trans.

    destruct (L te), (L edge'); ins; desf.
    by inv_lplus l; unfold prot_plus in *; ins; desf.
  }

  eapply (compat_def2 CONS LR CC) with (edge := edge) (edge' := edge'); eauto.
    by intro Z; rewrite Z in *; desf.

    ins; rewrite TGT in *; desf.
    by eapply T, mhb_trans, mhbE; eauto using hb_one.

    ins; rewrite TGT in *; desf.
    eapply hb_one in TGT; eauto.
    by rewrite mhbE in MHB; desf; eauto using hb_trans.

  destruct (L edge), (L edge'); ins; desf.
  by inv_lplus l; unfold prot_plus in *; ins; desf.
Qed.

Visibility of atomics


Lemma incoming_atomic :
   acts L b l tau S (GG: res_get (incoming acts L b) l = p_at tau S) s
    (IN : In s (SL_list S)),
     te S', te_tgt te = Some b res_get (L te) l = p_at tau S'
       In s (SL_list S').
Proof.
  ins; repeat first [eapply get_plus_at_oneD in GG; eauto; desf|
                     eapply get_rsum_at_oneD in GG; eauto; desf];
  repeat (rewrite in_map_iff in *; desf); eexists _,_; repeat split; eauto; ins.
Qed.

Lemma res_get_plus_at_iff :
   r r' (D: r +!+ r' Rundef) l tau s,
    ( S',
      res_get (r +!+ r') l = p_at tau S'
      In s (SL_list S'))
    ( S,
      res_get r l = p_at tau S
      In s (SL_list S))
    ( S,
      res_get r' l = p_at tau S
      In s (SL_list S)).
Proof.
  split; ins; desf.
    destruct r, r'; ins; desf; ins.
    inv_lplus l; rewrite H in *; clear H; destruct (pmap l), (pmap0 l);
      ins; desf; desf; eauto.
    unfold mk_slist in *; desf; ins.
    by rewrite in_undup_iff, In_sort, in_app_iff in *; desf; eauto.
  by exploit res_get_plus; eauto; ins; desf; eauto.
  by rewrite res_plusC in *; exploit res_get_plus; eauto; ins; desf; eauto.
Qed.

Lemma res_get_rsum_at_iff :
   rl (D: rsum rl Rundef) l tau s,
    ( S',
       res_get (rsum rl) l = p_at tau S'
       In s (SL_list S'))
    ( r S,
       In r rl
       res_get r l = p_at tau S
       In s (SL_list S)).
Proof.
  induction rl; ins; try rewrite res_get_plus_at_iff, IHrl;
    try split; ins; desf; eauto 8.
  by destruct a; ins; desf.
Qed.

Lemma outgoing_atomic :
    acts amap sb rf mo sc L edge
     (CONS: Consistent acts amap sb rf mo sc)
     (ND: NoDup acts) E (ND' : NoDup E)
     (CC: compat amap sb rf L)
     (LR : label_restr acts amap sb rf L E) l tau S
     (G: res_get (L edge) l = p_at tau S) s
     (IN: In s (SL_list S)),
    S',
     res_get (outgoing acts L E (te_src edge)) l = p_at tau S'
     In s (SL_list S').
Proof.
  ins;
  assert (DEF := helper_out_def (te_src edge) CONS ND ND' CC LR).
  assert (AI: b, te_tgt edge = Some b In b acts).
    by intros; eapply lab_tgt_in_acts; eauto.
  assert (AI': sigma a, edge = TescS sigma a In sigma E).
    by ins; apply NNPP; intro; red in LR; desf; rewrite LRescS in G; vauto.

  unfold outgoing, out_esc, out_rf, out_sb in ×.
  rewrite !res_get_plus_at_iff, !res_get_rsum_at_iff;
    try (by intro X; rewrite X, ?res_plus_undef in *; ins).
  by destruct edge; ins; eauto 14 using in_map.
Qed.

Lemma vnode_atomic :
    acts M amap sb rf mo sc L edge
     (CONS: Consistent acts amap sb rf mo sc)
     (ND: NoDup acts) E (ND': NoDup E)
     (CC: compat amap sb rf L)
     (LR : label_restr acts amap sb rf L E) IE
     (V: valid_node IE acts M amap rf L E (te_src edge)) l tau S
     (G: res_get (L edge) l = p_at tau S) s
     (IN: In s (SL_list S))
     (NW: ¬ is_writeL (amap (te_src edge)) l ¬ is_release (amap (te_src edge))),
    S',
     res_get (incoming acts L (te_src edge)) l = p_at tau S'
     In s (SL_list S').
Proof.
  ins; red in V; desc.
  cut ( S',
         res_get (r +!+ out_esc acts L E (te_src edge)) l =
         p_at tau S' In s (SL_list S')).
    by clear - VG; red in VG; desf; rewrite VG, VG0.
  assert (DEF := helper_out_def (te_src edge) CONS ND ND' CC LR).
  assert (Y: S',
         res_get (outgoing acts L E (te_src edge)) l =
         p_at tau S' In s (SL_list S')).
    by eapply outgoing_atomic; eauto.
  unfold outgoing in *; red in VG.
  rewrite <- res_plusA in Y, DEF.
  rewrite res_get_plus_at_iff in *;
      try (by desf; intro X; rewrite X, ?res_plus_undef in *; ins); desf; eauto 10;
  left;
  revert GUAR VG0 NW Y Y0; clear;
  generalize (out_sb acts L (te_src edge)) as rsb;
  generalize (out_rf acts L (te_src edge)) as rrf; ins;

  red in GUAR; desf; revert NW; simpls; try case eqP; ins;
  unfold atomic_guar in *; desf;
  rewrite ?GUAR, ?GUAR0, ?GUAR1, ?res_plus_emp_r, ?VG0, ?REQ in *; ins; eauto;
  by destruct r; ins; desf; eauto; destruct (eqnP l l0); desf.
Qed.

Lemma visible_atomic2 :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (CC: compat amap sb rf L)
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a) te
    (PC: prefix_closed sb rf N) l tau S
    (G : res_get (L te) l = p_at tau S) s
    (IN: In s (SL_list S))
    (INn: In (te_src te) N),
   a,
    << MHB : may_happens_before amap sb rf a (te_src te) >>
    << WA : is_writeL (amap a) l >>
    << RELA: is_release (amap a) >>
     Sout,
    << Gout: res_get (out_rf acts L a) l = p_at tau Sout >>
    << Iout: get_state Sout = s >>
    << NEW : Sin (Gin: res_get (incoming acts L a) l = p_at tau Sin),
               ¬ In s (SL_list Sin) >>.
Proof.
  ins.
  revert S G IN; pattern te.
  eapply edge_depth_ind with (lab:=amap) (V:=N); eauto.
    by red in CONS; desc; intros ? ?; edestruct ACYC; eauto.
  clear te INn; ins; desf; unfold NW.
  destruct (classic (¬ (is_writeL (amap (te_src edge)) l is_release (amap (te_src edge))))); [|apply NNPP in H].
    exploit vnode_atomic; eauto using lab_tgt_in_acts; try tauto.
    intro Z; desf; eapply incoming_atomic in Z; eauto; desf.
    assert (K:=Z1); eapply IH in Z1; eauto using hb_one; desf;
    eexists; split; eauto 10.
    by eapply mhb_trans, mhbE; eauto using hb_one.
  destruct
    (classic ( Sin, res_get (incoming acts L (te_src edge)) l = p_at tau Sin)); desf.
    destruct (classic (In s (SL_list Sin))); desf.
      eapply incoming_atomic in H0; eauto; desf.
      assert (K:=H4); eapply IH in H4; desf; eauto using hb_one.
      by eexists; split; eauto 10; eapply mhb_trans, mhbE; eauto; right;
         eapply hb_one; eauto.
  { clear IH.
     (te_src edge); rewrite mhbE; repeat split; eauto.
    eapply outgoing_atomic in G; eauto; clear IN0; desf.

    specialize (V _ IN); red in V; desf.
    assert ( v, atomic_guar IE r l v (out_sb acts L (te_src edge))
                                        (out_rf acts L (te_src edge))).
      by red in GUAR; desf; ins; destruct (eqP l0 l); desf; eauto.
    assert (K:=VG); eapply vghost_get_at in K; eauto.
    unfold atomic_guar in *; desf; rewrite GET in *; desf.
    assert (In s (SL_list S'0)).
      eapply get_plus_at_oneD in G; eauto; desf; try rewrite G in *; desf.
      eapply get_plus_at_oneD in G; eauto; desf; try rewrite G in *; desf.
      rewrite res_plusC in VG; red in VG; desf.
      eapply res_get_plus with (r':=r) in G; desf; rewrite VG, VG0 in *; ins.
      by rewrite G in *; desf; rewrite SEQ; eauto.
    rewrite SEQ, H0 in *; desf; eexists; split; try edone; split; ins; desf; eauto.
    eapply get_state_eq_prove; ins; rewrite SEQ in *; desf; eauto using prot_trans_refl.
  }
  { clear IH.
     (te_src edge); rewrite mhbE; repeat split; eauto.
    eapply outgoing_atomic in G; eauto; clear IN0; desf.

    specialize (V _ IN); red in V; desf.
    assert ( v, atomic_guar IE r l v (out_sb acts L (te_src edge))
                                        (out_rf acts L (te_src edge))).
      by red in GUAR; desf; ins; destruct (eqP l0 l); desf; eauto.
    unfold atomic_guar in *; desf.
    rewrite Grf.
    eapply get_plus_at_oneD in G; eauto; desf; try rewrite G in *; desf; eauto.
      rewrite SEQ in *; ins; desf; eauto.
      eexists; split; ins; split; [|by ins; destruct H0; eauto].
      by eapply get_state_eq_prove; ins;
         rewrite SEQ in *; ins; desf; eauto using prot_trans_refl.
    eapply get_plus_at_oneD in G; eauto; desf; try rewrite G in *; desf; eauto.
      rewrite SEQ in *; ins; desf; eauto.
      eexists; split; ins; split; [|by ins; destruct H0; eauto].
      by eapply get_state_eq_prove; ins;
         rewrite SEQ in *; ins; desf; eauto using prot_trans_refl.
    rewrite res_plusC in VG; red in VG; desf.
    eapply res_get_plus with (r':=r) in G; desf; rewrite VG, VG0 in *; ins.
    by destruct H0; rewrite G in *; desf; eauto.
    assert (K:=VG); eapply vghost_get_back_at in K; eauto.
    destruct H0; rewrite K; eauto.
      eapply get_plus_at_oneD in G; eauto; desf; try rewrite G in *; desf; eauto.
      eapply get_plus_at_oneD in G; eauto; desf; try rewrite G in *; desf; eauto.
    rewrite res_plusC in VG; red in VG; desf.
    eapply res_get_plus with (r':=r) in G; desf; rewrite VG, VG0 in *; ins.
    by rewrite G in *; desf; eauto.
  }
Qed.

Lemma res_get_plus_back :
   r1 r2 l tau S
    (G : res_get (res_plus r1 r2) l = p_at tau S)
    (NBOT : res_get r1 l p_bot),
     S_pre,
      res_get r1 l = p_at tau S_pre
      ( x, In x (SL_list S_pre) In x (SL_list S)).
Proof.
  ins; destruct r1; ins; desf; ins; desf.
  inv_lplus l; rewrite G in *; destruct (pmap l); ins; desf; desf;
  eauto 7 using In_mk_slist, in_or_app.
Qed.

Lemma get_state_eq1 :
   acts L a r r'
    (VG : valid_ghost (incoming acts L a) (r +!+ r')) IE l0 v
    (G : atomic_guar IE r l0 v (out_sb acts L a) (out_rf acts L a))
    (LR: res_lt (res_strip (incoming acts L a)) r) l tau Sin
    (Gin : res_get (incoming acts L a) l = p_at tau Sin) Sout
    (Gout : res_get (out_rf acts L a) l = p_at tau Sout) s''
    (Iout : In s'' (SL_list Sout))
    (NIin : ¬ In s'' (SL_list Sin)),
  get_state Sout = s''.
Proof.
  ins; apply get_state_eq_prove; ins.
  exploit vghost_get_at; eauto; intro M.
  red in G; desc.
  destruct (res_get_plus _ _ (out_sb acts L a) Gout) as (?&A&?).
    by rewrite res_plusC, REQ; destruct r.
  rewrite res_plusC, REQ in A.
  destruct (eqP l l0); clarify.
    rewrite res_get_upds in A; desf; rewrite M, Grf in *; desf; try (by intro; desf).
    by rewrite SEQ in *; desf; eauto using prot_trans_refl.
  destruct r; ins; desf; ins; desf;
  by rewrite A in *; clarify; destruct NIin; eauto.
Qed.

Lemma get_state_eq2 :
   IE acts N amap rf L E a
         (V : valid_node IE acts N amap rf L E a) l tau Sin
         (Gin : res_get (incoming acts L a) l = p_at tau Sin) Sout
         (Gout : res_get (out_rf acts L a) l = p_at tau Sout) s''
         (Iout : In s'' (SL_list Sout))
         (NIin : ¬ In s'' (SL_list Sin)),
    get_state Sout = s''.
Proof.
  ins; red in V; desf.
  destruct (amap a); ins; desf; desf;
  try rewrite GUAR0 in *;
  try rewrite GUAR1 in *; ins;
  eapply get_state_eq1; eauto.
Qed.

Lemma visible_atomic :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (CC: compat amap sb rf L)
    (LR: label_restr acts amap sb rf L E) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) b (IN: pres_in sb rf b N) l tau S
    (IN: res_get (incoming acts L b) l = p_at tau S),
   a S',
    happens_before amap sb rf a b
    is_writeL (amap a) l is_release (amap a)
    res_get (out_rf acts L a) l = p_at tau S'
    slist_lt S S' slist_lt S' S.
Proof.
  ins; eapply incoming_atomic in IN0; eauto using get_state_in; desf.
  exploit visible_atomic2; eauto.
    eapply pres_in_hb; eauto.
    by eapply hb_one; eauto; intro X; rewrite X in ×.
  intro; desf.
  assert (happens_before amap sb rf a b).
    by eapply mhb_hb_trans; eauto; eapply hb_one; eauto; intro X; rewrite X in ×.
  eexists _, _; repeat (split; try edone); eauto; try rewrite slist_ltD;
    eauto using get_state_lt.
  rewrite Iout; eauto using prot_trans_refl.
  rewrite Iout; eauto using prot_trans_refl.
Qed.

Lemma visible_atomic2_cor :
   acts amap sb rf mo sc
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts) E (ND': NoDup E) L
    (CC: compat amap sb rf L) N M IE
    (V : a (IN: In a N), valid_node IE acts M amap rf L E a)
    (PC: prefix_closed sb rf N) b l tau S
    (G : res_get (incoming acts L b) l = p_at tau S) s
    (LR : label_restr acts amap sb rf L E)
    (IN: In s (SL_list S))
    (PI: pres_in sb rf b N),
   a Sout,
    << MHB : may_happens_before amap sb rf a b >>
    << AW : is_writeL (amap a) l >>
    << AREL: is_release (amap a) >>
    << Gout: res_get (out_rf acts L a) l = p_at tau Sout >>
    << Iout: get_state Sout = s >>
    << Va : valid_node IE acts M amap rf L E a >>
    << NEW : Sin (Gin: res_get (incoming acts L a) l = p_at tau Sin),
               ¬ In s (SL_list Sin) >>.
Proof.
  unfold incoming, NW; ins.
  repeat (first [eapply get_rsum_at_oneD in G|eapply get_plus_at_oneD in G];
          eauto; desf);
  repeat (rewrite in_map_iff in *; desf);
  (assert (happens_before amap sb rf x0 b);
    [by apply NNPP; intro X; edestruct nemp_of_get_at; eauto;
        apply LR; intro Y; destruct X; vauto|]);
  exploit visible_atomic2; eauto using prefix_closed_pres_in, pres_in_hb; ins; desf; eauto;
  do 8 try eexists; try edone; try eapply mhb_trans; eauto; rewrite ?mhbE; eauto;
  try (eapply V; rewrite mhbE in *; desf; eauto using pres_in_hb, hb_trans).
Qed.

Lemma exists_immediate_helper :
   b acts amap sb rf mo sc
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b::acts)) E (ND' : NoDup E) M L
    (CC: compat amap sb rf L)
    (LR : label_restr (b::acts) amap sb rf L E) IE
    (V : a (IN: In a acts), valid_node IE (b::acts) M amap rf L E a)
    (PC : prefix_closed sb rf acts)
    (PI : pres_in sb rf b acts) l tau S
    (GET : res_get (incoming (b :: acts) L b) l = p_at tau S)
    (CO: conform (b::acts) amap mo L acts)
    (WRI: is_writeL (amap b) l),
   a,
    << MO : immediate mo a b >>
    << Wa : is_writeL (amap a) l >>
    << RELa: is_release (amap a) >>
    << INa: In a acts >>.
Proof.
  unfold NW; ins.
  edestruct visible_atomic with (b:=b) (l:=l) as [c ?]; eauto; desf.
  red in CONS; desc; red in Cmo; desc.
  destruct exists_immediate with (r:=mo) (a:=c) (b:=b) (l:=b::acts)
    as (a & [N N'] & DISJ); eauto.
      by eapply Cmo3; eauto; rewrite H.
    intros ? X; eapply Cmo in X; ins; desf.
    by eapply (proj1 FIN); clear - X0; intro Y; rewrite Y in ×.
   a; split; ins.
  specialize (Cmo _ _ N); desc.
  assert (INa : In a acts).
    clear DISJ; exploit (proj1 FIN a); ins; desf;
    [by destruct (amap a)|by exfalso; eauto].
  assert (In c acts) by eauto using pres_in_hb.
  desf; eauto.
  assert (l0 = l) by (destruct (amap b); ins; desf); subst.
  repeat split; desf.
  eapply (CO l) in DISJ; eauto.
  eapply V in INa; red in INa; desf.
    by destruct (amap a); ins; desf; red in DISJ; desf; rewrite GUAR1 in ×.
  by destruct (amap c); ins; desf.
Qed.


This page has been generated by coqdoc