ownp.v 9.71 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
9
10
11
12
13
14
15
16
17
18

Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
  ownP_invG : invG Σ;
  ownP_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
  ownP_name : gname;
}.
Notation ownPG Λ Σ := (ownPG' (state Λ) Σ).

Instance ownPG_irisG `{ownPG' Λstate Σ} : irisG' Λstate Σ := {
  iris_invG := ownP_invG;
  state_interp σ := own ownP_name ( (Excl' (σ:leibnizC Λstate)))
}.
19
Global Opaque iris_invG.
20
21
22

Definition ownPΣ (Λstate : Type) : gFunctors :=
  #[invΣ;
23
    GFunctor (authUR (optionUR (exclR (leibnizC Λstate))))].
24
25
26
27
28
29
30
31

Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
  ownPPre_invG :> invPreG Σ;
  ownPPre_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
}.
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).

Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ  ownPPreG' Λstate Σ.
32
Proof. solve_inG. Qed.
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

(** Ownership *)
Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
  own ownP_name ( (Excl' σ)).
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3.


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

53
Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ :
54
  ( `{ownPG Λ Σ},
55
    ownP σ1 ={}= WP e {{ _, True }}  |={,}=>  σ', ownP σ'  ⌜φ σ') 
56
57
58
  rtc step ([e], σ1) (t2, σ2) 
  φ σ2.
Proof.
59
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _)=> //.
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
  iIntros (?) "". iMod (own_alloc ( (Excl' (σ1 : leibnizC _))   (Excl' σ1)))
    as (γσ) "[Hσ Hσf]"; first done.
  iExists (λ σ, own γσ ( (Excl' (σ:leibnizC _)))). iFrame "Hσ".
  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
  iDestruct (own_valid_2 with "Hσ Hσf")
    as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
Qed.


(** Lifting *)
Section lifting.
  Context `{ownPG Λ Σ}.
  Implicit Types e : expr Λ.
  Implicit Types Φ : val Λ  iProp Σ.

  Lemma ownP_twice σ1 σ2 : ownP σ1  ownP σ2  False.
  Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
  Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
  Proof. rewrite /ownP; apply _. Qed.

  Lemma ownP_lift_step E Φ e1 :
    (|={E,}=>  σ1, reducible e1 σ1   ownP σ1 
        e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2
            ={,E}= WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
      move: Hred; by rewrite to_of_val.
    - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
      iMod "H" as (σ1') "(% & >Hσf & H)". rewrite /ownP.
      iDestruct (own_valid_2 with "Hσ Hσf")
        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
      iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
      { by apply auth_update, option_local_update,
          (exclusive_local_update _ (Excl σ2)). }
99
      iFrame "Hσ". iApply ("H" with "[]"); eauto.
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
  Qed.

  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
    ( σ1, reducible e1 σ1) 
    ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
    (  e2 efs σ, prim_step e1 σ e2 σ efs 
      WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
    { eapply reducible_not_val, (Hsafe inhabitant). }
    iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
    iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
    destruct (Hstep σ1 e2 σ2 efs); auto; subst.
    iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
  Qed.

  (** Derived lifting lemmas. *)
  Lemma ownP_lift_atomic_step {E Φ} e1 σ1 :
    reducible e1 σ1 
    ( ownP σ1    e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs - ownP σ2 -
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (?) "[Hσ H]". iApply (ownP_lift_step E _ e1).
    iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver. iModIntro.
    iExists σ1. iFrame "Hσ"; iSplit; eauto.
    iNext; iIntros (e2 σ2 efs) "% Hσ".
    iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
    destruct (to_val e2) eqn:?; last by iExFalso.
    iMod "Hclose". iApply wp_value; auto using to_of_val. done.
  Qed.

  Lemma ownP_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
    reducible e1 σ1 
    ( e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' 
                     σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
     ownP σ1   (ownP σ2 -
      Φ v2  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (ownP_lift_atomic_step _ σ1); try done.
    iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
    edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
  Qed.

  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
    ( σ1, reducible e1 σ1) 
    ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
     (WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (? Hpuredet) "?". iApply (ownP_lift_pure_step E); try done.
    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
  Qed.
End lifting.

Section ectx_lifting.
  Import ectx_language.
  Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
160
  Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
161
162
163
164
165
166
167
168
169
170
171
172
173
  Implicit Types Φ : val  iProp Σ.
  Implicit Types e : expr.
  Hint Resolve head_prim_reducible head_reducible_prim_step.

  Lemma ownP_lift_head_step E Φ e1 :
    (|={E,}=>  σ1, head_reducible e1 σ1   ownP σ1 
        e2 σ2 efs, head_step e1 σ1 e2 σ2 efs - ownP σ2
            ={,E}= WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros "H". iApply (ownP_lift_step E); try done.
    iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
    iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
174
    iApply ("Hwp" with "[]"); eauto.
175
176
177
178
179
180
181
182
  Qed.

  Lemma ownP_lift_pure_head_step E Φ e1 :
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
    (  e2 efs σ, head_step e1 σ e2 σ efs 
      WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
183
  Proof using Hinh.
184
185
186
187
188
189
190
191
192
193
194
195
    iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
    iIntros (????). iApply "H". eauto.
  Qed.

  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
    head_reducible e1 σ1 
     ownP σ1   ( e2 σ2 efs,
    head_step e1 σ1 e2 σ2 efs - ownP σ2 -
      default False (to_val e2) Φ  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof.
    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iFrame. iNext.
196
    iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
  Qed.

  Lemma ownP_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
    head_reducible e1 σ1 
    ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
      σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
     ownP σ1   (ownP σ2 - Φ v2  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
  Proof. eauto using ownP_lift_atomic_det_step. Qed.

  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
    head_reducible e1 σ1 
    ( e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' 
      σ2 = σ2'  to_val e2' = Some v2  [] = efs') 
    {{{  ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
  Proof.
    intros. rewrite -(ownP_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
  Qed.

  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs') 
     (WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
     WP e1 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
222
223
224
  Proof using Hinh.
    intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_step; eauto.
  Qed.
225
226
227
228
229
230

  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
    to_val e1 = None 
    ( σ1, head_reducible e1 σ1) 
    ( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  [] = efs') 
     WP e2 @ E {{ Φ }}  WP e1 @ E {{ Φ }}.
231
  Proof using Hinh.
232
233
234
    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
  Qed.
End ectx_lifting.