sort.v 4.81 KB
Newer Older
1
From stdpp Require Import sorting.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From actris.channel Require Import proto_channel proofmode.
3
From iris.heap_lang Require Import proofmode notation.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From actris.utils Require Import list compare.
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6

Definition lmerge : val :=
7 8 9 10 11 12 13 14
  rec: "go" "cmp" "ys" "zs" :=
    if: lisnil "ys" then "zs" else
    if: lisnil "zs" then "ys" else
    let: "y" := lhead "ys" in
    let: "z" := lhead "zs" in
    if: "cmp" "y" "z"
    then lcons "y" ("go" "cmp" (ltail "ys") "zs")
    else lcons "z" ("go" "cmp" "ys" (ltail "zs")).
Robbert Krebbers's avatar
Robbert Krebbers committed
15

Robbert Krebbers's avatar
Robbert Krebbers committed
16
Definition sort_service : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
17 18 19
  rec: "go" "c" :=
    let: "cmp" := recv "c" in
    let: "xs" := recv "c" in
Robbert Krebbers's avatar
Robbert Krebbers committed
20
    if: llength !"xs"  #1 then send "c" #() else
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22 23
    let: "ys_zs" := lsplit !"xs" in
    let: "ys" := ref (Fst "ys_zs") in
    let: "zs" := ref (Snd "ys_zs") in
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27 28
    let: "cy" := start_chan "go" in
    let: "cz" := start_chan "go" in
    send "cy" "cmp";; send "cy" "ys";;
    send "cz" "cmp";; send "cz" "zs";;
    recv "cy";; recv "cz";;
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30 31
    "xs" <- lmerge "cmp" !"ys" !"zs";;
    send "c" #().

Robbert Krebbers's avatar
Robbert Krebbers committed
32
Section sort.
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35
  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).

  Definition sort_protocol : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
36
    (<!> A (I : A  val  iProp Σ) (R : A  A  Prop)
37
         `{!RelDecision R, !Total R} (cmp : val),
Robbert Krebbers's avatar
Robbert Krebbers committed
38
       MSG cmp {{ cmp_spec I R cmp }};
Robbert Krebbers's avatar
Robbert Krebbers committed
39
     <!> (xs : list A) (l : loc) (vs : list val),
40
       MSG #l {{ l  llist vs  [ list] x;v  xs;vs, I x v }};
Robbert Krebbers's avatar
Robbert Krebbers committed
41
     <?> (xs' : list A) (vs' : list val),
Robbert Krebbers's avatar
Robbert Krebbers committed
42
       MSG #() {{  Sorted R xs'    xs'  xs  
43
                  l  llist vs'  [ list] x;v  xs';vs', I x v }};
Robbert Krebbers's avatar
Robbert Krebbers committed
44
     END)%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46

  Lemma lmerge_spec {A} (I : A  val  iProp Σ) (R : A  A  Prop)
47
      `{!RelDecision R, !Total R} (cmp : val) xs1 xs2 vs1 vs2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
    cmp_spec I R cmp -
    {{{ ([ list] x;v  xs1;vs1, I x v)  ([ list] x;v  xs2;vs2, I x v) }}}
50 51
      lmerge cmp (llist vs1) (llist vs2)
    {{{ ws, RET llist ws; [ list] x;v  list_merge R xs1 xs2;ws, I x v }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53
  Proof.
    iIntros "#Hcmp" (Ψ) "!> [HI1 HI2] HΨ". iLöb as "IH" forall (xs1 xs2 vs1 vs2 Ψ).
54
    wp_lam. wp_apply (lisnil_spec with "[//]"); iIntros (_).
55 56
    destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; done || wp_pures.
    { iApply "HΨ". by rewrite list_merge_nil_l. }
57
    wp_apply (lisnil_spec with "[//]"); iIntros (_).
58 59
    destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; done || wp_pures.
    { iApply "HΨ". iFrame. }
60 61
    wp_apply (lhead_spec with "[//]"); iIntros (_).
    wp_apply (lhead_spec with "[//]"); iIntros (_).
Robbert Krebbers's avatar
Robbert Krebbers committed
62 63 64 65
    iDestruct "HI1" as "[HI1 HI1']"; iDestruct "HI2" as "[HI2 HI2']".
    wp_apply ("Hcmp" with "[$HI1 $HI2]"); iIntros "[HI1 HI2]".
    case_bool_decide; wp_pures.
    - rewrite decide_True //.
66
      wp_apply (ltail_spec with "[//]"); iIntros (_).
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68
      wp_apply ("IH" $! _ (x2 :: _) with "HI1'[HI2 HI2']"); [simpl; iFrame|].
      iIntros (ws) "HI".
69
      wp_apply (lcons_spec with "[//]"); iIntros (_).
Robbert Krebbers's avatar
Robbert Krebbers committed
70 71
      iApply "HΨ". iFrame.
    - rewrite decide_False //.
72
      wp_apply (ltail_spec with "[//]"); iIntros (_).
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74
      wp_apply ("IH" $! (x1 :: _) with "[HI1 HI1'] HI2'"); [simpl; iFrame|].
      iIntros (ws) "HI".
75
      wp_apply (lcons_spec with "[//]"); iIntros (_).
Robbert Krebbers's avatar
Robbert Krebbers committed
76 77
      iApply "HΨ". iFrame.
  Qed.
78

Robbert Krebbers's avatar
Robbert Krebbers committed
79
  Lemma sort_service_spec p c :
Robbert Krebbers's avatar
Robbert Krebbers committed
80
    {{{ c  iProto_dual sort_protocol <++> p @ N }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
81
      sort_service c
Robbert Krebbers's avatar
Robbert Krebbers committed
82
    {{{ RET #(); c  p @ N }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
    iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    wp_lam.
86 87
    wp_recv (A I R ?? cmp) as "#Hcmp".
    wp_recv (xs l vs) as "[Hl HI]".
88
    wp_load. wp_apply (llength_spec with "[//]"); iIntros (_).
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90 91 92
    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. }
93
      wp_send with "[$Hl $HI]"; first by auto. by iApply "HΨ". }
94
    wp_load. wp_apply (lsplit_spec with "[//]"); iIntros (vs1 vs2 ->).
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96
    wp_alloc l1 as "Hl1"; wp_alloc l2 as "Hl2".
    iDestruct (big_sepL2_app_inv_r with "HI") as (xs1 xs2 ->) "[HI1 HI2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98 99 100 101 102
    wp_apply (start_chan_proto_spec N sort_protocol); 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".
    { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
      wp_apply ("IH" with "Hcz"); auto. }
103 104 105 106
    wp_send with "[$Hcmp]".
    wp_send with "[$Hl1 $HI1]".
    wp_send with "[$Hcmp]".
    wp_send with "[$Hl2 $HI2]".
107 108
    wp_recv (ys1 ws1) as (??) "[Hl1 HI1]".
    wp_recv (ys2 ws2) as (??) "[Hl2 HI2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    do 2 wp_load.
110
    wp_apply (lmerge_spec with "Hcmp [$HI1 $HI2]"). iIntros (ws) "HI".
Robbert Krebbers's avatar
Robbert Krebbers committed
111
    wp_store.
112 113 114 115 116
    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Ψ".
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
End sort.