adequacy.v 12 KB
Newer Older
1
From stdpp Require Import namespaces.
2
From iris.program_logic Require Export weakestpre.
3
From iris.algebra Require Import gmap auth agree gset coPset.
4
From iris.base_logic.lib Require Import wsat.
5
From iris.proofmode Require Import tactics.
6
Set Default Proof Using "Type".
7
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
(* Program logic adequacy *)
10 11
Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
    (φ : val Λ  state Λ  Prop) := {
12
  adequate_result t2 σ2 v2 :
13
   rtc erased_step ([e1], σ1) (of_val v2 :: t2, σ2)  φ v2 σ2;
14
  adequate_not_stuck t2 σ2 e2 :
Ralf Jung's avatar
Ralf Jung committed
15
   s = NotStuck 
16
   rtc erased_step ([e1], σ1) (t2, σ2) 
17 18 19 20
   e2  t2  (is_Some (to_val e2)  reducible e2 σ2)
}.

Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
Ralf Jung's avatar
Ralf Jung committed
21
  adequate NotStuck e1 σ1 φ 
22 23
  rtc erased_step ([e1], σ1) (t2, σ2) 
  Forall (λ e, is_Some (to_val e)) t2   κ t3 σ3, step (t2, σ2) κ (t3, σ3).
24 25 26 27
Proof.
  intros Had ?.
  destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
  apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
28
  destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(κ&e3&σ3&efs&?)];
29 30 31
    rewrite ?eq_None_not_Some; auto.
  { exfalso. eauto. }
  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
