Commit deb6d9e5 authored by Robbert Krebbers's avatar Robbert Krebbers

Large refactoring.

- Protocols are no longer contractive in the message
- New type `iMsg` for messages to avoid telescopes in protocols
- Better rules for subprotocols that do not involve telescopes, but allow introduction
  and elimination of quantifiers and the payload
- Better notations for protocols
- Notation ⊑ for subprotocols
- Make ⊑ except-0 so one can strip laters when proving a ⊑
- Restore recursive domain equation to push later inwards to support protocols
  that are not contractive in the mssage.
- Proofmode support for easy manipulation of ⊑
parent 4aba4857
Pipeline #27440 passed with stage
in 5 minutes and 43 seconds
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -8,7 +8,7 @@ Important: This file should not be used directly, but rather the wrappers in
Dependent Separation Protocols are modeled as the solution of the following
recursive domain equation:
[proto = 1 + (action * ▶ (V → proto → PROP))]
[proto = 1 + (action * (V → ▶ proto → PROP))]
Here, the left-hand side of the sum is used for the terminated process, while
the right-hand side is used for the communication constructors. The type
......@@ -16,7 +16,7 @@ the right-hand side is used for the communication constructors. The type
[Recv]. Compared to having an additional sum in [proto], this makes it
possible to factorize the code in a better way.
The remainder [▶ (V → proto → PROP)] is a predicate that ranges over the
The remainder [V → ▶ proto → PROP] is a predicate that ranges over the
communicated value [V] and the tail protocol [proto]. Note that to solve this
recursive domain equation using Iris's COFE solver, the recursive occurrence
of [proto] appear under the later [▶].
......@@ -49,9 +49,9 @@ Module Export action.
End action.
Definition proto_auxO (V : Type) (PROP : ofeT) (A : ofeT) : ofeT :=
optionO (prodO actionO (laterO (V -d> A -n> PROP))).
optionO (prodO actionO (V -d> laterO A -n> PROP)).
Definition proto_auxOF (V : Type) (PROP : ofeT) : oFunctor :=
optionOF (actionO * (V -d> -n> PROP)).
optionOF (actionO * (V -d> -n> PROP)).
Definition proto_result (V : Type) := result_2 (proto_auxOF V).
Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
......@@ -77,23 +77,13 @@ Proof. apply (ofe_iso_21 proto_iso). 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 proto V PROP PROPn -n> PROP) : proto V PROPn PROP :=
proto_fold (Some (a, Next pc)).
(pc : V laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
proto_fold (Some (a, pc)).
Instance proto_message_contractive {V} `{!Cofe PROPn, !Cofe PROP} a n :
Proper (pointwise_relation V (dist_later n) ==> dist n)
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
Proof.
intros c1 c2 Hc. rewrite /proto_message. f_equiv. do 2 constructor=>//=.
apply Next_contractive. by destruct n.
Qed.
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. apply proto_message_contractive=> v.
by destruct n; [|apply dist_S].
Qed.
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).
......@@ -104,15 +94,14 @@ Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
Proof.
destruct (proto_unfold p) as [[a pc]|] eqn:E; simpl in *; last first.
- left. by rewrite -(proto_fold_unfold p) E.
- right. destruct (Next_uninj pc) as [pc' Hpc]. exists a, pc'.
by rewrite /proto_message -Hpc -E proto_fold_unfold.
- right. exists a, pc. by rewrite /proto_message -E proto_fold_unfold.
Qed.
Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
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 p', pc1 v p' pc2 v p').
@{SPROP} a1 = a2 ( v p', pc1 v p' pc2 v p').
Proof.
trans (proto_unfold (proto_message a1 pc1) proto_unfold (proto_message a2 pc2) : SPROP)%I.
{ iSplit.
......@@ -120,7 +109,7 @@ Proof.
- 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 /=.
rewrite bi.discrete_eq bi.later_equivI bi.discrete_fun_equivI.
rewrite bi.discrete_eq bi.discrete_fun_equivI.
by setoid_rewrite bi.ofe_morO_equivI.
Qed.
Lemma proto_message_end_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a pc :
......@@ -137,13 +126,13 @@ Proof. by rewrite bi.internal_eq_sym proto_message_end_equivI. Qed.
(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
is contractive *)
Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
(x : A) (f : action (V proto V PROP PROPn -n> PROP) A)
(x : A) (f : action (V laterO (proto V PROP PROPn) -n> PROP) A)
(p : proto V PROPn PROP) : A :=
match proto_unfold p with None => x | Some (a, pc) => f a (later_car pc) end.
match proto_unfold p with None => x | Some (a, pc) => f a pc end.
Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
(x : A) (f1 f2 : action (V proto V PROP PROPn -n> PROP) A) p1 p2 n :
( a pc1 pc2, ( v, dist_later n (pc1 v) (pc2 v)) f1 a pc1 {n} f2 a pc2)
(x : A) (f1 f2 : action (V laterO (proto V PROP PROPn) -n> PROP) A) p1 p2 n :
( a pc1 pc2, ( v, pc1 v {n} pc2 v) f1 a pc1 {n} f2 a pc2)
p1 {n} p2
proto_elim x f1 p1 {n} proto_elim x f2 p2.
Proof.
......@@ -154,7 +143,7 @@ Proof.
Qed.
Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
(x : A) (f : action (V proto V PROP PROPn -n> PROP) A) :
(x : A) (f : action (V laterO (proto V PROP PROPn) -n> PROP) A) :
proto_elim x f proto_end x.
Proof.
rewrite /proto_elim /proto_end.
......@@ -162,14 +151,14 @@ Proof.
by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
Qed.
Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
(x : A) (f : action (V proto V PROP PROPn -n> PROP) A)
(x : A) (f : action (V laterO (proto V PROP PROPn) -n> PROP) A)
`{Hf : a, Proper (pointwise_relation _ () ==> ()) (f a)} a pc :
proto_elim x f (proto_message a pc) f a pc.
Proof.
rewrite /proto_elim /proto_message /=.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
(PROP:=PROP) (Some (a, Next pc))) as Hfold.
destruct (proto_unfold (proto_fold (Some (a, Next pc))))
(PROP:=PROP) (Some (a, pc))) as Hfold.
destruct (proto_unfold (proto_fold (Some (a, pc))))
as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
by f_equiv=> v.
Qed.
......@@ -178,12 +167,10 @@ Qed.
Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
proto_elim proto_end (λ a pc, proto_message a (λ v, g pc v rec)) p.
proto_elim proto_end (λ a pc, proto_message a (λ v, g pc v laterO_map rec)) p.
Next Obligation.
intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
apply proto_elim_ne=> // a pc1 pc2 Hpc.
apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
do 2 f_equiv. apply Hpc.
apply proto_elim_ne=> // a pc1 pc2 Hpc. by repeat f_equiv.
Qed.
Instance proto_map_aux_contractive {V}
......@@ -191,8 +178,8 @@ Instance proto_map_aux_contractive {V}
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
Proof.
intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a pc1 pc2 Hpc.
apply proto_message_contractive; destruct n as [|n]=> // v p'; simpl in *.
by rewrite (Hrec p') (Hpc _ (rec2 _)).
f_equiv=> v p' /=. do 2 f_equiv; [done|].
apply Next_contractive; destruct n as [|n]=> //=.
Qed.
Definition proto_map_aux_2 {V}
......@@ -234,7 +221,7 @@ Proof. by rewrite proto_map_unfold /proto_map_aux /= proto_elim_end. Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a pc :
proto_map (V:=V) gn g (proto_message a pc)
proto_message a (λ v, g pc v proto_map g gn).
proto_message a (λ v, g pc v laterO_map (proto_map g gn)).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
apply: proto_elim_message=> a' pc1 pc2 Hpc; f_equiv; solve_proper.
......@@ -251,8 +238,8 @@ Proof.
PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
destruct (proto_case p) as [->|(a & pc & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
rewrite (dist_S _ _ _ (Hg _)) IH //; auto using dist_S with lia.
apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
apply Next_contractive; destruct n as [|n]=> //=; auto using dist_S with lia.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
......@@ -267,9 +254,8 @@ Proof.
apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
destruct (proto_case p) as [->|(a & pc & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
by rewrite IH; last lia.
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
apply Next_contractive; destruct n as [|n]=> //=; auto.
Qed.
Lemma proto_map_compose {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
......@@ -283,9 +269,8 @@ Proof.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
by rewrite IH; last lia.
rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
do 3 f_equiv. apply Next_contractive; destruct n as [|n]=> //=; auto.
Qed.
Program Definition protoOF (V : Type) (Fn F : oFunctor)
......
......@@ -112,34 +112,34 @@ Definition prot : iProto Σ :=
(<?> MSG #42; END)%proto.
Definition prot_ref : iProto Σ :=
(<?> l : loc, MSG #l {{ l #42 }}; END)%proto.
(<? (l : loc)> MSG #l {{ l #42 }}; END)%proto.
Definition prot_del : iProto Σ :=
(<?> c : val, MSG c {{ c prot }}; END)%proto.
(<? c> MSG c {{ c prot }}; END)%proto.
Definition prot_dep : iProto Σ :=
(<!> x : Z, MSG #x; <?> MSG #(x + 2); END)%proto.
(<! (x : Z)> MSG #x; <?> MSG #(x + 2); END)%proto.
Definition prot_dep_ref : iProto Σ :=
(<!> (l : loc) (x : Z), MSG #l {{ l #x }};
(<! (l : loc) (x : Z)> MSG #l {{ l #x }};
<?> MSG #() {{ l #(x + 2) }};
END)%proto.
Definition prot_dep_del : iProto Σ :=
(<?> c : val, MSG c {{ c prot_dep }}; END)%proto.
(<? c> MSG c {{ c prot_dep }}; END)%proto.
Definition prot_dep_del_2 : iProto Σ :=
(<!> c : val, MSG c {{ c prot_dep }};
(<! c> MSG c {{ c prot_dep }};
<?> MSG #() {{ c <?> MSG #42; END }};
END)%proto.
Definition prot_dep_del_3 : iProto Σ :=
(<!> c : val, MSG c {{ c prot_dep }};
<!> y : Z, MSG #y; <?> MSG #() {{ c <?> MSG #(y + 2); END }};
(<! c> MSG c {{ c prot_dep }};
<! (y : Z)> MSG #y; <?> MSG #() {{ c <?> MSG #(y + 2); END }};
END)%proto.
Definition prot_loop_aux (rec : iProto Σ) : iProto Σ :=
(<!> x : Z, MSG #x; <?> MSG #(x + 2); rec)%proto.
(<! (x : Z)> MSG #x; <?> MSG #(x + 2); rec)%proto.
Instance prot_loop_contractive : Contractive prot_loop_aux.
Proof. solve_proto_contractive. Qed.
Definition prot_loop : iProto Σ := fixpoint prot_loop_aux.
......@@ -148,9 +148,9 @@ Global Instance prot_loop_unfold :
Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
Definition prot_fun : iProto Σ :=
(<!> (P : iProp Σ) (Φ : Z iProp Σ) (vf : val),
(<! (P : iProp Σ) (Φ : Z iProp Σ) (vf : val)>
MSG vf {{ {{{ P }}} vf #() {{{ x, RET #x; Φ x }}} }};
<?> (vg : val),
<? (vg : val)>
MSG vg {{ {{{ P }}} vg #() {{{ x, RET #(x + 2); Φ x }}} }};
END)%proto.
......@@ -161,13 +161,13 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
end%proto.
Definition prot_swap : iProto Σ :=
(<!> x : Z, MSG #x;
(<! (x : Z)> MSG #x;
<?> MSG #20;
<?> MSG #x; END)%proto.
Definition prot_swap_twice : iProto Σ :=
(<!> x : Z, MSG #x;
<!> y : Z, MSG #y;
(<! (x : Z)> MSG #x;
<! (y : Z)> MSG #y;
<?> MSG #20;
<?> MSG #(x+y); END)%proto.
......@@ -285,9 +285,9 @@ Proof.
c iProto_dual (prot_lock n))%I
with "[Hc Hs]"); first by eauto with iFrame.
iIntros (lk γlk) "#Hlk".
iAssert ( (client γ ε -
WP acquire lk;; send c #21;; release lk {{ _, True }}))%I as "#Hhelp".
{ iIntros "!> Hcl".
iAssert (client γ ε -
WP acquire lk;; send c #21;; release lk {{ _, True }})%I with "[]" as "#Hhelp".
{ iIntros "Hcl".
wp_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
iDestruct "H" as (n) "[Hs Hc]".
iDestruct (server_agree with "Hs Hcl") as %[? _].
......
......@@ -72,11 +72,11 @@ Section map.
nat -d> gmultiset A -d> iProto Σ := λ i X,
let rec : nat gmultiset A iProto Σ := rec in
(if i is 0 then END else
((<!> x v, MSG v {{ IA x v }}; rec i (X {[ x ]}))
((<! x v> MSG v {{ IA x v }}; rec i (X {[ x ]}))
<+>
rec (pred i) X
) <{ i 1 X = }&>
<?> x (l : loc), MSG #l {{ x X llist IB l (map x) }};
<? x (l : loc)> MSG #l {{ x X llist IB l (map x) }};
rec i (X {[ x ]}))%proto.
Instance par_map_protocol_aux_contractive : Contractive par_map_protocol_aux.
Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
......
......@@ -45,13 +45,13 @@ Section sort.
Context `{!heapG Σ, !chanG Σ}.
Definition sort_protocol {A} (I : A val iProp Σ) (R : A A Prop) : iProto Σ :=
(<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
<?> (xs' : list A), MSG #() {{ Sorted R xs' xs' xs llist I l xs' }};
(<! (xs : list A) (l : loc)> MSG #l {{ llist I l xs }};
<? (xs' : list A)> MSG #() {{ Sorted R xs' xs' xs llist I l xs' }};
END)%proto.
Definition sort_protocol_func : iProto Σ :=
(<!> A (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val),
(<! A (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val)>
MSG cmp {{ cmp_spec I R cmp }};
sort_protocol I R)%proto.
......
......@@ -60,7 +60,7 @@ Section sort_service_br_del.
Qed.
Definition sort_protocol_del_aux (rec : iProto Σ) : iProto Σ :=
((<?> c, MSG c {{ c sort_protocol I R }}; rec) <+> END)%proto.
((<? c> MSG c {{ c sort_protocol I R }}; rec) <+> END)%proto.
Instance sort_protocol_del_aux_contractive : Contractive sort_protocol_del_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_del : iProto Σ := fixpoint sort_protocol_del_aux.
......@@ -83,7 +83,7 @@ Section sort_service_br_del.
Qed.
Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c rec }}; rec) <+> END))%proto.
((sort_protocol I R <++> rec) <+> ((<? c> MSG c {{ c rec }}; rec) <+> END))%proto.
Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_br_del : iProto Σ := fixpoint sort_protocol_br_del_aux.
......
......@@ -79,7 +79,7 @@ Section sort_fg.
Definition sort_fg_tail_protocol_aux (xs : list A)
(rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ ys,
((<?> y v, MSG v {{ TlRel R y ys I y v }}; (rec : _ iProto Σ) (ys ++ [y]))
((<? y v> MSG v {{ TlRel R y ys I y v }}; rec (ys ++ [y]))
<&{ ys xs }> END)%proto.
Instance sort_fg_tail_protocol_aux_contractive xs :
......@@ -94,7 +94,7 @@ Section sort_fg.
Definition sort_fg_head_protocol_aux
(rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ xs,
((<!> x v, MSG v {{ I x v }}; (rec : _ iProto Σ) (xs ++ [x]))
((<! x v > MSG v {{ I x v }}; (rec : _ iProto Σ) (xs ++ [x]))
<+> sort_fg_tail_protocol xs [])%proto.
Instance sort_fg_head_protocol_aux_contractive :
......@@ -293,8 +293,8 @@ Section sort_fg.
End sort_fg_inner.
Definition sort_fg_func_protocol : iProto Σ :=
(<!> A (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val),
(<! A (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val)>
MSG cmp {{ cmp_spec I R cmp }};
sort_fg_head_protocol I R [])%proto.
......
......@@ -22,14 +22,14 @@ Section double.
Context `{heapG Σ, chanG Σ, inG Σ fracR, spawnG Σ}.
Definition prog_prot : iProto Σ :=
(<?> (x : Z), MSG #x; <?> (y : Z), MSG #y; END)%proto.
(<? (x : Z)> MSG #x; <? (y : Z)> MSG #y; END)%proto.
Definition chan_inv (c : val) (γ : gname) : iProp Σ :=
((c prog_prot)
(own γ (1/2)%Qp c (<?> (x : Z), MSG #x; END)%proto)
(c prog_prot
(own γ (1/2)%Qp c <? (x : Z)> MSG #x; END)
(own γ 1%Qp c END))%I.
Lemma wp_prog (c : val):
Lemma wp_prog c :
{{{ c prog_prot }}}
prog c
{{{ (k1 k2 : Z), RET (#k1, #k2); True }}}.
......@@ -93,13 +93,8 @@ Section double.
iIntros (c) "Hc".
iApply (wp_prog with "[Hc]").
{ iApply (iProto_mapsto_le _ (lsty_car (<??> lty_int; <??> lty_int; END)) with "Hc").
iApply iProto_le_recv.
iIntros "!> !> !>" (? [x ->]).
iExists _. do 2 (iSplit; [done|]).
iApply iProto_le_recv.
iIntros "!>" (? [y ->]).
iExists _. do 2 (iSplit; [done|]).
iApply iProto_le_refl. }
iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists x1.
iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists x2. auto. }
iIntros "!>" (k1 k2 _).
iExists _, _. iSplit; first done. eauto.
Qed.
......
......@@ -46,13 +46,13 @@ Section lty_ofe.
| lty_kind => λ n S T, lsty_car S {n} lsty_car T
end.
Lemma lty_mixin k : OfeMixin (lty Σ k).
Lemma lty_ofe_mixin k : OfeMixin (lty Σ k).
Proof.
destruct k.
- by apply (iso_ofe_mixin (ltty_car : _ val -d> _)).
- by apply (iso_ofe_mixin (lsty_car : _ iProto _)).
Qed.
Canonical Structure ltyO k := OfeT (lty Σ k) (lty_mixin k).
Canonical Structure ltyO k := OfeT (lty Σ k) (lty_ofe_mixin k).
Global Instance lty_cofe k : Cofe (ltyO k).
Proof.
......
......@@ -5,10 +5,10 @@ From actris.channel Require Export channel.
Definition lty_end {Σ} : lsty Σ := Lsty END.
Definition lty_message {Σ} (a : action) (A : ltty Σ) (S : lsty Σ) : lsty Σ :=
Lsty (<a> v, MSG v {{ ltty_car A v }}; lsty_car S).
Lsty (<a@v> MSG v {{ ltty_car A v }}; lsty_car S).
Definition lty_choice {Σ} (a : action) (Ss : gmap Z (lsty Σ)) : lsty Σ :=
Lsty (<a> x : Z, MSG #x {{ is_Some (Ss !! x) }}; lsty_car (Ss !!! x)).
Lsty (<a@(x : Z)> MSG #x {{ is_Some (Ss !! x) }}; lsty_car (Ss !!! x)).
Definition lty_dual {Σ} (S : lsty Σ) : lsty Σ :=
Lsty (iProto_dual (lsty_car S)).
......@@ -35,29 +35,22 @@ Section session_types.
Context {Σ : gFunctors}.
Global Instance lty_message_ne a : NonExpansive2 (@lty_message Σ a).
Proof. intros n A A' ? S S' ?. by apply iProto_message_ne; simpl. Qed.
Proof. solve_proper. Qed.
Global Instance lty_message_proper a :
Proper (() ==> () ==> ()) (@lty_message Σ a).
Proof. apply ne_proper_2, _. Qed.
Global Instance lty_message_contractive n a :
Proper (dist_later n ==> dist_later n ==> dist n) (@lty_message Σ a).
Proof.
intros A A' ? S S' ?.
apply iProto_message_contractive; simpl; done || by destruct n.
Qed.
Proof. solve_contractive. Qed.
Global Instance lty_choice_ne a : NonExpansive (@lty_choice Σ a).
Proof.
intros n Ss1 Ss2 Pseq. apply iProto_message_ne; simpl; solve_proper.
Qed.
Proof. solve_proper. Qed.
Global Instance lty_choice_proper a : Proper (() ==> ()) (@lty_choice Σ a).
Proof. apply ne_proper. apply _. Qed.
Proof. apply ne_proper, _. Qed.
(* FIXME
Global Instance lty_choice_contractive a : Contractive (@lty_choice Σ a).
Proof.
intros ? Ss1 Ss2 ?.
apply iProto_message_contractive; destruct n; simpl; done || solve_proper.
Qed.
Proof. solve_contractive. Qed.
*)
Global Instance lty_dual_ne : NonExpansive (@lty_dual Σ).
Proof. solve_proper. Qed.
Global Instance lty_dual_proper : Proper (() ==> ()) (@lty_dual Σ).
......
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment