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

Set Implicit Arguments.

Lemma clos_rt_inclusion A R Q:
  inclusion A R Q → inclusion A (clos_refl_trans A R) (clos_refl_trans A Q).
Proof.
  unfold inclusion; ins.
  induction H0; vauto.
  apply rt_step; eauto.
Qed.

Lemma clos_t_inclusion A R Q:
  inclusion A R Q → inclusion A (clos_trans A R) (clos_trans A Q).
Proof.
  unfold inclusion; ins.
  induction H0; vauto.
  apply t_step; eauto.
Qed.

Lemma release_seq_implies_hbUrf lab sb rf mo a b:
  release_seq lab sb rf mo a b →
  clos_refl_trans _ (happens_before_union_rf sb rf) a b.
Proof.
  induction 1; vauto.
    by apply rt_step; vauto.
  by eapply rt_trans, rt_step; vauto.
Qed.

Lemma hb_implies_hbUrf lab sb rf mo a b:
  happens_before lab sb rf mo a b →
  happens_before_union_rf sb rf a b.
Proof.
  ins; induction H; eauto with hb.
  red in H; desf; vauto.
  red in H; desf.
  × eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H1; desf; vauto.
    eapply happens_before_union_rf_trans; vauto.
  × apply clos_refl_transE in H1; eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H2; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
  × apply clos_refl_transE in H1; eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H2; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
  × apply clos_refl_transE in H1; apply clos_refl_transE in H2;
    eapply release_seq_implies_hbUrf, clos_refl_trans_hbUrfE in H3; desf; vauto;
    repeat (eapply happens_before_union_rf_trans; vauto; try by eapply clos_t_inclusion; eauto; vauto).
