ownp.v 9.7 KB
Newer Older
1 2 3 4 5
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
From iris.algebra Require Import auth.
From iris.proofmode Require Import tactics classes.
6
Set Default Proof Using "Type*".
7 8 9 10 11 12 13 14 15 16 17 18

Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
  ownP_invG : invG Σ;
  ownP_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
  ownP_name : gname;
}.
Notation ownPG Λ Σ := (ownPG' (state Λ) Σ).

Instance ownPG_irisG `{ownPG' Λstate Σ} : irisG' Λstate Σ := {
  iris_invG := ownP_invG;
  state_interp σ := own ownP_name ( (Excl' (σ:leibnizC Λstate)))
}.
19
Global Opaque iris_invG.
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 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 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 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233

Definition ownPΣ (Λstate : Type) : gFunctors :=
  #[invΣ;
    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].

Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
  ownPPre_invG :> invPreG Σ;
  ownPPre_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
}.
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).

Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ  ownPPreG' Λstate Σ.
Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.


(** Ownership *)
Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
  own ownP_name ( (Excl' σ)).
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3.


(* Adequacy *)
Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} e σ φ :
  ( `{ownPG Λ Σ}, ownP σ  WP e {{ v, ⌜φ v }}) 
  adequate e σ φ.
Proof.
  intros Hwp. apply (wp_adequacy Σ _).
  iIntros (?) "". iMod (own_alloc ( (Excl' (σ : leibnizC _))   (Excl' σ)))
    as (γσ) "[Hσ Hσf]"; first done.
  iModIntro. iExists (λ σ, own γσ ( (Excl' (σ:leibnizC _)))). iFrame "Hσ".
  iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
Qed.

Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ Φ :
  ( `{ownPG Λ Σ},
    ownP σ1 ={}= WP e {{ Φ }}  |={,}=>  σ', ownP σ'  ⌜φ σ') 
  rtc step ([e], σ1) (t2, σ2) 
  φ σ2.
Proof.
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _ Φ)=> //.
  iIntros (?) "". iMod (own_alloc ( (Excl' (σ1 : leibnizC _))   (Excl' σ1)))
    as (γσ) "[Hσ Hσf]"; first done.
  iExists (λ σ, own γσ ( (Excl' (σ:leibnizC _)))). iFrame "Hσ".
  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
  iDestruct (own_valid_2 with "Hσ Hσf")
    as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
Qed.


(** Lifting *)
Section lifting.
  Context `{ownPG Λ Σ}.
  Implicit Types e : expr Λ.
  Implicit Types Φ : val Λ  iProp Σ.

  Lemma ownP_twice σ1 σ2 : ownP σ1  ownP σ2  False.
  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
  Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
  Proof. rewrite /ownP; apply _. Qed.

  Lemma ownP_lift_step E Φ e1 :
    (|={E,}=>  σ1, reducible e1 σ1   ownP σ1 
        e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2
            ={,E}= WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
      move: Hred; by rewrite to_of_val.
    - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
      iMod "H" as (σ1') "(% & >Hσf & H)". rewrite /ownP.
      iDestruct (own_valid_2 with "Hσ Hσf")
        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
      iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
      { by apply auth_update, option_local_update,
          (exclusive_local_update _ (Excl σ2)). }
      iFrame "Hσ". iApply ("H" with "* []"); eauto.
  Qed.

  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
    ( σ1, reducible e1 σ1) 
    ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
    (  e2 efs σ, prim_step e1 σ e2 σ efs 
      WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
    { eapply reducible_not_val, (Hsafe inhabitant). }
    iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
    iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
    destruct (Hstep σ1 e2 σ2 efs); auto; subst.
    iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
  Qed.

  (** Derived lifting lemmas. *)
  Lemma ownP_lift_atomic_step {E Φ} e1 σ1 :
    reducible e1 σ1 
    ( ownP σ1    e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2 -
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (?) "[Hσ H]". iApply (ownP_lift_step E _ e1).
    iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver. iModIntro.
    iExists σ1. iFrame "Hσ"; iSplit; eauto.
    iNext; iIntros (e2 σ2 efs) "% Hσ".
    iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
    destruct (to_val e2) eqn:?; last by iExFalso.
    iMod "Hclose". iApply wp_value; auto using to_of_val. done.
  Qed.

  Lemma ownP_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
    reducible e1 σ1 
    ( e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' 
                     σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
     ownP σ1   (ownP σ2 -
      Φ v2  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (ownP_lift_atomic_step _ σ1); try done.
    iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
    edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
  Qed.

  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
    ( σ1, reducible e1 σ1) 
    ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
     (WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (? Hpuredet) "?". iApply (ownP_lift_pure_step E); try done.
    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
  Qed.
End lifting.

Section ectx_lifting.
  Import ectx_language.
  Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
  Context `{ownPG (ectx_lang expr) Σ} `{Inhabited state}.
  Implicit Types Φ : val  iProp Σ.
  Implicit Types e : expr.
  Hint Resolve head_prim_reducible head_reducible_prim_step.

  Lemma ownP_lift_head_step E Φ e1 :
    (|={E,}=>  σ1, head_reducible e1 σ1   ownP σ1 
        e2 σ2 efs, head_step e1 σ1 e2 σ2 efs - ownP σ2
            ={,E}= WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros "H". iApply (ownP_lift_step E); try done.
    iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
    iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
    iApply ("Hwp" with "* []"); by eauto.
  Qed.

  Lemma ownP_lift_pure_head_step E Φ e1 :
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
    (  e2 efs σ, head_step e1 σ e2 σ efs 
      WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
    iIntros (????). iApply "H". eauto.
  Qed.

  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
    head_reducible e1 σ1 
     ownP σ1   ( e2 σ2 efs,
    head_step e1 σ1 e2 σ2 efs - ownP σ2 -
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iFrame. iNext.
    iIntros (???) "% ?". iApply ("H" with "* []"); eauto.
  Qed.

  Lemma ownP_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
    head_reducible e1 σ1 
    ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
      σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
     ownP σ1   (ownP σ2 - Φ v2  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof. eauto using ownP_lift_atomic_det_step. Qed.

  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
    head_reducible e1 σ1 
    ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
      σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
    {{{  ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
  Proof.
    intros. rewrite -(ownP_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
  Qed.

  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs') 
     (WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof. eauto using wp_lift_pure_det_step. Qed.

  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
    to_val e1 = None 
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  [] = efs') 
     WP e2 @ E {{ Φ }}  WP e1 @ E {{ Φ }}.
  Proof.
    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
  Qed.
End ectx_lifting.