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.

B.2. Semantic structures

B.2.1. Parameters

Assume a partial order per protocol type.

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

Type for exchanges

Inductive escrowTy := mkEscrowTy (n : nat).

Decidable equality on escrow types

Definition eq_escrow (x y: escrowTy) :=
   match x, y with
     | mkEscrowTy n1, mkEscrowTy n2n1 == 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.

B.2.2. Domains

Traces

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 frev 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.

Protocols

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

Arguments p_at : clear implicits.

Ghost resources: see GpsSepAlg.v
Resources

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

B.2.3. Resource composition

Protocol composition

Definition prot_plus (pi1 pi2 : protocol) :=
  match pi1, pi2 with
    | p_bot, _Some pi2
    | _, p_botSome 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 taulist (prot_state tau)) (SL_list s2) _ PF) with
            | Some sSome (p_at tau1 s)
            | NoneNone
          end
        | _None
      end
    | p_na k1 v1, p_na k2 v2
        if v1 == v2 then
          match fraction_plus k1 k2 with
            | Some kSome (p_na k v1)
            | NoneNone
          end
        else None
    | _, _None
  end.

Empty resource

Definition res_emp : resource :=
  Rdef (fun _p_bot) gres_emp (fun _false).

Resource composition

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

Multiple resource composition

Fixpoint rsum rl :=
  match rl with
    | nilres_emp
    | a :: rlres_plus a (rsum rl)
  end.

Read location from resource

Definition res_get r loc :=
  match r with
    | Rundefp_bot
    | Rdef pmap _ _pmap loc
  end.

Resource update

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

Resource multiple update

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

Read ghost location from resource

Definition res_gget r l :=
  match r with
    | RundefNone
    | Rdef p g eg l
  end.

Read escrow from resource

Definition res_escr r sigma :=
  match r with
      RundefFalse
    | Rdef p g ee sigma
  end.

Trace comparison

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'.

Protocol transition is allowed

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.

ACI properties of protocol composition

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.

ACIZ properties of resource composition

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.

The composition preorder on resources

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.

B.2.4. Resource stripping


Definition prot_strip (pi : protocol) :=
  match pi with
    | p_at _ _pi
    | _p_bot
  end.

Definition res_strip (r : resource) :=
  match r with
    | RundefRundef
    | Rdef p g eRdef (fun locprot_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.

B.2.5. Propositions


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.

B.2.6. Exchanger and protocol type interpretations


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 }.

B.3. Local safety


Section local_safety.

Variable IE : interp_env.

B.3.1. Protocols


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

B.3.2. Rely/guarantee


Require Import c11.

Definition rely (r : resource) (alpha : act) (r': resource) :=
  match alpha with
    | Askipr' = r r' Rundef
    | Aalloc l nr' = 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
    | Askipr_sb = r r_rf = res_emp r Rundef
    | Aalloc l nr_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.

B.3.3. Ghost moves


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 ss == 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.

B.3.4. Protocol equivalence for writes


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.

B.3.5. Local safety


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.

This page has been generated by coqdoc