Library iris.program_logic.auth
From iris.algebra Require Export auth upred_tactics.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import invariants ghost_ownership pstepshifts.
Import uPred.
Class authG Λ Σ (A : ucmraT) := AuthG {
auth_inG :> inG Λ Σ (gmapUR gname (authR A));
auth_timeless :> CMRADiscrete A;
}.
Definition authGF (A : ucmraT) : gFunctor := GFunctor (gmapURF gname (constRF (authR A))).
Instance authGF_inGF (A : ucmraT) `{inGF Λ Σ (authGF A)}
`{CMRADiscrete A} : authG Λ Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed.
Section definitions.
Context `{authG Λ Σ A} (γ : gname).
Definition auth_own (a : A) : iPropG Λ Σ :=
own γ (◯ a).
Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
(∃ a, own γ (● a) ★ ⧆φ a)%I.
Definition auth_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
inv N (auth_inv φ).
Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_affine a : AffineP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_own_atimeless a : ATimelessP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_ctx_relevant N φ : RelevantP (auth_ctx N φ).
Proof. apply _. Qed.
Global Instance auth_ctx_affine N φ : AffineP (auth_ctx N φ).
Proof. apply _. Qed.
Global Instance auth_inv_ne n :
Proper (pointwise_relation A (dist n) ==> dist n) (auth_inv).
Proof. solve_proper. Qed.
Global Instance auth_ctx_ne n N :
Proper (pointwise_relation A (dist n) ==> dist n) (auth_ctx N).
Proof. solve_proper. Qed.
End definitions.
Typeclasses Opaque auth_own auth_ctx.
Instance: Params (@auth_inv) 5.
Instance: Params (@auth_own) 5.
Instance: Params (@auth_ctx) 6.
Section auth.
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.
Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Global Instance auth_own_relevant γ a :
Persistent a → RelevantP (auth_own γ a).
Proof. rewrite /auth_own. apply _. Qed.
Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
Proof. intros [? ->]. by rewrite auth_own_op affine_sep_elim_l'. Qed.
Lemma auth_own_valid γ a : auth_own γ a ⊢ ⧆✓ a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Lemma auth_alloc_strong N E a (G : gset gname) :
✓ a → nclose N ⊆ E →
⧆▷ φ a ={E}=> ∃ γ, ⧆■(γ ∉ G) ★ auth_ctx γ N φ ★ auth_own γ a.
Proof.
iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc_strong' (Auth (Excl' a) a) _ G) as (γ) "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
{ iIntros "@". iNext. iExists a. by iFrame. }
iPvsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
Qed.
Lemma auth_alloc N E a :
✓ a → nclose N ⊆ E →
⧆▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ★ auth_own γ a.
Proof.
iIntros (??) "Hφ".
iPvs (auth_alloc_strong N E a ∅ with "Hφ") as (γ) "[_ ?]"; [done..|].
by iExists γ.
Qed.
Lemma auth_empty γ E : Emp ={E}=> auth_own γ ∅.
Proof. by rewrite -own_empty. Qed.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!AffineFrameShiftAssertion fsaV fsa}.
Lemma auth_afsa E N (Ψ : V → iPropG Λ Σ) γ a :
fsaV → nclose N ⊆ E →
auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ (∀ af,
⧆■ ✓ (a ⋅ af) ★ ⧆▷ φ (a ⋅ af) -★
fsa (E ∖ nclose N) (λ x, ∃ b,
⧆■ (a ¬l~> b @ Some af) ★ ⧆▷ φ (b ⋅ af) ★ (auth_own γ b -★ Ψ x)))
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affine_elim (own γ _)).
iDestruct (own_valid with "#Hγ") as "Hvalid".
iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl.
iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_afsa_afsa. iApply afsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ". iSplitL ""; first by iPureIntro.
by rewrite -affine_affine_later. }
iIntros "@". iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iIntros "@". iNext. iExists (b ⋅ af). by iFrame.
Qed.
Global Instance from_assumption_affine p P Q:
FromAssumption p P Q → FromAssumption p (⧆P) Q.
Proof. destruct p; by rewrite /FromAssumption /= ?affine_elim. Qed.
Lemma auth_afsa_alt E N (Ψ : V → iPropG Λ Σ) γ a :
fsaV → nclose N ⊆ E →
auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ (∀ af,
⧆■ ✓ (a ⋅ af) ★ ⧆▷ φ (a ⋅ af) -★
∃ b, ⧆■ (a ¬l~> b @ Some af) ★ (auth_own γ b -★
fsa (E ∖ nclose N) (λ x, ⧆▷ φ (b ⋅ af) ★ Ψ x)))
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affine_elim (own γ _)).
iDestruct (own_valid with "#Hγ") as "Hvalid".
iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl.
iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_afsa_afsa.
iDestruct ("HΨ" $! af with "[Hφ]") as (b) "(%&HΨ)".
{ iSplitL ""; first done. iIntros "@". iNext. iAssumption. }
iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iSpecialize ("HΨ" with "Hγf").
iApply afsa_wand_r. iSplitL "HΨ".
{ iClear "Hinv". iClear "Hvalid". iAssumption. }
iIntros "@". iIntros (v) "HL". iDestruct "HL" as "(Hφ & HΨ)".
iPvsIntro. iSplitL "Hφ Hγ".
- iIntros "@". rewrite /auth_inv.
iNext. iExists (b ⋅ af). by iFrame "Hφ".
- iAssumption.
Qed.
End auth.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import invariants ghost_ownership pstepshifts.
Import uPred.
Class authG Λ Σ (A : ucmraT) := AuthG {
auth_inG :> inG Λ Σ (gmapUR gname (authR A));
auth_timeless :> CMRADiscrete A;
}.
Definition authGF (A : ucmraT) : gFunctor := GFunctor (gmapURF gname (constRF (authR A))).
Instance authGF_inGF (A : ucmraT) `{inGF Λ Σ (authGF A)}
`{CMRADiscrete A} : authG Λ Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed.
Section definitions.
Context `{authG Λ Σ A} (γ : gname).
Definition auth_own (a : A) : iPropG Λ Σ :=
own γ (◯ a).
Definition auth_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
(∃ a, own γ (● a) ★ ⧆φ a)%I.
Definition auth_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
inv N (auth_inv φ).
Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_affine a : AffineP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_own_atimeless a : ATimelessP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_ctx_relevant N φ : RelevantP (auth_ctx N φ).
Proof. apply _. Qed.
Global Instance auth_ctx_affine N φ : AffineP (auth_ctx N φ).
Proof. apply _. Qed.
Global Instance auth_inv_ne n :
Proper (pointwise_relation A (dist n) ==> dist n) (auth_inv).
Proof. solve_proper. Qed.
Global Instance auth_ctx_ne n N :
Proper (pointwise_relation A (dist n) ==> dist n) (auth_ctx N).
Proof. solve_proper. Qed.
End definitions.
Typeclasses Opaque auth_own auth_ctx.
Instance: Params (@auth_inv) 5.
Instance: Params (@auth_own) 5.
Instance: Params (@auth_ctx) 6.
Section auth.
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.
Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Global Instance auth_own_relevant γ a :
Persistent a → RelevantP (auth_own γ a).
Proof. rewrite /auth_own. apply _. Qed.
Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
Proof. intros [? ->]. by rewrite auth_own_op affine_sep_elim_l'. Qed.
Lemma auth_own_valid γ a : auth_own γ a ⊢ ⧆✓ a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Lemma auth_alloc_strong N E a (G : gset gname) :
✓ a → nclose N ⊆ E →
⧆▷ φ a ={E}=> ∃ γ, ⧆■(γ ∉ G) ★ auth_ctx γ N φ ★ auth_own γ a.
Proof.
iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc_strong' (Auth (Excl' a) a) _ G) as (γ) "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
{ iIntros "@". iNext. iExists a. by iFrame. }
iPvsIntro; iExists γ. iSplit; first by iPureIntro. by iFrame.
Qed.
Lemma auth_alloc N E a :
✓ a → nclose N ⊆ E →
⧆▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ★ auth_own γ a.
Proof.
iIntros (??) "Hφ".
iPvs (auth_alloc_strong N E a ∅ with "Hφ") as (γ) "[_ ?]"; [done..|].
by iExists γ.
Qed.
Lemma auth_empty γ E : Emp ={E}=> auth_own γ ∅.
Proof. by rewrite -own_empty. Qed.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!AffineFrameShiftAssertion fsaV fsa}.
Lemma auth_afsa E N (Ψ : V → iPropG Λ Σ) γ a :
fsaV → nclose N ⊆ E →
auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ (∀ af,
⧆■ ✓ (a ⋅ af) ★ ⧆▷ φ (a ⋅ af) -★
fsa (E ∖ nclose N) (λ x, ∃ b,
⧆■ (a ¬l~> b @ Some af) ★ ⧆▷ φ (b ⋅ af) ★ (auth_own γ b -★ Ψ x)))
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affine_elim (own γ _)).
iDestruct (own_valid with "#Hγ") as "Hvalid".
iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl.
iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_afsa_afsa. iApply afsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ". iSplitL ""; first by iPureIntro.
by rewrite -affine_affine_later. }
iIntros "@". iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iIntros "@". iNext. iExists (b ⋅ af). by iFrame.
Qed.
Global Instance from_assumption_affine p P Q:
FromAssumption p P Q → FromAssumption p (⧆P) Q.
Proof. destruct p; by rewrite /FromAssumption /= ?affine_elim. Qed.
Lemma auth_afsa_alt E N (Ψ : V → iPropG Λ Σ) γ a :
fsaV → nclose N ⊆ E →
auth_ctx γ N φ ★ ⧆▷ auth_own γ a ★ (∀ af,
⧆■ ✓ (a ⋅ af) ★ ⧆▷ φ (a ⋅ af) -★
∃ b, ⧆■ (a ¬l~> b @ Some af) ★ (auth_own γ b -★
fsa (E ∖ nclose N) (λ x, ⧆▷ φ (b ⋅ af) ★ Ψ x)))
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affine_elim (own γ _)).
iDestruct (own_valid with "#Hγ") as "Hvalid".
iDestruct (auth_validI' _ with "Hvalid") as "[Ha' %]"; simpl.
iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_afsa_afsa.
iDestruct ("HΨ" $! af with "[Hφ]") as (b) "(%&HΨ)".
{ iSplitL ""; first done. iIntros "@". iNext. iAssumption. }
iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iSpecialize ("HΨ" with "Hγf").
iApply afsa_wand_r. iSplitL "HΨ".
{ iClear "Hinv". iClear "Hvalid". iAssumption. }
iIntros "@". iIntros (v) "HL". iDestruct "HL" as "(Hφ & HΨ)".
iPvsIntro. iSplitL "Hφ Hγ".
- iIntros "@". rewrite /auth_inv.
iNext. iExists (b ⋅ af). by iFrame "Hφ".
- iAssumption.
Qed.
End auth.