Qed.

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 :
  ∀ e QQ (T: triple Atrue 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) (pre :: nil)).
    {
      split; ins.
      unnw; red; ins; desf.
      red; rewrite pL; unfold not in ×.
      ∃ nil, (fst :: nil), (fun _ ⇒ HVnone); repeat (split; ins);
        desf; eauto using eq_sym.
      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) as hmap, acts´ as acts.
      induction n; ins; desf.
      destruct (classic (acts = nil)); subst; ins.
        ∃ hmap,; 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.
        + unnw; red; ins; eapply (proj1 VALID); desf; find_in_list.
        + unnw; ins; apply ((proj2 VALID) 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,; 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 :
  ∀ P 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 :
  ∀ acts_cmd acts_ctx lab sb rf n (hmap : hbcase → heap) (V : list actid) lst res (Q Q´ : nat → heap → 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 :
  ∀ P 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 :
  ∀ P1 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 :
  ∀ PP 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 v QQ :
  triple (QQ v) (Evalue v) QQ.
Proof.
  eapply triple_helper_start; ins; desf; ins; desf.
  eapply safe_final_plain; eauto.
    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.

  eexists (prev :: nil), (next :: nil), hf0.
  ins; rewrite !hsum_one; repeat (split; ins; desf); eauto;
    unfold mupd; desf; try congruence.
  rewrite pDEF.
  cut (hmap (hb_sink fst) = hemp).
    by intro E; rewrite E; rewrite hplus_emp_r.
  eapply (proj2 VALID); eauto.
Qed.

Theorem rule_let :
  ∀ P 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.
    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 :
  ∀ P1 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).
  {
    ∃ (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).
    × red; rewrite LABF.
      eapply hdef_alt in pDEF; desfh.
      ∃ (prev :: nil), (fst1 :: fst2 :: nil), hf.
      ins; rewrite hsum_one, hsum_two; desf; desfh.
      unfold unique in *; des.
      repeat split; ins; des; subst; try done; eauto.
      by repeat econstructor; red; ins; desf.
      by eapply UF0 in H; desf; vauto.
      rewrite <- pDEF, pEQ, hplusA.
      cut (hmap (hb_sink e) = hemp).
        by intro E; rewrite E; rewrite hplus_emp_r.
      eapply (proj2 VALID); eauto.
    × by do 2 (eapply valid_ext; eauto); apply (proj1 VALID).
    × eapply (proj2 VALID (hb_fst edge)); eauto.
    × eapply (proj2 VALID 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, hmap (hb_sb lst1 a) +!+ hmap (hb_sb lst2 a) = Hdef hf).
  { 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.

  eapply safe_final_plain with (h := hmap (hb_sb lst1 a) +!+ hmap (hb_sb lst2 a));
    ins; desf; eauto.
    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.
  ∃ (lst1 :: lst2 :: nil), (next :: nil), hf; simpl.
  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.
  rewrite H.
  cut (hmap (hb_sink a) = hemp).
    by intro E; rewrite E; rewrite hplus_emp_r.
  eapply (proj2 VALID); eauto.

  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. edone.
Qed.

Theorem rule_repeat :
  ∀ P 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,; 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.

Theorem rule_alloc_na :
  triple (Aemp) (Ealloc) (fun x ⇒ Aptu 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.
    assert (c = fst) by eauto; subst.
    by apply clos_refl_trans_hbUrfE in NEQ0; desf; eauto with hb.
  }

  eapply safe_final_plain with (h := Hdef (hupd hFR l (HVuval HLnormal))); eauto.
    ∃ hemp; repeat eexists; try edone.
    rewrite hplus_emp_r, hplus_unfold; desf; ins.
      by f_equal; extensionality y; unfold hupd; desf; ins; desf.
    by destruct n0; intro; unfold hupd; desf; ins; desf.
  red; rewrite SEM1.
  eexists,,hFR; repeat (split; try edone); auto using mupds; unfold NW.
  rewrite mupdo; try red; ins; desf.
Qed.

Theorem rule_store_na1 :
  ∀ typ E E´ E´´,
  triple (Apt E E´) (Estore typ E E´´) (fun x ⇒ Apt E E´´).
Proof.
  intros; eapply triple_helper_start; ins; desf; ins.

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

  assert (EQ: hsingl E (HVval E´ HLnormal) +!+ Hdef hFR = Hdef (hupd hFR E (HVval E´ HLnormal))).
  {
    clear - pDEF pEQ; rewrite hplus_unfold in *; desf.
    by f_equal; extensionality y; specialize (h y); clear pEQ;
       unfold hupd in *; desf; ins; desf.
  }

  eapply safe_final3 with (h := Hdef (hupd hFR E (HVval E´´ HLnormal))); eauto.
  × ∃ hemp.
    repeat eexists; try edone.
    symmetry; revert EQ; clear; rewrite hplus_emp_r, !hplus_unfold; ins; desf.
      f_equal; extensionality y; specialize (h y); specialize (h0 y).
      by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
    destruct n; intro y; specialize (h y).
    by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
  × red; ins; desf; unfold NW.
    eexists prev, next,(hupd hFR E (HVval E´ HLnormal)).
    repeat split; try done; try (by apply LST); try (by apply FST);
      try left; repeat split; unfold mupd, hupd; ins; desf; desf.
    by rewrite pEQ, EQ; f_equal; extensionality y; desf; desf.
    by f_equal; extensionality y; desf; desf.
    by eapply (proj2 VALID); eauto.
    by eapply (proj2 VALID); eauto.
Qed.

Theorem rule_store_na2 :
  ∀ typ E E´´,
  triple (Aptu E) (Estore typ E E´´) (fun x ⇒ Apt E E´´).
Proof.
  intros; eapply triple_helper_start; ins; desf; ins.

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

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

  eapply safe_final3 with (h := Hdef (hupd hFR E (HVval E´´ HLnormal))); eauto.
  × ∃ hemp.
    repeat eexists; try edone.
    symmetry; revert EQ; clear; rewrite hplus_emp_r, !hplus_unfold; ins; desf.
      f_equal; extensionality y; specialize (h y); specialize (h0 y).
      by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
    destruct n; intro y; specialize (h y).
    by apply (f_equal (fun f ⇒ f y)) in H0; unfold hupd in *; desf; ins; desf.
  × red; ins; desf; unfold NW.
    eexists prev, next,(hupd hFR E (HVuval HLnormal)).
    repeat split; try done; try (by apply LST); try (by apply FST);
      try left; repeat split; unfold mupd, hupd; ins; desf; desf.
    by rewrite pEQ, EQ; f_equal; extensionality y; desf; desf.
    by f_equal; extensionality y; desf; desf.
    by eapply (proj2 VALID); eauto.
    by eapply (proj2 VALID); eauto.
Qed.

Theorem rule_load_na :
  ∀ typ E E´,
  triple (Apt E E´) (Eload typ E)
            (fun x ⇒ if x == E´ then Apt E E´ else Afalse).
Proof.
  intros; eapply triple_helper_start; ins; subst.

  destruct hFR as [|hFR]; [by rewrite pEQ, hplusC in pDEF|].
  assert (EQ: hsingl E (HVval E´ HLnormal) +!+ Hdef hFR = Hdef (hupd hFR E (HVval E´ HLnormal))).
  {
    clear - pDEF pEQ; rewrite hplus_unfold in *; desf.
    by f_equal; extensionality y; specialize (h y); clear pEQ;
       unfold hupd in *; desf; ins; desf.
  }

  rewrite EQ in *; 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.

      destruct (valid_accessD _ _ _ _ _ ((proj1 VALID) _ INa)) as [aprev AA]; eauto; desc.

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

      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).
          desc; ins; rewrite hsum_two, AA0, pEQ, hplusC, hplus_unfold in IND;
          des_if; clarify.
          by specialize (h0 l); rewrite hupds in *; simpls; desf.
        by constructor; ins; intro; desf.
      }

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

      edestruct (two_access_cases cpre c a) with (V := V); eauto; try (by desf; eauto using hist_closedD).
        by exact (proj1 VALID).
        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 (nonatomics_strongly_connected FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                               CONS_RF Ca HC (proj1 VALID) aprev (b1 := a) cpre (b2 := c)); eauto.
          by intro; subst; eauto with hb.
          by exploit (hist_closedD HC0 HBc); ins; clear HBa; desf; eauto with hb.
          { eapply (hist_closedD HC); try exact V_PREV.
            destruct x4; eauto with hb; vauto.
          }
          by intro U; rewrite U in ×.
        intro HB; destruct HB as [HB | HB].
        × clear - HB x0; apply clos_refl_trans_hbE in HB; desf; eauto with hb.
        × exfalso; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC).
          eapply happens_before_union_rf_trans; eauto.
          apply clos_refl_trans_hbE in HB; destruct HB 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 (nonatomics_strongly_connected FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                               CONS_RF Ca HC (proj1 VALID) cpre (b1 := c) prev (b2 := fst)); eauto;
          try by rewrite hupds.
          by intro; subst; eauto with hb.
          by exploit (hist_closedD HC0 HBc); ins; clear HBa; desf; eauto with hb.
          by intro U; rewrite U in ×.
        intro HB; destruct HB as [HB | HB].
        × clear - HB FST; apply clos_refl_trans_hbE in HB; desf; eauto with hb.
        × clear - HBc HB x0 ACYC; exfalso; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC).
          eapply happens_before_union_rf_trans; eauto.
          apply clos_refl_trans_hbE in HB; destruct HB 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 (nonatomics_strongly_connected FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                               CONS_RF Ca HC (proj1 VALID) cpre (b1 := c) prev (b2 := fst)); 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 intro U; rewrite U in ×.
   intro HB; destruct HB as [HB | HB].
   × clear - HB FST; apply clos_refl_trans_hbE in HB; desf; eauto with hb.
   × clear - FST HB x0 x4 ACYC; exfalso; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC).
     apply clos_refl_trans_hbE in HB; desf; try apply hb_implies_hbUrf in HB; eauto 6 with hb.
  }

  eapply safe_final_plain2; eauto.
    instantiate (1 := Hdef (hupd hFR E (HVval E´ HLnormal))).
    by ∃ hemp; rewrite eqxx; repeat eexists; rewrite ?hplus_emp_r; try done.

  red; ins; desf; unfold NW.
  eexists prev, next,(hupd hFR E (HVval E´ HLnormal)).
  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 eapply (proj2 VALID); eauto; ins; right; split; eauto; intro SB; red in SB; desf.
  by eapply (proj2 VALID); eauto.

  Grab Existential Variables. edone.
