Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple.
Require Import ihc drf memsafe initread path.
Require Import GpsSepAlg.
Require Import Omega.

Set Implicit Arguments.

Definition prg_sem e res acts lab sb rf mo sc :=
  ∃ fst lst pre post acts',
    acts = pre :: acts' ∧
    << pNIN: ¬ In pre acts' >> ∧
    << qNIN: ¬ In post acts' >> ∧
    << NEQ : pre ≠ post >> ∧
    << ESEM: exp_sem e res acts' lab sb fst lst >> ∧
    << CONS: Consistent (post :: acts) lab sb rf mo sc Model_hb_rf_acyclic >> ∧
    << pSB1: ∀ x, ¬ sb x pre >> ∧
    << pSB2: ∀ x, sb pre x → x = fst >> ∧
    << pSB : unique (sb^~ fst) pre >> ∧ << pL : lab pre = Askip >> ∧
    << qSB : unique (sb lst) post >> ∧ << qL : lab post = Askip >>.

Theorem adequacy PS PSg :
  ∀ e QQ (T: triple (@Atrue PS PSg) e QQ) reso acts lab sb rf mo sc
    (SEM : prg_sem e reso acts lab sb rf mo sc),
    mem_safe acts lab sb rf mo ∧
    race_free acts lab sb rf mo ∧
    initialized_reads acts lab rf ∧
    (∀ res, reso = Some res → ∃ h, assn_sem (QQ res) h).
