ownp.v 12.2 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

Definition ownPΣ (Λstate : Type) : gFunctors :=
  #[invΣ;
23
    GFunctor (authUR (optionUR (exclR (leibnizC Λstate))))].
24 25 26 27 28 29 30 31

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 Σ.
32
Proof. solve_inG. Qed.
33 34 35 36 37 38 39 40 41

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


(* Adequacy *)
42 43 44
Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
  ( `{ownPG Λ Σ}, ownP σ  WP e @ s;  {{ v, ⌜φ v }}) 
  adequate s e σ φ.
45 46 47 48 49 50 51 52
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.

53
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
54
  ( `{ownPG Λ Σ},
55
    ownP σ1 ={}= WP e @ s;  {{ _, True }}  |={,}=>  σ', ownP σ'  ⌜φ σ') 
56 57 58
  rtc step ([e], σ1) (t2, σ2) 
  φ σ2.
Proof.
59
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
60 61 62 63
  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.
64
  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite/ownP.
65 66 67 68 69 70 71 72
  iDestruct (own_valid_2 with "Hσ Hσf")
    as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
Qed.


(** Lifting *)
Section lifting.
  Context `{ownPG Λ Σ}.
73
  Implicit Types s : stuckness.
74 75 76
  Implicit Types e : expr Λ.
  Implicit Types Φ : val Λ  iProp Σ.

77 78 79 80 81 82
  Lemma ownP_eq σ1 σ2 : state_interp σ1 - ownP σ2 - ⌜σ1 = σ2.
  Proof.
    iIntros "Hσ1 Hσ2"; rewrite/ownP.
    by iDestruct (own_valid_2 with "Hσ1 Hσ2")
      as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
  Qed.
83 84
  Lemma ownP_twice σ1 σ2 : ownP σ1  ownP σ2  False.
  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
85
  Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
86 87
  Proof. rewrite /ownP; apply _. Qed.

88
  Lemma ownP_lift_step s E Φ e1 :
89
    (|={E,}=>  σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None   ownP σ1 
90
        e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2
91 92
            ={,E}= WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
93
  Proof.
94 95 96 97 98 99 100 101 102 103 104 105
    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.
      destruct s; last done. apply reducible_not_val in Hred.
      move: Hred; by rewrite to_of_val.
    - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
      iMod "H" as (σ1' ?) "[>Hσf H]". iDestruct (ownP_eq with "Hσ Hσf") as %->.
      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
      rewrite /ownP; 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.
106 107 108
  Qed.

  Lemma ownP_lift_stuck E Φ e :
109
    (|={E,}=>  σ, stuck e σ⌝   ownP σ)
110 111 112
     WP e @ E ?{{ Φ }}.
  Proof.
    iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
113 114 115 116
    - apply of_to_val in EQe as <-. iApply fupd_wp.
      iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
      by rewrite to_of_val in Hnv.
    - iApply wp_lift_stuck; [done|]. iIntros (σ1) "Hσ".
117 118 119 120
      iMod "H" as (σ1') "(% & >Hσf)".
      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
  Qed.

121 122
  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
    ( σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) 
123 124
    ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
    (  e2 efs σ, prim_step e1 σ e2 σ efs 
125 126
      WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
127
  Proof.
128 129 130
    iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
    { specialize (Hsafe inhabitant). destruct s; last done.
      by eapply reducible_not_val. }
131
    iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
132
    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
133
    destruct (Hstep σ1 e2 σ2 efs); auto; subst.
134
    by iMod "Hclose"; iModIntro; iFrame; iApply "H".
135 136 137
  Qed.

  (** Derived lifting lemmas. *)
138
  Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
139
    (if s is not_stuck then reducible e1 σ1 else to_val e1 = None) 
140
    ( ownP σ1    e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2 -
141 142
      default False (to_val e2) Φ  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
143
  Proof.
144
    iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
145 146
    iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
    iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
147 148 149
    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.
150
    by iMod "Hclose"; iApply wp_value; auto using to_of_val.
151 152
  Qed.

153
  Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
154
    (if s is not_stuck then reducible e1 σ1 else to_val e1 = None) 
155 156 157
    ( e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' 
                     σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
     ownP σ1   (ownP σ2 -
158 159 160
      Φ v2  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
  Proof.
161
    iIntros (? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; try done.
162 163 164 165 166
    iFrame; iNext; iIntros (e2' σ2' efs') "% Hσ2'".
    edestruct Hdet as (->&Hval&->). done. by rewrite Hval; iApply "Hσ2".
  Qed.

  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
167
    (if s is not_stuck then reducible e1 σ1 else to_val e1 = None) 
168 169 170
    ( e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' 
      σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
    {{{  ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
171
  Proof.
172 173
    intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
174 175
  Qed.

176 177
  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
    ( σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) 
178
    ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
179 180 181
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s; {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
  Proof.
182
    iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
183 184 185 186
    by apply Hpuredet. by iNext; iIntros (e' efs' σ (_&->&->)%Hpuredet).
  Qed.

  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
187
    ( σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) 
188 189
    ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  [] = efs') 
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
190
  Proof.
191
    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
192
  Qed.
193 194 195 196
End lifting.

Section ectx_lifting.
  Import ectx_language.
197
  Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
198
  Implicit Types s : stuckness.
199 200
  Implicit Types Φ : val Λ  iProp Σ.
  Implicit Types e : expr Λ.
201
  Hint Resolve head_prim_reducible head_reducible_prim_step.
202
  Hint Resolve (reducible_not_val _ inhabitant).
203
  Hint Resolve head_stuck_stuck.
204

205
  Lemma ownP_lift_head_step s E Φ e1 :
206 207
    (|={E,}=>  σ1, head_reducible e1 σ1   ownP σ1 
        e2 σ2 efs, head_step e1 σ1 e2 σ2 efs - ownP σ2
208 209
            ={,E}= WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
210
  Proof.
211 212 213 214
    iIntros "H". iApply ownP_lift_step.
    iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1. iSplit.
    { destruct s; try by eauto using reducible_not_val. }
    iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
215
    iApply ("Hwp" with "[]"); eauto.
216 217
  Qed.

218
  Lemma ownP_lift_head_stuck E Φ e :
219 220
    sub_redexes_are_values e 
    (|={E,}=>  σ, head_stuck e σ⌝   ownP σ)
221 222
     WP e @ E ?{{ Φ }}.
  Proof.
223 224
    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
    iExists σ. by auto.
225 226 227
  Qed.

  Lemma ownP_lift_pure_head_step s E Φ e1 :
228 229 230
    ( σ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 
231 232
      WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
233
  Proof using Hinh.
234
    iIntros (??) "H".  iApply ownP_lift_pure_step; eauto.
235 236
    { by destruct s; auto. }
    iNext. iIntros (????). iApply "H"; eauto.
237 238
  Qed.

239
  Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 :
240 241 242
    head_reducible e1 σ1 
     ownP σ1   ( e2 σ2 efs,
    head_step e1 σ1 e2 σ2 efs - ownP σ2 -
243 244
      default False (to_val e2) Φ  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
245
  Proof.
246 247
    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto.
    { by destruct s; eauto using reducible_not_val. }
248
    iFrame. iNext. iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
249 250
  Qed.

251
  Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 v2 σ2 efs :
252 253 254
    head_reducible e1 σ1 
    ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
      σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
255 256 257
     ownP σ1   (ownP σ2 - Φ v2  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
  Proof.
258
    by destruct s; eauto 10 using ownP_lift_atomic_det_step, reducible_not_val.
259
  Qed.
260

261
  Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 v2 σ2 :
262 263 264
    head_reducible e1 σ1 
    ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
      σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
265
    {{{  ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
266
  Proof.
267
    intros ???; apply ownP_lift_atomic_det_step_no_fork; eauto.
268
    by destruct s; eauto using reducible_not_val.
269
  Qed.
270

271
  Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
272 273
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs') 
274 275
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
276
  Proof using Hinh.
277 278
    iIntros (??) "H"; iApply wp_lift_pure_det_step; eauto.
    by destruct s; eauto using reducible_not_val.
279
  Qed.
280

281
  Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
282 283
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  [] = efs') 
284
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
285
  Proof using Hinh.
286 287
    iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
    by destruct s; eauto using reducible_not_val.
288
  Qed.
289
End ectx_lifting.