proto_model.v 15.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(** This file defines the model of Dependent Separation Protocols,
along with various operations on the connective, such as append
and map.

Dependent Separation Protocols can ultimately be expressed as:
proto := 1 + (B * (V -> (▶ proto -> PROP) -> PROP))

Here the left-hand side of the sum is the terminal protocol
[proto_end], while the right-hand side is [proto_message],
where B is the canonical representation of actions determining
whether the protocol sends or receives, and
(V -> (▶ proto -> PROP) -> PROP) is a continuation that
depends on a communicated value V and the dependent tail
(▶ proto -> PROP) from protocols guarded under laters,
 to the propositions of the logic.

The type is defined as a solution to a recursive domain
equation, as it is self-referential under the guard of ▶.
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
21
22
23
24
25
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import cofe_solver.
Set Default Proof Using "Type".

Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
31
32
33
34
Module Export action.
  Inductive action := Send | Receive.
  Instance action_inhabited : Inhabited action := populate Send.
  Definition action_dual (a : action) : action :=
    match a with Send => Receive | Receive => Send end.
  Instance action_dual_involutive : Involutive (=) action_dual.
  Proof. by intros []. Qed.
  Canonical Structure actionO := leibnizO action.
End action.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

Definition protoOF_helper (V : Type) (PROPn PROP : ofeT) : oFunctor :=
  optionOF (actionO * (V -d> (  -n> PROPn) -n> PROP)).
Definition proto_result (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} :
  solution (protoOF_helper V PROPn PROP) := solver.result _.
Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
  proto_result V PROPn PROP.
Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
Proof. apply _. Qed.

Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
    protoOF_helper V PROPn PROP (proto V PROPn PROP) _ -n> proto V PROPn PROP :=
  solution_fold (proto_result V PROPn PROP).
Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
    proto V PROPn PROP -n> protoOF_helper V PROPn PROP (proto V PROPn PROP) _ :=
  solution_unfold (proto_result V PROPn PROP).

Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
  proto_fold (proto_unfold p)  p.
Proof. apply solution_fold_unfold. Qed.
Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
    (p : protoOF_helper V PROPn PROP (proto V PROPn PROP) _) :
  proto_unfold (proto_fold p)  p.
Proof. apply solution_unfold_fold. Qed.

Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
  proto_fold None.
Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
    (pc : V  (laterO (proto V PROPn PROP) -n> PROPn) -n> PROP) : proto V PROPn PROP :=
  proto_fold (Some (a, pc)).

Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
  Proper (pointwise_relation V (dist n) ==> dist n)
         (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
  Proper (pointwise_relation V () ==> ())
         (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.

Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
  p  proto_end   a pc, p  proto_message a pc.
Proof.
  destruct (proto_unfold p) as [[a pc]|] eqn:E; simpl in *; last first.
  - left. by rewrite -(proto_fold_unfold p) E.
  - right. exists a, pc. by rewrite -(proto_fold_unfold p) E.
Qed.
Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
  Inhabited (proto V PROPn PROP) := populate proto_end.

Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
87
88
89
90
91
92
93
94
95
96
97
98
Lemma proto_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 pc1 pc2 :
  proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 pc1  proto_message a2 pc2
  @{SPROP}  a1 = a2   ( v, pc1 v  pc2 v).
Proof.
  trans (proto_unfold (proto_message a1 pc1)  proto_unfold (proto_message a2 pc2) : SPROP)%I.
  { iSplit.
    - iIntros "Heq". by iRewrite "Heq".
    - iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
      iRewrite "Heq". by rewrite proto_fold_unfold. }
  rewrite /proto_message !proto_unfold_fold bi.option_equivI bi.prod_equivI /=.
  by rewrite bi.discrete_fun_equivI bi.discrete_eq.
Qed.

Definition proto_cont_map
Robbert Krebbers's avatar
Robbert Krebbers committed
99
   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP', !Cofe A, !Cofe B}
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103
    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') (h : A -n> B) :
    ((laterO A -n> PROPn) -n> PROP) -n> (laterO B -n> PROPn') -n> PROP' :=
  ofe_morO_map (ofe_morO_map (laterO_map h) gn) g.

Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
(** Append *)
Program Definition proto_app_flipped_aux {V} `{!Cofe PROPn, !Cofe PROP}
    (p2 : proto V PROPn PROP) (rec : proto V PROPn PROP -n> proto V PROPn PROP) :
    proto V PROPn PROP -n> proto V PROPn PROP := λne p1,
  match proto_unfold p1 return _ with
  | None => p2
  | Some (a, c) => proto_message a (proto_cont_map cid cid rec  c)
  end.
Next Obligation.
  intros V PROPn ? PROP ? rec n p2 p1 p1' Hp.
  apply (ofe_mor_ne _ _ proto_unfold) in Hp.
  destruct Hp as [[??][??] [-> ?]|]; simplify_eq/=; last done.
  f_equiv=> v /=. by f_equiv.
Qed.

Instance proto_app_flipped_aux_contractive {V} `{!Cofe PROPn, !Cofe PROP}
  (p2 : proto V PROPn PROP) : Contractive (proto_app_flipped_aux p2).
Proof.
  intros n rec1 rec2 Hrec p1. simpl.
  destruct (proto_unfold p1) as [[a c]|]; last done.
  f_equiv=> v /=. do 2 f_equiv.
  intros=> p'. apply Next_contractive. destruct n as [|n]=> //=.
Qed.

Definition proto_app_flipped {V} `{!Cofe PROPn, !Cofe PROP}
    (p2 : proto V PROPn PROP) : proto V PROPn PROP -n> proto V PROPn PROP :=
  fixpoint (proto_app_flipped_aux p2).
Definition proto_app {V} `{!Cofe PROPn, !Cofe PROP}
  (p1 p2 : proto V PROPn PROP) : proto V PROPn PROP := proto_app_flipped p2 p1.
Instance: Params (@proto_app) 5.

Lemma proto_app_flipped_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP):
  proto_app_flipped p2 p1  proto_app_flipped_aux p2 (proto_app_flipped p2) p1.
Proof. apply (fixpoint_unfold (proto_app_flipped_aux p2)). Qed.
Lemma proto_app_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP):
  proto_app (V:=V) p1 p2  proto_app_flipped_aux p2 (proto_app_flipped p2) p1.
Proof. apply (fixpoint_unfold (proto_app_flipped_aux p2)). Qed.

Lemma proto_app_end_l {V} `{!Cofe PROPn, !Cofe PROP} (p2 : proto V PROPn PROP) :
  proto_app proto_end p2  p2.
Proof.
  rewrite proto_app_unfold /proto_end /=.
  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
  by destruct (proto_unfold (proto_fold None))
    as [[??]|] eqn:E; rewrite E; inversion Hfold.
Qed.
Lemma proto_app_message {V} `{!Cofe PROPn, !Cofe PROP} a c (p2 : proto V PROPn PROP) :
  proto_app (proto_message a c) p2
   proto_message a (proto_cont_map cid cid (proto_app_flipped p2)  c).
Proof.
  rewrite proto_app_unfold /proto_message /=.
  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) (Some (a, c))) as Hfold.
  destruct (proto_unfold (proto_fold (Some (a, c))))
    as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
  rewrite /proto_message. do 3 f_equiv. intros v=> /=.
  apply equiv_dist=> n. f_equiv. by apply equiv_dist.
