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

Robbert Krebbers's avatar
Robbert Krebbers committed
8
Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
9
  ownP_invG : invG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  ownP_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
11
  ownP_name : gname;
12 13
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
14
Instance ownPG_irisG `{ownPG Λ Σ} : irisG Λ Σ := {
15
  iris_invG := ownP_invG;
Robbert Krebbers's avatar
Robbert Krebbers committed
16
  state_interp σ κs _ := own ownP_name ( (Excl' σ))%I;
17
  fork_post _ := True%I;
18
}.
19
Global Opaque iris_invG.
20

Robbert Krebbers's avatar
Robbert Krebbers committed
21
Definition ownPΣ (Λ : language) : gFunctors :=
22
  #[invΣ;
Robbert Krebbers's avatar
Robbert Krebbers committed
23
    GFunctor (authR (optionUR (exclR (stateC Λ))))].
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
26
  ownPPre_invG :> invPreG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))))
28 29
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
30
Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ  ownPPreG Λ Σ.
31
Proof. solve_inG. Qed.
32 33

(** Ownership *)
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
Definition ownP `{ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
  own ownP_name ( (Excl' σ)).
36

37
Typeclasses Opaque ownP.
38
Instance: Params (@ownP) 3 := {}.
39 40

(* Adequacy *)
41
Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
42
  ( `{ownPG Λ Σ}, ownP σ  WP e @ s;  {{ v, ⌜φ v }}) 
43
  adequate s e σ (λ v _, φ v).
44 45
Proof.
  intros Hwp. apply (wp_adequacy Σ _).
46
  iIntros (? κs).
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48
  iMod (own_alloc ( (Excl' σ)   (Excl' σ))) as (γσ) "[Hσ Hσf]"; first done.
  iModIntro. iExists (λ σ κs, own γσ ( (Excl' σ)))%I.
49
  iFrame "Hσ".
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
51 52
Qed.

53
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
54 55 56
  ( `{ownPG Λ Σ},
      ownP σ1 ={}= WP e @ s;  {{ _, True }} 
      |={,}=>  σ', ownP σ'  ⌜φ σ') 
57
  rtc erased_step ([e], σ1) (t2, σ2) 
58 59
  φ σ2.
Proof.
60
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
61
  iIntros (? κs κs').
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  iMod (own_alloc ( (Excl' σ1)   (Excl' σ1))) as (γσ) "[Hσ Hσf]"; first done.
63
  iExists (λ σ κs' _, own γσ ( (Excl' σ)))%I, (λ _, True%I).
64
  iFrame "Hσ".
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
66
    first by rewrite /ownP; iFrame.
67 68 69
  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.
70 71 72 73 74 75
Qed.


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

80
  Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n - ownP σ2 - ⌜σ1 = σ2.
81
  Proof.
82
    iIntros "Hσ● Hσ◯". rewrite /ownP.
83 84
    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_valid_discrete_2.
    by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
85
  Qed.
86 87
  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
88
  Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
89
  Proof. rewrite /ownP; apply _. Qed.
90

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

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

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

  (** Derived lifting lemmas. *)
145
  Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
Ralf Jung's avatar
Ralf Jung committed
146
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
147 148 149
    ( (ownP σ1) 
         κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs -
         ownP σ2 -
Ralf Jung's avatar
Ralf Jung committed
150
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
151
     WP e1 @ s; E {{ Φ }}.
152
  Proof.
153
    iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
154
    iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
155 156 157
    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..|].
158
    destruct (to_val e2) eqn:?; last by iExFalso.
159
    iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
160 161
  Qed.

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

176
  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
Ralf Jung's avatar
Ralf Jung committed
177
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
178
    ( κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' 
179
      σ2' = σ2  to_val e2' = Some v2  efs' = []) 
180
    {{{  (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
181
  Proof.
182
    intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
183
    rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
184
    iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
185 186
  Qed.

187
  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
Ralf Jung's avatar
Ralf Jung committed
188
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
189
    ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = []  σ2 = σ1  e2' = e2  efs' = []) 
190
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
191
  Proof.
192
    intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //; eauto.
193 194 195 196 197
  Qed.
End lifting.

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

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

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

  Lemma ownP_lift_pure_head_step s E Φ e1 :
230
    ( σ1, head_reducible e1 σ1) 
231
    ( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs  κ = []  σ2 = σ1) 
232
    (  κ e2 efs σ, head_step e1 σ κ e2 σ efs 
233 234
      WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
235
  Proof using Hinh.
236
    iIntros (??) "H".  iApply ownP_lift_pure_step; eauto.
237
    { by destruct s; auto. }
238
    iNext. iIntros (?????). iApply "H"; eauto.
239 240
  Qed.

241
  Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 :
242
    head_reducible e1 σ1 
243 244
     (ownP σ1)   ( κ e2 σ2 efs,
    head_step e1 σ1 κ e2 σ2 efs - ownP σ2 -
Ralf Jung's avatar
Ralf Jung committed
245
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
246
     WP e1 @ s; E {{ Φ }}.
247
  Proof.
248
    iIntros (?) "[Hst H]". iApply ownP_lift_atomic_step; eauto.
249
    { by destruct s; eauto using reducible_not_val. }
250
    iSplitL "Hst"; first done.
251
    iNext. iIntros (???? ?) "Hσ". iApply ("H" with "[] Hσ"); eauto.
252 253
  Qed.

254
  Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 v2 σ2 efs :
255
    head_reducible e1 σ1 
256
    ( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' 
257
      σ2' = σ2  to_val e2' = Some v2  efs' = efs) 
258 259
     (ownP σ1)   (ownP σ2 -
                      Φ v2  [ list] ef  efs, WP ef @ s;  {{ _, True }})
260 261
     WP e1 @ s; E {{ Φ }}.
  Proof.
262 263 264
    intros Hr Hs.
    destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val;
    intros; eapply Hs; eauto 10.
265
  Qed.
266

267
  Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 κ v2 σ2 :
268
    head_reducible e1 σ1 
269
    ( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' 
270
      κ' = κ  σ2' = σ2  to_val e2' = Some v2  efs' = []) 
271
    {{{  (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
272
  Proof.
273
    intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
274
    by destruct s; eauto using reducible_not_val.
275 276
  Qed.

277
  Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
278
    ( σ1, head_reducible e1 σ1) 
279
    ( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs'  κ = []  σ2 = σ1  e2' = e2  efs' = []) 
280
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
281
  Proof using Hinh.
282
    iIntros (??) "H"; iApply wp_lift_pure_det_step_no_fork; try by eauto.
283
    by destruct s; eauto using reducible_not_val.
284 285
  Qed.
End ectx_lifting.