sort.v 4.75 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.
4
From actris.utils Require Export llist 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")).
15
*) Admitted.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

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

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

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

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

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