adequacy.v 12.4 KB
Newer Older
1
From iris.algebra Require Import gmap auth agree gset coPset.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.proofmode Require Import tactics.
3
From iris.base_logic.lib Require Import wsat.
4
From iris.program_logic Require Export weakestpre.
Ralf Jung's avatar
Ralf Jung committed
5
From iris.prelude Require Import options.
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. *)
10

Robbert Krebbers's avatar
Robbert Krebbers committed
11
Section adequacy.
12
Context `{!irisG Λ Σ}.
13
Implicit Types e : expr Λ.
14
15
16
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types Φs : list (val Λ  iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
17

18
Notation wptp s t Φs := ([ list] e;Φ  t;Φs, WP e @ s;  {{ Φ }})%I.
19

20
Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
21
  prim_step e1 σ1 κ e2 σ2 efs 
22
23
24
  state_interp σ1 ns (κ ++ κs) nt - WP e1 @ s;  {{ Φ }}
    ={,}= |={}=>^(S $ num_laters_per_step ns) |={,}=>
    state_interp σ2 (S ns) κs (nt + length efs)  WP e2 @ s;  {{ Φ }} 
25
    wptp s efs (replicate (length efs) fork_post).
26
Proof.
27
  rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
28
  rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
29
30
  iMod ("H" $! σ1 ns with "Hσ") as "(_ & H)". iModIntro.
  iApply (step_fupdN_wand with "[H]"); first by iApply "H". iIntros ">H".
31
  by rewrite Nat.add_comm big_sepL2_replicate_r.
32
33
Qed.

34
Lemma wptp_step s es1 es2 κ κs σ1 ns σ2 Φs nt :
35
  step (es1,σ1) κ (es2, σ2) 
36
37
38
  state_interp σ1 ns (κ ++ κs) nt - wptp s es1 Φs -
   nt', |={,}=> |={}=>^(S $ num_laters_per_step$ ns) |={,}=>
         state_interp σ2 (S ns) κs (nt + nt') 
39
         wptp s es2 (Φs ++ replicate nt' fork_post).
40
Proof.
41
42
43
44
  iIntros (Hstep) "Hσ Ht".
  destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq/=.
  iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ->) "[? Ht]".
  iDestruct (big_sepL2_cons_inv_l with "Ht") as (Φ Φs3 ->) "[Ht ?]".
45
46
  iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done. iModIntro.
  iApply (step_fupdN_wand with "H"). iIntros ">($ & He2 & Hefs) !>".
47
  rewrite -(assoc_L app) -app_comm_cons. iFrame.
48
49
Qed.

50
51
52
53
54
55
56
57
58
59
(* The total number of laters used between the physical steps number
   [start] (included) to [start+ns] (excluded). *)
Local Fixpoint steps_sum (num_laters_per_step : nat  nat) (start ns : nat) : nat :=
  match ns with
  | O => 0
  | S ns =>
    S $ num_laters_per_step start + steps_sum num_laters_per_step (S start) ns
  end.

Lemma wptp_steps s n es1 es2 κs κs' σ1 ns σ2 Φs nt :
60
  nsteps n (es1, σ1) κs (es2, σ2) 
61
62
63
64
  state_interp σ1 ns (κs ++ κs') nt - wptp s es1 Φs
  ={,}= |={}=>^(steps_sum num_laters_per_step ns n) |={,}=>  nt',
    state_interp σ2 (n + ns) κs' (nt + nt') 
    wptp s es2 (Φs ++ replicate nt' fork_post).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof.
66
67
  revert nt es1 es2 κs κs' σ1 ns σ2 Φs.
  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 ns σ2 Φs /=.
68
  { inversion_clear 1; iIntros "? ?"; iExists 0=> /=.
69
    rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_mask_subseteq. }
70
  iIntros (Hsteps) "Hσ He". inversion_clear Hsteps as [|?? [t1' σ1']].
71
  rewrite -(assoc_L (++)) Nat_iter_add plus_n_Sm.
72
  iDestruct (wptp_step with "Hσ He") as (nt') ">H"; first eauto; simplify_eq.
73
74
75
76
77
  iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
  iIntros ">(Hσ & He)". iMod (IH with "Hσ He") as "IH"; first done. iModIntro.
  iApply (step_fupdN_wand with "IH"). iIntros ">IH".
  iDestruct "IH" as (nt'') "[??]".
  rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus. by eauto with iFrame.
78
79
Qed.

80
81
Lemma wp_not_stuck κs nt e σ ns Φ :
  state_interp σ ns κs nt - WP e {{ Φ }} ={}= not_stuck e σ⌝.
82
Proof.
Amin Timany's avatar
Amin Timany committed
83
  rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
84
  destruct (to_val e) as [v|] eqn:?; first by eauto.
85
  iSpecialize ("H" $! σ ns [] κs with "Hσ"). rewrite sep_elim_l.
86
  iMod (fupd_plain_mask with "H") as %?; eauto.
87
Qed.
Ralf Jung's avatar
Ralf Jung committed
88

89
Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 ns σ2 nt:
90
  nsteps n (es1, σ1) κs (es2, σ2) 
91
92
  state_interp σ1 ns (κs ++ κs') nt - wptp s es1 Φs
  ={,}= |={}=>^(steps_sum num_laters_per_step ns n) |={,}=>  nt',
93
      e2, s = NotStuck  e2  es2  not_stuck e2 σ2  
94
    state_interp σ2 (n + ns) κs' (nt + nt') 
95
    [ list] e;Φ  es2;Φs ++ replicate nt' fork_post, from_option Φ True (to_val e).
96
Proof.
97
98
99
  iIntros (Hstep) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
  iModIntro. iApply (step_fupdN_wand with "Hwp").
  iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
100
  iMod (fupd_plain_keep_l 
101
      e2, s = NotStuck  e2  es2  not_stuck e2 σ2 %I
102
103
    (state_interp σ2 (n + ns) κs' (nt + nt') 
     wptp s es2 (Φs ++ replicate nt' fork_post))%I
104
105
106
107
108
109
110
111
112
113
114
    with "[$Hσ $Ht]") as "(%&Hσ&Hwp)".
  { iIntros "(Hσ & Ht)" (e' -> He').
    move: He' => /(elem_of_list_split _ _)[?[?->]].
    iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ?) "[? Hwp]".
    iDestruct (big_sepL2_cons_inv_l with "Hwp") as (Φ Φs3 ->) "[Hwp ?]".
    iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto. }
  iExists _. iSplitR; first done. iFrame "Hσ".
  iApply big_sepL2_fupd.
  iApply (big_sepL2_impl with "Hwp").
  iIntros "!#" (? e Φ ??) "Hwp".
  destruct (to_val e) as [v2|] eqn:He2'; last done.
115
  apply of_to_val in He2' as <-. simpl. iApply wp_value_fupd'. done.
116
Qed.
117
End adequacy.
Ralf Jung's avatar
Ralf Jung committed
118

119
(** Iris's generic adequacy result *)
120
121
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} es σ1 n κs t2 σ2 φ
        (num_laters_per_step : nat  nat) :
122
  ( `{Hinv : !invG Σ},
