pviewshifts.v 10.2 KB
Newer Older
1 2 3
From prelude Require Export co_pset.
From program_logic Require Export model.
From program_logic Require Import ownership wsat.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Hint Extern 10 (_  _) => omega.
5 6
Local Hint Extern 100 (@eq coPset _ _) => set_solver.
Local Hint Extern 100 (_  _) => set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Local Hint Extern 10 ({_} _) =>
8 9 10
  repeat match goal with
  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
  end; solve_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12
Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  {| uPred_holds n r1 :=  rf k Ef σ,
14
       0 < k  n  (E1  E2)  Ef =  
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17
       wsat k (E1  Ef) σ (r1  rf) 
        r2, P k r2  wsat k (E2  Ef) σ (r2  rf) |}.
Next Obligation.
18
  intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21
  apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
Qed.
Next Obligation.
22
  intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
23 24
  destruct (HP (r3rf) k Ef σ) as (r'&?&Hws'); rewrite ?(assoc op); auto.
  exists (r'  r3); rewrite -assoc; split; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  apply uPred_weaken with k r'; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Qed.
27 28
Arguments pvs {_ _} _ _ _%I : simpl never.
Instance: Params (@pvs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

30 31 32 33 34 35 36
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
  (at level 199, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
Notation "|={ E }=> Q" := (pvs E E Q%I)
  (at level 199, E at level 50, Q at level 200,
   format "|={ E }=>  Q") : uPred_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
37
Section pvs.
38 39 40
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
41
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
42

43
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46
Proof.
  intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
    destruct (HP rf k Ef σ) as (r2&?&?); auto;
47
    exists r2; split_and?; auto; apply HPQ; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Qed.
49
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51
Proof. apply ne_proper, _. Qed.

52
Lemma pvs_intro E P : P  |={E}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55
  intros n r ? HP rf k Ef σ ???; exists r; split; last done.
  apply uPred_weaken with n r; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Qed.
57
Lemma pvs_mono E1 E2 P Q : P  Q  (|={E1,E2}=> P)  (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
58
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  intros HPQ n r ? HP rf k Ef σ ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61
  destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto.
Qed.
62
Lemma pvs_timeless E P : TimelessP P  ( P)  (|={E}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  rewrite uPred.timelessP_spec=> HP [|n] r ? HP' rf k Ef σ ???; first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  exists r; split; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68
Qed.
Lemma pvs_trans E1 E2 E3 P :
69
  E2  E1  E3  (|={E1,E2}=> |={E2,E3}=> P)  (|={E1,E3}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  intros ? n r1 ? HP1 rf k Ef σ ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74
  destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
75
  Ef  (E1  E2) =   (|={E1,E2}=> P)  (|={E1  Ef,E2  Ef}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
  intros ? n r ? HP rf k Ef' σ ???.
78 79
  destruct (HP rf k (EfEf') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
  by exists r'; rewrite -(assoc_L _).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Qed.
81
Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P)  Q)  (|={E1,E2}=> P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
  intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
  destruct (HP (r2  rf) k Ef σ) as (r'&?&?); eauto.
85 86
  { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
  exists (r'  r2); split; last by rewrite -assoc.
87
  exists r', r2; split_and?; auto; apply uPred_weaken with n r2; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Qed.
89
Lemma pvs_openI i P : ownI i P  (|={{[i]},}=>  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  intros [|n] r ? Hinv rf [|k] Ef σ ???; try lia.
92
  apply ownI_spec in Hinv; last auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94
  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. }
95
  exists (rP  r); split; last by rewrite (left_id_L _ _) -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  eapply uPred_weaken with (S k) rP; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Qed.
98
Lemma pvs_closeI i P : (ownI i P   P)  (|={,{[i]}}=> True).
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  intros [|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ; split; [done|].
101
  rewrite left_id; apply wsat_close with P r.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  - apply ownI_spec, uPred_weaken with (S n) r; auto.
103
  - set_solver +HE.
104
  - by rewrite -(left_id_L  () Ef).
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  - apply uPred_weaken with n r; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Qed.
107
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ  Prop) :
108
  m ~~>: P  ownG m  (|={E}=>  m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  intros Hup%option_updateP' [|n] r ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  destruct (wsat_update_gst k (E  Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
112
  { apply cmra_includedN_le with (S n); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114
  by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
115
Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
Robbert Krebbers's avatar
Robbert Krebbers committed
116
    E (P : iGst Λ Σ  Prop) :
117
   ~~>: P  True  (|={E}=>  m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  intros Hup [|n] r ? _ rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
120 121 122 123 124 125
  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.
126
Lemma pvs_allocI E P : ¬set_finite E   P  (|={E}=>  i,  (i  E)  ownI i P).
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  intros ? [|n] r ? HP rf [|k] Ef σ ???; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  { apply uPred_weaken with n r; eauto. }
131
  exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]}  ).
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133 134
  by split; [by exists i; split; rewrite /uPred_holds /=|].
Qed.

135
(** * Derived rules *)
136
Opaque uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Import uPred.
138
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof. intros P Q; apply pvs_mono. Qed.
140
Lemma pvs_trans' E P : (|={E}=> |={E}=> P)  (|={E}=> P).
141
Proof. apply pvs_trans; set_solver. Qed.
142
Lemma pvs_strip_pvs E P Q : P  (|={E}=> Q)  (|={E}=> P)  (|={E}=> Q).
143
Proof. move=>->. by rewrite pvs_trans'. Qed.
144
Lemma pvs_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q)  (|={E1,E2}=> P  Q).
145
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
146
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
147
  (P  |={E1,E2}=> Q)  (|={E1,E2}=> P  Q).
148
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
149
Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
150
  ((|={E1,E2}=> P)  Q)  (|={E1,E2}=> P  Q).
151
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
152
Lemma pvs_impl_l E1 E2 P Q : ( (P  Q)  (|={E1,E2}=> P))  (|={E1,E2}=> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
154
Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P)   (P  Q))  (|={E1,E2}=> Q).
155
Proof. by rewrite comm pvs_impl_l. Qed.
156
Lemma pvs_wand_l E1 E2 P Q R :
157
  P  (|={E1,E2}=> Q)  ((Q - R)  P)  (|={E1,E2}=> R).
158
Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
159
Lemma pvs_wand_r E1 E2 P Q R :
160
  P  (|={E1,E2}=> Q)  (P  (Q - R))  (|={E1,E2}=> R).
161
Proof. rewrite comm. apply pvs_wand_l. Qed.
Ralf Jung's avatar
Ralf Jung committed
162 163 164
Lemma pvs_sep E P Q:
  ((|={E}=> P)  (|={E}=> Q))  (|={E}=> P  Q).
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
165

166
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
167 168
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
  (|={E1',E2'}=> P)  (|={E1,E2}=> P).
169
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
  intros HE1 HE2 HEE.
171
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
  by rewrite {2}HEE -!union_difference_L.
173
Qed.
Ralf Jung's avatar
Ralf Jung committed
174 175 176

Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
177
  P  Q  (|={E1',E2'}=> P)  (|={E1,E2}=> Q).
Ralf Jung's avatar
Ralf Jung committed
178 179
Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.

180
(** It should be possible to give a stronger version of this rule
Ralf Jung's avatar
Ralf Jung committed
181 182
   that does not force the conclusion view shift to have twice the
   same mask. However, even expressing the side-conditions on the
183
   mask becomes really ugly then, and we have not found an instance
Ralf Jung's avatar
Ralf Jung committed
184
   where that would be useful. *)
Ralf Jung's avatar
Ralf Jung committed
185
Lemma pvs_trans3 E1 E2 Q :
186
  E2  E1  (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q)  (|={E1}=> Q).
187
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
188

189
Lemma pvs_mask_weaken E1 E2 P : E1  E2  (|={E1}=> P)  (|={E2}=> P).
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Proof. auto using pvs_mask_frame'. Qed.
Ralf Jung's avatar
Ralf Jung committed
191

192
Lemma pvs_ownG_update E m m' : m ~~> m'  ownG m  (|={E}=> ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Proof.
194
  intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
Robbert Krebbers's avatar
Robbert Krebbers committed
195 196
  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.
Ralf Jung's avatar
Ralf Jung committed
197

Robbert Krebbers's avatar
Robbert Krebbers committed
198
End pvs.
199 200 201 202 203 204

(** * Frame Shift Assertions. *)
(* 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. *)
205 206
Notation FSA Λ Σ A := (coPset  (A  iProp Λ Σ)  iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
207 208
  fsa_mask_frame_mono E1 E2 Φ Ψ :
    E1  E2  ( a, Φ a  Ψ a)  fsa E1 Φ  fsa E2 Ψ;
209
  fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a))  fsa E Φ;
210
  fsa_open_close E1 E2 Φ :
211
    fsaV  E2  E1  (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a))  fsa E1 Φ;
212
  fsa_frame_r E P Φ : (fsa E Φ  P)  fsa E (λ a, Φ a  P)
213 214
}.

215 216
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
217
Implicit Types Φ Ψ : A  iProp Λ Σ.
218

219
Lemma fsa_mono E Φ Ψ : ( a, Φ a  Ψ a)  fsa E Φ  fsa E Ψ.
220
Proof. apply fsa_mask_frame_mono; auto. Qed.
221
Lemma fsa_mask_weaken E1 E2 Φ : E1  E2  fsa E1 Φ  fsa E2 Φ.
222
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
223
Lemma fsa_frame_l E P Φ : (P  fsa E Φ)  fsa E (λ a, P  Φ a).
224
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
225
Lemma fsa_strip_pvs E P Φ : P  fsa E Φ  (|={E}=> P)  fsa E Φ.
226
Proof.
227 228
  move=>->. rewrite -{2}fsa_trans3.
  apply pvs_mono, fsa_mono=>a; apply pvs_intro.
229
Qed.
230
Lemma fsa_mono_pvs E Φ Ψ : ( a, Φ a  (|={E}=> Ψ a))  fsa E Φ  fsa E Ψ.
231
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
232 233
End fsa.

234
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
235
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
236
Proof.
237 238
  rewrite /pvs_fsa.
  split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
239
Qed.