resources.v 10.3 KB
Newer Older
1
2
3
From iris.algebra Require Export fin_maps agree excl.
From iris.algebra Require Import upred.
From iris.program_logic Require Export language.
4

5
Record res (Λ : language) (A : cofeT) (M : cmraT) := Res {
6
  wld : mapR positive (agreeR A);
7
  pst : exclR (stateC Λ);
8
  gst : M;
9
10
}.
Add Printing Constructor res.
11
12
13
14
15
16
17
18
Arguments Res {_ _ _} _ _ _.
Arguments wld {_ _ _} _.
Arguments pst {_ _ _} _.
Arguments gst {_ _ _} _.
Instance: Params (@Res) 3.
Instance: Params (@wld) 3.
Instance: Params (@pst) 3.
Instance: Params (@gst) 3.
19
20

Section res.
21
22
Context {Λ : language} {A : cofeT} {M : cmraT}.
Implicit Types r : res Λ A M.
23

24
Inductive res_equiv' (r1 r2 : res Λ A M) := Res_equiv :
25
  wld r1  wld r2  pst r1  pst r2  gst r1  gst r2  res_equiv' r1 r2.
26
27
Instance res_equiv : Equiv (res Λ A M) := res_equiv'.
Inductive res_dist' (n : nat) (r1 r2 : res Λ A M) := Res_dist :
28
  wld r1 {n} wld r2  pst r1 {n} pst r2  gst r1 {n} gst r2 
29
  res_dist' n r1 r2.
30
Instance res_dist : Dist (res Λ A M) := res_dist'.
31
Global Instance Res_ne n :
32
  Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ A M).
33
Proof. done. Qed.
34
Global Instance Res_proper : Proper (() ==> () ==> () ==> ()) (@Res Λ A M).
35
Proof. done. Qed.
36
Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ A M).
37
Proof. by destruct 1. Qed.
38
Global Instance wld_proper : Proper (() ==> ()) (@wld Λ A M).
39
Proof. by destruct 1. Qed.
40
Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ A M).
41
Proof. by destruct 1. Qed.
42
Global Instance pst_ne' n : Proper (dist n ==> ()) (@pst Λ A M).
43
Proof. destruct 1; apply: timeless; apply dist_le with n; auto with lia. Qed.
44
Global Instance pst_proper : Proper (() ==> (=)) (@pst Λ A M).
45
Proof. by destruct 1; unfold_leibniz. Qed.
46
Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ A M).
47
Proof. by destruct 1. Qed.
48
Global Instance gst_proper : Proper (() ==> ()) (@gst Λ A M).
49
Proof. by destruct 1. Qed.
50
Instance res_compl : Compl (res Λ A M) := λ c,
51
52
  Res (compl (chain_map wld c))
      (compl (chain_map pst c)) (compl (chain_map gst c)).
53
Definition res_cofe_mixin : CofeMixin (res Λ A M).
54
55
Proof.
  split.
56
  - intros w1 w2; split.
57
58
    + by destruct 1; constructor; apply equiv_dist.
    + by intros Hw; constructor; apply equiv_dist=>n; destruct (Hw n).
59
  - intros n; split.
60
61
    + done.
    + by destruct 1; constructor.
62
    + do 2 destruct 1; constructor; etrans; eauto.
63
  - by destruct 1; constructor; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
  - intros n c; constructor.
    + apply (conv_compl n (chain_map wld c)).
    + apply (conv_compl n (chain_map pst c)).
    + apply (conv_compl n (chain_map gst c)).
68
69
70
71
Qed.
Canonical Structure resC : cofeT := CofeT res_cofe_mixin.
Global Instance res_timeless r :
  Timeless (wld r)  Timeless (gst r)  Timeless r.
72
Proof. by destruct 3; constructor; try apply: timeless. Qed.
73

74
Instance res_op : Op (res Λ A M) := λ r1 r2,
75
  Res (wld r1  wld r2) (pst r1  pst r2) (gst r1  gst r2).
