Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.

Local Open Scope string_scope.

Set Implicit Arguments.

Lemma outgoing_ext_one acts L EE b r :
  outgoing acts L EE b = res_emp →
  outgoing acts (upd L (TsbS b) (L (TsbS b) +!+ r)) EE b = r.
Proof.
  unfold outgoing, out_sb, out_rf, out_esc; rupd.
  rewrite !map_upd_irr; try (by intro; rewrite in_map_iff in *; desf).
  rewrite !res_plusA, (res_plusAC r); intros ->; apply res_plus_emp_r.
Qed.

Lemma rely_step :
  ∀ b acts (NIN: ¬ In b acts) amap sb rf mo sc L
    (PC : prefix_closed sb rf acts) IE EE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) acts amap rf L EE a)
    (CC: compat amap sb rf L)
    (CO: conform (b::acts) amap mo L acts)
    (ECO : ∀ sigma,
             exch_conform IE (b::acts) amap sb rf
                (upd L (TsbS b) (L (TsbS b) +!+ in_sb (b :: acts) L b))
                (upd L (TsbS b) (L (TsbS b) +!+ in_sb (b :: acts) L b)) EE sigma)
    (GAC: ghost_alloc_conform (b::acts)
                (upd L (TsbS b) (L (TsbS b) +!+ in_sb (b :: acts) L b)) EE)
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (INrf: in_rf (b::acts) L b = res_emp)
    (INesc: in_esc (b::acts) L b = res_emp)
    (INsb: in_sb (b :: acts) L b ≠ Rundef)
    (INsbOK: ∀ a, ¬ sb a b → L (Tsb a b) = res_emp)
    (OUT : outgoing (b::acts) L EE b = res_emp)
    (ND : NoDup (b ::acts))
    (ND' : NoDup EE)
    (LR : label_restr (b::acts) amap sb rf L EE),
  ∃ L',
    << V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L' EE a >> ∧
    << CC: compat amap sb rf L' >> ∧
    << CO: conform (b::acts) amap mo L' acts >> ∧
    << ECO : ∀ sigma, exch_conform IE (b::acts) amap sb rf
               (upd L' (TsbS b) (L' (TsbS b) +!+ in_sb (b :: acts) L' b +!+ in_rf (b :: acts) L' b))
               (upd L' (TsbS b) (L' (TsbS b) +!+ in_sb (b :: acts) L' b +!+ in_rf (b :: acts) L' b))
               EE sigma >> ∧
    << GAC: ghost_alloc_conform (b::acts)
               (upd L' (TsbS b)
                    (L' (TsbS b) +!+ in_sb (b :: acts) L' b
                        +!+ in_rf (b :: acts) L' b)) EE >> ∧
    << RELY: rely IE (in_sb (b::acts) L' b) (amap b)
                  (in_sb (b::acts) L' b +!+ in_rf (b::acts) L' b) >> ∧
    << INesc: in_esc (b::acts) L' b = res_emp >> ∧
    << OUT : outgoing (b::acts) L' EE b = res_emp >> ∧
    << Esb : ∀ a b, L' (Tsb a b) = L (Tsb a b) >> ∧
    << EsbS : ∀ a, L' (TsbS a) = L (TsbS a) >> ∧
    << LR : label_restr (b::acts) amap sb rf L' EE >>.
Proof.
  ins.
  assert (PI: pres_in sb rf b acts). {
    split; ins.
      assert (X := SB); apply (proj1 CONS), proj1 in SB; ins; desf.
      by exfalso; red in CONS; desf; edestruct ACYC; eauto using t_step.
    red in CONS; desc; red in FIN; desc.
    specialize (Crf b); desf; desf.
    exploit (CLOlab a); destruct (amap a); ins; desf;
      exfalso; edestruct ACYC; eauto using t_step.
  }

  unfold NW; case_eq (amap b); ins; desf.
   ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
   by ins; apply valid_node_ext_helper; try rewrite H; auto.

Case "Aalloc".
   ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
   by ins; apply valid_node_ext_helper; try rewrite H; auto.

   destruct (classic (typ = RATna)) as [|Nna]; desf.
Case "Aload RATna".
   ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
   by ins; apply valid_node_ext_helper; try rewrite H; auto.

   revert INsb; case_eq (in_sb (b :: acts) L b) as INsb; intros _.
   left; repeat eexists; ins.

   edestruct visible_na with (b:=b) (l:=l) (v:=v') as [b_rf ?]; eauto; desf.
     by unfold incoming; rewrite INsb, INrf, INesc, !res_plus_emp_r; vauto.
   assert (CONS':=CONS); red in CONS'; desc.
   specialize (Crf b); desf; desf.
   2: by edestruct Crf; eauto; instantiate; rewrite H.
   rewrite H in *; ins; desf.
   assert (X := Crf0); eapply is_write_weaken, OTH in X; ins.
   2: by apply PI in Heq.
   rewrite mhbE in *; desf; ins; [by destruct (amap b_rf); ins; desf|].
   edestruct Cwr; try eapply Heq; try eapply X; try eapply Cmo; eauto.
   by rewrite H; destruct (amap b_rf); ins; desf.

  rewrite mhbE; intro FHB; desf; try rewrite H in *; desf.
  pose proof (hb_in_acts2 CONS FHB); ins; desf.
    by edestruct ACYC; eauto.
  by destruct NIN; eauto using prefix_closed_hb.

   destruct (classic (typ = RATrlx)) as [|Nrlx]; desf.
Case "Aload RATrlx".
   ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
   by ins; apply valid_node_ext_helper; try rewrite H; auto.

   assert (ISACQ: is_acquire_rtyp typ) by (destruct typ; done).
Case "Aload ATat".
  destruct (rf b) as [b_rf|] eqn: RF.
  2: ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
     2: by ins; apply valid_node_ext_helper; try rewrite H; auto.
  2: right; right; split; [by destruct typ|].
  2: ∃ res_emp; rewrite res_strip_emp, res_plus_emp_r; split; eauto.
  2: ins; exfalso.
  2: edestruct visible_atomic with (b:=b) (l:=l) as [b_rf' ?]; eauto; desf.
     2: eby unfold incoming; rewrite INrf, INesc, !res_plus_emp_r.
  2: red in CONS; desc.
  2: by specialize (Crf b); rewrite RF in *; eapply Crf; eauto; rewrite H.

  assert (b_rf ≠ b) by (intro; desf; red in CONS; desc; edestruct ACYC; eauto using t_step).
  assert (INrf': In b_rf acts) by (by apply PI in RF).

  destruct (classic (¬ synchronizes_with amap rf b_rf b)) as [SW|SW]; [|apply NNPP in SW].
  {
    ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
      by ins; apply valid_node_ext_helper; try rewrite H; auto.
    right; right; split; [by destruct typ|].
    ∃ res_emp; rewrite res_strip_emp, res_plus_emp_r; split; eauto.
    ins; exfalso.
    edestruct visible_atomic with (b:=b) (l:=l) as [b_rf' ?]; eauto; desf.
      eby unfold incoming; rewrite INrf, INesc, !res_plus_emp_r.
    red in CONS; desc.
    destruct SW; red; rewrite H; repeat split; try done.
    destruct (classic (b_rf' = b_rf)); desf.
    red in Cmo; desc.
    specialize (Crf b); rewrite RF, H in *; ins; desf.
    edestruct (Cmo1 _ b_rf' H3 b_rf) as [MO|MO]; ins; eauto.
    2: by edestruct Cwr; eauto; instantiate;
          rewrite H; ins; destruct (amap b_rf').
    exploit (CO l0); try apply MO; eauto using pres_in_hb.
     by (destruct (amap b_rf'); ins; desf).
    rewrite H5; ins; desf; desf.
    specialize (V _ INrf'); red in V; desf.
    by destruct (amap b_rf); desf; ins; desf; desc; rewrite GUAR1 in ×.
  }

  ∃ (upd L (Trf b_rf b) (res_strip (out_rf (b :: acts) L b_rf))); ins.
  rewrite in_rf_upds; ins; eauto.
  unfold in_sb, in_esc, outgoing, out_sb, out_esc; ins.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  unfold in_rf; ins.
  repeat first [rewrite upds | rewrite updo; [|by intro; desf]].

  destruct (In_NoDup_Permutation _ INrf') as (? & P & ?); ins; desc; [by inv ND|].

  assert (DEF: in_sb (b :: acts) L b +!+ out_rf (b :: acts) L b_rf ≠ Rundef).
  {
    destruct (classic (∃ c, rf c = Some b_rf ∧ is_rmw (amap c) ∧ is_acquire (amap c) ∧ In c acts)) as [N|N]; desf.
  {
    replace (in_sb (b :: acts) L b) with
      (rsum (map L (map (Tsb^~ b) (filter (mydecf (sb^~ b)) acts)))).
    intro; apply (CC (Trf b_rf c :: map (Tsb^~ b) (filter (mydecf (sb^~ b)) acts))).
        constructor; ins; [by rewrite in_map_iff; intro; desf|].
        by eapply nodup_map; ins; try solve [by apply nodup_filter; inv ND|congruence].
      ins; desf; try rewrite in_map_iff in *; rewrite mhbE in *; desf; ins; desf;
      try rewrite filter_In in *; desf;
      try by red in CONS; desc; destruct (ACYC b_rf); eauto using clos_trans.
    by unfold mydecf in *; desf;
       eapply no_rf_rmw_overtaken with (a:=x0) (b:=b); eauto using hb_trans.
    by unfold mydecf in *; desf;
       eapply no_rf_rmw_overtaken with (a:=b0) (b:=b); eauto using hb_trans.
    by unfold mydecf in *; desf; red in CONS; desc;
       destruct (ACYC b0); eauto using clos_trans.
    by simpl; specialize (V _ INrf'); red in V; desf; rewrite res_plusC, VrfM.
    unfold in_sb; ins; rewrite INsbOK, res_plus_emp_l, rsum_map_map_filter; auto.
    by intro; red in CONS; desf; edestruct ACYC; eauto using t_step.
  }
  { intro; apply (CC (TrfS b_rf :: map (Tsb^~ b) acts)).
        constructor; ins; [by rewrite in_map_iff; intro; desf|].
        eapply nodup_map; ins; try solve [by inv ND|congruence].
      ins; desf; rewrite in_map_iff, mhbE in *; desf; ins; desf.
      by red in CONS; desc; destruct (ACYC b_rf); eauto using clos_trans.
     by apply NIN; clear - PC IN0 HB; red in PC; desf; induction HB as [? ? [|[]]|]; eauto.
    ins.
    rewrite res_plusC in H2; revert H2; unfold in_sb; ins.
    unfold outgoing, out_sb in OUT; rewrite !res_plusA, res_plusAC in OUT.
    rewrite (rsum_eq_empD _ (proj1 (res_plus_eq_empD _ _ OUT)) (L (Tsb b b))), res_plus_emp_l in *; vauto.
    by specialize (V _ INrf'); red in V; desf; rewrite <- VrfS in H2; ins; destruct N; eauto.
  }
  }

  do 10 try split; eauto.
    ins; apply valid_node_ext_helper; try rewrite H; auto.
    ins; assert (NEQ: a ≠ b) by congruence.
    specialize (V _ IN).
    unfold valid_node in *; ins; desf.
    eexists r; ins.
    rewrite !replace_out_rf; ins.
    unfold incoming, out_esc, out_sb, in_sb, in_rf, in_esc in *; ins.
    rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
    unfold NW.
    rewrite !updo; try (by intro X; desf); repeat split; ins.
    by rewrite updo; eauto; intro; desf; rewrite H in ×.
    eapply rsum_eq_empD in INrf; eauto.
    by apply in_map, in_map_iff; eauto using in_cons.

  red; ins.
  destruct (classic (In (Trf b_rf b) E)) as [Z|]; [|by rewrite map_upd_irr; eauto].
  intro K.
  exploit (CC (undup (TrfS b_rf :: E))); try done; intros.
    by rewrite ?in_undup_iff in *; ins; desf; eauto.
  specialize (V _ INrf'); red in V; desf.
  rewrite <- VrfS', replace_edge_emp in K; try apply helper2; ins.
  eapply rsum_eq_empD in INrf; eauto.
  by apply in_map, in_map_iff; eauto using in_cons.

  red; ins; exploit CO; try eapply MO; eauto.
  by rewrite !replace_out_rf; ins; try congruence;
    try (by eapply (rsum_eq_empD _ INrf), in_map, in_map_iff; eauto using in_cons).

  {
    assert (IS_EMP: L (Trf b_rf b) = res_emp).
      eapply rsum_eq_empD in INrf; eauto.
      by apply in_map, in_map_iff; eexists; vauto.
    change (L (Tsb b b) +!+ rsum (map L (map (Tsb^~ b) acts)))
      with (in_sb (b :: acts) L b).
    ins; rewrite updC; ins; eapply exch_conform_irr1; ins; eauto.
    rewrite updC with (l' := Trf b_rf b); ins.
    rewrite <- res_plusA.
    specialize (V _ INrf'); red in V; desc.
    pattern L at 5; rewrite <- (updI L (TrfS b_rf)).
    eapply exch_conform_upd3; ins; eauto.
    2: by rewrite IS_EMP, res_plus_emp_l.
    2: by rewrite IS_EMP, res_plus_emp_l, res_plus_emp_r,
                  <- VrfS', res_plus_strip_idemp.
    2: by rewrite outgoing_upd_in, OUT, res_plus_emp_l; ins;
          apply res_plus_strip_def.
    2: by rewrite outgoing_upd_in, OUT, res_plus_emp_l in M2;
          unfold incoming in M1; rewrite INrf, INesc, !res_plus_emp_r in M1.
    red; ins.
    unfold upd in ESC; desf; desf.
    apply res_escr_plusE in ESC; desf.
    × by destruct (ECO sigma (TsbS b)) as [a Z]; ins; rupd; ins; desc;
         ∃ a; revert Z; rupd; desf; eauto.
    × rewrite <- VrfS', res_escr_strip in ESC.
      destruct (ECO sigma (TrfS b_rf)) as [a Z]; ins; rupd; desc.
      ∃ a; revert Z; rupd; desf; eauto.
      by split; ins; left; eapply mhb_trans; eauto; apply rt_step; eauto.
    × by destruct (ECO sigma edge) as [a Z]; ins; rupd; desc;
         ∃ a; revert Z; rupd.
  }

  change (L (Tsb b b) +!+ rsum (map L (map (Tsb^~ b) acts)))
    with (in_sb (b :: acts) L b).
  assert (EQ: L (Trf b_rf b) = res_emp).
    by apply (rsum_eq_empD _ INrf), in_map, in_map_iff; eauto using in_cons.

  rewrite <- (updI L (TrfS b_rf)) at 1.
  eapply ghostalloc_upd3; eauto; ins; try rewrite EQ, res_plus_emp_l; eauto.
    rewrite res_plus_emp_r; specialize (V _ INrf'); red in V; desc.
    by rewrite <- VrfS', res_plus_strip_idemp.
  by rewrite res_plusA.
  by rewrite outgoing_upd_in, OUT, res_plus_emp_l; ins; apply res_plus_strip_def.

  right; right; split; try done; ∃ (out_rf (b :: acts) L b_rf); ins.
  change (L (Tsb b b) +!+ rsum (map L (map (Tsb^~ b) acts)))
    with (in_sb (b :: acts) L b).

  ins; desf.
  split; ins.

    edestruct visible_atomic with (b:=b) (l:=l) as [b_rf' ?]; eauto; desf.
      by unfold incoming; rewrite INrf, INesc, !res_plus_emp_r; eauto.
    red; unfold NW.
    destruct (classic (b_rf' = b_rf)); desf.

   rewrite H2, H6; repeat (first [∃ eq_refl | eexists]; try edone).

   specialize (V _ INrf'); red in V; desf.
   assert (is_writeLV (amap b_rf) l v).
     clear - RF CONS H; red in CONS; desc.
     by specialize (Crf b); rewrite RF, H in *; ins; desf.
   by destruct (amap b_rf); ins; desf;
     desc; (try by rewrite GUAR0 in *; ins);
     eauto using aguar_interp_prot.

    red in CONS; desc; red in Cmo; desc.
    specialize (Crf b); rewrite RF, H in *; ins; desf.
    edestruct (Cmo1 _ b_rf' H4 b_rf) as [MO|MO]; ins; eauto.
    2: by edestruct Cwr; eauto; instantiate;
          rewrite H; ins; destruct (amap b_rf').

    exploit (CO l0); try apply MO; eauto using pres_in_hb.
      by (destruct (amap b_rf'); ins; desf).

    rewrite H2, H6; ins.
    destruct (out_rf (b :: acts) L b_rf) eqn: Y; ins; destruct (pmap l0) eqn: Y'; ins; desf.
    repeat (eexists; eauto using slist_lt_trans).
    specialize (V _ INrf'); red in V; desf.
    destruct (amap b_rf); ins; desf; rewrite Y in *;
       desc; eauto using aguar_interp_prot.
     by unfold res_emp in *; desf.
    by unfold res_emp in *; desf.

  by eauto using res_plus_strip_def.

  by unfold out_rf; rewrite map_upd_irr, updo; ins; rewrite in_map_iff; intro; desf.

  by ins; rewrite updo.
  by ins; rewrite updo.

   destruct (classic (typ = WATna)) as [|Nna]; desf.
Case "Astore WATna".
   ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto); try done.
   by ins; apply valid_node_ext_helper; try rewrite H; auto.

   destruct (classic (typ = WATrlx)) as [|Nrlx]; desf.
Case "Astore WATrlx".
   ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto); try done.
   by ins; apply valid_node_ext_helper; try rewrite H; auto.

   assert (ISREL: is_release_wtyp typ) by (destruct typ; done).
Case "Astore ATat".
  ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
    by ins; apply valid_node_ext_helper; try rewrite H; auto.
  ins.
  exploit exists_immediate_helper; eauto.
     eby unfold incoming; rewrite INrf, INesc, !res_plus_emp_r.
    by rewrite H.
  intro Z; desf.

  desf; generalize (V _ INa); intro V'; red in V'; desf.
  assert (NEQ: a ≠ b) by congruence.
  assert (DEF: in_sb (b :: acts) L b +!+ L (TrfS a) ≠ Rundef).
    by eapply helper_plus_insb_rfS_def; eauto.

  assert (K := res_plus_get1 _ _ l DEF).
  unfold env_move, NW.

  assert (AG: ∃ v0, atomic_guar IE r l v0 (out_sb (b :: acts) L a)
                                            (out_rf (b :: acts) L a)).
    by red in GUAR; desf; desf; ins; desf; vauto.

  desf; generalize AG; red in AG; desc; intros; clear AG1.
  eexists _, (out_rf (b :: acts) L a); revert DEF K; rewrite H0, Grf in *;
  rewrite VrfS, Grf; try done; eauto using no_rmw_between.
  ins; desf; eexists _,_; repeat split; eauto using aguar_interp_prot.
  ∃ eq_refl; simpl.

  edestruct visible_atomic with (b:=b) (l:=l) as [c ?]; eauto; desf.
    eby unfold incoming; rewrite INrf, INesc, !res_plus_emp_r.
  destruct (eqP c a); [by subst; rewrite Grf in *; desf|].
  assert (In c acts).
    red in CONS; desf; ins; exploit (proj1 FIN c); ins; desf;
    [by destruct (amap c)|by exfalso; eauto].
  assert (MOca: mo c a).
    red in CONS; desc; red in Cmo; desc.
    edestruct (Cmo1 l); try eapply n; ins.
    exfalso; eapply MO; try edone; eapply Cmo3; eauto.
    by rewrite H.
  eapply (CO l) in MOca; eauto.
  by red in MOca; desf; desf; rewrite <- eq_rect_eq in *; eauto using slist_lt_trans.
  by destruct (amap c); ins; desf.

Case "Armw".
   destruct (rf b) as [b_rf|] eqn: RF.
   2: ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
     2: by ins; apply valid_node_ext_helper2; try congruence; auto.
   2: ∃ res_emp; rewrite res_plus_emp_r; split; eauto.
   2: ins; exfalso.
   2: edestruct visible_atomic with (b:=b) (l:=l) as [b_rf' ?]; eauto; desf.
      2: eby unfold incoming; rewrite INrf, INesc, !res_plus_emp_r.
   2: red in CONS; desc.
   2: by specialize (Crf b); rewrite RF in *; eapply Crf; eauto; rewrite H.

  assert (b_rf ≠ b) by (intro; desf; red in CONS; desc; edestruct ACYC; eauto using t_step).
  assert (INrf': In b_rf acts) by (by apply PI in RF).

  destruct (classic (¬ synchronizes_with amap rf b_rf b)) as [SW|SW]; [|apply NNPP in SW].
  {
    ∃ L; ins; rewrite INrf, res_plus_emp_r; repeat (split; eauto).
      ins.
      destruct (eqP a b_rf); desf;
       [|by apply valid_node_ext_helper2; try congruence; auto].
      specialize (V _ IN); red in V; red; unfold NW; desf.
      ∃ r; repeat (split; try done); ins; desf; eauto.
      unfold synchronizes_with in SW.
      rewrite H in *; ins.
      red in CONS; desc.
      specialize (Crf c); rewrite RF0 in *; desf.
      apply not_and_or in SW; desf.
      destruct (amap b_rf); ins; desf; desf; ins; desc; try (by destruct SW);
      by rewrite GUAR1; apply (rsum_eq_empD _ INrf), in_map, in_map_iff; eauto using in_cons.

    ∃ res_emp; rewrite res_plus_emp_r; split; eauto.
    ins; exfalso.
    edestruct visible_atomic with (b:=b) (l:=l) as [b_rf' ?]; eauto; desf.
      eby unfold incoming; rewrite INrf, INesc, !res_plus_emp_r.
    red in CONS; desc.
    destruct SW; red; rewrite H; repeat split; try done.
    destruct (classic (b_rf' = b_rf)); desf.
    red in Cmo; desc.
    specialize (Crf b); rewrite RF, H in *; ins; desf.
    edestruct (Cmo1 _ b_rf' H3 b_rf) as [MO|MO]; ins; eauto.
    2: by edestruct Cwr; eauto; instantiate;
          rewrite H; ins; destruct (amap b_rf').
    exploit (CO l0); try apply MO; eauto using pres_in_hb.
      by (destruct (amap b_rf'); ins; desf).
    rewrite H5; ins; desf; desf.
    specialize (V _ INrf'); red in V; desf.
    by destruct (amap b_rf); desf; ins; desf; desc; rewrite GUAR1 in ×.
  }

   assert (DEF: in_sb (b :: acts) L b +!+ L (TrfS b_rf) ≠ Rundef). {
     replace (in_sb (b :: acts) L b) with
       (rsum (map L (map (Tsb^~ b) (filter (mydecf (sb^~ b)) acts)))).
     unfold in_sb; rewrite res_plusC.
     intro; eapply (CC (TrfS b_rf :: map (Tsb^~ b) (filter (mydecf (sb^~ b)) acts))).
        constructor; [by rewrite in_map_iff; intro; desf|].
        by eapply nodup_map; try eapply nodup_filter; ins; try solve [by inv ND|congruence].
      by ins; desf; ins; try rewrite in_map_iff, mhbE in *; desf; ins; desf;
         try rewrite filter_In in *; desf; eauto using prefix_closed_hb.
      by ins; rewrite in_map_iff; intro; desf.
     unfold in_sb; ins; rewrite INsbOK, res_plus_emp_l, rsum_map_map_filter; auto.
     by intro; red in CONS; desc; edestruct ACYC; eauto using t_step.
   }

  assert (LrfS: L (TrfS b_rf) = out_rf (b :: acts) L b_rf).
    specialize (V _ INrf'); red in V; desf.
    eapply VrfS; ins.
    assert (b = c) by (by eapply no_rf_rmw_double; eauto; instantiate; try rewrite H).
    desf.

  ∃ (upd (upd L (TrfS b_rf) (res_strip (out_rf (b :: acts) L b_rf)))
                     (Trf b_rf b) (out_rf (b :: acts) L b_rf)).
  unfold outgoing, incoming, in_sb, in_esc, out_sb, out_esc; rupd.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  rewrite replace_out_rf2; ins; vauto.
  rewrite in_rf_upds; ins; eauto.
  2: by unfold in_rf; rewrite !map_upd_irr;
        try (by rewrite in_map_iff; intro; desf).

  split.
    intros; specialize (V _ IN); red in V; desf.
    ∃ r; unfold NW.
ins.
    rewrite replace_out_rf2; ins; vauto.
    unfold outgoing, incoming, in_sb, in_rf, in_esc, out_sb, out_esc.
    rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf).

    repeat (split; auto; try by rupd).
      ins; desf; rupd; eauto; congruence.
      ins; desf; rupd; eauto; intro; desf; eauto.
      by red in SW; desc; eapply (H1 b); eauto; rewrite H; ins.
    destruct (eqP a b_rf); desf; rupd; auto using res_strip_idemp; congruence.
  split.
    apply compat_upd2; ins; rewrite LrfS, <- ?res_plusA, ?res_plus_strip_l; vauto.
    by eexists; apply res_plus_strip_l.
  split.
    by red; ins; rewrite !replace_out_rf2; ins; eauto.
  split. {
    assert (IS_EMP: L (Trf b_rf b) = res_emp).
      eapply rsum_eq_empD in INrf; eauto.
      by apply in_map, in_map_iff; eexists; vauto.
    change (L (Tsb b b) +!+ rsum (map L (map (Tsb^~ b) acts))) with (in_sb (b :: acts) L b).
    ins; rewrite updC; ins; eapply exch_conform_irr1; ins; eauto.
    rewrite updC with (l' := Trf b_rf b); ins.
    rewrite <- res_plusA.
    eapply exch_conform_upd3; ins; eauto.
    2: by rewrite IS_EMP, res_plus_emp_l.
    2: by rewrite res_plusC, res_plusA, res_plus_strip_idemp, res_plusC, LrfS.
    2: by rewrite outgoing_upd_in, OUT, res_plus_emp_l; ins; congruence.
    2: by rewrite outgoing_upd_in, OUT, res_plus_emp_l in M2;
          unfold incoming in M1; rewrite INrf, INesc, !res_plus_emp_r in M1.
    red; ins.
    unfold upd in ESC; desf; desf.
    apply res_escr_plusE in ESC; desf.
    × by destruct (ECO sigma (TsbS b)) as [a Z]; ins; rupd; ins; desc;
         ∃ a; revert Z; rupd; desf; eauto.
    × rewrite <- LrfS in ESC.
      destruct (ECO sigma (TrfS b_rf)) as [a Z]; ins; rupd; desc;
      ∃ a; revert Z; rupd; desf; eauto.
      by split; ins; left; eapply mhb_trans; eauto; apply rt_step; eauto.
    × rewrite <- LrfS, res_escr_strip in ESC.
      by destruct (ECO sigma (TrfS b_rf)) as [a Z]; ins; rupd; desc;
         ∃ a; revert Z; rupd.
    × by destruct (ECO sigma edge) as [a Z]; ins; rupd; desc;
         ∃ a; revert Z; rupd.
  }
  split.

  change (L (Tsb b b) +!+ rsum (map L (map (Tsb^~ b) acts)))
    with (in_sb (b :: acts) L b).
  assert (EQ: L (Trf b_rf b) = res_emp).
    by apply (rsum_eq_empD _ INrf), in_map, in_map_iff; eauto using in_cons.

  eapply ghostalloc_upd3; eauto; ins; try rewrite EQ, res_plus_emp_l; eauto.
      by rewrite res_plus_emp_r, res_plus_strip_l.
    by rewrite res_plusA.
  by rewrite outgoing_upd_in, OUT, res_plus_emp_l; ins; congruence.

  split.
    ∃ (out_rf (b :: acts) L b_rf); repeat (split; ins).

    assert (is_writeLV (amap b_rf) l v).
      clear - H CONS RF; red in CONS; desc.
      by specialize (Crf b); rewrite RF in Crf; desf; rewrite H in *; ins; desf.

    rewrite LrfS in ×.

    edestruct visible_atomic with (b:=b) (l:=l) as [b_rf' ?]; eauto; desf.
      eby unfold incoming; rewrite INrf, INesc, !res_plus_emp_r.

    specialize (V _ INrf'); red in V; desf.
    generalize (proj1 (proj2 SW)).
    red; unfold NW.

    destruct (eqP b_rf' b_rf); desf.

    rewrite H1, H6.

  repeat (first [∃ eq_refl | eexists]; ins).
  generalize (proj1 (proj2 SW)).
  destruct (amap b_rf); ins; desf; desc; eauto using aguar_interp_prot.

  red in CONS; desc; red in Cmo; desc.
  eapply Cmo1 in n; eauto; desf.

  eapply CO in n; eauto using pres_in_hb.
  rewrite H6 in *; ins; desf; desf.
  rewrite H1.

  eexists _, _; repeat (first [split | ∃ eq_refl]; ins);
    eauto using slist_lt_trans.
  destruct (amap b_rf); ins; desf; desc; eauto using aguar_interp_prot.
    by destruct (amap b_rf'); ins; desf.

  eapply (Cwr _ _ H3) in n; ins.
  by destruct (amap b_rf'); try done; destruct (amap b); ins; desf.

  by rewrite <- LrfS.

  repeat (split; eauto using in_cons); ins; rupd.
Qed.

Lemma rely_compat_post :
  ∀ b acts amap sb rf
    (LAST: ∀ x, ¬ happens_before amap sb rf b x) L EE
    (LR : label_restr (b::acts) amap sb rf L EE)
    (CC: compat amap sb rf L)
    (ND : NoDup (b::acts))
    (OUT : outgoing (b::acts) L EE b = res_emp),
  compat amap sb rf
    (upd L (TsbS b)
         (L (TsbS b) +!+ in_sb (b::acts) L b +!+ in_rf (b::acts) L b)).
Proof.
  red; ins; destruct (classic (In (TsbS b) E)).
  2: by rewrite map_upd_irr; eauto.
  eapply In_NoDup_Permutation in H; desf.
  rewrite !(Permutation_rsum (Permutation_map _ H)); simpl; rupd.
  rewrite !map_upd_irr; try done.
  assert (NoDup l') by (eapply Permutation_nodup in H; eauto; inv H).
  intro; apply (CC (map (Tsb^~ b) (filter (mydecf (sb^~ b)) acts) ++
                    map (Trf^~ b) (filter (mydecf (synchronizes_with amap rf ^~ b)) acts) ++
                    filter (mydecf (fun te ⇒ (te_src te) ≠ b ∧ te_tgt te ≠ Some b
                                       )) l')).
   repeat rewrite nodup_app; repeat split; unfold disjoint; try done;
     try apply nodup_map; try apply nodup_filter; ins; try congruence;
     rewrite ?in_app_iff, ?in_map_iff, ?filter_In in *; unfold mydecf in *;
     desf; ins; desf; try tauto;
       try by inv ND.

  inv ND.
  intros; rewrite !in_app_iff, !in_map_iff, !filter_In in *; desf; ins; desf; eauto;
    rewrite ?filter_In in *; desf; unfold mydecf in *; desf; desf;
    try (eby edestruct LAST; eauto);
    try (solve [rewrite mhbE in *; desf; eby edestruct LAST; eauto]);
    try (rewrite mhbE in *; desf; try (eby edestruct LAST; eauto); []);
    try (solve [match goal with H : Permutation E (?x :: _) |- _ ⇒
                  eapply IND with (te := x); try edone;
                  eauto using Permutation_in, Permutation_sym, in_eq, in_cons;
                  eapply mhb_trans; vauto
                end]).
  eapply IND in HB; try edone;
    eauto using Permutation_in, Permutation_sym, in_eq, in_cons.

  inv ND; rewrite !map_app, !rsum_app.
  apply res_plus_eq_empD in OUT; desc.
  apply res_plus_eq_empD in OUT0; desc.
  apply res_plus_eq_empD in OUT1; desc.
  apply res_plus_eq_empD in OUT; desc; rewrite OUT, res_plus_emp_l in ×.
  apply res_plus_eq_empD in OUT0; desc.
  rewrite <- H2, res_plusA; unfold in_sb, in_rf; ins.
  rewrite (proj1 (res_plus_eq_empD _ _ OUT3)), res_plus_emp_l.
  rewrite (proj1 (res_plus_eq_empD _ _ OUT4)), res_plus_emp_l.
  f_equal; [|f_equal]; try apply rsum_map_map_filter;
    try apply rsum_map_filter; ins; try eby apply LR.
  apply not_and_or in H4; desf.
    apply NNPP; intro M; destruct H4; intro; desf; destruct M, x; ins;
    try by apply LR; ins; intro; edestruct LAST; eauto.
    destruct (classic (In sigma EE)); [|by apply LR; vauto].
    by eapply rsum_eq_empD, in_map, in_map_iff; eauto.

  destruct x; try (destruct (classic (In sigma EE)); [|by apply LR; vauto]);
    apply LR; ins; try intro; desf; destruct H4; vauto;
    try intro; desf; try (by edestruct LAST; eauto);
    try match goal with
      H : Permutation _ (?x :: _), H' : In ?y _ |- _ ⇒
        by eapply IND with (te := x) (te' := y); try edone;
          eauto using Permutation_in, Permutation_sym, in_eq, in_cons; vauto
    end.
Qed.