adequacy.v 7.19 KB
Newer Older
1 2 3 4 5
From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
From iris.program_logic Require Import ownership.
From iris.proofmode Require Import tactics weakestpre.
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
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).
23
  destruct (adequate_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
24 25 26
    rewrite ?eq_None_not_Some; auto.
  { exfalso. eauto. }
  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
27
  right; exists (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
28 29
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
30
Section adequacy.
31
Context `{irisG Λ Σ}.
32
Implicit Types e : expr Λ.
33 34 35
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types Φs : list (val Λ  iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
36

37 38 39 40 41 42 43 44 45
Notation world σ := (wsat  ownE   ownP_auth σ)%I.

Definition wptp (t : list (expr Λ)) := ([] (flip (wp ) (λ _, True) <$> t))%I.

Lemma wptp_cons e t : wptp (e :: t)  WP e {{ _, True }}  wptp t.
Proof. done. Qed.
Lemma wptp_app t1 t2 : wptp (t1 ++ t2)  wptp t1  wptp t2.
Proof. by rewrite /wptp fmap_app big_sep_app. Qed.

46 47 48
Lemma wp_step e1 σ1 e2 σ2 efs Φ :
  prim_step e1 σ1 e2 σ2 efs 
  world σ1  WP e1 {{ Φ }} =r=>  |=r=>  (world σ2  WP e2 {{ Φ }}  wp_fork efs).
49 50 51 52
Proof.
  rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]".
  { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
  rewrite pvs_eq /pvs_def.
53
  iVs ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
54
  iVsIntro; iNext.
55
  iVs ("H" $! e2 σ2 efs with "[%] [Hw HE]")
56
    as ">($ & $ & $ & $)"; try iFrame; eauto.
57 58 59 60 61 62 63 64
Qed.

Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
  step (e1 :: t1,σ1) (t2, σ2) 
  world σ1  WP e1 {{ Φ }}  wptp t1
  =r=>  e2 t2', t2 = e2 :: t2'   |=r=>  (world σ2  WP e2 {{ Φ }}  wptp t2').
Proof.
  iIntros (Hstep) "(HW & He & Ht)".
65 66 67 68 69
  destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
  - iExists e2', (t2' ++ efs); iSplitR; first eauto.
    rewrite wptp_app. iFrame "Ht". iApply wp_step; try iFrame; eauto.
  - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
    rewrite !wptp_app !wptp_cons wptp_app.
70 71 72 73 74 75 76 77 78
    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) 
  world σ1  WP e1 {{ Φ }}  wptp t1 
  Nat.iter (S n) (λ P, |=r=>  P) ( e2 t2',
    t2 = e2 :: t2'  world σ2  WP e2 {{ Φ }}  wptp t2').
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof.
80 81 82 83
  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']].
  iVs (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
84
  iVsIntro; iNext; iVs "H" as ">?". by iApply IH.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Qed.
86 87 88 89

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

90 91 92 93 94 95 96
Lemma rvs_iter_frame_l n R Q :
  R  Nat.iter n (λ P, |=r=>  P) Q  Nat.iter n (λ P, |=r=>  P) (R  Q).
Proof.
  induction n as [|n IH]; simpl; [done|].
  by rewrite rvs_frame_l {1}(later_intro R) -later_sep IH.
Qed.

97 98 99 100
Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
  nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) 
  world σ1  WP e1 {{ v,  φ v }}  wptp t1 
  Nat.iter (S (S n)) (λ P, |=r=>  P) ( φ v2).
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Proof.
Ralf Jung's avatar
Ralf Jung committed
102 103
  intros. rewrite wptp_steps //.
  rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
104 105
  iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq.
  iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def.
106
  iVs ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Qed.
Ralf Jung's avatar
Ralf Jung committed
108

109 110
Lemma wp_safe e σ Φ :
  world σ  WP e {{ Φ }} =r=>   (is_Some (to_val e)  reducible e σ).
111
Proof.
112 113
  rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]".
  { iDestruct "H" as (v) "[% _]"; eauto 10. }
114 115
  rewrite pvs_eq. iVs ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
  eauto 10.
116
Qed.
Ralf Jung's avatar
Ralf Jung committed
117

118 119 120 121
Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
  nsteps step n (e1 :: t1, σ1) (t2, σ2)  e2  t2 
  world σ1  WP e1 {{ Φ }}  wptp t1 
  Nat.iter (S (S n)) (λ P, |=r=>  P) ( (is_Some (to_val e2)  reducible e2 σ2)).
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof.
123
  intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
124 125 126 127
  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").
  iApply wp_safe. iFrame "Hw".
  iApply (big_sep_elem_of with "Htp"); apply elem_of_list_fmap; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Qed.
129

Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ :
131 132
  nsteps step n (e1 :: t1, σ1) (t2, σ2) 
  (I ={,}=>  σ', ownP σ'   φ σ') 
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  I  world σ1  WP e1 {{ Φ }}  wptp t1 
134 135
  Nat.iter (S (S n)) (λ P, |=r=>  P) ( φ σ2).
Proof.
136
  intros ? HI. rewrite wptp_steps //.
137 138 139 140 141 142 143 144
  rewrite (Nat_iter_S_r (S n)) rvs_iter_frame_l. apply rvs_iter_mono.
  iIntros "[HI H]".
  iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
  rewrite pvs_eq in HI;
    iVs (HI with "HI [Hw HE]") as "> (_ & _ & H)"; first by iFrame.
  iDestruct "H" as (σ2') "[Hσf %]".
  iDestruct (ownP_agree σ2 σ2' with "[#]") as %<-. by iFrame. eauto.
Qed.
145
End adequacy.
Ralf Jung's avatar
Ralf Jung committed
146

147 148 149
Theorem wp_adequacy Σ `{irisPreG Λ Σ} e σ φ :
  ( `{irisG Λ Σ}, ownP σ  WP e {{ v,  φ v }}) 
  adequate e σ φ.
Ralf Jung's avatar
Ralf Jung committed
150
Proof.
151 152 153 154 155 156 157 158 159 160 161
  intros Hwp; split.
  - intros t2 σ2 v2 [n ?]%rtc_nsteps.
    eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
    rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(?&?&?&Hσ)".
    iVsIntro. iNext. iApply wptp_result; eauto.
    iFrame. iSplitL; auto. by iApply Hwp.
  - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
    eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
    rewrite Nat_iter_S. iVs (iris_alloc σ) as (?) "(Hw & HE & Hσ & Hσf)".
    iVsIntro. iNext. iApply wptp_safe; eauto.
    iFrame "Hw HE Hσ". iSplitL; auto. by iApply Hwp.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Qed.
163

Robbert Krebbers's avatar
Robbert Krebbers committed
164 165
Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
  ( `{irisG Λ Σ}, ownP σ1 ={}=> I  WP e {{ Φ }}) 
166 167 168 169
  ( `{irisG Λ Σ}, I ={,}=>  σ', ownP σ'   φ σ') 
  rtc step ([e], σ1) (t2, σ2) 
  φ σ2.
Proof.
170
  intros Hwp HI [n ?]%rtc_nsteps.
171 172 173 174 175 176
  eapply (adequacy (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
  rewrite Nat_iter_S. iVs (iris_alloc σ1) as (?) "(Hw & HE & ? & Hσ)".
  rewrite pvs_eq in Hwp.
  iVs (Hwp _ with "Hσ [Hw HE]") as ">(? & ? & ? & ?)"; first by iFrame.
  iVsIntro. iNext. iApply wptp_invariance; eauto. by iFrame.
Qed.