Skip to content
GitLab
Commit 0f4e744e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tactics `wp_send` and `wp_recv`.

parent 2c2ed933
Hide whitespace changes
Inline Side-by-side
_CoqProject
View file @ 0f4e744e
......@@ -7,6 +7,7 @@ theories/utils/compare.v
theories/channel/channel.v
theories/channel/proto_model.v
theories/channel/proto_channel.v
theories/channel/proofmode.v
theories/examples/list_sort.v
theories/examples/list_sort_instances.v
theories/examples/list_sort_elem.v
......
theories/examples/list_sort.v
View file @ 0f4e744e
From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel.
From osiris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From osiris.utils Require Import list compare.
......@@ -89,17 +89,14 @@ Section list_sort.
Proof.
iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ).
wp_lam.
wp_apply (recv_proto_spec with "Hc"); simpl.
iIntros (A I R ?? cmp) "/= Hc #Hcmp".
wp_apply (recv_proto_spec with "Hc"); simpl.
iIntros (xs l vs) "/= Hc [Hl HI]".
wp_recv (A I R ?? cmp) with "#Hcmp".
wp_recv (xs l vs) with "[Hl HI]".
wp_load. wp_apply (llength_spec (A:=val) with "[//]"); iIntros (_).
iDestruct (big_sepL2_length with "HI") as %<-.
wp_op; case_bool_decide as Hlen; wp_if.
{ assert (Sorted R xs).
{ destruct xs as [|x1 [|x2 xs]]; simpl in *; eauto with lia. }
wp_apply (send_proto_spec with "Hc"); simpl.
iExists xs, vs; iSplit; first done. eauto 10 with iFrame. }
wp_send with "[$Hl $HI]"; first by auto. by iApply "HΨ". }
wp_load. wp_apply (lsplit_spec (A:=val) with "[//]"); iIntros (vs1 vs2 <-).
wp_alloc l1 as "Hl1"; wp_alloc l2 as "Hl2".
iDestruct (big_sepL2_app_inv_r with "HI") as (xs1 xs2 ->) "[HI1 HI2]".
......@@ -109,26 +106,20 @@ Section list_sort.
wp_apply (start_chan_proto_spec N sort_protocol); iIntros (cz) "Hcz".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcz"); auto. }
wp_apply (send_proto_spec with "Hcy"); simpl.
iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcy".
wp_apply (send_proto_spec with "Hcy"); simpl.
iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} !> Hcy".
wp_apply (send_proto_spec with "Hcz"); simpl.
iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcz".
wp_apply (send_proto_spec with "Hcz"); simpl.
iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} !> Hcz".
wp_apply (recv_proto_spec with "Hcy"); simpl.
iIntros (ys1 ws1) "_". iDestruct 1 as (??) "[Hl1 HI1]".
wp_apply (recv_proto_spec with "Hcz"); simpl.
iIntros (ys2 ws2) "_". iDestruct 1 as (??) "[Hl2 HI2]".
wp_send with "[$Hcmp]".
wp_send with "[$Hl1 $HI1]".
wp_send with "[$Hcmp]".
wp_send with "[$Hl2 $HI2]".
wp_recv (ys1 ws1) with (??) "[Hl1 HI1]".
wp_recv (ys2 ws2) with (??) "[Hl2 HI2]".
do 2 wp_load.
wp_apply (lmerge_spec with "Hcmp [$HI1 $HI2]"). iIntros (ws) "HI".
wp_store.
wp_apply (send_proto_spec with "Hc"); simpl.
iExists (list_merge R ys1 ys2), ws.
iSplit; first done. iFrame. iSplit; iPureIntro.
- by apply (Sorted_list_merge _).
- rewrite (merge_Permutation R). by f_equiv.
wp_send ((list_merge R ys1 ys2) ws) with "[$Hl $HI]".
- iSplit; iPureIntro.
+ by apply (Sorted_list_merge _).
+ rewrite (merge_Permutation R). by f_equiv.
- by iApply "HΨ".
Qed.
Lemma list_sort_client_spec {A} (I : A → val → iProp Σ) R
......@@ -143,17 +134,9 @@ Section list_sort.
wp_apply (start_chan_proto_spec N sort_protocol); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (list_sort_service_spec with "Hc"); auto. }
wp_apply (send_proto_spec with "Hc"); simpl.
iExists _, I, R, _, _, cmp.
iSplitR=> //.
iSplitR=> //.
iIntros "!> Hc".
wp_apply (send_proto_spec with "Hc"); simpl.
iExists xs, l, vs.
iSplitR=> //.
iIntros "{$Hl} !> Hc".
wp_apply (recv_proto_spec with "Hc"); simpl.
iIntros (ys ws) "Hc (Hsorted & Hperm & Hl & HI)".
wp_pures. iApply "HΦ". iFrame.
wp_send with "[$Hcmp]".
wp_send with "[$Hl]".
wp_recv (ys ws) with "(Hsorted & Hperm & Hl & HI)".
wp_pures. iApply "HΦ"; iFrame.
Qed.
End list_sort.
theories/examples/list_sort_elem.v
View file @ 0f4e744e
From stdpp Require Import sorting.
From osiris.channel Require Import proto_channel.
From osiris.channel Require Import proto_channel proofmode.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Import assert.
From osiris.utils Require Import list compare.
......@@ -93,10 +93,9 @@ Section list_sort_elem.
Proof.
iIntros (Ψ) "(Hc & Hc1 & Hc2) HΨ". iLöb as "IH" forall (c c1 c2 xs xs1 xs2 Ψ).
wp_rec. wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
- wp_apply (recv_proto_spec with "Hc"); iIntros (x v) "/= Hc HI".
- wp_recv (x v) with "HI".
wp_apply (select_spec with "[$Hc1]")=> //=; iIntros "Hc1".
wp_apply (send_proto_spec with "Hc1"); simpl.
iExists x, v. iSplit; [done|]. iIntros "{$HI} !> Hc1".
wp_send with "[$HI]".
wp_apply ("IH" with "Hc Hc2 Hc1").
iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hc2 & Hc1)".
rewrite -!(assoc_L (++)).
......@@ -121,12 +120,9 @@ Section list_sort_elem.
iIntros (Hxs Hys Hsorted Hrel Ψ) "[Hc Hcin] HΨ".
iLöb as "IH" forall (c cin xs ys xs' ys' Hxs Hys Hsorted Hrel).
wp_rec. wp_apply (branch_spec with "Hcin"); iIntros ([]) "[Hcin Hys']".
- iClear "Hys'".
wp_apply (recv_proto_spec with "Hcin"); iIntros (x v) "/= Hcin".
iDestruct 1 as (Hx) "HI".
- iClear "Hys'". wp_recv (x v) with (Htl) "HI".
wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_apply (send_proto_spec with "Hc"); simpl.
iExists x, v. iFrame "HI". do 2 (iSplit; [by auto|]); iIntros "!> Hc".
wp_send with "[$HI]"; first by auto.
wp_apply ("IH" with "[%] [%] [%] [%] Hc Hcin HΨ").
{ done. }
{ by rewrite Hys -!assoc_L (comm _ zs). }
......@@ -158,13 +154,11 @@ Section list_sort_elem.
iLöb as "IH" forall (c1 c2 xs1 xs2 ys y1 w1 ys1 ys2 Hxs Hys Hsort Htl Htl_le).
wp_rec. wp_apply (branch_spec with "[$Hc2]"); iIntros ([]) "[Hc2 Hys2]".
- iClear "Hys2".
wp_apply (recv_proto_spec with "Hc2"); iIntros (x v) "/= Hc2".
iDestruct 1 as (Htl2) "HIx".
wp_recv (x v) with (Htl2) "HIx".
wp_pures. wp_apply ("Hcmp" with "[$HIy1 $HIx]"); iIntros "[HIy1 HIx]".
case_bool_decide.
+ wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_apply (send_proto_spec with "Hc"); simpl.
iExists y1, w1. iFrame "HIy1". do 2 (iSplit; [done|]); iIntros "!> Hc".
wp_send with "[$HIy1 //]".
wp_apply ("IH" with "[%] [%] [%] [%] [%] Hc Hc2 Hc1 HIx").
{ by rewrite comm. }
{ by rewrite assoc (comm _ ys2) Hys. }
......@@ -174,10 +168,8 @@ Section list_sort_elem.
inversion 1; discriminate_list || simplify_list_eq. by constructor. }
iIntros "(?&?&?)". iApply "HΨ"; iFrame.
+ wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_apply (send_proto_spec with "Hc"); simpl.
iExists x, v. iFrame "HIx". iSplit; [done|]; iSplit.
wp_send with "[$HIx]".
{ iPureIntro. by apply Htl_le, total_not. }
iIntros "!> Hc".
wp_apply ("IH" with "[% //] [%] [%] [%] [%] Hc Hc1 Hc2 HIy1 HΨ").
{ by rewrite Hys assoc. }
{ rewrite fmap_app. by apply Sorted_snoc, Htl_le, total_not. }
......@@ -186,8 +178,7 @@ Section list_sort_elem.
inversion 1; discriminate_list || simplify_list_eq. by constructor. }
- iDestruct "Hys2" as %Hys2.
wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_apply (send_proto_spec with "Hc"); simpl.
iExists y1, w1. iFrame "HIy1". do 2 (iSplit; [done|]); iIntros "!> Hc".
wp_send with "[$HIy1 //]".
wp_apply (list_sort_elem_service_move_spec with "[$Hc $Hc1]").
{ done. }
{ by rewrite Hys Hys2 -!assoc_L (comm _ xs2). }
......@@ -206,9 +197,9 @@ Section list_sort_elem.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec; wp_pures.
wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
- wp_apply (recv_proto_spec with "Hc"); iIntros (x1 v1) "/= Hc HIx1".
- wp_recv (x1 v1) with "HIx1".
wp_apply (branch_spec with "Hc"); iIntros ([]) "[Hc _]"; wp_pures.
+ wp_apply (recv_proto_spec with "Hc"); iIntros (x2 v2) "/= Hc HIx2".
+ wp_recv (x2 v2) with "HIx2".
wp_apply (start_chan_proto_spec N list_sort_elem_protocol).
{ iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"); auto. }
iIntros (cy) "Hcy".
......@@ -216,26 +207,23 @@ Section list_sort_elem.
{ iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
iIntros (cz) "Hcz".
wp_apply (select_spec with "[$Hcy]")=> //; iIntros "Hcy".
wp_apply (send_proto_spec with "Hcy")=> //=.
iExists x1, v1. iFrame "HIx1". iSplit; [done|]; iIntros "!> Hcy".
wp_send with "[$HIx1]".
wp_apply (select_spec with "[$Hcz]")=> //; iIntros "Hcz".
wp_apply (send_proto_spec with "Hcz")=> //=.
iExists x2, v2. iFrame "HIx2". iSplit; [done|]; iIntros "!> Hcz".
wp_send with "[$HIx2]".
wp_apply (list_sort_elem_service_split_spec with "[$Hc $Hcy $Hcz]").
iIntros (xs' xs1' xs2'); iDestruct 1 as (Hxs') "(Hc & Hcy & Hcz) /=".
wp_apply (branch_spec with "Hcy"); iIntros (b) "[Hcy Hnil]".
destruct b; last first.
{ by iDestruct "Hnil" as %?%Permutation_nil_cons. }
iClear "Hnil".
wp_apply (recv_proto_spec with "Hcy"); iIntros (x v) "/= Hcy [_ HIx]".
wp_recv (x v) with "[_ HIx]".
wp_apply (list_sort_elem_service_merge_spec _ _ _ _ _ [] _ _ _ _ [] []
with "Hcmp [$Hc $Hcy $Hcz $HIx]"); simpl; auto using TlRel_nil, Sorted_nil.
{ by rewrite Hxs' Permutation_middle. }
iIntros "(Hc & Hcy & Hcz)". by iApply "HΨ".
+ wp_apply (select_spec with "[$Hc]")=> //=; iIntros "Hc".
wp_apply (send_proto_spec with "Hc"); simpl.
iExists x1, v1. iFrame "HIx1". do 2 (iSplit; [by auto using TlRel_nil|]).
iIntros "!> Hc". by wp_apply (select_spec with "[$Hc]").
wp_send with "[$HIx1]"; first by auto using TlRel_nil.
by wp_apply (select_spec with "[$Hc]").
- by wp_apply (select_spec with "[$Hc]").
Qed.
End list_sort_elem.
Supports Markdown
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