adequacy.v 9.78 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
10
11
(* Global functor setup *)
Definition invΣ : gFunctors :=
  #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
12
13
    GFunctor coPset_disjUR;
    GFunctor (gset_disjUR positive)].
14
15
16
17
18
19
20
21

Class invPreG (Σ : gFunctors) : Set := WsatPreG {
  inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
  enabled_inPreG :> inG Σ coPset_disjR;
  disabled_inPreG :> inG Σ (gset_disjR positive);
}.

Instance subG_invΣ {Σ} : subG invΣ Σ  invPreG Σ.
22
Proof. solve_inG. Qed.
23
24

(* Allocation *)
25
Lemma wsat_alloc `{invPreG Σ} : (|==>  _ : invG Σ, wsat  ownE )%I.
26
27
28
29
30
31
Proof.
  iIntros.
  iMod (own_alloc ( ( : gmap _ _))) as (γI) "HI"; first done.
  iMod (own_alloc (CoPset )) as (γE) "HE"; first done.
  iMod (own_alloc (GSet )) as (γD) "HD"; first done.
  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  rewrite /wsat /ownE -lock; iFrame.
33
  iExists . rewrite fmap_empty big_opM_empty. by iFrame.
34
35
36
Qed.

(* Program logic adequacy *)
37
38
Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
    (φ : val Λ  state Λ  Prop) := {
39
  adequate_result t2 σ2 v2 :
40
   rtc step ([e1], σ1) (of_val v2 :: t2, σ2)  φ v2 σ2;
41
  adequate_not_stuck t2 σ2 e2 :
Ralf Jung's avatar
Ralf Jung committed
42
   s = NotStuck 
43
44
45
46
47
   rtc step ([e1], σ1) (t2, σ2) 
   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
48
  adequate NotStuck e1 σ1 φ 
49
50
51
52
53
54
  rtc step ([e1], σ1) (t2, σ2) 
  Forall (λ e, is_Some (to_val e)) t2   t3 σ3, step (t2, σ2) (t3, σ3).
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).
55
  destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
56
57
58
    rewrite ?eq_None_not_Some; auto.
  { exfalso. eauto. }
  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
59
  right; exists (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
60
61
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
62
Section adequacy.
63
Context `{irisG Λ Σ}.
64
Implicit Types e : expr Λ.
65
66
67
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types Φs : list (val Λ  iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
68

69
70
Notation world' E σ := (wsat  ownE E  state_interp σ)%I (only parsing).
Notation world σ := (world'  σ) (only parsing).
71

72
Notation wptp s t := ([ list] ef  t, WP ef @ s;  {{ _, True }})%I.
73

74
Lemma wp_step s E e1 σ1 e2 σ2 efs Φ :
75
  prim_step e1 σ1 e2 σ2 efs 
76
77
  world' E σ1  WP e1 @ s; E {{ Φ }}
  ==  |==>  (world' E σ2  WP e2 @ s; E {{ Φ }}  wptp s efs).
78
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
80
  rewrite (val_stuck e1 σ1 e2 σ2 efs) // uPred_fupd_eq.
81
  iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
82
83
  iMod ("H" $! e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
  iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
84
85
Qed.

86
Lemma wptp_step s e1 t1 t2 σ1 σ2 Φ :
87
  step (e1 :: t1,σ1) (t2, σ2) 
88
89
  world σ1  WP e1 @ s;  {{ Φ }}  wptp s t1
  ==  e2 t2', t2 = e2 :: t2'   |==>  (world σ2  WP e2 @ s;  {{ Φ }}  wptp s t2').
90
91
Proof.
  iIntros (Hstep) "(HW & He & Ht)".
92
93
  destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
  - iExists e2', (t2' ++ efs); iSplitR; first eauto.
94
    iFrame "Ht". iApply wp_step; eauto with iFrame.
95
  - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
96
97
    iDestruct "Ht" as "($ & He' & $)". iFrame "He".
    iApply wp_step; eauto with iFrame.
98
99
Qed.

100
Lemma wptp_steps s n e1 t1 t2 σ1 σ2 Φ :
101
  nsteps step n (e1 :: t1, σ1) (t2, σ2) 
102
  world σ1  WP e1 @ s;  {{ Φ }}  wptp s t1 
103
  Nat.iter (S n) (λ P, |==>  P) ( e2 t2',
104
    t2 = e2 :: t2'  world σ2  WP e2 @ s;  {{ Φ }}  wptp s t2').
Robbert Krebbers's avatar
Robbert Krebbers committed
105
Proof.
106
107
108
  revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
  { inversion_clear 1; iIntros "?"; eauto 10. }
  iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
109
110
  iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
  iModIntro; iNext; iMod "H" as ">?". by iApply IH.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
Qed.
112

113
114
115
116
117
Lemma bupd_iter_laterN_mono n P Q `{!Plain Q} :
  (P  Q)  Nat.iter n (λ P, |==>  P)%I P  ^n Q.
Proof.
  intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_plain.
Qed.
118

119
Lemma bupd_iter_frame_l n R Q :
120
  R  Nat.iter n (λ P, |==>  P) Q  Nat.iter n (λ P, |==>  P) (R  Q).
121
122
Proof.
  induction n as [|n IH]; simpl; [done|].
123
  by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
124
125
Qed.

126
Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ :
127
  nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) 
128
129
  world σ1  WP e1 @ s;  {{ v,  σ, state_interp σ ={,}= ⌜φ v σ⌝ }}  wptp s t1
   ^(S (S n)) ⌜φ v2 σ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Proof.
131
  intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
132
  iDestruct 1 as (e2 t2' ?) "((Hw & HE & Hσ) & H & _)"; simplify_eq.
133
  iDestruct (wp_value_inv' with "H") as "H". rewrite uPred_fupd_eq.
134
135
  iMod ("H" with "[$]") as ">(Hw & HE & H)".
  iMod ("H" with "Hσ [$]") as ">(_ & _ & $)".
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Qed.
Ralf Jung's avatar
Ralf Jung committed
137

138
Lemma wp_safe E e σ Φ :
139
  world' E σ - WP e @ E {{ Φ }} ==  is_Some (to_val e)  reducible e σ⌝.
140
Proof.
141
  rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
142
143
  destruct (to_val e) as [v|] eqn:?.
  { iIntros "!> !> !%". left. by exists v. }
144
  rewrite uPred_fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
145
  iIntros "!> !> !%". by right.
146
Qed.
Ralf Jung's avatar
Ralf Jung committed
147

148
149
Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
  nsteps step n (e1 :: t1, σ1) (t2, σ2)  e2  t2 
Ralf Jung's avatar
Ralf Jung committed
150
  world σ1  WP e1 {{ Φ }}  wptp NotStuck t1
151
   ^(S (S n)) is_Some (to_val e2)  reducible e2 σ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof.
153
  intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
154
  iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
155
156
157
  apply elem_of_cons in He2 as [<-|?].
  - iMod (wp_safe with "Hw H") as "$".
  - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Qed.
159

160
Lemma wptp_invariance s n e1 e2 t1 t2 σ1 σ2 φ Φ :
161
  nsteps step n (e1 :: t1, σ1) (t2, σ2) 
162
  (state_interp σ2 ={,}= ⌜φ⌝)  world σ1  WP e1 @ s;  {{ Φ }}  wptp s t1
163
   ^(S (S n)) ⌜φ⌝.
164
Proof.
165
166
167
  intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
  apply: bupd_iter_laterN_mono.
  iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
168
  rewrite uPred_fupd_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
170
Qed.
171
End adequacy.
Ralf Jung's avatar
Ralf Jung committed
172

173
Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
174
  ( `{Hinv : invG Σ},
Robbert Krebbers's avatar
Robbert Krebbers committed
175
     (|={}=>  stateI : state Λ  iProp Σ,
176
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
177
       stateI σ  WP e @ s;  {{ v,  σ, stateI σ ={,}= ⌜φ v σ⌝ }})%I) 
178
  adequate s e σ φ.
Ralf Jung's avatar
Ralf Jung committed
179
Proof.
180
181
  intros Hwp; split.
  - intros t2 σ2 v2 [n ?]%rtc_nsteps.
182
    eapply (soundness (M:=iResUR Σ) _ (S (S n))).
183
    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
184
    rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
185
    iDestruct "Hwp" as (Istate) "[HI Hwp]".
186
    iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
187
  - destruct s; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?.
188
    eapply (soundness (M:=iResUR Σ) _ (S (S n))).
189
190
    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
    rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
191
    iDestruct "Hwp" as (Istate) "[HI Hwp]".
192
    iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Qed.
194

195
196
197
198
199
200
201
202
203
204
205
206
207
Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
  ( `{Hinv : invG Σ},
     (|={}=>  stateI : state Λ  iProp Σ,
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
       stateI σ  WP e @ s;  {{ v, ⌜φ v }})%I) 
  adequate s e σ (λ v _, φ v).
Proof.
  intros Hwp. apply (wp_strong_adequacy Σ _)=> Hinv.
  iMod Hwp as (stateI) "[Hσ H]". iExists stateI. iIntros "{$Hσ} !>".
  iApply (wp_wand with "H"). iIntros (v ? σ') "_".
  iMod (fupd_intro_mask'  ) as "_"; auto.
Qed.

208
Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
209
  ( `{Hinv : invG Σ},
Robbert Krebbers's avatar
Robbert Krebbers committed
210
     (|={}=>  stateI : state Λ  iProp Σ,
211
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
212
       stateI σ1  WP e @ s;  {{ _, True }}  (stateI σ2 ={,}= ⌜φ⌝))%I) 
213
  rtc step ([e], σ1) (t2, σ2) 
214
  φ.
215
Proof.
216
  intros Hwp [n ?]%rtc_nsteps.
217
  eapply (soundness (M:=iResUR Σ) _ (S (S n))).
218
219
  iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
  rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
221
  iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
222
Qed.
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239

(* 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 φ :
  ( `{Hinv : invG Σ},
     (|={}=>  stateI : state Λ  iProp Σ,
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
       stateI σ1  WP e @ s;  {{ _, True }}  (stateI σ2 -  E, |={,E}=> ⌜φ⌝))%I) 
  rtc step ([e], σ1) (t2, σ2) 
  φ.
Proof.
  intros Hwp. eapply wp_invariance; first done.
  intros Hinv. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
  iModIntro. iExists stateI. iFrame. iIntros "Hσ".
  iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
  iMod (fupd_intro_mask') as "_"; last by iModIntro. solve_ndisj.
Qed.