Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 rslassn rslmodel rslassnlemmas.

Set Implicit Arguments.

Lemma vshift_refl h : vshift h h.
Proof. vauto. Qed.

Lemma vshift_eqI x y : x = y → vshift x y.
Proof. intros; subst; eapply vshift_refl. Qed.

Lemma vshift_trans h1 h2 h3: vshift h1 h2 → vshift h2 h3 → vshift h1 h3.
Proof. vauto. Qed.

Lemma vshift_star_l :
  ∀ h h1 h1' (V1: vshift h1 h1'),
    vshift (hplus h1 h) (hplus h1' h).
Proof.
  induction 1; ins; eauto using vshift_refl, vshift_trans.
Qed.

Lemma vshift_star :
  ∀ h1 h1' (V1: vshift h1 h1') h2 h2' (V1: vshift h2 h2'),
    vshift (hplus h1 h2) (hplus h1' h2').
Proof.
  ins; eapply vshift_trans, vshift_star_l; eauto.
  by rewrite !(hplusC h1); apply vshift_star_l.
Qed.

Lemma vshift_star_def :
  ∀ h1 h1' (V1: vshift h1 h1') h (D: hplus h1 h ≠ Hundef),
    hplus h1' h ≠ Hundef.
Proof.
  induction 1; ins; eauto.
Qed.

Lemma vshift_def :
  ∀ hf y,
    vshift (Hdef hf) y →
    ∃ hf', y = Hdef hf'.
Proof.
  intros; remember (Hdef hf) as x; revert hf Heqx.
  induction H; ins; subst; eauto.
  by edestruct IHclos_refl_trans1; desf; eauto.
Qed.