Qed.

Instance proto_app_ne {V} `{!Cofe PROPn, !Cofe PROP} :
  NonExpansive2 (proto_app (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
Proof.
  intros n p1 p1' Hp1 p2 p2' Hp2. rewrite /proto_app -Hp1 {p1' Hp1}.
  revert p1. induction (lt_wf n) as [n _ IH]=> p1 /=.
  rewrite !proto_app_flipped_unfold /proto_app_flipped_aux /=.
  destruct (proto_unfold p1) as [[a c]|]; last done.
  f_equiv=> v f /=. do 2 f_equiv. intros p. apply Next_contractive.
  destruct n as [|n]=> //=. apply IH; first lia; auto using dist_S.
Qed.
Instance proto_app_proper {V} `{!Cofe PROPn, !Cofe PROP} :
  Proper (() ==> () ==> ()) (proto_app (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
Proof. apply (ne_proper_2 _). Qed.

Lemma proto_app_end_r {V} `{!Cofe PROPn, !Cofe PROP} (p1 : proto V PROPn PROP) :
  proto_app p1 proto_end  p1.
Proof.
  apply equiv_dist=> n. revert p1. induction (lt_wf n) as [n _ IH]=> p1 /=.
  destruct (proto_case p1) as [->|(a & c & ->)].
  - by rewrite !proto_app_end_l.
  - rewrite !proto_app_message /=. f_equiv=> v c' /=. f_equiv=> p' /=. f_equiv.
    apply Next_contractive. destruct n as [|n]=> //=.
    apply IH; first lia; auto using dist_S.
Qed.
Lemma proto_app_assoc {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 p3 : proto V PROPn PROP) :
  proto_app p1 (proto_app p2 p3)  proto_app (proto_app p1 p2) p3.
Proof.
  apply equiv_dist=> n. revert p1. induction (lt_wf n) as [n _ IH]=> p1 /=.
  destruct (proto_case p1) as [->|(a & c & ->)].
  - by rewrite !proto_app_end_l.
  - rewrite !proto_app_message /=. f_equiv=> v c' /=. f_equiv=> p' /=. f_equiv.
    apply Next_contractive. destruct n as [|n]=> //=.
    apply IH; first lia; auto using dist_S.
Qed.

(** Functor *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Program Definition proto_map_aux {V}
   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f : action  action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
    (rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
    proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
  match proto_unfold p return _ with
  | None => proto_end
  | Some (a, c) => proto_message (f a) (proto_cont_map gn g rec  c)
  end.
Next Obligation.
  intros V PROPn ? PROPn' ? PROP ? PROP' ? f g1 g2 rec n p1 p2 Hp.
  apply (ofe_mor_ne _ _ proto_unfold) in Hp.
  destruct Hp as [[??][??] [-> ?]|]; simplify_eq/=; last done.
  f_equiv=> v /=. by f_equiv.
Qed.
Instance proto_map_aux_contractive {V}
   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f : action  action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
  Contractive (proto_map_aux (V:=V) f gn g).
Proof.
  intros n rec1 rec2 Hrec p. simpl.
  destruct (proto_unfold p) as [[a c]|]; last done.
  f_equiv=> v /=. do 2 f_equiv.
  intros=> p'. apply Next_contractive. destruct n as [|n]=> //=.
Qed.
Definition proto_map {V}
   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f : action  action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
    proto V PROPn PROP -n> proto V PROPn' PROP' :=
  fixpoint (proto_map_aux f gn g).

Lemma proto_map_unfold {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f : action  action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
  proto_map (V:=V) f gn g p  proto_map_aux f gn g (proto_map f gn g) p.
Proof. apply (fixpoint_unfold (proto_map_aux f gn g)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
Robbert Krebbers's avatar
Robbert Krebbers committed
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
    (f : action  action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
  proto_map (V:=V) f gn g proto_end  proto_end.
Proof.
  rewrite proto_map_unfold /proto_end /=.
  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
  by destruct (proto_unfold (proto_fold None))
    as [[??]|] eqn:E; rewrite E; inversion Hfold.
Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f : action  action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a c :
  proto_map (V:=V) f gn g (proto_message a c)  proto_message (f a) (proto_cont_map gn g (proto_map f gn g)  c).
Proof.
  rewrite proto_map_unfold /proto_message /=.
  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) (Some (a, c))) as Hfold.
  destruct (proto_unfold (proto_fold (Some (a, c))))
    as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
  rewrite /proto_message. do 3 f_equiv. intros v=> /=.
  apply equiv_dist=> n. f_equiv. by apply equiv_dist.
Qed.

Lemma proto_map_ne {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f1 f2 : action  action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
  ( a, f1 a = f2 a)  ( x, gn1 x {n} gn2 x)  ( x, g1 x {n} g2 x) 
  proto_map (V:=V) f1 gn1 g1 p {n} proto_map (V:=V) f2 gn2 g2 p.
Proof.
  intros Hf. revert p. induction (lt_wf n) as [n _ IH]=> p Hgn Hg /=.
  destruct (proto_case p) as [->|(a & c & ->)].
  - by rewrite !proto_map_end.
  - rewrite !proto_map_message /= Hf. f_equiv=> v /=. do 2 (f_equiv; last done).
    intros p'. apply Next_contractive. destruct n as [|n]=> //=.
    apply IH; first lia; auto using dist_S.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f1 f2 : action  action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
  ( a, f1 a = f2 a)  ( x, gn1 x  gn2 x)  ( x, g1 x  g2 x) 
  proto_map (V:=V) f1 gn1 g1 p  proto_map (V:=V) f2 gn2 g2 p.
Proof.
  intros Hf Hgn Hg. apply equiv_dist=> n.
  apply proto_map_ne=> // ?; by apply equiv_dist.
Qed.
Lemma proto_map_id {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
  proto_map id cid cid p  p.
Proof.
  apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
  destruct (proto_case p) as [->|(a & c & ->)].
  - by rewrite !proto_map_end.
  - rewrite !proto_map_message /=. f_equiv=> v c' /=. f_equiv=> p' /=. f_equiv.
    apply Next_contractive. destruct n as [|n]=> //=.
    apply IH; first lia; auto using dist_S.
Qed.
Lemma proto_map_compose {V}
   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROPn'', !Cofe PROP, !Cofe PROP', !Cofe PROP''}
    (f1 f2 : action  action)
    (gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
    (g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
  proto_map (f2  f1) (gn2  gn1) (g2  g1) p  proto_map f2 gn1 g2 (proto_map f1 gn2 g1 p).
Proof.
  apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
  destruct (proto_case p) as [->|(a & c & ->)].
  - by rewrite !proto_map_end.
  - rewrite !proto_map_message /=. f_equiv=> v c' /=. do 3 f_equiv. move=> p' /=.
    do 3 f_equiv. apply Next_contractive. destruct n as [|n]=> //=.
    apply IH; first lia; auto using dist_S.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
299
300
301
302
303
304
305
306
307
308
309
310
311
312
Lemma proto_map_app {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
    (f : action  action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p1 p2 :
  proto_map (V:=V) f gn g (proto_app p1 p2)
   proto_app (proto_map (V:=V) f gn g p1) (proto_map (V:=V) f gn g p2).
Proof.
  apply equiv_dist=> n. revert p1 p2. induction (lt_wf n) as [n _ IH]=> p1 p2 /=.
  destruct (proto_case p1) as [->|(a & c & ->)].
  - by rewrite proto_map_end !proto_app_end_l.
  - rewrite proto_map_message !proto_app_message proto_map_message /=.
    f_equiv=> v c' /=. do 2 f_equiv. move=> p' /=. do 2 f_equiv.
    apply Next_contractive. destruct n as [|n]=> //=.
    apply IH; first lia; auto using dist_S.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
Program Definition protoOF (V : Type) (Fn F : oFunctor)
    `{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
    `{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} : oFunctor := {|
  oFunctor_car A _ B _ := proto V (oFunctor_car Fn B A) (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    proto_map id (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F fg)
|}.
Next Obligation.
  intros V Fn F ?? A1 ? A2 ? B1 ? B2 ? n f g [??] p; simpl in *.
  apply proto_map_ne=> // y; by apply oFunctor_ne.
Qed.
Next Obligation.
  intros V Fn F ?? A ? B ? p; simpl in *. rewrite /= -{2}(proto_map_id p).
  apply proto_map_ext=> //= y; by rewrite oFunctor_id.
Qed.
Next Obligation.
  intros V Fn F ?? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' p; simpl in *.
  rewrite -proto_map_compose.
  apply proto_map_ext=> //= y; by rewrite oFunctor_compose.
Qed.

Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
    `{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
    `{! A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
  oFunctorContractive Fn  oFunctorContractive F  
  oFunctorContractive (protoOF V Fn F).
Proof.
  intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
  apply proto_map_ne=> //= y.
  - destruct n; [|destruct Hfg]; by apply oFunctor_contractive.
  - destruct n; [|destruct Hfg]; by apply oFunctor_contractive.
Qed.