ownp.v 12.2 KB
Newer Older
1
From iris.proofmode Require Import tactics classes.
2
From iris.algebra Require Import lib.excl_auth.
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.
6
Set Default Proof Using "Type".
7

Ralf Jung's avatar
Ralf Jung committed
8 9 10 11 12 13 14 15 16
(**
This module provides an interface to handling ownership of the global state that
works more like Iris 2.0 did.  The state interpretation (in WP) is fixed to be
authoritative ownership of the entire state (using the [excl] RA).  Users can
then put the corresponding fragment into an invariant on their own to establish
a more interesting notion of ownership, such as the standard heap with disjoint
union.
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
17
Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
18
  ownP_invG : invG Σ;
19
  ownP_inG :> inG Σ (excl_authR (stateO Λ));
20
  ownP_name : gname;
21 22
}.

23
Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
24
  iris_invG := ownP_invG;
25
  state_interp σ κs _ := own ownP_name (E σ)%I;
26
  fork_post _ := True%I;
27
}.
28
Global Opaque iris_invG.
29

Robbert Krebbers's avatar
Robbert Krebbers committed
30
Definition ownPΣ (Λ : language) : gFunctors :=
31
  #[invΣ;
32
    GFunctor (excl_authR (stateO Λ))].
33

Robbert Krebbers's avatar
Robbert Krebbers committed
34
Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
35
  ownPPre_invG :> invPreG Σ;
36
  ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
37 38
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
39
Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ  ownPPreG Λ Σ.
40
Proof. solve_inG. Qed.
41 42

(** Ownership *)
43
Definition ownP `{!ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
44
  own ownP_name (E σ).
45
Typeclasses Opaque ownP.
46
Instance: Params (@ownP) 3 := {}.
47 48

(* Adequacy *)
49 50
Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
  ( `{!ownPG Λ Σ}, ownP σ  WP e @ s;  {{ v, ⌜φ v }}) 
51
  adequate s e σ (λ v _, φ v).
52 53
Proof.
  intros Hwp. apply (wp_adequacy Σ _).
54
  iIntros (? κs).
55 56 57
  iMod (own_alloc (E σ  E σ)) as (γσ) "[Hσ Hσf]";
    first by apply excl_auth_valid.
  iModIntro. iExists (λ σ κs, own γσ (E σ))%I, (λ _, True%I).
58
  iFrame "Hσ".
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
60 61
Qed.

