Squashed commit of the following:

commit a96494d6
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Tue May 7 18:39:41 2019 +0200

    Finalized List sort example, and introduced list encodings

commit 1b9fc4de
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Fri May 3 15:28:21 2019 +0200

    WIP List sort example

commit 4ce5eb98
Author: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date:   Fri May 3 11:18:07 2019 +0200

    WIP list sort example
parent 44759644
......@@ -15,3 +15,4 @@ theories/examples/proofs.v
theories/examples/proofs_enc.v
theories/examples/branching_examples.v
theories/examples/branching_proofs.v
theories/examples/list_sort.v
......@@ -70,7 +70,7 @@ Section channel.
Context `{!heapG Σ, !chanG Σ} (N : namespace).
Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
( l':loc, hd : val, l = #l' l' hd is_list hd xs)%I.
( l':loc, l = #l' l' encode xs)%I.
Record chan_name := Chan_name {
chan_lock_name : gname;
......@@ -119,8 +119,8 @@ Section channel.
Proof.
iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (ls Hls). wp_alloc l as "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (rs Hrs). wp_alloc r as "Hr".
wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
as (lsγ) "[Hls Hls']"; first done.
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
......@@ -164,8 +164,9 @@ Section channel.
wp_apply get_side_spec; wp_pures.
iDestruct (chan_inv_alt s with "Hinv") as
(vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
wp_load. wp_apply (lsnoc_spec with "Hlvs"). iIntros (lhd' Hlvs).
iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
wp_load.
wp_apply (lsnoc_spec (T:=val))=> //; iIntros (_).
wp_bind (_ <- _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
......@@ -174,7 +175,7 @@ Section channel.
iModIntro.
wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
iApply (chan_inv_alt s).
rewrite /is_list_ref. eauto 10 with iFrame.
rewrite /is_list_ref. eauto 20 with iFrame.
Qed.
Lemma try_recv_spec Φ E γ c s :
......@@ -193,22 +194,20 @@ Section channel.
wp_apply dual_side_spec. wp_apply get_side_spec; wp_pures.
iDestruct (chan_inv_alt (dual_side s) with "Hinv") as
(vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
iDestruct "Href" as (ll Hslr) "Hll"; rewrite Hslr.
wp_bind (! _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
wp_load.
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
destruct vs as [|v vs]; simpl.
- iDestruct "Hlvs" as %->.
iDestruct "HΦ" as "[HΦ _]".
- iDestruct "HΦ" as "[HΦ _]".
iMod ("HΦ" with "[//] Hchan") as "HΦ".
iModIntro.
wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
{ iApply (chan_inv_alt (dual_side s)).
rewrite /is_list_ref. eauto 10 with iFrame. }
iIntros (_). wp_pures. by iApply "HΦ".
- iDestruct "Hlvs" as %(hd' & -> & Hhd').
iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
- iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
iDestruct "HΦ" as "[_ HΦ]".
iMod ("HΦ" with "[//] Hchan") as "HΦ".
iModIntro. wp_store.
......
......@@ -64,3 +64,14 @@ Proof.
- intros.
apply decenc. eauto.
Qed.
Lemma enc_inj {A : Type} `{ED : EncDec A}
x y : encode x = encode y -> x = y.
Proof.
intros Heq.
assert (decode (encode x) = decode (encode y)).
{ by f_equiv. }
erewrite encdec in H=> //.
erewrite encdec in H=> //.
by inversion H.
Qed.
\ No newline at end of file
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.
From osiris Require Export encodable.
(** Immutable ML-style functional lists *)
Fixpoint is_list (hd : val) (xs : list val) : Prop :=
Instance pair_encodable `{Encodable A, Encodable B} : Encodable (A * B) :=
λ p, (encode p.1, encode p.2)%V.
Instance option_encodable `{Encodable A} : Encodable (option A) := λ mx,
match mx with Some x => SOMEV (encode x) | None => NONEV end%V.
Instance list_encodable `{Encodable A} : Encodable (list A) :=
fix go xs :=
let _ : Encodable _ := @go in
match xs with
| [] => hd = NONEV
| x :: xs => hd', hd = SOMEV (x,hd') is_list hd' xs
| [] => encode None
| x :: xs => encode (Some (x,xs))
end.
Definition lnil : val := λ: <>, NONEV.
......@@ -65,134 +74,110 @@ Definition lsnoc : val :=
Section lists.
Context `{heapG Σ}.
Implicit Types i : nat.
Implicit Types v : val.
Context `{EncDec T}.
Implicit Types x : T.
Implicit Types xs : list T.
Lemma lnil_spec :
{{{ True }}}
lnil #()
{{{ hd, RET hd; is_list hd [] }}}.
{{{ True }}} lnil #() {{{ RET encode []; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
Lemma lcons_spec hd vs v :
{{{ is_list hd vs }}}
lcons v hd
{{{ hd', RET hd'; is_list hd' (v :: vs) }}}.
Proof.
iIntros (Φ ?) "HΦ". wp_lam. wp_pures.
iApply "HΦ". simpl; eauto.
Qed.
Lemma lcons_spec x xs :
{{{ True }}} lcons (encode x) (encode xs) {{{ RET (encode (x :: xs)); True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma lhead_spec x xs:
{{{ True }}} lhead (encode (x::xs)) {{{ RET encode x; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma lhead_spec hd vs v :
{{{ is_list hd (v :: vs) }}}
lhead hd
{{{ RET v; True }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma ltail_spec hd vs v :
{{{ is_list hd (v :: vs) }}}
ltail hd
{{{ hd', RET hd'; is_list hd' vs }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma llookup_spec i hd vs v :
vs !! i = Some v
{{{ is_list hd vs }}}
llookup #i hd
{{{ RET v; True }}}.
Lemma ltail_spec x xs :
{{{ True }}} ltail (encode (x::xs)) {{{ RET encode xs; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma llookup_spec i xs x:
xs !! i = Some x
{{{ True }}}
llookup #i (encode xs)
{{{ RET encode x; True }}}.
Proof.
iIntros (Hi Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl);
iInduction xs as [|x' xs] "IH" forall (i Hi Hl);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
wp_lam. wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
Lemma linsert_spec i hd vs v :
is_Some (vs !! i)
{{{ is_list hd vs }}}
linsert #i v hd
{{{ hd', RET hd'; is_list hd' (<[i:=v]> vs) }}}.
Lemma linsert_spec i xs x :
is_Some (xs !! i)
{{{ True }}}
linsert #i (encode x) (encode xs)
{{{ RET encode (<[i:=x]>xs); True }}}.
Proof.
iIntros ([w Hi] Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ);
iInduction xs as [|x' xs] "IH" forall (i Hi Hl Φ);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
{ wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (?).
wp_let. by iApply (lcons_spec with "[//]"). }
wp_lam; wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
wp_apply ("IH" with "[//] [//]"). iIntros (?). wp_let.
wp_apply (lhead_spec with "[//]"); iIntros "_".
by wp_apply (lcons_spec with "[//]").
Qed.
Lemma llist_member_spec hd vs v :
{{{ is_list hd vs }}}
llist_member v hd
{{{ RET #(bool_decide (v vs)); True }}}.
Lemma llist_member_spec `{EqDecision T} (xs : list T) (x : T) :
{{{ True }}}
llist_member (encode x) (encode xs)
{{{ RET #(bool_decide (x xs)); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=.
{ wp_lam; wp_pures. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam; wp_pures.
destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
{ rewrite (bool_decide_true (_ _ :: _)); last by left. by iApply "HΦ". }
wp_lam; wp_pures.
destruct (bool_decide_reflect (encode x' = encode x)) as [Heq|?]; wp_if.
{ apply enc_inj in Heq. rewrite Heq. rewrite (bool_decide_true (_ _ :: _)). by iApply "HΦ". by left. }
wp_proj. wp_let. iApply ("IH" with "[//]").
destruct (bool_decide_reflect (v vs)).
destruct (bool_decide_reflect (x xs)).
- by rewrite bool_decide_true; last by right.
- by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
Qed.
Lemma lreplicate_spec i v :
Lemma lreplicate_spec i x :
{{{ True }}}
lreplicate #i v
{{{ hd, RET hd; is_list hd (replicate i v) }}}.
lreplicate #i (encode x)
{{{ RET encode (replicate i x); True }}}.
Proof.
iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
{ wp_lam; wp_pures.
iApply (lnil_spec with "[//]"). iApply "HΦ". }
wp_lam; wp_pures.
rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
wp_apply "IH"; iIntros (Hl). wp_let. by iApply (lcons_spec with "[//]").
Qed.
Lemma llength_spec hd vs :
{{{ is_list hd vs }}} llength hd {{{ RET #(length vs); True }}}.
Lemma llength_spec xs :
{{{ True }}} llength (encode xs) {{{ RET #(length xs); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl Φ); simplify_eq/=.
iInduction xs as [|x' xs] "IH" forall (Hl Φ); simplify_eq/=.
{ wp_lam. wp_match. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj.
wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
wp_lam. wp_match. wp_proj.
wp_apply ("IH" with "[//]"); iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
Lemma lsnoc_spec hd vs v :
{{{ is_list hd vs }}}
lsnoc hd v
{{{ hd', RET hd'; is_list hd' (vs++[v]) }}}.
Lemma lsnoc_spec xs x :
{{{ True }}} lsnoc (encode xs) (encode x) {{{ RET (encode (xs++[x])); True }}}.
Proof.
iIntros (Φ Hvs) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hvs Φ).
- simplify_eq/=.
wp_rec.
wp_pures.
wp_lam.
wp_pures.
iApply "HΦ". simpl. eauto.
- destruct Hvs as [vs' [-> Hvs']].
wp_rec.
wp_pures.
wp_bind (lsnoc vs' v).
iApply "IH".
eauto.
iNext.
iIntros (hd' Hhd').
wp_pures.
iApply lcons_spec.
eauto.
iApply "HΦ".
iInduction xs as [|x' xs] "IH" forall (Hvs Φ).
{ wp_rec. wp_pures. wp_lam. wp_pures. by iApply "HΦ". }
wp_rec.
wp_apply "IH"=> //.
iIntros (_). by wp_apply lcons_spec=> //.
Qed.
End lists.
\ No newline at end of file
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris.typing Require Import side stype.
From osiris.encodings Require Import list channel stype_enc.
From iris.base_logic Require Import invariants.
From stdpp Require Import sorting.
Require Import Coq.Lists.List.
Require Import Omega.
Section ListSortExample.
Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
Definition lsplit : val :=
λ: "xs",
let: "hd" := lhead "xs" in
let: "ys" := lcons "hd" NONEV in
let: "zs" := ltail "xs" in
("ys", "zs").
Lemma lsplit_spec (x : Z) (xs : list Z) :
{{{ True }}}
lsplit (encode (x::xs))
{{{ RET (encode [x],encode xs); True }}}.
Proof.
iIntros (Φ _) "HΦ".
wp_lam. wp_apply (lhead_spec (T := Z))=> //.
iIntros (_).
wp_apply (lcons_spec (T := Z) _ [])=> //.
iIntros (_).
wp_apply (ltail_spec (T := Z))=> //.
iIntros (_).
wp_pures.
by iApply "HΦ".
Qed.
Definition lsplit_ref : val :=
λ: "xs", let: "ys_zs" := lsplit !"xs" in
(ref (Fst "ys_zs"), ref (Snd ("ys_zs"))).
Lemma lsplit_ref_spec lxs (x : Z) (xs : list Z) :
{{{ lxs encode (x::xs) }}}
lsplit_ref #lxs
{{{ lys lzs ys zs, RET (#lys,#lzs);
(x::xs) = ys++zs
lxs encode (x::xs)
lys encode ys
lzs encode zs }}}.
Proof.
iIntros (Φ) "Hhd HΦ".
wp_lam. wp_load. wp_apply (lsplit_spec)=> //; iIntros (_).
wp_alloc lzs as "Hlzs".
wp_alloc lys as "Hlys".
wp_pures.
iApply "HΦ".
eauto 10 with iFrame.
Qed.
Definition compare_vals : val :=
λ: "x" "y", "x" "y".
Lemma compare_vals_spec (x y : Z) :
{{{ True }}}
compare_vals (encode x) (encode y)
{{{ RET (encode (bool_decide (x y))); True }}}.
Proof. iIntros (Φ) "_ HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Definition lmerge : val :=
rec: "go" "hys" "hzs" :=
if: llength "hys" = #0
then "hzs"
else if: llength "hzs" = #0
then "hys"
else let: "y" := lhead "hys" in
let: "z" := lhead "hzs" in
if: (compare_vals "y" "z")
then lcons "y" ("go" (ltail "hys") "hzs")
else lcons "z" ("go" "hys" (ltail "hzs")).
Lemma list_merge_emp1 (ys : list Z) : list_merge () [] ys = ys.
Proof. induction ys; eauto. Qed.
Lemma list_merge_emp2 (xs : list Z) : list_merge () xs [] = xs.
Proof. induction xs; eauto. Qed.
Lemma lmerge_spec (ys zs : list Z) :
{{{ True }}}
lmerge (encode ys) (encode zs)
{{{ RET (encode (list_merge () ys zs)); True }}}.
Proof.
revert ys zs.
iLöb as "IH".
iIntros (ys zs Φ _) "HΦ".
wp_lam.
wp_apply (llength_spec (T:=Z))=> //; iIntros "_".
destruct ys as [|y ys].
{ wp_pures. rewrite list_merge_emp1. by iApply ("HΦ"). }
wp_apply (llength_spec (T:=Z))=> //; iIntros "_".
destruct zs as [|z zs].
{ wp_pures. by iApply ("HΦ"). }
wp_apply (lhead_spec (T:=Z))=> //; iIntros "_".
wp_apply (lhead_spec (T:=Z))=> //; iIntros "_".
wp_apply (compare_vals_spec)=> //; iIntros "_".
rewrite list_merge_cons.
destruct (decide (y z)).
- rewrite bool_decide_true=> //.
wp_apply (ltail_spec (T:=Z))=> //; iIntros (_).
wp_apply ("IH")=> //; iIntros (_).
wp_apply (lcons_spec (T:=Z))=> //.
- rewrite bool_decide_false=> //.
wp_apply (ltail_spec (T:=Z))=> //; iIntros (_).
wp_apply ("IH")=> //; iIntros (_).
wp_apply (lcons_spec (T:=Z))=> //.
Qed.
Definition lmerge_ref : val :=
λ: "lxs" "hys" "hzs",
"lxs" <- lmerge "hys" "hzs".
Lemma lmerge_ref_spec ldx tmp ys zs :
{{{ ldx tmp }}}
lmerge_ref #ldx (encode ys) (encode zs)
{{{ RET #(); ldx encode (list_merge () ys zs) }}}.
Proof.
iIntros (Φ) "Hldx HΦ".
wp_lam.
wp_apply (lmerge_spec ys zs)=> //.
iIntros (_).
wp_store.
by iApply ("HΦ").
Qed.
Definition list_sort_service : val :=
rec: "go" "c" :=
let: "xs" := recv "c" #Right in
if: llength (!"xs") #1
then send "c" #Right "xs"
else let: "ys_zs" := lsplit_ref "xs" in
let: "ys" := Fst "ys_zs" in
let: "zs" := Snd "ys_zs" in
let: "cy" := new_chan #() in Fork("go" "cy");;
let: "cz" := new_chan #() in Fork("go" "cz");;
send "cy" #Left "ys";;
send "cz" #Left "zs";;
let: "ys" := recv "cy" #Left in
let: "zs" := recv "cz" #Left in
lmerge_ref "xs" !"ys" !"zs";;
send "c" #Right "xs".
Lemma list_sort_service_spec γ c xs :
{{{ c @ Right : (<?> l @ l encode xs,
<!> l' @
l = l' ( ys : list Z,
l' encode ys
Sorted () ys
Permutation ys xs),
TEnd) {N,γ} }}}
list_sort_service c
{{{ RET #(); c @ Right : TEnd {N,γ} }}}.
Proof.
revert γ c xs.
iLöb as "IH".
iIntros (γ c xs Φ) "Hstr HΦ".
wp_lam.
wp_apply (recv_st_spec N loc with "Hstr").
iIntros (v) "Hstr".
iDestruct "Hstr" as "[Hstr HP]".
wp_load.
destruct xs.
{
wp_apply (llength_spec (T:=Z))=> //; iIntros (_).
wp_apply (send_st_spec N loc with "[HP Hstr]")=> //. iFrame.
eauto 10 with iFrame.
}
destruct xs.
{
wp_apply (llength_spec (T:=Z))=> //; iIntros (_).
wp_apply (send_st_spec N loc with "[HP Hstr]")=> //. iFrame.
eauto 10 with iFrame.
}
wp_apply (llength_spec (T:=Z))=> //; iIntros (_).
wp_pures.
assert (bool_decide (S (S (length xs)) 1) = false) as HSS.
{ apply bool_decide_false. lia. }
rewrite HSS.
wp_apply (lsplit_ref_spec with "HP");
iIntros (hdy hdz ys zs) "(Heq & Hhdx & Hhdy & Hhdz)".
iDestruct "Heq" as %->.
wp_apply (new_chan_st_spec N
(<!> l @ l encode ys,
<?> l' @ l = l'
( ys' : list Z,
l' encode ys'
Sorted () ys'
Permutation ys' ys),
TEnd))=>//;
iIntros (cy γy) "[Hstly Hstry]".
wp_apply (wp_fork with "[Hstry]").
{ iNext. iApply ("IH" with "Hstry"). iNext. by iIntros "Hstry". }
wp_apply (new_chan_st_spec N
(<!> l @ l encode zs,
<?> l' @ l = l'
( zs' : list Z,
l' encode zs'
Sorted () zs'
Permutation zs' zs),
TEnd))=>//;
iIntros (cz γz) "[Hstlz Hstrz]".
wp_apply (wp_fork with "[Hstrz]").
{ iNext. iApply ("IH" with "Hstrz"). iNext. by iIntros "Hstrz". }
wp_apply (send_st_spec N loc with "[Hhdy Hstly]"). iFrame.
iIntros "Hstly".
wp_apply (send_st_spec N loc with "[Hhdz Hstlz]"). iFrame.
iIntros "Hstlz".
wp_apply (recv_st_spec N loc with "Hstly").
iIntros (ly') "[Hstly Hys']".
iDestruct "Hys'" as (<- ys') "(Hys' & Hys'_sorted_of)".
iDestruct "Hys'_sorted_of" as %[Hys'_sorted Hys'_perm].
wp_apply (recv_st_spec N loc with "Hstlz").
iIntros (lz') "[Hstlz Hzs']".
iDestruct "Hzs'" as (<- zs') "(Hzs' & Hzs'_sorted_of)".
iDestruct "Hzs'_sorted_of" as %[Hzs'_sorted Hzs'_perm].
wp_load.
wp_load.
wp_apply (lmerge_ref_spec with "Hhdx")=> //.
iIntros "Hhdx".
wp_apply (send_st_spec N loc with "[Hstr Hhdx]").
{
iFrame.
iSplit=> //.
iExists (list_merge () ys' zs').
iSplit=> //.
iPureIntro.
split.
- apply Sorted_list_merge=> //.
{ intros x y. lia. } (* Why is this needed? *)
- rewrite merge_Permutation.
by apply Permutation_app.
}
iIntros "Hstr".
by iApply "HΦ".
Qed.
Definition list_sort : val :=
λ: "xs",
let: "c" := new_chan #() in
Fork(list_sort_service "c");;
send "c" #Left "xs";;
recv "c" #Left.
Lemma list_sort_spec l xs :
{{{ l encode xs }}}
list_sort #l
{{{ ys, RET #l; l encode ys Sorted () ys Permutation ys xs }}}.
Proof.
iIntros (Φ) "Hc HΦ".
wp_lam.
wp_apply (new_chan_st_spec N
(<!> l @ l encode xs,
<?> l' @ l = l'
( ys : list Z,
l' encode ys
Sorted () ys
Permutation ys xs), TEnd))=>//.
iIntros (c γ) "[Hstl Hstr]".
wp_apply (wp_fork with "[Hstr]").
{
iApply (list_sort_service_spec γ c xs with "[Hstr]"). iFrame.
iNext. iNext. iIntros "Hstr". done.
}
wp_apply (send_st_spec N loc with "[Hc $Hstl]"). iFrame.
iIntros "Hstl".
wp_apply (recv_st_spec N loc with "Hstl").
iIntros (v) "[Hstl HP]".
iDestruct "HP" as (<- ys) "[Hys Hys_sorted_of]".
iApply "HΦ". iFrame.
Qed.
End ListSortExample.
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