Commit 3fa2232a authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Introduced new notation for stypes

parent ab6a6c3b
......@@ -40,8 +40,8 @@ Section DualBranch.
End DualBranch.
Global Typeclasses Opaque TSB.
Notation TSelect := (TSB Send).
Notation TBranch := (TSB Receive).
Infix "<+>" := (TSB Send) (at level 85) : stype_scope.
Infix "<&>" := (TSB Receive) (at level 85) : stype_scope.
Section branching_specs.
Context `{!heapG Σ} (N : namespace).
......@@ -58,7 +58,7 @@ Section branching_specs.
else "b2".
Lemma select_st_spec st1 st2 γ c s (b : bool) :
{{{ c @ s : TSelect st1 st2 {N,γ} }}}
{{{ c @ s : st1 <+> st2 {N,γ} }}}
select c #s #b
{{{ RET #(); c @ s : (if b then st1 else st2) {N,γ} }}}.
Proof.
......@@ -72,7 +72,7 @@ Section branching_specs.
Qed.
Lemma branch_st_spec st1 st2 γ c s (b1 b2 : val) Φ :
c @ s : TBranch st1 st2 {N,γ} -
c @ s : st1 <&> st2 {N,γ} -
( c @ s : st1 {N,γ} - (Φ b1)) -
( c @ s : st2 {N,γ} - (Φ b2)) -
WP branch c #s b1 b2 {{ v, Φ v }}.
......
......@@ -75,7 +75,7 @@ Section stype_interp.
match vs with
| [] => st1 dual_stype st2
| v::vs => match st2 with
| TReceive P st2 => P v st_eval vs st1 (st2 v)
| TSR Receive P st2 => P v st_eval vs st1 (st2 v)
| _ => False
end
end%I.
......@@ -109,7 +109,7 @@ Section stype_interp.
Qed.
Lemma st_eval_send (P : val -> iProp Σ) st l str v :
P v - st_eval l (TSend P st) str - st_eval (l ++ [v]) (st v) str.
P v - st_eval l (TSR Send P st) str - st_eval (l ++ [v]) (st v) str.
Proof.
iIntros "HP".
iRevert (str).
......@@ -128,7 +128,7 @@ Section stype_interp.
Qed.
Lemma st_eval_recv (P : val iProp Σ) st1 l st2 v :
st_eval (v :: l) st1 (TReceive P st2) - st_eval l st1 (st2 v) P v.
st_eval (v :: l) st1 (TSR Receive 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 Σ :=
......@@ -166,9 +166,9 @@ Section stype_interp.
Qed.
End stype_interp.
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τ ⟧{ N , γ }").
Notation "⟦ c @ s : st ⟧{ N , γ }" := (interp_st N γ st c s)
(at level 10, s at next level, st at next level, γ at next level,
format "⟦ c @ s : st ⟧{ N , γ }").
Section stype_specs.
Context `{!heapG Σ} (N : namespace).
......@@ -221,7 +221,7 @@ Section stype_specs.
Lemma send_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TSend P st {N,γ} ={E,E∖↑N}=
c @ s : TSR Send 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])
......@@ -273,11 +273,12 @@ Section stype_specs.
iApply (st_eval_send with "HP").
by iRewrite -"Heq".
}
iModIntro. iFrame. rewrite /is_st. auto.
Qed.
Lemma send_st_spec st γ c s (P : val iProp Σ) v :
{{{ P v c @ s : TSend P st {N,γ} }}}
{{{ P v c @ s : <!> @ P , st {N,γ} }}}
send c #s v
{{{ RET #(); c @ s : st v {N,γ} }}}.
Proof.
......@@ -292,11 +293,11 @@ Section stype_specs.
Lemma try_recv_vs c γ s (P : val iProp Σ) st E :
N E
c @ s : TReceive P st {N,γ}
c @ s : TSR Receive 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 {N,γ})
c @ s : TSR Receive P st {N,γ})
( v vs', vs = v :: vs' -
chan_own (st_c_name γ) (dual_side s) vs' - |={E∖↑N,E}=>
c @ s : (st v) {N,γ} P v))).
......@@ -364,9 +365,9 @@ Section stype_specs.
Qed.
Lemma try_recv_st_spec st γ c s (P : val iProp Σ) :
{{{ c @ s : TReceive P st {N,γ} }}}
{{{ c @ s : <?> @ P , st {N,γ} }}}
try_recv c #s
{{{ v, RET v; (v = NONEV c @ s : TReceive P st {N,γ})
{{{ v, RET v; (v = NONEV c @ s : <?> @ P, st {N,γ})
( w, v = SOMEV w c @ s : st w {N,γ} P w)}}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
......@@ -393,7 +394,7 @@ Section stype_specs.
Qed.
Lemma recv_st_spec st γ c s (P : val iProp Σ) :
{{{ c @ s : TReceive P st {N,γ} }}}
{{{ c @ s : <?> @ P , st {N,γ} }}}
recv c #s
{{{ v, RET v; c @ s : st v {N,γ} P v}}}.
Proof.
......
......@@ -91,8 +91,20 @@ Section DualStypeEnc.
End DualStypeEnc.
Notation TSend := (TSR' Send).
Notation TReceive := (TSR' Receive).
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.
Section stype_enc_specs.
Context `{!heapG Σ} (N : namespace).
......@@ -100,7 +112,7 @@ Section stype_enc_specs.
Lemma send_st_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) w :
{{{ P w c @ s : (TSend P st) {N,γ} }}}
{{{ P w c @ s : <!> @ P, st {N,γ} }}}
send c #s (encode w)
{{{ RET #(); c @ s : st w {N,γ} }}}.
Proof.
......@@ -116,7 +128,7 @@ Section stype_enc_specs.
Lemma recv_st_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) :
{{{ c @ s : (TReceive P st) {N,γ} }}}
{{{ c @ s : <?> @ P, st {N,γ} }}}
recv c #s
{{{ v, RET (encode v); c @ s : st v {N,γ} P v }}}.
Proof.
......
......@@ -20,9 +20,8 @@ Section BranchingExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /branch_example.
wp_apply (new_chan_st_spec N (TSelect
(TReceive (λ v, v = 5%I) (λ v, TEnd))
TEnd))=> //;
wp_apply (new_chan_st_spec N
((<?> v @ v = 5, TEnd) <+> (TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]".
wp_apply (select_st_spec with "Hstl");
iIntros "Hstl".
......
......@@ -10,16 +10,12 @@ Section ExampleProofs.
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)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = #5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec N with "[$Hstl //]");
iIntros "Hstl".
......@@ -33,7 +29,7 @@ Section ExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /par_example.
wp_apply (new_chan_st_spec N (TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = #5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext. wp_apply (send_st_spec N with "[$Hstl //]"). eauto.
......@@ -49,13 +45,10 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /par_2_example.
wp_apply (new_chan_st_spec N
(TSend
(λ v, v = #5%I)
(λ v, TReceive
(λ v',
( w, v = LitV $ LitInt $ w
w', v' = LitV $ LitInt $ w' w' >= w+2)%I)
(λ v', TEnd))))=> //;
(<!> v @ v = #5,
<?> v' @ ( w, v = LitV $ LitInt $ w
w', v' = LitV $ LitInt $ w' w' >= w+2),
TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
......@@ -80,8 +73,8 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /heaplet_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, ( l, v = LitV $ LitLoc $ l (l #5))%I)
(λ v, TEnd)))=> //;
(<!> v @ ( l, v = LitV $ LitLoc $ l (l #5)),
TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
......@@ -102,12 +95,8 @@ Section ExampleProofs.
iIntros (Φ H) "HΦ".
rewrite /channel_example.
wp_apply (new_chan_st_spec N
(TSend
(λ v, γ,
v @ Right : (TReceive
(λ v : val, v = #5)
(λ _ : val, TEnd)) {γ})%I
(λ v, TEnd)))=> //;
(<!> v @ ( γ, v @ Right : <?> v @ v = #5, TEnd {N,γ}),
TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
......@@ -132,8 +121,7 @@ Section ExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_seq_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = #5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
......@@ -148,8 +136,7 @@ Section ExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_par_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = #5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext. by wp_finish.
......@@ -162,10 +149,9 @@ Section ExampleProofs.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_interleave_example.
wp_apply (new_chan_st_spec N (TSend (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = #5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (new_chan_st_spec N
(TReceive (λ v, v = #5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<?> v @ v = #5, TEnd))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (wp_fork with "[Hstr Hstr']").
- iNext. wp_apply (recv_st_spec _ with "Hstr");
......
......@@ -15,8 +15,7 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /seq_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
......@@ -35,11 +34,9 @@ Section ExampleProofsEnc.
iIntros (Φ H) "HΦ".
rewrite /par_2_example.
wp_apply (new_chan_st_spec N
(TSend
(λ v:Z, 5 v%I)
(λ v:Z, TReceive
(λ v':Z, v+2 v'%I)
(λ v':Z, TEnd))))=> //;
(<!> v @ 5 v,
<?> v' @ v+2 v',
TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
......@@ -62,9 +59,7 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /heaplet_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, (v #5)%I)
(λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ (v #5), TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
......@@ -85,16 +80,12 @@ Section ExampleProofsEnc.
iIntros (Φ H) "HΦ".
rewrite /channel_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, γ, v @ Right :
(TReceive
(λ v, v = 5)
(λ _, TEnd)) {N, γ})%I
(λ v, TEnd)))=> //;
(<!> v @ ( γ, v @ Right : <?> v @ v = 5, TEnd {N,γ}),
TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (send_st_spec N val with "[Hstl Hstr']");
first by eauto 10 with iFrame.
......@@ -116,8 +107,7 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_seq_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (recv_st_spec N Z with "Hstr");
iIntros (v) "[Hstr HP]".
......@@ -133,8 +123,7 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_par_example.
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext. by wp_finish.
......@@ -149,10 +138,9 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_interleave_example.
wp_apply (new_chan_st_spec N (TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<!> v @ v = 5, TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (new_chan_st_spec N
(TReceive (λ v, v = 5%I) (λ v, TEnd)))=> //;
wp_apply (new_chan_st_spec N (<?> v @ v = 5, TEnd))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (wp_fork with "[Hstr Hstr']").
- iNext. wp_apply (recv_st_spec _ with "Hstr");
......
......@@ -30,8 +30,23 @@ 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).
Delimit Scope stype_scope with stype.
Bind Scope stype_scope with stype.
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.
Section stype_ofe.
Context {V : Type}.
......
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