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

Local Open Scope string_scope.

Set Implicit Arguments.

Lemma conform_suff_immediate :
  ∀ b acts amap sb rf mo sc
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI: pres_in sb rf b acts) L IE EE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L EE a)
    (CO: conform (b::acts) amap mo L acts) r'
    (CC: compat amap sb rf (upd L (TsbS b) (L (TsbS b) +!+ r')))
    (NIN: ¬ In b acts) loc
    (Orf: rsum (map L (map (Trf b) (b::acts))) = res_emp)
    (LR : label_restr (b :: acts) amap sb rf L EE)
    (ND': NoDup EE)
    (LOC: is_atomic_writeL (amap b) loc)
    (HPL: res_get (incoming (b :: acts) L b) loc ≠ p_bot)
    (G : res_get r' loc ≠ p_bot) vb rsb r
    (MAG : atomic_guar IE r' loc vb rsb r)
    (PREV: ∀ a (IMM: immediate mo a b) (IN: In a acts)
      (AW: is_atomic_writeL (amap a) loc),
      prot_trans_ok (res_get (out_rf (b::acts) L a) loc) (res_get r loc))
    (GIMP: ∀ tau S
      (G1: res_get r loc = p_at tau S) S'
      (G2: res_get (L (TsbS b)) loc = p_at tau S'),
      slist_lt S' S),
  conform (b::acts) amap mo (upd L (TrfS b) r) (b::acts).
Proof.
  ins; assert (PREV': ∀ a (IN: In a acts) (MO: mo a b)
                    (AW: is_atomic_writeL (amap a) loc),
          prot_trans_ok (res_get (out_rf (b::acts) L a) loc) (res_get r loc)).
  {
    ins; red in CONS; desc; red in Cmo; desc.
    destruct exists_immediate with (r:=mo) (a:=a) (b:=b) (l:=b::acts)
      as (a' & IMM & DISJ); eauto.
      intros ? X; eapply Cmo in X; ins; desf.
      by eapply (proj1 FIN); clear - X0; intro Y; rewrite Y in ×.
    assert (IN': In a' acts).
      exploit (proj1 FIN a'); intro; desf; try eapply Cmo in DISJ; try rewrite H in *; ins; desf.
      by exfalso; destruct IMM; eauto.
    assert (W' : is_writeL (amap a') loc).
      by desf; eauto; eapply proj1, Cmo in IMM; desf; destruct (amap b); ins; desf; desf.
    desf; [|eapply prot_trans_ok_trans; [eapply CO|]]; try eapply (PREV a'); eauto.
    eapply CO in DISJ; eauto.
    specialize (V _ IN'); red in V; desc.
    destruct (amap a'); ins; desf; desc;
    rewrite GUAR1 in DISJ; clear - DISJ; red in DISJ; ins; desf.
  }
  clear PREV; red; ins; unfold out_rf; rewrite !map_upd_irr;
    try (by rewrite in_map_iff; intro; desf).
  ins; desf; desf; rupd; try congruence; try (eby eapply CO); rewrite ?Orf, ?res_plus_emp_r.
    by exfalso; red in CONS; desc; red in Cmo; desf; eauto.

  assert (loc = loc0) by (destruct (amap b0); ins; desf); subst.
  by eapply PREV'; eauto.


  assert (CONS' := CONS); red in CONS'; desc; red in Cmo; desc.
  assert (loc0 = loc) by (destruct (amap a); ins; desf; desf); subst.
  edestruct exists_immediate with (r:=(fun x y ⇒ mo y x)) (l:=a::acts)
    as (a' & [N N'] & DISJ); unfold transitive; eauto.
    intros ? _ X; eapply Cmo in X; desf.
    by eapply (proj1 FIN); clear - X0; intro Y; rewrite Y in ×.
  assert (IN': In a' acts).
    exploit (proj1 FIN a'); intro; desf; try eapply Cmo in DISJ; try rewrite H in *; ins; desf.
    by exfalso; eauto.
  assert (W' : is_writeL (amap a') loc).
    by desf; eauto; eapply Cmo in N; desf; destruct (amap a); ins; desf; desf.

  assert (ISREL: is_release (amap a')). {
    clear DISJ b0 INb Wb MO.
    assert (V' := V _ IN'); red in V'; desf.
    destruct (amap a'); ins; desf;
    exploit helper_plus_inc_sbS_back_def;
      eauto using in_eq, in_cons; ins.
    rewrite incoming_upd_irr, upds; ins.
    rewrite res_plusAC, res_plusC.
    replace (incoming (a :: acts) L a' +!+ r') with Rundef; try done.
    red in VG; desf; rewrite VG; ins; desf;
    destruct r0; ins; desf; inv_lplus loc;
    try rewrite GUAR2 in *; ins; desf; try rewrite <- H0 in *; ins; desf.

    rewrite incoming_upd_irr, upds; ins.
    rewrite res_plusAC, res_plusC.
    replace (incoming (a :: acts) L a' +!+ r') with Rundef; try done.
    red in VG; desf; rewrite VG; ins; desf;
    destruct r0; ins; desf; inv_lplus loc;
    rewrite GUAR2 in *; ins; desf; desf; rewrite <- H0 in *; ins; desf; desf.
  }

  assert (AW: is_atomic_writeL (amap a') loc).
    by destruct (amap a'); ins; desf.

  destruct (is_rmw (amap a')) eqn: RMW. {
    revert DISJ; specialize (Crf a'); desf.
    exploit Crmw; eauto; []; intros [? ?].
    intro; exfalso; destruct (eqP a a0) as [|NEQ]; revert DISJ; desf; [by apply PC in Heq|].
    edestruct (Cmo _ _ H) as (? & ? & ?).
    ins; desf; desf; destruct (amap a'); ins; desf; desf; subst;
      try by eapply Cmo1 in NEQ; desf; eauto.
    exfalso.
    assert (V' := V _ IN'); red in V'; desf.
    destruct (amap a'); ins; desf.
    eapply vghost_get_back_at in VG; eauto.
    clear PI;
    exploit visible_atomic; try solve [clear CC; edone]; eauto using compat_mon_upd.
      by red in PC; desf; split; ins; eauto.
    by intro; desf; eauto.
  }
  cut (prot_trans_ok (res_get r loc) (res_get (out_rf (a::acts) L a') loc)).
    by ins; desf; eapply prot_trans_ok_trans, CO; eauto.
  clear b0 DISJ INb MO Wb.
  assert (V' := V _ IN'); red in V'; desf.

  assert (DEF := helper_plus_inc_sbS_back_def _ _ CONS ND CC N (lr_upd_sbS _ _ LR (in_eq _ _))).
  rewrite incoming_upd_irr, upds in DEF; ins.

  clear AW.
  destruct (amap a') eqn: LEQ'; ins; desf; unfold atomic_guar in AG; desf.
    exfalso.
    exploit visible_uninit2; try solve [clear PI; eauto using vghost_get_back_uninit];
      eauto using prefix_closed_pres_in, compat_mon_upd.
    rewrite mhbE; intro; desf.
    by eapply Cmo3 in H; eauto; instantiate; rewrite LEQ'.
  exploit vghost_get_back_at; eauto; intro Gin; desf.

  revert MAG; intro.
  red in MAG; desf.
    destruct DEF.
    rewrite res_plusAC, res_plusC.
    destruct (incoming (a :: acts) L a'); ins; desf.
    exfalso; inv_lplus loc; ins.
    by red in VG; desf; unfold prot_plus in *; desf.

  assert (get_state S'0 = s0); subst.
    by eapply get_state_eq_prove; ins; rewrite SEQ0 in *;
       desf; eauto using prot_trans_refl.

  eapply WG; red; unfold NW; repeat (eexists; try edone).
  {
    intro X; apply DEF; unfold incoming.
    apply (f_equal (fun x ⇒ x +!+ L (TsbS a) +!+ in_esc (a :: acts) L a' +!+ rsb)) in X.
    revert X; simpl; rewrite !res_plusA, !(res_plusAC _ r), (res_plusC r), REQ0.
    rewrite !(res_plusAC _ (L (TsbS a))).
    rewrite <- !res_plusA; intro X; rewrite res_plusC in X |- ×.
    eapply plus_upd_def; eauto.
    ins; rewrite SEQ0 in *; desf; clear X.
    eapply get_plus_at_oneD in G'; eauto; desf.
    2: by edestruct GIMP as (?&?&?); eauto using get_state_lt, prot_trans_trans.

    rewrite res_plusA in G'.
    change (in_sb (a :: acts) L a' +!+
            in_rf (a :: acts) L a' +!+ in_esc (a :: acts) L a')
      with (incoming (a :: acts) L a') in ×.

    exploit visible_atomic2_cor; try solve [clear CC; eauto];
      eauto using prefix_closed_pres_in, compat_mon_upd.
    intro; desc; rewrite G' in *; desf.
    rewrite mhbE in *; desf; [by edestruct NEW; eauto|].

    right; destruct (classic (a = a0)) as [|NEQ]; desf.
      by destruct NIN; eauto using prefix_closed_hb.
    eapply Cmo1 in NEQ; eauto; desf.
      by exfalso; eapply Cmo3 in MHB; eauto; (try by rewrite LEQ').
    exploit (PREV' a0); eauto using prefix_closed_hb.
      by (destruct (amap a0); ins; desf).
    by rewrite Gout, Grf0, <- slist_ltD; ins; desf; rewrite <- eq_rect_eq in ×.
  }

  clear PI; exploit visible_atomic; unfold incoming; try solve [clear CC; eauto];
    eauto using compat_mon_upd.
    by red in PC; desf; split; ins; eauto.
  intro; desf; eauto.
  assert (NEQ: a0 ≠ a).
    by intro; desf; destruct NIN; eauto using prefix_closed_hb.
  assert (is_writeL (amap a') loc).
    clear - ATa N Cmo; apply Cmo in N; desf.
    by destruct (amap a); ins; desf; desf.
  eapply Cmo1 in NEQ; eauto; desf.
  2: by exfalso; eapply N' in NEQ; try eapply Cmo3; eauto.
  eapply PREV' in NEQ; eauto using prefix_closed_hb.
  unfold incoming in Gin; rewrite <- res_plusA in Gin.
  destruct (res_get_plus_back _ _ _ Gin) as (?&AA&?); try done.
  rewrite x3, AA, Grf0 in *; ins; desf.
  ∃ eq_refl; ins; eapply slist_lt_trans; eauto.
  by red; eauto.
  by (destruct (amap a0); ins; desf).
Qed.

Lemma vghost_get_back_at2 :
  ∀ r1 r r'
    (VG : valid_ghost r1 (r +!+ r')) l tau S
    (G : res_get r l = p_at tau S),
    ∃ S_pre,
      res_get r1 l = p_at tau S_pre.
Proof.
  ins; red in VG; desf.
  destruct r; ins; desf; ins; desf.
  inv_lplus l; rewrite G in *; destruct (pmap l); ins; desf; eauto.
Qed.

Lemma guar_sidecond :
  ∀ IE r l v r_sb r_rf
    (G : atomic_guar IE r l v r_sb r_rf)
    acts L b EE
    (VG : valid_ghost (incoming acts L b)
           (r +!+ out_esc acts L EE b))
    (RS : res_lt (res_strip (incoming acts L b)) r) tau S
    (G1 : res_get r_rf l = p_at tau S) S' sigma
    (G2 : res_get (L (TescS sigma b)) l = p_at tau S')
    (IN : In sigma EE)
    (ND : NoDup EE),
    slist_lt S' S.
Proof.
   ins; unfold out_esc in *; ins.
   eapply In_NoDup_Permutation in IN; desf.
   rewrite (Permutation_rsum (Permutation_map _ (Permutation_map _ IN))) in VG; ins.
   rewrite !res_plusA, res_plusAC in ×.
   exploit vghost_get_back_at2; eauto; intro X; desf.
   red in VG; desf.
   rewrite VG in *; ins.
   edestruct res_get_plus
     with (r':=r +!+ rsum (map L (map (TescS^~ b) l')) +!+ rsum (map L (map (Tesc b) acts)))
     as (?&?&?); eauto.
     congruence.
   rewrite VG0 in *; ins; rewrite X in *; desf.
   red in RS; desf.
   rewrite !res_plusA in ×.
   red in G; desf.
     destruct (L (TescS sigma b)); ins; desf.
     inv_lplus l; clear Heq2; ins.
     by rewrite X, GET in *; ins; desf.

   destruct (L (TescS sigma b)); ins; desf.
   inv_lplus l; clear Heq2; ins.
   rewrite X, G1, G2, GET in *; ins; desf.
   by clear - H0 SEQ; red; ins; eexists; try rewrite SEQ; eauto using prot_trans_refl.
   by clear - H0 SEQ Heq7; red; ins; eexists; try rewrite SEQ;
      eauto 7 using prot_trans_refl, In_mk_slist, in_or_app.
   by clear - H0 SEQ Heq7; red; ins; eexists; try rewrite SEQ;
      eauto 7 using prot_trans_refl, In_mk_slist, in_or_app.
   by clear - H0 SEQ Heq8; red; ins; eexists; try rewrite SEQ;
      eauto 7 using prot_trans_refl, In_mk_slist, in_or_app.
Qed.

Lemma res_lt_rf_in acts a b L :
  In a acts →
  NoDup acts →
  res_lt (L (Trf a b)) (incoming acts L b).
Proof.
  ins; unfold incoming, in_rf.
  eapply In_NoDup_Permutation in H; desf.
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ H))); ins.
  eauto using res_lt_plus_l, res_lt_plus_r, res_lt_refl.
Qed.

Lemma compat_atom_write :
  ∀ b acts amap sb rf mo sc
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (PC: prefix_closed sb rf acts)
    (ND: NoDup (b::acts)) l
    (AW: is_atomic_writeL (amap b) l) M L IE EE
    (V : ∀ a, In a acts → valid_node IE (b :: acts) M amap rf L EE a) r
    (CC : compat amap sb rf (upd L (TsbS b) r))
    (CO : conform (b :: acts) amap mo L acts)
    (VG : valid_ghost (incoming (b :: acts) L b)
                      (r +!+ out_esc (b :: acts) L EE b))
    (Orf : L (TrfS b) = res_emp)
    (Orf0 : rsum (map L (map (Trf b) (b::acts))) = res_emp)
    (Osb : L (TsbS b) = res_emp)
    (Osb0 : rsum (map L (map (Tsb b) (b::acts))) = res_emp)
    (LR : label_restr (b :: acts) amap sb rf L EE)
    (ND': NoDup EE)
    tau s S' r_sb r_rf
    (REQ : r_sb +!+ r_rf = res_upd r l (p_at tau S'))
    (Gsb : res_get r_sb l = p_at tau S')
    (Grf : res_get r_rf l = p_at tau S')
    S (GET : res_get r l = p_at tau S)
    v (AG : atomic_guar IE r l v r_sb r_rf)
    (LT: res_lt (res_strip (incoming (b :: acts) L b)) r)
    (LAST : ∀ s0, In s0 (SL_list S) → prot_trans tau s0 s)
    (SEQ : ∀ s0, In s0 (SL_list S') ↔ s0 = s ∨ In s0 (SL_list S))
    (CO' : conform (b :: acts) amap mo (upd L (TrfS b) r_rf) (b :: acts)),
    compat amap sb rf (upd L (TsbS b) (res_upd r l (p_at tau S'))).
Proof.
  repeat red; ins; eapply CC; eauto.
  revert H.
  destruct (classic (In (TsbS b) E)) as [N|N];
   [apply In_NoDup_Permutation in N; desf;
    rewrite !(Permutation_rsum (Permutation_map _ N)); simpls |];
  rewrite !map_upd_irr; rupd; ins.
  eapply plus_upd_def; eauto.
  intros.

  rewrite SEQ in *; desf.
  eapply get_rsum_at_oneD in G'; eauto; desf.
  rewrite in_map_iff in *; desf.
  assert (get_state S' = s); subst.
    by apply get_state_eq_prove; ins; rewrite SEQ in *; desf; eauto using prot_trans_refl.

  assert (IN' : In (te_src x) (b :: acts)).
    by eapply lab_src_in_acts; eauto.

  simpls; desf.
  revert G'0; intro.
  {
    assert (K:=VG); eapply vghost_get_back_at in K; eauto.

    destruct x; ins.
    rewrite (rsum_eq_empD (_ :: _) Osb0 (L (Tsb a b))) in G'0; try done.
    eapply (in_map L (_ :: _)), (in_map (Tsb a) (_ :: _)).
    by eapply lab_tgt_in_acts; eauto.

    rewrite (rsum_eq_empD (_ :: _) Orf0 (L (Trf a b))) in G'0; try done.
    eapply (in_map L (_ :: _)), (in_map (Trf a) (_ :: _)).
    by eapply lab_tgt_in_acts; eauto.

    by ins; rewrite Orf in G'0.

    cut (L (Tesc a b) = res_emp); [by intro XX; rewrite XX in *; ins|].
    apply LR; intro HB.
    destruct (hb_in_acts2 CONS HB); desf.
      by red in CONS; desc; edestruct ACYC; eauto.
    by inv ND; eauto using prefix_closed_hb.

    exploit guar_sidecond; eauto.
      by apply NNPP; intro; red in LR; desc; rewrite LRescS in G'0; vauto.
    by intro; desf; right; eauto using prot_trans_trans, get_state_lt.
  }

  exploit visible_atomic2; try solve [clear CC; eauto]; eauto.
    eby eapply compat_mon_upd with (a := TsbS b); ins; rewrite Osb, res_plus_emp_l.
  intro; desf.
  destruct (eqP a b) as [|NEQ]; desf.
    by unfold out_rf in *; ins; rewrite Orf, Orf0, res_plus_emp_r in *; ins.
  assert (IN: In a (b::acts)).
    by rewrite mhbE in *; ins; desf; eauto using prefix_closed_hb, pres_in_hb.
  clear IN'; ins; desf.
  assert (MO:=NEQ).
  red in CONS; desc; red in Cmo; desc; eapply Cmo1 in MO; eauto; try by rewrite LEQ.
  desf.
    eapply CO' in MO; eauto using in_eq, in_cons; try (by rewrite LEQ).
    unfold out_rf in *; revert MO; simpls; rupd; try congruence.
    rewrite !map_upd_irr, Gout, Orf0, res_plus_emp_r, Grf;
      try (by rewrite in_map_iff; intro; desf); ins; desf;
    rewrite <- eq_rect_eq in ×.
    by rewrite slist_ltD in *; eauto.
    by destruct (amap a); ins; desf.
  eapply CO' in MO; eauto using in_eq, in_cons; try (by rewrite LEQ; ins; desf; desf).
  unfold out_rf in *; revert MO; simpls; rupd; try congruence.
  rewrite !map_upd_irr, Gout, Orf0, res_plus_emp_r, Grf;
    try (by rewrite in_map_iff; intro; desf); ins; desf.
    rewrite <- eq_rect_eq in ×.
    by rewrite slist_ltD in *; eauto.
Qed.

Lemma vghost_get_bot r1 r r' l :
  valid_ghost r1 (r +!+ r') →
  res_get r1 l = p_bot →
  res_get r l = p_bot.
Proof.
  unfold valid_ghost; ins; desf; destruct r; ins; desf.
  inv_lplus l; ins; unfold prot_plus in *; desf; congruence.
Qed.

Lemma res_escr_atomic_guar IE r l v r_sb r_rf sigma :
  atomic_guar IE r l v r_sb r_rf →
  r ≠ Rundef →
  res_escr r_sb sigma ∨ res_escr r_rf sigma →
  res_escr r sigma.
Proof.
  unfold atomic_guar; ins; desc; clear H3.
  destruct r_sb, r_rf, r; ins; desf; apply orbT.
Qed.


Lemma guar_step :
  ∀ b acts (NIN: ¬ In b acts) amap sb rf mo sc r
    (CONS: Consistent (b :: acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI: pres_in sb rf b acts) IE r_pre r_sb r_rf
    (G: guar IE r_pre r (amap b) r_sb r_rf) L
    (RPRE: r_pre = in_sb (b::acts) L b +!+ in_rf (b::acts) L b) r_pre_sb
    (RELY: rely IE r_pre_sb (amap b) r_pre) EE
    (V : ∀ a (IN: In a acts), valid_node IE (b::acts) (b::acts) amap rf L EE a)
    (CC: compat amap sb rf (upd L (TsbS b) (L (TsbS b) +!+ r)))
    (ECO: ∀ sigma,
            exch_conform IE (b::acts) amap sb rf
                         (upd L (TsbS b) (L (TsbS b) +!+ r))
                         (upd L (TsbS b) (L (TsbS b) +!+ r)) EE sigma)
    (CO: conform (b::acts) amap mo L acts)
    (GAC: ghost_alloc_conform (b::acts)
                (upd L (TsbS b) (L (TsbS b) +!+ r)) EE)
    (VG: valid_ghost (incoming (b::acts) L b)
                     (r +!+ out_esc (b::acts) L EE b))
    
    (Orf: out_rf (b::acts) L b = res_emp)
    (Osb: out_sb (b::acts) L b = res_emp)
    (RS: res_lt (res_strip (incoming (b::acts) L b)) r)
    
    (LR : label_restr (b :: acts) amap sb rf L EE)
    (ND': NoDup EE)
    (WPE: pre_write_prot_equiv IE acts amap mo L b r_pre (incoming (b::acts) L b)),
  ∃ L',
    << V : ∀ a (IN: In a (b::acts)), valid_node IE (b::acts) (b::acts) amap rf L' EE a >> ∧
    << CC: compat amap sb rf L' >> ∧
    << ECO: ∀ sigma, exch_conform IE (b::acts) amap sb rf L' L' EE sigma >> ∧
    << CO: conform (b::acts) amap mo L' (b :: acts) >> ∧
    << GAC: ghost_alloc_conform (b::acts) L' EE >> ∧
    << EsbS: ∀ a, a ≠ b → L' (TsbS a) = L (TsbS a) >> ∧
    << EsbS': L' (TsbS b) = r_sb >> ∧
    << LR : label_restr (b :: acts) amap sb rf L' EE >>.
Proof.
  intros; unfold NW.
  apply res_plus_eq_empD in Orf; desc.
  apply res_plus_eq_empD in Osb; desc.
  assert (NRF: ∀ c, ¬ rf c = Some b).
    intros c RF; red in CONS; desc.
    specialize (Crf c); rewrite RF in *; desc.
    destruct (proj1 FIN c); desf.
      by intro X; rewrite X in ×.
     by eapply ACYC; eauto using t_step.
    by eapply PC in RF.
  assert (NSW: ∀ c, ¬ synchronizes_with amap rf b c).
    eby unfold synchronizes_with; red; ins; desc; edestruct NRF.
  assert (LRF: L (Trf b b) = res_emp) by (apply LR; done).
  destruct (amap b) eqn: LEQ; ins; desc; clarify.

Case "Askip".
  rewrite Osb, res_plus_emp_l in ×.

  ∃ (upd L (TsbS b) r); repeat (split; eauto using in_eq, upds, compat_guar1); ins;
    rupd; desc; try congruence.
  destruct IN; clarify; [|by apply valid_node_upd_irr; eauto; intro; desf].

  red; unfold NW; eexists r; rewrite LEQ; rupd; repeat (split; ins; rupd; try edone);
  unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in *;
  rewrite ?map_upd_irr, ?escr_ffun_upd_irr; rupd; try done;
    try (by rewrite in_map_iff; intro; desf);
    try (by ins; rewrite ?Osb0, ?Orf, ?Orf0, ?res_plus_emp_r; try done; apply LR).

  by eapply conform_upd_irr, conform_ext_irr; eauto; rewrite LEQ; ins.

Case "Aalloc".
  rewrite Osb, res_plus_emp_l in ×.

  assert (V': ∀ a (IN: b = a ∨ In a acts),
    valid_node IE (b :: acts) (b :: acts) amap rf
      (upd L (TsbS b) (res_mupd r l n p_uninit)) EE a).
  {
    ins; destruct IN; clarify; [|by apply valid_node_upd_irr; eauto; intro; desf].
    red; unfold NW; eexists r; rewrite LEQ; rupd; repeat (split; ins; rupd; try edone);
    unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in *;
    rewrite ?map_upd_irr, ?escr_ffun_upd_irr; rupd; try done;
    try (by rewrite in_map_iff; intro; desf);
    try (by ins; rewrite ?Osb0, ?Orf, ?Orf0, ?res_plus_emp_r; try done; apply LR).
  }

  assert (CC': compat amap sb rf (upd L (TsbS b) (res_mupd r l n p_uninit))).
  { red; ins; intro.
    eapply CC; eauto; revert H.
    destruct (classic (In (TsbS b) E)) as [P|];
      [eapply In_NoDup_Permutation in P; desc; clarify;
       rewrite !(Permutation_rsum (Permutation_map _ P)); try done |]; simpl;
      rewrite !map_upd_irr; try done; rupd; eauto.
      intro; apply NNPP; intro.
      assert (BOT: ∀ loc, l ≤ loc ≤ l + n → res_get (r +!+ rsum (map L l')) loc = p_bot).
      {
        ins; rewrite res_get_plus_bot, res_get_rsum_bot; try kundef.
        red in WPE; rewrite LEQ in WPE; specialize (WPE _ H1).
        split; eauto using vghost_get_bot.
        ins; rewrite in_map_iff in *; desf.
        apply NNPP; intro M.
        assert (INx: In (te_src x) (b :: acts)).
          by eapply lab_src_in_acts; eauto.
        edestruct visible_allocation_one with (N := b::acts) (te:=x)
          (L := upd L (TsbS b) (res_mupd r l n p_uninit)) (l:=loc);
          eauto using Consistent_prefix_closed, in_eq; desf.
          by rupd; intro; desf.

        assert (AA: L x ≠ res_emp) by (intro AA; rewrite AA in *; simpls).
        assert (BB := lab_tgt_in_acts CONS LR _ AA); clear AA.
        red in CONS; desc; destruct (Ca _ _ _ H5 _ _ _ LEQ); clarify; try omega.
        ins; desf.
          clear - Orf Orf0 Osb Osb0 WPE M VG BB LR.
          assert (r +!+ out_esc (te_src x :: acts) L EE (te_src x) ≠ Rundef).
            by red in VG; desf; congruence.
          rewrite res_plusC in VG; eapply vghost_get_bot in VG; eauto; unfold out_esc in ×.
          (apply res_get_plus_bot in VG; desc; try kundef).
          destruct M, x; ins; rewrite ?Orf, ?Osb, ?Osb0; ins; try specialize (BB _ eq_refl).
          by erewrite rsum_eq_empD with (l := L (Tsb a a) :: _) (r := L (Tsb a b)); eauto;
             desf; ins; eauto using in_map.
          by erewrite rsum_eq_empD with (l := L (Trf a a) :: _) (r := L (Trf a b)); eauto;
             desf; ins; eauto using in_map.
          by eapply res_get_rsum_bot with (rl := _ :: _); eauto; ins; try kundef;
             desf; ins; eauto using in_map.
          destruct (classic (In sigma EE)).
            by eapply res_get_rsum_bot; eauto; ins; try kundef;
               apply in_map; apply in_map_iff; eauto.
          by red in LR; desc; rewrite LRescS; eauto.
        by rewrite mhbE in *; destruct NIN; desf; eauto using prefix_closed_hb.
     }
     clear - BOT H H0.
     destruct r; ins; desf.
     eapply lift_plus_none_inv in Heq2; desc; inv_lplus l0; ins; desf; try congruence.
     desf; rewrite BOT in Heq0; auto; clear - Heq0 Heq2.
     by unfold prot_plus in *; simpls; desf.
  }

  ∃ (upd L (TsbS b) (res_mupd r l n p_uninit));
    repeat (split; eauto using in_eq, upds, compat_guar1); ins;
    rupd; desc; try congruence.

  eapply exch_conform_helper1 with (r:=r); ins; eauto using helper_out_def, in_eq.
    red; ins; destruct (ECO sigma edge) as (a' & M & M'); ins.
      by revert ESC; unfold upd; desf; rewrite ?res_escr_mupd.
    by ∃ a'; split; ins; revert M; rupd.
  by destruct r.

  by eapply conform_upd_irr, conform_ext_irr; eauto; rewrite LEQ; ins.

  eapply ghost_alloc_conform_helper1; eauto using helper_out_def, in_eq.
  by destruct r.

clear RELY; desf; rewrite Osb, res_plus_emp_l in ×.
Case "Aload ATna".

  ∃ (upd L (TsbS b) r); repeat (split; eauto using in_eq, upds, compat_guar1); ins;
    rupd; desc; try congruence.
  destruct IN; clarify; [|by apply valid_node_upd_irr; eauto; intro; desf].

  red; unfold NW; eexists r; rewrite LEQ; rupd; repeat (split; ins; rupd; try edone);
  unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in *;
  rewrite ?map_upd_irr, ?escr_ffun_upd_irr; rupd; eauto;
    try (by rewrite in_map_iff; intro; desf);
    try (by ins; rewrite ?Osb0, ?Orf, ?Orf0, ?res_plus_emp_r; try done; apply LR).

  by eapply conform_upd_irr, conform_ext_irr; eauto; rewrite LEQ; ins.

Case "Aload ATat".

  ∃ (upd L (TsbS b) r); repeat (split; eauto using in_eq, upds, compat_guar1); ins;
    rupd; desc; try congruence.
  destruct IN; clarify; [|by apply valid_node_upd_irr; eauto; intro; desf].

  red; unfold NW; eexists r; rewrite LEQ; rupd; repeat (split; ins; rupd; try edone);
  unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in *;
  rewrite ?map_upd_irr, ?escr_ffun_upd_irr; rupd; vauto;
    try (by rewrite in_map_iff; intro; desf);
    try (by ins; rewrite ?Osb0, ?Orf, ?Orf0, ?res_plus_emp_r; try done; apply LR); eauto.

  by eapply conform_upd_irr, conform_ext_irr; eauto; rewrite LEQ; ins.

destruct G as [G|G]; desc.
Case "Astore ATna".
  rewrite Osb, res_plus_emp_l in ×.

  assert (CC': compat amap sb rf (upd L (TsbS b) r_sb)).
    by subst; eapply compat_guar2; eauto.

  ∃ (upd L (TsbS b) r_sb); repeat (split; eauto using in_eq, upds, compat_guar1); ins;
    rupd; desc; try congruence.
  destruct IN; clarify; [|by apply valid_node_upd_irr; eauto; intro; desf].

  red; unfold NW; eexists r; rewrite LEQ; rupd; repeat (split; ins; rupd; try edone); try left;
  unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in *;
  rewrite ?map_upd_irr, ?escr_ffun_upd_irr; rupd; try done;
    try (by rewrite in_map_iff; intro; desf);
    try (by ins; rewrite ?Osb0, ?Orf, ?Orf0, ?res_plus_emp_r; try done; apply LR).

  subst; eapply exch_conform_helper1 with (r:=r); ins; eauto using helper_out_def, in_eq.
    red; ins; destruct (ECO sigma edge) as (a' & M & M'); ins.
      by revert ESC; unfold upd; desf; rewrite ?res_escr_upd.
    by ∃ a'; split; ins; revert M; rupd.
  by destruct r.

  apply conform_upd_irr; red; ins.
  destruct INa as [|INa]; clarify; [by rewrite LEQ in *|].
  destruct INb; clarify; eauto.
  assert (l = loc); subst.
    red in CONS; desc; clear G2; eapply (proj1 Cmo) in MO; desc.
    by rewrite LEQ in *; ins; desf; destruct (amap a); ins; desf.
  edestruct (CC (TrfS a :: TsbS b0 :: nil)).
    by repeat constructor; ins; intro; desf.
   by clear; intros ? _; ins; desf.
  simpl; rupd.

  eapply V in INa; red in INa; desc.
  rewrite !(res_plusAC r), <- (res_plus_strip_l (L (TrfS a))).
  rewrite res_plusA, <- res_plusA, VrfS'.
  replace (r +!+ res_strip (out_rf (b0 :: acts) L a)) with Rundef; ins.
  revert G2; clear - GUAR ATa.
  destruct (amap a); simpls; desf; desf;
  red in AG; desc; clarify;
  clear - Grf; destruct r, (out_rf (b0 :: acts) L a); simpl; desf; ins;
  inv_lplus loc; rewrite prot_plusC, Grf in *; ins; desf; ins.

  eapply ghost_alloc_conform_helper1; eauto using helper_out_def, in_eq.
  by subst; destruct r.

Case "Astore ATat".

  ∃ (upd (upd L (TrfS b) r_rf) (TsbS b) r_sb); split; ins;
    rupd; desc; try congruence.

  destruct IN; clarify; [|by repeat apply valid_node_upd_irr; eauto; intro; desf].

  red; unfold NW; eexists r; rewrite LEQ; rupd; repeat (split; ins; rupd; try edone);
    try right; repeat (split; ins; rupd; try edone);
  unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in *;
  rewrite ?map_upd_irr, ?escr_ffun_upd_irr in *; rupd; try done;
    try (by rewrite in_map_iff; intro; desf);
    try (by ins; rewrite ?Osb0, ?Orf, ?Orf0, ?res_plus_emp_r; try done; apply LR).

  eby edestruct NRF.

  assert (CO': conform (b :: acts) amap mo (upd L (TrfS b) r_rf) (b :: acts)).
  {
    eapply conform_suff_immediate; eauto.
      by destruct (amap b); ins; desf.
      by intro; eapply vghost_get_bot in VG; eauto; red in AG; desf; desf; congruence.
      by red in AG; desf; congruence.
      2: by rewrite Osb in ×.
    red in WPE; rewrite LEQ in WPE.
    ins; red in AG; desf.
      exploit visible_uninit; eauto using vghost_get_back_uninit, compat_mon_upd.
      rewrite mhbE; intro; desf.
      red in CONS; desc; red in Cmo; desc.
      exfalso; red in IMM; desc.
      by eapply Cmo2, Cmo0, Cmo3; eauto; instantiate; rewrite LEQ.
    exploit WPE; clear WPE; eauto using vghost_get_back_at.
    intro WPE; desf.
    assert (a0 = a); desf; eauto.
    destruct (eqP a0 a); desf.
    by exfalso; red in CONS; desc; eapply Cmo in n; unfold immediate in *; desf; eauto.
  }

  rewrite Osb, res_plus_emp_l in ×.

  assert (CC': compat amap sb rf (upd L (TsbS b) (r_sb +!+ r_rf))).
    assert (AG':=AG); red in AG; desc; rewrite REQ; desf.
      by eapply compat_guar2; eauto.
    by eapply compat_atom_write; eauto; rewrite LEQ; ins; desf.

  repeat (split; eauto using in_eq, upds, compat_guar1, conform_upd_irr); ins;
    rupd; desc; try congruence.
  rewrite updC; ins; eapply compat_upd2_acc with (r := r_rf); eauto; ins.
  by replace (L (TrfS b)) with res_emp; eauto using res_plus_emp_l.

  assert (r ≠ Rundef) by (intro X; rewrite X in *; red in VG; desf).
  eapply exch_conform_upd2_acc with (r := r_rf); ins.
  2: by rewrite Orf, res_plus_emp_l.
  subst; eapply exch_conform_helper1 with (r:=r); ins; eauto using helper_out_def, in_eq.
  2: by revert GNA; clear - AG; red in AG; desc; rewrite REQ; destruct r.
  red; ins;
  destruct (ECO sigma (if excluded_middle_informative (edge = TrfS b) then TsbS b else edge))
    as (a' & M & M'); ins.
        by desf.
      by revert ESC; unfold upd; desf; eauto using res_escr_atomic_guar.
    ∃ a'; split; ins; revert M; rupd.
  by desf; ins; eauto.

  eapply ghostalloc_upd2_acc with (r := r_rf); ins.
  2: by rewrite Orf, res_plus_emp_l.
  eapply ghost_alloc_conform_helper1; eauto using helper_out_def, in_eq.
  by clear - AG; red in AG; desc; rewrite REQ; destruct r.

Case "Armw".

  ∃ (upd (upd L (TrfS b) r_rf) (TsbS b) r_sb).

  assert (CO': conform (b :: acts) amap mo (upd L (TrfS b) r_rf) (b :: acts)).
  {
    eapply conform_suff_immediate; eauto.
      by rewrite LEQ; ins.
      by intro; eapply vghost_get_bot in VG; eauto; red in AG; desf; desf; congruence.
      by red in AG; desf; congruence.
      2: by rewrite Osb.

    ins; red in AG; desf.
      exploit visible_uninit; eauto using vghost_get_back_uninit, compat_mon_upd.
      rewrite mhbE; intro; desf.
      red in CONS; desc; red in Cmo; desc.
      exfalso; red in IMM; desc.
      by eapply Cmo2, Cmo0, Cmo3; eauto; instantiate; rewrite LEQ.

    eapply prot_trans_ok_trans with (res_get r l).
    2: rewrite GET, Grf; ∃ eq_refl; ins.
    2: by eexists; rewrite SEQ; eauto.

    assert (RF: rf b = Some a).
      edestruct visible_atomic with (l:=l); try solve [clear CC; eauto];
        eauto using vghost_get_back_at, compat_mon_upd; desf.
      clear - H H0 CONS LEQ IMM AW.
      red in CONS; desc; specialize (Crf b); desf; ins; desf.
      2: by edestruct Crf; eauto; rewrite LEQ; ins.
      rewrite LEQ in *; ins; desf.
      exploit Crmw; eauto; instantiate; try rewrite LEQ; try done; intros IMM'.
      destruct (eqP a0 a) as [|NEQ]; desf.
      by eapply Cmo in NEQ; eauto; desf; exfalso; unfold immediate in *; desc; eauto.

    specialize (V a IN); red in V; desc.
    assert (OG: ∃ tau S, res_get (out_rf (b :: acts) L a) l = p_at tau S).
      by clear - GUAR AW; destruct (amap a); ins; desf; desf; try red in AG; desf; eauto.
    desf; revert OG.
    rewrite <- VrfM with (c:=b); eauto using in_eq; try (by rewrite LEQ).
    intro; rewrite OG, GET.
    edestruct res_lt_rf_in with (L:=L) (a:=a) (b:=b) (acts:=b::acts) as (rrr & XX);
      eauto using in_cons.
    rewrite <- XX in ×.
    edestruct (res_get_plus _ _ rrr OG) as (?&?&?).
      by intro A; rewrite A in *; red in VG; desf.
    eapply vghost_get_at in VG; eauto.
    rewrite VG in *; desf; ∃ eq_refl; ins; red; eauto using prot_trans_refl.
  }

  rewrite Osb, res_plus_emp_l in ×.
  assert (CC': compat amap sb rf (upd L (TsbS b) (r_sb +!+ r_rf))).
    assert (AG':=AG); red in AG; desc; rewrite REQ; desf.
      by eapply compat_guar2; eauto.
    by eapply compat_atom_write; eauto; rewrite LEQ; ins; desf.

  repeat (split; eauto using in_eq, upds, compat_guar1, conform_upd_irr); ins;
    rupd; desc; try congruence.
  destruct IN; clarify; [|by repeat apply valid_node_upd_irr; eauto; intro; desf].

  red; unfold NW; eexists r; rewrite LEQ; rupd; repeat (split; ins; rupd; try edone);
  unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in *;
  rewrite ?map_upd_irr, ?escr_ffun_upd_irr in *; rupd; vauto;
    try (by rewrite in_map_iff; intro; desf);
    try (by ins; rewrite ?Osb0, ?Orf, ?Orf0, ?res_plus_emp_r; try done; apply LR).
  eby edestruct NRF.

  rewrite updC; ins.
  eapply compat_upd2_acc with (r := r_rf); eauto; ins.
  by replace (L (TrfS b)) with res_emp; eauto using res_plus_emp_l.

  assert (r ≠ Rundef) by (intro X; rewrite X in *; red in VG; desf).
  eapply exch_conform_upd2_acc with (r := r_rf); ins.
  2: by rewrite Orf, res_plus_emp_l.
  subst; eapply exch_conform_helper1 with (r:=r); ins; eauto using helper_out_def, in_eq.
  2: by revert GNA; clear - AG; red in AG; desc; rewrite REQ; destruct r.
  red; ins;
  destruct (ECO sigma (if excluded_middle_informative (edge = TrfS b) then TsbS b else edge))
    as (a' & M & M'); ins.
        by desf.
      by revert ESC; unfold upd; desf; eauto using res_escr_atomic_guar.
    ∃ a'; split; ins; revert M; rupd.
  by desf; ins; eauto.

  eapply ghostalloc_upd2_acc with (r := r_rf); ins.
  2: by rewrite Orf, res_plus_emp_l.
  eapply ghost_alloc_conform_helper1; eauto using helper_out_def, in_eq.
  by clear - AG; red in AG; desc; rewrite REQ; destruct r.
Qed.