ownp.v 13.4 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
  ownP_inG :> inG Σ (authR (optionUR (exclR (prodC (leibnizC Λstate) (leibnizC (list Λobservation))))));
11 12
  ownP_name : gname;
}.
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), (κs:leibnizC (list Λobservation)))))
18
}.
19
Global Opaque iris_invG.
20

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

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

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

(** Ownership *)
35 36
Definition ownP `{ownPG' Λstate Λobservation Σ} (σ : Λstate) (κs : list Λobservation) : iProp Σ :=
  own ownP_name ( (Excl' (σ, κs))).
37 38 39 40 41
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3.


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

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


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

79
  Lemma ownP_eq σ1 σ2 κs1 κs2 : state_interp σ1 κs1 - ownP σ2 κs2 - ⌜σ1 = σ2  κs1 = κs2.
80 81
  Proof.
    iIntros "Hσ1 Hσ2"; rewrite/ownP.
82 83 84 85
    iDestruct (own_valid_2 with "Hσ1 Hσ2")
      as %[Hp _]%auth_valid_discrete_2.
    pose proof (Excl_included _ _ Hp) as Hp'. apply leibniz_equiv in Hp'. inversion Hp'; subst. auto.
  (* TODO (MR) inline this proof in introduction pattern? *)
86
  Qed.
87
  Lemma ownP_twice σ1 σ2 κs1 κs2 : ownP σ1 κs1  ownP σ2 κs2  False.
88
  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
89
  Global Instance ownP_timeless σ κs : Timeless (@ownP (state Λ) (observation Λ) Σ _ σ κs).
90 91
  Proof. rewrite /ownP; apply _. Qed.

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

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

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

  (** Derived lifting lemmas. *)
142
  Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
Ralf Jung's avatar
Ralf Jung committed
143
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
144
    ( ownP σ1    κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs - ownP σ2 -
Ralf Jung's avatar
Ralf Jung committed
145
      from_option Φ False (to_val e2)  [ list] ef  efs, WP ef @ s;  {{ _, True }})
146
     WP e1 @ s; E {{ Φ }}.
147
  Proof.
148
    iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
149 150
    iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
    iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
151 152
    iNext; iIntros (κ e2 σ2 efs) "% Hσ".
    iDestruct ("H" $! κ e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
153
    destruct (to_val e2) eqn:?; last by iExFalso.
154
    iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
155 156
  Qed.

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

  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
Ralf Jung's avatar
Ralf Jung committed
171
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
172
    ( κ e2' σ2' efs', prim_step e1 σ1 κ e2' σ2' efs' 
173 174
      σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
    {{{  ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
175
  Proof.
176
    intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
177
    rewrite big_sepL_nil right_id. by apply bi.wand_intro_r.
178 179
  Qed.

180
  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
Ralf Jung's avatar
Ralf Jung committed
181
    ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
182
    ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  efs = efs')
183 184
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s; {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
185
  Proof.
186
    iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
187
    naive_solver. by iNext; iIntros (κ e' efs' σ (&_&&)%Hpuredet).
188 189 190
  Qed.

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

Section ectx_lifting.
  Import ectx_language.
201
  Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
202
  Implicit Types s : stuckness.
203 204
  Implicit Types Φ : val Λ  iProp Σ.
  Implicit Types e : expr Λ.
205
  Hint Resolve head_prim_reducible head_reducible_prim_step.
206
  Hint Resolve (reducible_not_val _ inhabitant).
207
  Hint Resolve head_stuck_stuck.
208

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

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

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

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

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

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

276
  Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
277
    ( σ1, head_reducible e1 σ1) 
278
    ( σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  efs = efs') 
279 280
     (WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
     WP e1 @ s; E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
281
  Proof using Hinh.
282 283
    iIntros (??) "H"; iApply wp_lift_pure_det_step; eauto.
    by destruct s; eauto using reducible_not_val.
Ralf Jung's avatar
Ralf Jung committed
284
  Qed.
285

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'  κ = None  σ1 = σ2  e2 = e2'  [] = efs') 
289
     WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
290
  Proof using Hinh.
291 292
    iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
    by destruct s; eauto using reducible_not_val.
293 294
  Qed.
End ectx_lifting.