Commit 3b201219 authored by Robbert Krebbers's avatar Robbert Krebbers

Update sorting examples to be consistent with paper.

parent c4f9d470
......@@ -10,10 +10,9 @@ theories/channel/proto_model.v
theories/channel/proto_channel.v
theories/channel/proofmode.v
theories/examples/sort.v
theories/examples/sort_client.v
theories/examples/sort_elem.v
theories/examples/loop_sort.v
theories/examples/sort_elem_client.v
theories/examples/sort_fg.v
theories/examples/sort_fg_client.v
theories/examples/map.v
theories/examples/map_reduce.v
theories/examples/basics.v
From stdpp Require Import sorting.
From actris.channel Require Import proto_channel.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From actris.examples Require Import sort.
Definition loop_sort_service : val :=
rec: "go" "c" :=
if: recv "c" then sort_service "c";; "go" "c"
Definition sort_service_br : val :=
rec: "go" "cmp" "c" :=
if: ~recv "c" then #() else
sort_service "cmp" "c";;
"go" "cmp" "c".
Definition sort_service_del : val :=
rec: "go" "cmp" "c" :=
if: ~recv "c" then #() else
send "c" (start_chan (λ: "c", sort_service "cmp" "c"));;
"go" "cmp" "c".
Definition sort_service_br_del : val :=
rec: "go" "cmp" "c" :=
if: recv "c" then
sort_service "cmp" "c";;
"go" "cmp" "c"
else if: recv "c" then
let: "d" := start_chan "go" in
send "c" "d";;
"go" "c"
send "c" (start_chan (λ: "c", "go" "cmp" "c"));;
"go" "cmp" "c"
else #().
Section loop_sort.
Section sort_service_br_del.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
Context {A} (I : A val iProp Σ) (R : A A Prop) `{!RelDecision R, !Total R}.
Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
((sort_protocol I R <++> rec) <+> END)%proto.
Instance sort_protocol_br_aux_contractive : Contractive sort_protocol_br_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_br : iProto Σ := fixpoint sort_protocol_br_aux.
Global Instance sort_protocol_br_unfold :
ProtoUnfold sort_protocol_br (sort_protocol_br_aux sort_protocol_br).
Proof. apply proto_unfold_eq, (fixpoint_unfold sort_protocol_br_aux). Qed.
Lemma sort_service_br_spec cmp c :
cmp_spec I R cmp -
{{{ c iProto_dual sort_protocol_br @ N }}}
sort_service_br cmp c
{{{ RET #(); c END @ N }}}.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
Definition sort_protocol_del_aux (rec : iProto Σ) : iProto Σ :=
((<?> c, MSG c {{ c sort_protocol I R @ N }}; rec) <+> END)%proto.
Instance sort_protocol_del_aux_contractive : Contractive sort_protocol_del_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_del : iProto Σ := fixpoint sort_protocol_del_aux.
Global Instance sort_protocol_del_unfold :
ProtoUnfold sort_protocol_del (sort_protocol_del_aux sort_protocol_del).
Proof. apply proto_unfold_eq, (fixpoint_unfold sort_protocol_del_aux). Qed.
Definition loop_sort_protocol_aux (rec : iProto Σ) : iProto Σ :=
((sort_protocol <++> rec) <+> ((<?> c, MSG c {{ c rec @ N }}; rec) <+> END))%proto.
Lemma sort_protocol_del_spec cmp c :
cmp_spec I R cmp -
{{{ c iProto_dual sort_protocol_del @ N }}}
sort_service_del cmp c
{{{ RET #(); c END @ N }}}.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (start_chan_proto_spec _ (sort_protocol I R <++> END)%proto);
iIntros (c') "Hc'".
{ wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
by iApply "HΨ".
Qed.
Instance loop_sort_protocol_aux_contractive : Contractive loop_sort_protocol_aux.
Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c rec @ N }}; rec) <+> END))%proto.
Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
Proof. solve_proto_contractive. Qed.
Definition loop_sort_protocol : iProto Σ := fixpoint loop_sort_protocol_aux.
Global Instance loop_sort_protocol_unfold :
ProtoUnfold loop_sort_protocol (loop_sort_protocol_aux loop_sort_protocol).
Proof. apply proto_unfold_eq, (fixpoint_unfold loop_sort_protocol_aux). Qed.
Lemma loop_sort_service_spec c :
{{{ c iProto_dual loop_sort_protocol @ N }}}
loop_sort_service c
Definition sort_protocol_br_del : iProto Σ := fixpoint sort_protocol_br_del_aux.
Global Instance sort_protocol_br_del_unfold :
ProtoUnfold sort_protocol_br_del (sort_protocol_br_del_aux sort_protocol_br_del).
Proof. apply proto_unfold_eq, (fixpoint_unfold sort_protocol_br_del_aux). Qed.
Lemma sort_service_br_del_spec cmp c :
cmp_spec I R cmp -
{{{ c iProto_dual sort_protocol_br_del @ N }}}
sort_service_br_del cmp c
{{{ RET #(); c END @ N }}}.
Proof.
iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
{ wp_apply (sort_service_spec with "Hc"); iIntros "Hc".
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. wp_branch; wp_pures.
{ wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
wp_branch; wp_pures.
{ wp_apply (start_chan_proto_spec N sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_apply ("IH" with "Hc'"); auto. }
wp_send with "[$Hc']".
by wp_apply ("IH" with "Hc"). }
wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
- wp_apply (start_chan_proto_spec N loop_sort_protocol); iIntros (d) "Hd".
{ wp_apply ("IH" with "Hd"); auto. }
wp_apply (send_proto_spec with "Hc"); simpl.
iExists d; iSplit; first done. iIntros "{$Hd} !> Hc".
by wp_apply ("IH" with "Hc").
- by iApply "HΨ".
by iApply "HΨ".
Qed.
End loop_sort.
\ No newline at end of file
End sort_service_br_del.
......@@ -2,7 +2,7 @@ From stdpp Require Import sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From actris.utils Require Import llist compare contribution.
From actris.examples Require Import map sort_elem sort_elem_client.
From actris.examples Require Import map sort_fg_client.
From iris.algebra Require Import gmultiset.
From Coq Require Import SetoidPermutation.
......@@ -80,7 +80,7 @@ Definition cmpZfst : val := λ: "x" "y", Fst "x" ≤ Fst "y".
Definition par_map_reduce : val := λ: "n" "map" "red" "xs",
let: "cmap" := start_map_service "n" "map" in
let: "csort" := start_chan (λ: "c", sort_elem_service cmpZfst "c") in
let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
par_map_reduce_map_server "n" "cmap" "csort" "xs";;
send "csort" #stop;;
let: "cred" := start_map_service "n" "red" in
......@@ -245,12 +245,12 @@ Section mapper.
{{{
llist IA l xs
cmap map_worker_protocol IA IZB map n (X : gmultiset A) @ N
csort sort_elem_head_protocol IZB RZB ys @ N
csort sort_fg_head_protocol IZB RZB ys @ N
}}}
par_map_reduce_map_server #n cmap csort #l
{{{ ys', RET #();
ys' (xs ++ elements X) = map
csort sort_elem_head_protocol IZB RZB (ys ++ ys') @ N
csort sort_fg_head_protocol IZB RZB (ys ++ ys') @ N
}}}.
Proof.
iIntros (Hn Φ) "(Hl & Hcmap & Hcsort) HΦ".
......@@ -269,7 +269,7 @@ Section mapper.
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
rewrite assoc_L -(comm _ [x]). iApply "HΦ".
- wp_recv (x k) as (Hx) "Hk".
rewrite -(right_id END%proto _ (sort_elem_head_protocol _ _ _)).
rewrite -(right_id END%proto _ (sort_fg_head_protocol _ _ _)).
wp_apply (send_all_spec with "[$Hk $Hcsort]"); iIntros "Hcsort".
rewrite right_id.
wp_apply ("IH" with "[] Hl Hcmap Hcsort"); first done.
......@@ -289,7 +289,7 @@ Section mapper.
i iys_sorted.*1
{{{
llist (IB i) l (reverse ys)
csort sort_elem_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys)) @ N
csort sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys)) @ N
}}}
par_map_reduce_collect csort #i #l
{{{ ys' miy, RET accv miy;
......@@ -297,7 +297,7 @@ Section mapper.
from_option (λ '(j,_,_), i j j iys_sorted.*1)
(iys_sorted ++ ((i,) <$> ys ++ ys') iys) miy
llist (IB i) l (reverse (ys ++ ys'))
csort from_option (λ _, sort_elem_tail_protocol IZB RZB iys
csort from_option (λ _, sort_fg_tail_protocol IZB RZB iys
((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)) END%proto miy @ N
from_option (λ '(i,y,w), IB i y w) True miy
}}}.
......@@ -338,7 +338,7 @@ Section mapper.
Sorted RZB (iys_sorted ++ acc miy)
{{{
llist IC l zs
csort from_option (λ _, sort_elem_tail_protocol IZB RZB iys
csort from_option (λ _, sort_fg_tail_protocol IZB RZB iys
(iys_sorted ++ acc miy)) END%proto miy @ N
cred map_worker_protocol IZBs IC (curry red) n (Y : gmultiset (Z * list B)) @ N
from_option (λ '(i,y,w), IB i y w) True miy
......@@ -398,9 +398,9 @@ Section mapper.
Proof.
iIntros (?) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
wp_apply (start_map_service_spec with "Hmap [//]"); iIntros (cmap) "Hcmap".
wp_apply (start_chan_proto_spec N (sort_elem_protocol IZB RZB <++> END)%proto);
wp_apply (start_chan_proto_spec N (sort_fg_protocol IZB RZB <++> END)%proto);
iIntros (csort) "Hcsort".
{ wp_apply (sort_elem_service_spec N with "[] Hcsort"); last by auto.
{ wp_apply (sort_service_fg_spec N with "[] Hcsort"); last by auto.
iApply RZB_cmp_spec. }
rewrite right_id.
wp_apply (par_map_reduce_map_server_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
......
......@@ -14,29 +14,41 @@ Definition lmerge : val :=
else lpop "zs";; "go" "cmp" "ys" "zs";; lcons "z" "ys".
Definition sort_service : val :=
rec: "go" "c" :=
let: "cmp" := recv "c" in
rec: "go" "cmp" "c" :=
let: "xs" := recv "c" in
if: llength "xs" #1 then send "c" #() else
let: "zs" := lsplit "xs" in
let: "cy" := start_chan "go" in
let: "cz" := start_chan "go" in
send "cy" "cmp";; send "cy" "xs";;
send "cz" "cmp";; send "cz" "zs";;
let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
send "cy" "xs";;
send "cz" "zs";;
recv "cy";; recv "cz";;
lmerge "cmp" "xs" "zs";;
send "c" #().
Definition sort_service_func : val := λ: "c",
let: "cmp" := recv "c" in
sort_service "cmp" "c".
Definition sort_client_func : val := λ: "cmp" "xs",
let: "c" := start_chan sort_service_func in
send "c" "cmp";; send "c" "xs";;
recv "c".
Section sort.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
Definition sort_protocol : iProto Σ :=
Definition sort_protocol {A} (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} : iProto Σ :=
(<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
<?> (xs' : list A), MSG #() {{ Sorted R xs' xs' xs llist I l xs' }};
END)%proto.
Definition sort_protocol_func : iProto Σ :=
(<!> A (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val),
MSG cmp {{ cmp_spec I R cmp }};
<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
<?> (xs' : list A), MSG #() {{ Sorted R xs' xs' xs llist I l xs' }};
END)%proto.
sort_protocol I R)%proto.
Lemma lmerge_spec {A} (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val) l1 l2 xs1 xs2 :
......@@ -72,13 +84,14 @@ Section sort.
wp_apply (lcons_spec with "[$Hl1 $HIx2]"); iIntros "Hl1". iApply "HΨ". iFrame.
Qed.
Lemma sort_service_spec p c :
{{{ c iProto_dual sort_protocol <++> p @ N }}}
sort_service c
Lemma sort_service_spec {A} (I : A val iProp Σ) (R : A A Prop)
`{!RelDecision R, !Total R} (cmp : val) p c :
cmp_spec I R cmp -
{{{ c iProto_dual (sort_protocol I R) <++> p @ N }}}
sort_service cmp c
{{{ RET #(); c p @ N }}}.
Proof.
iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
wp_recv (A I R ?? cmp) as "#Hcmp".
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
wp_recv (xs l) as "Hl".
wp_apply (llength_spec with "Hl"); iIntros "Hl".
wp_op; case_bool_decide as Hlen; wp_if.
......@@ -87,15 +100,13 @@ Section sort.
wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
iDestruct 1 as (->) "[Hl1 Hl2]".
wp_apply (start_chan_proto_spec N sort_protocol); iIntros (cy) "Hcy".
wp_apply (start_chan_proto_spec N (sort_protocol I R)); iIntros (cy) "Hcy".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcy"); auto. }
wp_apply (start_chan_proto_spec N sort_protocol); iIntros (cz) "Hcz".
wp_apply (start_chan_proto_spec N (sort_protocol I R)); iIntros (cz) "Hcz".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcz"); auto. }
wp_send with "[$Hcmp]".
wp_send with "[$Hl1]".
wp_send with "[$Hcmp]".
wp_send with "[$Hl2]".
wp_recv (ys1) as (??) "Hl1".
wp_recv (ys2) as (??) "Hl2".
......@@ -106,4 +117,31 @@ Section sort.
+ rewrite (merge_Permutation R). by f_equiv.
- by iApply "HΨ".
Qed.
Lemma sort_service_func_spec p c :
{{{ c iProto_dual sort_protocol_func <++> p @ N }}}
sort_service_func c
{{{ RET #(); c p @ N }}}.
Proof.
iIntros (Ψ) "Hc HΨ". wp_lam.
wp_recv (A I R ?? cmp) as "#Hcmp".
by wp_apply (sort_service_spec with "Hcmp Hc").
Qed.
Lemma sort_client_func_spec {A} (I : A val iProp Σ) R
`{!RelDecision R, !Total R} cmp l (xs : list A) :
cmp_spec I R cmp -
{{{ llist I l xs }}}
sort_client_func cmp #l
{{{ ys, RET #(); Sorted R ys ys xs llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_proto_spec N sort_protocol_func); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (sort_service_func_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
wp_send with "[$Hl]".
wp_recv (ys) as "(Hsorted & Hperm & Hl)".
wp_pures. iApply "HΦ"; iFrame.
Qed.
End sort.
From stdpp Require Import sorting.
From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From actris.examples Require Import sort.
Definition sort_client : val := λ: "cmp" "xs",
let: "c" := start_chan sort_service in
send "c" "cmp";; send "c" "xs";;
recv "c".
Section sort_client.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
Lemma sort_client_spec {A} (I : A val iProp Σ) R
`{!RelDecision R, !Total R} cmp l (xs : list A) :
cmp_spec I R cmp -
{{{ llist I l xs }}}
sort_client cmp #l
{{{ ys, RET #(); Sorted R ys ys xs llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (sort_service_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
wp_send with "[$Hl]".
wp_recv (ys) as "(Hsorted & Hperm & Hl)".
wp_pures. iApply "HΦ"; iFrame.
Qed.
End sort_client.
......@@ -3,7 +3,7 @@ From actris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
From actris.utils Require Import llist compare.
From actris.examples Require Import sort_elem.
From actris.examples Require Export sort_fg.
Definition send_all : val :=
rec: "go" "c" "xs" :=
......@@ -16,22 +16,20 @@ Definition recv_all : val :=
let: "x" := recv "c" in
let: "l" := "go" "c" in lcons "x" "l";; "l".
Definition sort_elem_client : val :=
λ: "cmp" "xs",
let: "c" := start_chan sort_elem_service_top in
send "c" "cmp";;
send_all "c" "xs";;
send "c" #stop;;
recv_all "c".
Definition sort_client_fg : val := λ: "cmp" "xs",
let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
send_all "c" "xs";;
send "c" #stop;;
recv_all "c".
Section sort_elem_client.
Section sort_fg_client.
Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
Context {A} (I : A val iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
Lemma send_all_spec c p xs' l xs :
{{{ llist I l xs c sort_elem_head_protocol I R xs' <++> p @ N }}}
{{{ llist I l xs c sort_fg_head_protocol I R xs' <++> p @ N }}}
send_all c #l
{{{ RET #(); c sort_elem_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
{{{ RET #(); c sort_fg_head_protocol I R (xs' ++ xs) <++> p @ N }}}.
Proof.
iIntros (Φ) "[Hl Hc] HΦ".
iInduction xs as [|x xs] "IH" forall (xs').
......@@ -44,7 +42,7 @@ Section sort_elem_client.
Lemma recv_all_spec c p xs ys' :
Sorted R ys'
{{{ c sort_elem_tail_protocol I R xs ys' <++> p @ N }}}
{{{ c sort_fg_tail_protocol I R xs ys' <++> p @ N }}}
recv_all c
{{{ l ys, RET #l;
Sorted R (ys' ++ ys) ys' ++ ys xs llist I l ys c p @ N
......@@ -62,22 +60,20 @@ Section sort_elem_client.
iApply ("HΦ" $! _ []); rewrite /= right_id_L; by iFrame.
Qed.
Lemma sort_client_spec cmp l xs :
Lemma sort_client_fg_spec cmp l xs :
cmp_spec I R cmp -
{{{ llist I l xs }}}
sort_elem_client cmp #l
sort_client_fg cmp #l
{{{ k ys, RET #k; Sorted R ys ys xs llist I k ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
wp_apply (start_chan_proto_spec N (sort_elem_top_protocol <++> END)%proto);
wp_apply (start_chan_proto_spec N (sort_fg_protocol I R <++> END)%proto);
iIntros (c) "Hc".
{ wp_apply (sort_elem_service_top_spec N with "Hc"); auto. }
rewrite /sort_elem_top_protocol.
wp_send (A I R) with "[$Hcmp]".
{ wp_apply (sort_service_fg_spec N with "Hcmp Hc"); auto. }
wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "Hc".
wp_select.
wp_apply (recv_all_spec with "Hc"); auto.
iIntros (k ys) "/=". iDestruct 1 as (??) "[Hk _]".
iApply "HΦ"; auto with iFrame.
Qed.
End sort_elem_client.
End sort_fg_client.
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