Robbert Krebbers committed Aug 05, 2016 1 2 ``````From iris.program_logic Require Export weakestpre. From iris.algebra Require Import gmap auth agree gset coPset upred_big_op. `````` Ralf Jung committed Oct 12, 2016 3 ``````From iris.program_logic Require Import wsat. `````` Robbert Krebbers committed Oct 05, 2016 4 ``````From iris.proofmode Require Import tactics. `````` Robbert Krebbers committed Aug 05, 2016 5 ``````Import uPred. `````` Robbert Krebbers committed Jan 20, 2016 6 `````` `````` Robbert Krebbers committed Aug 05, 2016 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). `````` Robbert Krebbers committed Aug 08, 2016 23 `````` destruct (adequate_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)]; `````` Robbert Krebbers committed Aug 05, 2016 24 25 26 `````` rewrite ?eq_None_not_Some; auto. { exfalso. eauto. } destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto. `````` Robbert Krebbers committed Aug 08, 2016 27 `````` right; exists (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto. `````` Robbert Krebbers committed Aug 05, 2016 28 29 ``````Qed. `````` Robbert Krebbers committed Jan 20, 2016 30 ``````Section adequacy. `````` Robbert Krebbers committed Aug 05, 2016 31 ``````Context `{irisG Λ Σ}. `````` Robbert Krebbers committed Feb 01, 2016 32 ``````Implicit Types e : expr Λ. `````` Robbert Krebbers committed Aug 05, 2016 33 34 35 ``````Implicit Types P Q : iProp Σ. Implicit Types Φ : val Λ → iProp Σ. Implicit Types Φs : list (val Λ → iProp Σ). `````` Robbert Krebbers committed Jan 20, 2016 36 `````` `````` Robbert Krebbers committed Aug 05, 2016 37 38 ``````Notation world σ := (wsat ★ ownE ⊤ ★ ownP_auth σ)%I. `````` Robbert Krebbers committed Aug 28, 2016 39 ``````Notation wptp t := ([★ list] ef ∈ t, WP ef {{ _, True }})%I. `````` Robbert Krebbers committed Aug 05, 2016 40 `````` `````` Robbert Krebbers committed Aug 08, 2016 41 42 ``````Lemma wp_step e1 σ1 e2 σ2 efs Φ : prim_step e1 σ1 e2 σ2 efs → `````` Robbert Krebbers committed Aug 28, 2016 43 `````` world σ1 ★ WP e1 {{ Φ }} =r=> ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp efs). `````` Robbert Krebbers committed Aug 05, 2016 44 45 46 47 ``````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. `````` Robbert Krebbers committed Aug 05, 2016 48 `````` iVs ("H" \$! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame. `````` Robbert Krebbers committed Aug 05, 2016 49 `````` iVsIntro; iNext. `````` Robbert Krebbers committed Aug 08, 2016 50 `````` iVs ("H" \$! e2 σ2 efs with "[%] [Hw HE]") `````` Robbert Krebbers committed Aug 05, 2016 51 `````` as ">(\$ & \$ & \$ & \$)"; try iFrame; eauto. `````` Robbert Krebbers committed Aug 05, 2016 52 53 54 55 56 57 58 59 ``````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)". `````` Robbert Krebbers committed Aug 08, 2016 60 61 `````` destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=. - iExists e2', (t2' ++ efs); iSplitR; first eauto. `````` Robbert Krebbers committed Aug 28, 2016 62 `````` rewrite big_sepL_app. iFrame "Ht". iApply wp_step; try iFrame; eauto. `````` Robbert Krebbers committed Aug 08, 2016 63 `````` - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto. `````` Robbert Krebbers committed Aug 28, 2016 64 `````` rewrite !big_sepL_app !big_sepL_cons big_sepL_app. `````` Robbert Krebbers committed Aug 05, 2016 65 66 67 68 69 70 71 72 73 `````` 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 committed Jan 20, 2016 74 ``````Proof. `````` Robbert Krebbers committed Aug 05, 2016 75 76 77 78 `````` 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. `````` Robbert Krebbers committed Aug 05, 2016 79 `````` iVsIntro; iNext; iVs "H" as ">?". by iApply IH. `````` Robbert Krebbers committed Jan 20, 2016 80 ``````Qed. `````` Robbert Krebbers committed Aug 05, 2016 81 82 83 84 `````` 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. `````` Robbert Krebbers committed Aug 23, 2016 85 86 87 88 89 90 91 ``````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. `````` Robbert Krebbers committed Aug 05, 2016 92 93 94 95 ``````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 committed Jan 20, 2016 96 ``````Proof. `````` Ralf Jung committed Aug 08, 2016 97 98 `````` intros. rewrite wptp_steps //. rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono. `````` Robbert Krebbers committed Aug 05, 2016 99 100 `````` iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq. iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def. `````` Robbert Krebbers committed Aug 05, 2016 101 `````` iVs ("H" with "[Hw HE]") as ">(_ & _ & \$)"; iFrame; auto. `````` Robbert Krebbers committed Jan 20, 2016 102 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 103 `````` `````` Robbert Krebbers committed Aug 05, 2016 104 105 ``````Lemma wp_safe e σ Φ : world σ ★ WP e {{ Φ }} =r=> ▷ ■ (is_Some (to_val e) ∨ reducible e σ). `````` Ralf Jung committed Jan 25, 2016 106 ``````Proof. `````` Robbert Krebbers committed Aug 05, 2016 107 108 `````` rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]". { iDestruct "H" as (v) "[% _]"; eauto 10. } `````` Robbert Krebbers committed Aug 05, 2016 109 110 `````` rewrite pvs_eq. iVs ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame. eauto 10. `````` Ralf Jung committed Jan 25, 2016 111 ``````Qed. `````` Ralf Jung committed Mar 07, 2016 112 `````` `````` Robbert Krebbers committed Aug 05, 2016 113 114 115 116 ``````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 committed Jan 20, 2016 117 ``````Proof. `````` Robbert Krebbers committed Aug 08, 2016 118 `````` intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono. `````` Robbert Krebbers committed Aug 05, 2016 119 120 `````` 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"). `````` Robbert Krebbers committed Aug 28, 2016 121 `````` iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp"). `````` Robbert Krebbers committed Jan 20, 2016 122 ``````Qed. `````` Robbert Krebbers committed Aug 23, 2016 123 `````` `````` Robbert Krebbers committed Aug 23, 2016 124 ``````Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ : `````` Robbert Krebbers committed Aug 23, 2016 125 126 `````` nsteps step n (e1 :: t1, σ1) (t2, σ2) → (I ={⊤,∅}=> ∃ σ', ownP σ' ∧ ■ φ σ') → `````` Robbert Krebbers committed Aug 23, 2016 127 `````` I ★ world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢ `````` Robbert Krebbers committed Aug 23, 2016 128 129 `````` Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ φ σ2). Proof. `````` Robbert Krebbers committed Aug 23, 2016 130 `````` intros ? HI. rewrite wptp_steps //. `````` Robbert Krebbers committed Aug 23, 2016 131 132 133 134 135 136 `````` 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 %]". `````` Robbert Krebbers committed Sep 09, 2016 137 `````` iDestruct (ownP_agree σ2 σ2' with "[-]") as %<-. by iFrame. eauto. `````` Robbert Krebbers committed Aug 23, 2016 138 ``````Qed. `````` Robbert Krebbers committed Aug 05, 2016 139 ``````End adequacy. `````` Ralf Jung committed Mar 07, 2016 140 `````` `````` Robbert Krebbers committed Aug 05, 2016 141 142 143 ``````Theorem wp_adequacy Σ `{irisPreG Λ Σ} e σ φ : (∀ `{irisG Λ Σ}, ownP σ ⊢ WP e {{ v, ■ φ v }}) → adequate e σ φ. `````` Ralf Jung committed Mar 07, 2016 144 ``````Proof. `````` Robbert Krebbers committed Aug 05, 2016 145 146 147 148 149 `````` 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. `````` Robbert Krebbers committed Aug 28, 2016 150 `````` iFrame. iSplitL. by iApply Hwp. by iApply big_sepL_nil. `````` Robbert Krebbers committed Aug 05, 2016 151 152 153 154 `````` - 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. `````` Robbert Krebbers committed Aug 28, 2016 155 `````` iFrame "Hw HE Hσ". iSplitL. by iApply Hwp. by iApply big_sepL_nil. `````` Robbert Krebbers committed Jan 20, 2016 156 ``````Qed. `````` Robbert Krebbers committed Aug 23, 2016 157 `````` `````` Robbert Krebbers committed Aug 23, 2016 158 159 ``````Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ : (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=> I ★ WP e {{ Φ }}) → `````` Robbert Krebbers committed Aug 23, 2016 160 161 162 163 `````` (∀ `{irisG Λ Σ}, I ={⊤,∅}=> ∃ σ', ownP σ' ∧ ■ φ σ') → rtc step ([e], σ1) (t2, σ2) → φ σ2. Proof. `````` Robbert Krebbers committed Aug 23, 2016 164 `````` intros Hwp HI [n ?]%rtc_nsteps. `````` Robbert Krebbers committed Aug 23, 2016 165 166 167 168 `````` 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. `````` Robbert Krebbers committed Aug 28, 2016 169 `````` iVsIntro. iNext. iApply wptp_invariance; eauto. iFrame. by iApply big_sepL_nil. `````` Robbert Krebbers committed Aug 23, 2016 170 ``Qed.``