adequacy.v 8.34 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2 3
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic Require Import big_op soundness.
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 32 33 34 35 36
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).
  rewrite /wsat /ownE; iFrame.
  iExists . rewrite fmap_empty big_sepM_empty. by iFrame.
Qed.

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

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

67
Notation world σ := (wsat  ownE   state_interp σ)%I.
68

69
Notation wptp t := ([ list] ef  t, WP ef {{ _, True }})%I.
70

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

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

Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ :
  nsteps step n (e1 :: t1, σ1) (t2, σ2) 
99
  world σ1  WP e1 {{ Φ }}  wptp t1 
100
  Nat.iter (S n) (λ P, |==>  P) ( e2 t2',
Ralf Jung's avatar
Ralf Jung committed
101
    t2 = e2 :: t2'  world σ2  WP e2 {{ Φ }}  wptp t2').
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Proof.
103 104 105
  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']].
106 107
  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
108
Qed.
109

110
Instance bupd_iter_mono n : Proper (() ==> ()) (Nat.iter n (λ P, |==>  P)%I).
111 112
Proof. intros P Q HP. induction n; simpl; do 2?f_equiv; auto. Qed.

113
Lemma bupd_iter_frame_l n R Q :
114
  R  Nat.iter n (λ P, |==>  P) Q  Nat.iter n (λ P, |==>  P) (R  Q).
115 116
Proof.
  induction n as [|n IH]; simpl; [done|].
117
  by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
118 119
Qed.

120 121
Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
  nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) 
Ralf Jung's avatar
Ralf Jung committed
122 123
  world σ1  WP e1 {{ v, ⌜φ v }}  wptp t1 
  Nat.iter (S (S n)) (λ P, |==>  P) ⌜φ v2.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Proof.
Ralf Jung's avatar
Ralf Jung committed
125
  intros. rewrite wptp_steps //.
126
  rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
127
  iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq.
128
  iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
129
  iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Qed.
Ralf Jung's avatar
Ralf Jung committed
131

132
Lemma wp_safe e σ Φ :
Ralf Jung's avatar
Ralf Jung committed
133
  world σ  WP e {{ Φ }} ==  is_Some (to_val e)  reducible e σ⌝.
134
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136
  rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) H]".
  destruct (to_val e) as [v|] eqn:?; [eauto 10|].
137
  rewrite fupd_eq. iMod ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
138
  eauto 10.
139
Qed.
Ralf Jung's avatar
Ralf Jung committed
140

141 142
Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
  nsteps step n (e1 :: t1, σ1) (t2, σ2)  e2  t2 
143
  world σ1  WP e1 {{ Φ }}  wptp t1 
Ralf Jung's avatar
Ralf Jung committed
144
  Nat.iter (S (S n)) (λ P, |==>  P) is_Some (to_val e2)  reducible e2 σ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof.
146
  intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
147 148
  iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
  apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
149
  iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Qed.
151

Robbert Krebbers's avatar
Robbert Krebbers committed
152
Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
153
  nsteps step n (e1 :: t1, σ1) (t2, σ2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  (state_interp σ2 ={,}= ⌜φ⌝)  world σ1  WP e1 {{ Φ }}  wptp t1
155
   Nat.iter (S (S n)) (λ P, |==>  P) ⌜φ⌝.
156
Proof.
157 158
  intros ?. rewrite wptp_steps //.
  rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l. apply bupd_iter_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  iIntros "[Hback H]".
160
  iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
161
  rewrite fupd_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
  iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
163
Qed.
164
End adequacy.
Ralf Jung's avatar
Ralf Jung committed
165

166
Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
167 168 169 170
  ( `{Hinv : invG Σ},
     True ={}=  stateI : state Λ  iProp Σ,
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
       stateI σ  WP e {{ v, ⌜φ v }}) 
171
  adequate e σ φ.
Ralf Jung's avatar
Ralf Jung committed
172
Proof.
173 174
  intros Hwp; split.
  - intros t2 σ2 v2 [n ?]%rtc_nsteps.
175
    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
176 177 178 179 180
    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
    iDestruct "Hwp" as (Istate) "[HI Hwp]".
    iModIntro. iNext. iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto.
    iFrame. by iApply big_sepL_nil.
181
  - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
182
    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
183 184 185 186 187
    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
    iDestruct "Hwp" as (Istate) "[HI Hwp]".
    iModIntro. iNext. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto.
    iFrame. by iApply big_sepL_nil.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Qed.
189

190
Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ Φ :
191 192 193
  ( `{Hinv : invG Σ},
     True ={}=  stateI : state Λ  iProp Σ,
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
Robbert Krebbers's avatar
Robbert Krebbers committed
194
       stateI σ1  WP e {{ Φ }}  (stateI σ2 ={,}= ⌜φ⌝)) 
195
  rtc step ([e], σ1) (t2, σ2) 
196
  φ.
197
Proof.
198
  intros Hwp [n ?]%rtc_nsteps.
199
  eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
200 201
  rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
  rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203 204
  iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
  iModIntro. iNext. iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto.
  iFrame "Hw HE Hwp HIstate Hclose". by iApply big_sepL_nil.
205
Qed.