62 63
Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
  ( `{!ownPG Λ Σ},
64 65
      ownP σ1 ={}= WP e @ s;  {{ _, True }} 
      |={,}=>  σ', ownP σ'  ⌜φ σ') 
66
  rtc erased_step ([e], σ1) (t2, σ2) 
67 68
  φ σ2.
Proof.
69
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
70
  iIntros (? κs).
71
  iMod (own_alloc (E σ1  E σ1)) as (γσ) "[Hσ Hσf]";
72
    first by apply auth_both_valid.
73
  iExists (λ σ κs' _, own γσ (E σ))%I, (λ _, True%I).
74
  iFrame "Hσ".
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
76
    first by rewrite /ownP; iFrame.
77
  iIntros "!> Hσ". iExists . iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
78
  iDestruct (own_valid_2 with "Hσ Hσf")
79
    as %[Hp%Excl_included _]%auth_both_valid; simplify_eq; auto.
80 81 82 83 84
Qed.


(** Lifting *)
Section lifting.
85
  Context `{!ownPG Λ Σ}.
86
  Implicit Types s : stuckness.
87 88 89
  Implicit Types e : expr Λ.
  Implicit Types Φ : val Λ  iProp Σ.

90
  Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n - ownP σ2 - ⌜σ1 = σ2.
91
  Proof.
92
    iIntros "Hσ● Hσ◯". rewrite /ownP.
93 94
    by iDestruct (own_valid_2 with "Hσ● Hσ◯")
      as %[->%Excl_included _]%auth_both_valid.
95
  Qed.
96 97
  Lemma ownP_state_twice σ1 σ2 : ownP σ1  ownP σ2  False.
  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
99
  Proof. rewrite /ownP; apply _. Qed.
100

101
  Lemma ownP_lift_step s E Φ e1 :
102 103 104 105
    (|={E,}=>  σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None 
       ownP σ1 
        κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs -
      ownP σ2
106 107
            ={,E}= WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
108 109 110
  Proof.
    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
111
      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred.
112
      destruct s; last done. apply reducible_not_val in Hred.
113
      move: Hred; by rewrite to_of_val.
114
    - iApply wp_lift_step; [done|]; iIntros (σ1 κ κs n) "Hσκs".
115 116
      iMod "H" as (σ1' ?) "[>Hσf H]".
      iDestruct (ownP_eq with "Hσκs Hσf") as %<-.
117
      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
118
      iDestruct "Hσκs" as "Hσ". rewrite /ownP.
119
      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
120
      { apply excl_auth_update. }
121
      iFrame "Hσ". iApply ("H" with "[]"); eauto with iFrame.
122 123
  Qed.

124
  Lemma ownP_lift_stuck E Φ e :
125
    (|={E,}=>  σ, stuck e σ⌝   (ownP σ))
126 127 128
     WP e @ E ?{{ Φ }}.
  Proof.
    iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
129
    - apply of_to_val in EQe as <-. iApply fupd_wp.
130
      iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
131
      by rewrite to_of_val in Hnv.
132
    - iApply wp_lift_stuck; [done|]. iIntros (σ1 κs n) "Hσ".
133 134
      iMod "H" as (σ1') "(% & >Hσf)".
      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
135 136
  Qed.

137
  Lemma ownP_lift_pure_step `{!Inhabited (state Λ)} s E Φ e1 :
Ralf Jung's avatar
Ralf Jung committed
138
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
139
    ( σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs  κ = []  σ2 = σ1) 
140
    (  κ e2 efs σ, prim_step e1 σ κ e2 σ efs 
141 142
      WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
143
  Proof.
144 145 146
    iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
    { specialize (Hsafe inhabitant). destruct s; last done.
      by eapply reducible_not_val. }
147
    iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
148
    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
149
    destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
150
    by iMod "Hclose"; iModIntro; iFrame; iApply "H".
151 152 153
  Qed.

  (** Derived lifting lemmas. *)
154
  Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
Ralf Jung's avatar
Ralf Jung committed
155
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
156 157 158
    ( (ownP σ1) 
         κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs -
         ownP σ2 -
Ralf Jung's avatar
Ralf Jung committed
159
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
160
     WP e1 @ s; E {{ Φ }}.
161
  Proof.
162
    iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
163
    iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
164 165 166
    iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
    iNext; iIntros (κ e2 σ2 efs ?) "Hσ".
    iDestruct ("H" $! κ e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
167
    destruct (to_val e2) eqn:?; last by iExFalso.
168
    iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
169 170
  Qed.

171
  Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
Ralf Jung's avatar
Ralf Jung committed
172
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
173
    ( κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' 
174
                     σ2' = σ2  to_val e2' = Some v2  efs' = efs) 
175
     (ownP σ1)   (ownP σ2 -
176 177 178
      Φ v2  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
  Proof.
179 180
    iIntros (? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; try done.
    iFrame; iNext; iIntros (κ' e2' σ2' efs' ?) "Hσ2'".
181
    edestruct (Hdet κ') as (<-&Hval&<-); first done. rewrite Hval.
182
    iApply ("Hσ2" with "Hσ2'").
183 184
  Qed.

185
  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
Ralf Jung's avatar
Ralf Jung committed
186
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
187
    ( κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' 
188
      σ2' = σ2  to_val e2' = Some v2  efs' = []) 
189
    {{{  (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
190
  Proof.
191
    intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
192
    rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
193
    iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
194 195
  Qed.

196
  Lemma ownP_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E Φ} e1 e2 :
Ralf Jung's avatar
Ralf Jung committed
197
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
198
    ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = []  σ2 = σ1  e2' = e2  efs' = []) 
199
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
200
  Proof.
201
    intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //; eauto.
202 203 204 205 206
  Qed.
End lifting.

Section ectx_lifting.
  Import ectx_language.
207
  Context {Λ : ectxLanguage} `{!ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
208
  Implicit Types s : stuckness.
209 210
  Implicit Types Φ : val Λ  iProp Σ.
  Implicit Types e : expr Λ.
Tej Chajed's avatar
Tej Chajed committed
211
  Hint Resolve head_prim_reducible head_reducible_prim_step : core.
212 213
  Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
  Hint Resolve reducible_not_val_inhabitant : core.
Tej Chajed's avatar
Tej Chajed committed
214
  Hint Resolve head_stuck_stuck : core.
215

216
  Lemma ownP_lift_head_step s E Φ e1 :
217 218 219
    (|={E,}=>  σ1, head_reducible e1 σ1   (ownP σ1) 
              κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs -
            ownP σ2
220 221
            ={,E}= WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
222
  Proof.
223
    iIntros "H". iApply ownP_lift_step.
224
    iMod "H" as (σ1 ?) "[>Hσ1 Hwp]". iModIntro. iExists σ1. iSplit.
225
    { destruct s; try by eauto using reducible_not_val. }
226
    iFrame. iNext. iIntros (κ e2 σ2 efs ?) "Hσ2".
227
    iApply ("Hwp" with "[] Hσ2"); eauto.
228 229
  Qed.

230
  Lemma ownP_lift_head_stuck E Φ e :
231
    sub_redexes_are_values e 
232
    (|={E,}=>  σ, head_stuck e σ⌝   (ownP σ))
233 234
     WP e @ E ?{{ Φ }}.
  Proof.
235 236
    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
    iExists σ. iModIntro. by auto with iFrame.
237 238 239
  Qed.

  Lemma ownP_lift_pure_head_step s E Φ e1 :
240
    ( σ1, head_reducible e1 σ1) 
241
    ( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs  κ = []  σ2 = σ1) 
242
    (  κ e2 efs σ, head_step e1 σ κ e2 σ efs 
243 244
      WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
245
  Proof using Hinh.
246
    iIntros (??) "H".  iApply ownP_lift_pure_step; eauto.
247
    { by destruct s; auto. }
248
    iNext. iIntros (?????). iApply "H"; eauto.
249 250
  Qed.

251
  Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 :
252
    head_reducible e1 σ1 
253 254
     (ownP σ1)   ( κ e2 σ2 efs,
    head_step e1 σ1 κ e2 σ2 efs - ownP σ2 -
Ralf Jung's avatar
Ralf Jung committed
255
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
256
     WP e1 @ s; E {{ Φ }}.
257
  Proof.
258
    iIntros (?) "[Hst H]". iApply ownP_lift_atomic_step; eauto.
259
    { by destruct s; eauto using reducible_not_val. }
260
    iSplitL "Hst"; first done.
261
    iNext. iIntros (???? ?) "Hσ". iApply ("H" with "[] Hσ"); eauto.
262 263
  Qed.

264
  Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 v2 σ2 efs :
265
    head_reducible e1 σ1 
266
    ( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' 
267
      σ2' = σ2  to_val e2' = Some v2  efs' = efs) 
268 269
     (ownP σ1)   (ownP σ2 -
                      Φ v2  [ list] ef  efs, WP ef @ s;  {{ _, True }})
270 271
     WP e1 @ s; E {{ Φ }}.
  Proof.
272 273 274
    intros Hr Hs.
    destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val;
    intros; eapply Hs; eauto 10.
275
  Qed.
276

277
  Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 κ v2 σ2 :
278
    head_reducible e1 σ1 
279
    ( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' 
280
      κ' = κ  σ2' = σ2  to_val e2' = Some v2  efs' = []) 
281
    {{{  (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
282
  Proof.
283
    intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
284
    by destruct s; eauto using reducible_not_val.
285 286
  Qed.

287
  Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
288
    ( σ1, head_reducible e1 σ1) 
289
    ( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs'  κ = []  σ2 = σ1  e2' = e2  efs' = []) 
290
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
291
  Proof using Hinh.
292
    iIntros (??) "H"; iApply wp_lift_pure_det_step_no_fork; try by eauto.
293
    by destruct s; eauto using reducible_not_val.
294 295
  Qed.
End ectx_lifting.