Gregory Malecha's avatar
Gregory Malecha committed
123
     |={}=> 
124
         (s: stuckness)
125
         (stateI : state Λ  nat  list (observation Λ)  nat  iProp Σ)
126
         (Φs : list (val Λ  iProp Σ))
127
         (fork_post : val Λ  iProp Σ)
128
129
         (* Note: existentially quantifying over Iris goal! [iExists _] should
         usually work. *)
130
131
132
133
134
         state_interp_mono,
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post num_laters_per_step
                                  state_interp_mono
       in
       stateI σ1 0 κs 0 
135
136
137
138
139
140
       ([ list] e;Φ  es;Φs, WP e @ s;  {{ Φ }}) 
       ( es' t2',
         (* es' is the final state of the initial threads, t2' the rest *)
          t2 = es' ++ t2'  -
         (* es' corresponds to the initial threads *)
          length es' = length es  -
141
         (* If this is a stuck-free triple (i.e. [s = NotStuck]), then all
142
143
         threads in [t2] are not stuck *)
           e2, s = NotStuck  e2  t2  not_stuck e2 σ2  -
144
         (* The state interpretation holds for [σ2] *)
145
         stateI σ2 n [] (length t2') -
146
147
148
149
         (* If the initial threads are done, their post-condition [Φ] holds *)
         ([ list] e;Φ  es';Φs, from_option Φ True (to_val e)) -
         (* For all forked-off threads that are done, their postcondition
            [fork_post] holds. *)
150
151
152
         ([ 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,
Ralf Jung's avatar
Ralf Jung committed
153
         one can use [fupd_mask_subseteq] to introduce the fancy update. *)
Gregory Malecha's avatar
Gregory Malecha committed
154
         |={,}=>  φ )) 
155
  nsteps n (es, σ1) κs (t2, σ2) 
156
157
  (* Then we can conclude [φ] at the meta-level. *)
  φ.
Ralf Jung's avatar
Ralf Jung committed
158
Proof.
159
  intros Hwp ?.
160
161
  apply (step_fupdN_soundness _ (steps_sum num_laters_per_step 0 n))=> Hinv.
  iMod Hwp as (s stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
162
  iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
163
164
165
166
167
168
169
170
  iMod (@wptp_strong_adequacy _ _
       (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
    with "[Hσ] Hwp") as "H"; [done|by rewrite right_id_L|].
  iAssert (|={}=>^(steps_sum num_laters_per_step 0 n) |={}=> ⌜φ⌝)%I
    with "[-]" as "H"; last first.
  { destruct steps_sum; [done|]. by iApply step_fupdN_S_fupd. }
  iApply (step_fupdN_wand with "H").
  iMod 1 as (nt' ?) "(Hσ & Hval) /=".
171
172
173
174
  iDestruct (big_sepL2_app_inv_r with "Hval") as (es' t2' ->) "[Hes' Ht2']".
  iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
  rewrite replicate_length in Hlen2; subst.
  iDestruct (big_sepL2_length with "Hes'") as %Hlen3.
175
  rewrite -plus_n_O.
176
177
  iApply ("Hφ" with "[//] [%] [//] Hσ Hes'"); [congruence|].
  by rewrite big_sepL2_replicate_r // big_sepL_omap.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
Qed.
179

180
(** Since the full adequacy statement is quite a mouthful, we prove some more
Robbert Krebbers's avatar
Robbert Krebbers committed
181
182
intuitive and simpler corollaries. These lemmas are morover stated in terms of
[rtc erased_step] so one does not have to provide the trace. *)
183
184
185
186
187
188
189
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
190
   e2  t2  not_stuck e2 σ2
191
}.
192

193
194
195
196
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
197
      ( e2, s = NotStuck  e2  t2  not_stuck e2 σ2).
Tej Chajed's avatar
Tej Chajed committed
198
199
200
201
202
Proof.
  split.
  - intros []; naive_solver.
  - constructor; naive_solver.
Qed.
203

204
205
206
207
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).
208
Proof.
209
210
211
212
213
214
215
216
  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.
217
218
Qed.

219
220
221
222
223
224
225
226
227
228
229
230
231
(** This simpler form of adequacy requires the [irisG] instance that you use
everywhere to syntactically be of the form
{|
  iris_invG := ...;
  state_interp σ _ κs _ := ...;
  fork_post v := ...;
  num_laters_per_step _ := 0;
  state_interp_mono _ _ _ _ := fupd_intro _ _;
|}
In other words, the state interpretation must ignore [ns] and [nt], the number
of laters per step must be 0, and the proof of [state_interp_mono] must have
this specific proof term.
*)
232
233
Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
  ( `{Hinv : !invG Σ} κs,
Gregory Malecha's avatar
Gregory Malecha committed
234
      |={}=> 
235
         (stateI : state Λ  list (observation Λ)  iProp Σ)
236
         (fork_post : val Λ  iProp Σ),
237
238
239
240
       let _ : irisG Λ Σ :=
           IrisG _ _ Hinv (λ σ _ κs _, stateI σ κs) fork_post (λ _, 0)
                 (λ _ _ _ _, fupd_intro _ _)
       in
Gregory Malecha's avatar
Gregory Malecha committed
241
       stateI σ κs  WP e @ s;  {{ v, ⌜φ v }}) 
242
  adequate s e σ (λ v _, φ v).
243
Proof.
244
245
246
  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]".
247
  iExists s, (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v%I)], fork_post, _ => /=.
248
  iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
249
  iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
250
251
  iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
  iDestruct (big_sepL2_nil_inv_r with "H") as %->.
252
  iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
253
Qed.
254

255
Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
256
  ( `{Hinv : !invG Σ} κs,
Gregory Malecha's avatar
Gregory Malecha committed
257
      |={}=> 
258
         (stateI : state Λ  list (observation Λ)  nat  iProp Σ)
259
         (fork_post : val Λ  iProp Σ),
260
261
       let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ _, stateI σ) fork_post
              (λ _, 0) (λ _ _ _ _, fupd_intro _ _) in
262
       stateI σ1 κs 0  WP e1 @ s;  {{ _, True }} 
Gregory Malecha's avatar
Gregory Malecha committed
263
       (stateI σ2 [] (pred (length t2)) -  E, |={,E}=> ⌜φ⌝)) 
264
  rtc erased_step ([e1], σ1) (t2, σ2) 
265
266
  φ.
Proof.
267
268
269
  intros Hwp [n [κs ?]]%erased_steps_nsteps.
  eapply (wp_strong_adequacy Σ _); [|done]=> ?.
  iMod (Hwp _ κs) as (stateI fork_post) "(Hσ & Hwp & Hφ)".
270
  iExists s, (λ σ _, stateI σ), [(λ _, True)%I], fork_post, _ => /=.
271
272
273
  iIntros "{$Hσ $Hwp} !>" (e2 t2' -> _ _) "Hσ H _ /=".
  iDestruct (big_sepL2_cons_inv_r with "H") as (? ? ->) "[_ H]".
  iDestruct (big_sepL2_nil_inv_r with "H") as %->.
274
  iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
275
  by iApply fupd_mask_intro_discard; first set_solver.
276
Qed.