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

8
Class ownPG' (Λstate Λobservation : Type) (Σ : gFunctors) := OwnPG {
9
  ownP_invG : invG Σ;
10 11
  ownP_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
  ownP_name : gname;
12
}.
13
Notation ownPG Λ Σ := (ownPG' (state Λ) (observation Λ) Σ).
14

15
Instance ownPG_irisG `{ownPG' Λstate Λobservation Σ} : irisG' Λstate Λobservation Σ := {
16
  iris_invG := ownP_invG;
17
  state_interp σ κs := (own ownP_name ( (Excl' (σ:leibnizC Λstate))))%I
18
}.
19
Global Opaque iris_invG.
20

21
Definition ownPΣ (Λstate : Type) : gFunctors :=
22
  #[invΣ;
23
    GFunctor (authR (optionUR (exclR (leibnizC Λstate))))].
24

25
Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
26
  ownPPre_invG :> invPreG Σ;
27
  ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
28
}.
29
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
30

31
Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ  ownPPreG' Λstate Σ.
32
Proof. solve_inG. Qed.
33 34

(** Ownership *)
35 36
Definition ownP `{ownPG' Λstate Λobservation Σ} (σ : Λstate) : iProp Σ :=
  own ownP_name ( (Excl' (σ:leibnizC Λstate))).
37

38 39
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3.
40 41

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

56
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
57 58 59
  ( `{ownPG Λ Σ},
      ownP σ1 ={}= WP e @ s;  {{ _, True }} 
      |={,}=>  σ', ownP σ'  ⌜φ σ') 
60
  rtc erased_step ([e], σ1) (t2, σ2) 
61 62
  φ σ2.
Proof.
63
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
64
  iIntros (? κs κs').
65
  iMod (own_alloc ( (Excl' (σ1 : leibnizC _))   (Excl' σ1)))
66
    as (γσ) "[Hσ Hσf]"; first done.
67
  iExists (λ σ κs',
68 69 70 71 72
           own γσ ( (Excl' (σ:leibnizC _))))%I.
  iFrame "Hσ".
  iMod (Hwp (OwnPG _ _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
    first by rewrite /ownP; iFrame.
  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite/ownP.
73 74
  iDestruct (own_valid_2 with "Hσ Hσf") as %[Hp _]%auth_valid_discrete_2.
  pose proof (Excl_included _ _ Hp) as Hp'. apply leibniz_equiv in Hp'. inversion Hp'; subst. auto.
75 76 77 78 79 80
Qed.


(** Lifting *)
Section lifting.
  Context `{ownPG Λ Σ}.
81
  Implicit Types s : stuckness.
82 83 84
  Implicit Types e : expr Λ.
  Implicit Types Φ : val Λ  iProp Σ.

85
  Lemma ownP_eq σ1 σ2 κs : state_interp σ1 κs - ownP σ2 - ⌜σ1 = σ2.
86
  Proof.
87
    iIntros "Hσ● Hσ◯". rewrite /ownP.
88 89 90 91
    iDestruct (own_valid_2 with "Hσ● Hσ◯")
      as %[Hps _]%auth_valid_discrete_2.
    pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
    done.
92
  Qed.
93 94 95 96
  Lemma ownP_state_twice σ1 σ2 : ownP σ1  ownP σ2  False.
  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
  Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) (observation Λ) Σ _ σ).
  Proof. rewrite /ownP; apply _. Qed.
97

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

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

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

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

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

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

194
  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
Ralf Jung's avatar
Ralf Jung committed
195
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
196
    ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = []  σ1 = σ2  e2 = e2'  efs = efs')
197 198
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s; {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
199
  Proof.
200
    iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
201
    naive_solver. by iNext; iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
202 203 204
  Qed.

  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
Ralf Jung's avatar
Ralf Jung committed
205
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
206
    ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = []  σ1 = σ2  e2 = e2'  [] = efs') 
207
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
208
  Proof.
209
    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
210 211 212 213 214
  Qed.
End lifting.

Section ectx_lifting.
  Import ectx_language.
215
  Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
216
  Implicit Types s : stuckness.
217 218
  Implicit Types Φ : val Λ  iProp Σ.
  Implicit Types e : expr Λ.
219
  Hint Resolve head_prim_reducible head_reducible_prim_step.
220
  Hint Resolve (reducible_not_val _ inhabitant).
221
  Hint Resolve head_stuck_stuck.
222

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

237
  Lemma ownP_lift_head_stuck E Φ e :
238
    sub_redexes_are_values e 
239
    (|={E,}=>  σ, head_stuck e σ⌝   (ownP σ))
240 241
     WP e @ E ?{{ Φ }}.
  Proof.
242 243
    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
    iExists σ. iModIntro. by auto with iFrame.
244 245 246
  Qed.

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

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

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

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

294
  Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
295
    ( σ1, head_reducible e1 σ1) 
296
    ( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs'  κ = []  σ1 = σ2  e2 = e2'  efs = efs') 
297 298
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
299
  Proof using Hinh.
300 301
    iIntros (??) "H"; iApply wp_lift_pure_det_step; eauto.
    by destruct s; eauto using reducible_not_val.
Ralf Jung's avatar
Ralf Jung committed
302
  Qed.
303

304
  Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
305
    ( σ1, head_reducible e1 σ1) 
306
    ( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs'  κ = []  σ1 = σ2  e2 = e2'  [] = efs') 
307
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
308
  Proof using Hinh.
309 310
    iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
    by destruct s; eauto using reducible_not_val.
311 312
  Qed.
End ectx_lifting.