fcinv.v 9.79 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
(** 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.
From iris.algebra Require Import frac_auth.
From iron.algebra Require Import vfrac.
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 Σ :=
  (<affine>  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 π
                 then own (fcinv_frac_name γ) (!{p} (π:vfrac)) else False)%I.
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 Σ :=
  (<affine>  cinv N (fcinv_cinv_name γ) ( π1 π2,
    own (fcinv_frac_name γ) (! (π1 ? π2 : vfrac))  perm π1  P π2) )%I.
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.
52
Instance: Params (@fcinv) 5 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 123 124 125 126 127 128 129 130 131 132 133 134 135 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

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".
  iMod (cinv_alloc_strong  _ N) as (γinv ?) "[Hγinv Halloc]".
  iMod (own_alloc (! (1%Qp : vfrac)  ! (1%Qp : vfrac)))
    as (γf) "[Hγauth Hγ]"; first done.
  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,
      (replace_local_update _ ((π3 / 2)%Qp ? π2 : vfrac)). }
  iMod ("Halloc" $! ( π1 π2, own (fcinv_frac_name γ) (! (π1 ? π2 : vfrac)) 
    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.