Qed.

Theorem rule_alloc_atom_acq QQ :
  triple (Aemp) (Ealloc) (fun x ⇒ Astar (Arel x QQ) (Aacq x QQ)).
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.
    assert (c = fst) by (eby eapply Ca).
    by apply clos_refl_trans_hbUrfE in NEQ0; desf; eauto with hb.
  }

  pose (QQ´ := fun x ⇒ mk_assn_mod (QQ x)).
  assert (EQ : ∀ isrmw,
    hsingl l (HVra QQ´ Remp false (Some HLCnormal) None) +!+
    hsingl l (HVra Wemp QQ´ isrmw None None) =
    hsingl l (HVra QQ´ QQ´ isrmw (Some HLCnormal) None)).
  {
    clear; intro; rewrite hplus_unfold; desf.
      f_equal; extensionality y; specialize (h y); unfold hupd in *; desf; ins; desf; ins.
      by f_equal; extensionality v; desf; specialize (h v); desf; ins;
         eapply assn_mod_eqI1; ins; try rewrite e; Asim_simpl.
      by f_equal; extensionality v; desf; specialize (h v); desf; ins;
         eapply assn_mod_eqI; ins; try rewrite e; Asim_simpl.
    by destruct n; intro; unfold hupd; desf; split; ins; vauto; destruct isrmw; vauto.
  }

  eapply safe_final_plain with (h := Hdef (hupd hFR l (HVra QQ´ QQ´ false (Some HLCnormal) None))); eauto.
    subst QQ´; ∃ hemp; repeat eexists; try edone; instantiate; rewrite ?hplus_emp_r, EQ; try done.
    rewrite hplus_unfold; desf; ins.
      by f_equal; extensionality y; unfold hupd; desf; ins; desf.
    by destruct n0; intro; unfold hupd; desf; ins; desf.
  red; rewrite SEM1.
  eexists,,hFR; repeat (split; try edone); eauto using mupds; unfold NW.
  rewrite mupdo; try red; ins; desf.