32
  right; exists κ, (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
33 34
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
35
Section adequacy.
36
Context `{irisG Λ Σ}.
37
Implicit Types e : expr Λ.
38 39 40
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types Φs : list (val Λ  iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
41

42
Notation wptp s t := ([ list] ef  t, WP ef @ s;  {{ fork_post }})%I.
43

44
Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
45
  prim_step e1 σ1 κ e2 σ2 efs 
46 47
  state_interp σ1 (κ ++ κs) m - WP e1 @ s;  {{ Φ }} ={,}=
  state_interp σ2 κs (length efs + m)  WP e2 @ s;  {{ Φ }}  wptp s efs.
48
Proof.
49
  rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
50 51 52 53
  rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
  iMod ("H" $! σ1 with "Hσ") as "(_ & H)".
  iMod ("H" $! e2 σ2 efs with "[//]") as "H".
  by iIntros "!> !>".
54 55
Qed.

56
Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
57
  step (e1 :: t1,σ1) κ (t2, σ2) 
58 59 60
  state_interp σ1 (κ ++ κs) (length t1) - WP e1 @ s;  {{ Φ }} - wptp s t1 ==
   e2 t2', t2 = e2 :: t2' 
  |={,}=> state_interp σ2 κs (pred (length t2))  WP e2 @ s;  {{ Φ }}  wptp s t2'.
61
Proof.
62
  iIntros (Hstep) "Hσ He Ht".
63
  destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
64 65 66 67
  - iExists e2', (t2' ++ efs). iModIntro. iSplitR; first by eauto.
    iMod (wp_step with "Hσ He") as "H"; first done.
    iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)".
    iIntros "!>". rewrite Nat.add_comm app_length. iFrame.
68
  - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
69 70 71 72 73 74
    iFrame "He". iDestruct "Ht" as "(Ht1 & He1 & Ht2)".
    iModIntro. iMod (wp_step with "Hσ He1") as "H"; first done.
    iIntros "!> !>". iMod "H" as "(Hσ & He2 & Hefs)". iIntros "!>".
    rewrite !app_length /= !app_length.
    replace (length t1' + S (length t2' + length efs))
      with (length efs + (length t1' + S (length t2'))) by omega. iFrame.
75 76
Qed.

77
Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
78
  nsteps n (e1 :: t1, σ1) κs (t2, σ2) 
79 80 81 82 83
  state_interp σ1 (κs ++ κs') (length t1) - WP e1 @ s;  {{ Φ }} - wptp s t1
  ={,}=^n  e2 t2',
    t2 = e2 :: t2' 
    state_interp σ2 κs' (pred (length t2)) 
    WP e2 @ s;  {{ Φ }}  wptp s t2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Proof.
85 86 87 88 89 90 91 92
  revert e1 t1 κs κs' t2 σ1 σ2; simpl.
  induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
  { inversion_clear 1; iIntros "???"; iExists e1, t1; iFrame; eauto 10. }
  iIntros (Hsteps) "Hσ He Ht". inversion_clear Hsteps as [|?? [t1' σ1']].
  rewrite -(assoc_L (++)).
  iMod (wptp_step with "Hσ He Ht") as (e1' t1'' ?) ">H"; first eauto; simplify_eq.
  iIntros "!> !>". iMod "H" as "(Hσ & He & Ht)". iModIntro.
  by iApply (IH with "Hσ He Ht").
93 94
Qed.

95
Lemma wptp_result φ κs' s n e1 t1 κs v2 t2 σ1 σ2  :
96
  nsteps n (e1 :: t1, σ1) κs (of_val v2 :: t2, σ2) 
97 98 99
  state_interp σ1 (κs ++ κs') (length t1) -
  WP e1 @ s;  {{ v,  σ, state_interp σ κs' (length t2) ={,}= ⌜φ v σ⌝ }} -
  wptp s t1 ={,}=^(S n) ⌜φ v2 σ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Proof.
101 102 103
  iIntros (?) "Hσ He Ht". rewrite Nat_iter_S_r.
  iDestruct (wptp_steps with "Hσ He Ht") as "H"; first done.
  iApply (step_fupdN_wand with "H").
104 105
  iDestruct 1 as (e2 t2' ?) "(Hσ & H & _)"; simplify_eq.
  iMod (wp_value_inv' with "H") as "H".
106 107 108
  iMod (fupd_plain_mask_empty _ ⌜φ v2 σ2%I with "[H Hσ]") as %?.
  { by iMod ("H" with "Hσ") as "$". }
  by iApply step_fupd_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Qed.
Ralf Jung's avatar
Ralf Jung committed
110

111 112 113 114
Lemma wptp_all_result φ κs' s n e1 t1 κs v2 vs2 σ1 σ2 :
  nsteps n (e1 :: t1, σ1) κs (of_val <$> v2 :: vs2, σ2) 
  state_interp σ1 (κs ++ κs') (length t1) -
  WP e1 @ s;  {{ v,
115 116
    state_interp σ2 κs' (length vs2) -
    ([ list] v  vs2, fork_post v) ={,}= ⌜φ v  }} -
117 118 119 120 121 122 123 124
  wptp s t1
  ={,}=^(S n) ⌜φ v2 .
Proof.
  iIntros (Hstep) "Hσ He Ht". rewrite Nat_iter_S_r.
  iDestruct (wptp_steps with "Hσ He Ht") as "H"; first done.
  iApply (step_fupdN_wand with "H").
  iDestruct 1 as (e2 t2' ?) "(Hσ & H & Hvs)"; simplify_eq/=.
  rewrite fmap_length. iMod (wp_value_inv' with "H") as "H".
125
  iAssert ([ list] v  vs2, fork_post v)%I with "[> Hvs]" as "Hm".
126 127 128 129 130 131 132 133 134 135 136
  { clear Hstep. iInduction vs2 as [|v vs] "IH"; csimpl; first by iFrame.
    iDestruct "Hvs" as "[Hv Hvs]".
    iMod (wp_value_inv' with "Hv") as "$". by iApply "IH". }
  iMod (fupd_plain_mask_empty _ ⌜φ v2%I with "[H Hm Hσ]") as %?.
  { iApply ("H" with "Hσ Hm"). }
  by iApply step_fupd_intro.
Qed.

Lemma wp_safe κs m e σ Φ :
  state_interp σ κs m -
  WP e {{ Φ }} ={,}= is_Some (to_val e)  reducible e σ⌝.
137
Proof.
138
  rewrite wp_unfold /wp_pre. iIntros "Hσ H".
139
  destruct (to_val e) as [v|] eqn:?.
140
  { iApply step_fupd_intro. set_solver. eauto. }
141
  iMod (fupd_plain_mask_empty _ reducible e σ⌝%I with "[H Hσ]") as %?.
142
  { by iMod ("H" $! σ [] κs with "Hσ") as "[$ H]". }
143 144
  iApply step_fupd_intro; first by set_solver+. 
  iIntros "!> !%". by right.
145
Qed.
Ralf Jung's avatar
Ralf Jung committed
146

147
Lemma wptp_safe κs' n e1 κs e2 t1 t2 σ1 σ2 Φ :
148
  nsteps n (e1 :: t1, σ1) κs (t2, σ2)  e2  t2 
149 150
  state_interp σ1 (κs ++ κs') (length t1) - WP e1 {{ Φ }} - wptp NotStuck t1
  ={,}=^(S n) is_Some (to_val e2)  reducible e2 σ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
152 153 154 155 156 157 158
  iIntros (? He2) "Hσ He Ht". rewrite Nat_iter_S_r.
  iDestruct (wptp_steps  with "Hσ He Ht") as "H"; first done.
  iApply (step_fupdN_wand with "H").
  iDestruct 1 as (e2' t2' ?) "(Hσ & H & Ht)"; simplify_eq.
  apply elem_of_cons in He2 as [<-|(t1''&t2''&->)%elem_of_list_split].
  - iMod (wp_safe with "Hσ H") as "$"; auto.
  - iDestruct "Ht" as "(_ & He2 & _)". by iMod (wp_safe with "Hσ He2").
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Qed.
160

161
Lemma wptp_invariance φ s n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
162
  nsteps n (e1 :: t1, σ1) κs (t2, σ2) 
163 164 165 166
  (state_interp σ2 κs' (pred (length t2)) ={,}= ⌜φ⌝) -
  state_interp σ1 (κs ++ κs') (length t1) -
  WP e1 @ s;  {{ Φ }} - wptp s t1
  ={,}=^(S n) ⌜φ⌝.
167
Proof.
168 169 170 171 172 173
  iIntros (?) "Hφ Hσ He Ht". rewrite Nat_iter_S_r.
  iDestruct (wptp_steps _ n with "Hσ He Ht") as "H"; first done.
  iApply (step_fupdN_wand with "H"). iDestruct 1 as (e2' t2' ->) "[Hσ _]".
  iSpecialize ("Hφ" with "Hσ").
  iMod (fupd_plain_mask_empty _ ⌜φ⌝%I with "Hφ") as %?.
  by iApply step_fupd_intro.
174
Qed.
175
End adequacy.
Ralf Jung's avatar
Ralf Jung committed
176

177
Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
178
  ( `{Hinv : invG Σ} κs,
179 180
     (|={}=> 
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
181
         (fork_post : val Λ  iProp Σ),
Robbert Krebbers's avatar
Robbert Krebbers committed
182
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
183 184 185
       (* This could be strengthened so that φ also talks about the number 
       of forked-off threads *)
       stateI σ κs 0  WP e @ s;  {{ v,  σ m, stateI σ [] m ={,}= ⌜φ v σ⌝ }})%I) 
