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