fcinv.v 9.81 KB
Newer Older
 Robbert Krebbers committed Oct 31, 2018 1 2 3 4 5 6 7 8 9 10 11 12 13 14 ``````(** This file defines the notion of trackable invariants. It provides definitions of the main connectives: - The trackable invariant assertion [fcinv N γ P] - The opening token [fcinv_own γ p] - The deallocation token [fcinv_cancel_own γ p] Contrary to the paper, we define trackable invariants directly in the lifted logic, and do not have the version in the unlifted logic. The construction of trackable invariants follows the usual Iris pattern: it uses Iris cancable invariants, and on top of that, uses an authoritative camera construction to take care of resource transfer. *) From iron.iron_logic Require Export iron. `````` Robbert Krebbers committed Feb 03, 2019 15 ``````From iris.algebra Require Import frac_auth ufrac. `````` Robbert Krebbers committed Oct 31, 2018 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 ``````From iris.proofmode Require Import tactics. Record fcinv_name := FcInvName { fcinv_cinv_name : gname; fcinv_frac_name : gname; }. Instance fcinv_name_eq_dec : EqDecision fcinv_name. Proof. solve_decision. Defined. Instance fcinv_name_inhabited : Inhabited fcinv_name := populate (FcInvName inhabitant inhabitant). (** Use the sealing trick from Iris to improve performance, i.e. to make sure that Coq's type kernel does not blindly unfold these definitions. *) Definition fcinv_own_def `{ironInvG Σ} (γ : fcinv_name) (p : frac) : ironProp Σ := ( ⎡ cinv_own (fcinv_cinv_name γ) p ⎤)%I. Definition fcinv_own_aux `{ironInvG Σ} : seal fcinv_own_def. by eexists. Qed. Definition fcinv_own `{ironInvG Σ} := fcinv_own_aux.(unseal). Definition fcinv_own_eq `{ironInvG Σ} : fcinv_own = _ := fcinv_own_aux.(seal_eq). Definition fcinv_cancel_own_def `{ironInvG Σ} (γ : fcinv_name) (p : frac) : ironProp Σ := FracPred (λ π, if π is Some π `````` Ralf Jung committed Jun 11, 2019 37 `````` then own (fcinv_frac_name γ) (◯F{p} (π:ufrac)) else False)%I. `````` Robbert Krebbers committed Oct 31, 2018 38 39 40 41 42 43 44 45 ``````Definition fcinv_cancel_own_aux `{ironInvG Σ} : seal fcinv_cancel_own_def. by eexists. Qed. Definition fcinv_cancel_own `{ironInvG Σ} := fcinv_cancel_own_aux.(unseal). Definition fcinv_cancel_own_eq `{ironInvG Σ} : fcinv_cancel_own = _ := fcinv_cancel_own_aux.(seal_eq). Definition fcinv_def `{ironInvG Σ, invG Σ} (N : namespace) (γ : fcinv_name) (P : ironProp Σ) : ironProp Σ := ( ⎡ cinv N (fcinv_cinv_name γ) (∃ π1 π2, `````` Ralf Jung committed Jun 11, 2019 46 `````` own (fcinv_frac_name γ) (●F (π1 ⋅? π2 : ufrac)) ∗ perm π1 ∗ P π2) ⎤)%I. `````` Robbert Krebbers committed Oct 31, 2018 47 48 49 50 ``````Definition fcinv_aux `{ironInvG Σ, invG Σ} : seal fcinv_def. by eexists. Qed. Definition fcinv `{ironInvG Σ, invG Σ} := fcinv_aux.(unseal). Definition fcinv_eq `{ironInvG Σ, invG Σ} : fcinv = _ := fcinv_aux.(seal_eq). Arguments fcinv {_ _ _} _ _ _%I. `````` Robbert Krebbers committed Feb 01, 2019 51 ``````Instance: Params (@fcinv) 5 := {}. `````` Robbert Krebbers committed Oct 31, 2018 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 `````` Section fcinv. Context `{ironInvG Σ, invG Σ}. Implicit Types P : ironProp Σ. Global Instance fcinv_own_fractional γ : Fractional (fcinv_own γ). Proof. rewrite fcinv_own_eq=> p1 p2. iStartProof (iProp _); iIntros (π); iSplit. - iIntros "[-> [Hγ Hγ']]". iExists ε, ε. rewrite bi.pure_True // !left_id. iFrame. - iDestruct 1 as (π1 π2 ->) "[[-> Hγ1] [-> Hγ2]] /=". rewrite bi.pure_True // !left_id. by iSplitL "Hγ1". Qed. Global Instance fcinv_own_as_fractional γ p : AsFractional (fcinv_own γ p) (fcinv_own γ) p. Proof. split. done. apply _. Qed. Lemma fcinv_own_valid γ p q : fcinv_own γ p -∗ fcinv_own γ q -∗ ⎡ ✓ (p ⋅ q) ⎤. Proof. rewrite fcinv_own_eq. iStartProof (iProp _); iIntros (π) "[-> H1]"; iIntros (π') "[-> H2]". by iDestruct (cinv_own_valid with "H1 H2") as "?". Qed. Global Instance fcinv_cancel_own_fractional γ : Fractional (fcinv_cancel_own γ). Proof. rewrite fcinv_cancel_own_eq=> p1 p2. iStartProof (iProp _); iIntros (π); iSplit. - iIntros "Hγ". destruct π as [π|]; simpl; [|done]. iDestruct "Hγ" as "[??]". iExists (Some (π / 2)%Qp), (Some (π / 2)%Qp). rewrite -Some_op frac_op' Qp_div_2. by iFrame. - iDestruct 1 as ([π1|] [π2|] ->) "[Hγ1 Hγ2] /="; try done. rewrite frac_auth_frag_op. by iSplitL "Hγ1". Qed. Global Instance fcinv_cancel_own_as_fractional γ p : AsFractional (fcinv_cancel_own γ p) (fcinv_cancel_own γ) p. Proof. split. done. apply _. Qed. Lemma fcinv_cancel_own_valid γ p q : fcinv_cancel_own γ p -∗ fcinv_cancel_own γ q -∗ ⎡ ✓ (p + q)%Qp ⎤. Proof. rewrite fcinv_cancel_own_eq. iStartProof (iProp _); iIntros ([π|]) "H1"; iIntros ([π'|]) "H2 //=". iDestruct (own_valid_2 with "H1 H2") as %Hv. move: Hv. by rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[??]. Qed. Global Instance fcinv_own_timeless p : Timeless (fcinv_own γ p). Proof. rewrite fcinv_own_eq=> γ. apply fracPred_at_timeless_alt. apply _. Qed. Global Instance fcinv_own_affine γ p : Affine (fcinv_own γ p). Proof. rewrite fcinv_own_eq. apply _. Qed. Global Instance fcinv_own_uniform γ p : Uniform (fcinv_own γ p). Proof. apply affine_uniform, _. Qed. Global Instance fcinv_cancel_own_timeless γ p : Timeless (fcinv_cancel_own γ p). Proof. rewrite fcinv_cancel_own_eq. apply fracPred_at_timeless_alt, _. Qed. Global Instance fcinv_ne N γ : Contractive (fcinv N γ). Proof. rewrite fcinv_eq=> n P1 P2 ?. solve_contractive. Qed. Global Instance fcinv_affine N γ P : Affine (fcinv N γ P). Proof. rewrite fcinv_eq. apply _. Qed. Global Instance fcinv_uniform N γ P : Uniform (fcinv N γ P). Proof. apply affine_uniform, _. Qed. Global Instance fcinv_persistent N γ P : Persistent (fcinv N γ P). Proof. rewrite fcinv_eq. apply _. Qed. Lemma fcinv_alloc_strong E N : (|={E}=> ∃ γ, fcinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ fcinv_cancel_own γ 1 ∗ fcinv N γ P)%I. Proof. rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq. iStartProof (iProp _); iIntros (π1) "Hp". `````` Robbert Krebbers committed Mar 06, 2019 123 124 `````` iMod (cinv_alloc_strong (λ _, True) _ N) as (γinv ?) "[Hγinv Halloc]". { apply pred_infinite_True. } `````` Ralf Jung committed Jun 11, 2019 125 `````` iMod (own_alloc (●F (1%Qp : ufrac) ⋅ ◯F (1%Qp : ufrac))) `````` Hai Dang committed May 24, 2019 126 `````` as (γf) "[Hγauth Hγ]"; first by apply auth_both_valid. `````` Robbert Krebbers committed Oct 31, 2018 127 128 129 130 131 132 133 `````` set (γ := FcInvName γinv γf). iModIntro. iExists π1, ε. iSplit; [done|iFrame "Hp"]. iExists γ, ε, ε; iSplit; [done|iSplitL "Hγinv"; [auto|]]. iIntros (P π2) "HP"; iIntros (π3) "[Hp Hp']". iExists (π3 / 2)%Qp, (Some (π3 / 2)%Qp ⋅ π2). iFrame "Hp'". iMod (own_update_2 with "Hγauth Hγ") as "[Hγauth Hγ]". { by apply frac_auth_update, `````` Robbert Krebbers committed Feb 03, 2019 134 `````` (replace_local_update _ ((π3 / 2)%Qp ⋅? π2 : ufrac)). } `````` Ralf Jung committed Jun 11, 2019 135 `````` iMod ("Halloc" \$! (∃ π1 π2, own (fcinv_frac_name γ) (●F (π1 ⋅? π2 : ufrac)) ∗ `````` Robbert Krebbers committed Oct 31, 2018 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 `````` perm π1 ∗ P π2)%I with "[Hγauth Hp HP]"); first by eauto with iFrame. iModIntro; iSplit; [by rewrite -!cmra_opM_opM_assoc_L /= frac_op' Qp_div_2|]. iExists (Some (π3 / 2)%Qp ⋅ π2), ε; iSplit; first by rewrite right_id_L. rewrite Some_op_opM /=. eauto with iFrame. Qed. Lemma fcinv_open_strong E N γ p P `{!Uniform P} : ↑N ⊆ E → fcinv N γ P -∗ fcinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ fcinv_own γ p ∗ (▷ P ∨ fcinv_own γ 1 ∗ fcinv_cancel_own γ 1 ={E∖↑N,E}=∗ emp). Proof. rewrite fcinv_eq fcinv_own_eq fcinv_cancel_own_eq. iStartProof (iProp _). iIntros (? π1) "#[-> ?]"; iIntros (?) "[-> Hγinv]"; iIntros (π2) "Hp". iMod (cinv_open_strong _ N with "[\$] [\$]") as "(Hinv & Hγinv & Hclose)"; first done. iDestruct "Hinv" as (π21 π22) "(>Hγauth & >Hp' & HP)". iAssert (▷ ∃ π3 π4, ⌜ π2 = π3 ⋅? π4 ⌝ ∗ perm (π3 ⋅ (π21 ⋅? π22)) ∗ P π4)%I with "[Hp Hp' HP]" as (π3 π4) "(>-> & >[Hp Hp'] & HP)". { iIntros "/= !>". destruct π22 as [π22|]; last (iExists π2, ε; by iFrame). iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (uniform with "[\$HP \$Hp1]") as "HP". rewrite (comm_L _ π22). iDestruct (uniform with "HP") as "[HP Hp1]". iExists (π2 / 2)%Qp, (Some (π2 / 2)%Qp). iFrame. by rewrite /= !frac_op' Qp_div_2. } iExists π3, π4. iModIntro; iSplit; [done|iFrame "Hp"]. iExists π4, ε; iSplit; [by rewrite right_id_L|iFrame "HP"]. iExists ε, ε; iSplit; [done|]; iSplitL "Hγinv"; [by auto|]. iIntros (π5) "[HP|Hcancel]"; iIntros (π6) "Hp". - iAssert (▷ ∃ π7 π8, ⌜ π21 ⋅? π22 = π7 ⋅? π8 ⌝ ∧ (perm (π7 ⋅ (π6 ⋅? π5)) ∗ P π8))%I with "[HP Hp Hp']" as (π7 π8) "(>-> & >[Hp Hp'] & HP)". { iNext. destruct π5 as [π5|]; last (iExists (π21 ⋅? π22), ε; by iFrame). iDestruct "Hp'" as "[Hp1 Hp2]". iDestruct (uniform with "[\$HP \$Hp1]") as "HP". rewrite (comm_L _ π5). iDestruct (uniform with "HP") as "[HP Hp1]". iExists ((π21 ⋅? π22) / 2)%Qp, (Some ((π21 ⋅? π22) / 2)%Qp). iFrame. by rewrite /= !frac_op' Qp_div_2. } iMod ("Hclose" with "[Hγauth Hp HP]") as "_"; first by eauto with iFrame. iModIntro. iExists (π6 ⋅? π5), ε; iSplit; first by rewrite left_id_L. eauto 10 with iFrame. - iDestruct "Hcancel" as (π7 [π8|] ->) "[[-> Hγinv] Hγ] /="; try done. iMod ("Hclose" with "[Hγinv]") as "_"; first by eauto. iDestruct (own_valid_2 with "Hγauth Hγ") as %<-%frac_auth_agreeL. iExists (π6 ⋅ (π21 ⋅? π22)), ε. eauto with iFrame. Qed. Lemma fcinv_alloc_named E N Ψ : ▷ (∀ γ, Ψ γ) ={E}=∗ ∃ γ, fcinv_own γ 1 ∗ fcinv_cancel_own γ 1 ∗ fcinv N γ (Ψ γ). Proof. iIntros "HΨ". iMod (fcinv_alloc_strong _ N) as (γ) "[Hγ Halloc]". iSpecialize ("HΨ" \$! γ). iMod ("Halloc" with "HΨ") as "[??]". iExists γ; iModIntro; iFrame. Qed. Lemma fcinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, fcinv_own γ 1 ∗ fcinv_cancel_own γ 1 ∗ fcinv N γ P. Proof. iIntros "HP". iApply fcinv_alloc_named; auto. Qed. Lemma fcinv_cancel E N γ P `{!Uniform P} : ↑N ⊆ E → fcinv N γ P -∗ fcinv_cancel_own γ 1 -∗ fcinv_own γ 1 ={E}=∗ ▷ P. Proof. iIntros (?) "#? Hγc Hγ". iMod (fcinv_open_strong with "[\$] [\$]") as "(\$ & Hγ & Hclose)"; first done. iApply "Hclose"; iRight; iFrame. Qed. Lemma fcinv_open E N γ p P `{!Uniform P} : ↑N ⊆ E → fcinv N γ P -∗ fcinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ fcinv_own γ p). Proof. iIntros (?) "#? Hγ". iMod (fcinv_open_strong with "[\$] [\$]") as "(\$ & \$ & Hclose)"; first done. iIntros "!> HP". iApply "Hclose"; auto. Qed. End fcinv.``````