pviewshifts.v 9.62 KB
 Ralf Jung committed Feb 08, 2016 1 2 3 ``````Require Export prelude.co_pset. Require Export program_logic.model. Require Import program_logic.ownership program_logic.wsat. `````` Robbert Krebbers committed Jan 17, 2016 4 5 6 7 ``````Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of. Local Hint Extern 100 (_ ∉ _) => solve_elem_of. 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 ``````Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ := `````` Robbert Krebbers committed Jan 17, 2016 13 `````` {| uPred_holds n r1 := ∀ rf k Ef σ, `````` Robbert Krebbers committed Feb 10, 2016 14 `````` 0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ → `````` Robbert Krebbers committed Jan 17, 2016 15 16 17 `````` wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) → ∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}. Next Obligation. `````` Robbert Krebbers committed Feb 01, 2016 18 `````` intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *. `````` Robbert Krebbers committed Jan 17, 2016 19 20 21 `````` apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia. Qed. Next Obligation. `````` Robbert Krebbers committed Feb 01, 2016 22 `````` intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst. `````` Robbert Krebbers committed Jan 17, 2016 23 24 `````` destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto. exists (r' ⋅ r3); rewrite -(associative _); split; last done. `````` Robbert Krebbers committed Feb 01, 2016 25 `````` apply uPred_weaken with r' k; eauto using cmra_included_l. `````` Robbert Krebbers committed Jan 17, 2016 26 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 27 28 ``````Arguments pvs {_ _} _ _ _%I : simpl never. Instance: Params (@pvs) 4. `````` Robbert Krebbers committed Jan 17, 2016 29 30 `````` Section pvs. `````` Robbert Krebbers committed Feb 01, 2016 31 32 33 ``````Context {Λ : language} {Σ : iFunctor}. Implicit Types P Q : iProp Λ Σ. Implicit Types m : iGst Λ Σ. `````` Robbert Krebbers committed Jan 19, 2016 34 ``````Transparent uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 35 `````` `````` Robbert Krebbers committed Feb 01, 2016 36 ``````Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 37 38 39 40 41 ``````Proof. intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???; destruct (HP rf k Ef σ) as (r2&?&?); auto; exists r2; split_ands; auto; apply HPQ; eauto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 42 ``````Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 ``````Proof. apply ne_proper, _. Qed. Lemma pvs_intro E P : P ⊑ pvs E E P. Proof. intros r n ? HP rf k Ef σ ???; exists r; split; last done. apply uPred_weaken with r n; eauto. Qed. Lemma pvs_mono E1 E2 P Q : P ⊑ Q → pvs E1 E2 P ⊑ pvs E1 E2 Q. Proof. intros HPQ r n ? HP rf k Ef σ ???. destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto. Qed. Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ pvs E E P. Proof. rewrite uPred.timelessP_spec=> HP r [|n] ? HP' rf k Ef σ ???; first lia. exists r; split; last done. `````` Robbert Krebbers committed Feb 01, 2016 59 `````` apply HP, uPred_weaken with r n; eauto using cmra_validN_le. `````` Robbert Krebbers committed Jan 17, 2016 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 ``````Qed. Lemma pvs_trans E1 E2 E3 P : E2 ⊆ E1 ∪ E3 → pvs E1 E2 (pvs E2 E3 P) ⊑ pvs E1 E3 P. Proof. intros ? r1 n ? HP1 rf k Ef σ ???. destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto. Qed. Lemma pvs_mask_frame E1 E2 Ef P : Ef ∩ (E1 ∪ E2) = ∅ → pvs E1 E2 P ⊑ pvs (E1 ∪ Ef) (E2 ∪ Ef) P. Proof. intros ? r n ? HP rf k Ef' σ ???. destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(associative_L _); eauto. by exists r'; rewrite -(associative_L _). Qed. Lemma pvs_frame_r E1 E2 P Q : (pvs E1 E2 P ★ Q) ⊑ pvs E1 E2 (P ★ Q). Proof. intros r n ? (r1&r2&Hr&HP&?) rf k Ef σ ???. destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto. { by rewrite (associative _) -(dist_le _ _ _ _ Hr); last lia. } exists (r' ⋅ r2); split; last by rewrite -(associative _). exists r', r2; split_ands; auto; apply uPred_weaken with r2 n; auto. Qed. `````` Ralf Jung committed Feb 09, 2016 82 ``````Lemma pvs_openI i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P). `````` Robbert Krebbers committed Jan 17, 2016 83 84 ``````Proof. intros r [|n] ? Hinv rf [|k] Ef σ ???; try lia. `````` Ralf Jung committed Feb 09, 2016 85 `````` apply ownI_spec in Hinv; last auto. `````` Robbert Krebbers committed Jan 17, 2016 86 87 88 `````` destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto. { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. } exists (rP ⋅ r); split; last by rewrite (left_id_L _ _) -(associative _). `````` Robbert Krebbers committed Feb 01, 2016 89 `````` eapply uPred_weaken with rP (S k); eauto using cmra_included_l. `````` Robbert Krebbers committed Jan 17, 2016 90 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 91 ``````Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True. `````` Robbert Krebbers committed Jan 17, 2016 92 93 94 ``````Proof. intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|]. rewrite (left_id _ _); apply wsat_close with P r. `````` Ralf Jung committed Feb 09, 2016 95 `````` * apply ownI_spec, uPred_weaken with r (S n); auto. `````` Robbert Krebbers committed Jan 17, 2016 96 97 98 99 `````` * solve_elem_of +HE. * by rewrite -(left_id_L ∅ (∪) Ef). * apply uPred_weaken with r n; auto. Qed. `````` Ralf Jung committed Feb 08, 2016 100 ``````Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) : `````` Ralf Jung committed Feb 03, 2016 101 `````` m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). `````` Robbert Krebbers committed Jan 17, 2016 102 ``````Proof. `````` Robbert Krebbers committed Feb 08, 2016 103 104 `````` intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia. destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto. `````` Robbert Krebbers committed Feb 04, 2016 105 `````` { apply cmra_includedN_le with (S n); auto. } `````` Robbert Krebbers committed Jan 17, 2016 106 107 `````` by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|]. Qed. `````` Ralf Jung committed Feb 08, 2016 108 ``````Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} `````` Robbert Krebbers committed Feb 08, 2016 109 110 111 112 113 114 115 116 117 118 `````` E (P : iGst Λ Σ → Prop) : ∅ ~~>: P → True ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). Proof. intros Hup r [|n] ? _ rf [|k] Ef σ ???; try lia. destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto. { apply cmra_empty_leastN. } { apply cmra_updateP_compose_l with (Some ∅), option_updateP with P; auto using option_update_None. } by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|]. Qed. `````` Ralf Jung committed Feb 09, 2016 119 ``````Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ ownI i P). `````` Robbert Krebbers committed Jan 17, 2016 120 121 122 123 ``````Proof. intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia. destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto. { apply uPred_weaken with r n; eauto. } `````` Robbert Krebbers committed Feb 10, 2016 124 `````` exists (Res {[ i ↦ to_agree (Next (iProp_unfold P)) ]} ∅ ∅). `````` Robbert Krebbers committed Jan 17, 2016 125 126 127 `````` by split; [by exists i; split; rewrite /uPred_holds /=|]. Qed. `````` Robbert Krebbers committed Feb 09, 2016 128 ``````(** * Derived rules *) `````` Robbert Krebbers committed Feb 01, 2016 129 ``````Opaque uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 130 ``````Import uPred. `````` Robbert Krebbers committed Feb 01, 2016 131 ``````Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 132 133 134 ``````Proof. intros P Q; apply pvs_mono. Qed. Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P. Proof. apply pvs_trans; solve_elem_of. Qed. `````` Ralf Jung committed Feb 10, 2016 135 136 ``````Lemma pvs_strip_pvs E P Q : P ⊑ pvs E E Q → pvs E E P ⊑ pvs E E Q. Proof. move=>->. by rewrite pvs_trans'. Qed. `````` Robbert Krebbers committed Jan 17, 2016 137 138 ``````Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q). Proof. rewrite !(commutative _ P); apply pvs_frame_r. Qed. `````` Robbert Krebbers committed Jan 18, 2016 139 140 141 142 143 144 ``````Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} : (P ∧ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ∧ Q). Proof. by rewrite !always_and_sep_l' pvs_frame_l. Qed. Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} : (pvs E1 E2 P ∧ Q) ⊑ pvs E1 E2 (P ∧ Q). Proof. by rewrite !always_and_sep_r' pvs_frame_r. Qed. `````` Robbert Krebbers committed Jan 17, 2016 145 146 147 148 ``````Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ pvs E1 E2 P) ⊑ pvs E1 E2 Q. Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed. Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q. Proof. by rewrite (commutative _) pvs_impl_l. Qed. `````` Ralf Jung committed Feb 09, 2016 149 `````` `````` Ralf Jung committed Feb 09, 2016 150 151 152 ``````Lemma pvs_mask_frame' E1 E1' E2 E2' P : E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → pvs E1' E2' P ⊑ pvs E1 E2 P. Proof. `````` Robbert Krebbers committed Feb 09, 2016 153 154 155 `````` intros HE1 HE2 HEE. rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last solve_elem_of. by rewrite {2}HEE -!union_difference_L. `````` Ralf Jung committed Feb 09, 2016 156 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 157 158 159 160 161 162 `````` Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q : E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → P ⊑ Q → pvs E1' E2' P ⊑ pvs E1 E2 Q. Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed. `````` Robbert Krebbers committed Feb 09, 2016 163 ``````(** It should be possible to give a stronger version of this rule `````` Ralf Jung committed Feb 09, 2016 164 165 `````` that does not force the conclusion view shift to have twice the same mask. However, even expressing the side-conditions on the `````` Robbert Krebbers committed Feb 09, 2016 166 `````` mask becomes really ugly then, and we have not found an instance `````` Ralf Jung committed Feb 09, 2016 167 `````` where that would be useful. *) `````` Ralf Jung committed Feb 09, 2016 168 169 ``````Lemma pvs_trans3 E1 E2 Q : E2 ⊆ E1 → pvs E1 E2 (pvs E2 E2 (pvs E2 E1 Q)) ⊑ pvs E1 E1 Q. `````` Robbert Krebbers committed Feb 09, 2016 170 ``````Proof. intros HE. rewrite !pvs_trans; solve_elem_of. Qed. `````` Ralf Jung committed Feb 09, 2016 171 `````` `````` Robbert Krebbers committed Jan 17, 2016 172 ``````Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P. `````` Robbert Krebbers committed Feb 09, 2016 173 ``````Proof. auto using pvs_mask_frame'. Qed. `````` Ralf Jung committed Feb 09, 2016 174 `````` `````` Ralf Jung committed Feb 08, 2016 175 ``````Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m'). `````` Robbert Krebbers committed Jan 17, 2016 176 ``````Proof. `````` Ralf Jung committed Feb 08, 2016 177 `````` intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP. `````` Robbert Krebbers committed Jan 17, 2016 178 179 `````` by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->. Qed. `````` Ralf Jung committed Feb 09, 2016 180 `````` `````` Robbert Krebbers committed Jan 17, 2016 181 ``````End pvs. `````` Ralf Jung committed Feb 11, 2016 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 `````` (** * Frame Shift Assertions. *) Section fsa. Context {Λ : language} {Σ : iFunctor} {A : Type}. Implicit Types P : iProp Λ Σ. Implicit Types Q : A → iProp Λ Σ. (* Yes, the name is horrible... Frame Shift Assertions take a mask and a predicate over some type (that's their "postcondition"). They support weakening the mask, framing resources into the postcondition, and composition witn mask-changing view shifts. *) Class FrameShiftAssertion (FSA : coPset → (A → iProp Λ Σ) → iProp Λ Σ) := { fsa_mask_frame_mono E1 E2 Q Q' :> E1 ⊆ E2 → (∀ a, Q a ⊑ Q' a) → FSA E1 Q ⊑ FSA E2 Q'; fsa_trans3 E1 E2 Q : E2 ⊆ E1 → pvs E1 E2 (FSA E2 (λ a, pvs E2 E1 (Q a))) ⊑ FSA E1 Q; fsa_frame_r E P Q : (FSA E Q ★ P) ⊑ FSA E (λ a, Q a ★ P) }. Context FSA `{FrameShiftAssertion FSA}. Lemma fsa_mono E Q Q' : (∀ a, Q a ⊑ Q' a) → FSA E Q ⊑ FSA E Q'. Proof. apply fsa_mask_frame_mono; auto. Qed. Lemma fsa_mask_weaken E1 E2 Q : E1 ⊆ E2 → FSA E1 Q ⊑ FSA E2 Q. Proof. intros. apply fsa_mask_frame_mono; auto. Qed. Lemma fsa_frame_l E P Q : (P ★ FSA E Q) ⊑ FSA E (λ a, P ★ Q a). Proof. rewrite commutative fsa_frame_r. apply fsa_mono=>a. by rewrite commutative. Qed. Lemma fsa_strip_pvs E P Q : P ⊑ FSA E Q → pvs E E P ⊑ FSA E Q. Proof. move=>->. rewrite -{2}fsa_trans3; last reflexivity. apply pvs_mono, fsa_mono=>a. apply pvs_intro. Qed. Lemma fsa_mono_pvs E Q Q' : (∀ a, Q a ⊑ pvs E E (Q' a)) → FSA E Q ⊑ FSA E Q'. Proof. move=>HQ. rewrite -[FSA E Q']fsa_trans3; last reflexivity. rewrite -pvs_intro. by apply fsa_mono. Qed. End fsa. (** View shifts are a FSA. *) Section pvs_fsa. Context {Λ : language} {Σ : iFunctor}. Implicit Types P : iProp Λ Σ. Implicit Types Q : () → iProp Λ Σ. Global Instance pvs_fsa : FrameShiftAssertion (λ E Q, pvs E E (Q ())). Proof. split; intros. - apply pvs_mask_frame_mono; auto. - apply pvs_trans3; auto. - apply pvs_frame_r; auto. Qed. End pvs_fsa.``````