Commit 61f47cc8 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Made stype interp notation global and clean-up

parent 488bb70f
......@@ -10,4 +10,4 @@ theories/encodings/stype.v
theories/encodings/stype_enc.v
theories/examples/examples.v
theories/examples/proofs.v
theories/examples/proofs_enc.v
\ No newline at end of file
theories/examples/proofs_enc.v
......@@ -79,7 +79,7 @@ Section stype_interp.
| _ => False
end
end%I.
Arguments st_eval : simpl nomatch.
Global Arguments st_eval : simpl nomatch.
Lemma st_later_eq a P2 (st : stype val (iProp Σ)) st2 :
( (st TSR a P2 st2) -
......@@ -148,7 +148,8 @@ Section stype_interp.
(c : val) (s : side) : iProp Σ :=
(st_own γ s st is_st γ st c)%I.
Global Instance interp_st_proper γ : Proper (() ==> (=) ==> (=) ==> ()) (interp_st γ).
Global Instance interp_st_proper γ :
Proper (() ==> (=) ==> (=) ==> ()) (interp_st γ).
Proof.
intros st1 st2 Heq v1 v2 <- s1 s2 <-.
iSplit;
......@@ -163,10 +164,15 @@ Section stype_interp.
f_equiv;
apply stype_map_equiv=> //.
Qed.
End stype_interp.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st γ sτ c s)
Notation "⟦ c @ s : sτ ⟧{ N , γ }" := (interp_st N γ sτ c s)
(at level 10, s at next level, sτ at next level, γ at next level,
format "⟦ c @ s : sτ ⟧{ γ }").
format "⟦ c @ s : sτ ⟧{ N , γ }").
Section stype_specs.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Lemma new_chan_vs st E c cγ :
is_chan N cγ c
......@@ -175,7 +181,7 @@ Section stype_interp.
={E}=
lγ rγ,
let γ := SessionType_name cγ lγ rγ in
c @ Left : st {γ} c @ Right : dual_stype st {γ}.
c @ Left : st {N,γ} c @ Right : dual_stype st {N,γ}.
Proof.
iIntros "[#Hcctx [Hcol Hcor]]".
iMod (own_alloc ( (to_stype_auth_excl st)
......@@ -196,8 +202,8 @@ Section stype_interp.
IsDualStype st1 st2
{{{ True }}}
new_chan #()
{{{ c γ, RET c; c @ Left : st1 {γ}
c @ Right : st2 {γ} }}}.
{{{ c γ, RET c; c @ Left : st1 {N,γ}
c @ Right : st2 {N,γ} }}}.
Proof.
rewrite /IsDualStype.
iIntros (Hst Φ _) "HΦ".
......@@ -210,16 +216,16 @@ Section stype_interp.
iDestruct "H" as (lγ rγ) "[Hl Hr]".
iApply "HΦ".
rewrite Hst.
by iFrame.
by iFrame.
Qed.
Lemma send_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TSend P st {γ} ={E,E∖↑N}=
c @ s : TSend P st {N,γ} ={E,E∖↑N}=
vs, chan_own (st_c_name γ) s vs
( v, P v -
chan_own (st_c_name γ) s (vs ++ [v])
={E N,E}= c @ s : st v {γ}).
={E N,E}= c @ s : st v {N,γ}).
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
iMod (inv_open with "Hinv") as "Hinv'"=> //.
......@@ -271,9 +277,9 @@ Section stype_interp.
Qed.
Lemma send_st_spec st γ c s (P : val iProp Σ) v :
{{{ P v c @ s : TSend P st {γ} }}}
{{{ P v c @ s : TSend P st {N,γ} }}}
send c #s v
{{{ RET #(); c @ s : st v {γ} }}}.
{{{ RET #(); c @ s : st v {N,γ} }}}.
Proof.
iIntros (Φ) "[HP Hsend] HΦ".
iApply (send_spec with "[#]").
......@@ -286,14 +292,14 @@ Section stype_interp.
Lemma try_recv_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TReceive P st {γ}
c @ s : TReceive P st {N,γ}
={E,E∖↑N}=
vs, chan_own (st_c_name γ) (dual_side s) vs
( ((vs = [] - chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=
c @ s : TReceive P st {γ})
c @ s : TReceive P st {N,γ})
( v vs', vs = v :: vs' -
chan_own (st_c_name γ) (dual_side s) vs' - |={E∖↑N,E}=>
c @ s : (st v) {γ} P v))).
c @ s : (st v) {N,γ} P v))).
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
iMod (inv_open with "Hinv") as "Hinv'"=> //.
......@@ -358,10 +364,10 @@ Section stype_interp.
Qed.
Lemma try_recv_st_spec st γ c s (P : val iProp Σ) :
{{{ c @ s : TReceive P st {γ} }}}
{{{ c @ s : TReceive P st {N,γ} }}}
try_recv c #s
{{{ v, RET v; (v = NONEV c @ s : TReceive P st {γ})
( w, v = SOMEV w c @ s : st w {γ} P w)}}}.
{{{ v, RET v; (v = NONEV c @ s : TReceive P st {N,γ})
( w, v = SOMEV w c @ s : st w {N,γ} P w)}}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iApply (try_recv_spec with "[#]").
......@@ -387,9 +393,9 @@ Section stype_interp.
Qed.
Lemma recv_st_spec st γ c s (P : val iProp Σ) :
{{{ c @ s : TReceive P st {γ} }}}
{{{ c @ s : TReceive P st {N,γ} }}}
recv c #s
{{{ v, RET v; c @ s : st v {γ} P v}}}.
{{{ v, RET v; c @ s : st v {N,γ} P v}}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iLöb as "IH". wp_rec.
......@@ -407,4 +413,4 @@ Section stype_interp.
iFrame.
Qed.
End stype_interp.
\ No newline at end of file
End stype_specs.
\ No newline at end of file
......@@ -70,18 +70,15 @@ Proof.
apply decenc. eauto.
Qed.
Definition TSR' `{PROP: bi} {V} `{ED : EncDec V}
Section DualStypeEnc.
Context `{EncDec V} `{PROP: bi} .
Definition TSR'
(a : action) (P : V PROP) (st : V stype val PROP) : stype 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 *)).
Instance: Params (@TSR') 4.
Notation TSend P st := (TSR' Send P st).
Notation TReceive P st := (TSR' Receive P st).
Section DualStypeEnc.
Context `{PROP: bi} `{EncDec V}.
Global Instance: Params (@TSR') 3.
Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V stype val PROP) :
IsDualAction a1 a2
......@@ -92,44 +89,20 @@ Section DualStypeEnc.
constructor=> x. done. by destruct (decode x).
Qed.
Global Instance is_dual_send P (st1 st2 : V stype val PROP) :
( x, IsDualStype (st1 x) (st2 x))
IsDualStype (TSend P st1) (TReceive P st2).
Proof. intros Heq. by apply is_dual_tsr'. Qed.
Global Instance is_dual_receive P (st1 st2 : V stype val PROP) :
( x, IsDualStype (st1 x) (st2 x))
IsDualStype (TReceive P st1) (TSend P st2).
Proof. intros Heq. by apply is_dual_tsr'. Qed.
End DualStypeEnc.
Section Encodings.
Notation TSend := (TSR' Send).
Notation TReceive := (TSR' Receive).
Section stype_enc_specs.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Example ex_st : stype val (iProp Σ) :=
(TReceive
(λ v', v' = 5%I)
(λ v', TEnd)).
Example ex_st2 : stype val (iProp Σ) :=
TSend
(λ b, b = true%I)
(λ b,
(TReceive
(λ v', (v' > 5) = b%I)
(λ _, TEnd))).
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
(at level 10, s at next level, sτ at next level, γ at next level,
format "⟦ c @ s : sτ ⟧{ γ }").
Lemma send_st_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) w :
{{{ P w c @ s : (TSend P st) {γ} }}}
{{{ P w c @ s : (TSend P st) {N,γ} }}}
send c #s (encode w)
{{{ RET #(); c @ s : st w {γ} }}}.
{{{ RET #(); c @ s : st w {N,γ} }}}.
Proof.
iIntros (Φ) "[HP Hsend] HΦ".
iApply (send_st_spec with "[HP Hsend]").
......@@ -143,9 +116,9 @@ Section Encodings.
Lemma recv_st_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) :
{{{ c @ s : (TReceive P st) {γ} }}}
{{{ c @ s : (TReceive P st) {N,γ} }}}
recv c #s
{{{ v, RET (encode v); c @ s : st v {γ} P v }}}.
{{{ v, RET (encode v); c @ s : st v {N,γ} P v }}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iApply (recv_st_spec with "Hrecv").
......@@ -164,4 +137,4 @@ Section Encodings.
- inversion Hw.
Qed.
End Encodings.
\ No newline at end of file
End stype_enc_specs.
\ No newline at end of file
......@@ -52,5 +52,5 @@ Section Examples.
let: "c'" := new_chan #() in
Fork(recv "c" #Right;; send "c'" #Right #5);;
recv "c'" #Left;; send "c" #Left #5)%E.
End Examples.
\ No newline at end of file
......@@ -10,24 +10,20 @@ Section ExampleProofsEnc.
Context `{!heapG Σ} (N : namespace).
Context `{!logrelG val Σ}.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
(at level 10, s at next level, sτ at next level, γ at next level,
format "⟦ c @ s : sτ ⟧{ γ }").
Lemma seq_proof :
{{{ True }}} seq_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
rewrite /seq_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //.
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
wp_apply (recv_st_spec N Z with "[Hstr]"). iApply "Hstr".
iIntros (v) "[Hstr HP]".
iApply "HΦ".
iDestruct "HP" as %->.
iDestruct "HP" as %->.
eauto.
Qed.
......@@ -92,7 +88,7 @@ Section ExampleProofsEnc.
(TSend (λ v, γ, v @ Right :
(TReceive
(λ v, v = 5)
(λ _, TEnd)) {γ})%I
(λ _, TEnd)) {N, γ})%I
(λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
......@@ -123,9 +119,9 @@ Section ExampleProofsEnc.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (recv_st_spec _ with "Hstr");
wp_apply (recv_st_spec N Z with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec N with "[$Hstl //]");
wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
iDestruct "HP" as %->.
wp_pures.
......@@ -161,10 +157,10 @@ Section ExampleProofsEnc.
wp_apply (wp_fork with "[Hstr Hstr']").
- iNext. wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec _ with "[$Hstr' //]"). eauto.
- wp_apply (recv_st_spec _ with "[$Hstl' //]");
wp_apply (send_st_spec _ Z with "[$Hstr' //]"). eauto.
- wp_apply (recv_st_spec _ Z with "[$Hstl' //]");
iIntros (v) "[Hstl' HP]".
wp_apply (send_st_spec _ with "[$Hstl //]");
wp_apply (send_st_spec _ Z with "[$Hstl //]");
iIntros "Hstl".
by iApply "HΦ".
Qed.
......
......@@ -14,15 +14,6 @@ Definition dual_action (a : action) : action :=
Instance dual_action_involutive : Involutive (=) dual_action.
Proof. by intros []. Qed.
Class IsDualAction (a1 a2 : action) :=
is_dual_action : dual_action a1 = a2.
Instance is_dual_action_default : IsDualAction a (dual_action a) | 100.
Proof. done. Qed.
Instance is_dual_action_Send : IsDualAction Send Receive.
Proof. done. Qed.
Instance is_dual_action_Receive : IsDualAction Receive Send.
Proof. done. Qed.
Inductive stype (V A : Type) :=
| TEnd
| TSR (a : action) (P : V A) (st : V stype V A).
......@@ -53,7 +44,7 @@ Section stype_ofe.
pointwise_relation V () st1 st2
TSR a P1 st1 TSR a P2 st2.
Existing Instance stype_equiv.
Inductive stype_dist' (n : nat) : relation (stype V A) :=
| TEnd_dist : stype_dist' n TEnd TEnd
| TSR_dist a P1 P2 st1 st2 :
......@@ -227,20 +218,29 @@ Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_contractive.
Qed.
Class IsDualStype {V} {A : ofeT} (st1 st2 : stype V A) :=
is_dual_stype : dual_stype st1 st2.
Class IsDualAction (a1 a2 : action) :=
is_dual_action : dual_action a1 = a2.
Instance is_dual_action_default : IsDualAction a (dual_action a) | 100.
Proof. done. Qed.
Instance is_dual_action_Send : IsDualAction Send Receive.
Proof. done. Qed.
Instance is_dual_action_Receive : IsDualAction Receive Send.
Proof. done. Qed.
Section DualStype.
Context `{PROP: bi} {V : Type}.
Context {V : Type} {A : ofeT}.
Class IsDualStype (st1 st2 : stype V A) :=
is_dual_stype : dual_stype st1 st2.
Global Instance is_dual_default (st : stype V PROP) :
Global Instance is_dual_default (st : stype V A) :
IsDualStype st (dual_stype st) | 100.
Proof. by rewrite /IsDualStype. Qed.
Global Instance is_dual_end : IsDualStype (TEnd : stype V PROP) TEnd.
Global Instance is_dual_end : IsDualStype (TEnd : stype V A) TEnd.
Proof. constructor. Qed.
Global Instance is_dual_tsr a1 a2 P (st1 st2 : V stype V PROP) :
Global Instance is_dual_tsr a1 a2 P (st1 st2 : V stype V A) :
IsDualAction a1 a2
( x, IsDualStype (st1 x) (st2 x))
IsDualStype (TSR a1 P st1) (TSR a2 P st2).
......@@ -248,15 +248,5 @@ Section DualStype.
rewrite /IsDualAction /IsDualStype. intros <- Hst.
by constructor=> x.
Qed.
Global Instance is_dual_send P (st1 st2 : V stype V PROP) :
( x, IsDualStype (st1 x) (st2 x))
IsDualStype (TSR Send P st1) (TSR Receive P st2).
Proof. intros H. by apply is_dual_tsr. Qed.
Global Instance is_dual_receive P (st1 st2 : V stype V PROP) :
( x, IsDualStype (st1 x) (st2 x))
IsDualStype (TSR Receive P st1) (TSR Send P st2).
Proof. intros H. by apply is_dual_tsr. Qed.
End DualStype.
\ No newline at end of file
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