auth.v 5.97 KB
 Ralf Jung committed Oct 12, 2016 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 ``````From iris.program_logic Require Export invariants. From iris.algebra Require Export auth. From iris.algebra Require Import gmap. From iris.proofmode Require Import tactics. Import uPred. (* The CMRA we need. *) Class authG Σ (A : ucmraT) := AuthG { auth_inG :> inG Σ (authR A); auth_discrete :> CMRADiscrete A; }. Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ]. Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A. Proof. intros ?%subG_inG ?. by split. Qed. Section definitions. `````` Robbert Krebbers committed Oct 12, 2016 18 19 `````` Context `{irisG Λ Σ, authG Σ A} {T : Type} (γ : gname). `````` Ralf Jung committed Oct 12, 2016 20 21 22 23 24 25 26 27 28 29 30 31 32 `````` Definition auth_own (a : A) : iProp Σ := own γ (◯ a). Definition auth_inv (f : T → A) (φ : T → iProp Σ) : iProp Σ := (∃ t, own γ (● f t) ★ φ t)%I. Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ := inv N (auth_inv f φ). 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_timeless a : TimelessP (auth_own a). Proof. apply _. Qed. `````` Robbert Krebbers committed Oct 12, 2016 33 34 35 36 37 38 39 40 `````` Global Instance auth_own_persistent a : Persistent a → PersistentP (auth_own a). Proof. apply _. Qed. Global Instance auth_inv_ne n : Proper (pointwise_relation T (dist n) ==> pointwise_relation T (dist n) ==> dist n) auth_inv. Proof. solve_proper. Qed. Global Instance auth_inv_proper : `````` Ralf Jung committed Oct 12, 2016 41 `````` Proper (pointwise_relation T (≡) ==> `````` Robbert Krebbers committed Oct 12, 2016 42 43 44 45 46 `````` pointwise_relation T (⊣⊢) ==> (⊣⊢)) auth_inv. Proof. solve_proper. Qed. Global Instance auth_ctx_ne N n : Proper (pointwise_relation T (dist n) ==> pointwise_relation T (dist n) ==> dist n) (auth_ctx N). `````` Ralf Jung committed Oct 12, 2016 47 `````` Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 12, 2016 48 `````` Global Instance auth_ctx_proper N : `````` Ralf Jung committed Oct 12, 2016 49 `````` Proper (pointwise_relation T (≡) ==> `````` Robbert Krebbers committed Oct 12, 2016 50 `````` pointwise_relation T (⊣⊢) ==> (⊣⊢)) (auth_ctx N). `````` Ralf Jung committed Oct 12, 2016 51 52 53 54 55 56 57 `````` Proof. solve_proper. Qed. Global Instance auth_ctx_persistent N f φ : PersistentP (auth_ctx N f φ). Proof. apply _. Qed. End definitions. Typeclasses Opaque auth_own auth_inv auth_ctx. Instance: Params (@auth_own) 4. `````` Robbert Krebbers committed Oct 12, 2016 58 59 ``````Instance: Params (@auth_inv) 5. Instance: Params (@auth_ctx) 8. `````` Ralf Jung committed Oct 12, 2016 60 61 62 63 64 65 66 67 68 69 70 71 72 73 `````` Section auth. Context `{irisG Λ Σ, authG Σ A}. Context {T : Type} `{!Inhabited T}. Context (f : T → A) (φ : T → iProp Σ). Implicit Types N : namespace. Implicit Types P Q R : iProp Σ. Implicit Types a b : A. Implicit Types t u : T. 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. `````` Robbert Krebbers committed Oct 12, 2016 74 75 76 77 78 79 80 81 `````` Global Instance from_sep_auth_own γ a b1 b2 : FromOp a b1 b2 → FromSep (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90. Proof. rewrite /FromOp /FromSep=> <-. by rewrite auth_own_op. Qed. Global Instance into_and_auth_own p γ a b1 b2 : IntoOp a b1 b2 → IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90. Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) auth_own_op. Qed. `````` Ralf Jung committed Oct 12, 2016 82 83 84 85 86 87 `````` Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a. Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed. Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a. Proof. by rewrite /auth_own own_valid auth_validI. Qed. `````` Robbert Krebbers committed Oct 12, 2016 88 89 90 91 92 `````` Global Instance auth_own_cmra_homomorphism : CMRAHomomorphism (auth_own γ). Proof. split. apply _. apply auth_own_op. Qed. Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (auth_own γ). Proof. intros a1 a2. apply auth_own_mono. Qed. `````` Ralf Jung committed Oct 12, 2016 93 94 95 96 97 98 `````` Lemma auth_alloc_strong N E t (G : gset gname) : ✓ (f t) → ▷ φ t ={E}=> ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. iIntros (?) "Hφ". rewrite /auth_own /auth_ctx. iVs (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done. iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']". `````` Robbert Krebbers committed Oct 12, 2016 99 `````` iVs (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?". `````` Ralf Jung committed Oct 12, 2016 100 `````` { iNext. rewrite /auth_inv. iExists t. by iFrame. } `````` Robbert Krebbers committed Oct 12, 2016 101 `````` eauto. `````` Ralf Jung committed Oct 12, 2016 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 `````` Qed. Lemma auth_alloc N E t : ✓ (f t) → ▷ φ t ={E}=> ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t). Proof. iIntros (?) "Hφ". iVs (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto. Qed. Lemma auth_empty γ : True =r=> auth_own γ ∅. Proof. by rewrite /auth_own -own_empty. Qed. Lemma auth_acc E γ a : ▷ auth_inv γ f φ ★ auth_own γ a ={E}=> ∃ t, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b. Proof. iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own. `````` Robbert Krebbers committed Oct 12, 2016 120 121 122 `````` iDestruct "Hinv" as (t) "[>Hγa Hφ]". iVsIntro. iExists t. iDestruct (own_valid_2 with "[\$Hγa \$Hγf]") as % [? ?]%auth_valid_discrete_2. `````` Ralf Jung committed Oct 12, 2016 123 `````` iSplit; first done. iFrame. iIntros (u b) "[% Hφ]". `````` Robbert Krebbers committed Oct 12, 2016 124 125 `````` iVs (own_update_2 with "[\$Hγa \$Hγf]") as "[Hγa Hγf]". { eapply auth_update; eassumption. } `````` Ralf Jung committed Oct 12, 2016 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 `````` iVsIntro. iFrame. iExists u. iFrame. Qed. Lemma auth_open E N γ a : nclose N ⊆ E → auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=> ∃ t, ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b, ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b. Proof. iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose". (* 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 to unpack and repack various proofs. TODO: Make this mostly automatic, by supporting "opening accessors around accessors". *) `````` Robbert Krebbers committed Oct 12, 2016 142 `````` iVs (auth_acc with "[\$Hinv \$Hγf]") as (t) "(?&?&HclAuth)". `````` Ralf Jung committed Oct 12, 2016 143 144 145 146 `````` iVsIntro. iExists t. iFrame. iIntros (u b) "H". iVs ("HclAuth" \$! u b with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv"). Qed. End auth. `````` Robbert Krebbers committed Oct 12, 2016 147 148 `````` Arguments auth_open {_ _ _ _} [_] {_} [_] _ _ _ _ _ _ _.``````