Commit 730b296a authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Aliased encoding specification lemmas with original stype ones

parent 1955329c
......@@ -141,7 +141,7 @@ Section Encodings.
(at level 10, s at next level, sτ at next level, γ at next level,
format "⟦ c @ s : sτ ⟧{ γ }").
Lemma new_chan_st_enc_spec st :
Lemma new_chan_st_spec st :
{{{ True }}}
new_chan #()
{{{ c γ, RET c; c @ Left : st {γ}
......@@ -166,7 +166,7 @@ Section Encodings.
apply lift_dual_comm.
Qed.
Lemma send_st_enc_spec (A : Type) `{Encodable A} `{Decodable A} `{EncDec A}
Lemma send_st_spec (A : Type) `{Encodable A} `{Decodable A} `{EncDec A}
st γ c s (P : A iProp Σ) w :
{{{ P w c @ s : (TSend P st) {γ} }}}
send c #s (encode w)
......@@ -182,7 +182,7 @@ Section Encodings.
by iApply "HΦ".
Qed.
Lemma recv_st_enc_spec (A : Type) `{EncDec A}
Lemma recv_st_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) :
{{{ c @ s : (TReceive P st) {γ} }}}
recv c #s
......
......@@ -19,12 +19,12 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /seq_example.
wp_apply (new_chan_st_enc_spec N
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_enc_spec N Z with "[$Hstl //]");
wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
wp_apply (recv_st_enc_spec N Z with "Hstr");
wp_apply (recv_st_spec N Z with "Hstr");
iIntros (v) "[Hstr HP]".
iApply "HΦ".
iDestruct "HP" as %->.
......@@ -38,7 +38,7 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /par_2_example.
wp_apply (new_chan_st_enc_spec N
wp_apply (new_chan_st_spec N
(TSend
(λ v:Z, 5 v%I)
(λ v:Z, TReceive
......@@ -47,14 +47,14 @@ Section ExampleProofsEnc.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
wp_apply (recv_st_enc_spec N Z with "Hstr");
wp_apply (recv_st_spec N Z with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_enc_spec N Z with "[$Hstr //]");
wp_apply (send_st_spec N Z with "[$Hstr //]");
iIntros "Hstr".
eauto.
- wp_apply (send_st_enc_spec N Z with "[$Hstl //]");
- wp_apply (send_st_spec N Z with "[$Hstl //]");
iIntros "Hstl".
wp_apply (recv_st_enc_spec N Z with "Hstl");
wp_apply (recv_st_spec N Z with "Hstl");
iIntros (v) "[Hstl HP]".
iApply "HΦ".
iDestruct "HP" as %HP.
......@@ -66,17 +66,17 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /heaplet_example.
wp_apply (new_chan_st_enc_spec N
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_alloc l as "HP".
wp_apply (send_st_enc_spec N loc with "[$Hstl HP]")=> //;
wp_apply (send_st_spec N loc with "[$Hstl HP]")=> //;
iIntros "Hstl".
eauto.
- wp_apply (recv_st_enc_spec N loc with "Hstr");
- wp_apply (recv_st_spec N loc with "Hstr");
iIntros (v) "[Hstr HP]".
wp_load.
iApply "HΦ".
......@@ -88,7 +88,7 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /channel_example.
wp_apply (new_chan_st_enc_spec N
wp_apply (new_chan_st_spec N
(TSend (λ v, γ, v @ Right :
(TReceive
(λ v, v = 5)
......@@ -97,19 +97,19 @@ Section ExampleProofsEnc.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
wp_apply (new_chan_st_enc_spec N
wp_apply (new_chan_st_spec N
(TSR Send (λ v, v = 5%I) (λ v, TEnd)))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (send_st_enc_spec N val with "[Hstl Hstr']");
wp_apply (send_st_spec N val with "[Hstl Hstr']");
first by eauto 10 with iFrame.
iIntros "Hstl".
wp_apply (send_st_enc_spec N Z with "[$Hstl' //]");
wp_apply (send_st_spec N Z with "[$Hstl' //]");
iIntros "Hstl'".
eauto.
- wp_apply (recv_st_enc_spec N val with "Hstr");
- wp_apply (recv_st_spec N val with "Hstr");
iIntros (v) "[Hstr Hstr']".
iDestruct "Hstr'" as (γ') "Hstr'".
wp_apply (recv_st_enc_spec N Z with "Hstr'");
wp_apply (recv_st_spec N Z with "Hstr'");
iIntros (v') "[Hstr' HP]".
iDestruct "HP" as %<-.
by iApply "HΦ".
......@@ -120,12 +120,12 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_seq_example.
wp_apply (new_chan_st_enc_spec N
wp_apply (new_chan_st_spec N
(TSend (λ v, v = 5%I) (λ v, TEnd)))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (recv_st_enc_spec _ with "Hstr");
wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_enc_spec N with "[$Hstl //]");
wp_apply (send_st_spec N with "[$Hstl //]");
iIntros "Hstl".
iDestruct "HP" as %->.
wp_pures.
......@@ -137,12 +137,12 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_par_example.
wp_apply (new_chan_st_enc_spec N
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. by wp_finish.
- wp_apply (recv_st_enc_spec _ with "Hstr");
- wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
iDestruct "HP" as %->.
by iApply "HΦ".
......@@ -153,18 +153,18 @@ Section ExampleProofsEnc.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_interleave_example.
wp_apply (new_chan_st_enc_spec N (TSend (λ 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_enc_spec N
wp_apply (new_chan_st_spec N
(TReceive (λ v, v = 5%I) (λ v, TEnd)))=> //;
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (wp_fork with "[Hstr Hstr']").
- iNext. wp_apply (recv_st_enc_spec _ with "Hstr");
- iNext. wp_apply (recv_st_spec _ with "Hstr");
iIntros (v) "[Hstr HP]".
wp_apply (send_st_enc_spec _ with "[$Hstr' //]"). eauto.
- wp_apply (recv_st_enc_spec _ with "[$Hstl' //]");
wp_apply (send_st_spec _ with "[$Hstr' //]"). eauto.
- wp_apply (recv_st_spec _ with "[$Hstl' //]");
iIntros (v) "[Hstl' HP]".
wp_apply (send_st_enc_spec _ with "[$Hstl //]");
wp_apply (send_st_spec _ with "[$Hstl //]");
iIntros "Hstl".
by iApply "HΦ".
Qed.
......
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