Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting Program extralib MMergesort.
Require Import GpsSepAlg GpsFraction c11 exps.

Set Implicit Arguments.
Obligation Tactic := intros; desc; try done.

Structure protTy := mkProtTy
  { prot_state : Type ;
    prot_id : nat ;
    prot_trans : relation prot_state ;
    prot_trans_ord : order _ prot_trans }.

Inductive escrowTy := mkEscrowTy (n : nat).

Definition eq_escrow (x y: escrowTy) :=
   match x, y with
     | mkEscrowTy n1, mkEscrowTy n2 ⇒ n1 == n2
   end.

Lemma eq_escrowP: ∀ x y, reflect (x = y) (eq_escrow x y).
Proof.
  induction[] x [y]; ins; case eqP; constructor; congruence.
Qed.

Canonical Structure escrowTy_eqMixin := EqMixin eq_escrowP.
Canonical Structure escrowTy_eqType := Eval hnf in EqType escrowTy escrowTy_eqMixin.

Lemma prot_trans_trans : ∀ tau x y z,
  prot_trans tau x y → prot_trans tau y z → prot_trans tau x z.
Proof.
  eby ins; eapply (ord_trans _ _ (prot_trans_ord _)).
Qed.

Lemma prot_trans_refl : ∀ tau x, prot_trans tau x x.
Proof.
  eby ins; eapply (ord_refl _ _ (prot_trans_ord _)).
Qed.

Definition dec_prot_trans tau x y :=
  if excluded_middle_informative (prot_trans tau x y) then true else false.

Record slist (tau : protTy) :=
  { SL_list : list (prot_state tau) ;
    SL_nemp : SL_list ≠ nil ;
    SL_ndup : NoDup SL_list ;
    SL_sort : StronglySorted (prot_trans tau) SL_list }.

Lemma Sorted_prot tau l :
  (∀ x y, In x l → In y l → prot_trans tau x y ∨ prot_trans tau y x) →
  StronglySorted (prot_trans tau) (sort (dec_prot_trans tau) l).
Proof.
  ins; exploit (sort_sorted (dec_prot_trans tau) l).
    by unfold dec_prot_trans; ins; desf; auto;
       exfalso; specialize (H _ _ H0 H1); desf.
    by unfold dec_prot_trans; red; ins; desf; destruct n;
       eauto using prot_trans_trans.
  clear; induction 1; econstructor; eauto.
  rewrite Forall_forall in *; ins; eapply H in H0;
  unfold dec_prot_trans in *; desf.
Qed.

Program Definition mk_slist (tau : protTy) (l : list (prot_state tau)) :
  option (slist tau) :=
  if excluded_middle_informative
       (l ≠ nil ∧ ∀ x y, In x l → In y l →
                    prot_trans tau x y ∨ prot_trans tau y x)
  then Some {| SL_list := undup (sort (dec_prot_trans tau) l) ;
               SL_ndup := nodup_undup _ |}
  else None.
Next Obligation.
  apply undup_nonnil.
  intro X; destruct H; eapply Permutation_nil; rewrite <- X; apply sort_perm.
Qed.
Next Obligation. by apply Sorted_undup, Sorted_prot. Qed.

Program Definition mk_slist_singl tau s : slist tau :=
  {| SL_list := s :: nil |}.
Next Obligation. vauto. Qed.

Program Definition get_state tau (l : slist tau) : prot_state tau :=
  match rev (SL_list l) with
    | nil ⇒ !
    | x :: _ ⇒ x
  end.
Next Obligation.
  destruct l as [[] ? ?]; ins.
  apply eq_sym, app_eq_nil in Heq_anonymous; desf.
Qed.

