Commit b07dd0b5 authored by Robbert Krebbers's avatar Robbert Krebbers

Use bundled type classes for ghost ownership.

* These type classes bundle an identifier into the global CMRA with a proof
  that the identifier points to the correct CMRA. Bundling allows us to get
  rid of many arguments everywhere.

* I have setup the type classes so that we no longer have to keep track of the
  global CMRA identifiers. These are implicit and resolved automatically.

* For heap I am also bundling the name of the heap RA instance. There always
  should be at most one heap instance so this does not introduce ambiguities.

* We now have a "maps to" notation!
parent aebb1246
......@@ -68,9 +68,8 @@ Module barrier_proto.
(* The set of low states *)
Definition low_states : set stateT :=
mkSet (λ s, if state_phase s is Low then True else False).
Lemma low_states_closed :
sts.closed low_states {[ Send ]}.
Lemma low_states_closed : sts.closed low_states {[ Send ]}.
Proof.
split.
- apply (non_empty_inhabited(State Low )). by rewrite !mkSet_elem_of /=.
......@@ -97,9 +96,9 @@ Section proof.
Context {Σ : iFunctorG} (N : namespace).
(* TODO: Bundle HeapI and HeapG and have notation so that we can just write
"l ↦ '0". *)
Context (HeapI : gid) `{!HeapInG Σ HeapI} (HeapG : gname) (HeapN : namespace).
Context (StsI : gid) `{!STSInG heap_lang Σ StsI sts}.
Context (SpI : gid) `{!SavedPropInG heap_lang Σ SpI}.
Context `{heapG Σ} (HeapN : namespace).
Context `{stsG heap_lang Σ sts}.
Context `{savedPropG heap_lang Σ}.
(* TODO We could alternatively construct the namespaces to be disjoint.
But that would take a lot of flexibility from the client, who probably
wants to also use the heap_ctx elsewhere. *)
......@@ -109,28 +108,28 @@ Section proof.
Definition waiting (P : iProp) (I : gset gname) : iProp :=
( R : gname iProp, (P - Π★{set I} (λ i, R i))
Π★{set I} (λ i, saved_prop_own SpI i (R i)))%I.
Π★{set I} (λ i, saved_prop_own i (R i)))%I.
Definition ress (I : gset gname) : iProp :=
(Π★{set I} (λ i, R, saved_prop_own SpI i R R))%I.
(Π★{set I} (λ i, R, saved_prop_own i R R))%I.
Local Notation state_to_val s :=
(match s with State Low _ => 0 | State High _ => 1 end).
Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
(heap_mapsto HeapI HeapG l '(state_to_val s)
(l !=> '(state_to_val s)
match s with State Low I' => waiting P I' | State High I' => ress I' end
)%I.
Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
(heap_ctx HeapI HeapG HeapN sts_ctx StsI sts γ N (barrier_inv l P))%I.
(heap_ctx HeapN sts_ctx γ N (barrier_inv l P))%I.
Definition send (l : loc) (P : iProp) : iProp :=
( γ, barrier_ctx γ l P sts_ownS StsI sts γ low_states {[ Send ]})%I.
( γ, barrier_ctx γ l P sts_ownS γ low_states {[ Send ]})%I.
Definition recv (l : loc) (R : iProp) : iProp :=
( γ (P Q : iProp) i, barrier_ctx γ l P sts_ownS StsI sts γ (i_states i) {[ Change i ]}
saved_prop_own SpI i Q (Q - R))%I.
( γ (P Q : iProp) i, barrier_ctx γ l P sts_ownS γ (i_states i) {[ Change i ]}
saved_prop_own i Q (Q - R))%I.
Lemma newchan_spec (P : iProp) (Q : val iProp) :
( l, recv l P send l P - Q (LocV l)) wp coPset_all (newchan '()) Q.
Proof.
......@@ -142,9 +141,9 @@ Section proof.
rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
(* I think some evars here are better than repeating *everything* *)
eapply (sts_fsaS sts _ (wp_fsa _)) with (N0:=N) (γ0:=γ);simpl; eauto with I.
eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ);simpl; eauto with I.
{ solve_elem_of+. (* FIXME eauto should do this *) }
rewrite [(_ sts_ownS _ _ _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
rewrite [(_ sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
apply const_elim_sep_l=>Hs. destruct p; last done.
rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
......@@ -156,7 +155,7 @@ Section proof.
erewrite later_sep. apply sep_mono_r. apply later_intro. }
apply wand_intro_l. rewrite -(exist_intro (State High I)).
rewrite -(exist_intro ). rewrite const_equiv /=; last first.
{ constructor; first constructor; rewrite /= /tok /=; solve_elem_of+. }
{ constructor; first constructor; rewrite /= /tok /=; solve_elem_of. }
rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
rewrite !assoc [(_ P)%I]comm !assoc -2!assoc.
apply sep_mono; last first.
......
......@@ -9,28 +9,32 @@ Import uPred.
Definition heapRA := mapRA loc (exclRA (leibnizC val)).
Class HeapInG Σ (i : gid) := heap_inG :> InG heap_lang Σ i (authRA heapRA).
Instance heap_inG_auth `{HeapInG Σ i} : AuthInG heap_lang Σ i heapRA.
Proof. split; apply _. Qed.
Class heapG Σ := HeapG {
heap_inG : inG heap_lang Σ (authRA heapRA);
heap_name : gname
}.
Instance heap_authG `{i : heapG Σ} : authG heap_lang Σ heapRA :=
{| auth_inG := heap_inG |}.
Definition to_heap : state heapRA := fmap Excl.
Definition of_heap : heapRA state := omap (maybe Excl).
Definition heap_mapsto {Σ} (i : gid) `{HeapInG Σ i}
(γ : gname) (l : loc) (v : val) : iPropG heap_lang Σ :=
auth_own i γ {[ l Excl v ]}.
Definition heap_inv {Σ} (i : gid) `{HeapInG Σ i}
(h : heapRA) : iPropG heap_lang Σ := ownP (of_heap h).
Definition heap_ctx {Σ} (i : gid) `{HeapInG Σ i}
(γ : gname) (N : namespace) : iPropG heap_lang Σ := auth_ctx i γ N (heap_inv i).
Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l Excl v ]}.
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
ownP (of_heap h).
Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
auth_ctx heap_name N heap_inv.
(* FIXME: ↦ is already used for the singleton empty map. Resolve that... *)
Notation "l !=> v" := (heap_mapsto l v) (at level 20) : uPred_scope.
Section heap.
Context {Σ : iFunctorG} (HeapI : gid) `{!HeapInG Σ HeapI}.
Context {Σ : iFunctorG}.
Implicit Types N : namespace.
Implicit Types P : iPropG heap_lang Σ.
Implicit Types σ : state.
Implicit Types h g : heapRA.
Implicit Types γ : gname.
(** Conversion to heaps and back *)
Global Instance of_heap_proper : Proper (() ==> (=)) of_heap.
......@@ -58,25 +62,15 @@ Section heap.
by case: (h !! l)=> [[]|]; auto.
Qed.
(** Propers *)
Global Instance heap_inv_proper : Proper (() ==> ()) (heap_inv HeapI).
Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
(** General properties of mapsto *)
Lemma heap_mapsto_disjoint γ l v1 v2 :
(heap_mapsto HeapI γ l v1 heap_mapsto HeapI γ l v2)%I False.
Proof.
rewrite /heap_mapsto -auto_own_op auto_own_valid map_op_singleton.
rewrite map_validI (forall_elim l) lookup_singleton.
by rewrite option_validI excl_validI.
Qed.
(** Allocation *)
Lemma heap_alloc N σ :
ownP σ pvs N N ( γ, heap_ctx HeapI γ N Π★{map σ} heap_mapsto HeapI γ).
authG heap_lang Σ heapRA
ownP σ pvs N N ( (_ : heapG Σ), heap_ctx N Π★{map σ} heap_mapsto).
Proof.
rewrite -{1}(from_to_heap σ); etransitivity;
first apply (auth_alloc (ownP of_heap) N (to_heap σ)), to_heap_valid.
apply pvs_mono, exist_mono=> γ; apply and_mono_r.
rewrite -{1}(from_to_heap σ). etransitivity.
{ apply (auth_alloc (ownP of_heap) N (to_heap σ)), to_heap_valid. }
apply pvs_mono, exist_elim=> γ.
rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty; apply True_intro. }
rewrite to_heap_insert big_sepM_insert //.
......@@ -85,18 +79,32 @@ Section heap.
by rewrite auto_own_op IH.
Qed.
Context `{heapG Σ}.
(** Propers *)
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
(** General properties of mapsto *)
Lemma heap_mapsto_disjoint l v1 v2 : (l !=> v1 l !=> v2)%I False.
Proof.
rewrite /heap_mapsto -auto_own_op auto_own_valid map_op_singleton.
rewrite map_validI (forall_elim l) lookup_singleton.
by rewrite option_validI excl_validI.
Qed.
(** Weakest precondition *)
Lemma wp_alloc N E γ e v P Q :
Lemma wp_alloc N E e v P Q :
to_val e = Some v nclose N E
P heap_ctx HeapI γ N
P ( l, heap_mapsto HeapI γ l v - Q (LocV l))
P heap_ctx N
P ( l, l !=> v - Q (LocV l))
P wp E (Alloc e) Q.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
transitivity (pvs E E (auth_own HeapI γ P))%I.
{ by rewrite -pvs_frame_r -(auth_empty E γ) left_id. }
apply wp_strip_pvs, (auth_fsa (heap_inv HeapI) (wp_fsa (Alloc e)))
with N γ ; simpl; eauto with I.
transitivity (pvs E E (auth_own heap_name P))%I.
{ by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I.
rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
rewrite -assoc left_id; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
......@@ -113,16 +121,16 @@ Section heap.
apply later_intro.
Qed.
Lemma wp_load N E γ l v P Q :
Lemma wp_load N E l v P Q :
nclose N E
P heap_ctx HeapI γ N
P ( heap_mapsto HeapI γ l v (heap_mapsto HeapI γ l v - Q v))
P heap_ctx N
P ( l !=> v (l !=> v - Q v))
P wp E (Load (Loc l)) Q.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>HN ? HPQ.
apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id)
with N γ {[ l Excl v ]}; simpl; eauto with I.
rewrite HPQ{HPQ}. apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l Excl v ]}; simpl; eauto with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
......@@ -132,16 +140,15 @@ Section heap.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Qed.
Lemma wp_store N E γ l v' e v P Q :
Lemma wp_store N E l v' e v P Q :
to_val e = Some v nclose N E
P heap_ctx HeapI γ N
P ( heap_mapsto HeapI γ l v'
(heap_mapsto HeapI γ l v - Q (LitV LitUnit)))
P heap_ctx N
P ( l !=> v' (l !=> v - Q (LitV LitUnit)))
P wp E (Store (Loc l) e) Q.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>? HN ? HPQ.
apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v) l))
with N γ {[ l Excl v' ]}; simpl; eauto with I.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
with N heap_name {[ l Excl v' ]}; simpl; eauto with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
......@@ -153,17 +160,16 @@ Section heap.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
Qed.
Lemma wp_cas_fail N E γ l v' e1 v1 e2 v2 P Q :
Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Q :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1
nclose N E
P heap_ctx HeapI γ N
P ( heap_mapsto HeapI γ l v'
(heap_mapsto HeapI γ l v' - Q (LitV (LitBool false))))
P heap_ctx N
P ( l !=> v' (l !=> v' - Q (LitV (LitBool false))))
P wp E (Cas (Loc l) e1 e2) Q.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=>??? HN ? HPQ.
apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) id)
with N γ {[ l Excl v' ]}; simpl; eauto 10 with I.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l Excl v' ]}; simpl; eauto 10 with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
......@@ -174,17 +180,16 @@ Section heap.
apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
Qed.
Lemma wp_cas_suc N E γ l e1 v1 e2 v2 P Q :
Lemma wp_cas_suc N E l e1 v1 e2 v2 P Q :
to_val e1 = Some v1 to_val e2 = Some v2
nclose N E
P heap_ctx HeapI γ N
P ( heap_mapsto HeapI γ l v1
(heap_mapsto HeapI γ l v2 - Q (LitV (LitBool true))))
P heap_ctx N
P ( l !=> v1 (l !=> v2 - Q (LitV (LitBool true))))
P wp E (Cas (Loc l) e1 e2) Q.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? HN ? HPQ.
apply (auth_fsa' (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v2) l))
with N γ {[ l Excl v1 ]}; simpl; eauto 10 with I.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
with N heap_name {[ l Excl v1 ]}; simpl; eauto 10 with I.
rewrite HPQ{HPQ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite {1}[(ownP _)%I]pvs_timeless pvs_frame_r; apply wp_strip_pvs.
......
......@@ -22,15 +22,15 @@ Section LangTests.
End LangTests.
Section LiftingTests.
Context {Σ : iFunctorG} (HeapI : gid) `{!HeapInG Σ HeapI}.
Context `{heapG Σ}.
Implicit Types P : iPropG heap_lang Σ.
Implicit Types Q : val iPropG heap_lang Σ.
Definition e : expr :=
let: "x" := ref '1 in "x" <- !"x" + '1;; !"x".
Goal γh N, heap_ctx HeapI γh N wp N e (λ v, v = '2).
Goal N, heap_ctx N wp N e (λ v, v = '2).
Proof.
move=> γh N. rewrite /e.
move=> N. rewrite /e.
wp_focus (ref '1)%L. eapply wp_alloc; eauto; [].
rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
wp_rec.
......
......@@ -2,53 +2,52 @@ From algebra Require Export auth.
From program_logic Require Export invariants ghost_ownership.
Import uPred.
Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
auth_inG :> InG Λ Σ i (authRA A);
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
is constantly valid. *)
Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
auth_inG :> inG Λ Σ (authRA A);
auth_identity :> CMRAIdentity A;
auth_timeless (a : A) :> Timeless a;
}.
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a is
constantly valid. *)
Section definitions.
Context {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A} (γ : gname).
Context `{authG Λ Σ A} (γ : gname).
Definition auth_inv (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
( a, ( a own i γ ( a)) φ a)%I.
Definition auth_own (a : A) : iPropG Λ Σ := own i γ ( a).
( a, ( a own γ ( a)) φ a)%I.
Definition auth_own (a : A) : iPropG Λ Σ := own γ ( a).
Definition auth_ctx (N : namespace) (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
inv N (auth_inv φ).
End definitions.
Instance: Params (@auth_inv) 7.
Instance: Params (@auth_own) 7.
Instance: Params (@auth_ctx) 8.
Instance: Params (@auth_inv) 6.
Instance: Params (@auth_own) 6.
Instance: Params (@auth_ctx) 7.
Section auth.
Context `{AuthInG Λ Σ AuthI A}.
Context `{AuthI : authG Λ Σ A}.
Context (φ : A iPropG Λ Σ) {φ_proper : Proper (() ==> ()) φ}.
Implicit Types N : namespace.
Implicit Types P Q R : iPropG Λ Σ.
Implicit Types a b : A.
Implicit Types γ : gname.
Global Instance auth_own_ne n γ :
Proper (dist n ==> dist n) (auth_own AuthI γ).
Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
Proof. by rewrite /auth_own=> a b ->. Qed.
Global Instance auth_own_proper γ : Proper (() ==> ()) (auth_own AuthI γ).
Global Instance auth_own_proper γ : Proper (() ==> ()) (auth_own γ).
Proof. by rewrite /auth_own=> a b ->. Qed.
Lemma auto_own_op γ a b :
auth_own AuthI γ (a b) (auth_own AuthI γ a auth_own AuthI γ b)%I.
auth_own γ (a b) (auth_own γ a auth_own γ b)%I.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Lemma auto_own_valid γ a : auth_own AuthI γ a a.
Lemma auto_own_valid γ a : auth_own γ a a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Lemma auth_alloc N a :
a φ a pvs N N ( γ, auth_ctx AuthI γ N φ auth_own AuthI γ a).
a φ a pvs N N ( γ, auth_ctx γ N φ auth_own γ a).
Proof.
intros Ha. eapply sep_elim_True_r.
{ by eapply (own_alloc AuthI (Auth (Excl a) a) N). }
{ by eapply (own_alloc (Auth (Excl a) a) N). }
rewrite pvs_frame_l. apply pvs_strip_pvs.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
transitivity ( auth_inv AuthI γ φ auth_own AuthI γ a)%I.
transitivity ( auth_inv γ φ auth_own γ a)%I.
{ rewrite /auth_inv -later_intro -(exist_intro a).
rewrite const_equiv // left_id.
rewrite [(_ φ _)%I]comm -assoc. apply sep_mono; first done.
......@@ -57,12 +56,12 @@ Section auth.
by rewrite always_and_sep_l.
Qed.
Lemma auth_empty E γ : True pvs E E (auth_own AuthI γ ).
Proof. by rewrite own_update_empty /auth_own. Qed.
Lemma auth_empty γ E : True pvs E E (auth_own γ ).
Proof. by rewrite /auth_own -own_update_empty. Qed.
Lemma auth_opened E γ a :
( auth_inv AuthI γ φ auth_own AuthI γ a)
pvs E E ( a', (a a') φ (a a') own AuthI γ ( (a a') a)).
( auth_inv γ φ auth_own γ a)
pvs E E ( a', (a a') φ (a a') own γ ( (a a') a)).
Proof.
rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
rewrite later_sep [((_ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
......@@ -71,7 +70,7 @@ Section auth.
rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
apply exist_elim=>a'.
rewrite left_id -(exist_intro a').
apply (eq_rewrite b (a a') (λ x, x ▷φ x own AuthI γ ( x a))%I).
apply (eq_rewrite b (a a') (λ x, x φ x own γ ( x a))%I).
{ by move=>n ? ? /timeless_iff ->. }
{ by eauto with I. }
rewrite const_equiv // left_id comm.
......@@ -81,8 +80,8 @@ Section auth.
Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
Lv a (L a a')
( φ (L a a') own AuthI γ ( (a a') a))
pvs E E ( auth_inv AuthI γ φ auth_own AuthI γ (L a)).
( φ (L a a') own γ ( (a a') a))
pvs E E ( auth_inv γ φ auth_own γ (L a)).
Proof.
intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a a')).
rewrite later_sep [(_ ▷φ _)%I]comm -assoc.
......@@ -99,12 +98,12 @@ Section auth.
Lemma auth_fsa E N P (Q : V iPropG Λ Σ) γ a :
fsaV
nclose N E
P auth_ctx AuthI γ N φ
P ( auth_own AuthI γ a a',
P auth_ctx γ N φ
P ( auth_own γ a a',
(a a') φ (a a') -
fsa (E nclose N) (λ x, L Lv (Hup : LocalUpdate Lv L),
(Lv a (L a a')) φ (L a a')
(auth_own AuthI γ (L a) - Q x)))
(auth_own γ (L a) - Q x)))
P fsa E Q.
Proof.
rewrite /auth_ctx=>? HN Hinv Hinner.
......@@ -131,12 +130,12 @@ Section auth.
Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Q: V iPropG Λ Σ) γ a :
fsaV
nclose N E
P auth_ctx AuthI γ N φ
P ( auth_own AuthI γ a ( a',
P auth_ctx γ N φ
P ( auth_own γ a ( a',
(a a') φ (a a') -
fsa (E nclose N) (λ x,
(Lv a (L a a')) φ (L a a')
(auth_own AuthI γ (L a) - Q x))))
(auth_own γ (L a) - Q x))))
P fsa E Q.
Proof.
intros ??? HP. eapply auth_fsa with N γ a; eauto.
......
......@@ -11,101 +11,103 @@ Definition gname := positive.
Definition globalF (Σ : gid iFunctor) : iFunctor :=
iprodF (λ i, mapF gname (Σ i)).
Class InG (Λ : language) (Σ : gid iFunctor) (i : gid) (A : cmraT) :=
inG : A = Σ i (laterC (iPreProp Λ (globalF Σ))).
Class inG (Λ : language) (Σ : gid iFunctor) (A : cmraT) := InG {
inG_id : gid;
inG_prf : A = Σ inG_id (laterC (iPreProp Λ (globalF Σ)))
}.
Definition to_globalF {Λ Σ A}
(i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton i {[ γ cmra_transport inG a ]}.
Definition own {Λ Σ A}
(i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
ownG (to_globalF i γ a).
Instance: Params (@to_globalF) 6.
Instance: Params (@own) 6.
Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton inG_id {[ γ cmra_transport inG_prf a ]}.
Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
ownG (to_globalF γ a).
Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5.
Typeclasses Opaque to_globalF own.
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation iFunctorG := (gid iFunctor).
Section global.
Context {Λ : language} {Σ : iFunctorG} (i : gid) `{!InG Λ Σ i A}.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
(** * Properties of to_globalC *)
Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF i γ).
Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_globalF_op γ a1 a2 :
to_globalF i γ (a1 a2) to_globalF i γ a1 to_globalF i γ a2.
to_globalF γ (a1 a2) to_globalF γ a1 to_globalF γ a2.
Proof.
by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
Qed.
Lemma to_globalF_unit γ a : unit (to_globalF i γ a) to_globalF i γ (unit a).
Lemma to_globalF_unit γ a : unit (to_globalF γ a) to_globalF γ (unit a).
Proof.
by rewrite /to_globalF
iprod_unit_singleton map_unit_singleton cmra_transport_unit.
Qed.
Instance to_globalF_timeless γ m : Timeless m Timeless (to_globalF i γ m).
Instance to_globalF_timeless γ m : Timeless m Timeless (to_globalF γ m).
Proof. rewrite /to_globalF; apply _. Qed.
(** * Transport empty *)
Instance inG_empty `{Empty A} : Empty (Σ i (laterC (iPreProp Λ (globalF Σ)))) :=
cmra_transport inG .
Instance inG_empty `{Empty A} :
Empty (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))) := cmra_transport inG_prf .
Instance inG_empty_spec `{Empty A} :
CMRAIdentity A CMRAIdentity (Σ i (laterC (iPreProp Λ (globalF Σ)))).
CMRAIdentity A CMRAIdentity (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))).
Proof.
split.
* apply cmra_transport_valid, cmra_empty_valid.
* intros x; rewrite /empty /inG_empty; destruct inG. by rewrite left_id.
* intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
* apply _.
Qed.
(** * Properties of own *)
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
Proof. by intros m m' Hm; rewrite /own Hm. Qed.
Global Instance own_proper γ : Proper (() ==> ()) (own i γ) := ne_proper _.
Global Instance own_proper γ : Proper (() ==> ()) (own γ) := ne_proper _.
Lemma own_op γ a1 a2 : own i γ (a1 a2) (own i γ a1 own i γ a2)%I.
Lemma own_op γ a1 a2 : own γ (a1 a2) (own γ a1 own γ a2)%I.
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
Global Instance own_mono γ : Proper (flip () ==> ()) (own i γ).
Global Instance own_mono γ : Proper (flip () ==> ()) (own γ).
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
Lemma always_own_unit γ a : ( own i γ (unit a))%I own i γ (unit a).
Lemma always_own_unit γ a : ( own γ (unit a))%I own γ (unit a).
Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
Lemma own_valid γ a : own i γ a a.
Lemma own_valid γ a : own γ a a.
Proof.
rewrite /own ownG_valid /to_globalF.
rewrite iprod_validI (forall_elim i) iprod_lookup_singleton.
rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
by destruct inG.
by destruct inG_prf.
Qed.
Lemma own_valid_r γ a : own i γ a (own i γ a a).
Lemma own_valid_r γ a : own γ a (own γ a a).
Proof. apply (uPred.always_entails_r _ _), own_valid. Qed.
Lemma own_valid_l γ a : own i γ a ( a own i γ a).
Lemma own_valid_l γ a : own γ a ( a own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
Global Instance own_timeless γ a : Timeless a TimelessP (own i γ a).
Global Instance own_timeless γ a : Timeless a TimelessP (own γ a).
Proof. unfold own; apply _. Qed.
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a E (G : gset gname) : a True pvs E E ( γ, (γ G) own i γ a).
Lemma own_alloc_strong a E (G : gset gname) :
a True pvs E E ( γ, (γ G) own γ a).
Proof.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( γ, γ G m = to_globalF i γ a) ownG m)%I).
* eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha); naive_solver.
rewrite -(pvs_mono _ _ ( m, ( γ, γ G m = to_globalF γ a) ownG m)%I).
* eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty inG_id);
first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
naive_solver.
* apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
by rewrite -(exist_intro γ) const_equiv.
Qed.
Lemma own_alloc a E : a True pvs E E ( γ, own i γ a).
Lemma own_alloc a E : a True pvs E E ( γ, own γ a).
Proof.
intros Ha. rewrite (own_alloc_strong a E ) //; []. apply pvs_mono.
apply exist_mono=>?. eauto with I.
Qed.
Lemma own_updateP P γ a E :
a ~~>: P own i γ a pvs E E ( a', P a' own i γ a').
a ~~>: P own γ a pvs E E ( a', P a' own γ a').
Proof.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalF i γ a' P a') ownG m)%I).
rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalF γ a' P a') ownG m)%I).
* eapply pvs_ownG_updateP, iprod_singleton_updateP;