Qed.

Theorem rule_alloc_atom_rmwacq QQ :
  triple (Aemp) (Ealloc) (fun x ⇒ Astar (Arel x QQ) (Armwacq x QQ)).
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.
    assert (c = fst) by (eby eapply Ca).
    by apply clos_refl_trans_hbUrfE in NEQ0; desf; eauto with hb.
  }

  pose (QQ´ := fun x ⇒ mk_assn_mod (QQ x)).
  assert (EQ : ∀ isrmw,
    hsingl l (HVra QQ´ Remp false (Some HLCnormal) None) +!+
    hsingl l (HVra Wemp QQ´ isrmw (Some HLCnormal) None) =
    hsingl l (HVra QQ´ QQ´ isrmw (Some HLCnormal) None)).
  {
    clear; intro; rewrite hplus_unfold; desf.
      f_equal; extensionality y; specialize (h y); unfold hupd in *; desf; ins; desf; ins.
      by f_equal; extensionality v; desf; specialize (h v); desf; ins;
         eapply assn_mod_eqI1; ins; try rewrite e; Asim_simpl.
      by f_equal; extensionality v; desf; specialize (h v); desf; ins;
         eapply assn_mod_eqI; ins; try rewrite e; Asim_simpl.
    by destruct n; intro; unfold hupd; desf; split; ins; vauto; destruct isrmw; vauto.
  }
  eapply safe_final_plain with (h := Hdef (hupd hFR l (HVra QQ´ QQ´ true (Some HLCnormal) None))); eauto.
    subst QQ´; ∃ hemp; repeat eexists; try edone; instantiate; rewrite ?hplus_emp_r, EQ; try done.
    rewrite hplus_unfold; desf; ins.
      by f_equal; extensionality y; unfold hupd; desf; ins; desf.
    by destruct n0; intro; unfold hupd; desf; ins; desf.
  red; rewrite SEM1.
  eexists,,hFR; repeat (split; try edone); eauto using mupds; unfold NW.
  rewrite mupdo; try red; ins; desf.
Qed.