weakestpre.v 10.2 KB
Newer Older
 Robbert Krebbers committed Feb 13, 2016 1 2 ``````From program_logic Require Export pviewshifts. From program_logic Require Import wsat. `````` Robbert Krebbers committed Jan 17, 2016 3 4 5 ``````Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of. Local Hint Extern 100 (_ ∉ _) => solve_elem_of. `````` Robbert Krebbers committed Feb 10, 2016 6 ``````Local Hint Extern 100 (@subseteq coPset _ _ _) => solve_elem_of. `````` Robbert Krebbers committed Jan 17, 2016 7 ``````Local Hint Extern 10 (✓{_} _) => `````` Robbert Krebbers committed Feb 10, 2016 8 9 10 `````` repeat match goal with | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega end; solve_validN. `````` Robbert Krebbers committed Jan 17, 2016 11 `````` `````` Robbert Krebbers committed Feb 01, 2016 12 13 ``````Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ → nat → iRes Λ Σ → Prop) (k : nat) (rf : iRes Λ Σ) (e1 : expr Λ) (σ1 : state Λ) := { `````` Robbert Krebbers committed Jan 19, 2016 14 `````` wf_safe : reducible e1 σ1; `````` Robbert Krebbers committed Jan 17, 2016 15 16 17 18 19 20 21 `````` wp_step e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → ∃ r2 r2', wsat k E σ2 (r2 ⋅ r2' ⋅ rf) ∧ Q e2 k r2 ∧ ∀ e', ef = Some e' → Qfork e' k r2' }. `````` Robbert Krebbers committed Feb 01, 2016 22 23 ``````CoInductive wp_pre {Λ Σ} (E : coPset) (Q : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop := `````` Robbert Krebbers committed Feb 10, 2016 24 `````` | wp_pre_value n r v : pvs E E (Q v) n r → wp_pre E Q (of_val v) n r `````` Robbert Krebbers committed Jan 17, 2016 25 26 27 `````` | wp_pre_step n r1 e1 : to_val e1 = None → (∀ rf k Ef σ1, `````` Robbert Krebbers committed Feb 10, 2016 28 `````` 0 < k < n → E ∩ Ef = ∅ → `````` Robbert Krebbers committed Jan 17, 2016 29 30 `````` wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) → wp_go (E ∪ Ef) (wp_pre E Q) `````` Robbert Krebbers committed Feb 17, 2016 31 `````` (wp_pre ⊤ (λ _, True%I)) k rf e1 σ1) → `````` Robbert Krebbers committed Jan 17, 2016 32 `````` wp_pre E Q e1 n r1. `````` Robbert Krebbers committed Feb 01, 2016 33 34 ``````Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Q e |}. `````` Robbert Krebbers committed Jan 17, 2016 35 ``````Next Obligation. `````` Robbert Krebbers committed Feb 01, 2016 36 `````` intros Λ Σ E e Q r1 r2 n Hwp Hr. `````` Robbert Krebbers committed Jan 22, 2016 37 `````` destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto. `````` Robbert Krebbers committed Jan 17, 2016 38 39 40 `````` intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver. Qed. Next Obligation. `````` Robbert Krebbers committed Feb 01, 2016 41 `````` intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2. `````` Robbert Krebbers committed Jan 17, 2016 42 `````` induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2. `````` Robbert Krebbers committed Jan 22, 2016 43 `````` destruct 1 as [|n1 r1 e1 ? Hgo]. `````` Robbert Krebbers committed Feb 17, 2016 44 45 `````` - constructor; eauto using uPred_weaken. - intros [rf' Hr] ??; constructor; [done|intros rf k Ef σ1 ???]. `````` Robbert Krebbers committed Jan 17, 2016 46 `````` destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep]; `````` Robbert Krebbers committed Feb 11, 2016 47 `````` rewrite ?assoc -?Hr; auto; constructor; [done|]. `````` Robbert Krebbers committed Jan 17, 2016 48 `````` intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. `````` Robbert Krebbers committed Feb 01, 2016 49 `````` exists r2, (r2' ⋅ rf'); split_ands; eauto 10 using (IH k), cmra_included_l. `````` Robbert Krebbers committed Feb 11, 2016 50 `````` by rewrite -!assoc (assoc _ r2). `````` Robbert Krebbers committed Jan 17, 2016 51 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 52 ``````Instance: Params (@wp) 4. `````` Robbert Krebbers committed Jan 17, 2016 53 54 `````` Section wp. `````` Robbert Krebbers committed Feb 01, 2016 55 56 57 58 59 ``````Context {Λ : language} {Σ : iFunctor}. Implicit Types P : iProp Λ Σ. Implicit Types Q : val Λ → iProp Λ Σ. Implicit Types v : val Λ. Implicit Types e : expr Λ. `````` Robbert Krebbers committed Jan 19, 2016 60 ``````Transparent uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 61 `````` `````` Robbert Krebbers committed Feb 10, 2016 62 63 ``````Global Instance wp_ne E e n : Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e). `````` Robbert Krebbers committed Jan 17, 2016 64 ``````Proof. `````` Ralf Jung committed Feb 10, 2016 65 `````` cut (∀ Q1 Q2, (∀ v, Q1 v ≡{n}≡ Q2 v) → `````` Robbert Krebbers committed Feb 10, 2016 66 67 68 69 70 71 72 73 `````` ∀ r n', n' ≤ n → ✓{n'} r → wp E e Q1 n' r → wp E e Q2 n' r). { by intros help Q Q' HQ; split; apply help. } intros Q1 Q2 HQ r n'; revert e r. induction n' as [n' IH] using lt_wf_ind=> e r. destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo]. { constructor. by eapply pvs_ne, HpvsQ; eauto. } constructor; [done|]=> rf k Ef σ1 ???. destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto. `````` Robbert Krebbers committed Jan 17, 2016 74 75 `````` split; [done|intros e2 σ2 ef ?]. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. `````` Robbert Krebbers committed Feb 10, 2016 76 `````` exists r2, r2'; split_ands; [|eapply IH|]; eauto. `````` Robbert Krebbers committed Jan 17, 2016 77 78 ``````Qed. Global Instance wp_proper E e : `````` Robbert Krebbers committed Feb 01, 2016 79 `````` Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e). `````` Robbert Krebbers committed Jan 17, 2016 80 81 82 ``````Proof. by intros Q Q' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist. Qed. `````` Robbert Krebbers committed Feb 10, 2016 83 84 85 86 87 88 89 90 ``````Lemma wp_mask_frame_mono E1 E2 e Q1 Q2 : E1 ⊆ E2 → (∀ v, Q1 v ⊑ Q2 v) → wp E1 e Q1 ⊑ wp E2 e Q2. Proof. intros HE HQ r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r. destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo]. { constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. } constructor; [done|]=> rf k Ef σ1 ???. assert (E2 ∪ Ef = E1 ∪ (E2 ∖ E1 ∪ Ef)) as HE'. `````` Robbert Krebbers committed Feb 11, 2016 91 `````` { by rewrite assoc_L -union_difference_L. } `````` Robbert Krebbers committed Feb 10, 2016 92 93 94 95 96 `````` destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto. split; [done|intros e2 σ2 ef ?]. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto. Qed. `````` Robbert Krebbers committed Jan 17, 2016 97 `````` `````` Robbert Krebbers committed Feb 10, 2016 98 ``````Lemma wp_value_inv E Q v n r : wp E (of_val v) Q n r → pvs E E (Q v) n r. `````` Robbert Krebbers committed Jan 20, 2016 99 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 100 `````` by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_equality. `````` Robbert Krebbers committed Jan 20, 2016 101 102 ``````Qed. Lemma wp_step_inv E Ef Q e k n σ r rf : `````` Robbert Krebbers committed Feb 10, 2016 103 `````` to_val e = None → 0 < k < n → E ∩ Ef = ∅ → `````` Robbert Krebbers committed Jan 20, 2016 104 `````` wp E e Q n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) → `````` Robbert Krebbers committed Feb 17, 2016 105 `````` wp_go (E ∪ Ef) (λ e, wp E e Q) (λ e, wp ⊤ e (λ _, True%I)) k rf e σ. `````` Robbert Krebbers committed Jan 22, 2016 106 ``````Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed. `````` Robbert Krebbers committed Jan 20, 2016 107 `````` `````` Ralf Jung committed Feb 12, 2016 108 ``````Lemma wp_value' E Q v : Q v ⊑ wp E (of_val v) Q. `````` Robbert Krebbers committed Feb 10, 2016 109 110 ``````Proof. by constructor; apply pvs_intro. Qed. Lemma pvs_wp E e Q : pvs E E (wp E e Q) ⊑ wp E e Q. `````` Robbert Krebbers committed Jan 17, 2016 111 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 112 `````` intros r n ? Hvs. `````` Robbert Krebbers committed Jan 17, 2016 113 `````` destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|]. `````` Robbert Krebbers committed Feb 10, 2016 114 115 116 `````` { constructor; eapply pvs_trans', pvs_mono, Hvs; eauto. intros ???; apply wp_value_inv. } constructor; [done|]=> rf k Ef σ1 ???. `````` Robbert Krebbers committed Jan 17, 2016 117 `````` destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto. `````` Robbert Krebbers committed Feb 10, 2016 118 119 120 121 122 123 124 125 126 `````` eapply wp_step_inv with (S k) r'; eauto. Qed. Lemma wp_pvs E e Q : wp E e (λ v, pvs E E (Q v)) ⊑ wp E e Q. Proof. intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HQ. destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|]. { constructor; apply pvs_trans', (wp_value_inv _ (pvs E E ∘ Q)); auto. } constructor; [done|]=> rf k Ef σ1 ???. destruct (wp_step_inv E Ef (pvs E E ∘ Q) e k n σ1 r rf) as [? Hstep]; auto. `````` Robbert Krebbers committed Jan 17, 2016 127 128 `````` split; [done|intros e2 σ2 ef ?]. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto. `````` Robbert Krebbers committed Feb 10, 2016 129 `````` exists r2, r2'; split_ands; [|apply (IH k)|]; auto. `````` Robbert Krebbers committed Jan 17, 2016 130 131 132 133 ``````Qed. Lemma wp_atomic E1 E2 e Q : E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Q v))) ⊑ wp E1 e Q. Proof. `````` Robbert Krebbers committed Feb 02, 2016 134 `````` intros ? He r n ? Hvs; constructor; eauto using atomic_not_val. `````` Robbert Krebbers committed Jan 17, 2016 135 136 `````` intros rf k Ef σ1 ???. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto. `````` Robbert Krebbers committed Feb 10, 2016 137 138 139 `````` destruct (wp_step_inv E2 Ef (pvs E2 E1 ∘ Q) e k (S k) σ1 r' rf) as [Hsafe Hstep]; auto using atomic_not_val. split; [done|]=> e2 σ2 ef ?. `````` Robbert Krebbers committed Jan 17, 2016 140 `````` destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); clear Hsafe Hstep; auto. `````` Robbert Krebbers committed Jan 22, 2016 141 142 `````` destruct Hwp' as [k r2 v Hvs'|k r2 e2 Hgo]; [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver]. `````` Robbert Krebbers committed Feb 10, 2016 143 `````` apply pvs_trans in Hvs'; auto. `````` Robbert Krebbers committed Feb 11, 2016 144 `````` destruct (Hvs' (r2' ⋅ rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto. `````` Robbert Krebbers committed Feb 10, 2016 145 `````` exists r3, r2'; split_ands; last done. `````` Robbert Krebbers committed Feb 17, 2016 146 147 `````` - by rewrite -assoc. - constructor; apply pvs_intro; auto. `````` Robbert Krebbers committed Jan 17, 2016 148 149 150 151 152 153 ``````Qed. Lemma wp_frame_r E e Q R : (wp E e Q ★ R) ⊑ wp E e (λ v, Q v ★ R). Proof. intros r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp. induction n as [n IH] using lt_wf_ind; intros e r1. `````` Robbert Krebbers committed Feb 10, 2016 154 155 156 157 `````` destruct 1 as [|n r e ? Hgo]=>?. { constructor; apply pvs_frame_r; auto. exists r, rR; eauto. } constructor; [done|]=> rf k Ef σ1 ???. destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep]; auto. `````` Robbert Krebbers committed Feb 11, 2016 158 `````` { by rewrite assoc. } `````` Robbert Krebbers committed Jan 17, 2016 159 160 161 `````` split; [done|intros e2 σ2 ef ?]. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. exists (r2 ⋅ rR), r2'; split_ands; auto. `````` Robbert Krebbers committed Feb 17, 2016 162 `````` - by rewrite -(assoc _ r2) `````` Robbert Krebbers committed Feb 11, 2016 163 `````` (comm _ rR) !assoc -(assoc _ _ rR). `````` Robbert Krebbers committed Feb 17, 2016 164 `````` - apply IH; eauto using uPred_weaken. `````` Robbert Krebbers committed Jan 17, 2016 165 166 167 168 169 ``````Qed. Lemma wp_frame_later_r E e Q R : to_val e = None → (wp E e Q ★ ▷ R) ⊑ wp E e (λ v, Q v ★ R). Proof. intros He r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr. `````` Robbert Krebbers committed Feb 10, 2016 170 171 `````` destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|]. constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega. `````` Robbert Krebbers committed Feb 11, 2016 172 `````` destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto. `````` Robbert Krebbers committed Jan 17, 2016 173 174 175 `````` split; [done|intros e2 σ2 ef ?]. destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. exists (r2 ⋅ rR), r2'; split_ands; auto. `````` Robbert Krebbers committed Feb 17, 2016 176 `````` - by rewrite -(assoc _ r2) `````` Robbert Krebbers committed Feb 11, 2016 177 `````` (comm _ rR) !assoc -(assoc _ _ rR). `````` Robbert Krebbers committed Feb 17, 2016 178 `````` - apply wp_frame_r; [auto|exists r2, rR; split_ands; auto]. `````` Robbert Krebbers committed Jan 17, 2016 179 180 `````` eapply uPred_weaken with rR n; eauto. Qed. `````` Ralf Jung committed Feb 02, 2016 181 182 ``````Lemma wp_bind `{LanguageCtx Λ K} E e Q : wp E e (λ v, wp E (K (of_val v)) Q) ⊑ wp E (K e) Q. `````` Robbert Krebbers committed Jan 17, 2016 183 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 184 185 186 187 `````` intros r n; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?. destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|]. constructor; auto using fill_not_val=> rf k Ef σ1 ???. destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto. `````` Robbert Krebbers committed Jan 17, 2016 188 189 `````` split. { destruct Hsafe as (e2&σ2&ef&?). `````` Ralf Jung committed Feb 02, 2016 190 `````` by exists (K e2), σ2, ef; apply fill_step. } `````` Robbert Krebbers committed Jan 17, 2016 191 `````` intros e2 σ2 ef ?. `````` Ralf Jung committed Feb 02, 2016 192 `````` destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto. `````` Robbert Krebbers committed Jan 17, 2016 193 194 195 196 `````` destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto. exists r2, r2'; split_ands; try eapply IH; eauto. Qed. `````` Ralf Jung committed Feb 11, 2016 197 ``````(** * Derived rules *) `````` Ralf Jung committed Jan 26, 2016 198 ``````Opaque uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 199 ``````Import uPred. `````` Robbert Krebbers committed Feb 10, 2016 200 201 ``````Lemma wp_mono E e Q1 Q2 : (∀ v, Q1 v ⊑ Q2 v) → wp E e Q1 ⊑ wp E e Q2. Proof. by apply wp_mask_frame_mono. Qed. `````` Robbert Krebbers committed Jan 17, 2016 202 ``````Global Instance wp_mono' E e : `````` Robbert Krebbers committed Feb 01, 2016 203 `````` Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e). `````` Robbert Krebbers committed Jan 17, 2016 204 ``````Proof. by intros Q Q' ?; apply wp_mono. Qed. `````` Ralf Jung committed Feb 10, 2016 205 206 ``````Lemma wp_strip_pvs E e P Q : P ⊑ wp E e Q → pvs E E P ⊑ wp E e Q. Proof. move=>->. by rewrite pvs_wp. Qed. `````` Ralf Jung committed Feb 12, 2016 207 208 ``````Lemma wp_value E Q e v : to_val e = Some v → Q v ⊑ wp E e Q. Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed. `````` Robbert Krebbers committed Jan 17, 2016 209 ``````Lemma wp_frame_l E e Q R : (R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v). `````` Robbert Krebbers committed Feb 11, 2016 210 ``````Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed. `````` Robbert Krebbers committed Jan 17, 2016 211 212 213 ``````Lemma wp_frame_later_l E e Q R : to_val e = None → (▷ R ★ wp E e Q) ⊑ wp E e (λ v, R ★ Q v). Proof. `````` Robbert Krebbers committed Feb 11, 2016 214 `````` rewrite (comm _ (▷ R)%I); setoid_rewrite (comm _ R). `````` Robbert Krebbers committed Jan 17, 2016 215 216 `````` apply wp_frame_later_r. Qed. `````` Robbert Krebbers committed Jan 18, 2016 217 218 ``````Lemma wp_always_l E e Q R `{!AlwaysStable R} : (R ∧ wp E e Q) ⊑ wp E e (λ v, R ∧ Q v). `````` Ralf Jung committed Feb 12, 2016 219 ``````Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed. `````` Robbert Krebbers committed Jan 18, 2016 220 221 ``````Lemma wp_always_r E e Q R `{!AlwaysStable R} : (wp E e Q ∧ R) ⊑ wp E e (λ v, Q v ∧ R). `````` Ralf Jung committed Feb 12, 2016 222 ``````Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed. `````` Robbert Krebbers committed Jan 17, 2016 223 224 ``````Lemma wp_impl_l E e Q1 Q2 : ((□ ∀ v, Q1 v → Q2 v) ∧ wp E e Q1) ⊑ wp E e Q2. Proof. `````` Robbert Krebbers committed Feb 10, 2016 225 `````` rewrite wp_always_l; apply wp_mono=> // v. `````` Ralf Jung committed Jan 30, 2016 226 `````` by rewrite always_elim (forall_elim v) impl_elim_l. `````` Robbert Krebbers committed Jan 17, 2016 227 228 ``````Qed. Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 ∧ □ ∀ v, Q1 v → Q2 v) ⊑ wp E e Q2. `````` Robbert Krebbers committed Feb 11, 2016 229 ``````Proof. by rewrite comm wp_impl_l. Qed. `````` Ralf Jung committed Feb 11, 2016 230 231 232 233 ``````Lemma wp_mask_weaken E1 E2 e Q : E1 ⊆ E2 → wp E1 e Q ⊑ wp E2 e Q. Proof. auto using wp_mask_frame_mono. Qed. (** * Weakest-pre is a FSA. *) `````` Robbert Krebbers committed Feb 13, 2016 234 235 ``````Definition wp_fsa (e : expr Λ) : FSA Λ Σ (val Λ) := λ E, wp E e. Global Instance wp_fsa_prf : FrameShiftAssertion (atomic e) (wp_fsa e). `````` Ralf Jung committed Feb 11, 2016 236 ``````Proof. `````` Robbert Krebbers committed Feb 13, 2016 237 238 `````` rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic, wp_frame_r. intros E Q. by rewrite -(pvs_wp E e Q) -(wp_pvs E e Q). `````` Ralf Jung committed Feb 11, 2016 239 ``````Qed. `````` Robbert Krebbers committed Jan 17, 2016 240 ``End wp.``