Commit 88c199a5 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Made notation alias for send and receive

parent 7a866933
......@@ -75,7 +75,7 @@ Section logrel.
match vs with
| [] => st1 dual_stype st2
| v::vs => match st2 with
| TSR Receive P st2 => P v st_eval vs st1 (st2 v)
| TReceive P st2 => P v st_eval vs st1 (st2 v)
| _ => False
end
end%I.
......@@ -109,7 +109,7 @@ Section logrel.
Qed.
Lemma st_eval_send (P : val -> iProp Σ) st l str v :
P v - st_eval l (TSR Send P st) str - st_eval (l ++ [v]) (st v) str.
P v - st_eval l (TSend P st) str - st_eval (l ++ [v]) (st v) str.
Proof.
iIntros "HP".
iRevert (str).
......@@ -128,7 +128,7 @@ Section logrel.
Qed.
Lemma st_eval_recv (P : val iProp Σ) st1 l st2 v :
st_eval (v :: l) st1 (TSR Receive P st2) - st_eval l st1 (st2 v) P v.
st_eval (v :: l) st1 (TReceive P st2) - st_eval l st1 (st2 v) P v.
Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
Definition inv_st (γ : st_name) (c : val) : iProp Σ :=
......@@ -196,7 +196,7 @@ Section logrel.
Lemma send_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TSR Send P st {γ} ={E,E∖↑N}=
c @ s : TSend P st {γ} ={E,E∖↑N}=
vs, chan_own (st_c_name γ) s vs
( v, P v -
chan_own (st_c_name γ) s (vs ++ [v])
......@@ -252,7 +252,7 @@ Section logrel.
Qed.
Lemma send_st_spec st γ c s (P : val iProp Σ) v :
{{{ P v c @ s : TSR Send P st {γ} }}}
{{{ P v c @ s : TSend P st {γ} }}}
send c #s v
{{{ RET #(); c @ s : st v {γ} }}}.
Proof.
......@@ -267,11 +267,11 @@ Section logrel.
Lemma try_recv_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TSR Receive P st {γ}
c @ s : TReceive P st {γ}
={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 : TSR Receive P st {γ})
c @ s : TReceive P st {γ})
( v vs', vs = v :: vs' -
chan_own (st_c_name γ) (dual_side s) vs' - |={E∖↑N,E}=>
c @ s : (st v) {γ} P v))).
......@@ -339,9 +339,9 @@ Section logrel.
Qed.
Lemma try_recv_st_spec st γ c s (P : val iProp Σ) :
{{{ c @ s : TSR Receive P st {γ} }}}
{{{ c @ s : TReceive P st {γ} }}}
try_recv c #s
{{{ v, RET v; (v = NONEV c @ s : TSR Receive P st {γ})
{{{ v, RET v; (v = NONEV c @ s : TReceive P st {γ})
( w, v = SOMEV w c @ s : st w {γ} P w)}}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
......@@ -368,7 +368,7 @@ Section logrel.
Qed.
Lemma recv_st_spec st γ c s (P : val iProp Σ) :
{{{ c @ s : TSR Receive P st {γ} }}}
{{{ c @ s : TReceive P st {γ} }}}
recv c #s
{{{ v, RET v; c @ s : st v {γ} P v}}}.
Proof.
......
......@@ -78,6 +78,9 @@ Arguments TEnd {_}.
Arguments TSR {_ _ _ _} _ _ _.
Instance: Params (@TSR) 4.
Notation TSend P st := (TSR Send P st).
Notation TReceive P st := (TSR Receive P st).
Fixpoint dual_stype {A} (st : stype A) :=
match st with
| TEnd => TEnd
......@@ -91,15 +94,15 @@ Section Encodings.
Context `{!logrelG val Σ}.
Example ex_st : stype (iProp Σ) :=
(TSR Receive
(TReceive
(λ v', v' = 5%I)
(λ v', TEnd)).
Example ex_st2 : stype (iProp Σ) :=
TSR Send
TSend
(λ b, b = true%I)
(λ b,
(TSR Receive
(TReceive
(λ v', (v' > 5) = b%I)
(λ _, TEnd))).
......@@ -120,6 +123,9 @@ Section Encodings.
Global Instance: Params (@lift_stype) 1.
Global Arguments lift_stype : simpl never.
Instance stype_equiv : Equiv (stype (iProp Σ)) :=
λ st1 st2, lift_stype st1 lift_stype st2.
Lemma lift_dual_comm st :
lift_stype (dual_stype st) stype.dual_stype (lift_stype st).
Proof.
......@@ -162,7 +168,7 @@ Section Encodings.
Lemma send_st_enc_spec (A : Type) `{Encodable A} `{Decodable A} `{EncDec A}
st γ c s (P : A iProp Σ) w :
{{{ P w c @ s : (TSR Send P st) {γ} }}}
{{{ P w c @ s : (TSend P st) {γ} }}}
send c #s (encode w)
{{{ RET #(); c @ s : st w {γ} }}}.
Proof.
......@@ -178,7 +184,7 @@ Section Encodings.
Lemma recv_st_enc_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) :
{{{ c @ s : (TSR Receive P st) {γ} }}}
{{{ c @ s : (TReceive P st) {γ} }}}
recv c #s
{{{ v, RET (encode v); c @ s : st v {γ} P v }}}.
Proof.
......
......@@ -19,7 +19,7 @@ Section ExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /seq_example.
wp_apply (new_chan_st_spec N (TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec N with "[$Hstl //]");
iIntros "Hstl".
......@@ -33,7 +33,7 @@ Section ExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /par_example.
wp_apply (new_chan_st_spec N (TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext. wp_apply (send_st_spec N with "[$Hstl //]"). eauto.
......@@ -49,13 +49,13 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /par_2_example.
wp_apply (new_chan_st_spec N
(TSR Send
(λ v, v = #5%I)
(λ v, TSR Receive
(λ v',
( w, v = LitV $ LitInt $ w
w', v' = LitV $ LitInt $ w' w' >= w+2)%I)
(λ v', TEnd))))=> //;
(TSend
(λ v, v = #5%I)
(λ v, TReceive
(λ v',
( w, v = LitV $ LitInt $ w
w', v' = LitV $ LitInt $ w' w' >= w+2)%I)
(λ v', TEnd))))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
......@@ -80,8 +80,8 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /heaplet_example.
wp_apply (new_chan_st_spec N
(TSR Send (λ v, ( l, v = LitV $ LitLoc $ l (l #5))%I)
(λ v, TEnd)))=> //;
(TSend (λ v, ( l, v = LitV $ LitLoc $ l (l #5))%I)
(λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
......@@ -102,11 +102,12 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /channel_example.
wp_apply (new_chan_st_spec N
(TSR Send (λ v, γ, v @ Right :
(TSR Receive
(λ v : val, v = #5)
(λ _ : val, TEnd)) {γ})%I
(λ v, TEnd)))=> //;
(TSend
(λ v, γ,
v @ Right : (TReceive
(λ v : val, v = #5)
(λ _ : val, TEnd)) {γ})%I
(λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
......@@ -132,7 +133,7 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /bad_seq_example.
wp_apply (new_chan_st_spec N
(TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //;
(TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
......@@ -148,7 +149,7 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /bad_par_example.
wp_apply (new_chan_st_spec N
(TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //;
(TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext. by wp_finish.
......@@ -161,10 +162,10 @@ Section ExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_interleave_example.
wp_apply (new_chan_st_spec N (TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (new_chan_st_spec N
(TSR Receive (λ v, v = #5%I) (λ v, TEnd)))=> //;
(TReceive (λ v, v = #5%I) (λ v, TEnd)))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (wp_fork with "[Hstr Hstr']").
- iNext. wp_apply (recv_st_spec _ with "Hstr");
......
......@@ -20,7 +20,7 @@ Section ExampleProofsEnc.
iIntros (Φ H) "HΦ".
rewrite /seq_example.
wp_apply (new_chan_st_enc_spec N
(TSR Send (λ v, v = 5%I) (λ v, TEnd)))=> //;
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_enc_spec N Z with "[$Hstl //]");
iIntros "Hstl".
......@@ -39,11 +39,11 @@ Section ExampleProofsEnc.
iIntros (Φ H) "HΦ".
rewrite /par_2_example.
wp_apply (new_chan_st_enc_spec N
(TSR Send
(λ v:Z, 5 v%I)
(λ v:Z, TSR Receive
(λ v':Z, v+2 v'%I)
(λ v':Z, TEnd))))=> //;
(TSend
(λ v:Z, 5 v%I)
(λ v:Z, TReceive
(λ v':Z, v+2 v'%I)
(λ v':Z, TEnd))))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
......@@ -67,8 +67,8 @@ Section ExampleProofsEnc.
iIntros (Φ H) "HΦ".
rewrite /heaplet_example.
wp_apply (new_chan_st_enc_spec N
(TSR Send (λ v, (v #5)%I)
(λ v, TEnd)))=> //;
(TSend (λ v, (v #5)%I)
(λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
......@@ -89,11 +89,11 @@ Section ExampleProofsEnc.
iIntros (Φ H) "HΦ".
rewrite /channel_example.
wp_apply (new_chan_st_enc_spec N
(TSR Send (λ v, γ, v @ Right :
(TSR Receive
(λ v, v = 5)
(λ _, TEnd)) {γ})%I
(λ v, TEnd)))=> //;
(TSend (λ v, γ, v @ Right :
(TReceive
(λ v, v = 5)
(λ _, TEnd)) {γ})%I
(λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
......
......@@ -30,6 +30,9 @@ Fixpoint dual_stype {V A} (st : stype V A) :=
end.
Instance: Params (@dual_stype) 2.
Notation TSend P st := (TSR Send P st).
Notation TReceive P st := (TSR Receive P st).
Section stype_ofe.
Context {V : Type}.
Context {A : ofeT}.
......@@ -41,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 :
......
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