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

8 9
(** This file contains the adequacy statements of the Iris program logic. First
we prove a number of auxilary results. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Section adequacy.
11
Context `{!irisG Λ Σ}.
12
Implicit Types e : expr Λ.
13 14 15
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types Φs : list (val Λ  iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
16

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

19
Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
20
  prim_step e1 σ1 κ e2 σ2 efs 
21 22
  state_interp σ1 (κ ++ κs) m - WP e1 @ s;  {{ Φ }} ={,}=
  state_interp σ2 κs (length efs + m)  WP e2 @ s;  {{ Φ }}  wptp s efs.
23
Proof.
24
  rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
25 26 27 28
  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 "!> !>".
29 30
Qed.

31
Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
32
  step (e1 :: t1,σ1) κ (t2, σ2) 
33 34 35
  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'.
36
Proof.
37
  iIntros (Hstep) "Hσ He Ht".
38
  destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
39 40 41 42
  - 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.
43
  - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
44 45 46 47 48 49
    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.
50 51
Qed.

52
Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
53
  nsteps n (e1 :: t1, σ1) κs (t2, σ2) 
54 55 56 57 58
  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
59
Proof.
60 61 62 63 64 65 66 67
  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").
68 69
Qed.

Amin Timany's avatar
Amin Timany committed
70 71
Lemma wp_not_stuck κs m e σ Φ :
  state_interp σ κs m - WP e {{ Φ }} ={}= not_stuck e σ⌝.
72
Proof.
Amin Timany's avatar
Amin Timany committed
73
  rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
74 75 76
  destruct (to_val e) as [v|] eqn:?; first by eauto.
  iSpecialize ("H" $! σ [] κs with "Hσ"). rewrite sep_elim_l.
  iMod (fupd_plain_mask with "H") as %?; eauto.
77
Qed.
Ralf Jung's avatar
Ralf Jung committed
78

79
Lemma wptp_strong_adequacy Φ κs' s n e1 t1 κs e2 t2 σ1 σ2 :
80
  nsteps n (e1 :: t1, σ1) κs (t2, σ2) 
81
  state_interp σ1 (κs ++ κs') (length t1) -
82
  WP e1 @ s;  {{ Φ }} -
83 84 85 86 87 88
  wptp s t1 ={,}=^(S n)  e2 t2',
     t2 = e2 :: t2'  
      e2, s = NotStuck  e2  t2  (is_Some (to_val e2)  reducible e2 σ2)  
    state_interp σ2 κs' (length t2') 
    from_option Φ True (to_val e2) 
    ([ list] v  omap to_val t2', fork_post v).
89
Proof.
90
  iIntros (Hstep) "Hσ He Ht". rewrite Nat_iter_S_r.
91 92 93 94 95 96 97 98 99
  iDestruct (wptp_steps with "Hσ He Ht") as "Hwp"; first done.
  iApply (step_fupdN_wand with "Hwp").
  iDestruct 1 as (e2' t2' ?) "(Hσ & Hwp & Ht)"; simplify_eq/=.
  iMod (fupd_plain_keep_l 
      e2, s = NotStuck  e2  (e2' :: t2')  (is_Some (to_val e2)  reducible e2 σ2) %I
    (state_interp σ2 κs' (length t2')  WP e2' @ s;  {{ v, Φ v }}  wptp s t2')%I
    with "[$Hσ $Hwp $Ht]") as "(Hsafe&Hσ&Hwp&Hvs)".
  { iIntros "(Hσ & Hwp & Ht)" (e' -> He').
    apply elem_of_cons in He' as [<-|(t1''&t2''&->)%elem_of_list_split].
Amin Timany's avatar
Amin Timany committed
100 101
    - iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto.
    - iDestruct "Ht" as "(_ & He' & _)". by iMod (wp_not_stuck with "Hσ He'"). }
102 103 104
  iApply step_fupd_fupd. iApply step_fupd_intro; first done. iNext.
  iExists _, _. iSplitL ""; first done. iFrame "Hsafe Hσ".
  iSplitL "Hwp".
105 106 107 108 109 110 111
  - destruct (to_val e2') as [v2|] eqn:He2'; last done.
    apply of_to_val in He2' as <-. iApply (wp_value_inv' with "Hwp").
  - clear Hstep. iInduction t2' as [|e t2'] "IH"; csimpl; first by iFrame.
    iDestruct "Hvs" as "[Hv Hvs]". destruct (to_val e) as [v|] eqn:He.
    + apply of_to_val in He as <-. iMod (wp_value_inv' with "Hv") as "$".
      by iApply "IH".
    + by iApply "IH".
112
Qed.
113
End adequacy.
Ralf Jung's avatar
Ralf Jung committed
114

115
(** Iris's generic adequacy result *)
116
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e1 σ1 n κs t2 σ2 φ :
117
  ( `{Hinv : !invG Σ},
118
     (|={}=> 
119
         (s: stuckness)
120
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
121
         (Φ fork_post : val Λ  iProp Σ),
Robbert Krebbers's avatar
Robbert Krebbers committed
122
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
123
       stateI σ1 κs 0 
124
       WP e1 @ s;  {{ Φ }} 
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141
       ( e2 t2',
         (* e2 is the final state of the main thread, t2' the rest *)
          t2 = e2 :: t2'  -
         (* If this is a stuck-free triple (i.e. [s = NotStuck]), then all
         threads in [t2] are either done (a value) or reducible *)
           e2, s = NotStuck  e2  t2  (is_Some (to_val e2)  reducible e2 σ2)  -
         (* The state interpretation holds for [σ2] *)
         stateI σ2 [] (length t2') -
         (* If the main thread is done, its post-condition [Φ] holds *)
         from_option Φ True (to_val e2) -
         (* For all threads that are done, their postcondition [fork_post] holds. *)
         ([ list] v  omap to_val t2', fork_post v) -
         (* Under all these assumptions, and while opening all invariants, we
         can conclude [φ] in the logic. After opening all required invariants,
         one can use [fupd_intro_mask'] or [fupd_mask_weaken] to introduce the
         fancy update. *)
         |={,}=>  φ ))%I) 
142
  nsteps n ([e1], σ1) κs (t2, σ2) 
143 144
  (* Then we can conclude [φ] at the meta-level. *)
  φ.
Ralf Jung's avatar
Ralf Jung committed
145
Proof.
146 147
  intros Hwp ?.
  eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv. rewrite Nat_iter_S.
148
  iMod Hwp as (s stateI Φ fork_post) "(Hσ & Hwp & Hφ)".
149
  iApply step_fupd_intro; [done|]; iModIntro.
150 151 152 153 154 155
  iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "[-Hφ]").
  { iApply (@wptp_strong_adequacy _ _ (IrisG _ _ Hinv stateI fork_post) _ []
    with "[Hσ] Hwp"); eauto; by rewrite right_id_L. }
  iIntros "Hpost". iDestruct "Hpost" as (e2 t2' ->) "(? & ? & ? & ?)".
  iApply fupd_plain_mask_empty.
  iMod ("Hφ" with "[% //] [$] [$] [$] [$]"). done.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Qed.
157

158
(** Since the full adequacy statement is quite a mouthful, we prove some more
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160
intuitive and simpler corollaries. These lemmas are morover stated in terms of
[rtc erased_step] so one does not have to provide the trace. *)
161 162 163 164 165 166 167
Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
    (φ : val Λ  state Λ  Prop) := {
  adequate_result t2 σ2 v2 :
   rtc erased_step ([e1], σ1) (of_val v2 :: t2, σ2)  φ v2 σ2;
  adequate_not_stuck t2 σ2 e2 :
   s = NotStuck 
   rtc erased_step ([e1], σ1) (t2, σ2) 
Amin Timany's avatar
Amin Timany committed
168
   e2  t2  not_stuck e2 σ2
169
}.
170

171 172 173 174
Lemma adequate_alt {Λ} s e1 σ1 (φ : val Λ  state Λ  Prop) :
  adequate s e1 σ1 φ   t2 σ2,
    rtc erased_step ([e1], σ1) (t2, σ2) 
      ( v2 t2', t2 = of_val v2 :: t2'  φ v2 σ2) 
Amin Timany's avatar
Amin Timany committed
175
      ( e2, s = NotStuck  e2  t2  not_stuck e2 σ2).
176 177
Proof. split. intros []; naive_solver. constructor; naive_solver. Qed.

178 179 180 181
Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
  adequate NotStuck e1 σ1 φ 
  rtc erased_step ([e1], σ1) (t2, σ2) 
  Forall (λ e, is_Some (to_val e)) t2   t3 σ3, erased_step (t2, σ2) (t3, σ3).
182
Proof.
183 184 185 186 187 188 189 190
  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).
  destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(κ&e3&σ3&efs&?)];
    rewrite ?eq_None_not_Some; auto.
  { exfalso. eauto. }
  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
  right; exists (t2' ++ e3 :: t2'' ++ efs), σ3, κ; econstructor; eauto.
191 192
Qed.

193 194
Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
  ( `{Hinv : !invG Σ} κs,
195
     (|={}=> 
196
         (stateI : state Λ  list (observation Λ)  iProp Σ)
197
         (fork_post : val Λ  iProp Σ),
198 199 200
       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) fork_post in
       stateI σ κs  WP e @ s;  {{ v, ⌜φ v }})%I) 
  adequate s e σ (λ v _, φ v).
201
Proof.
202 203 204
  intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
  eapply (wp_strong_adequacy Σ _); [|done]=> ?.
  iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
Ralf Jung's avatar
Ralf Jung committed
205
  iExists s, (λ σ κs _, stateI σ κs), (λ v, ⌜φ v%I), fork_post.
206 207 208
  iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ?) "_ H _".
  iApply fupd_mask_weaken; [done|]. iSplit; [|done].
  iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
209
Qed.
210

211
Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
212
  ( `{Hinv : !invG Σ} κs,
213 214
     (|={}=> 
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
215
         (fork_post : val Λ  iProp Σ),
Robbert Krebbers's avatar
Robbert Krebbers committed
216
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
217
       stateI σ1 κs 0  WP e1 @ s;  {{ _, True }} 
218
       (stateI σ2 [] (pred (length t2)) -  E, |={,E}=> ⌜φ⌝))%I) 
219
  rtc erased_step ([e1], σ1) (t2, σ2) 
220 221
  φ.
Proof.
222 223 224
  intros Hwp [n [κs ?]]%erased_steps_nsteps.
  eapply (wp_strong_adequacy Σ _); [|done]=> ?.
  iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
Ralf Jung's avatar
Ralf Jung committed
225
  iExists s, stateI, (λ _, True)%I, fork_post.
226
  iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _) "Hσ _ _ /=".
227
  iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
228
  by iApply fupd_mask_weaken; first set_solver.
229
Qed.