186
  adequate s e σ φ.
Ralf Jung's avatar
Ralf Jung committed
187
Proof.
188
  intros Hwp; split.
189
  - intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
190 191 192
    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
    iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]".
    iApply step_fupd_intro; first done. iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
    iApply (@wptp_result _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] [Hwp]"); eauto.
194
    iApply (wp_wand with "Hwp"). iIntros (v) "H"; iIntros (σ'). iApply "H".
195
  - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
196 197 198
    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
    iMod (Hwp _ (κs ++ [])) as (stateI fork_post) "[Hσ Hwp]".
    iApply step_fupd_intro; first done. iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
    iApply (@wptp_safe _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
Qed.
201

202
Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
203 204
  ( `{Hinv : invG Σ} κs,
     (|={}=>  stateI : state Λ  list (observation Λ)  iProp Σ,
205
       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) (λ _, True%I) in
206
       stateI σ κs  WP e @ s;  {{ v, ⌜φ v }})%I) 
207 208
  adequate s e σ (λ v _, φ v).
Proof.
209
  intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv κs.
210
  iMod Hwp as (stateI) "[Hσ H]". iExists (λ σ κs _, stateI σ κs), (λ _, True%I).
211
  iIntros "{$Hσ} !>".
212
  iApply (wp_wand with "H"). iIntros (v ? σ') "_".
213 214 215 216 217 218 219
  iIntros "_". by iApply fupd_mask_weaken.
Qed.

Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
  ( `{Hinv : invG Σ} κs,
     (|={}=> 
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
220
         (fork_post : val Λ  iProp Σ),
Robbert Krebbers's avatar
Robbert Krebbers committed
221
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
222
       stateI σ1 κs 0  WP e @ s;  {{ v,
223 224
         stateI σ2 [] (length vs) -
         ([ list] v  vs, fork_post v) ={,}=  φ v  }})%I) 
225 226 227 228 229 230 231
  rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) 
  φ v.
Proof.
  intros Hwp [n [κs ?]]%erased_steps_nsteps.
  eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
  iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
  iApply step_fupd_intro; first done. iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
  iApply (@wptp_all_result _ _ (IrisG _ _ Hinv stateI fork_post)
233
    with "[Hσ] [Hwp]"); eauto. by rewrite right_id_L.
234 235
Qed.

236
Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
237
  ( `{Hinv : invG Σ} κs κs',
238 239
     (|={}=> 
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
240
         (fork_post : val Λ  iProp Σ),
Robbert Krebbers's avatar
Robbert Krebbers committed
241
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
242 243
       stateI σ1 (κs ++ κs') 0  WP e @ s;  {{ _, True }} 
       (stateI σ2 κs' (pred (length t2)) ={,}= ⌜φ⌝))%I) 
244
  rtc erased_step ([e], σ1) (t2, σ2) 
245
  φ.
246
Proof.
247
  intros Hwp [n [κs ?]]%erased_steps_nsteps.
248 249
  apply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
  iMod (Hwp Hinv κs []) as (Istate fork_post) "(Hσ & Hwp & Hclose)".
250
  iApply step_fupd_intro; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
  iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate fork_post)
252
    with "Hclose [Hσ] [Hwp]"); eauto.
253
Qed.
254 255 256 257

(* An equivalent version that does not require finding [fupd_intro_mask'], but
can be confusing to use. *)
Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
258
  ( `{Hinv : invG Σ} κs κs',
259 260
     (|={}=> 
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
261
         (fork_post : val Λ  iProp Σ),
Robbert Krebbers's avatar
Robbert Krebbers committed
262
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
263 264
       stateI σ1 κs 0  WP e @ s;  {{ _, True }} 
       (stateI σ2 κs' (pred (length t2)) -  E, |={,E}=> ⌜φ⌝))%I) 
265
  rtc erased_step ([e], σ1) (t2, σ2) 
266 267 268
  φ.
Proof.
  intros Hwp. eapply wp_invariance; first done.
269 270
  intros Hinv κs κs'. iMod (Hwp Hinv) as (stateI fork_post) "(? & ? & Hφ)".
  iModIntro. iExists stateI, fork_post. iFrame. iIntros "Hσ".
271
  iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
272
  by iApply fupd_mask_weaken; first set_solver.
273
Qed.