Proof.
  ins; red in SEM; unfold unique in *; desf; red in CONS; desf; ins.
  assert (HC: hist_closed sb rf (pre :: acts')).
  {
    assert (hist_closed sb rf (post :: pre :: acts')).
    {
      red; intros; destruct HB.
      × by eapply FIN, proj1 in HB_SB.
      × apply (proj1 FIN).
        intro N.
        specialize (Crf a); desf; desf.
        by rewrite N in ×.
    }
    red; intros; generalize HB; eapply H in HB; eauto using In_cons.
    destruct HB; try done; subst.
    destruct 1.
    × ins; desf; [eby edestruct pSB1|].
      by destruct (exp_sem_pre_closed _ _ _ _ _ _ _ ESEM _ _ HB_SB); desf; eauto.
    × exfalso.
      specialize (Crf a); desf; desf.
      by rewrite qL in ×.
  }

  assert (ND: NoDup (post :: pre :: acts')).
    by repeat constructor; eauto using exp_sem_nodup; ins; intuition.

  assert (∃ hmap, hmap_valids_strong lab sb rf hmap (pre :: (acts' ++ nil))
              ∧ with_opt reso (fun res h ⇒ ∃ hFR' hq, assn_sem (QQ res) hq ∧
                                                             h = hq +!+ hFR' ∧ h ≠ Hundef)
                          (hmap (hb_sb lst post))).
  {
    assert (VAL: hmap_valids_strong lab sb rf (fun _ : hbcase ⇒ @hemp PS PSg) (pre :: nil)).
    {
      split; ins; unnw; red.

      ∃ (fun _ ⇒ None); split.
        by ∃ 0; ins.

      red; ins; desf.

      red; rewrite pL; unfold not in ×.

      ∃ gres_emp; split.
        by split; ins; exploit H; ins.

      ∃ nil, (fst :: nil); repeat (split; ins);
        desf; eauto using eq_sym.
      by rewrite hplus_emp_r, hsum_one.
      by rewrite !hplus_emp_r, hsum_one.
    }

    assert (HC': hist_closed sb rf (pre :: nil)).
    {
      red; ins; desf; unfold not in *; destruct HB; rewrite ?pL in *; eauto.
      by specialize (Crf a); rewrite HB_RF, pL in *; desf.
    }

    cut (safe acts' (post :: pre :: nil) lab sb rf (S (length acts'))
           (pre :: nil) (fun _ ⇒ hemp) lst
           (with_opt reso (fun res h ⇒ ∃ hFR' hq, h ≠ Hundef ∧ h = hq +!+ hemp +!+ hFR'
                                                   ∧ assn_sem (QQ res) hq))).

    {
      assert (INlst: In lst acts') by eauto using exp_sem_lst.
      revert ND HC HC' VAL INlst.
      change (pre :: acts') with ((pre :: nil) ++ acts').
      rewrite <- (appl0 acts') at 3 4.
      change (pre :: nil) with (nil ++ pre :: nil) at 6.
      generalize (@nil actid) at 1 2 3 4 5 6 8 10 as V.
      clear - qSB IRR Crf' Cna.
      remember (S (length acts')) as n; revert Heqn.
      generalize (fun _ : hbcase ⇒ @hemp PS PSg) as hmap, acts' as acts.
      induction n; ins; desf.
      destruct (classic (acts = nil)); subst; ins.
        ∃ hmap; split; ins; desf.
        exploit POST; clear POST RELY GUAR; eauto using In_appI1.
        by clear; destruct reso; ins; desf; rewrite ?hplus_emp_l in *; eauto.

      clear POST RELY.

      eapply get_shallow with (V := pre :: V) in H4; try edone; desc;
        try (by destruct mt).
      exploit (GUAR e); clear GUAR; eauto using In_appI1.
        by clear - IN H; rewrite ?nodup_cons, ?nodup_app, In_app in *;
           ins; intro; desf; eauto.
        by eapply Permutation_hist_closed, HC;
           eauto using Permutation_cons_append.
      intro M; desc.
      eapply In_implies_perm in IN; desc.
      assert (P' : Permutation (V ++ acts) (e :: V ++ l')).
      {
        clear - IN; simpl; etransitivity.
          by eapply Permutation_app, IN; apply Permutation_refl.
        by auto using Permutation_sym, Permutation_cons_app.
      }
      specialize (IHn hmap' l').
      rewrite (Permutation_length IN) in IHn.
      specialize (IHn eq_refl (e :: V)).
      exploit IHn; clear IHn;
        eauto using Permutation_NoDup, Permutation_hist_closed.
      × by eapply Permutation_hist_closed, HC; vauto.
      × split.
        + red in VALID; desf.
          red in VALIDS; desf.
          ∃ ga; split; eauto.
          red; ins; eapply VLD; desf; find_in_list.
        + red in VALID; desf.
          red; ins; eapply (RESTR e0).
          - intro; destruct NIN; ins; desf; rewrite In_app in *; desf; ins; desf; find_in_list.
          - clear NIN; desf; eauto.
            right; split; eauto; intro SB; destruct H5; clear - SB.
            unfold is_sb_out in *; desf; split; eauto.
            ins; desf; eauto; rewrite In_app in *; desf; ins; desf; find_in_list.
      × by ins; desf;
           rewrite In_app in H3; des; try eapply (Permutation_in _ IN) in H3;
           ins; desf; eauto using In_appI1, In_appI2, In_eq, In_cons.
      × rewrite (Permutation_length (Permutation_sym IN)); simpl.
        eapply Permutation_safe1, SAFE.
        change (e :: V) with ((e :: nil) ++ V); rewrite <- appA.
        by eauto using Permutation_app, Permutation_trans,
                       Permutation_cons_append.
      × clear - IN; intro M; desf; eexists; split; try edone.
        eapply Permutation_hmap_valids_strong, M.
        constructor; change (e :: V) with ((e :: nil) ++ V); rewrite <- appA.
        apply Permutation_sym, Permutation_app; eauto using Permutation_trans, Permutation_cons_append.
    }

    {
      eapply T in ESEM; desc; eapply ESEM with (rf := rf) (sc := sc) (mo := mo);
      clear ESEM T; vauto.
        eapply ConsistentWeaken2, Consistent_perm; try edone.
         2: by rewrite perm_eq_sym, perm_appC; apply perm_eq_refl.
         by repeat (split; try done).
        by eapply Permutation_NoDup; try apply Permutation_app_comm.
        by rewrite hplus_emp_r.
        done.
    }
  }

  desc; rewrite appl0 in ×.
  red in H; desc.
  repeat split; eauto using valid_implies_mem_safe, valid_implies_race_free, valid_implies_initialized_reads.
  by ins; desf; ins; desf; vauto.
Qed.

Theorem rule_frame PS PSg :
  ∀ (P: assn PS PSg) E QQ (T: triple P E QQ) F,
    triple (Astar P F) E (fun y ⇒ Astar (QQ y) F).
Proof.
  red; ins; apply T in SEM; desc; try done.
  clear T; ins; desf; rewrite hplusA in ×.
  exploit SEM; try edone.
  instantiate (1 := n); clear - pSAT2; revert hmap V.
  induction n; ins; desc; unfold NW; repeat split; ins; eauto.
  specialize (POST IN _ SB); clear - POST pSAT2; desf.
  { destruct res; ins; desf.
    ∃ hFR', (hq +!+ h2); rewrite <- !hplusA in *; repeat eexists; try edone.
    by intro U; rewrite U, !hplus_undef_l in ×.
  }
  specialize (GUAR _ INcmd NIN HC'); clear - GUAR IHn; desf; eauto.
Qed.

Lemma conseq_helper PS PSg :
  ∀ acts_cmd acts_ctx lab sb rf n (hmap : hbcase → heap PS PSg)
    (V : list actid) lst res (Q Q' : nat → heap PS PSg → Prop)
    (IMP: ∀ res h, Q res h → Q' res h),
  safe acts_cmd acts_ctx lab sb rf n V hmap lst (with_opt res Q) →
  safe acts_cmd acts_ctx lab sb rf n V hmap lst (with_opt res Q').
Proof.
  induction n; ins; desc; unfold NW; repeat split; ins; eauto.
  specialize (POST IN _ SB); clear - POST IMP; desf.
    by destruct res; ins; desf; repeat (eexists; try edone); apply IMP.
  specialize (GUAR _ INcmd NIN HC'); clear - GUAR IHn IMP; desf; eauto.
Qed.

Theorem rule_conseq PS PSg :
  ∀ (P: assn PS PSg) E QQ (T: triple P E QQ)
            P' (PI: implies P' P)
            QQ' (QI: ∀ y, implies (QQ y) (QQ' y)),
    triple P' E QQ'.
Proof.
  red; ins; apply T in SEM; desc; try done.
  clear T; ins; desf.
  exploit SEM; try apply PI; try edone.
  by eapply conseq_helper; ins; desf; repeat eexists; eauto; eapply QI.
Qed.

Theorem rule_disj PS PSg :
  ∀ (P1: assn PS PSg) E QQ (T1: triple P1 E QQ)
            P2 (T2: triple P2 E QQ),
    triple (Adisj P1 P2) E QQ.
Proof.
  red; intros; rewrite assn_sem_disj in *; desf; [ eapply T1 | eapply T2 ]; eauto.
Qed.

Theorem rule_exists PS PSg :
  ∀ (PP: val → assn PS PSg) E QQ (T: ∀ x, triple (PP x) E QQ),
    triple (Aexists PP) E QQ.
Proof.
  red; intros; rewrite assn_sem_exists in *; desc; eapply T; eauto.
Qed.

Theorem rule_value PS PSg v (QQ: val → assn PS PSg) :
  triple (QQ v) (Evalue v) QQ.
Proof.
  eapply triple_helper_start; ins; desf; ins; desf.
  red in VALID; desc.
  red in VALIDS; desc.
  eapply safe_final_plain with (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    eexists hemp; repeat eexists; try edone.
    rewrite hplus_emp_r; congruence.
  rewrite hplus_emp_r.
  red; ins; desf; unfold NW.
  unfold unique in *; desf.
  eapply assn_sem_satD in pSAT; desf.
  rewrite pEQ in *; eapply hdef_alt in pDEF; desf.

  ∃ gres_emp; split.
    by unfold ga_clear; split; ins; desf.
  eexists (prev :: nil), (next :: nil).
  assert (S: hmap (hb_sink fst) = hemp) by (eapply RESTR; eauto).
  ins; rewrite !hsum_one; repeat (split; ins; desf); eauto;
    unfold mupd; desf; try congruence.
  by rewrite pDEF, S, hplus_emp_r.
  by rewrite S, !hplus_emp_r.
Qed.

Theorem rule_let PS PSg :
  ∀ (P: assn PS PSg) e QQ (T1: triple P e QQ)
         RR e' (T2: ∀ x, triple (QQ x) (e' x) RR),
    triple P (Elet e e') RR.
Proof.
  red; ins; desf; ins.
     by eapply T1 in SEM0; exploit SEM0; eauto.

  rewrite appA in ×.
  assert (UU1: unique (sb lst1) fst2) by (ins; desf; red; eauto using eq_sym).

  generalize ((T1 _ _ _ _ _ _ ESEM1) _ _ _ _ CONS UNIQ _ FST _ UU1
                    n V V_PREV (fun x H ⇒ In_appI2 (V_CTX x H) _)
                    HC hmap VALID pDEF _ _ pEQ pSAT); clear T1; intro T1.
  assert (CONS': weakConsistent (acts2 ++ acts1 ++ acts_ctx) lab sb rf mo sc Model_hb_rf_acyclic).
    eapply weakConsistent_perm; eauto.
    by rewrite perm_appCA, perm_eq_refl.
  assert (UNIQ': NoDup (acts2 ++ acts1 ++ acts_ctx)).
    eapply nodup_perm; eauto.
    by rewrite perm_appCA, perm_eq_refl.

  assert (UU2: unique (sb^~ fst2) lst1) by (red; eauto using eq_sym).
  specialize ((T2 _ _ _ _ _ _ _ ESEM2) _ _ _ _ CONS' UNIQ' _ UU2 _ LST).
  clear UU1 CONS' UNIQ' UU2.

  assert (RNG: ∀ x, In x V → In x (acts1 ++ acts_ctx))
    by eauto using In_appI2.

  clear V_PREV V_CTX pEQ pDEF pSAT.
  revert hmap V HC T1 VALID RNG; induction n; ins; unfold NW.
  ins; desf; repeat split; ins.
      exfalso; eapply RNG in IN; rewrite In_app in *; desf;
      eauto using exp_sem_lst.
      by rewrite !nodup_app in *; desf; eauto using exp_sem_lst.

     eapply IHn; eauto using In_appI2; unfold not; ins; desf;
       eauto using In_appI2.

  rewrite In_app in *; desf.
    exploit GUAR; eauto; ins; desf.
    ∃ hmap'; repeat (split; try done).
    eapply IHn; ins; unfold not; ins; desf; eauto using In_appI1.

  clear IHn RELY GUAR.

  assert (In fst2 (a :: V)).
    by eapply (hist_closed_trans HC'); eauto using exp_sem_fst_reach, In_eq.
  assert (¬ In fst2 V).
    intro M; eapply RNG in M; rewrite In_app in *; desf; eauto using exp_sem_fst.
    by rewrite !nodup_app in *; desf; eauto using exp_sem_fst.
  ins; desf.

  assert (In lst1 V).
    exploit HC'; eauto using In_eq; ins; desf; vauto; desf.
    by exfalso; eauto using exp_sem_lst.

  exploit POST; eauto; intro M; desf.

  exploit (T2 (S n) V); eauto; []; intros (_ & _ & G).
  exploit G; clear G; eauto; []; intro; desf.
  ∃ hmap'; repeat (split; ins).
  eapply conseq_helper, safe_mod; try eassumption; instantiate; ins; desf; try rewrite In_app in *; desf; eauto.
    by repeat eexists; eauto; rewrite hplusA.
  by destruct NIN0; right; eapply hist_closed_trans; eauto using exp_sem_lst_reach.
Qed.

Theorem rule_par PS PSg :
  ∀ (P1: assn PS PSg) e1 QQ1 (T1: triple P1 e1 QQ1)
         P2 e2 Q2 (T2: triple P2 e2 (fun x ⇒ Q2)),
    triple (Astar P1 P2) (Epar e1 e2) (fun x ⇒ Astar (QQ1 x) Q2).
Proof.
  ins; eapply triple_helper_start; ins; desf; ins.

    assert (NEQf: fst1 ≠ fst2).
      by intro; ins; rewrite !nodup_cons, nodup_app in NODUP;
         desf; eauto using exp_sem_fst.
    assert (NEQl: lst1 ≠ lst2).
      by intro; ins; rewrite !nodup_cons, nodup_app in NODUP;
         desf; eauto using exp_sem_lst.

  assert (∃ hmap',
            << AGR: agrees sb rf V hmap hmap' >> ∧
            << VALID: hmap_valids_strong lab sb rf hmap' (fst::V) >> ∧
            hmap' (hb_sb fst fst1) = h1 ∧
            hmap' (hb_sb fst fst2) = h2 +!+ hFR ∧
            hmap' (hb_sb fst fst2) ≠ Hundef).
  {
    red in VALID; desc.
    red in VALIDS; desc.
    ∃ (mupd (mupd hmap (hb_sb fst fst1) h1) (hb_sb fst fst2) (h2 +!+ hFR)).
    repeat split; unfold NW, hmap_valids; ins; unfold mupd; desf; desf; ins; desf;
      try (by destruct NIN0; eauto); try (by desf; destruct H0; vauto).
    × ∃ (ga_clear ga fst).
      split.
        by eauto using ga_clear_fin.
      red; ins; desf; desf.
      + red; rewrite LABF.
        ∃ gres_emp; split.
          by unfold ga_clear; split; ins; desf.
        eapply hdef_alt in pDEF; desfh.
        ∃ (prev :: nil), (fst1 :: fst2 :: nil).
        ins; rewrite hsum_one, hsum_two; desf; desfh.
        unfold unique in *; des.
        assert (S: hmap (hb_sink e) = hemp) by (eapply RESTR; eauto).
        repeat split; ins; des; subst; try done; eauto.
          by repeat econstructor; red; ins; desf.
          by eapply UF0 in H; desf; vauto.
          by rewrite S, hplus_emp_r, <- hplusA, <- pEQ; congruence.
          by rewrite S, !hplus_emp_r, pEQ, hplusA.
        + eapply hmap_irr_change_valid; eauto.
            by ins; apply ga_clear_agrees; congruence.
            by ins; desf; desf; ins; desf; destruct NIN; eapply HC; vauto.
    × eapply (RESTR (hb_fst edge)); eauto.
    × eapply (RESTR e); eauto.
      right; split; try done.
      intro SB; destruct H0; clear - SB.
      red in SB; split; desf; ins; eauto.
    × by intro U; eapply pDEF; rewrite pEQ, hplusA, U, hplusC.
  }


  clear pEQ pSAT pDEF VALID HC; desf.
  ∃ hmap'; repeat (split; try done); clear hmap AGR.

  assert (PERM : perm_eq (fst :: lst :: (acts1 ++ acts2) ++ acts_ctx)
                         (acts1 ++ fst :: lst :: acts2 ++ acts_ctx)).
  {
    rewrite appA, perm_appCA with
      (s1 := fst :: lst :: nil) (s2 := acts1)
      (s3 := acts2 ++ acts_ctx); simpl.
    by rewrite perm_eq_refl.
  }
  assert (UUF: unique (sb^~ fst1) fst) by (red; eauto using eq_sym).
  assert (UUL: unique (sb lst1) lst) by (split; ins; desf; eauto using eq_sym).
  assert (S1: safe acts1 (fst :: lst :: acts2 ++ acts_ctx) lab sb rf n
                   (fst :: V) hmap' lst1
                   (with_opt res1 (fun res h ⇒ ∃ hFR' hq, h ≠ Hundef ∧ h = hq +!+ hemp +!+ hFR'
                                        ∧ assn_sem (QQ1 res) hq))).
  {
    eapply T1; ins; desf; eauto using In_appI2, In_eq, weakConsistent_perm.
      by eapply (nodup_perm _ _ _ PERM).
      eby eapply assn_sem_def.
    by rewrite hplus_emp_r.
  }

  clear PERM UUF UUL.

  assert (PERM : perm_eq (fst :: lst :: (acts1 ++ acts2) ++ acts_ctx)
                         (acts2 ++ fst :: lst :: acts1 ++ acts_ctx)).
  {
    by rewrite perm_eq_sym, <- perm_appCA with
      (s1 := fst :: lst :: acts1) (s2 := acts2)
      (s3 := acts_ctx), appA, perm_eq_refl.
  }
  assert (UUF: unique (sb^~ fst2) fst) by (red; eauto using eq_sym).
  assert (UUL: unique (sb lst2) lst) by (split; ins; desf; eauto using eq_sym).
  assert (S2: safe acts2 (fst :: lst :: acts1 ++ acts_ctx) lab sb rf n
                   (fst :: V) hmap' lst2
       (with_opt res2 (fun _ h ⇒ ∃ hFR' hq, h ≠ Hundef ∧ h = hq +!+ hFR +!+ hFR'
                                             ∧ assn_sem Q2 hq))).
  {
    eapply T2; ins; desf; eauto using In_appI2, weakConsistent_perm.
    by eapply (nodup_perm _ _ _ PERM).
  }
  clear PERM UUF UUL.
  revert S1 S2.

  assert (RNG: ∀ x, In x (fst :: V) →
               In x (fst :: acts1 ++ acts2 ++ acts_ctx)).
    by ins; desf; eauto using In_appI2.
  generalize (In_eq fst V) as INfst.
  clear H0 H2 pSAT1 T1 T2 NEQf FST UF0 UF1 UF2 SBF1 SBF2 LABF.
  revert RNG VALID HC0.
  generalize (fst :: V); clear V V_PREV NIN V_CTX; intro V; revert V;
  rename hmap' into hmap; revert hmap.
  induction n; ins; desf; unfold NW; repeat (split; ins); eauto using In_cons.
    by exfalso; rewrite !appA, !nodup_cons in *; apply RNG in IN; ins; desf; eauto.

    eapply IHn; eauto using In_appI2, In_cons.
    by ins; desf; rewrite !nodup_cons in UNIQ; desf; eauto using In_appI2.

  rewrite In_app in INcmd; desf.

  assert (ACYC: IrreflexiveHBuRF sb rf) by (red in CONS; desc; ins; eauto).
  assert (NEQ1 : lst1 ≠ a).
    by intro; subst; rewrite !nodup_cons, !In_app in UNIQ; desf; eauto using exp_sem_lst.
  assert (NEQ2 : lst2 ≠ a).
    by intro; subst; rewrite !nodup_cons, !In_app in UNIQ; desf; eauto using exp_sem_lst.

  assert (IN1: In lst1 V)
    by (assert (In lst1 (a :: V)); eauto using In_eq with hb; ins; desf).
  assert (IN2: In lst2 V)
    by (assert (In lst2 (a :: V)); eauto using In_eq with hb; ins; desf).

  clear RELY GUAR RELY0 GUAR0.

  assert (∃ hf g, hmap (hb_sb lst1 a) +!+ hmap (hb_sb lst2 a) = Hdef hf g).
  { clear IHn.
    rewrite <- hsum_two.
    change (hmap (hb_sb lst1 a) :: hmap (hb_sb lst2 a) :: nil) with
            (map hmap (hb_sb lst1 a :: hb_sb lst2 a :: nil)).
    eapply independent_heap_compat with (V := V); eauto; ins; desf; eauto.
      eby red in CONS; desf.
      eby red in CONS; desf.
      eby red in CONS; desf.
      by exact (proj1 VALID).
      by constructor; ins; intro; desf.
      eapply independent_two; eauto; ins; intro; desf; eapply ACYC, t_trans; vauto.
  }
  desf.

  red in VALID; desc; red in VALIDS; desc.

  eapply safe_final_plain with (h := hmap (hb_sb lst1 a) +!+ hmap (hb_sb lst2 a)) (ga' := ga_clear ga a);
    ins; desf; eauto.
    by apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    eapply POST in IN2; eauto.
    eapply POST0 in IN1; eauto.
    clear - CVAL IN1 IN2 H; desf.
    destruct res; ins; desf; destruct res2; ins; desf.
    rewrite hplus_emp_l in ×.
    ∃ (hFR' +!+ hFR'0), (hq +!+ hq0); rewrite IN0, IN4, !hplusA in *;
      repeat (eexists; try edone); try congruence.
    by rewrite! (hplusAC hFR').
    by intro X; rewrite (hplusAC hq0), <- hplusA, X in H.
  red; ins; desf; destruct LST; unfold NW.
  ∃ gres_emp; split.
    by unfold ga_clear; split; ins; desf.
  ∃ (lst1 :: lst2 :: nil), (next :: nil); simpl.
  assert (S: hmap (hb_sink a) = hemp) by (eapply RESTR; eauto).
  rewrite hsum_one, hsum_two; unfold mupd; desf; desf.
  repeat split; ins; desf; eauto.
    by repeat econstructor; red; ins; desf.
    by edestruct UL0; desf; eauto.
  by rewrite H, S, hplus_emp_r.
  by rewrite S, !hplus_emp_r.

  specialize (GUAR0 _ INcmd NIN HC'); desf.
  repeat (eexists; try edone); eapply IHn; eauto using In_appI1, In_cons.
  by ins; desf; rewrite !nodup_cons in UNIQ; desf; eauto using In_appI1, In_appI2.

  specialize (GUAR _ INcmd NIN HC'); desf.
  repeat (eexists; try edone); eapply IHn; eauto using In_appI1, In_cons.
  by ins; desf; rewrite !nodup_cons in UNIQ; desf; eauto using In_appI1, In_appI2.

  Grab Existential Variables. done.
Qed.

Theorem rule_repeat PS PSg :
  ∀ (P: assn PS PSg) e QQ (T: triple P e QQ) (IMP: implies (QQ 0) P),
    triple P (Erepeat e) (fun x ⇒ if x == 0 then Afalse else QQ x).
Proof.

  ins; red; intros until 1; simpls; desf; clear NODUP.
  revert fst resI actsI lstI GET_F ESEM REP GET_I.
  induction sems; ins; desf; ins.
rewrite flatten_cons, appA in ×.

  assert (N : ∃! next, sb lstI next).
    clear IHsems CONS UNIQ.
    destruct sems as [|[[[??]?]?]]; ins; desf; eauto.
    by exploit (REP nil); ins; desf; eexists; split; eauto using eq_sym.
  destruct N as [next' N].

  assert (RNG: ∀ x, In x V → In x (actsI ++ acts_ctx))
    by eauto using In_appI2.

  assert (S := ESEM _ _ _ _ (In_eq _ _)); apply T in S.
  exploit S; clear S; eauto using In_appI2.
  instantiate (1 := n).
  clear prev FST V_PREV pDEF pEQ V_CTX.
  revert V hmap HC VALID RNG.
  induction n; ins; desf; unfold NW; repeat split; ins.

  clear RELY GUAR IHn IHsems CONS.
  assert (lstI = lst ∧ res = resI).
    destruct (lastP sems); ins; desf.
    rewrite last_snoc in *; desf.
    rewrite snocE, map_app, !map_cons, flatten_app, flatten_cons in UNIQ; ins.
    rewrite snocE in ×.
    assert (M := ESEM _ _ _ _ (In_cons _ (In_appI2 (In_eq _ _) s))).
    apply exp_sem_lst in M; apply RNG in IN.
    exfalso; clear -IN UNIQ M.
    by rewrite ?nodup_app, ?In_app in *; desf; eauto using In_appI1, In_appI2.
  by subst; destruct res; ins; desf; subst; ins; apply POST.

  by eapply IHn, RELY; ins; desf; eauto using In_appI2.

  rewrite In_app in INcmd; desf.
    by exploit GUAR; eauto; ins; desf; repeat (eexists; try edone);
       eapply IHn; ins; desf; eauto using In_appI1.

  clear RELY GUAR IHn.
  destruct sems as [|[[[resJ actsJ]fstJ]lstJ]]; ins.
  rewrite flatten_cons in ×.
  eapply weakConsistent_Permutation in CONS; [|apply Permutation_app_comm].
  rewrite appA in UNIQ; eapply Permutation_NoDup in UNIQ; [|apply Permutation_app_comm].
  rewrite !appA in ×.
  exploit (REP nil); ins; desf.
  clear next' N.
rewrite H0 in *; clear H0.
  specialize (IHsems fstJ resJ actsJ lstJ eq_refl).
  assert (ESEM0 := (ESEM _ _ _ _ (or_introl eq_refl))).
  specialize (fun r a f l H ⇒ ESEM r a f l (or_intror H)).
  assert (a = fstJ); subst.
    assert (clos_refl_trans _ sb fstJ a).
      clear - REP INcmd ESEM.
      rewrite In_app in *; desf; eauto using exp_sem_fst_reach.
      assert (R := (ESEM _ _ _ _ (or_introl eq_refl))).
      eapply exp_sem_fst_reach in R; [|by eapply exp_sem_lst, R].
      specialize (fun r a f l H ⇒ ESEM r a f l (or_intror H)).
      specialize (fun p r1 a1 f1 l1 r2 a2 f2 l2 s H ⇒
        REP (_ :: p) r1 a1 f1 l1 r2 a2 f2 l2 s (f_equal (cons _) H)); simpls.
      eapply rt_trans; eauto; clear R.
      revert resJ actsJ fstJ lstJ REP; induction sems as [|[[[r a']f]l]]; ins.
      rewrite flatten_cons, In_app in *; desf.
        exploit (REP nil); ins; desf.
        by eapply rt_trans with f; eauto using exp_sem_fst_reach, rt_step.
      exploit (REP nil); ins; desf.
        eapply rt_trans with f; eauto using exp_sem_fst_reach, rt_step.
        eapply rt_trans with l; eauto 7 using exp_sem_fst_reach, exp_sem_lst.
        eapply IHsems; ins; eauto.
        by eapply (REP (_ :: _)); ins; f_equal; apply H.
    assert (In fstJ actsJ) by eauto using exp_sem_fst.
    assert (Z: In fstJ (a :: V)) by eauto using hist_closed_trans, In_eq.
    ins; desf; apply RNG, In_app in Z.
    exfalso; clear - H0 Z UNIQ; rewrite nodup_app in UNIQ.
    by desf; eauto using In_appI1, In_appI2.
  assert (In lstI V).
    assert (In lstI (fstJ :: V)) by eauto using In_eq with hb.
    by ins; desf; exfalso; clear - CONS SB; red in CONS; desc; eauto with hb.
  exploit POST; clear POST; try edone; ins; desf.

  exploit IHsems; clear IHsems; rewrite ?appA; eauto using f_equal.
    eby ins; eapply (REP (_ :: prefix)); ins; f_equal.
    by split; eauto using eq_sym.
    by clear - RNG; intros ? X; eapply RNG in X; rewrite In_app in *; tauto.
  instantiate (1 := S n); ins; desf.
  exploit (GUAR fstJ); clear POST RELY GUAR; ins; desf.

  ∃ hmap'; repeat (split; try edone).
  eapply conseq_helper, safe_mod; try exact SAFE; eauto using In_appI1.
    ins; desc; ∃ (hFR' +!+ hFR'0), hq0; repeat (split; try edone).
    by rewrite hplusA in H1.
  ins; rewrite In_app in IN; desf.
  by destruct NIN0; right; eapply hist_closed_trans; eauto using exp_sem_lst_reach.
Qed.

Require Import permission.

Theorem rule_alloc_na PS PSg :
  triple (@Aemp PS PSg) (Ealloc) (fun x ⇒ @Aptu PS PSg x).
Proof.
  eapply triple_helper_start; ins; desf; ins.
  destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
  rewrite hplus_emp_l in ×.

  assert (hFR l = HVnone). {
    apply NNPP; intro NEQ.
    red in CONS; desc; ins.
    eapply (heap_loc_allocated (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                       Crf HC (proj1 VALID) (hb_sb _ _) (proj1 FST)) in NEQ;
      ins; desc; eauto.
    assert (c = fst) by eauto; subst.
    by apply clos_refl_trans_hbUrfE in NEQ0; desf; eauto with hb.
  }

  red in VALID; desc; red in VALIDS; desc.

  eapply safe_final_plain with (h := Hdef (hupd hFR l (HVuval HLnormal)) g) (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    eexists hemp, (hsingl _ _ l (HVuval HLnormal)); repeat split; try edone.
    rewrite hplus_emp_r, hplus_unfold; desf; ins.
      by rewrite gres_plus_total_emp_l; f_equal; extensionality y; [unfold hupd; desf; ins; desf].
    by rewrite gres_plusC, gres_plus_emp_r in n0; destruct n0; split; intro; unfold hupd; desf; ins; desf.
  red; rewrite SEM1.
  ∃ gres_emp; split.
    by unfold ga_clear; split; ins; desf.
  eexists _, _, hFR, g; repeat (split; try edone).
  by rewrite mupdo; try red; ins; desf.
  by rewrite mupds.
  by rewrite mupds, hplus_emp_r; eauto.
Qed.

Program Definition Apt_full PS PSg Perm (IN: In Perm PS) l v := @Apt PS PSg Perm IN (Pfull Perm) _ l v.
Next Obligation. split; [apply Pfull_is_not_Pundef | apply Pfull_is_not_Pzero]. Qed.

Theorem rule_store_na1 PS PSg :
  ∀ typ E E' E'' Perm Perm' (IN: In Perm PS) (IN': In Perm' PS),
  triple (Apt_full PS PSg Perm IN E E') (Estore typ E E'') (fun x ⇒ Apt_full PS PSg Perm' IN' E E'').
Proof.
  intros; eapply triple_helper_start; ins; desf; ins.

  destruct hFR as [|hFR gFR]; [by rewrite pEQ, hplusC in pDEF|].

  assert (EQ: hsingl _ _ E (lvalue _ _ Perm E') +!+ Hdef hFR gFR = Hdef (hupd hFR E (lvalue _ _ Perm E')) gFR).
  {
    clear - pDEF pEQ; rewrite hplus_unfold in *; desf; desf.
    × rewrite gres_plus_total_emp_l.
      f_equal; extensionality y; specialize (HEAPcompat y); clear pEQ.
      unfold hupd in *; desf; ins; desf; desf.
      eby exfalso; red in p; desf; rewrite permission_plusA in PSUMdef;
          apply nonextendable_full_permission in PSUMdef;
          pplus_eq_zero; eapply all_permissions_zero.
    × destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r.
      split; ins; specialize (HEAPcompat v); desf; unfold hupd in *; desf; desf.
  }

  red in VALID; desc; red in VALIDS; desc.

  eapply safe_final3 with (h := Hdef (hupd hFR E (lvalue _ _ Perm' E'')) gFR) (ga' := ga_clear ga fst); eauto; ins.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
  × ∃ hemp, (hsingl _ _ E (lvalue _ _ Perm' E'')); repeat split; try edone.
      2: by clear; f_equal; extensionality x; unfold hupd; desf; desf; eapply HVval_equal; eq_rect_simpl.
    symmetry; revert EQ; clear; rewrite hplus_emp_r, !hplus_unfold; ins; desf; desf.
      rewrite gres_plus_total_emp_l.
      f_equal; extensionality y; specialize (HEAPcompat y); specialize (HEAPcompat0 y).
      apply (f_equal (fun f ⇒ f y)) in H1; unfold hupd in *; desf; ins; desf; desf.
      by eapply HVval_equal; eq_rect_simpl; pplus_zero_simpl; try done;
         red in HEAPcompat1; desf; rewrite permission_plusA in PSUMdef;
         apply nonextendable_full_permission in PSUMdef; pplus_eq_zero;
         pplus_zero_simpl.
    destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r; split; try done.
    intro y; specialize (HEAPcompat y).
    apply (f_equal (fun f ⇒ f y)) in H1; unfold hupd in *; desf; ins; desf; desf.
    exfalso; clear H1.
      eq_rect_simpl.
      eby red in p; desf; rewrite permission_plusA in PSUMdef;
          apply nonextendable_full_permission in PSUMdef;
          pplus_eq_zero; eapply all_permissions_zero.
    eq_rect_simpl.
    eby red in HEAPcompat0; desf; rewrite permission_plusA in PSUMdef;
          apply nonextendable_full_permission in PSUMdef;
          pplus_eq_zero; eapply all_permissions_zero.
  × red; ins; desf; unfold NW.
    ∃ gres_emp; split.
      by unfold ga_clear; split; ins; desf.
    eexists prev, next, (hupd hFR E (lvalue _ _ Perm E')), gFR.
    repeat split; try done; try (by apply LST); try (by apply FST);
      try left; repeat split; unfold mupd, hupd; ins; desf; desf.
    + rewrite pEQ, hplus_unfold in *; clear - pDEF; desf. f_equal.
        2: by rewrite gres_plus_total_emp_l.
      extensionality x; desc; specialize (HEAPcompat x); unfold hupd in *; desf; desf; ins; desf; desf.
      by eapply HVval_equal; eq_rect_simpl.
      eby exfalso; red in p; desf; rewrite permission_plusA in PSUMdef;
          apply nonextendable_full_permission in PSUMdef;
          pplus_eq_zero; eapply all_permissions_zero.
    + ∃ Perm'; rewrite hplus_emp_r; f_equal; extensionality y; desf; desf.
    + eapply RESTR; eauto.
    + eapply RESTR; eauto.

  Grab Existential Variables. all: done.
Qed.

Theorem rule_store_na2 PS PSg :
  ∀ typ E E'' Perm (IN: In Perm PS),
  triple (@Aptu PS PSg E) (Estore typ E E'') (fun x ⇒ Apt_full PS PSg Perm IN E E'').
Proof.
  intros; eapply triple_helper_start; ins; desf; ins.

  destruct hFR as [|hFR gFR]; [by rewrite pEQ, hplusC in pDEF|].

  assert (EQ: hsingl _ _ E (HVuval HLnormal) +!+ Hdef hFR gFR = Hdef (hupd hFR E (HVuval HLnormal)) gFR).
  {
    clear - pDEF pEQ; rewrite hplus_unfold in *; desf; desf.
    rewrite gres_plus_total_emp_l.
    f_equal; extensionality y; specialize (HEAPcompat y); clear pEQ; unfold hupd in *; desf; ins; desf.
  }

  red in VALID; desc; red in VALIDS; desc.

  eapply safe_final3 with (h := Hdef (hupd hFR E (lvalue _ _ Perm E'')) gFR) (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
  × ∃ hemp, (hsingl _ _ E (lvalue _ _ Perm E'')); repeat split; try edone.
      2: by clear; f_equal; extensionality x; unfold hupd; desf; desf; eapply HVval_equal; eq_rect_simpl.
    symmetry; revert EQ; clear; rewrite hplus_emp_r, !hplus_unfold; ins; desf; desf.
      rewrite gres_plus_total_emp_l.
      f_equal; extensionality y; specialize (HEAPcompat y); specialize (HEAPcompat0 y).
      by apply (f_equal (fun f ⇒ f y)) in H1; unfold hupd in *; desf; ins; desf.
    destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r; split; try done.
    intro y; specialize (HEAPcompat y).
    apply (f_equal (fun f ⇒ f y)) in H1; unfold hupd in *; desf; ins; desf.
  × red; ins; desf; unfold NW.
    ∃ gres_emp; split.
      by unfold ga_clear; split; ins; desf.
    eexists prev, next, (hupd hFR E (HVuval HLnormal)), gFR.
    repeat split; try done; try (by apply LST); try (by apply FST);
      try left; repeat split; unfold mupd, hupd; ins; desf; desf.
    + rewrite pEQ, hplus_unfold in *; clear - pDEF; desf; desf. f_equal.
        2: by rewrite gres_plus_total_emp_l.
      extensionality x; specialize (HEAPcompat x); unfold hupd in *; desf; desf; ins; desf; desf.
    + by ∃ Perm; rewrite hplus_emp_r; f_equal; extensionality y; desf; desf.
    + eapply RESTR; eauto.
    + eapply RESTR; eauto.

  Grab Existential Variables. done.
Qed.

Theorem rule_load_na PS PSg :
  ∀ typ Perm (IN: In Perm PS) p E E' (NONZERO: p ≠ Pzero Perm) (DEF: p ≠ Pundef Perm),
  triple (@Apt PS PSg Perm IN p (conj DEF NONZERO) E E') (Eload typ E)
            (fun x ⇒ if x == E' then @Apt PS PSg Perm IN p (conj DEF NONZERO) E E' else @Afalse PS PSg).
Proof.
  intros; eapply triple_helper_start; ins.
  rewrite pSAT in *; clear pSAT; desf.

  destruct hFR as [|hFR gFR]; [by rewrite pEQ, hplusC in pDEF|].

  assert (EQ: ∃ p' pT pNbl PERM,
                hmap (hb_sb prev fst) = Hdef (hupd hFR E (HVval E' Perm (p ## p') pT pNbl PERM)) gFR).
  {
    clear - pDEF pEQ; rewrite hplus_unfold in *; desf; desf; clear pDEF.
    rewrite gres_plus_total_emp_l in pEQ.
    assert (HE := HEAPcompat E); rewrite hupds in HE; ins; desf; desf.
    × repeat eexists; rewrite pEQ.
      f_equal; extensionality l.
      unfold hupd; desf; desf; ins; desf.
      eapply HVval_equal; eq_rect_simpl; try edone.
      by rewrite permission_plus_zero_r.
    × repeat eexists; rewrite pEQ.
      f_equal; extensionality l.
      unfold hupd; desf; desf; ins; desf.
      eby eapply HVval_equal; eq_rect_simpl.
      by destruct n; eq_rect_simpl.
  }

  desf.

  assert (M: v = E'); desf; ins.
  {
    exploit heap_loc_na_initialized2; try exact HC; eauto; ins; try eapply FST;
      try (eby red in CONS; red in VALID; desc; eauto); try (by rewrite hupds); desc.

    red in CONS; desc; ins.
    assert (CONS_RF := Crf).
    specialize (Crf fst); des_if; desc.
    {
      rewrite SEM1 in *; ins; desc; subst.
      cut (a = c); [by intro; subst; clear - Crf0 x1; destruct (lab c); ins; desf; omega | ].

      assert (INa: In a V).
        by destruct (HC0 _ (In_eq _ _) a); clarify; auto using hc_edge;
              edestruct ACYC; eauto with hb.

      red in VALID; desc; assert (V' := VALIDS); red in V'; desc.

      destruct (valid_writeD (VLD _ INa)) as [aprev AA]; eauto; desc.

      replace (loc (lab a)) with l in × by (destruct (lab a); ins; desf).

      destruct AA1 as [LVAL | AT].
      Focus 2.         exfalso; clear HC0; eapply atomicity_is_globally_exclusive; try exact AT; try exact EQ; eauto; ins.
        by eapply HC; vauto.
        by exact (proj1 FST).
        by rewrite hupds.

      assert (HBa: a = prev ∨ happens_before_union_rf sb rf a prev).
      {
        clear x4.
        apply NNPP; intro NHB; unfold unique in *; apply not_or_and in NHB; desc.
        assert (IND: independent sb rf (hb_sb aprev a :: hb_sb prev fst :: nil)).
          by eapply independent_two; ins; eauto; intro; desf; eauto with hb.
        eapply independent_heap_compat in IND; try exact HC; try exact (proj1 VALID); eauto;
          try (by ins; desf; eauto with hb).
          2: by constructor; ins; intro; desf.
        desc; ins; rewrite hsum_two, AA0, EQ, hplusC, hplus_unfold in IND; des_if; clarify; desc.
        specialize (HEAPcompat l); rewrite hupds in *; simpls; desf; ins; desf.
        by rewrite permission_plusC in HEAPcompat0; red in HEAPcompat0; desf; rewrite permission_plusA in PSUMdef;
           apply nonextendable_full_permission in PSUMdef; pplus_eq_zero.
      }

      assert (HBc: happens_before_union_rf sb rf c fst) by (destruct FST; desf; eauto with hb).

      assert (INc: In c V) by (exploit (hist_closedD HC0 HBc); ins; clear HBa; desf; eauto with hb).

      edestruct (two_access_cases (PS := PS) (PSg := PSg) cpre c a) with (V := V);
        eauto; try (by desf; eauto using hist_closedD).
        by destruct (lab c); ins; desc; congruence.
        by destruct (lab a), (lab c); ins; desc; congruence.

      unfold not in *; destruct H; exfalso; [by desf; eauto|].

      assert (happens_before lab sb rf mo a c).
      {
        exploit connection_to_lvalue; try exact LVAL; try exact x2; try exact VALIDS; try exact AA0; eauto.
          by intro; subst; eauto with hb.
          by exploit (hist_closedD HC0 HBc); ins; clear HBa; desf; eauto with hb.
          by eapply HC; vauto.
          by intro U; rewrite U in ×.
        intro PATH; desc; destruct PATH as [PATH | PATH]; eapply hb_from_path in PATH; ins; eauto.
        × clear - PATH x0; apply clos_refl_trans_hbE in PATH; desf; eauto with hb.
        × exfalso; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC).
          eapply happens_before_union_rf_trans; eauto.
          apply clos_refl_trans_hbE in PATH; destruct PATH as [HB | HB].
          by eapply hb_implies_hbUrf, happens_before_trans; eauto with hb.
          by clarify; eauto with hb.
      }

      assert (happens_before lab sb rf mo c fst).
      {
        red in FST; desc.
        exploit connection_to_lvalue; try exact x3; try exact EQ; try exact VALIDS; try exact x2; eauto;
          try (by rewrite hupds).
          by intro; subst; eauto with hb.
          by eapply HC; vauto.
          by rewrite hupds; ins; intro; pplus_eq_zero; congruence.
        intro PATH; desc; destruct PATH as [PATH | PATH]; eapply hb_from_path in PATH; ins; eauto.
        × clear - PATH FST; apply clos_refl_trans_hbE in PATH; desf; eauto with hb.
        × clear - HBc PATH x0 ACYC; exfalso; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC).
          eapply happens_before_union_rf_trans; eauto.
          apply clos_refl_trans_hbE in PATH; destruct PATH as [HB | HB].
          by eapply hb_implies_hbUrf, happens_before_trans; eauto with hb.
          by clarify; eauto with hb.
      }

      eapply (Cwr c); try apply Heq; try by desf; eauto with hb.
        by rewrite SEM1; destruct (lab c); ins; desf.
       eapply Cmo; eauto.
   }
   edestruct (Crf c); try rewrite SEM1; ins; instantiate; try rewrite addn0; eauto.
   red in FST; desc.
   exploit connection_to_lvalue; try exact x3; try exact EQ; try exact (proj1 VALID); try exact x2; eauto;
     try by rewrite hupds.
     { clear - ACYC FST x4.
       intro; subst; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC); desf; vauto.
       eapply happens_before_union_rf_trans; vauto.
     }
     { clear - x0 x4 HC V_PREV; desf.
       by eapply HC; vauto.
       by eapply hist_closedD; eauto with hb.
     }
     by rewrite hupds; ins; intro; pplus_eq_zero; congruence.
   intro PATH; desc; destruct PATH as [PATH | PATH]; eapply hb_from_path in PATH; ins; eauto.
   × clear - PATH FST; apply clos_refl_trans_hbE in PATH; desf; eauto with hb.
   × clear - PATH FST x0 x4 ACYC; exfalso; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC).
     apply clos_refl_trans_hbE in PATH; desf; try apply hb_implies_hbUrf in PATH; eauto 6 with hb.
  }
  
  assert (PERM': permissionsOK p (Pzero Perm) (Pzero Perm)) by (split; pplus_zero_simpl; done).
  red in VALID; desc; red in VALIDS; desc.
  eapply safe_final_plain2 with (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
  {
    instantiate (1 := hmap (hb_sb prev fst)); rewrite EQ.
    ∃ hemp, (hsingl _ _ E (HVval E' Perm p (Pzero Perm) (Pzero Perm) PERM')).
    rewrite eqxx, hplus_emp_r; repeat split; try done.
    × rewrite EQ, hplus_unfold in *; clear - pEQ; desf.
      + rewrite gres_plus_total_emp_l; f_equal; extensionality x; unfold hupd in *; desf; desf.
        specialize (HEAPcompat0 E); apply equal_f with (x := E) in H1.
        assert (EQ: hFR E = HVnone ∨ ∃ nrm tri nab OK, hFR E = HVval E' Perm nrm tri nab OK).
          by clear - HEAPcompat0; rewrite eqxx in *; ins; desf; desf; eauto 10.
        by rewrite eqxx in *; desf; rewrite EQ in *; ins; desf; eapply HVval_equal; eq_rect_simpl.
      + desf; destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r; split; try done.
        desc; clear - HEAPcompat; ins; specialize (HEAPcompat v).
        unfold hupd in *; desf; desf.
    × ins; clear; f_equal.
      extensionality x; unfold hupd; desf; desf.
      by eapply HVval_equal; eq_rect_simpl.
  }

  red; ins; desf; unfold NW.
  ∃ gres_emp; split.
      by unfold ga_clear; split; ins; desf.
  eexists prev, next, (hupd hFR E (HVval E' Perm (p ## p') pT pNbl PERM)), gFR.
  repeat split; try done; try (by apply LST); try (by apply FST);
  unfold mupd; desf; desf.
  left; repeat (eexists; try edone); unfold hupd; ins; desf; desf.
  by split; [ | intro; pplus_eq_zero; congruence].
  by rewrite hplus_emp_r.
  by eapply RESTR; eauto; ins; right; split; eauto; intro SB; red in SB; desf.
  by eapply RESTR; eauto.

  Grab Existential Variables.
  all: try done.
  by split; pplus_zero_simpl.
Qed.