ownp.v 16.1 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 12 13
  ownP_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
  ownP_obs_inG :> inG Σ (authR (optionUR (exclR (leibnizC (list Λobservation)))));
  ownP_state_name : gname;
  ownP_obs_name : gname
14
}.
15
Notation ownPG Λ Σ := (ownPG' (state Λ) (observation Λ) Σ).
16

17
Instance ownPG_irisG `{ownPG' Λstate Λobservation Σ} : irisG' Λstate Λobservation Σ := {
18
  iris_invG := ownP_invG;
19 20
  state_interp σ κs := (own ownP_state_name ( (Excl' (σ:leibnizC Λstate))) 
                       own ownP_obs_name ( (Excl' (κs:leibnizC (list Λobservation)))))%I
21
}.
22
Global Opaque iris_invG.
23

24
Definition ownPΣ (Λstate Λobservation : Type) : gFunctors :=
25
  #[invΣ;
26 27
    GFunctor (authR (optionUR (exclR (leibnizC Λstate))));
    GFunctor (authR (optionUR (exclR (leibnizC (list Λobservation)))))].
28

29
Class ownPPreG' (Λstate Λobservation : Type) (Σ : gFunctors) : Set := IrisPreG {
30
  ownPPre_invG :> invPreG Σ;
31 32
  ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
  ownPPre_obs_inG :> inG Σ (authR (optionUR (exclR (leibnizC (list Λobservation)))))
33
}.
34
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) (observation Λ) Σ).
35

36
Instance subG_ownPΣ {Λstate Λobservation Σ} : subG (ownPΣ Λstate Λobservation) Σ  ownPPreG' Λstate Λobservation Σ.
37
Proof. solve_inG. Qed.
38 39

(** Ownership *)
40 41
Definition ownP_state `{ownPG' Λstate Λobservation Σ} (σ : Λstate) : iProp Σ :=
  own ownP_state_name ( (Excl' (σ:leibnizC Λstate))).
42

43 44 45 46 47 48
Definition ownP_obs `{ownPG' Λstate Λobservation Σ} (κs: list Λobservation) : iProp Σ :=
  own ownP_obs_name ( (Excl' (κs:leibnizC (list Λobservation)))).

Typeclasses Opaque ownP_state ownP_obs.
Instance: Params (@ownP_state) 3.
Instance: Params (@ownP_obs) 3.
49 50

(* Adequacy *)
51
Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
52
  ( `{ownPG Λ Σ} κs, ownP_state σ  ownP_obs κs  WP e @ s;  {{ v, ⌜φ v }}) 
53
  adequate s e σ (λ v _, φ v).
54 55
Proof.
  intros Hwp. apply (wp_adequacy Σ _).
56 57
  iIntros (? κs).
  iMod (own_alloc ( (Excl' (σ : leibnizC _))   (Excl' σ)))
58
    as (γσ) "[Hσ Hσf]"; first done.
59 60 61 62 63 64
  iMod (own_alloc ( (Excl' (κs : leibnizC _))   (Excl' κs)))
    as (γκs) "[Hκs Hκsf]"; first done.
  iModIntro. iExists (λ σ κs,
                      own γσ ( (Excl' (σ:leibnizC _)))  own γκs ( (Excl' (κs:leibnizC _))))%I.
  iFrame "Hσ Hκs".
  iApply (Hwp (OwnPG _ _ _ _ _ _ γσ γκs)). rewrite /ownP_state /ownP_obs. iFrame.
65 66
Qed.

67
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
68
  ( `{ownPG Λ Σ} κs,
69 70
      ownP_state σ1  ownP_obs κs ={}= WP e @ s;  {{ _, True }} 
      |={,}=>  σ' κs', ownP_state σ'  ownP_obs κs'  ⌜φ σ') 
71
  rtc erased_step ([e], σ1) (t2, σ2) 
72 73
  φ σ2.
Proof.
74
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
75
  iIntros (? κs κs').
76
  iMod (own_alloc ( (Excl' (σ1 : leibnizC _))   (Excl' σ1)))
77
    as (γσ) "[Hσ Hσf]"; first done.
78 79 80 81 82 83 84 85
  iMod (own_alloc ( (Excl' (κs ++ κs' : leibnizC _))   (Excl' (κs ++ κs'))))
    as (γκs) "[Hκs Hκsf]"; first done.
  iExists (λ σ κs',
           own γσ ( (Excl' (σ:leibnizC _)))  own γκs ( (Excl' (κs':leibnizC _))))%I.
  iFrame "Hσ Hκs".
  iMod (Hwp (OwnPG _ _ _ _ _ _ γσ γκs) with "[Hσf Hκsf]") as "[$ H]";
    first by rewrite /ownP_state /ownP_obs; iFrame.
  iIntros "!> [Hσ Hκs]". iMod "H" as (σ2' κs'') "[Hσf [Hκsf %]]". rewrite/ownP_state /ownP_obs.
86 87
  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.
88 89 90 91 92 93
Qed.


(** Lifting *)
Section lifting.
  Context `{ownPG Λ Σ}.
94
  Implicit Types s : stuckness.
95 96 97
  Implicit Types e : expr Λ.
  Implicit Types Φ : val Λ  iProp Σ.

98
  Lemma ownP_eq σ1 σ2 κs1 κs2 : state_interp σ1 κs1 - ownP_state σ2 - ownP_obs κs2 - ⌜σ1 = σ2  κs1 = κs2.
99
  Proof.
100 101 102 103 104 105 106 107
    iIntros "[Hσ● Hκs●] Hσ◯ Hκs◯". rewrite /ownP_state /ownP_obs.
    iDestruct (own_valid_2 with "Hσ● Hσ◯")
      as %[Hps _]%auth_valid_discrete_2.
    iDestruct (own_valid_2 with "Hκs● Hκs◯")
      as %[Hpo _]%auth_valid_discrete_2.
    pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
    pose proof (leibniz_equiv _ _ (Excl_included _ _ Hpo)) as ->.
    done.
108
  Qed.
109 110 111 112 113 114 115 116
  Lemma ownP_state_twice σ1 σ2 : ownP_state σ1  ownP_state σ2  False.
  Proof. rewrite /ownP_state -own_op own_valid. by iIntros (?). Qed.
  Lemma ownP_obs_twice κs1 κs2 : ownP_obs κs1  ownP_obs κs2  False.
  Proof. rewrite /ownP_obs -own_op own_valid. by iIntros (?). Qed.
  Global Instance ownP_state_timeless σ : Timeless (@ownP_state (state Λ) (observation Λ) Σ _ σ).
  Proof. rewrite /ownP_state; apply _. Qed.
  Global Instance ownP_obs_timeless κs : Timeless (@ownP_obs (state Λ) (observation Λ) Σ _ κs).
  Proof. rewrite /ownP_obs; apply _. Qed.
117

118
  Lemma ownP_lift_step s E Φ e1 :
119 120 121 122
    (|={E,}=>  σ1 κs, if s is NotStuck then reducible e1 σ1 else to_val e1 = None 
       ownP_state σ1   ownP_obs κs 
        κ κs' e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs  κs = cons_obs κ κs' -
      ownP_state σ2  ownP_obs κs'
123 124
            ={,E}= WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
125 126 127
  Proof.
    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
128
      iMod "H" as (σ1 κs) "[Hred _]"; iDestruct "Hred" as %Hred.
129
      destruct s; last done. apply reducible_not_val in Hred.
130
      move: Hred; by rewrite to_of_val.
131 132
    - iApply wp_lift_step; [done|]; iIntros (σ1 κs) "Hσκs".
      iMod "H" as (σ1' κs' ?) "[>Hσf [>Hκsf H]]". iDestruct (ownP_eq with "Hσκs Hσf Hκsf") as %[-> ->].
133
      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ κs'' e2 σ2 efs [Hstep ->]).
134 135 136
      iDestruct "Hσκs" as "[Hσ Hκs]".
      rewrite /ownP_state /ownP_obs.
      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
Ralf Jung's avatar
Ralf Jung committed
137 138
      { apply auth_update. apply: option_local_update.
        by apply: (exclusive_local_update _ (Excl σ2)). }
139 140 141 142
      iMod (own_update_2 with "Hκs Hκsf") as "[Hκs Hκsf]".
      { apply auth_update. apply: option_local_update.
        by apply: (exclusive_local_update _ (Excl (κs'':leibnizC _))). }
      iFrame "Hσ Hκs". iApply ("H" with "[]"); eauto with iFrame.
143 144
  Qed.

145
  Lemma ownP_lift_stuck E Φ e :
146
    (|={E,}=>  σ κs, stuck e σ⌝   (ownP_state σ  ownP_obs κs))
147 148 149
     WP e @ E ?{{ Φ }}.
  Proof.
    iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
150
    - apply of_to_val in EQe as <-. iApply fupd_wp.
151
      iMod "H" as (σ1 κs) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
152
      by rewrite to_of_val in Hnv.
153 154 155
    - iApply wp_lift_stuck; [done|]. iIntros (σ1 κs) "Hσ".
      iMod "H" as (σ1' κs') "(% & >[Hσf Hκsf])".
      by iDestruct (ownP_eq with "Hσ Hσf Hκsf") as %[-> _].
156 157
  Qed.

158
  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
Ralf Jung's avatar
Ralf Jung committed
159
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
160
    ( σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs  κ = None  σ1 = σ2) 
161
    (  κ e2 efs σ, prim_step e1 σ κ e2 σ efs 
162 163
      WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
164
  Proof.
165 166 167
    iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
    { specialize (Hsafe inhabitant). destruct s; last done.
      by eapply reducible_not_val. }
168 169
    iIntros (σ1 κs) "Hσ". iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ κs' e2 σ2 efs [??]).
170
    destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
171
    by iMod "Hclose"; iModIntro; iFrame; iApply "H".
172 173 174
  Qed.

  (** Derived lifting lemmas. *)
175
  Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 κs :
Ralf Jung's avatar
Ralf Jung committed
176
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
177 178 179
    ( (ownP_state σ1  ownP_obs κs) 
         κ κs' e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs  κs = cons_obs κ κs' -
         ownP_state σ2 - ownP_obs κs' -
Ralf Jung's avatar
Ralf Jung committed
180
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
181
     WP e1 @ s; E {{ Φ }}.
182
  Proof.
183
    iIntros (?) "[[Hσ Hκs] H]"; iApply ownP_lift_step.
184
    iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
185 186 187
    iModIntro; iExists σ1, κs; iFrame; iSplit; first by destruct s.
    iNext; iIntros (κ κs' e2 σ2 efs [??]) "[Hσ Hκs]".
    iDestruct ("H" $! κ κs' e2 σ2 efs with "[] [Hσ] [Hκs]") as "[HΦ $]"; [by eauto..|].
188
    destruct (to_val e2) eqn:?; last by iExFalso.
189
    iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
190 191
  Qed.

192
  Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 κ κs v2 σ2 efs :
Ralf Jung's avatar
Ralf Jung committed
193
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
194 195 196
    ( κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' 
                     κ = κ'  σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
     (ownP_state σ1  ownP_obs (cons_obs κ κs))   (ownP_state σ2 - ownP_obs κs -
197 198 199
      Φ v2  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
  Proof.
200 201 202 203
    iIntros (? Hdet) "[[Hσ1 Hκs] Hσ2]"; iApply ownP_lift_atomic_step; try done.
    iFrame; iNext; iIntros (κ' κs' e2' σ2' efs' (? & Heq)) "Hσ2' Hκs'".
    edestruct (Hdet κ') as (->&->&Hval&->); first done. rewrite Hval. apply app_inv_head in Heq as ->.
    iApply ("Hσ2" with "Hσ2' Hκs'").
204 205
  Qed.

206
  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 κ κs v2 σ2 :
Ralf Jung's avatar
Ralf Jung committed
207
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
208 209 210
    ( κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' 
      κ = κ'  σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
    {{{  (ownP_state σ1  ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2  ownP_obs κs}}}.
211
  Proof.
212 213 214
    intros. rewrite -(ownP_lift_atomic_det_step σ1 κ κs v2 σ2 []); [|done..].
    rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
    iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2 Hκs". iApply "Hs'". iFrame.
215 216
  Qed.

217
  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
Ralf Jung's avatar
Ralf Jung committed
218
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
219
    ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  efs = efs')
220 221
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s; {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
222
  Proof.
223
    iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
224
    naive_solver. by iNext; iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
225 226 227
  Qed.

  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
Ralf Jung's avatar
Ralf Jung committed
228
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
229
    ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  [] = efs') 
230
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
231
  Proof.
232
    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
233 234 235 236 237
  Qed.
End lifting.

Section ectx_lifting.
  Import ectx_language.
238
  Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
239
  Implicit Types s : stuckness.
240 241
  Implicit Types Φ : val Λ  iProp Σ.
  Implicit Types e : expr Λ.
242
  Hint Resolve head_prim_reducible head_reducible_prim_step.
243
  Hint Resolve (reducible_not_val _ inhabitant).
244
  Hint Resolve head_stuck_stuck.
245

246
  Lemma ownP_lift_head_step s E Φ e1 :
247 248 249
    (|={E,}=>  σ1 κs, head_reducible e1 σ1   (ownP_state σ1   ownP_obs κs) 
              κ κs' e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs  κs = cons_obs κ κs' -
            ownP_state σ2 - ownP_obs κs'
250 251
            ={,E}= WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
252
  Proof.
253
    iIntros "H". iApply ownP_lift_step.
254
    iMod "H" as (σ1 κs ?) "[>[Hσ1 Hκs] Hwp]". iModIntro. iExists σ1, κs. iSplit.
255
    { destruct s; try by eauto using reducible_not_val. }
256 257
    iFrame. iNext. iIntros (κ κs' e2 σ2 efs [? ->]) "[Hσ2 Hκs']".
    iApply ("Hwp" with "[] Hσ2"); eauto.
258 259
  Qed.

260
  Lemma ownP_lift_head_stuck E Φ e :
261
    sub_redexes_are_values e 
262
    (|={E,}=>  σ κs, head_stuck e σ⌝   (ownP_state σ  ownP_obs κs))
263 264
     WP e @ E ?{{ Φ }}.
  Proof.
265 266
    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ κs) "[% >[Hσ Hκs]]".
    iExists σ, κs. iModIntro. by auto with iFrame.
267 268 269
  Qed.

  Lemma ownP_lift_pure_head_step s E Φ e1 :
270
    ( σ1, head_reducible e1 σ1) 
271
    ( σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs  κ = None  σ1 = σ2) 
272
    (  κ e2 efs σ, head_step e1 σ κ e2 σ efs 
273 274
      WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
275
  Proof using Hinh.
276
    iIntros (??) "H".  iApply ownP_lift_pure_step; eauto.
277
    { by destruct s; auto. }
278
    iNext. iIntros (?????). iApply "H"; eauto.
279 280
  Qed.

281
  Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 κs :
282
    head_reducible e1 σ1 
283 284
     (ownP_state σ1  ownP_obs κs)   ( κ κs' e2 σ2 efs,
    head_step e1 σ1 κ e2 σ2 efs  κs = cons_obs κ κs' - ownP_state σ2 - ownP_obs κs' -
Ralf Jung's avatar
Ralf Jung committed
285
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
286
     WP e1 @ s; E {{ Φ }}.
287
  Proof.
288
    iIntros (?) "[Hst H]". iApply ownP_lift_atomic_step; eauto.
289
    { by destruct s; eauto using reducible_not_val. }
290 291
    iSplitL "Hst"; first done.
    iNext. iIntros (????? [? ->]) "Hσ ?". iApply ("H" with "[] Hσ"); eauto.
292 293
  Qed.

294
  Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 κ κs v2 σ2 efs :
295
    head_reducible e1 σ1 
296 297 298 299
    ( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' 
      κ = κ'  σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
     (ownP_state σ1  ownP_obs (cons_obs κ κs))   (ownP_state σ2 - ownP_obs κs -
                                                    Φ v2  [ list] ef  efs, WP ef @ s;  {{ _, True }})
300 301
     WP e1 @ s; E {{ Φ }}.
  Proof.
302
    intros Hr Hs. destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val.
303
  Qed.
304

305
  Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 κ κs v2 σ2 :
306
    head_reducible e1 σ1 
307 308 309
    ( κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' 
      κ = κ'  σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
    {{{  (ownP_state σ1  ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2  ownP_obs κs }}}.
310
  Proof.
311
    intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
312
    by destruct s; eauto using reducible_not_val.
313 314
  Qed.

315
  Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
316
    ( σ1, head_reducible e1 σ1) 
317
    ( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  efs = efs') 
318 319
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
320
  Proof using Hinh.
321 322
    iIntros (??) "H"; iApply wp_lift_pure_det_step; eauto.
    by destruct s; eauto using reducible_not_val.
Ralf Jung's avatar
Ralf Jung committed
323
  Qed.
324

325
  Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
326
    ( σ1, head_reducible e1 σ1) 
327
    ( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  [] = efs') 
328
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
329
  Proof using Hinh.
330 331
    iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
    by destruct s; eauto using reducible_not_val.
332 333
  Qed.
End ectx_lifting.