pviewshifts.v 10.1 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 47 48
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.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  exists r', r2; split_ands; 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
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
164 165
  E1'  E1  E2'  E2  E1  E1' = E2  E2' 
  (|={E1',E2'}=> P)  (|={E1,E2}=> P).
166
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  intros HE1 HE2 HEE.
168
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  by rewrite {2}HEE -!union_difference_L.
170
Qed.
Ralf Jung's avatar
Ralf Jung committed
171 172 173

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
195
End pvs.
196 197 198 199 200 201

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

212 213
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
214
Implicit Types Φ Ψ : A  iProp Λ Σ.
215

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

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