Skip to content

GitLab

I
iris
Commit eb36249e authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

accessor-style iInv without Hclose

parent 8a0ff185
Hide whitespace changes
Inline Side-by-side
Showing with 248 additions and 207 deletions
theories/base_logic/lib/auth.v
View file @ eb36249e
......@@ -144,7 +144,8 @@ Section auth.
⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E∖↑N,E}=∗ auth_own γ b.
Proof using Type*.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
iIntros (?) "[Hinv Hγf]". rewrite /auth_ctx.
iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
(* The following is essentially a very trivial composition of the accessors
[auth_acc] and [inv_open] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having
......
theories/base_logic/lib/boxes.v
View file @ eb36249e
......@@ -130,11 +130,11 @@ Lemma slice_delete_empty E q f P Q γ :
Proof.
iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
iInv N as (b) "[>Hγ _]" "Hclose".
iInv N as (b) "[>Hγ _]".
iDestruct (big_opM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
iMod ("Hclose" with "[Hγ]"); first iExists false; eauto.
iModIntro. iSplitL "Hγ"; first iExists false; eauto.
iModIntro. iNext. iSplit.
- iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
......@@ -147,11 +147,11 @@ Lemma slice_fill E q f γ P Q :
slice N γ Q -∗ ▷ Q -∗ ▷?q box N f P ={E}=∗ ▷?q box N (<[γ:=true]> f) P.
Proof.
iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b') "[>Hγ _]" "Hclose".
iInv N as (b') "[>Hγ _]".
iDestruct (big_opM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_opM_insert_override.
- rewrite -insert_delete big_opM_insert ?lookup_delete //.
......@@ -164,13 +164,13 @@ Lemma slice_empty E q f P Q γ :
slice N γ Q -∗ ▷?q box N f P ={E}=∗ ▷ Q ∗ ▷?q box N (<[γ:=false]> f) P.
Proof.
iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b) "[>Hγ HQ]" "Hclose".
iInv N as (b) "[>Hγ HQ]".
iDestruct (big_opM_delete _ f with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iFrame "HQ".
iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_opM_insert_override.
- rewrite -insert_delete big_opM_insert ?lookup_delete //.
......@@ -213,9 +213,9 @@ Proof.
rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
iApply (@big_sepM_impl with "Hf").
iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose".
iInv N as (b) "[>Hγ _]".
iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iApply "Hclose". iNext; iExists true. by iFrame.
iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
Qed.
Lemma box_empty E f P :
......@@ -230,10 +230,10 @@ Proof.
{ rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]" "Hclose".
iInv N as (b) "[>Hγ HΦ]".
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
iModIntro. iSplitL "Hγ"; first (iNext; iExists false; iFrame; eauto).
iFrame "HγΦ Hinv". by iApply "HΦ". }
iModIntro; iSplitL "HΦ".
- rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
......
theories/base_logic/lib/cancelable_invariants.v
View file @ eb36249e
......@@ -73,9 +73,8 @@ Section proofs.
Lemma cinv_cancel E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
Proof.
iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]".
iInv N as "[HP|>Hγ']" "Hclose".
- iMod ("Hclose" with "[Hγ]") as "_"; first by eauto. iModIntro. iNext.
iApply "HP'". done.
iInv N as "[HP|>Hγ']".
- iModIntro. iFrame "Hγ". iModIntro. iApply "HP'". done.
- iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
Qed.
......@@ -84,23 +83,22 @@ Section proofs.
cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]".
iInv N as "[HP | >Hγ']" "Hclose".
iMod (inv_open with "Hinv") as "[[HP | >Hγ'] Hclose]"; first done.
- iIntros "!> {$Hγ}". iSplitL "HP".
+ iNext. iApply "HP'". done.
+ iApply "HP'". done.
+ iIntros "HP". iApply "Hclose". iLeft. iNext. by iApply "HP'".
- iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
Qed.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
Global Instance elim_inv_cinv p γ E N P Q Q' :
(∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p)
(▷ P ∗ cinv_own γ p) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
Global Instance elim_inv_cinv E N γ P p Q Q' :
InvOpener E (E∖↑N) (▷ P ∗ cinv_own γ p) (▷ P) None Q Q' →
ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p) (▷ P ∗ cinv_own γ p) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
rewrite /ElimInv /InvOpener. iIntros (Helim ?) "(#Hinv & Hown & Hcont)".
iApply (Helim with "Hcont"). clear Helim. rewrite -assoc.
iApply (cinv_open with "Hinv"); done.
Qed.
End proofs.
......
theories/base_logic/lib/invariants.v
View file @ eb36249e
......@@ -110,12 +110,11 @@ Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N.
Global Instance elim_inv_inv E N P Q Q' :
(∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
ElimInv (↑N ⊆ E) (inv N P) True (▷ P) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
InvOpener E (E∖↑N) (▷ P) (▷ P) None Q Q' →
ElimInv (↑N ⊆ E) (inv N P) True (▷ P) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
iApply (Helim with "[H2]"); [done|]; simpl. iSplitR "H2"; [|done].
iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
rewrite /ElimInv /InvOpener. iIntros (Hopener ?) "(#Hinv & _ & Hcont)".
iApply (Hopener with "Hcont"). iApply inv_open; done.
Qed.
Lemma inv_open_timeless E N P `{!Timeless P} :
......
theories/base_logic/lib/na_invariants.v
View file @ eb36249e
......@@ -101,25 +101,26 @@ Section proofs.
rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".
iMod (inv_open with "Hinv") as "[[[$ >Hdis]|>Htoki2] Hclose]"; first done.
- iMod ("Hclose" with "[Htoki]") as "_"; first auto.
iIntros "!> [HP $]".
iInv N as "[[_ >Hdis2]|>Hitok]" "Hclose".
iInv N as "[[_ >Hdis2]|>Hitok]".
+ iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
set_solver.
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
+ iSplitR "Hitok"; last by iFrame. eauto with iFrame.
- iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
Qed.
Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
Global Instance elim_inv_na p F E N P Q Q':
(∀ R, ElimModal True false false (|={E}=> R)%I R Q Q') →
InvOpener E E (▷ P ∗ na_own p (F ∖ ↑ N)) (▷ P ∗ na_own p (F ∖ ↑ N))
(Some (na_own p F)) Q Q' →
ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F)
(▷ P ∗ na_own p (F∖↑N)) (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F) Q Q'.
(▷ P ∗ na_own p (F∖↑N)) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
rewrite /ElimInv /InvOpener. iIntros (Helim (?&?)) "(#Hinv & Hown & Hcont)".
iApply (Helim with "Hcont"). clear Helim. rewrite -assoc /=.
iApply (na_inv_open with "Hinv"); done.
Qed.
End proofs.
theories/base_logic/lib/sts.v
View file @ eb36249e
......@@ -156,7 +156,8 @@ Section sts.
⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
iIntros (?) "[Hinv Hγf]". rewrite /sts_ctx.
iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
(* The following is essentially a very trivial composition of the accessors
[sts_acc] and [inv_open] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having
......
theories/base_logic/lib/viewshifts.v
View file @ eb36249e
......@@ -72,7 +72,8 @@ Qed.
Lemma vs_inv N E P Q R :
↑N ⊆ E → inv N R ∗ (▷ R ∗ P ={E∖↑N}=> ▷ R ∗ Q) ⊢ P ={E}=> Q.
Proof.
iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
iIntros (?) "#[Hinv Hvs] !# HP".
iMod (inv_open with "Hinv") as "[HR Hclose]"; first done.
iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
by iApply "Hclose".
Qed.
......
theories/heap_lang/lib/counter.v
View file @ eb36249e
......@@ -46,24 +46,24 @@ Section mono_proof.
{{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
Proof.
iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "[#Hinv Hγf]".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
iDestruct "Hl" as (γ) "[#? Hγf]".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ (S c)); auto. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
wp_cas_suc. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf"). apply: auth_frag_mono.
by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
rewrite {3}/mcounter; eauto 10.
Qed.
......@@ -71,12 +71,13 @@ Section mono_proof.
{{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
Proof.
iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]".
iApply wp_fupd. wp_load.
iDestruct (own_valid_2 with "Hγ Hγf")
as %[?%mnat_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply auth_update, (mnat_local_update _ _ c); auto. }
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
Qed.
End mono_proof.
......@@ -123,19 +124,19 @@ Section contrib_spec.
{{{ RET #(); ccounter γ q (S n) }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
wp_let. wp_op.
wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
destruct (decide (c' = c)) as [->|].
- iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
{ apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); omega. }
wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
wp_cas_suc. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
iModIntro. wp_if. by iApply "HΦ".
wp_if. by iApply "HΦ".
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
Qed.
Lemma read_contrib_spec γ l q n :
......@@ -143,9 +144,9 @@ Section contrib_spec.
{{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
Qed.
......@@ -154,9 +155,9 @@ Section contrib_spec.
{{{ n, RET #n; ccounter γ 1 n }}}.
Proof.
iIntros (Φ) "[#? Hγf] HΦ".
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]". wp_load.
iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
by iApply "HΦ".
Qed.
End contrib_spec.
theories/heap_lang/lib/increment.v
View file @ eb36249e
......@@ -68,7 +68,7 @@ Section increment_client.
WP incr_client #x {{ _, True }}%I.
Proof using Type*.
wp_let. wp_alloc l as "Hl". wp_let.
iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
(* FIXME: I am only usign persistent stuff, so I should be allowed
to move this to the persisten context even without the additional □. *)
iAssert (□ atomic_update (λ (v: Z), l ↦ #v)
......@@ -78,7 +78,8 @@ Section increment_client.
{ iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
iIntros "!#" (E) "% _".
assert (E = ⊤) as -> by set_solver.
iInv nroot as (x) ">H↦" "Hclose".
iMod (inv_open with "Hinv") as "[>H↦ Hclose]"; first done.
iDestruct "H↦" as (x) "H↦".
iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
iExists _. iFrame. iSplit.
{ iIntros "H↦". iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"); last done.
......
theories/heap_lang/lib/spawn.v
View file @ eb36249e
......@@ -55,21 +55,21 @@ Proof.
wp_apply wp_fork; simpl. iSplitR "Hf".
- wp_seq. iApply "HΦ". rewrite /join_handle. eauto.
- wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
iInv N as (v') "[Hl _]".
wp_store. iSplit; last done. iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
Lemma join_spec (Ψ : val → iProp Σ) l :
{{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
Proof.
iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
- iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
- iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. by iApply "HΦ".
+ iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
wp_match. by iApply "HΦ".
+ iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
Qed.
End proof.
......
theories/heap_lang/lib/spin_lock.v
View file @ eb36249e
......@@ -61,12 +61,12 @@ Section proof.
{{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
Proof.
iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). done.
wp_rec. iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iSplitL "Hl"; first (iNext; iExists true; eauto).
iApply ("HΦ" $! false). done.
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
iSplitL "Hl"; first (iNext; iExists true; eauto).
rewrite /locked. by iApply ("HΦ" $! true with "[$Hγ $HR]").
Qed.
Lemma acquire_spec γ lk R :
......@@ -83,8 +83,9 @@ Section proof.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l ->) "#Hinv".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]".
wp_store. iSplitR "HΦ"; last by iApply "HΦ".
iNext. iExists false. by iFrame.
Qed.
End proof.
......
theories/heap_lang/lib/ticket_lock.v
View file @ eb36249e
......@@ -88,20 +88,18 @@ Section proof.
Proof.
iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
iInv N as (o n) "(Hlo & Hln & Ha)".
wp_load. destruct (decide (x = o)) as [->|Hneq].
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+ iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
+ iSplitL "Hlo Hln Hainv Ht".
{ iNext. iExists o, n. iFrame. }
iModIntro. wp_let. wp_op. case_bool_decide; [|done].
wp_if.
wp_let. wp_op. case_bool_decide; [|done]. wp_if.
iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
+ iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
set_solver.
- iMod ("Hclose" with "[Hlo Hln Ha]").
- iSplitL "Hlo Hln Ha".
{ iNext. iExists o, n. by iFrame. }
iModIntro. wp_let.
wp_op. case_bool_decide; [simplify_eq |].
wp_let. wp_op. case_bool_decide; [simplify_eq |].
wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
Qed.
......@@ -110,30 +108,28 @@ Section proof.
Proof.
iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
iInv N as (o n) "[Hlo [Hln Ha]]".
wp_load. iSplitL "Hlo Hln Ha".
{ iNext. iExists o, n. by iFrame. }
iModIntro. wp_let. wp_proj. wp_op.
wp_bind (CAS _ _ _).
iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)" "Hclose".
wp_let. wp_proj. wp_op. wp_bind (CAS _ _ _).
iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
- wp_cas_suc.
iMod (own_update with "Hauth") as "[Hauth Hofull]".
- iMod (own_update with "Hauth") as "[Hauth Hofull]".
{ eapply auth_update_alloc, prod_local_update_2.
eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
apply (seq_set_S_disjoint 0). }
rewrite -(seq_set_S_union_L 0).
iMod ("Hclose" with "[Hlo' Hln' Haown Hauth]") as "_".
wp_cas_suc. iSplitL "Hlo' Hln' Haown Hauth".
{ iNext. iExists o', (S n).
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
iModIntro. wp_if.
wp_if.
iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+ iFrame. rewrite /is_lock; eauto 10.
+ by iNext.
- wp_cas_fail.
iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
iSplitL "Hlo' Hln' Hauth Haown".
{ iNext. iExists o', n'. by iFrame. }
iModIntro. wp_if. by iApply "IH"; auto.
wp_if. by iApply "IH"; auto.
Qed.
Lemma release_spec γ lk R :
......@@ -142,15 +138,15 @@ Section proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iDestruct "Hγ" as (o) "Hγo".
wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
wp_load.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iMod ("Hclose" with "[Hlo Hln Hauth Haown]") as "_".
iSplitL "Hlo Hln Hauth Haown".
{ iNext. iExists o, n. by iFrame. }
iModIntro. wp_op.
iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
wp_store.
wp_op.
iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
iApply wp_fupd. wp_store.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iDestruct "Haown" as "[[Hγo' _]|Haown]".
......@@ -158,7 +154,7 @@ Section proof.
iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
{ apply auth_update, prod_local_update_1.
by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
iMod ("Hclose" with "[Hlo Hln Hauth Haown Hγo HR]") as "_"; last by iApply "HΦ".
iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
iNext. iExists (S o), n'.
rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
Qed.
......
theories/program_logic/weakestpre.v
View file @ eb36249e
......@@ -404,4 +404,26 @@ Section proofmode_classes.
Global Instance add_modal_fupd_wp s E e P Φ :
AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
Global Instance inv_opener_wp E1 E2 P P' (P'' : option _) e s Φ :
Atomic (stuckness_to_atomicity s) e →
InvOpener E1 E2 P P' P'' (WP e @ s; E1 {{ Φ }})
(WP e @ s; E2 {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
Proof.
intros ?. rewrite /InvOpener. setoid_rewrite coq_tactics.maybe_wand_sound.
iIntros "Hinner >[HP Hclose]".
iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".
Qed.
Global Instance inv_opener_wp_nonatomic E P P' (P'' : option _) e s Φ :
InvOpener E E P P' P'' (WP e @ s; E {{ Φ }})
(WP e @ s; E {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
Proof.
rewrite /InvOpener. setoid_rewrite coq_tactics.maybe_wand_sound.
iIntros "Hinner >[HP Hclose]". iApply wp_fupd.
iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".
Qed.
End proofmode_classes.
theories/proofmode/class_instances_sbi.v
View file @ eb36249e
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics.
From iris.proofmode Require Import modality_instances classes.
From iris.proofmode Require Import modality_instances classes class_instances_bi ltac_tactics.
Set Default Proof Using "Type".
Import bi.
......@@ -551,6 +551,18 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
Proof. by rewrite /AddModal !embed_fupd. Qed.
(* InvOpener *)
Global Instance inv_opener_vs `{BiFUpd PROP} E1 E2 E P P' (P'' : option PROP) Q :
(* FIXME: Why %I? ElimInv should set the right scopes! *)
InvOpener E1 E2 P P' P''
(|={E1,E}=> Q) (|={E2}=> (P' ∗ (coq_tactics.maybe_wand P'' (|={E1,E}=> Q))))%I.
Proof.
rewrite /InvOpener coq_tactics.maybe_wand_sound.
iIntros "Hinner >[HP Hclose]".
iMod (