Lemma slist_eq tau (l l' : slist tau) :
  SL_list l = SL_list l' → l = l'.
Proof.
  destruct l, l'; ins; desf; f_equal; apply proof_irrelevance.
Qed.

Lemma slist_eq2 tau (l l' : slist tau) :
  (∀ x, In x (SL_list l) ↔ In x (SL_list l')) →
  l = l'.
Proof.
  intros; apply slist_eq; destruct l, l'; ins.
  eapply sorted_perm_eq;
    eauto using NoDup_Permutation; try apply prot_trans_ord.
Qed.

Lemma sort_undup A (p : A → A → bool)
    (T: transitive _ p) (AS: antisymmetric _ p)
    (l : list A)
    (TOTAL: ∀ x y, In x l → In y l → p x y = true ∨ p y x = true) :
  sort p (undup l) = undup (sort p l).
Proof.
  eapply sorted_perm_eq; eauto using sort_sorted, Sorted_undup.
    by eapply NoDup_Permutation; eauto; ins;
       rewrite In_sort, !in_undup_iff, In_sort.
  apply sort_sorted; ins; rewrite in_undup_iff in *; eauto.
Qed.

Lemma undup_sort_undup A p (l : list A) :
  undup (sort p (undup l)) = sort p (undup l).
Proof. apply undup_nodup; eauto. Qed.

Lemma mk_slist_eq tau l l' :
  (∀ x, In x l ↔ In x l') →
  mk_slist tau l = mk_slist tau l'.
Proof.
  intros; unfold mk_slist; desf; f_equal.
    by apply slist_eq2; ins; rewrite !in_undup_iff, !In_sort.

  × exfalso; destruct n; split; try red; ins; desf.
      destruct l as [|aa ?]; ins; specialize (H aa); tauto.
      by apply a0; apply H.

  × exfalso; destruct n; split; try red; ins; desf.
      destruct l' as [|aa ?]; ins; specialize (H aa); tauto.
      by apply a0; apply H.
Qed.

Lemma In_mk_slist tau x l S :
  mk_slist tau l = Some S → In x l → In x (SL_list S).
Proof.
  by unfold mk_slist; ins; desf; ins; apply in_undup_iff, In_sort.
Qed.

Lemma mk_slist_cons_in tau s S S' :
  mk_slist tau (s :: SL_list S) = Some S' →
  In s (SL_list S) →
  S = S'.
Proof.
  unfold mk_slist in *; ins; desf; apply slist_eq; ins.
  destruct S; ins; desf.
  apply sorted_perm_eq with (cmp := prot_trans tau); try apply prot_trans_ord;
    eauto using Sorted_prot, Sorted_undup.
  apply NoDup_Permutation; ins; rewrite in_undup_iff, In_sort;
  split; ins; desf; vauto.
Qed.

Lemma get_state_in tau (S: slist tau) : In (get_state S) (SL_list S).
Proof.
  unfold get_state; destruct S; des_eqrefl; ins.
    by exfalso; induction SL_list0 using rev_ind; ins; rewrite rev_app_distr in ×.
  apply in_rev; rewrite <- EQ; vauto.
Qed.

Lemma get_state_lt tau (S: slist tau) s (IN: In s (SL_list S)) :
  prot_trans tau s (get_state S).
Proof.
  unfold get_state; destruct S; des_eqrefl; ins.
    by exfalso; induction SL_list0 using rev_ind; ins; rewrite rev_app_distr in ×.
  apply (f_equal (fun f ⇒ rev f)) in EQ; ins; rewrite rev_involutive in *; subst.
  rewrite in_app_iff in *; ins; desf; eauto using prot_trans_refl.
  eapply Sorted_app_end_inv; eauto.
Qed.

Inductive protocol :=
  | p_bot
  | p_uninit
  | p_na (k : fraction) (v : nat)
  | p_at (tau : protTy) (s : slist tau).

Arguments p_at : clear implicits.

Inductive resource :=
  | Rundef
  | Rdef (pmap: nat → protocol)
         (gres: ghost_resource)
         (escr: escrowTy → bool).

Definition prot_plus (pi1 pi2 : protocol) :=
  match pi1, pi2 with
    | p_bot, _ ⇒ Some pi2
    | _, p_bot ⇒ Some pi1
    | p_at tau1 s1, p_at tau2 s2 ⇒
      match excluded_middle_informative (tau2 = tau1) with
        | left PF ⇒
          match mk_slist tau1 (SL_list s1 ++ eq_rect _ (fun tau ⇒ list (prot_state tau)) (SL_list s2) _ PF) with
            | Some s ⇒ Some (p_at tau1 s)
            | None ⇒ None
          end
        | _ ⇒ None
      end
    | p_na k1 v1, p_na k2 v2 ⇒
        if v1 == v2 then
          match fraction_plus k1 k2 with
            | Some k ⇒ Some (p_na k v1)
            | None ⇒ None
          end
        else None
    | _, _ ⇒ None
  end.

Definition res_emp : resource :=
  Rdef (fun _ ⇒ p_bot) gres_emp (fun _ ⇒ false).

Definition res_plus (x y : resource) : resource :=
  match x, y with
    | Rundef, _ ⇒ Rundef
    | _, Rundef ⇒ Rundef
    | Rdef pmap1 gres1 escr1, Rdef pmap2 gres2 escr2 ⇒
        match lift_plus prot_plus pmap1 pmap2 with
          | None ⇒ Rundef
          | Some pmap ⇒
            match gres_plus gres1 gres2 with
              | None ⇒ Rundef
              | Some gres ⇒
                Rdef pmap gres (fun sigma ⇒ escr1 sigma || escr2 sigma)
            end
        end
  end.

Fixpoint rsum rl :=
  match rl with
    | nil ⇒ res_emp
    | a :: rl ⇒ res_plus a (rsum rl)
  end.

Definition res_get r loc :=
  match r with
    | Rundef ⇒ p_bot
    | Rdef pmap _ _ ⇒ pmap loc
  end.

Definition res_upd r loc pi :=
  match r with
    | Rundef ⇒ Rundef
    | Rdef pmap gres escr ⇒
      Rdef (fun l ⇒ if l == loc then pi else pmap l) gres escr
  end.

Definition res_mupd r loc n pi :=
  match r with
    | Rundef ⇒ Rundef
    | Rdef pmap gres escr ⇒
      Rdef (fun l ⇒ if excluded_middle_informative (loc ≤ l ≤ loc + n)
                     then pi else pmap l)
           gres escr
  end.

Definition res_gget r l :=
  match r with
    | Rundef ⇒ None
    | Rdef p g e ⇒ g l
  end.

Definition res_escr r sigma :=
  match r with
      Rundef ⇒ False
    | Rdef p g e ⇒ e sigma
  end.

Definition slist_lt tau (S: slist tau) (S': slist tau) :=
  ∀ s (SIN: In s (SL_list S)),
  ∃ s', In s' (SL_list S') ∧ prot_trans tau s s'.

Definition prot_trans_ok (pi1 pi2: protocol) :=
  match pi1, pi2 with
    | p_at tau1 sl1 , p_at tau2 sl2 ⇒
      ∃ (pf : tau2 = tau1),
        slist_lt sl1 (eq_rect _ slist sl2 _ pf)
    | _, _ ⇒ False
  end.

Lemma prot_plus_emp_l x : prot_plus p_bot x = Some x.
Proof. done. Qed.

Lemma prot_plus_emp_r x : prot_plus x p_bot = Some x.
Proof. by destruct x. Qed.

Lemma prot_plusC :
  ∀ x y, prot_plus x y = prot_plus y x.
Proof.
  destruct x, y; ins; try rewrite fraction_plusC; desf; ins;
  try (rewrite <- eq_rect_eq in *; (erewrite mk_slist_eq in Heq;
      [|intros; rewrite in_app_iff at 1; rewrite in_app_iff; apply or_comm])); desf.
Qed.

Lemma prot_plusA :
  ∀ x y xy (P1: prot_plus x y = Some xy) z xyz
                (P2: prot_plus xy z = Some xyz),
    ∃ yz, prot_plus y z = Some yz ∧ prot_plus x yz = Some xyz.
Proof.
  destruct x; ins; desf; eauto; try congruence; try solve [eexists; split; ins; desf].

  by ins; desf; desf; try (eapply fraction_plusA in Heq; eauto; []; desf);
     eexists; split; ins; desf; congruence.

  simpl in P2; desf; rewrite <- eq_rect_eq in *;
   try solve[eexists; split;ins;desf;rewrite <- eq_rect_eq in *;desf].
  cut (∃ s5, mk_slist tau (SL_list s0 ++ SL_list s2) = Some s5 ∧
                  mk_slist tau (SL_list s ++ SL_list s5) = Some s3).
    by clear; ins; desf; rewrite <- eq_rect_eq in *; desf;
       eexists; split; ins; desf; rewrite <- eq_rect_eq in *; desf.
  unfold mk_slist in Heq, Heq0; desf; ins; desf.
  unfold mk_slist at 1; desf; ins.
  2: destruct n; split; try red; ins; [by apply app_eq_nil in H; destruct s2; desf|].
  2: apply a1; repeat first [rewrite in_app_iff in × | rewrite In_sort in × | rewrite in_undup_iff in *]; tauto.
  eexists; split; try done.
  unfold mk_slist; desf; ins; [f_equal; apply slist_eq; simpl|].
  { eapply sorted_perm_eq with (cmp := dec_prot_trans tau); eauto.
     eby clear; red; unfold dec_prot_trans; ins; desf; destruct n; eapply prot_trans_trans.
     eby clear; red; unfold dec_prot_trans; ins; desf; eapply prot_trans_ord.
    eapply NoDup_Permutation; eauto; clear; ins.
      repeat first [rewrite in_undup_iff | rewrite In_sort | rewrite in_app_iff ]; tauto.
    eapply Sorted_undup, sort_sorted.
  by clear - a5; desf; ins; specialize (a0 _ _ H H0); unfold dec_prot_trans; desf; eauto.
   eby clear; red; unfold dec_prot_trans; ins; desf; destruct n; eapply prot_trans_trans.
    eapply Sorted_undup, sort_sorted.
   by clear - a1; desf; ins; specialize (a1 _ _ H H0); unfold dec_prot_trans; desf; eauto.
   eby clear; red; unfold dec_prot_trans; ins; desf; destruct n; eapply prot_trans_trans.
  }
  destruct n; split; try red; ins; [by apply app_eq_nil in H; destruct s; desf|].
  apply a1; repeat first [rewrite in_app_iff in × | rewrite In_sort in ×
                          | rewrite in_undup_iff in *]; tauto.
Qed.

Lemma res_plus_undef r : res_plus r Rundef = Rundef.
Proof. by destruct r. Qed.

Lemma res_plusC x y : res_plus x y = res_plus y x.
Proof.
  unfold res_plus; desf; rewrite lift_plusC in Heq; auto using prot_plusC;
    rewrite ?(gres_plusC gres) in *; desf.
  f_equal; ins; extensionality a; apply orbC.
Qed.

Lemma res_plus_emp_l x : res_plus res_emp x = x.
Proof.
  repeat split; ins; desf; try rewrite lift_plus_emp_l, gres_plusI in *; desf.
  by rewrite lift_plus_noneD in *; desf.
Qed.

Lemma res_plus_emp_r x : res_plus x res_emp = x.
Proof. by rewrite res_plusC, res_plus_emp_l. Qed.

Lemma res_plusA x y z : res_plus (res_plus x y) z = res_plus x (res_plus y z).
Proof.
  unfold res_plus at 3 4; desf.
  by unfold res_plus; desf.
  by unfold res_plus; desf; exploit (@gres_plusA gres); eauto; ins; desf.
  by unfold res_plus; desf; exploit (lift_plusA _ prot_plusA pmap);
     eauto; ins; desf.
  {
    rewrite gres_plusC, (lift_plusC _ prot_plusC) in × |-.
    exploit (lift_plusA _ prot_plusA pmap2); eauto.
    exploit (@gres_plusA gres2); eauto.
    intros; desf; rewrite gres_plusC, (lift_plusC _ prot_plusC) in × |-.
    unfold res_plus; desf; desf.
    by f_equal; ins; extensionality a; apply eq_sym, orbA.
  }
  by unfold res_plus; desf; exploit (@gres_plusA gres); eauto; ins; desf.
  by unfold res_plus; desf; exploit (lift_plusA _ prot_plusA pmap); eauto; ins; desf.
Qed.

Lemma res_plusAC x y z : res_plus y (res_plus x z) = res_plus x (res_plus y z).
Proof.
  rewrite <- !res_plusA; f_equal; apply res_plusC.
Qed.

Ltac kundef :=
  match goal with
    H: _ ≠ Rundef |- _ ≠ Rundef ⇒
      let X := fresh in intro X; apply H;
      clear - X; rewrite X, ?res_plus_undef; simpl; done
  end.

Definition res_lt r r' := ∃ r_rem, res_plus r r_rem = r'.

Lemma res_lt_refl r : res_lt r r.
Proof. red; eauto using res_plus_emp_r. Qed.

Lemma res_lt_trans x y z : res_lt x y → res_lt y z → res_lt x z.
Proof.
  unfold res_lt; ins; desf; rewrite res_plusA; vauto.
Qed.

Definition prot_strip (pi : protocol) :=
  match pi with
    | p_at _ _ ⇒ pi
    | _ ⇒ p_bot
  end.

Definition res_strip (r : resource) :=
  match r with
    | Rundef ⇒ Rundef
    | Rdef p g e ⇒ Rdef (fun loc ⇒ prot_strip (p loc)) (gres_strip g) e
  end.

Lemma res_strip_idemp r : res_strip (res_strip r) = res_strip r.
Proof.
  destruct r; ins; f_equal; auto using gres_strip_idemp.
  by extensionality loc; destruct (pmap loc); ins.
Qed.

Lemma mk_slist_idemp tau s :
  mk_slist tau (SL_list s ++ SL_list s) = Some s.
Proof.
  replace (Some s) with (mk_slist tau (SL_list s)).
     apply mk_slist_eq; ins; rewrite in_app_iff; tauto.
  unfold mk_slist; destruct s; desf; ins; f_equal; try apply slist_eq; ins.
  2: destruct n; split; ins; eapply Sorted_total; try red; eauto using prot_trans_refl.
  desf; eapply sorted_perm_eq; eauto using prot_trans_trans; try apply prot_trans_ord.
    by eapply NoDup_Permutation; eauto; ins; rewrite in_undup_iff, In_sort.
  by apply Sorted_undup, Sorted_prot.
Qed.

Lemma res_plus_strip_idemp r : res_plus r (res_strip r) = r.
Proof.
  destruct r; ins; desf;
    try rewrite gres_plusC, gres_plusI in Heq0; desf; f_equal;
    try rewrite gres_plus_strip_idemp in *; try congruence.

  extensionality l; eapply lift_plus_some_inv with (l := l) in Heq.
  destruct (pmap l); ins; desf; rewrite <- eq_rect_eq, mk_slist_idemp in *; desf.

  by extensionality sigma; apply orbb.

  apply lift_plus_none_inv in Heq; desf.
  destruct (pmap l); ins; desf; rewrite <- eq_rect_eq, mk_slist_idemp in *; desf.
Qed.

Lemma res_strip_plus r r' :
  res_plus r r' ≠ Rundef →
  res_strip (res_plus r r') = res_plus (res_strip r) (res_strip r').
Proof.
  destruct r, r'; ins; desf; ins; try rewrite gres_plusI in *; desf; f_equal;
    try (by apply gres_strip_plus in Heq0; desf).
    extensionality l; inv_lplus l.
    by destruct (pmap l), (pmap0 l); ins; destruct (p l), (p0 l); ins; desf.
  by exfalso; inv_lplus2 l; destruct (pmap l), (pmap0 l); ins; desf.
Qed.

Section Propositions.

Record RProp :=
  { RP_car :> resource → Prop ;
    RP_def : ¬ RP_car Rundef ;
    RP_ext : ∀ r (IN: RP_car r) r' (DEF: res_plus r r' ≠ Rundef),
      RP_car (res_plus r r') }.

Local Obligation Tactic :=
  (try red; intros; desf;
   repeat match goal with r : RProp |- _ ⇒ destruct r end;
   ins; desf; eauto).

Program Definition Rtrue := {| RP_car := fun r ⇒ r ≠ Rundef |}.
Program Definition Rfalse := {| RP_car := fun _ ⇒ False |}.

Program Definition Rpure P := {| RP_car := fun r ⇒ r ≠ Rundef ∧ P |}.

Program Definition Rsingl (r: resource) :=
  {| RP_car r'' := r'' ≠ Rundef ∧ ∃ r', r'' = res_plus r r' |}.
Next Obligation. eauto using res_plusA. Qed.

Program Definition Rstar (P1 P2: RProp) :=
  {| RP_car r := r ≠ Rundef ∧ ∃ r1 r2, P1 r1 ∧ P2 r2 ∧ r = res_plus r1 r2 |}.
Next Obligation.
  split; ins.
  eexists r1, (res_plus r2 r'); repeat split; eauto using res_plusA.
  apply RP_ext0; try done.
  by intro X; rewrite res_plusA, X, res_plusC in DEF.
Qed.

Program Definition Rconj (P Q : RProp) :=
  {| RP_car := fun r ⇒ P r ∧ Q r |}.

Program Definition Rdisj (P Q : RProp) :=
  {| RP_car := fun r ⇒ P r ∨ Q r |}.

Program Definition Rimpl (P Q : RProp) :=
  {| RP_car := fun r ⇒ r ≠ Rundef ∧
                        (∀ r', P (res_plus r r') → Q (res_plus r r')) |}.
Next Obligation. split; ins; rewrite res_plusA in *; eauto. Qed.

Program Definition Rforall A (PP : A → RProp) :=
  {| RP_car := fun r ⇒ r ≠ Rundef ∧ ∀ x, PP x r |}.
Next Obligation.
  split; ins; specialize (IN0 x); destruct (PP x); ins; eauto.
Qed.

Program Definition Rexists A (PP : A → RProp) :=
  {| RP_car := fun r ⇒ r ≠ Rundef ∧ ∃ x, PP x r |}.
Next Obligation. split; ins; ∃ x; destruct PP; ins; eauto. Qed.

Program Definition Rbox (P: RProp) :=
  {| RP_car := fun r ⇒ P (res_strip r) |}.
Next Obligation.
  rewrite res_strip_plus; ins.
  eapply RP_ext0; eauto.
  rewrite <- res_strip_plus;
  destruct (res_plus r r'); ins.
Qed.

Program Definition Runinit l :=
  {| RP_car := fun r ⇒ res_get r l = p_uninit |}.
Next Obligation.
  destruct r; ins; desf; inv_lplus l; rewrite IN in *; ins; desf.
Qed.

Program Definition Rpt k l v :=
  {| RP_car := fun r ⇒ ∃ k', res_get r l = p_na k' v ∧ fraction_le k k' |}.
Next Obligation.
  destruct r; ins; desf; inv_lplus l; rewrite IN in *; ins; desf; desf; eauto.
  eauto using fraction_le_trans, fraction_le1.
Qed.

Definition Rgres g :=
  Rsingl (Rdef (fun _ ⇒ p_bot) g (fun _ ⇒ false)).

Program Definition Rescr sigma :=
  {| RP_car := fun r ⇒ res_escr r sigma |}.
Next Obligation. destruct r, r'; ins; desf; vauto. Qed.

End Propositions.

Structure interp_env :=
  { interp_prot : ∀ protTy, prot_state protTy → nat → RProp
  ; interp_exch : escrowTy → RProp × RProp
  ; interp_exchOK1 :
      ∀ sigma r, ¬ Rstar (fst (interp_exch sigma))
                              (fst (interp_exch sigma)) r
  ; interp_exchOK2 :
      ∀ sigma r, ¬ Rstar (snd (interp_exch sigma))
                              (snd (interp_exch sigma)) r }.

Section local_safety.

Variable IE : interp_env.

Definition env_move r loc val rX :=
  ∃ tau Srf,
  << DEF: res_plus r rX ≠ Rundef >> ∧
  << TOK: prot_trans_ok (res_get r loc) (res_get rX loc) >> ∧
  << GRF: res_get rX loc = p_at tau Srf >> ∧
  << SP : interp_prot IE tau (get_state Srf) val rX >>.

Require Import c11.

Definition rely (r : resource) (alpha : act) (r': resource) :=
  match alpha with
    | Askip ⇒ r' = r ∧ r' ≠ Rundef
    | Aalloc l n ⇒ r' = r ∧ r' ≠ Rundef
    | Aload typ l v ⇒
         typ = RATna ∧ (∃ pmap gres escr,
                           r = Rdef pmap gres escr ∧
                           r' = r ∧ (∀ k v', pmap l = p_na k v' → v' = v))
       ∨ typ = RATrlx ∧ r' = r ∧ r' ≠ Rundef
       ∨ is_acquire_rtyp typ ∧
           ∃ rY,
             (∀ tau S, res_get r l = p_at tau S → env_move r l v rY) ∧
             r' = res_plus r (res_strip rY) ∧ r' ≠ Rundef
    | Astore typ l _ ⇒
        r' = r ∧ r' ≠ Rundef ∧
        (∀ (REL: is_release_wtyp typ) tau S, res_get r l = p_at tau S →
          ∃ v' rY, env_move r l v' rY)
    | Armw typ l v _ ⇒
      ∃ rY,
        (∀ (REL: is_release_utyp typ) (ACQ: is_acquire_utyp typ) tau S,
          res_get r l = p_at tau S → env_move r l v rY) ∧
        r' = res_plus r rY ∧ r' ≠ Rundef
  end.

Definition atomic_guar (r : resource) l v (r_sb r_rf: resource) :=
  ∃ tau s S',
    << PI : interp_prot IE tau s v r_rf >> ∧
    << REQ: res_plus r_sb r_rf = res_upd r l (p_at tau S') >> ∧
    << Gsb: res_get r_sb l = p_at tau S' >> ∧
    << Grf: res_get r_rf l = p_at tau S' >> ∧
    (<< GET: res_get r l = p_uninit >> ∧
     << SEQ: SL_list S' = s :: nil >>
    ∨ ∃ S,
         << GET : res_get r l = p_at tau S >> ∧
         << LAST: ∀ s0, In s0 (SL_list S) → prot_trans tau s0 s >> ∧
         << SEQ : ∀ s0, In s0 (SL_list S') ↔ s0 = s ∨ In s0 (SL_list S) >>).

Definition guar (r_pre r : resource) (alpha : act) (r_sb r_rf: resource) :=
  match alpha with
    | Askip ⇒ r_sb = r ∧ r_rf = res_emp ∧ r ≠ Rundef
    | Aalloc l n ⇒ r_sb = res_mupd r l n p_uninit
                         ∧ r_rf = res_emp ∧ r ≠ Rundef
    | Aload typ l _ ⇒ r_sb = r ∧ r_rf = res_emp ∧
      ((∃ k v, res_get r l = p_na k v)
       ∨ is_acquire_rtyp typ ∧ (∃ tau S, res_get r l = p_at tau S))
    | Astore typ l v ⇒
          typ = WATna ∧ r_sb = res_upd r l (p_na pe_full v) ∧ r_rf = res_emp ∧
          (res_get r l = p_uninit ∨ ∃ v, res_get r l = p_na pe_full v)
       ∨ << ISREL: is_release_wtyp typ >> ∧
          << AG: atomic_guar r l v r_sb r_rf >> ∧
          << NB: res_get r_pre l ≠ p_bot >> ∧
          << WG: ∀ v' rE (RELY: env_move r_pre l v' rE),
                 prot_trans_ok (res_get rE l) (res_get r_rf l) >>
    | Armw typ l _ v ⇒
        << ISACQ: is_acquire_utyp typ >> ∧
        << ISREL: is_release_utyp typ >> ∧
        << AG: atomic_guar r l v r_sb r_rf >> ∧
        << NB: res_get r_pre l ≠ p_bot >> ∧
        << WG: ∃ tau S, res_get r l = p_at tau S >>
  end.

Inductive ghost_elim (P1 P2 Q : RProp) r0 rE :=
  | GE_left
       (VINS: P1 rE)
       (IN' : ∀ r'', Rstar (Rsingl r0) P2 r'' → Q r'')
  | GE_right
       (VINS: P2 rE)
       (IN' : ∀ r'', Rstar (Rsingl r0) P1 r'' → Q r'').

Inductive ghost_move (r : resource) (Q : RProp) : Prop :=
  | GM_base (RINS: Q r)
  | GM_trans P (GM: ghost_move r P)
       (GM': ∀ r' (SAT: P r'), ghost_move r' Q)
  | GM_extend gone
       (PEQ : ∀ l r'' pmap g g' escr,
               gres_plus (gres_one l gone) g = Some g' →
               res_plus r (Rdef pmap g' escr) = r'' →
               r'' ≠ Rundef →
               Q r'')
  | GM_update p g e (REQ: r = Rdef p g e) g'
       (GDEF : ∀ gF, gres_plus g' gF = None → gres_plus g gF = None)
       (GDOM : ∀ gl, g gl = None → g' gl = None)
       (IN' : Q (Rdef p g' e))
  | GM_eintro sigma r1 r2 P1 P2
       (ESCR: interp_exch IE sigma = (P1 , P2))
       (REQ : r = res_plus r1 r2) (RDEF: r ≠ Rundef)
       (RINS: P1 r2 ∨ P2 r2)
       (IN' : Q (res_plus r1 (Rdef (fun _ ⇒ p_bot) gres_emp
                                   (fun s ⇒ s == sigma))))
  | GM_eelim sigma P1 P2 r0 rE
       (ESCR: interp_exch IE sigma = (P1 , P2))
       (REQ : r = res_plus rE r0) (RDEF: r ≠ Rundef)
       (EIN : res_escr r sigma)
       (GEL : ghost_elim P1 P2 Q r0 rE).

Lemma GM_weaken_post :
  ∀ r Q (GM: ghost_move r Q) (Q' : RProp)
         (IMP: ∀ r, Q r → Q' r),
  ghost_move r Q'.
Proof.
  induction 1; ins; eauto using ghost_move.
Qed.

Definition write_prot_equiv alpha r_pre r' :=
  match alpha with
    | Aalloc l n ⇒
          ∀ loc, l ≤ loc ≤ l + n → res_get r' loc = p_bot
    | Astore typ l _ ⇒
        ∀ (ISREL: is_release_wtyp typ) tau S_pre S,
          res_get r_pre l = p_at tau S_pre →
          res_get r' l = p_at tau S →
          ∃ r_env v_env,
            (∃ Sxxx, res_get r_env l = p_at tau Sxxx
                  ∧ slist_lt S Sxxx) ∧
            env_move r_pre l v_env r_env
    | Armw typ l _ _ ⇒
        ∀ (ISACQ: is_acquire_utyp typ) (ISREL: is_release_utyp typ) tau S,
          res_get r_pre l = p_at tau S →
          ∃ Su,
            res_get r' l = p_at tau Su ∧ get_state S = get_state Su
    | _ ⇒ True
  end.

Fixpoint safe n (e : exp) PP r :=
  match n with 0 ⇒ True | S n ⇒
    << END: ∀ val, e = Evalue val → ghost_move r (PP val) >> ∧
    << FORK: ∀ K (CTX: eval_ctx K) e', e = K (Efork e') →
         ∃ r1 r2, r = res_plus r1 r2 ∧
           safe n (K (Evalue 0)) PP r1 ∧
           safe n e' (fun _ ⇒ Rtrue) r2 >> ∧
    << STEP: ∀ alpha e' (STEP: exp_step e alpha e') rF r_pre
               (RELY : rely (res_plus r rF) alpha r_pre),
         ∃ P',
           ghost_move r_pre P' ∧
           ∀ r' (IN': P' r') (WPE : write_prot_equiv alpha r_pre r'),
           ∃ r_post rx,
             guar r_pre r' alpha (res_plus r_post rF) rx ∧
             safe n e' PP r_post >>
  end.

End local_safety.