Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import Omega List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas GpsLogic.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.
Require Import GpsPrep GpsRely GpsGhost GpsWPE GpsGuar.

Local Open Scope string_scope.

Set Implicit Arguments.

Definition erase (x : actid × exp × resource × (nat → RProp)) :=
   let '(a, e, r, QQ) := x in (a, e).

Theorem gsafe_pres :
  ∀ IE n mc L EE T mc',
    gsafe IE (n + 1) (Macts mc) (Mamap mc) (Msb mc) (Mrf mc) (Mmo mc) (Msc mc) L EE T →
    map erase T = Mtmap mc →
    mc_step mc mc' →
    ∃ L' EE' T',
      gsafe IE n (Macts mc') (Mamap mc') (Msb mc') (Mrf mc') (Mmo mc') (Msc mc') L' EE' T' ∧
      map erase T' = Mtmap mc' ∧
      ∃ rem, map (fun x ⇒ snd x) T' = map (fun x ⇒ snd x) T ++ rem.
Proof.
  destruct 3, mc as [? acts], mc' as [? ? amap sb rf mo]; ins; desf.

Case "normal step".
  eapply map_eq_app_inv in THR; desf.
  destruct l2' as [|[[? r] QQ] l2']; ins; desf.
  red in H; desf.
  exploit SAFE; eauto using in_or_app, in_eq.
  rewrite <- plus_n_Sm, <- plus_n_O; ins; desf.
  clear END FORK.
  rename a' into b.
  assert (ND' : NoDup (b :: acts)) by vauto; clear ND.

  assert (sb a b) by (rewrite SB; auto).
  assert (a ≠ b) by (intro; red in CONS; desc; edestruct ACYC; vauto).
  exploit (SBS a).
    by red in CONS; desc; red in FIN; desc; edestruct CLOsb as [? _]; eauto; ins; desf.
  rewrite filter_app, map_app, rsum_app; simpl; rewrite eqxx; simpl; rewrite res_plusAC.
  intro LAB.
  assert (PI := Consistent_pres_in CONS).

  rename L into Lold; edestruct prepare_step as (L & ?); eauto.
  clear AEQ SB RF MO SC LAB LR CC CO ECO GAC V Mamap Msb Mrf Mmo Msc CONS0; desc.
  generalize (fun a' IN NEQ ⇒ eq_trans (LEQ a' NEQ) (SBS a' IN));
    clear Lold SBS LEQ; intro SBS.

  assert (SBS': ∀ a', In a' acts →
              L (TsbS a') =
              rsum (map (fun aerP : nat × _ × _ × _ ⇒ snd (fst aerP))
                        (filter (fun aerP ⇒ fst (fst (fst aerP)) == a')
                                (l1' ++ l2')))).
  by clear - LAB SBS; intros; destruct (eqP a' a); desf;
     [rewrite LAB | rewrite SBS; ins]; rewrite !filter_app, !map_app, !rsum_app;
     ins; desf; desf.
  clear LAB SBS; rename SBS' into SBS.

  exploit rely_step; eauto.
    { inv ND'; unfold in_sb; simpl; rewrite (proj1 LR), res_plus_emp_l; ins;
      try apply CC; try apply nodup_map; intros; rewrite ?in_map_iff in *;
      ins; desf; ins; vauto; try congruence;
        try (by try intro; red in CONS; desc; edestruct ACYC; eauto using t_step);
        try (eby destruct FRESH; eapply prefix_closed_hb); try done.
      by destruct H3; rewrite ?mhbE in *; desf; eauto using prefix_closed_hb. }
    by ins; eapply Isb; intro; desf.
  clear V CC CO ECO GAC Irf Iesc Isb O LR; rename L into Lold; intros (L & ?); desf.
  generalize (fun a' IN ⇒ eq_trans (EsbS a') (SBS a' IN));
    clear EsbS SBS; intro SBS.
  assert (XXX: in_sb (b :: acts) Lold b = in_sb (b :: acts) L b).
    by clear - Esb ; unfold in_sb; induction (b :: acts); ins; f_equal; auto.
  rewrite XXX in *; clear Lold XXX Esb.

  eapply rely_compat_post in CC; eauto.
  2: intros c HB; assert (In c (b::acts)) by eauto using hb_in_acts2.
  2: ins; desf; [by red in CONS; desc; edestruct ACYC; eauto|].
  2: by destruct FRESH; eapply prefix_closed_hb; eauto.
  edestruct STEP0 with (rF := res_emp) as (P & GM & FUT); clear STEP0; eauto.
    eby rewrite res_plus_emp_r.

  apply res_plus_eq_empD in OUT; desc.
  apply res_plus_eq_empD in OUT0; desc.

  edestruct ghost_step
    as (L' & ?); try rewrite res_lt_strip_l; unfold res_lt;
    eauto using res_plus_emp_l, res_plus_emp_r; ins.

    unfold incoming; rewrite INesc, OUT1, !res_plus_emp_r.
    eby eapply valid_ghost_refl, rely_def.

    unfold incoming; rewrite INesc, res_plus_emp_r.
    by eauto using res_plus_emp_r.

    apply LR; intro HB.
    destruct (Consistent_hb_in CONS HB) as [_ []]; desf.
      by red in CONS; desc; edestruct ACYC; eauto.
    eby destruct FRESH; eapply prefix_closed_hb.


  rename L into Lold, L' into L; clear V CC CO ECO GAC INesc LR; desf.
  generalize (fun a' IN ⇒ eq_trans (EsbS a') (SBS a' IN));
    clear SBS; intro SBS.
  assert (XXX: in_sb (b :: acts) Lold b = in_sb (b :: acts) L b).
    by clear - Esb ; unfold in_sb; induction (b :: acts); ins; f_equal; auto.
  rewrite XXX in *; clear XXX.
  assert (XXX: out_sb (b :: acts) Lold b = out_sb (b :: acts) L b).
    by clear - Esb EsbS ; unfold out_sb; f_equal; auto;
       induction (b :: acts); ins; f_equal; auto.
  rewrite XXX in *; clear Esb EsbS XXX.
  assert (XXX: in_rf (b :: acts) Lold b = in_rf (b :: acts) L b).
    by clear - Erf ; unfold in_rf; induction (b :: acts); ins; f_equal; auto.
  rewrite XXX in *; clear XXX.
  assert (XXX: out_rf (b :: acts) Lold b = out_rf (b :: acts) L b).
    by clear - Erf ErfS ; unfold out_rf; f_equal; auto;
       induction (b :: acts); ins; f_equal; auto.
  rewrite XXX in *; clear Erf ErfS XXX OUT1 Lold.

  assert (WPE: pre_write_prot_equiv IE acts amap mo L b
               (in_sb (b :: acts) L b +!+ in_rf (b :: acts) L b)
               (incoming (b :: acts) L b)).
    by eapply pwpe; eauto.

  specialize (FUT _ IN' (wpe _ _ _ _ _ _ _ _ WPE VG RS));
      desf; rewrite res_plus_emp_r in ×.
  edestruct guar_step as [L' ?]; eauto.
  rename L into Lold, L' into L.
  clear CC CO ECO GAC V VG FUT; desf.
  generalize (fun a' IN NEQ ⇒ eq_trans (EsbS a' NEQ) (SBS a' IN));
    clear SBS; intro SBS.

  eexists L, EE', (l1' ++ (b,e', L (TsbS b), QQ) :: l2'); split;
    [|split; [|∃ nil; rewrite <- app_nil_end]]; rewrite ?map_app; try done.

  unfold gsafe, NW; repeat (apply conj; try done).
  ins; desf; rewrite filter_app; ins; desf; desf.
  by rewrite !filter_eq_nil; ins; auto using res_plus_emp_r; case eqP; ins;
     destruct FRESH; desf; apply CT; eauto using in_or_app, in_cons.
  by rewrite <- filter_app; apply SBS; congruence.

  by intro; rewrite in_app_iff; ins; desf; eauto 6 using in_or_app, in_cons.

  by intros until 0; repeat (rewrite in_app_iff; simpl); intro; desf; eauto;
     eapply safe_mon; try eapply SAFE; eauto using in_or_app, in_eq, in_cons with arith.

Case "fork".
  eapply map_eq_app_inv in THR; desf.
  destruct l2' as [|[[? r] QQ] l2']; ins; desf; ins.
  red in H; desf.
  exploit SAFE; eauto using in_or_app, in_eq.
  rewrite <- plus_n_Sm, <- plus_n_O; ins; desf.
  clear STEP END; exploit FORK; eauto; intro; desf.
  eexists L, EE, (l1' ++ (a,_,r1,QQ) :: l2' ++ (a,_,r2,(fun _ ⇒ Rtrue)) :: nil);
    split; ins.
  2: do 3 (rewrite map_app; ins); split; vauto.
  2: by eexists; rewrite !map_app, ?app_ass; ins.
  red; unfold NW; repeat (split; try done).
    by ins; rewrite SBS; ins;
       repeat (rewrite ?filter_app, ?map_app, ?rsum_app; ins; desf); rewrite ?res_plus_emp_r;
       f_equal; rewrite res_plusC, res_plusAC.
    intro; repeat (rewrite in_app_iff; simpl); ins; desf; ins;
    eauto 10 using in_or_app, in_eq, in_cons;
    apply (CT _ (in_or_app _ _ _ (or_intror _ (in_eq _ _)))).

  rewrite <- plus_n_Sm, <- plus_n_O in SAFE.
  intros until 0; repeat (rewrite in_app_iff; simpl); intro; desf; eauto;
  eapply safe_mon; try eapply SAFE; eauto using in_or_app, in_eq, in_cons.
Qed.

Lemma gsafe_memsafe IE n acts amap sb rf mo sc L EE T :
  gsafe IE n acts amap sb rf mo sc L EE T →
  mem_safe acts amap sb rf.
Proof.
  unfold gsafe; red; ins; desf; clear SAFE SBS CT.
  assert (GI: res_get (incoming acts L a) (loc (amap a)) ≠ p_bot).
    eapply V in IN; red in IN; desf.
    intro IN; eapply vghost_get_bot in VG; eauto.
    destruct (amap a); ins; desf; desf; try congruence.
    red in AG; desf; congruence.
  eapply visible_allocation in GI; eauto using Consistent_prefix_closed, prefix_closed_pres_in.
  desf; destruct (amap a); ins; desf; eauto 8.
Qed.

Lemma compat_inc2 :
  ∀ 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
    (NEQ : a ≠ b)
    (NHB : ¬ happens_before amap sb rf a b)
    (NHB': ¬ happens_before amap sb rf b a),
  incoming acts L a +!+ incoming acts L b ≠ Rundef.
Proof.
  ins; intro X.
  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)
             ++ map (Tsb^~ b) (filter (mydecf (happens_before amap sb rf^~ b)) acts)
             ++ map (Trf^~ b) (filter (mydecf (happens_before amap sb rf^~ b)) acts)
             ++ map (Tesc^~ b) (filter (mydecf (happens_before amap sb rf^~ b)) 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; 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].

  unfold incoming in *; rewrite !res_plusA in ×.
  by ins; rewrite !map_app, !rsum_app, !rsum_map_map_filter; ins; apply LR; eauto.
Qed.

Lemma gsafe_racefree IE n acts amap sb rf mo sc L EE T :
  gsafe IE n acts amap sb rf mo sc L EE T →
  race_free acts amap sb rf.
Proof.
  unfold gsafe; ins; desf; clear SAFE SBS CT.
  cut (∀ a b
          (INa : In a acts)
          (INb : In b acts)
          (NEQ : a ≠ b)
          (LOC : loc (amap a) = loc (amap b)),
          is_access (amap a) →
          is_access (amap b) →
          c11.is_na (amap a) →
          is_write (amap a) ∨ is_write (amap b) →
          happens_before amap sb rf a b ∨ happens_before amap sb rf b a); ins.
     by red; ins; desf; eauto; rewrite or_comm; eauto.
  apply NNPP; intro X; apply not_or_and in X; desf.
  {
    assert (GI: res_get (incoming acts L b) (loc (amap b)) ≠ p_bot).
      eapply V in INb; red in INb; desf.
      intro INb; eapply vghost_get_bot in VG; eauto.
      destruct (amap b); ins; desf; desf; try congruence.
      red in AG; desf; congruence.

    assert (GI': res_get (incoming acts L a) (loc (amap a)) = p_uninit ∨
                 ∃ v, res_get (incoming acts L a) (loc (amap a)) = p_na pe_full v).
      eapply V in INa; red in INa; desf; eauto.
      destruct (amap a); ins; desf; desf;
        eauto using vghost_get_back_uninit;
        right; red in VG; desf; rewrite VG in *; ins;
      match goal with H : res_get ?r ?loc = p_na _ _ |- _ ⇒
        destruct r; ins; desf; inv_lplus loc; rewrite H in *; ins; desf; desf; eauto
      end.

   eapply compat_inc2 with (a := a) (b := b); eauto.
   rewrite LOC in *; desf;
   by destruct (incoming acts L a), (incoming acts L b); ins; desf; inv_lplus (loc (amap b));
      unfold prot_plus in *; desf.
  }
  {
    assert (GI: writeL_pre (res_get (incoming acts L b) (loc (amap b)))).
      by eapply is_writeL_inc; eauto; destruct (amap b); ins.

    assert (GI': res_get (incoming acts L a) (loc (amap a)) = p_uninit ∨
                 ∃ k v, res_get (incoming acts L a) (loc (amap a)) = p_na k v).
      eapply V in INa; red in INa; desf; eauto.
      destruct (amap a); ins; desf; desf;
        eauto using vghost_get_back_uninit;
        right; red in VG; desf; rewrite VG in *; ins;
      match goal with H : res_get ?r ?loc = p_na _ _ |- _ ⇒
        destruct r; ins; desf; inv_lplus loc; rewrite H in *; ins; desf; desf; eauto
      end.

    eapply compat_inc2 with (a := a) (b := b); eauto.
    rewrite LOC in *; desf.
      2: by eapply res_plus_is_na_writeL_pre; vauto.
    by destruct (incoming acts L a), (incoming acts L b); ins; desf; inv_lplus (loc (amap b));
       unfold prot_plus in *; desf.
  }
Qed.

Lemma gsafe_rinit IE n acts amap sb rf mo sc L EE T :
  gsafe IE n acts amap sb rf mo sc L EE T →
  initialized_reads acts amap rf.
Proof.
  unfold gsafe; red; ins; desf; clear SAFE SBS CT.
  assert (K:=IN); eapply V in K; red in K; desf.
  destruct (amap a) eqn: LEQ; ins; desf; desf.
  {
    assert (GI': ∃ k, res_get (incoming acts L a) l = p_na k v1).
      red in VG; desf; rewrite VG in *; ins;
      match goal with H : res_get ?r ?loc = p_na _ _ |- _ ⇒
        destruct r; ins; desf; inv_lplus loc; rewrite H in *; ins; desf; desf; eauto
      end.
    eapply visible_na in GI'; eauto using Consistent_prefix_closed, prefix_closed_pres_in; desf.
    red in CONS; desc; specialize (Crf a); intro Z; rewrite Z in Crf.
    by eapply Crf; eauto; rewrite LEQ; ins.
  }
  {
    eapply vghost_get_back_at in VG; eauto.
    eapply visible_atomic in VG; eauto using Consistent_prefix_closed, prefix_closed_pres_in; desf.
    red in CONS; desc; specialize (Crf a); intro Z; rewrite Z in Crf.
    by eapply Crf; eauto; rewrite LEQ; ins.
  }
  {
    eapply vghost_get_back_at in VG; eauto.
    eapply visible_atomic in VG; eauto using Consistent_prefix_closed, prefix_closed_pres_in; desf.
    red in CONS; desc; specialize (Crf a); intro Z; rewrite Z in Crf.
    by eapply Crf; eauto; rewrite LEQ; ins.
  }
Qed.

Lemma Consistent_ext_skip :
  ∀ acts amap sb rf mo sc
    (CONS : Consistent acts amap sb rf mo sc)
    a' (INa : In a' acts)
    b' (NIN : ¬ In b' acts),
  Consistent (b' :: acts) amap (fun a b ⇒ sb a b ∨ a = a' ∧ b = b') rf mo sc.
Proof.
  ins.
  assert (HBM:
        ∀ a b,
          happens_before amap sb rf a b →
          happens_before amap (fun a0 b ⇒ sb a0 b ∨ a0 = a' ∧ b = b') rf a b).
    by clear; induction 1; try red in H; desf; eauto using hb_sb, hb_trans.
  assert (HBE: ∀ a b,
       happens_before amap (fun a b ⇒ sb a b ∨ a = a' ∧ b = b') rf a b
       ↔ happens_before amap sb rf a b ∨
           a = a' ∧ b = b' ∨
           happens_before amap sb rf a a' ∧ b = b').
    split; ins; desf; eauto using hb_sb.
    2: by eapply hb_trans, hb_sb; eauto.
    induction H; try red in H; desf; eauto using hb_trans;
    by eapply Consistent_hb_in in IHclos_trans2; eauto; desf.

  unfold Consistent, ExecutionFinite, ConsistentMO, ConsistentSC, SCrestriction,
    restr_subset, ConsistentRF_basic, CoherentRR, CoherentRW, CoherentWR in *;
    unfold NW; desf.
  assert (M': amap b' = Askip) by (apply NNPP; eauto).
  repeat apply conj; ins; desf; eauto.

  by eapply CLOsb in H; desf; eauto.
  {
    intros x C; apply (ACYC x).
    destruct (eqP x b'); desf.
      exfalso; revert C; generalize b' at 3; ins; revert NIN.
      induction C; eauto; desf.
          by eapply CLOsb in H; ins; desf.
        specialize (Crf y); desf; desf; ins.
        by destruct NIN; apply CLOlab; intro X; rewrite X in ×.
      by eapply Csc in H; intro X; apply X, CLOlab; clear X; intro X; rewrite X in *; desf.
    revert C n; clear - INa NIN Crf CLOlab CLOsb Crf Csc.
    generalize x at 1 4; induction 1; desf; eauto using clos_trans.
    cut (y ≠ b'); eauto using clos_trans.
    intro; desf; clear - INa NIN C2 Crf CLOlab CLOsb Csc.
    revert C2 NIN; generalize b' at 2 3; ins; revert NIN.
    induction C2; eauto; desf.
        by eapply CLOsb in H; ins; desf.
      specialize (Crf y); desf; desf; ins.
      by destruct NIN; apply CLOlab; intro X; rewrite X in ×.
    by eapply Csc in H; intro X; apply X, CLOlab; clear X; intro X; rewrite X in *; desf.
  }
  by eapply Cmo3; eauto; rewrite HBE in *; desf; ins;
     destruct NIN; apply CLOlab; intro X; rewrite X in ×.
  by rewrite HBE in REL; desf; eauto; rewrite M' in *; ins.
  by exploit Cscr; eauto; intro; desf; eauto;
     right; split; ins; rewrite HBE in *; desf; eauto;
     repeat apply proj1 in SC0; apply Csc in SC0; rewrite M' in *; desf.
  by specialize (Crf a); desf; desf; ins.
  by specialize (Crf a); desf; desf; ins;
     rewrite HBE in *; desf; ins; eauto;
     destruct NIN; apply CLOlab; intro X; rewrite X in ×.
  by rewrite HBE in *; desf; ins; eauto;
     specialize (Crf b'); desf; desf; ins;
     destruct NIN; apply CLOlab; intro X; rewrite X in ×.
  by rewrite HBE in *; desf; ins; eauto;
     specialize (Crf b'); desf; desf; ins;
     destruct NIN; apply CLOlab; intro X; rewrite X in ×.
  by rewrite HBE in *; desf; ins; eauto; eapply Cmo in MO; desf;
     destruct NIN; apply CLOlab; intro X; rewrite X in ×.
Qed.

Lemma gsafe_final_sat :
  ∀ IE acts amap sb rf mo sc
    (CONS' : Consistent acts amap sb rf mo sc) L' EE
    (V : ∀ a, In a acts → valid_node IE acts acts amap rf L' EE a)
    (CC : compat amap sb rf L')
    (CO : conform acts amap mo L' acts)
    (ECO: ∀ sigma, exch_conform IE acts amap sb rf L' L' EE sigma) a r r_rem
    (GAC : ghost_alloc_conform acts L' EE)
    (SBS : L' (TsbS a) = r +!+ r_rem)
    (CT : In a acts) QQ
    (END : ghost_move IE r QQ)
    (ND : NoDup acts)
    (NDE : NoDup EE)
    (LR : label_restr acts amap sb rf L' EE),
  ∃ r, QQ r.
Proof.
  ins; assert (FRESH: ∃ b, ¬ In b acts); desf.
    ∃ (S (fold_right (fun x y ⇒ x + y) 0 acts)); clear.
    assert (∀ n, In n acts → n ≤ fold_right (fun x y ⇒ x + y) 0 acts).
      induction acts; ins; desf; [omega|].
      by eapply IHacts in H; omega.
    by intro X; eapply H in X; omega.
  assert (ND' : NoDup (b::acts)) by vauto.
  assert (SKIP : amap b = Askip).
    by red in CONS'; desc; apply NNPP; intro X; eapply FIN in X.
  assert (CONS: Consistent (b :: acts) amap (fun a0 b0 ⇒ sb a0 b0 ∨ a0=a ∧ b0=b) rf mo sc).
    by eapply Consistent_ext_skip; eauto.
  assert (PI := Consistent_pres_in CONS).
  exploit prepare_step; eauto; vauto.
  clear CONS'.
  clear LR CC CO ECO GAC V; rename L' into Lold; intros (L & ?); desf.
  clear Lold LEQ SBS.
  exploit rely_step; eauto; vauto.
    { unfold in_sb; simpl; rewrite (proj1 LR), res_plus_emp_l; ins;
      try apply CC; try apply nodup_map; intros; rewrite ?in_map_iff in *;
      ins; desf; ins; vauto; try congruence;
        try (by try intro; red in CONS; desc; edestruct ACYC; eauto; vauto);
        try (eby destruct FRESH; eapply prefix_closed_hb); try done.
      by rewrite ?mhbE in *; desf; eauto using prefix_closed_hb. }
    by ins; eapply Isb; intro; desf; tauto.

  clear V CC CO ECO GAC Irf Iesc Isb O LR; rename L into Lold; intros (L & ?); desf.
  assert (XXX: in_sb (b :: acts) Lold b = in_sb (b :: acts) L b).
    by clear - Esb ; unfold in_sb; induction (b :: acts); ins; f_equal; auto.
  rewrite XXX in *; clear Lold XXX Esb EsbS.

  eapply rely_compat_post in CC; eauto; vauto.
  2: intros c HB; assert (In c (b::acts)) by eauto using hb_in_acts2.
  2: ins; desf; [by red in CONS; desc; edestruct ACYC; eauto|].
  2: by destruct FRESH; eapply prefix_closed_hb; eauto.
  rewrite SKIP in *; ins; desf.
  rewrite RELY in ×.
  apply res_plus_eq_empD in OUT; desc.
  apply res_plus_eq_empD in OUT0; desc.
  edestruct ghost_step
    as [L' ?]; try rewrite res_lt_strip_l; unfold res_lt;
    eauto using res_plus_emp_l, res_plus_emp_r; ins; desf; vauto.

    unfold incoming; rewrite INesc, OUT1, !res_plus_emp_r.
    eby rewrite RELY in *; eapply valid_ghost_refl.

    unfold incoming; rewrite INesc, res_plus_emp_r, RELY.
    by eauto using res_plus_emp_r.

    apply LR; intro HB.
    destruct (Consistent_hb_in CONS HB) as [_ []]; desf.
      by red in CONS; desc; edestruct ACYC; eauto.
    eby destruct FRESH; eapply prefix_closed_hb.
Qed.

Theorem adequacy :
  ∀ IE e QQ (T: triple IE Rtrue e QQ) e' acts amap sb rf mo sc,
    cexecutions e e' acts amap sb rf mo sc →
    mem_safe acts amap sb rf ∧
    race_free acts amap sb rf ∧
    initialized_reads acts amap rf ∧
    ∀ v, e' = Evalue v → ∃ r, (QQ v) r.
Proof.
  ins; red in T; red in H; desf.
  cut (∀ n, ∃ L' EE' T',
         gsafe IE n acts amap sb rf mo sc L' EE' T' ∧
         map erase T' = (a, e') :: l ∧
         ∃ rem, map (fun x ⇒ snd x) T' = QQ :: rem).
    clear; ins; specialize (H 1); desf.
    repeat apply conj; eauto 6 using gsafe_rinit, gsafe_memsafe, gsafe_racefree.
    ins; desf.
    destruct T' as [|[[]]]; ins; desf.
    red in H; desf.
    specialize (CT _ (in_eq _ _)).
    specialize (SAFE _ _ _ _ (in_eq _ _)).
    specialize (SBS _ CT); ins; desf; desf; ins.
    by eapply gsafe_final_sat; eauto.

  remember ((a, e') :: l) as tmap; clear Heqtmap.
  remember {|
        Mtmap := tmap;
        Macts := acts;
        Mamap := amap;
        Msb := sb;
        Mrf := rf;
        Mmo := mo;
        Msc := sc |} as c; revert tmap acts amap sb rf mo sc Heqc.
  apply clos_rt_rtn1 in H; induction H; ins; desf.
  2: by destruct y; exploit (IHclos_refl_trans_n1); ins; desf;
        eapply gsafe_pres in H; ins; eauto; desf; eauto;
        rewrite x1 in *; ins; eauto 8.

  assert (CONS: Consistent (init :: nil) (fun _ ⇒ Askip) (fun _ _ ⇒ False)
                     (fun _ ⇒ None) (fun _ _ ⇒ False) (fun _ _ ⇒ False)).
    red; unfold NW; repeat (split; ins); repeat red; ins.
    by induction H; ins; desf.

  exploit (T res_emp); clear T; try done; intro T.
  eapply ghost_step with (r:=res_emp) (EE:=nil) (L:= fun _ ⇒ res_emp) in T; try exact CONS; eauto;
    try (solve [repeat split; ins]); rewrite ?res_plus_emp_l, ?res_plus_emp_r;
    ins; eauto using res_lt_refl;
    try solve [by unfold incoming, out_esc, in_esc, out_sb, out_rf, in_rf, in_sb;
          repeat first [rewrite res_plus_eq_empI | rewrite rsum_eq_empI |
            rewrite res_strip_emp]; ins; desf; apply res_lt_refl].
    2: by red; ins; rewrite rsum_eq_empI; ins; rewrite in_map_iff in *; desf; unfold upd; desf.
    2: by red; ins; unfold upd in *; desf.
    2: by red; ins; desf.
    2: by unfold incoming, out_esc, in_esc, in_rf, in_sb; rewrite res_plus_emp_l;
          repeat first [rewrite res_plus_eq_empI | rewrite rsum_eq_empI]; ins; desf;
          do 7 eexists; intros; desf; desf.
  desf; clear V.
  ∃ (upd L' (TsbS init) r), EE', ((init, e, r, QQ)::nil); split; ins; eauto.
  red; unfold NW.
  rewrite EsbS, res_plus_emp_l in ×.
  do 8 try (split; try done); ins; desf; rupd; ins;
    eauto using in_eq, res_plus_emp_r.

  red; unfold NW; ∃ r.
  unfold incoming, out_esc, in_sb, in_rf, in_esc, out_sb, out_rf in *; ins.
  rewrite ?escr_ffun_upd_irr, !res_plus_emp_r; rupd; try done.
  rewrite Esb, Erf, ErfS, ?res_plus_emp_l, ?res_plus_emp_r in ×.
  repeat (split; try edone); ins.
  by rewrite map_upd_irr; ins; rewrite in_map_iff; intro; desf.
  by destruct P'; intro; desf.
Qed.