ownp.v 12.3 KB
Newer Older
1
2
From iris.proofmode Require Import tactics classes.
From iris.algebra Require Import 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 Σ (authR (optionUR (exclR (stateO Λ))));
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Σ;
32
    GFunctor (authR (optionUR (exclR (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 Σ (authR (optionUR (exclR (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 Σ :=
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
  iMod (own_alloc ( (Excl' σ)   (Excl' σ))) as (γσ) "[Hσ Hσf]";
57
    first by apply auth_both_valid.
58
  iModIntro. iExists (λ σ κs, own γσ ( (Excl' σ)))%I, (λ _, True%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).
72
  iMod (own_alloc ( (Excl' σ1)   (Excl' σ1))) as (γσ) "[Hσ Hσf]";
73
    first by apply auth_both_valid.
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
  iIntros "!> Hσ". iExists . iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
79
  iDestruct (own_valid_2 with "Hσ Hσf")
80
    as %[Hp%Excl_included _]%auth_both_valid; 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
    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid.
95
    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]".
121
122
      { apply auth_update. apply option_local_update.
         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.