76
Global Instance res_empty `{Empty M} : Empty (res Λ A M) := Res   .
Ralf Jung's avatar
Ralf Jung committed
77
78
Instance res_core : Core (res Λ A M) := λ r,
  Res (core (wld r)) (core (pst r)) (core (gst r)).
79
80
Instance res_valid : Valid (res Λ A M) := λ r,  wld r   pst r   gst r.
Instance res_validN : ValidN (res Λ A M) := λ n r,
81
  {n} wld r  {n} pst r  {n} gst r.
82

83
Lemma res_included (r1 r2 : res Λ A M) :
84
85
86
  r1  r2  wld r1  wld r2  pst r1  pst r2  gst r1  gst r2.
Proof.
  split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
87
  intros [r Hr]; split_and?;
88
89
    [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
Qed.
90
Lemma res_includedN (r1 r2 : res Λ A M) n :
91
92
93
  r1 {n} r2  wld r1 {n} wld r2  pst r1 {n} pst r2  gst r1 {n} gst r2.
Proof.
  split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
94
  intros [r Hr]; split_and?;
95
96
    [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
Qed.
97
Definition res_cmra_mixin : CMRAMixin (res Λ A M).
98
99
Proof.
  split.
100
101
102
103
104
105
  - by intros n x [???] ? [???]; constructor; cofe_subst.
  - by intros n [???] ? [???]; constructor; cofe_subst.
  - by intros n [???] ? [???] (?&?&?); split_and!; cofe_subst.
  - intros r; split.
    + intros (?&?&?) n; split_and!; by apply cmra_valid_validN.
    + intros Hr; split_and!; apply cmra_valid_validN=> n; apply Hr.
106
  - by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
107
108
  - by intros ???; constructor; rewrite /= assoc.
  - by intros ??; constructor; rewrite /= comm.
Ralf Jung's avatar
Ralf Jung committed
109
110
  - by intros ?; constructor; rewrite /= cmra_core_l.
  - by intros ?; constructor; rewrite /= cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  - intros r1 r2; rewrite !res_included.
Ralf Jung's avatar
Ralf Jung committed
112
    by intros (?&?&?); split_and!; apply cmra_core_preserving.
113
  - intros n r1 r2 (?&?&?);
114
      split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
115
116
117
118
119
  - intros n r r1 r2 (?&?&?) [???]; simpl in *.
    destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
      (cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
      (cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
    by exists (Res w σ m, Res w' σ' m').
120
Qed.
121
Canonical Structure resR : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
Ralf Jung's avatar
Ralf Jung committed
122
Global Instance res_cmra_unit `{CMRAUnit M} : CMRAUnit resR.
123
124
Proof.
  split.
Ralf Jung's avatar
Ralf Jung committed
125
  - split_and!; apply cmra_unit_valid.
126
127
  - by split; rewrite /= left_id.
  - apply _.
128
Qed.
129

130
Definition update_pst (σ : state Λ) (r : res Λ A M) : res Λ A M :=
131
  Res (wld r) (Excl σ) (gst r).
132
Definition update_gst (m : M) (r : res Λ A M) : res Λ A M :=
133
  Res (wld r) (pst r) m.
134

135
Lemma wld_validN n r : {n} r  {n} wld r.
136
Proof. by intros (?&?&?). Qed.
137
Lemma gst_validN n r : {n} r  {n} gst r.
138
139
140
141
Proof. by intros (?&?&?). Qed.
Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
  Res w1 σ1 m1  Res w2 σ2 m2 = Res (w1  w2) (σ1  σ2) (m1  m2).
Proof. done. Qed.
Ralf Jung's avatar
Ralf Jung committed
142
Lemma Res_core w σ m : core (Res w σ m) = Res (core w) (core σ) (core m).
143
144
Proof. done. Qed.
Lemma lookup_wld_op_l n r1 r2 i P :
145
  {n} (r1r2)  wld r1 !! i {n} Some P  (wld r1  wld r2) !! i {n} Some P.
146
147
Proof.
  move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