Lemma vshift_nalloc :
  ∀ hf hf' l,
    vshift (Hdef hf) (Hdef hf') →
    hf l = HVnone →
    hf' l = HVnone.
Proof.
  intros until 1.
  remember (Hdef hf) as x; remember (Hdef hf') as y; revert hf hf' Heqx Heqy.
  induction H; ins; subst; desf.
  by eapply vshift_def in H; desf; eauto.
Qed.

Lemma vshift_val :
  ∀ hf hf' l,
    vshift (Hdef hf) (Hdef hf') →
    is_val (hf' l) →
    hf' l = hf l.
Proof.
  intros until 1.
  remember (Hdef hf) as x; remember (Hdef hf') as y; revert hf hf' Heqx Heqy.
  induction H; ins; subst; desf.
     by edestruct (vshift_def H); subst;
        rewrite (IHclos_refl_trans2 _ _ eq_refl eq_refl H1) in H1 |- *; auto.
Qed.

Lemma vshift_ra :
  ∀ hf hf' l PP QQ isrmw init,
    vshift (Hdef hf) (Hdef hf') →
    hf' l = HVra PP QQ isrmw init →
    
    ∃ PP' QQ' isrmw' init',
      hf l = HVra PP' (fun v ⇒ mk_assn_mod (Astar (sval (QQ v)) (QQ' v))) isrmw' init'
      ∧ (∀ v, implies (sval (PP v)) (sval (PP' v)))
      ∧ (isrmw → isrmw')
      ∧ (init → init').
Proof.
  intros until 1.
  remember (Hdef hf) as x; remember (Hdef hf') as y; revert hf hf' Heqx Heqy.
  revert PP QQ isrmw init;
  induction H; ins; subst; desf.

∃ PP, (fun _ ⇒ Aemp), isrmw, init; repeat split; try red; ins.
    by rewrite H; f_equal; extensionality y; apply assn_mod_eqI; Asim_simpl.

    rename IHclos_refl_trans1 into X, IHclos_refl_trans2 into Y.
    edestruct (vshift_def H); subst.
    specialize (Y _ _ _ _ _ _ eq_refl eq_refl H1); desf.
    specialize (X _ _ _ _ _ _ eq_refl eq_refl Y); desf; vauto.
rewrite X; eexists _,(fun v ⇒ Astar (QQ' v) (QQ'0 v)),_,_.
    split; [f_equal; try done|by unfold implies in *; intuition].
    extensionality y; apply assn_mod_eqI; ins; Asim_simpl; eauto using Asim.
Qed.

Lemma vshift_hack:
  ∀ x y, vshift x y ↔ x = y.
Proof. split; ins; vauto; induction H; ins; congruence. Qed.

Hint Unfold imm_happens_before.

Lemma hupds A h l (y : A) : hupd h l y l = y.
Proof. unfold hupd; desf; congruence. Qed.

Lemma hist_closed_trans :
  ∀ mt lab sb rf mo V (HC: hist_closed mt lab sb rf mo V)
    a b (TR: clos_refl_trans _ sb a b) (IN: In b V), In a V.
Proof. induction 2; ins; eauto using hc_edge. Qed.

Lemma hist_closedD :
  ∀ mt lab sb rf mo V (HC: hist_closed mt lab sb rf mo V)
    a b (TR: happens_before lab sb rf mo a b) (IN: In b V), In a V.
Proof. induction 2; ins; unfold imm_happens_before in *; desf; eauto using hc_edge. Qed.

Lemma happens_before_trans lab sb rf mo a b c :
  happens_before lab sb rf mo a b →
  happens_before lab sb rf mo b c →
  happens_before lab sb rf mo a c.
Proof. apply t_trans. Qed.

Lemma happens_before_sb lab (sb : relation actid) rf mo a b :
  sb a b → happens_before lab sb rf mo a b.
Proof. ins; apply t_step; auto. Qed.

Lemma happens_before_sw lab sb rf mo a b :
  synchronizes_with lab sb rf mo a b → happens_before lab sb rf mo a b.
Proof. ins; apply t_step; auto. Qed.

Lemma happens_before_ann_sw lab sb rf mo a b :
  ann_sw lab rf a b → happens_before lab sb rf mo a b.
Proof.
  ins; apply t_step; red in H; desf; right; repeat (eexists; eauto); vauto.
Qed.

Lemma clos_trans_hbE :
  ∀ lab sb rf mo a b (HB: clos_trans actid (happens_before lab sb rf mo) a b),
    happens_before lab sb rf mo a b.
Proof.
  induction 1; vauto.
Qed.

Hint Immediate clos_trans_hbE : hb.

Hint Resolve
  happens_before_sb happens_before_sw happens_before_ann_sw
  happens_before_trans t_step hist_closedD : hb.

Lemma count_implies :
  ∀ (T: eqType) (f1 f2 : T → bool) (IMP : ∀ x, f1 x → f2 x) l,
  count f1 l ≤ count f2 l.
Proof.
  induction l; ins; desf; eauto.
  by rewrite IMP in Heq0.
Qed.

Lemma hasP' :
  ∀ (T : eqType) (a : pred T) (l : list_predType T),
    reflect (∃ x : T, In x l ∧ a x) (has a l).
Proof.
  ins; case hasP; intro H; constructor; try red; intros; destruct H; desf.
    by apply/inP in H; eauto.
  by ∃ x; try apply/inP; eauto.
Qed.

Lemma clos_refl_transE X rel a b :
    clos_refl_trans X rel a b ↔ a = b ∨ clos_trans X rel a b.
Proof.
  split; ins; desf; try induction H; desf; eauto using clos_refl_trans, clos_trans.
Qed.

Lemma clos_refl_trans_hbE :
  ∀ lab sb rf mo a b,
    clos_refl_trans actid (happens_before lab sb rf mo) a b →
    happens_before lab sb rf mo a b ∨ a = b.
Proof.
  unfold happens_before; induction 1; desf; vauto.
Qed.

Lemma helper_perm_filter_post :
  ∀ e T,
    ∃ posts_sb posts_sw,
      Permutation T (filter (fun x : hbcase ⇒ hb_fst x != e) T ++
                     map (hb_sb e) posts_sb ++
                     map (hb_sw e) posts_sw).
Proof.
  induction T as [|hb T']; ins; desc.
     by ∃ nil, nil.
  case eqP; ins; subst; [|eby do 2 eexists; eapply Permutation_cons].
  destruct hb; ins.
    eexists _,(_::_); rewrite <- appA in *; ins.
    by eapply Permutation_trans, Permutation_middle; eauto.
  by eexists (_ :: _),_; ins; eapply Permutation_trans, Permutation_middle; eauto.
Qed.

Lemma has_sw_succs acts lab sb rf a :
  ExecutionFinite acts lab sb →
  ∃ sws,
    << NDsws: NoDup sws >> ∧
    << INsws: ∀ x, In x sws ↔ ann_sw lab rf a x >>.
Proof.
  ∃ (undup (filter (fun x ⇒ mydec (ann_sw lab rf a x)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H; red in H0; desf.
  generalize (CLOlab x); destruct (lab x); ins; vauto; eapply H; done.
Qed.

Lemma has_sw_pres acts lab sb rf a :
  ExecutionFinite acts lab sb →
  ∃ sws,
    << NDsws: NoDup sws >> ∧
    << INsws: ∀ x, In x sws ↔ ann_sw lab rf x a >>.
Proof.
  ∃ (undup (filter (fun x ⇒ mydec (ann_sw lab rf x a)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H; red in H0; desf.
  generalize (CLOlab x); destruct (lab x); ins; vauto; eapply H; done.
Qed.

Definition wf_ltof A (f : A → nat) :
  well_founded (fun x y ⇒ f x < f y).
Proof.
  by apply Wf_nat.well_founded_lt_compat with f; intros x y; case ltP.
Qed.

Lemma In_implies_perm A (x : A) l (IN: In x l) :
  ∃ l', Permutation l (x :: l').
Proof.
  induction l; ins; desf; eauto.
  destruct IHl; eauto using Permutation.
Qed.

Lemma Permutation_count A l l' (P : Permutation (A:=A) l l') f :
  count f l = count f l'.
Proof.
  induction P; ins; desf; congruence.
Qed.

Lemma Permutation_hmap_valids :
  ∀ l l' (P : Permutation l l') lab sb rf hmap,
    hmap_valids lab sb rf hmap l →
    hmap_valids lab sb rf hmap l'.
Proof.
  by red; ins; eapply H, Permutation_in, IN; apply Permutation_sym.
Qed.

Lemma Permutation_hist_closed :
  ∀ l l' (P : Permutation l l') mt lab sb rf mo,
    hist_closed mt lab sb rf mo l →
    hist_closed mt lab sb rf mo l'.
Proof.
  red; ins; eapply H in HB.
    by apply (Permutation_in _ P) in HB.
  by eapply Permutation_in, IN; eauto using Permutation_sym.
Qed.

Lemma Consistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : Consistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    Consistent acts' lab sb rf mo sc mt.
Proof.
  unfold Consistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

Lemma weakConsistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

Lemma weakConsistent_Permutation :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: Permutation acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins.
    by apply (Permutation_in _ EQ), CLOlab.
  by apply CLOsb in H; desf; split; apply (Permutation_in _ EQ).
Qed.

Lemma Permutation_flatten A l l' (P : Permutation l l') :
  Permutation (A:=A) (flatten l) (flatten l').
Proof.
  induction P; ins; rewrite ?flatten_cons, <- ?appA;
  eauto using Permutation, Permutation_app, Permutation_app_comm.
Qed.

Lemma hc_edge_irr acts lab sb rf mo sc mt :
  weakConsistent acts lab sb rf mo sc mt →
  irreflexive (hc_edge mt lab sb rf mo).
Proof.
  unfold weakConsistent, irreflexive; ins; desf.
  destruct H0; ins; eauto with hb; destruct mt; ins; desf; eauto 7 with hb.
Qed.

Definition is_pred A (rel : A → A → Prop) B a :=
  has (fun b ⇒ mydec (clos_refl_trans A rel a b)) B.

Definition depth_metric A (rel: A → A → Prop) V a :=
  count (is_pred rel a) V.

Lemma clos_transK T (rel: relation T) x y :
  clos_trans _ (clos_trans _ rel) x y →
  clos_trans _ rel x y.
Proof. induction 1; eauto using clos_trans. Qed.

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b → a = b ∨ clos_trans T rel a b.
Proof. induction 1; desf; eauto using clos_trans. Qed.

Lemma depth_lt (rel : relation actid) V A B
  (HB : ∀ a, In a A → ¬ In a B →
        ∃ b, In b B ∧ rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: ∀ a, In a A → ¬ clos_trans _ rel b a)
  (SUB: ∀ b, In b B → In b V) :
  depth_metric rel V A < depth_metric rel V B.
Proof.
  unfold depth_metric; ins.
  assert (IMP: ∀ x, is_pred rel A x → is_pred rel B x).
    clear -HB; unfold is_pred, mydec; ins; desf.
    apply/@hasP'; apply/@hasP' in H; destruct H; desf.
    destruct (inP x0 B); [by ∃ x0; ins; desf|].
    eapply HB in H; desf; eexists; split; try edone; desf.
    by exfalso; eauto using rt_trans, rt_step.
  assert (P1: is_pred rel B b).
    unfold is_pred, mydec; desf.
    eapply In_split in IN; desf.
    rewrite has_app; ins; desf; clarsimp.
    by destruct n; vauto.
  assert (P2: is_pred rel A b = false).
    clear -NHB NIN; apply/hasP'; unfold mydec; intro; desf; eauto.
    by apply clos_refl_transD in c; unfold not in *; desf; eauto.
  assert (IN' : In b V) by eauto.
  eapply In_split in IN'; desf; rewrite !count_app; ins.
  ins; rewrite P1, P2, addnS, ltnS.
  eauto using len_add, count_implies.
Qed.

Lemma edge_depth_ind mt lab sb rf mo V
  (ACYCLIC: IrreflexiveHB lab sb rf mo)
  (HC: hist_closed mt lab sb rf mo V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge' (EV : edge_valid lab sb rf edge')
            (LT: happens_before lab sb rf mo (hb_fst edge') (hb_fst edge)),
      P edge')
    (EV : edge_valid lab sb rf edge)
    (IN : In (hb_fst edge) V),
    P edge) →
  ∀ edge (EV : edge_valid lab sb rf edge), In (hb_fst edge) V → P edge.
Proof.
  intros until edge.
  generalize (S (depth_metric (happens_before lab sb rf mo) V (hb_fst edge :: nil))),
             (ltnSn (depth_metric (happens_before lab sb rf mo) V (hb_fst edge :: nil))).
  intro n'.
  revert edge; induction n'; ins.
  eapply H; ins; eapply IHn'; ins; eauto.
  2: by clear -HC LT H1; induction LT; unfold imm_happens_before in *; desf;
        eauto with hb.
  eapply ltn_len_trans, H0.
  eapply depth_lt; ins; desf; eauto; instantiate; rewrite addn0 in *;
    intro; desf; [rewrite H2 in *|]; eauto using t_step, t_trans, clos_trans_hbE.
Qed.

Lemma edge_depth_ind2 mt lab sb rf mo V
  (ACYCLIC: acyclic (hc_edge mt lab sb rf mo))
  (HC: hist_closed mt lab sb rf mo V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge' (EV : edge_valid lab sb rf edge')
            (LT: clos_trans _ (hc_edge mt lab sb rf mo) (hb_fst edge') (hb_fst edge)),
      P edge')
    (EV : edge_valid lab sb rf edge)
    (IN : In (hb_fst edge) V),
    P edge) →
  ∀ edge (EV : edge_valid lab sb rf edge), In (hb_fst edge) V → P edge.
Proof.
  intros until edge.
  generalize (S (depth_metric (clos_trans _ (hc_edge mt lab sb rf mo)) V (hb_fst edge :: nil))),
             (ltnSn (depth_metric (clos_trans _ (hc_edge mt lab sb rf mo)) V (hb_fst edge :: nil))).
  intro n'.
  revert edge; induction n'; ins.
  eapply H; ins; eapply IHn'; ins; eauto.
  2: by clear -HC LT H1; induction LT; unfold imm_happens_before in *; desf;
        eauto with hb.
  eapply ltn_len_trans, H0.
  eapply depth_lt; ins; desf; eauto; instantiate; rewrite addn0 in *;
    intro; desf; [rewrite H2 in *|]; eauto using t_step, t_trans, clos_transK.
Qed.

Fixpoint find_max A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f curr ≤ f x then find_max x f xs else find_max curr f xs
  end.

Lemma find_max_range :
  ∀ A (curr: A) f l,
    In (find_max curr f l) (curr :: l).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_max_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f x ≤ f (find_max curr f l).
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

Lemma get_deepest :
  ∀ lab sb rf mo (ACYCLIC: IrreflexiveHB lab sb rf mo)
         mt V (HC: hist_closed mt lab sb rf mo V)
         T (NNIL: T ≠ nil)
         (INCL: ∀ edge (IN: In edge T), In (hb_fst edge) V),
  ∃ edge,
    << IN: In edge T >> ∧
    << INe: In (hb_fst edge) V >> ∧
    << DEEP: ∀ edge' (IN': In edge' T)
                 (HB': happens_before lab sb rf mo (hb_fst edge) (hb_fst edge')),
               False >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (happens_before lab sb rf mo) V (hb_fst x :: nil)).

  assert (IN:= find_max_range h f T).
  eexists; unfold NW; repeat split; eauto; ins.
  assert (D := find_max_greatest f IN'); ins.
  specialize (INCL _ IN'); clear IN IN'; subst f.
  erewrite lenE, depth_lt in D; ins; desf; try intro; desf.
    by ∃ (hb_fst edge'); vauto.
    by left; reflexivity.
    by rewrite H in *; eauto using t_step.
    by eauto using t_step, t_trans, clos_trans_hbE.
Qed.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f x ≤ f curr then find_min x f xs else find_min curr f xs
  end.

Lemma find_min_range :
  ∀ A (curr: A) f l,
    In (find_min curr f l) (curr :: l).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_min_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f (find_min curr f l) ≤ f x.
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

Lemma get_shallow :
  ∀ mt lab sb rf mo (ACYCLIC: with_mt mt AcyclicMedium AcyclicStrong lab sb rf mo)
         V (HC: hist_closed mt lab sb rf mo V)
         T (HC': hist_closed mt lab sb rf mo (V ++ T)) (NNIL: T ≠ nil),
  ∃ e,
    << IN: In e T >> ∧
    << HC: hist_closed mt lab sb rf mo (e :: V) >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (hc_edge mt lab sb rf mo) (V ++ a :: T) (x :: nil)).

  assert (IN:= find_min_range a f T).

  eexists; unfold NW; repeat split; eauto; ins.
  red; ins; destruct IN0; eauto; subst.
  generalize HB; eapply HC' in HB; eauto.
  2: by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
  rewrite In_app in HB; destruct HB as [|H]; vauto; intro.
  eapply find_min_greatest with (f:=f) in H.
  exfalso; clear IN.
  rewrite lenE in H; apply/negP in H; destruct H.
  eapply depth_lt; eauto using In_eq; ins; desf.
    by destruct HB; eauto using hc_edge with hb .
    by destruct mt; ins; intro; desf; destruct HB; desf; eauto 8 with hb.
    intro H.
    assert (X: clos_trans actid (hc_edge mt lab sb rf mo) a0 a0) by eauto using clos_trans.
    destruct mt; apply (ACYCLIC a0); revert X; clear;
    generalize a0 at 1 3; induction 1; eauto using clos_trans;
    by destruct H; desf; auto with hb.
  assert (IN:= find_min_range a f T).
  by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
Qed.

Lemma only_alloc_allocates:
  ∀ lab sb rf hmap edge h l
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge)
    (HM : hmap edge = Hdef h)
    (ALL: h l ≠ HVnone)
    (NAb: ∀ x h, sb x (hb_fst edge) →
                      hmap (hb_sb x (hb_fst edge)) = Hdef h → h l = HVnone)
    (NAw: ∀ x h, ann_sw lab rf x (hb_fst edge) →
                      hmap (hb_sw x (hb_fst edge)) = Hdef h → h l = HVnone),
    lab (hb_fst edge) = Aalloc l.
Proof.
  ins; unfold hmap_valid, unique in VAL.
  desf; try first [progress f_equal|exfalso]; desf; destruct edge; ins; desf;
   try (by red in EV; rewrite Heq in EV; desc);
   try (eapply qU0 in EV; desf);
   try (by rewrite HM in *; desf; unfold hupd in *; desf; desf;
           exploit NAb; eauto).

  assert (X: In e' posts) by (by apply qOK).
  edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
  eapply In_split in X; desf; rewrite !map_app, hsum_app in *;
  ins; rewrite hsum_cons, HM in ×.
  assert (hf' l ≠ HVnone).
    by intro; symmetry in VAL'; eapply hplus_nalloc in VAL'; eauto;
       desf; eapply hplus_nalloc in VAL'; eauto; desf;
       eapply hplus_nalloc in VAL'3; eauto; desf.
  eapply hsum_alloc in pEQ; eauto; desf; eauto using vshift_nalloc.
  eby repeat (rewrite In_map in *; desf);
      exploit NAb; try eapply pOK.

  rewrite qEQ in ×.
  eapply hplus_alloc in HM; eauto; desf.
    unfold hupd in HM0; desf; subst; try done.
    clear ALL; exploit NAb; eauto; ins.
    symmetry in pEQ'; eapply hplus_nalloc in pEQ'; eauto.
    by desf; rewrite hupds in ×.
  eapply hplus_alloc in HM; eauto; desf.
    by eapply hsum_alloc in swsEQ; eauto; desc;
       repeat (rewrite In_map in *; desf);
       eapply swsOK in swsEQ2; eauto.
  rewrite hplus_unfold in *; desf; intuition eauto.
  exploit NAb; eauto; instantiate; intro M; ins.
  by unfold hupd in M; desf; ins; desf.

  by rewrite wEQ in HM; unfold hemp in *; desf.

  rewrite HM in *; desf; unfold hupd in *; desf; desf;
  by exploit NAb; eauto; intro X; rewrite X in ×.

  specialize (NAb pre);
  destruct (hmap (hb_sb pre e)); desf;
  specialize (NAb _ pU eq_refl).
  destruct (vshift_def UPD) as [hf' VAL']; rewrite VAL' in *; symmetry in VAL'.
  eapply hplus_nalloc in VAL'; eauto; desf.
  2: eapply vshift_nalloc with (l := l); eauto;
     unfold initialize, hupd; desf; congruence.
  eapply hplus_nalloc in VAL'1; eauto; desf.
  eapply hplus_nalloc in VAL'4; eauto; desf.
  eapply hsum_nalloc in VAL'4;
    repeat (eapply In_map; repeat eexists; try eapply swsOK); desf; eauto.
  congruence.

  specialize (NAb pre);
  destruct (hmap (hb_sb pre e)); desf;
  specialize (NAb _ pU eq_refl).
  destruct (vshift_def UPD) as [hf' VAL']; rewrite VAL' in *; symmetry in VAL'.
  eapply hplus_nalloc in VAL'; desf.
  2: eapply vshift_nalloc with (l := l); eauto;
     unfold initialize, hupd; desf; congruence.
  eapply hplus_nalloc in VAL'1; eauto; desf; congruence.

  specialize (NAb pre); rewrite pEQ in *; desf;
  specialize (NAb _ pU eq_refl).
  assert (hi l = HVnone).
    clear - swsInOK pEQ' iEQ NAb NAw; apply NNPP; intro.
    eapply hplus_alloc in iEQ; eauto; desf; ins; desf.
    eapply hsum_alloc in iEQ; eauto; desf; ins; desf.
    by repeat (rewrite In_map in *; desf); rewrite swsInOK in *; eauto.
  destruct (vshift_def UPD) as [hf' VAL']; rewrite VAL' in *; symmetry in VAL'.
  eapply hplus_nalloc with (loc := l) in VAL'; eauto; desf.
  2: eapply vshift_nalloc with (l := l); eauto;
     unfold initialize, hupd; desf; congruence.
  eapply hplus_nalloc with (loc := l) in VAL'1; eauto; desf.
  eapply hplus_nalloc with (loc := l) in VAL'4; eauto; desf.
  eapply hsum_nalloc in VAL'4;
    repeat (eapply In_map; repeat eexists; try eapply swsOutOK); desf; eauto.
  congruence.

  specialize (NAb pre);
  destruct (hmap (hb_sb pre e)); desf;
  specialize (NAb _ pU eq_refl).
  assert (hi l = HVnone).
    clear - swsInOK pEQ' iEQ NAb NAw; apply NNPP; intro.
    eapply hplus_alloc in iEQ; eauto; desf; ins; desf.
    eapply hsum_alloc in iEQ; eauto; desf; ins; desf.
    by repeat (rewrite In_map in *; desf); rewrite swsInOK in *; eauto.
  destruct (vshift_def UPD) as [hf' VAL']; rewrite VAL' in *; symmetry in VAL'.
  eapply hplus_nalloc with (loc := l) in VAL'; eauto; desf.
  2: eapply vshift_nalloc with (l := l); eauto;
     unfold initialize, hupd; desf; congruence.
  eapply hplus_nalloc with (loc := l) in VAL'1; eauto; desf.
  congruence.
Qed.

Lemma heap_loc_allocated :
  ∀ mt lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l (LA: h l ≠ HVnone),
  ∃ c,
    lab c = Aalloc l ∧
    clos_refl_trans _ (happens_before lab sb rf mo) c (hb_fst edge).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  specialize (VALID _ IN).
  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ].
    by eauto using clos_refl_trans.
  cut (∃ edge' h',
         edge_valid lab sb rf edge' ∧
         hb_snd edge' = hb_fst edge ∧
         hmap edge' = Hdef h' ∧
         h' l ≠ HVnone).
    by intro; desf; exploit (IH edge'); eauto;
       [|intro; desf; repeat eexists; try edone];
       destruct edge'; ins; vauto; eauto using clos_refl_trans with hb.
  clear IH.
  apply NNPP; intro; destruct NEQ.
  eapply only_alloc_allocates; eauto.
    by ins; apply NNPP; intro; destruct H; eexists (hb_sb x _); ins; vauto.
  by ins; apply NNPP; intro; destruct H; eexists (hb_sw x _); ins; vauto.
Qed.

Theorem valid_implies_mem_safe :
  ∀ mt lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V),
  mem_safe V lab sb rf mo.
Proof.
  red; ins; cut (∃ b, sb b a ∧ ∃ hf,
                   hmap (hb_sb b a) = Hdef hf
                   ∧ hf (loc (lab a)) ≠ HVnone).
    intro; desf; exploit heap_loc_allocated; eauto; ins; desf; eauto with hb.
    by rewrite clos_refl_transE in *; desf; eauto with hb.
  specialize (VALID _ IN); clear - VALID Aa; red in VALID; unfold unique in ×.
  desf; desf; ∃ pre; split;ins; try solve [eexists hf; split; congruence];
  eexists; split; try edone; try intro.
  by symmetry in pEQ'; eapply hplus_nalloc in pEQ'; eauto; desf;
     unfold hupd in *; desf.
  by desf; rewrite H in *; desf.
  by destruct (vshift_def UPD) as [hf' VAL']; rewrite VAL' in *; symmetry in VAL';
    eapply hplus_nalloc in VAL';
     [|eapply vshift_nalloc with (l := l); eauto;
       unfold initialize, hupd; desf; congruence];
     desf; unfold hupd in *; desf; desf.
  congruence.
Qed.

Definition independent lab sb rf mo T :=
  ∀ edge1 (IN1: In edge1 T) edge2 (IN2: In edge2 T)
      (HB: hb_snd edge1 = hb_fst edge2 ∨
           happens_before lab sb rf mo (hb_snd edge1) (hb_fst edge2)),
    False.

Lemma go_back_one :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A : ConsistentAlloc lab) hmap e
    (VALID : hmap_valid lab sb rf hmap e) hFR
    (ALLOC : ∀ hf loc,
               hFR = Hdef hf → hf loc ≠ HVnone →
               ∃ c, lab c = Aalloc loc ∧ c ≠ e),
   ∃ pres_sb pres_sw posts_sb posts_sw,
     NoDup pres_sb ∧
     NoDup pres_sw ∧
     NoDup posts_sb ∧
     NoDup posts_sw ∧
     (∀ x : actid, In x pres_sb ↔ sb x e) ∧
     (∀ x : actid, In x pres_sw ↔ ann_sw lab rf x e) ∧
     (∀ x : actid, In x posts_sb ↔ sb e x) ∧
     (∀ x : actid, In x posts_sw ↔ ann_sw lab rf e x) ∧
     (∀ h
       (EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
            hsum (map hmap (map (hb_sw^~ e) pres_sw)) +!+ hFR =
            Hdef h),
      ∃ h0 : val → HeapVal,
        hsum (map hmap (map (hb_sb e) posts_sb)) +!+
        hsum (map hmap (map (hb_sw e) posts_sw)) +!+ hFR =
        Hdef h0).
Proof.
  unfold hmap_valid, unique; ins; desf; desf.

  Case Askip.
    ∃ pres, nil, posts, nil; repeat (split; ins).
    by red in H; desf; rewrite Heq in ×.
    by red in H; desf; rewrite Heq in ×.
    eapply hdef_alt, (hplus_not_undef_r hsink); eauto.
    rewrite hplusAC, <- hplusA; eapply vshift_star_def; eauto; congruence.

  Case Aalloc.
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    by red in H; desf; rewrite Heq in ×.
    rewrite pEQ, qEQ in *; destruct hFR; ins.
    rewrite hplus_unfold in *; desf; vauto.
    destruct n; intro l'; specialize (h0 l').
    unfold hupd in *; desf; desf.
    specialize (ALLOC _ l eq_refl).
    destruct (hf0 l); desf; destruct ALLOC; desf;
    by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.

  Case Aalloc.
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    by red in H; desf; rewrite Heq in ×.
    rewrite pEQ, qEQ in *; destruct hFR; ins.
    rewrite hplus_unfold in *; desf; vauto.
    destruct n; intro l'; specialize (h0 l').
    unfold hupd in *; desf; desf.
    specialize (ALLOC _ l eq_refl).
    destruct (hf0 l); desf; destruct ALLOC; desf;
    by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.

  Case Aload .
    pose proof (has_sw_pres rf e FIN); desc.
    ∃ (pre :: nil), sws, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one in *; eauto.

    by red in H; desf; rewrite Heq in ×.
    eby rewrite qEQ, hsum_nil, hplus_emp_l;
        rewrite (hplusC _ hFR), <- hplusA in EQ; eapply hplus_def_inv_l.

  Case Aload .
    ∃ (pre :: nil), sws, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    rewrite pEQ, swsEQ, <- pEQ', hplusA, (hplusAC _ hF),
            <- hplus_init1 with (init := true), hplusA,
            <- (hplusA _ hF), <- (hplusA _ (hplus _ hF)), <- qEQ in EQ.
    eby eapply hplus_def_inv_r.

  Case Astore .
    pose proof (has_sw_succs rf e FIN); desc.
    ∃ (pre :: nil), nil, (post :: nil), sws; ins; repeat (split; ins; desf);
      rewrite ?hsum_one in *; eauto.
      by red in H; desf; rewrite Heq in ×.
    assert (M: hsum (map hmap (map (hb_sw e) sws)) = hemp).
      generalize (fun x ⇒ proj1 (INsws x)); clear - wEQ.
      by induction sws; ins; rewrite hsum_cons, IHsws, hplus_emp_r; eauto.
    rewrite M; rewrite hsum_nil in ×.
    by rewrite pEQ, qEQ in *; eauto using hdef_upd_alloc.

  Case Astore .
    ∃ (pre :: nil), nil, (post :: nil), sws; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    by red in H; desf; rewrite Heq in ×.
    exploit hplus_def_inv_l; eauto; intros [hf'' EQ']; rewrite EQ' in ×.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.

    eapply vshift_star_def with (h := hFR) in UPD; try congruence; desf.
      by eapply hdef_alt; rewrite <- VAL', !hplusA, !(hplusAC hsink) in UPD; eauto.
    desf; eapply hplus_init_def; eauto; desf.

  Case Armw.
    ∃ (pre :: nil), swsIn, (post :: nil), swsOut; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.
    exploit hplus_def_inv_l; eauto; intros [hf'' EQ']; rewrite EQ' in ×.
    edestruct vshift_def as [hf' VAL']; eauto; rewrite VAL' in ×.
    desf.
    eapply vshift_star_def with (h := hFR) in UPD; try congruence; desf.
      rewrite <- VAL', !hplusA, !(hplusAC hsink) in UPD.
      by eapply hdef_alt; eauto.
    rewrite <- hplusA, iEQ in EQ.
    eapply hdef_alt; vauto.
Qed.

Lemma get_pres_aux :
  ∀ mt lab sb rf mo V a
    (HC : hist_closed mt lab sb rf mo V)
    (IN : In a V),
   ∃ pres_sb pres_sw,
     << NDb : NoDup pres_sb >> ∧
     << NDw : NoDup pres_sw >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x a >> ∧
     << Pw : ∀ x, In x pres_sw ↔ ann_sw lab rf x a >>.
Proof.
  intros; unfold NW.
  ∃ (undup (filter (fun x ⇒ mydec (sb x a)) V)),
         (undup (filter (fun x ⇒ mydec (ann_sw lab rf x a)) V)).
  do 2 (split; [by apply/uniqP; apply undup_uniq|]); split;
  ins; rewrite (In_mem_eq (mem_undup (T:=nat_eqType) _)), In_filter;
  unfold mydec; desf; split; ins; desf; eauto using hist_closedD with hb.
Qed.

Lemma get_pres :
  ∀ mt lab sb rf mo V
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (HC : hist_closed mt lab sb rf mo V) edge T
    (ND : NoDup T)
    (IN : In edge T)
    (INCL : ∀ edge, In edge T → In (hb_fst edge) V)
    (EVS : ∀ edge, In edge T → edge_valid lab sb rf edge)
    (DEEP : ∀ edge', In edge' T →
              happens_before lab sb rf mo (hb_fst edge) (hb_fst edge') → False)
    (IND: independent lab sb rf mo T),
   ∃ pres_sb pres_sw,
     let res := map (fun x ⇒ hb_sb x (hb_fst edge)) pres_sb ++
                map (fun x ⇒ hb_sw x (hb_fst edge)) pres_sw ++
                filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T in
     << NDb : NoDup pres_sb >> ∧
     << NDw : NoDup pres_sw >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x (hb_fst edge) >> ∧
     << Pw : ∀ x, In x pres_sw ↔ ann_sw lab rf x (hb_fst edge) >> ∧
     << ND' : NoDup res >> ∧
     << METR: (depth_metric (happens_before lab sb rf mo) V (map hb_fst res) <
               depth_metric (happens_before lab sb rf mo) V (map hb_fst T) : Prop) >> ∧
     << INCL': ∀ edge, In edge res → In (hb_fst edge) V >> ∧
     << EVS' : ∀ edge, In edge res → edge_valid lab sb rf edge >> ∧
     << IND' : independent lab sb rf mo res >>.
Proof.
  intros; exploit get_pres_aux; eauto; intro; desf.
  ∃ pres_sb, pres_sw; unfold NW;
  repeat (split; try done).

  by rewrite !nodup_app; intuition; try (apply nodup_map; try done; congruence);
     red; ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     apply (IND _ IN2 _ IN); vauto.

  {
    apply depth_lt with (hb_fst edge);
    eauto using In_mapI.
      by ins; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
         rewrite ?Pw, ?Pb in *; eauto using In_mapI with hb; exfalso; eauto.

     intro; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
         rewrite ?Pw, ?Pb in *; eauto using In_mapI with hb.
     by destruct (eqP (hb_fst x) (hb_fst edge)).

     red; ins; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
     rewrite ?Pw, ?Pb in *; eauto with hb.

     by ins; rewrite In_map in *; desf; eauto.
  }

  by ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pw, ?Pb in *; eauto with hb.

  by ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pw, ?Pb in *; eauto.

  {
     red; ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pw, ?Pb in *; subst; eauto with hb.
     revert IN0; case eqP; ins; congruence.
     revert IN0; case eqP; ins; congruence.
  }
Qed.