Refactoring: Definitions stype -> proto, st -> prot

parent 528c3ed5
......@@ -137,7 +137,7 @@ Section ListSortExample.
lmerge_ref "cmp" "xs" !"ys" !"zs";;
send "c" #Right "xs".
Definition sort_protocol xs :=
Definition sort_protocol xs : proto val (iProp Σ) :=
(<?> cmp @ cmp_spec cmp,
<?> l @ l encode xs,
<!> l' @ l = l'
......@@ -145,7 +145,7 @@ Section ListSortExample.
l' encode ys
Sorted (R) ys
Permutation ys xs),
TEnd)%stype.
TEnd).
Lemma list_sort_service_spec γ c xs :
{{{ c @ Right : sort_protocol xs {N,γ} }}}
......
......@@ -9,21 +9,21 @@ Section DualBranch.
Context `{PROP : bi}.
Definition TSB (a : action)
(st1 st2 : stype val PROP) : stype val PROP :=
TSR' a (λ _, True)%I (λ v, if v : bool then st1 else st2).
(prot1 prot2 : proto val PROP) : proto val PROP :=
TSR' a (λ _, True)%I (λ v, if v : bool then prot1 else prot2).
Global Instance is_dual_tsb a1 a2 st1 st1' st2 st2' :
Global Instance is_dual_tsb a1 a2 proto1 proto1' proto2 proto2' :
IsDualAction a1 a2
IsDualStype st1 st1' IsDualStype st2 st2'
IsDualStype (TSB a1 st1 st2) (TSB a2 st1' st2').
IsDualProto proto1 proto1' IsDualProto proto2 proto2'
IsDualProto (TSB a1 proto1 proto2) (TSB a2 proto1' proto2').
Proof.
rewrite /IsDualAction.
rewrite /IsDualStype.
rewrite /IsDualProto.
intros Ha Hst1 Hst2.
destruct a1.
- simpl.
simpl in Ha. rewrite -Ha.
rewrite -(stype_force_eq (dual_stype _)).
rewrite -(proto_force_eq (dual_proto _)).
constructor.
f_equiv.
f_equiv.
......@@ -31,7 +31,7 @@ Section DualBranch.
by destruct b. apply is_dual_end.
- simpl.
simpl in Ha. rewrite -Ha.
rewrite -(stype_force_eq (dual_stype _)).
rewrite -(proto_force_eq (dual_proto _)).
constructor.
f_equiv.
f_equiv.
......@@ -42,8 +42,8 @@ Section DualBranch.
End DualBranch.
Global Typeclasses Opaque TSB.
Infix "<+>" := (TSB Send) (at level 85) : stype_scope.
Infix "<&>" := (TSB Receive) (at level 85) : stype_scope.
Infix "<+>" := (TSB Send) (at level 85) : proto_scope.
Infix "<&>" := (TSB Receive) (at level 85) : proto_scope.
Section branching_specs.
Context `{!heapG Σ} (N : namespace).
......@@ -53,15 +53,15 @@ Section branching_specs.
λ: "c" "s" "b",
send "c" "s" "b".
Lemma select_st_spec st1 st2 γ c s (b : side) :
{{{ c @ s : st1 <+> st2 {N,γ} }}}
Lemma select_st_spec proto1 proto2 γ c s (b : side) :
{{{ c @ s : proto1 <+> proto2 {N,γ} }}}
select c #s #b
{{{ RET #(); c @ s : (if b then st1 else st2) {N,γ} }}}.
{{{ RET #(); c @ s : (if b then proto1 else proto2) {N,γ} }}}.
Proof.
iIntros (Φ) "Hst HΦ".
iIntros (Φ) "Hproto HΦ".
wp_pures. wp_lam.
wp_pures. rewrite /TSB.
wp_apply (send_st_spec N bool with "[$Hst //]");
wp_apply (send_st_spec N bool with "[$Hproto //]");
iIntros "Hstl".
iApply "HΦ".
by destruct b.
......@@ -73,17 +73,17 @@ Section branching_specs.
then "b1"
else "b2".
Lemma branch_st_spec st1 st2 γ c s (b1 b2 : val) :
{{{ c @ s : st1 <&> st2 {N,γ} }}}
Lemma branch_st_spec proto1 proto2 γ c s (b1 b2 : val) :
{{{ c @ s : proto1 <&> proto2 {N,γ} }}}
branch c #s b1 b2
{{{ v, RET v; (v = b1%V c @ s : st1 {N,γ})
(v = b2%V c @ s : st2 {N,γ})}}}.
{{{ v, RET v; (v = b1%V c @ s : proto1 {N,γ})
(v = b2%V c @ s : proto2 {N,γ})}}}.
Proof.
iIntros (Φ').
iIntros "Hst HΦ'".
iIntros "Hproto HΦ'".
wp_pures.
wp_lam. rewrite /TSB. simpl.
wp_apply (recv_st_spec N bool with "[$Hst //]").
wp_apply (recv_st_spec N bool with "[$Hproto //]").
iIntros (v) "[Hstl _]".
destruct v.
- wp_pures. iApply ("HΦ'"). eauto with iFrame.
......
This diff is collapsed.
......@@ -5,53 +5,53 @@ From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
From osiris.proto Require Export encodable proto_specs.
Section DualStypeEnc.
Section DualProtoEnc.
Context `{EncDec V} `{PROP: bi} .
Definition TSR'
(a : action) (P : V PROP) (st : V stype val PROP) : stype val PROP :=
(a : action) (P : V PROP) (prot : V proto val PROP) : proto val PROP :=
TSR a
(λ v, if decode v is Some x then P x else False)%I
(λ v, if decode v is Some x then st x else TEnd (* dummy *)).
(λ v, if decode v is Some x then prot x else TEnd (* dummy *)).
Global Instance: Params (@TSR') 3.
Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V stype val PROP) :
Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V proto val PROP) :
IsDualAction a1 a2
( x, IsDualStype (st1 x) (st2 x))
IsDualStype (TSR' a1 P st1) (TSR' a2 P st2).
( x, IsDualProto (st1 x) (st2 x))
IsDualProto (TSR' a1 P st1) (TSR' a2 P st2).
Proof.
rewrite /IsDualAction /IsDualStype. intros <- Hst.
rewrite -(stype_force_eq (dual_stype _)).
rewrite /IsDualAction /IsDualProto. intros <- Hst.
rewrite -(proto_force_eq (dual_proto _)).
constructor=> x. done. destruct (decode x)=> //.
apply is_dual_end.
Qed.
End DualStypeEnc.
End DualProtoEnc.
Notation "<!> x @ P , st" :=
(TSR' Send (λ x, P%I) (λ x, st%stype))
(at level 200, x pattern, st at level 200) : stype_scope.
Notation "<?> x @ P , st" :=
(TSR' Receive (λ x, P%I) (λ x, st%stype))
(at level 200, x pattern, st at level 200) : stype_scope.
Notation "<!> x , st" := (<!> x @ True, (st x))%stype
(at level 200, x pattern, st at level 200) : stype_scope.
Notation "<?> x , st" := (<?> x @ True, (st x))%stype
(at level 200, x pattern, st at level 200) : stype_scope.
Notation "<!> @ P , st" := (<!> dummy__ @ P dummy__, st dummy__)%stype
(at level 200, st at level 200) : stype_scope.
Notation "<?> @ P , st" := (<?> dummy__ @ P dummy__, st dummy__)%stype
(at level 200, st at level 200) : stype_scope.
Notation "<!> x @ P , prot" :=
(TSR' Send (λ x, P%I) (λ x, prot%proto))
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<?> x @ P , prot" :=
(TSR' Receive (λ x, P%I) (λ x, prot%proto))
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<!> x , prot" := (<!> x @ True, (prot x))%proto
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<?> x , prot" := (<?> x @ True, (prot x))%proto
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<!> @ P , prot" := (<!> dummy__ @ P dummy__, prot dummy__)%proto
(at level 200, prot at level 200) : proto_scope.
Notation "<?> @ P , prot" := (<?> dummy__ @ P dummy__, prot dummy__)%proto
(at level 200, prot at level 200) : proto_scope.
Section stype_enc_specs.
Section proto_enc_specs.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Lemma send_st_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) w :
{{{ P w c @ s : <!> @ P, st {N,γ} }}}
prot γ c s (P : A iProp Σ) w :
{{{ P w c @ s : <!> @ P, prot {N,γ} }}}
send c #s (encode w)
{{{ RET #(); c @ s : st w {N,γ} }}}.
{{{ RET #(); c @ s : prot w {N,γ} }}}.
Proof.
iIntros (Φ) "[HP Hsend] HΦ".
iApply (send_st_spec with "[HP Hsend]").
......@@ -64,10 +64,10 @@ Section stype_enc_specs.
Qed.
Lemma recv_st_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) :
{{{ c @ s : <?> @ P, st {N,γ} }}}
prot γ c s (P : A iProp Σ) :
{{{ c @ s : <?> @ P, prot {N,γ} }}}
recv c #s
{{{ v, RET (encode v); c @ s : st v {N,γ} P v }}}.
{{{ v, RET (encode v); c @ s : prot v {N,γ} P v }}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iApply (recv_st_spec with "Hrecv").
......@@ -86,4 +86,4 @@ Section stype_enc_specs.
- inversion Hw.
Qed.
End stype_enc_specs.
\ No newline at end of file
End proto_enc_specs.
\ No newline at end of file
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