Commit f4f29cb2 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Updated encoding specifications and separated examples and proofs

parent e05d2403
......@@ -5,4 +5,5 @@ theories/auth_excl.v
theories/typing.v
theories/channel.v
theories/logrel.v
theories/examples.v
theories/encodable.v
......@@ -94,7 +94,7 @@ Section Encodings.
(TSR' Receive
(λ v', v' = 5%I)
(λ v', TEnd')).
Example ex_st2 : stype' (iProp Σ) :=
TSR' Send
(λ b, b = true%I)
......@@ -106,22 +106,23 @@ Section Encodings.
Fixpoint stype'_to_stype (st : stype' (iProp Σ)) : stype val (iProp Σ) :=
match st with
| TEnd' => TEnd
| TSR' a P st => TSR a
(λ v, match decode v with
| Some v => P v
| None => False
end%I)
(λ v, match decode v with
| Some v => stype'_to_stype (st v)
| None => TEnd
end)
| TSR' a P st =>
TSR a
(λ v, match decode v with
| Some v => P v
| None => False
end%I)
(λ v, match decode v with
| Some v => stype'_to_stype (st v)
| None => TEnd
end)
end.
Global Instance: Params (@stype'_to_stype) 1.
Global Arguments stype'_to_stype : simpl never.
Lemma dual_stype'_comm st :
dual_stype (stype'_to_stype st) stype'_to_stype (dual_stype' st).
Proof.
stype'_to_stype (dual_stype' st) dual_stype (stype'_to_stype st).
Proof.
induction st.
- by simpl.
- unfold stype'_to_stype. simpl.
......@@ -130,9 +131,9 @@ Section Encodings.
+ intros v. destruct (decode v); eauto.
Qed.
Lemma dual_stype'_comm_eq st :
dual_stype (stype'_to_stype st) = stype'_to_stype (dual_stype' st).
Proof. Admitted.
Lemma stype_map_equiv {A B : ofeT} (f : A -n> B) (st st' : stype val A) :
st st' stype_map f st stype_map f st'.
Proof. induction 1=>//. constructor=>//. by repeat f_equiv. Qed.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
(at level 10, s at next level, sτ at next level, γ at next level,
......@@ -149,47 +150,57 @@ Section Encodings.
iNext.
iIntros (c γ) "[Hl Hr]".
iApply "HΦ".
iFrame.
rewrite dual_stype'_comm_eq.
iFrame.
iDestruct "Hr" as "[Hown Hctx]".
iFrame.
unfold st_own. simpl.
iApply (own_mono with "Hown").
apply (auth_frag_mono).
apply Some_included.
left.
f_equiv.
f_equiv.
apply stype_map_equiv.
apply dual_stype'_comm.
Qed.
Lemma send_st_enc_spec (A : Type) `{Encodable A} `{Decodable A} `{EncDec A}
st γ c s (P : A iProp Σ) v w :
decode v = Some w
st γ c s (P : A iProp Σ) w :
{{{ P w c @ s : (stype'_to_stype (TSR' Send P st)) {γ} }}}
send c #s v
send c #s (encode w)
{{{ RET #(); c @ s : stype'_to_stype (st w) {γ} }}}.
Proof.
intros Henc.
iIntros (Φ) "[HP Hsend] HΦ".
iApply (send_st_spec with "[HP Hsend]").
simpl.
iFrame.
by destruct (decode v); inversion Henc.
by rewrite encdec.
iNext.
destruct (decode v); inversion Henc.
rewrite encdec.
by iApply "HΦ".
Qed.
Lemma recv_st_enc_spec (A : Type) `{EncDec A}
st γ c s (P : A iProp Σ) :
{{{ c @ s : (stype'_to_stype (TSR' Receive P st)) {γ} }}}
recv c #s
{{{ v w, RET v; c @ s : stype'_to_stype (st w) {γ} P w
encode w = v }}}.
{{{ v, RET (encode v); c @ s : stype'_to_stype (st v) {γ} P v }}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iApply (recv_st_spec with "Hrecv").
iNext. iIntros (v). iSpecialize ("HΦ" $!v).
iNext. iIntros (v). (* iSpecialize ("HΦ" $!v). *)
iIntros "[H HP]".
iAssert (( w, decode v = Some w P w)%I) with "[HP]" as (w Hw) "HP".
destruct (decode v). iExists a. by iFrame. iDestruct "HP" as %HP=>//.
assert (encode w = v). by apply decenc.
destruct (decode v); inversion Hw.
{ destruct (decode v).
iExists a. by iFrame. iDestruct "HP" as %HP=>//. }
iSpecialize ("HΦ" $!w).
apply enc_dec in Hw. rewrite Hw.
iApply "HΦ".
iFrame.
iPureIntro. eauto.
apply enc_dec in Hw.
destruct (decode v).
- inversion Hw. subst. iApply "H".
- inversion Hw.
Qed.
End Encodings.
\ No newline at end of file
......@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris Require Import typing channel logrel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
Section Examples.
......@@ -18,103 +17,21 @@ Section Examples.
send "c" #Left #5;;
recv "c" #Right)%E.
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 (TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec N with "[$Hstl //]").
iIntros "Hstl".
wp_apply (recv_st_spec _ with "Hstr").
iIntros (v) "[Hstr HP]".
by iApply "HΦ".
Qed.
Definition par_example : expr :=
(let: "c" := new_chan #() in
Fork(send "c" #Left #5);;
recv "c" #Right)%E.
Lemma par_proof :
{{{ True }}} par_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
rewrite /par_example.
wp_apply (new_chan_st_spec N (TSR Send (λ 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]"). by iFrame. eauto.
- wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]". by iApply "HΦ".
Qed.
Definition par_2_example : expr :=
(let: "c" := new_chan #() in
Fork(let: "v" := recv "c" #Right in send "c" #Right ("v"+#2));;
send "c" #Left #5;;recv "c" #Left)%E.
Lemma par_2_proof :
{{{ True }}}
par_2_example
{{{ (v:Z), RET #v; 7 v }}}.
Proof.
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))))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]".
iDestruct "HP" as %->.
wp_apply (send_st_spec N with "[Hstr]"). iFrame; eauto 10 with iFrame.
eauto.
- wp_apply (send_st_spec _ with "[Hstl]"). by iFrame.
iIntros "Hstl".
wp_apply (recv_st_spec _ with "[Hstl]"). by iFrame.
iIntros (v) "[Hstl HP]".
iDestruct "HP" as %[w [HP [w' [-> HQ']]]].
iApply "HΦ".
iPureIntro. simplify_eq. lia.
Qed.
Definition heaplet_example : expr :=
(let: "c" := new_chan #() in
Fork(send "c" #Left (ref #5));;
!(recv "c" #Right))%E.
Lemma heaplet_proof :
{{{ True }}} heaplet_example {{{ v l, RET v; v = #5 l v }}}.
Proof.
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)))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
wp_apply (wp_alloc)=> //.
iIntros (l) "HP".
wp_apply (send_st_spec N with "[Hstl HP]"). eauto 10 with iFrame.
eauto.
- wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]".
iDestruct "HP" as (l ->) "HP".
wp_load.
iApply "HΦ".
iFrame. eauto.
Qed.
Definition channel_example : expr :=
(let: "c" := new_chan #() in
Fork(
......@@ -124,101 +41,20 @@ Section Examples.
recv "c'" #Right
)%E.
Lemma channel_proof :
{{{ True }}} channel_example {{{ v, RET v; v = #5 }}}.
Proof.
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)))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_pures.
wp_apply (wp_fork with "[Hstl]").
- iNext.
wp_apply (new_chan_st_spec N
(TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //.
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (send_st_spec N with "[Hstl Hstr']").
iFrame. iExists γ'. iFrame.
iIntros "Hstl".
wp_apply (send_st_spec N with "[Hstl']").
iFrame. eauto. eauto.
- wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr Hstr']".
iDestruct "Hstr'" as (γ') "Hstr'".
wp_apply (recv_st_spec _ with "[Hstr']").
iApply "Hstr'".
iIntros (v') "[Hstr' HP]".
by iApply "HΦ".
Qed.
Definition bad_seq_example : expr :=
(let: "c" := new_chan #() in
let: "v" := recv "c" #Right in
send "c" #Left #5;; "v")%E.
Lemma bad_seq_proof :
{{{ True }}} bad_seq_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_seq_example.
wp_apply (new_chan_st_spec N (TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (recv_st_spec _ with "Hstr").
iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec N with "[Hstl]"). by iFrame.
iIntros "Hstl".
wp_pures.
by iApply "HΦ".
Qed.
Definition bad_par_example : expr :=
(let: "c" := new_chan #() in
Fork(#());;
recv "c" #Right)%E.
Lemma bad_par_proof :
{{{ True }}} bad_par_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_par_example.
wp_apply (new_chan_st_spec N (TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext. wp_finish. eauto.
- wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]". by iApply "HΦ".
Qed.
Definition bad_interleave_example : expr :=
(let: "c" := new_chan #() in
let: "c'" := new_chan #() in
Fork(recv "c" #Right;; send "c'" #Right #5);;
recv "c'" #Left;; send "c" #Left #5)%E.
Lemma bad_interleave_proof :
{{{ True }}} bad_interleave_example {{{ v, RET v; v = #() }}}.
Proof.
iIntros (Φ H) "HΦ".
rewrite /bad_interleave_example.
wp_apply (new_chan_st_spec N (TSR Send (λ 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)))=> //.
iIntros (c' γ') "[Hstl' Hstr']"=> /=.
wp_apply (wp_fork with "[Hstr Hstr']").
- iNext. wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]".
wp_apply (send_st_spec _ with "[Hstr']"). iFrame. eauto.
eauto.
- wp_apply (recv_st_spec _ with "[Hstl']"). by iFrame.
iIntros (v) "[Hstl' HP]".
wp_apply (send_st_spec _ with "[Hstl]"). iFrame. eauto.
iIntros "Hstl".
by iApply "HΦ".
Qed.
End Examples.
\ No newline at end of file
......@@ -5,15 +5,15 @@ From osiris Require Import typing channel logrel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
From osiris Require Import encodable.
From osiris Require Import examples.
Section Encodings_Examples.
Context `{!heapG Σ} {N : namespace}.
Context `{!logrelG val Σ}.
Definition seq_example : expr :=
(let: "c" := new_chan #() in
send "c" #Left #5;;
recv "c" #Right)%E.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ (stype'_to_stype 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 }}}.
......@@ -26,18 +26,12 @@ Section Encodings_Examples.
wp_apply (send_st_enc_spec N Z with "[Hstl]")=> //. by iFrame.
iIntros "Hstl".
wp_apply (recv_st_enc_spec N Z with "[Hstr]"). iFrame.
iIntros (v w) "[Hstr [HP Heq]]".
iIntros (v) "[Hstr HP]".
iApply "HΦ".
iDestruct "Heq" as %<-.
iDestruct "HP" as %->.
eauto.
Qed.
Definition par_2_example : expr :=
(let: "c" := new_chan #() in
Fork(let: "v" := recv "c" #Right in send "c" #Right ("v"+#4));;
send "c" #Left #5;;recv "c" #Left)%E.
Lemma par_2_proof :
{{{ True }}}
par_2_example
......@@ -55,26 +49,19 @@ Section Encodings_Examples.
wp_apply (wp_fork with "[Hstr]").
- iNext.
wp_apply (recv_st_enc_spec N Z with "[Hstr]"). by iFrame.
iIntros (v w) "[Hstr HP]".
iDestruct "HP" as %[HP <-].
iIntros (v) "[Hstr HP]".
wp_apply (send_st_enc_spec N Z with "[Hstr]")=> //.
iFrame; eauto 10 with iFrame.
iPureIntro. lia.
eauto.
- wp_apply (send_st_enc_spec N Z with "[Hstl]")=> //. by iFrame.
iIntros "Hstl".
wp_apply (recv_st_enc_spec N Z with "[Hstl]"). by iFrame.
iIntros (v w) "[Hstl HP]".
iDestruct "HP" as %[HP <-].
iIntros (v) "[Hstl HP]".
iApply "HΦ".
iDestruct "HP" as %HP.
iPureIntro. lia.
Qed.
Definition heaplet_example : expr :=
(let: "c" := new_chan #() in
Fork(send "c" #Left (ref #5));;
!(recv "c" #Right))%E.
Lemma heaplet_proof :
{{{ True }}} heaplet_example {{{ v l, RET v; v = #5 l v }}}.
Proof.
......@@ -91,27 +78,12 @@ Section Encodings_Examples.
wp_apply (send_st_enc_spec N loc with "[Hstl HP]")=> //. by iFrame.
eauto.
- wp_apply (recv_st_enc_spec N loc with "[Hstr]"). iFrame.
iIntros (v w) "[Hstr HP]".
iDestruct "HP" as "[HP Henc]".
iDestruct "Henc" as %<-.
iIntros (v) "[Hstr HP]".
wp_load.
iApply "HΦ".
iFrame. eauto.
Qed.
Definition channel_example : expr :=
(let: "c" := new_chan #() in
Fork(
let: "c'" := new_chan #() in
send "c" #Left ("c'");; send "c'" #Left #5);;
let: "c'" := recv "c" #Right in
recv "c'" #Right
)%E.
Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ (stype'_to_stype sτ) c s)
(at level 10, s at next level, sτ at next level, γ at next level,
format "⟦ c @ s : sτ ⟧{ γ }").
Lemma channel_proof :
{{{ True }}} channel_example {{{ v, RET v; v = #5 }}}.
Proof.
......@@ -136,12 +108,10 @@ Section Encodings_Examples.
wp_apply (send_st_enc_spec N Z with "[Hstl']")=> //.
iFrame. eauto. eauto.
- wp_apply (recv_st_enc_spec N val with "[Hstr]")=> //.
iIntros (v w) "[Hstr [Hstr' Henc]]".
iDestruct "Henc" as %<-.
iIntros (v) "[Hstr Hstr']".
iDestruct "Hstr'" as (γ') "Hstr'".
wp_apply (recv_st_enc_spec N Z with "[Hstr']")=> //.
iIntros (v' w') "[Hstr' [HP Henc]]".
iDestruct "Henc" as %<-.
iIntros (v') "[Hstr' HP]".
iDestruct "HP" as %<-.
by iApply "HΦ".
Qed.
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris Require Import typing channel logrel.
From iris.base_logic Require Import invariants.
From osiris Require Import examples.
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 (TSR Send (λ v, v = #5%I) (λ v, TEnd)))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (send_st_spec N with "[$Hstl //]").
iIntros "Hstl".
wp_apply (recv_st_spec _ with "Hstr").
iIntros (v) "[Hstr HP]".
by iApply "HΦ".
Qed.
Lemma par_proof :
{{{ True }}} par_example {{{ v, RET v; v = #5 }}}.
Proof.
iIntros (Φ H) "HΦ".
rewrite /par_example.
wp_apply (new_chan_st_spec N (TSR Send (λ 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]"). by iFrame. eauto.
- wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]". by iApply "HΦ".
Qed.
Lemma par_2_proof :
{{{ True }}}
par_2_example
{{{ (v:Z), RET #v; 7 v }}}.
Proof.
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))))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstr]").
- iNext.
wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]".
iDestruct "HP" as %->.
wp_apply (send_st_spec N with "[Hstr]"). iFrame; eauto 10 with iFrame.
eauto.
- wp_apply (send_st_spec _ with "[Hstl]"). by iFrame.
iIntros "Hstl".
wp_apply (recv_st_spec _ with "[Hstl]"). by iFrame.
iIntros (v) "[Hstl HP]".
iDestruct "HP" as %[w [HP [w' [-> HQ']]]].
iApply "HΦ".
iPureIntro. simplify_eq. lia.
Qed.
Lemma heaplet_proof :
{{{ True }}} heaplet_example {{{ v l, RET v; v = #5 l v }}}.
Proof.
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)))=> //.
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
- iNext.
wp_apply (wp_alloc)=> //.
iIntros (l) "HP".
wp_apply (send_st_spec N with "[Hstl HP]"). eauto 10 with iFrame.
eauto.
- wp_apply (recv_st_spec _ with "[Hstr]"). by iFrame.
iIntros (v) "[Hstr HP]".
iDestruct "HP" as (l ->) "HP".
wp_load.
iApply "HΦ".
iFrame. eauto.
Qed.
Lemma channel_proof :
{{{ True }}} channel_example {{{ v, RET v; v = #5 }}}.