ownp.v 12.3 KB
Newer Older
1 2 3
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
4
From iris.algebra Require Import excl auth.
5
From iris.proofmode Require Import tactics classes.
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 Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  ownP_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
20
  ownP_name : gname;
21 22
}.

23
Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
24
  iris_invG := ownP_invG;
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  state_interp σ κs _ := own ownP_name ( (Excl' σ))%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Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
32
    GFunctor (authR (optionUR (exclR (stateC Λ))))].
33

Robbert Krebbers's avatar
Robbert Krebbers committed
34
Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
35
  ownPPre_invG :> invPreG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))))
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 Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  own ownP_name ( (Excl' σ)).
45

46
Typeclasses Opaque ownP.
47
Instance: Params (@ownP) 3 := {}.
48 49

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

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


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

91
  Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n - ownP σ2 - ⌜σ1 = σ2.
92
  Proof.
93
    iIntros "Hσ● Hσ◯". rewrite /ownP.
94 95
    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_valid_discrete_2.
    by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
96
  Qed.
97 98
  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
99
  Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
100
  Proof. rewrite /ownP; apply _. Qed.
101

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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