148
  destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  by constructor; rewrite (agree_op_inv _ P P') // agree_idemp.
150
151
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
152
  {n} (r1r2)  wld r2 !! i {n} Some P  (wld r1  wld r2) !! i {n} Some P.
153
Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
154
Global Instance Res_timeless eσ m : Timeless m  Timeless (@Res Λ A M  eσ m).
155
Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
156
157
Global Instance Res_persistent w m: Persistent m  Persistent (@Res Λ A M w  m).
Proof. constructor; apply (persistent _). Qed.
158
159

(** Internalized properties *)
160
Lemma res_equivI {M'} r1 r2 :
161
162
  (r1  r2)
   (wld r1  wld r2  pst r1  pst r2  gst r1  gst r2: uPred M').
163
164
165
Proof.
  uPred.unseal. do 2 split. by destruct 1. by intros (?&?&?); by constructor.
Qed.
166
Lemma res_validI {M'} r : ( r)  ( wld r   pst r   gst r : uPred M').
167
Proof. by uPred.unseal. Qed.
168
End res.
169
170

Arguments resC : clear implicits.
171
Arguments resR : clear implicits.
172

173
174
175
(* Functor *)
Definition res_map {Λ} {A A' : cofeT} {M M' : cmraT}
    (f : A  A') (g : M  M') (r : res Λ A M) : res Λ A' M' :=
176
  Res (agree_map f <$> wld r) (pst r) (g $ gst r).
177
178
179
180
181
Instance res_map_ne {Λ} {A A': cofeT} {M M' : cmraT} (f : A  A') (g : M  M') :
  ( n, Proper (dist n ==> dist n) f)  ( n, Proper (dist n ==> dist n) g) 
   n, Proper (dist n ==> dist n) (@res_map Λ _ _ _ _ f g).
Proof. intros Hf n [] ? [???]; constructor; by cofe_subst. Qed.
Lemma res_map_id {Λ A M} (r : res Λ A M) : res_map id id r  r.
182
Proof.
183
184
185
  constructor; rewrite /res_map /=; f_equal.
  - rewrite -{2}(map_fmap_id (wld r)). apply map_fmap_setoid_ext=> i y ? /=.
    by rewrite -{2}(agree_map_id y).
186
Qed.
187
188
189
Lemma res_map_compose {Λ} {A1 A2 A3 : cofeT} {M1 M2 M3 : cmraT}
   (f : A1  A2) (f' : A2  A3) (g : M1  M2) (g' : M2  M3) (r : res Λ A1 M1) :
  res_map (f'  f) (g'  g) r  res_map f' g' (res_map f g r).
190
Proof.
191
  constructor; rewrite /res_map /=; f_equal.
192
  - rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
193
    by rewrite -agree_map_compose.
194
Qed.
195
196
197
Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : cmraT}
    (f f' : A  A') (g g' : M  M') (r : res Λ A M) :
  ( x, f x  f' x)  ( m, g m  g' m)  res_map f g r  res_map f' g' r.
198
Proof.
199
  intros Hf Hg; split; simpl; auto.
200
  - by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
201
Qed.
202
203
204
205
Instance res_map_cmra_monotone {Λ}
    {A A' : cofeT} {M M': cmraT} (f: A  A') (g: M  M') :
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone g 
  CMRAMonotone (@res_map Λ _ _ _ _ f g).
206
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
  split; first apply _.
208
  - intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
  - by intros r1 r2; rewrite !res_included;
210
      intros (?&?&?); split_and!; simpl; try apply: included_preserving.
211
Qed.
212
213
214
215
216
Definition resC_map {Λ} {A A' : cofeT} {M M' : cmraT}
    (f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
  CofeMor (res_map f g : resC Λ A M  resC Λ A' M').
Instance resC_map_ne {Λ A A' M M'} n :
  Proper (dist n ==> dist n ==> dist n) (@resC_map Λ A A' M M').
217
Proof.
218
  intros f g Hfg r; split; simpl; auto.
219
  - by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
220
Qed.
Ralf Jung's avatar
Ralf Jung committed
221

222
Program Definition resRF (Λ : language)
223
224
225
    (F1 : cFunctor) (F2 : rFunctor) : rFunctor := {|
  rFunctor_car A B := resR Λ (cFunctor_car F1 A B) (rFunctor_car F2 A B);
  rFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F1 fg) (rFunctor_map F2 fg)
Ralf Jung's avatar
Ralf Jung committed
226
|}.
227
228
229
230
231
Next Obligation.
  intros Λ F1 F2 A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
  - by apply cFunctor_ne.
  - by apply rFunctor_ne.
Qed.
232
233
234
235
236
237
238
239
Next Obligation.
  intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).
  apply res_map_ext=>y. apply cFunctor_id. apply rFunctor_id.
Qed.
Next Obligation.
  intros Λ F Σ A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -res_map_compose.
  apply res_map_ext=>y. apply cFunctor_compose. apply rFunctor_compose.
Qed.
240
241
242
243
244
245
246
247
248

Instance resRF_contractive Λ F1 F2 :
  cFunctorContractive F1  rFunctorContractive F2 
  rFunctorContractive (resRF Λ F1 F2).
Proof.
  intros ?? A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
  - by apply cFunctor_contractive.
  - by apply rFunctor_contractive.
Qed.