Skip to content
Snippets Groups Projects
Commit a8fe7b7f authored by Ralf Jung's avatar Ralf Jung
Browse files

rename _access -> _acc

parent 1ff665fc
No related branches found
No related tags found
No related merge requests found
...@@ -112,7 +112,7 @@ Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ : ...@@ -112,7 +112,7 @@ Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
inv N P ( P -∗ WP e @ E N {{ v, P Φ v }}) WP e @ E {{ Φ }}. inv N P ( P -∗ WP e @ E N {{ v, P Φ v }}) WP e @ E {{ Φ }}.
Proof. Proof.
iIntros (??) "[#Hinv Hwp]". iIntros (??) "[#Hinv Hwp]".
iMod (inv_access E N P with "Hinv") as "[HP Hclose]"=>//. iMod (inv_acc E N P with "Hinv") as "[HP Hclose]"=>//.
iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|]. iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|].
iIntros (v) "[HP $]". by iApply "Hclose". iIntros (v) "[HP $]". by iApply "Hclose".
Qed. Qed.
......
...@@ -147,7 +147,7 @@ Section auth. ...@@ -147,7 +147,7 @@ Section auth.
iModIntro. iFrame. iExists u. iFrame. iModIntro. iFrame. iExists u. iFrame.
Qed. Qed.
Lemma auth_access E N γ a : Lemma auth_acc E N γ a :
N E N E
auth_ctx γ N f φ auth_own γ a ={E,E∖↑N}=∗ t, auth_ctx γ N f φ auth_own γ a ={E,E∖↑N}=∗ t,
a f t φ t u b, a f t φ t u b,
...@@ -155,7 +155,7 @@ Section auth. ...@@ -155,7 +155,7 @@ Section auth.
Proof using Type*. Proof using Type*.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose". iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors (* The following is essentially a very trivial composition of the accessors
[auth_inv_acc] and [inv_access] -- but since we don't have any good support [auth_inv_acc] and [inv_acc] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having for that currently, this gets more tedious than it should, with us having
to unpack and repack various proofs. to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors TODO: Make this mostly automatic, by supporting "opening accessors
...@@ -166,4 +166,4 @@ Section auth. ...@@ -166,4 +166,4 @@ Section auth.
Qed. Qed.
End auth. End auth.
Arguments auth_access {_ _ _} [_] {_} [_] _ _ _ _ _ _ _. Arguments auth_acc {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
...@@ -109,13 +109,13 @@ Section proofs. ...@@ -109,13 +109,13 @@ Section proofs.
Qed. Qed.
(*** Accessors *) (*** Accessors *)
Lemma cinv_access_strong E N γ p P : Lemma cinv_acc_strong E N γ p P :
N E N E
cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗ cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗
P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}=∗ True)). P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}=∗ True)).
Proof. Proof.
iIntros (?) "Hinv Hown". iIntros (?) "Hinv Hown".
iPoseProof (inv_access ( N) N with "Hinv") as "H"; first done. iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L. rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver. iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]". rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]".
...@@ -126,12 +126,12 @@ Section proofs. ...@@ -126,12 +126,12 @@ Section proofs.
- iDestruct (cinv_own_1_l with "Hown' Hown") as %[]. - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
Qed. Qed.
Lemma cinv_access E N γ p P : Lemma cinv_acc E N γ p P :
N E N E
cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ P cinv_own γ p ( P ={E∖↑N,E}=∗ True). cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ P cinv_own γ p ( P ={E∖↑N,E}=∗ True).
Proof. Proof.
iIntros (?) "#Hinv Hγ". iIntros (?) "#Hinv Hγ".
iMod (cinv_access_strong with "Hinv Hγ") as "($ & $ & H)"; first done. iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
iIntros "!> HP". iIntros "!> HP".
rewrite {2}(union_difference_L (N) E)=> //. rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iLeft. iApply "H". by iLeft.
...@@ -141,7 +141,7 @@ Section proofs. ...@@ -141,7 +141,7 @@ Section proofs.
Lemma cinv_cancel E N γ P : N E cinv N γ P -∗ cinv_own γ 1 ={E}=∗ P. Lemma cinv_cancel E N γ P : N E cinv N γ P -∗ cinv_own γ 1 ={E}=∗ P.
Proof. Proof.
iIntros (?) "#Hinv Hγ". iIntros (?) "#Hinv Hγ".
iMod (cinv_access_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done. iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
rewrite {2}(union_difference_L (N) E)=> //. rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iRight. iApply "H". by iRight.
Qed. Qed.
...@@ -155,7 +155,7 @@ Section proofs. ...@@ -155,7 +155,7 @@ Section proofs.
Proof. Proof.
rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown". rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
rewrite exist_unit -assoc. rewrite exist_unit -assoc.
iApply (cinv_access with "Hinv"); done. iApply (cinv_acc with "Hinv"); done.
Qed. Qed.
End proofs. End proofs.
......
...@@ -27,7 +27,7 @@ Section inv. ...@@ -27,7 +27,7 @@ Section inv.
Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ := Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i (N:coPset) ownI i P)%I. ( i, i (N:coPset) ownI i P)%I.
Lemma own_inv_access E N P : Lemma own_inv_acc E N P :
N E own_inv N P ={E,E∖↑N}=∗ P ( P ={E∖↑N,E}=∗ True). N E own_inv N P ={E,E∖↑N}=∗ P ( P ={E∖↑N,E}=∗ True).
Proof. Proof.
rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]". rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
...@@ -81,7 +81,7 @@ Section inv. ...@@ -81,7 +81,7 @@ Section inv.
Lemma own_inv_to_inv M P: own_inv M P -∗ inv M P. Lemma own_inv_to_inv M P: own_inv M P -∗ inv M P.
Proof. Proof.
iIntros "#I". rewrite inv_eq. iIntros (E H). iIntros "#I". rewrite inv_eq. iIntros (E H).
iPoseProof (own_inv_access with "I") as "H"; eauto. iPoseProof (own_inv_acc with "I") as "H"; eauto.
Qed. Qed.
(** ** Public API of invariants *) (** ** Public API of invariants *)
...@@ -97,7 +97,7 @@ Section inv. ...@@ -97,7 +97,7 @@ Section inv.
Global Instance inv_persistent N P : Persistent (inv N P). Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_eq. apply _. Qed. Proof. rewrite inv_eq. apply _. Qed.
Lemma inv_acc N P Q: Lemma inv_alter N P Q:
inv N P -∗ (P -∗ Q (Q -∗ P)) -∗ inv N Q. inv N P -∗ (P -∗ Q (Q -∗ P)) -∗ inv N Q.
Proof. Proof.
rewrite inv_eq. iIntros "#HI #Acc !>" (E H). rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
...@@ -108,7 +108,7 @@ Section inv. ...@@ -108,7 +108,7 @@ Section inv.
Lemma inv_iff N P Q : (P Q) -∗ inv N P -∗ inv N Q. Lemma inv_iff N P Q : (P Q) -∗ inv N P -∗ inv N Q.
Proof. Proof.
iIntros "#HPQ #HI". iApply (inv_acc with "HI"). iIntros "#HPQ #HI". iApply (inv_alter with "HI").
iIntros "!> !# HP". iSplitL "HP". iIntros "!> !# HP". iSplitL "HP".
- by iApply "HPQ". - by iApply "HPQ".
- iIntros "HQ". by iApply "HPQ". - iIntros "HQ". by iApply "HPQ".
...@@ -127,7 +127,7 @@ Section inv. ...@@ -127,7 +127,7 @@ Section inv.
iApply own_inv_to_inv. done. iApply own_inv_to_inv. done.
Qed. Qed.
Lemma inv_access E N P : Lemma inv_acc E N P :
N E inv N P ={E,E∖↑N}=∗ P ( P ={E∖↑N,E}=∗ True). N E inv N P ={E,E∖↑N}=∗ P ( P ={E∖↑N,E}=∗ True).
Proof. Proof.
rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI". rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
...@@ -146,11 +146,11 @@ Section inv. ...@@ -146,11 +146,11 @@ Section inv.
Qed. Qed.
(** ** Derived properties *) (** ** Derived properties *)
Lemma inv_access_strong E N P : Lemma inv_acc_strong E N P :
N E inv N P ={E,E∖↑N}=∗ P E', P ={E',N E'}=∗ True. N E inv N P ={E,E∖↑N}=∗ P E', P ={E',N E'}=∗ True.
Proof. Proof.
iIntros (?) "Hinv". iIntros (?) "Hinv".
iPoseProof (inv_access ( N) N with "Hinv") as "H"; first done. iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L. rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver. iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro. rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
...@@ -159,16 +159,16 @@ Section inv. ...@@ -159,16 +159,16 @@ Section inv.
by rewrite left_id_L. by rewrite left_id_L.
Qed. Qed.
Lemma inv_access_timeless E N P `{!Timeless P} : Lemma inv_acc_timeless E N P `{!Timeless P} :
N E inv N P ={E,E∖↑N}=∗ P (P ={E∖↑N,E}=∗ True). N E inv N P ={E,E∖↑N}=∗ P (P ={E∖↑N,E}=∗ True).
Proof. Proof.
iIntros (?) "Hinv". iMod (inv_access with "Hinv") as "[>HP Hclose]"; auto. iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!> {$HP} HP". iApply "Hclose"; auto. iIntros "!> {$HP} HP". iApply "Hclose"; auto.
Qed. Qed.
Lemma inv_sep_l N P Q : inv N (P Q) -∗ inv N P. Lemma inv_sep_l N P Q : inv N (P Q) -∗ inv N P.
Proof. Proof.
iIntros "#HI". iApply inv_acc; eauto. iIntros "#HI". iApply inv_alter; eauto.
iIntros "!> !# [$ $] $". iIntros "!> !# [$ $] $".
Qed. Qed.
......
...@@ -91,7 +91,7 @@ Section proofs. ...@@ -91,7 +91,7 @@ Section proofs.
iNext. iLeft. by iFrame. iNext. iLeft. by iFrame.
Qed. Qed.
Lemma na_inv_access p E F N P : Lemma na_inv_acc p E F N P :
N E N F N E N F
na_inv p N P -∗ na_own p F ={E}=∗ P na_own p (F∖↑N) na_inv p N P -∗ na_own p F ={E}=∗ P na_own p (F∖↑N)
( P na_own p (F∖↑N) ={E}=∗ na_own p F). ( P na_own p (F∖↑N) ={E}=∗ na_own p F).
...@@ -121,6 +121,6 @@ Section proofs. ...@@ -121,6 +121,6 @@ Section proofs.
Proof. Proof.
rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown". rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
rewrite exist_unit -assoc /=. rewrite exist_unit -assoc /=.
iApply (na_inv_access with "Hinv"); done. iApply (na_inv_acc with "Hinv"); done.
Qed. Qed.
End proofs. End proofs.
...@@ -150,7 +150,7 @@ Section sts. ...@@ -150,7 +150,7 @@ Section sts.
sts.steps (s, T) (s', T') φ s' ={E}=∗ sts_inv γ φ sts_own γ s' T'. sts.steps (s, T) (s', T') φ s' ={E}=∗ sts_inv γ φ sts_own γ s' T'.
Proof. by apply sts_inv_accS. Qed. Proof. by apply sts_inv_accS. Qed.
Lemma sts_accessS φ E N γ S T : Lemma sts_accS φ E N γ S T :
N E N E
sts_ctx γ N φ sts_ownS γ S T ={E,E∖↑N}=∗ s, sts_ctx γ N φ sts_ownS γ S T ={E,E∖↑N}=∗ s,
s S φ s s' T', s S φ s s' T',
...@@ -158,7 +158,7 @@ Section sts. ...@@ -158,7 +158,7 @@ Section sts.
Proof. Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose". iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors (* The following is essentially a very trivial composition of the accessors
[sts_inv_acc] and [inv_access] -- but since we don't have any good support [sts_inv_acc] and [inv_acc] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having for that currently, this gets more tedious than it should, with us having
to unpack and repack various proofs. to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors TODO: Make this mostly automatic, by supporting "opening accessors
...@@ -168,12 +168,12 @@ Section sts. ...@@ -168,12 +168,12 @@ Section sts.
iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv"). iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
Qed. Qed.
Lemma sts_access φ E N γ s0 T : Lemma sts_acc φ E N γ s0 T :
N E N E
sts_ctx γ N φ sts_own γ s0 T ={E,E∖↑N}=∗ s, sts_ctx γ N φ sts_own γ s0 T ={E,E∖↑N}=∗ s,
sts.frame_steps T s0 s φ s s' T', sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E∖↑N,E}=∗ sts_own γ s' T'. sts.steps (s, T) (s', T') φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
Proof. by apply sts_accessS. Qed. Proof. by apply sts_accS. Qed.
End sts. End sts.
Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx. Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
...@@ -308,7 +308,7 @@ Module linear2. Section linear2. ...@@ -308,7 +308,7 @@ Module linear2. Section linear2.
Context (gname : Type) (cinv : gname PROP PROP) (cinv_own : gname PROP). Context (gname : Type) (cinv : gname PROP PROP) (cinv_own : gname PROP).
Hypothesis cinv_alloc : E, Hypothesis cinv_alloc : E,
fupd E E ( γ, P, P -∗ fupd E E (cinv γ P cinv_own γ))%I. fupd E E ( γ, P, P -∗ fupd E E (cinv γ P cinv_own γ))%I.
Hypothesis cinv_access : P γ, Hypothesis cinv_acc : P γ,
cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 ( P cinv_own γ ( P -∗ fupd M0 M1 emp)). cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 ( P cinv_own γ ( P -∗ fupd M0 M1 emp)).
(** Some general lemmas and proof mode compatibility. *) (** Some general lemmas and proof mode compatibility. *)
...@@ -335,7 +335,7 @@ Module linear2. Section linear2. ...@@ -335,7 +335,7 @@ Module linear2. Section linear2.
iIntros "HP". iIntros "HP".
iMod cinv_alloc as (γ) "Hmkinv". iMod cinv_alloc as (γ) "Hmkinv".
iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]". iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]".
iMod (cinv_access with "Hinv Htok") as "(Htrue & Htok & Hclose)". iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
iApply "Hclose". done. iApply "Hclose". done.
Qed. Qed.
End linear2. End linear2. End linear2. End linear2.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment