pviewshifts.v 9.7 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

Section pvs.
31 32 33
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
34
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
35

36
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
42
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46
Proof. apply ne_proper, _. Qed.

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

128
(** * Derived rules *)
129
Opaque uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Import uPred.
131
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
Proof. intros P Q; apply pvs_mono. Qed.
Lemma pvs_trans' E P : pvs E E (pvs E E P)  pvs E E P.
134
Proof. apply pvs_trans; set_solver. Qed.
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's avatar
Robbert Krebbers committed
137
Lemma pvs_frame_l E1 E2 P Q : (P  pvs E1 E2 Q)  pvs E1 E2 (P  Q).
138
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
139 140
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
  (P  pvs E1 E2 Q)  pvs E1 E2 (P  Q).
141
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
142 143
Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
  (pvs E1 E2 P  Q)  pvs E1 E2 (P  Q).
144
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146 147
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.
148
Proof. by rewrite comm pvs_impl_l. Qed.
149 150
Lemma pvs_wand_l E1 E2 P Q R :
  P  pvs E1 E2 Q  ((Q - R)  P)  pvs E1 E2 R.
151
Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
152 153 154
Lemma pvs_wand_r E1 E2 P Q R :
  P  pvs E1 E2 Q  (P  (Q - R))  pvs E1 E2 R.
Proof. rewrite comm. apply pvs_wand_l. Qed.
Ralf Jung's avatar
Ralf Jung committed
155

156 157 158
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's avatar
Robbert Krebbers committed
159
  intros HE1 HE2 HEE.
160
  rewrite (pvs_mask_frame _ _ (E1  E1')); last set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  by rewrite {2}HEE -!union_difference_L.
162
Qed. 
Ralf Jung's avatar
Ralf Jung committed
163 164 165 166 167 168

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.

169
(** It should be possible to give a stronger version of this rule
Ralf Jung's avatar
Ralf Jung committed
170 171
   that does not force the conclusion view shift to have twice the
   same mask. However, even expressing the side-conditions on the
172
   mask becomes really ugly then, and we have not found an instance
Ralf Jung's avatar
Ralf Jung committed
173
   where that would be useful. *)
Ralf Jung's avatar
Ralf Jung committed
174 175
Lemma pvs_trans3 E1 E2 Q :
  E2  E1  pvs E1 E2 (pvs E2 E2 (pvs E2 E1 Q))  pvs E1 E1 Q.
176
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
Ralf Jung's avatar
Ralf Jung committed
177

Robbert Krebbers's avatar
Robbert Krebbers committed
178
Lemma pvs_mask_weaken E1 E2 P : E1  E2  pvs E1 E1 P  pvs E2 E2 P.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
Proof. auto using pvs_mask_frame'. Qed.
Ralf Jung's avatar
Ralf Jung committed
180

181
Lemma pvs_ownG_update E m m' : m ~~> m'  ownG m  pvs E E (ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Proof.
183
  intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185
  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.
Ralf Jung's avatar
Ralf Jung committed
186

Robbert Krebbers's avatar
Robbert Krebbers committed
187
End pvs.
188 189 190 191 192 193

(** * 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. *)
194 195
Notation FSA Λ Σ A := (coPset  (A  iProp Λ Σ)  iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
196 197 198 199 200 201
  fsa_mask_frame_mono E1 E2 Φ Ψ :
    E1  E2  ( a, Φ a  Ψ a)  fsa E1 Φ  fsa E2 Ψ;
  fsa_trans3 E Φ : pvs E E (fsa E (λ a, pvs E E (Φ a)))  fsa E Φ;
  fsa_open_close E1 E2 Φ :
    fsaV  E2  E1  pvs E1 E2 (fsa E2 (λ a, pvs E2 E1 (Φ a)))  fsa E1 Φ;
  fsa_frame_r E P Φ : (fsa E Φ  P)  fsa E (λ a, Φ a  P)
202 203
}.

204 205
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
206
Implicit Types Φ Ψ : A  iProp Λ Σ.
207

208
Lemma fsa_mono E Φ Ψ : ( a, Φ a  Ψ a)  fsa E Φ  fsa E Ψ.
209
Proof. apply fsa_mask_frame_mono; auto. Qed.
210
Lemma fsa_mask_weaken E1 E2 Φ : E1  E2  fsa E1 Φ  fsa E2 Φ.
211
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
212
Lemma fsa_frame_l E P Φ : (P  fsa E Φ)  fsa E (λ a, P  Φ a).
213
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
214
Lemma fsa_strip_pvs E P Φ : P  fsa E Φ  pvs E E P  fsa E Φ.
215
Proof.
216 217
  move=>->. rewrite -{2}fsa_trans3.
  apply pvs_mono, fsa_mono=>a; apply pvs_intro.
218
Qed.
219 220
Lemma fsa_mono_pvs E Φ Ψ : ( a, Φ a  pvs E E (Ψ a))  fsa E Φ  fsa E Ψ.
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
221 222
End fsa.

223
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, pvs E E (Φ ()).
224
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
225
Proof.
226 227
  rewrite /pvs_fsa.
  split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
228
Qed.