ownp.v 12.1 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
    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid.
94
    by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
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 212 213
  Hint Resolve head_prim_reducible head_reducible_prim_step : core.
  Hint Resolve (reducible_not_val _ inhabitant) : core.
  Hint Resolve head_stuck_stuck : core.
214

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

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

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

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

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

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

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